69 |
69 |
70 lemma alpha5_symp: |
70 lemma alpha5_symp: |
71 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
71 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
72 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
72 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
73 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
74 apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) |
|
75 (* |
|
76 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
74 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
77 apply (simp_all add: alpha5_inj) |
75 apply (simp only: alpha5_inj) |
|
76 apply (simp add: alpha5_inj) |
78 apply (erule exE) |
77 apply (erule exE) |
|
78 apply (simp only: alpha5_inj) |
79 apply (rule_tac x="- pi" in exI) |
79 apply (rule_tac x="- pi" in exI) |
80 apply (simp add: alpha_gen) |
80 apply (erule alpha_gen_compose_sym2) |
81 apply(simp add: fresh_star_def fresh_minus_perm) |
81 apply (simp_all add: alpha5_inj eqvts alpha5_eqvt) |
82 apply clarify |
|
83 apply (rule conjI) |
|
84 apply (rotate_tac 3) |
|
85 apply (frule_tac p="- pi" in alpha5_eqvt(2)) |
|
86 apply simp |
|
87 apply (rule conjI) |
|
88 apply (rotate_tac 5) |
|
89 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
|
90 apply simp |
|
91 apply (rotate_tac 6) |
|
92 apply simp |
|
93 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) |
|
94 apply (simp)*) |
|
95 done |
82 done |
96 |
83 |
97 lemma alpha5_transp: |
84 lemma alpha5_transp: |
98 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
85 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
99 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
86 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
100 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))" |
87 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))" |
101 (*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) |
88 apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *}) |
102 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
|
103 apply (rule_tac [!] allI) |
|
104 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
105 apply (simp_all add: alpha5_inj) |
|
106 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
107 apply (simp_all add: alpha5_inj) |
|
108 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
109 apply (simp_all add: alpha5_inj) |
|
110 defer |
|
111 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
112 apply (simp_all add: alpha5_inj) |
|
113 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
|
114 apply (simp_all add: alpha5_inj) |
|
115 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
|
116 (* HERE *) |
|
117 apply (simp add: alpha_gen) |
|
118 apply clarify |
|
119 apply(simp add: fresh_star_plus) |
|
120 apply (rule conjI) |
|
121 apply (erule_tac x="- pi \<bullet> rltsaa" in allE) |
|
122 apply (rotate_tac 5) |
|
123 apply (drule_tac p="- pi" in alpha5_eqvt(2)) |
|
124 apply simp |
|
125 apply (drule_tac p="pi" in alpha5_eqvt(2)) |
|
126 apply simp |
|
127 apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE) |
|
128 apply (rotate_tac 7) |
|
129 apply (drule_tac p="- pi" in alpha5_eqvt(1)) |
|
130 apply simp |
|
131 apply (rotate_tac 3) |
|
132 apply (drule_tac p="pi" in alpha5_eqvt(1)) |
|
133 apply simp |
|
134 done |
89 done |
135 |
90 |
136 lemma alpha5_equivp: |
91 lemma alpha5_equivp: |
137 "equivp alpha_rtrm5" |
92 "equivp alpha_rtrm5" |
138 "equivp alpha_rlts" |
93 "equivp alpha_rlts" |