1(* Title: HOL/HOLCF/IOA/ex/TrivEx.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Trivial Abstraction Example\<close> 6 7theory TrivEx 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,{},{})" 27 28definition 29 A_asig :: "action signature" where 30 "A_asig = ({},{INC},{})" 31definition 32 A_trans :: "(action, bool)transition set" where 33 "A_trans = 34 {tr. let s = fst(tr); 35 t = snd(snd(tr)) 36 in case fst(snd(tr)) 37 of 38 INC => t = True}" 39definition 40 A_ioa :: "(action, bool)ioa" where 41 "A_ioa = (A_asig, {False}, A_trans,{},{})" 42 43definition 44 h_abs :: "nat => bool" where 45 "h_abs n = (n~=0)" 46 47axiomatization where 48 MC_result: "validIOA A_ioa (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)" 49 50lemma h_abs_is_abstraction: 51 "is_abstraction h_abs C_ioa A_ioa" 52apply (unfold is_abstraction_def) 53apply (rule conjI) 54txt \<open>start states\<close> 55apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def) 56txt \<open>step case\<close> 57apply (rule allI)+ 58apply (rule imp_conj_lemma) 59apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def) 60apply (induct_tac "a") 61apply (simp add: h_abs_def) 62done 63 64lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)" 65apply (rule AbsRuleT1) 66apply (rule h_abs_is_abstraction) 67apply (rule MC_result) 68apply abstraction 69apply (simp add: h_abs_def) 70done 71 72end 73