Up to index of Isabelle/HOLCF/IOA/ex
theory TrivEx2(* Title: HOLCF/IOA/TrivEx.thy ID: $Id: TrivEx2.thy,v 1.4 2005/09/03 14:50:26 wenzelm Exp $ Author: Olaf Müller *) header {* Trivial Abstraction Example with fairness *} theory TrivEx2 imports IOA Abstraction begin datatype action = INC consts C_asig :: "action signature" C_trans :: "(action, nat)transition set" C_ioa :: "(action, nat)ioa" C_live_ioa :: "(action, nat)live_ioa" A_asig :: "action signature" A_trans :: "(action, bool)transition set" A_ioa :: "(action, bool)ioa" A_live_ioa :: "(action, bool)live_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,{},{})" C_live_ioa_def: "C_live_ioa == (C_ioa, WF C_ioa {INC})" 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,{},{})" A_live_ioa_def: "A_live_ioa == (A_ioa, WF A_ioa {INC})" h_abs_def: "h_abs n == n~=0" axioms MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(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 Enabled_implication:
Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s
theorem h_abs_is_liveabstraction:
is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})
theorem TrivEx2_abstraction:
validLIOA C_live_ioa (<> [] <%(n, a, m). n ≠ 0>)