equal
deleted
inserted
replaced
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}) (<>[] <%(b,a,c). b>)" |
54 MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box><%(b,a,c). b>)" |
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 (<>[] <%(n,a,m). n~=0>)" |
93 "validLIOA C_live_ioa (\<diamond>\<box><%(n,a,m). n~=0>)" |
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 |