equal
deleted
inserted
replaced
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) |