1(* Title: HOL/HOLCF/IOA/ex/TrivEx2.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Trivial Abstraction Example with fairness\<close> 6 7theory TrivEx2 8imports IOA.Abstraction 9begin 10 11datatype action = INC 12 13definition 14 C_asig :: "action signature" where 15 "C_asig = ({},{INC},{})" 16definition 17 C_trans :: "(action, nat)transition set" where 18 "C_trans = 19 {tr. let s = fst(tr); 20 t = snd(snd(tr)) 21 in case fst(snd(tr)) 22 of 23 INC => t = Suc(s)}" 24definition 25 C_ioa :: "(action, nat)ioa" where 26 "C_ioa = (C_asig, {0}, C_trans,{},{})" 27definition 28 C_live_ioa :: "(action, nat)live_ioa" where 29 "C_live_ioa = (C_ioa, WF C_ioa {INC})" 30 31definition 32 A_asig :: "action signature" where 33 "A_asig = ({},{INC},{})" 34definition 35 A_trans :: "(action, bool)transition set" where 36 "A_trans = 37 {tr. let s = fst(tr); 38 t = snd(snd(tr)) 39 in case fst(snd(tr)) 40 of 41 INC => t = True}" 42definition 43 A_ioa :: "(action, bool)ioa" where 44 "A_ioa = (A_asig, {False}, A_trans,{},{})" 45definition 46 A_live_ioa :: "(action, bool)live_ioa" where 47 "A_live_ioa = (A_ioa, WF A_ioa {INC})" 48 49definition 50 h_abs :: "nat => bool" where 51 "h_abs n = (n~=0)" 52 53axiomatization where 54 MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)" 55 56 57lemma h_abs_is_abstraction: 58"is_abstraction h_abs C_ioa A_ioa" 59apply (unfold is_abstraction_def) 60apply (rule conjI) 61txt \<open>start states\<close> 62apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def) 63txt \<open>step case\<close> 64apply (rule allI)+ 65apply (rule imp_conj_lemma) 66apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def) 67apply (induct_tac "a") 68apply (simp (no_asm) add: h_abs_def) 69done 70 71 72lemma Enabled_implication: 73 "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s" 74 apply (unfold Enabled_def enabled_def h_abs_def A_ioa_def C_ioa_def A_trans_def 75 C_trans_def trans_of_def) 76 apply auto 77 done 78 79 80lemma h_abs_is_liveabstraction: 81"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})" 82apply (unfold is_live_abstraction_def) 83apply auto 84txt \<open>is_abstraction\<close> 85apply (rule h_abs_is_abstraction) 86txt \<open>temp_weakening\<close> 87apply abstraction 88apply (erule Enabled_implication) 89done 90 91 92lemma TrivEx2_abstraction: 93 "validLIOA C_live_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)" 94apply (unfold C_live_ioa_def) 95apply (rule AbsRuleT2) 96apply (rule h_abs_is_liveabstraction) 97apply (rule MC_result) 98apply abstraction 99apply (simp add: h_abs_def) 100done 101 102end 103