Up to index of Isabelle/HOLCF/IOA/ex
theory TrivEx(* Title: HOLCF/IOA/TrivEx.thy ID: $Id: TrivEx.thy,v 1.4 2005/09/03 14:50:26 wenzelm Exp $ Author: Olaf Müller *) header {* Trivial Abstraction Example *} theory TrivEx imports Abstraction begin datatype action = INC consts C_asig :: "action signature" C_trans :: "(action, nat)transition set" C_ioa :: "(action, nat)ioa" A_asig :: "action signature" A_trans :: "(action, bool)transition set" A_ioa :: "(action, bool)ioa" h_abs :: "nat => bool" defs C_asig_def: "C_asig == ({},{INC},{})" C_trans_def: "C_trans == {tr. let s = fst(tr); t = snd(snd(tr)) in case fst(snd(tr)) of INC => t = Suc(s)}" C_ioa_def: "C_ioa == (C_asig, {0}, C_trans,{},{})" A_asig_def: "A_asig == ({},{INC},{})" A_trans_def: "A_trans == {tr. let s = fst(tr); t = snd(snd(tr)) in case fst(snd(tr)) of INC => t = True}" A_ioa_def: "A_ioa == (A_asig, {False}, A_trans,{},{})" h_abs_def: "h_abs n == n~=0" axioms MC_result: "validIOA A_ioa (<>[] <%(b,a,c). b>)" ML {* use_legacy_bindings (the_context ()) *} end
theorem h_abs_is_abstraction:
is_abstraction h_abs C_ioa A_ioa
theorem TrivEx_abstraction:
validIOA C_ioa (<> [] <%(n, a, m). n ≠ 0>)