src/HOL/HOLCF/IOA/ex/TrivEx.thy
changeset 62004 8c6226d88ced
parent 62002 f1599e98c4d0
child 62009 ecb5212d5885
equal deleted inserted replaced
62003:ba465fcd0267 62004:8c6226d88ced
    43 definition
    43 definition
    44   h_abs :: "nat => bool" where
    44   h_abs :: "nat => bool" where
    45   "h_abs n = (n~=0)"
    45   "h_abs n = (n~=0)"
    46 
    46 
    47 axiomatization where
    47 axiomatization where
    48   MC_result: "validIOA A_ioa (\<diamond>\<box><%(b,a,c). b>)"
    48   MC_result: "validIOA A_ioa (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
    49 
    49 
    50 lemma h_abs_is_abstraction:
    50 lemma h_abs_is_abstraction:
    51   "is_abstraction h_abs C_ioa A_ioa"
    51   "is_abstraction h_abs C_ioa A_ioa"
    52 apply (unfold is_abstraction_def)
    52 apply (unfold is_abstraction_def)
    53 apply (rule conjI)
    53 apply (rule conjI)
    59 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
    59 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
    60 apply (induct_tac "a")
    60 apply (induct_tac "a")
    61 apply (simp add: h_abs_def)
    61 apply (simp add: h_abs_def)
    62 done
    62 done
    63 
    63 
    64 lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box><%(n,a,m). n~=0>)"
    64 lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
    65 apply (rule AbsRuleT1)
    65 apply (rule AbsRuleT1)
    66 apply (rule h_abs_is_abstraction)
    66 apply (rule h_abs_is_abstraction)
    67 apply (rule MC_result)
    67 apply (rule MC_result)
    68 apply abstraction
    68 apply abstraction
    69 apply (simp add: h_abs_def)
    69 apply (simp add: h_abs_def)