src/HOL/HOLCF/IOA/ex/TrivEx2.thy
changeset 62004 8c6226d88ced
parent 62002 f1599e98c4d0
child 62009 ecb5212d5885
equal deleted inserted replaced
62003:ba465fcd0267 62004:8c6226d88ced
    49 definition
    49 definition
    50   h_abs :: "nat => bool" where
    50   h_abs :: "nat => bool" where
    51   "h_abs n = (n~=0)"
    51   "h_abs n = (n~=0)"
    52 
    52 
    53 axiomatization where
    53 axiomatization where
    54   MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box><%(b,a,c). b>)"
    54   MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
    55 
    55 
    56 
    56 
    57 lemma h_abs_is_abstraction:
    57 lemma h_abs_is_abstraction:
    58 "is_abstraction h_abs C_ioa A_ioa"
    58 "is_abstraction h_abs C_ioa A_ioa"
    59 apply (unfold is_abstraction_def)
    59 apply (unfold is_abstraction_def)
    88 apply (erule Enabled_implication)
    88 apply (erule Enabled_implication)
    89 done
    89 done
    90 
    90 
    91 
    91 
    92 lemma TrivEx2_abstraction:
    92 lemma TrivEx2_abstraction:
    93   "validLIOA C_live_ioa (\<diamond>\<box><%(n,a,m). n~=0>)"
    93   "validLIOA C_live_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
    94 apply (unfold C_live_ioa_def)
    94 apply (unfold C_live_ioa_def)
    95 apply (rule AbsRuleT2)
    95 apply (rule AbsRuleT2)
    96 apply (rule h_abs_is_liveabstraction)
    96 apply (rule h_abs_is_liveabstraction)
    97 apply (rule MC_result)
    97 apply (rule MC_result)
    98 apply abstraction
    98 apply abstraction