equal
deleted
inserted
replaced
55 done |
55 done |
56 |
56 |
57 lemma alpha5_reflp: |
57 lemma alpha5_reflp: |
58 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
58 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
59 apply (rule rtrm5_rlts.induct) |
59 apply (rule rtrm5_rlts.induct) |
|
60 thm rtrm5_rlts.induct |
|
61 alpha_rtrm5_alpha_rlts_alpha_rbv5.induct |
60 apply (simp_all add: alpha5_inj) |
62 apply (simp_all add: alpha5_inj) |
61 apply (rule_tac x="0::perm" in exI) |
63 apply (rule_tac x="0::perm" in exI) |
62 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
64 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
63 done |
65 done |
64 |
66 |
65 lemma alpha5_symp: |
67 lemma alpha5_symp: |
66 "(a \<approx>5 b \<longrightarrow> a \<approx>5 b) \<and> |
68 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
67 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
69 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
68 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
70 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
69 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
71 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
|
72 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct |
|
73 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros |
70 apply (simp_all add: alpha5_inj) |
74 apply (simp_all add: alpha5_inj) |
71 sorry |
75 sorry |
72 |
76 |
73 lemma alpha5_equivp: |
77 lemma alpha5_equivp: |
74 "equivp alpha_rtrm5" |
78 "equivp alpha_rtrm5" |