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 *}) |
74 apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *}) |
75 (* |
75 done |
|
76 |
|
77 lemma alpha5_symp1: |
|
78 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
|
79 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
|
80 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)" |
76 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
81 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
77 apply (simp_all add: alpha5_inj) |
82 apply (simp_all add: alpha5_inj) |
78 apply (erule exE) |
83 apply (erule exE) |
79 apply (rule_tac x="- pi" in exI) |
84 apply (rule_tac x="- pi" in exI) |
80 apply (simp add: alpha_gen) |
85 apply (simp add: alpha_gen) |
89 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
94 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
90 apply simp |
95 apply simp |
91 apply (rotate_tac 6) |
96 apply (rotate_tac 6) |
92 apply simp |
97 apply simp |
93 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) |
98 apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) |
94 apply (simp)*) |
99 apply (simp) |
|
100 done |
|
101 |
|
102 thm alpha_gen_sym[no_vars] |
|
103 thm alpha_gen_compose_sym[no_vars] |
|
104 |
|
105 lemma tt: |
|
106 "\<lbrakk>R (- p \<bullet> x) y \<Longrightarrow> R (p \<bullet> y) x; (bs, x) \<approx>gen R f (- p) (cs, y)\<rbrakk> \<Longrightarrow> (cs, y) \<approx>gen R f p (bs, x)" |
|
107 unfolding alphas |
|
108 unfolding fresh_star_def |
|
109 by (auto simp add: fresh_minus_perm) |
|
110 |
|
111 lemma alpha5_symp2: |
|
112 shows "a \<approx>5 b \<Longrightarrow> b \<approx>5 a" |
|
113 and "x \<approx>l y \<Longrightarrow> y \<approx>l x" |
|
114 and "alpha_rbv5 x y \<Longrightarrow> alpha_rbv5 y x" |
|
115 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
|
116 (* non-binding case *) |
|
117 apply(simp add: alpha5_inj) |
|
118 (* non-binding case *) |
|
119 apply(simp add: alpha5_inj) |
|
120 (* binding case *) |
|
121 apply(simp add: alpha5_inj) |
|
122 apply(erule exE) |
|
123 apply(rule_tac x="- pi" in exI) |
|
124 apply(rule tt) |
|
125 apply(simp add: alphas) |
|
126 apply(erule conjE)+ |
|
127 apply(drule_tac p="- pi" in alpha5_eqvt(2)) |
|
128 apply(drule_tac p="- pi" in alpha5_eqvt(2)) |
|
129 apply(drule_tac p="- pi" in alpha5_eqvt(1)) |
|
130 apply(drule_tac p="- pi" in alpha5_eqvt(1)) |
|
131 apply(simp) |
|
132 apply(simp add: alphas) |
|
133 apply(erule conjE)+ |
|
134 apply metis |
|
135 (* non-binding case *) |
|
136 apply(simp add: alpha5_inj) |
|
137 (* non-binding case *) |
|
138 apply(simp add: alpha5_inj) |
|
139 (* non-binding case *) |
|
140 apply(simp add: alpha5_inj) |
|
141 (* non-binding case *) |
|
142 apply(simp add: alpha5_inj) |
95 done |
143 done |
96 |
144 |
97 lemma alpha5_transp: |
145 lemma alpha5_transp: |
98 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and> |
146 "(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> |
147 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and> |
112 apply (simp_all add: alpha5_inj) |
160 apply (simp_all add: alpha5_inj) |
113 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
161 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) |
114 apply (simp_all add: alpha5_inj) |
162 apply (simp_all add: alpha5_inj) |
115 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
163 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) |
116 (* HERE *) |
164 (* HERE *) |
|
165 (* |
|
166 apply(rule alpha_gen_trans) |
|
167 thm alpha_gen_trans |
|
168 defer |
117 apply (simp add: alpha_gen) |
169 apply (simp add: alpha_gen) |
118 apply clarify |
170 apply clarify |
119 apply(simp add: fresh_star_plus) |
171 apply(simp add: fresh_star_plus) |
120 apply (rule conjI) |
172 apply (rule conjI) |
121 apply (erule_tac x="- pi \<bullet> rltsaa" in allE) |
173 apply (erule_tac x="- pi \<bullet> rltsaa" in allE) |