73 apply(simp only: tt1) |
73 apply(simp only: tt1) |
74 apply(simp only: foo.eq_iff) |
74 apply(simp only: foo.eq_iff) |
75 apply(simp add: uu1) |
75 apply(simp add: uu1) |
76 done |
76 done |
77 |
77 |
|
78 lemma Let2_rename: |
|
79 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(supp ([[atom y]]lst. t2)) \<sharp>* p" |
|
80 shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)" |
|
81 using assms |
|
82 apply - |
|
83 apply(drule supp_perm_eq[symmetric]) |
|
84 apply(drule supp_perm_eq[symmetric]) |
|
85 apply(simp only: foo.eq_iff) |
|
86 apply(simp only: eqvts) |
|
87 apply simp |
|
88 done |
|
89 |
|
90 lemma Let2_rename2: |
|
91 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(atom y) \<sharp> p" |
|
92 shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) y (p \<bullet> t1) t2" |
|
93 using assms |
|
94 apply - |
|
95 apply(drule supp_perm_eq[symmetric]) |
|
96 apply(simp only: foo.eq_iff) |
|
97 apply(simp only: eqvts) |
|
98 apply simp |
|
99 by (metis assms(2) atom_eqvt fresh_perm) |
|
100 |
|
101 lemma Let2_rename3: |
|
102 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" |
|
103 and "(supp ([[atom y]]lst. t2)) \<sharp>* p" |
|
104 and "(atom x) \<sharp> p" |
|
105 shows "Let2 x y t1 t2 = Let2 x (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)" |
|
106 using assms |
|
107 apply - |
|
108 apply(drule supp_perm_eq[symmetric]) |
|
109 apply(drule supp_perm_eq[symmetric]) |
|
110 apply(simp only: foo.eq_iff) |
|
111 apply(simp only: eqvts) |
|
112 apply simp |
|
113 by (metis assms(2) atom_eqvt fresh_perm) |
|
114 |
78 lemma strong_exhaust1: |
115 lemma strong_exhaust1: |
|
116 fixes c::"'a::fs" |
|
117 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
118 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
119 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
120 and "\<And>assn1 trm1 assn2 trm2. |
|
121 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
|
122 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
123 shows "P" |
|
124 apply(rule_tac y="y" in foo.exhaust(1)) |
|
125 apply(rule assms(1)) |
|
126 apply(assumption) |
|
127 apply(rule assms(2)) |
|
128 apply(assumption) |
|
129 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
130 apply(erule exE) |
|
131 apply(erule conjE) |
|
132 apply(rule assms(3)) |
|
133 apply(perm_simp) |
|
134 apply(assumption) |
|
135 apply(simp) |
|
136 apply(drule supp_perm_eq[symmetric]) |
|
137 apply(perm_simp) |
|
138 apply(simp) |
|
139 apply(rule at_set_avoiding2) |
|
140 apply(simp add: finite_supp) |
|
141 apply(simp add: finite_supp) |
|
142 apply(simp add: finite_supp) |
|
143 apply(simp add: foo.fresh fresh_star_def) |
|
144 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg1))) \<sharp>* c \<and> supp ([bn assg1]lst. trm1) \<sharp>* q") |
|
145 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg2))) \<sharp>* c \<and> supp ([bn assg2]lst. trm2) \<sharp>* q") |
|
146 apply(erule exE)+ |
|
147 apply(erule conjE)+ |
|
148 apply(rule assms(4)) |
|
149 apply(simp add: set_eqvt union_eqvt) |
|
150 apply(simp add: tt1) |
|
151 apply(simp add: fresh_star_union) |
|
152 apply(rule conjI) |
|
153 apply(assumption) |
|
154 apply(rotate_tac 3) |
|
155 apply(assumption) |
|
156 apply(simp add: foo.eq_iff) |
|
157 apply(drule supp_perm_eq[symmetric])+ |
|
158 apply(simp add: tt1 uu1) |
|
159 apply(auto)[1] |
|
160 apply(rule at_set_avoiding2) |
|
161 apply(simp add: finite_supp) |
|
162 apply(simp add: finite_supp) |
|
163 apply(simp add: finite_supp) |
|
164 apply(simp add: Abs_fresh_star) |
|
165 apply(rule at_set_avoiding2) |
|
166 apply(simp add: finite_supp) |
|
167 apply(simp add: finite_supp) |
|
168 apply(simp add: finite_supp) |
|
169 apply(simp add: Abs_fresh_star) |
|
170 apply(case_tac "name1 = name2") |
|
171 apply(subgoal_tac |
|
172 "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* c \<and> (supp (([[atom name1, atom name2]]lst. trm1), ([[atom name2]]lst. trm2))) \<sharp>* q") |
|
173 apply(erule exE)+ |
|
174 apply(erule conjE)+ |
|
175 apply(perm_simp) |
|
176 apply(rule assms(5)) |
|
177 |
|
178 apply (simp add: fresh_star_def eqvts) |
|
179 apply (simp only: supp_Pair) |
|
180 apply (simp only: fresh_star_Un_elim) |
|
181 apply (subst Let2_rename) |
|
182 apply assumption |
|
183 apply assumption |
|
184 apply (rule refl) |
|
185 apply(rule at_set_avoiding2) |
|
186 apply(simp add: finite_supp) |
|
187 apply(simp add: finite_supp) |
|
188 apply(simp add: finite_supp) |
|
189 apply clarify |
|
190 apply (simp add: fresh_star_def) |
|
191 apply (simp add: fresh_def supp_Pair supp_Abs) |
|
192 apply(subgoal_tac |
|
193 "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> (supp ((([[atom name1, atom name2]]lst. trm1)), (atom name2))) \<sharp>* q") |
|
194 prefer 2 |
|
195 apply(rule at_set_avoiding2) |
|
196 apply(simp add: finite_supp) |
|
197 apply(simp add: finite_supp) |
|
198 apply(simp add: finite_supp) |
|
199 apply (simp add: fresh_star_def) |
|
200 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
|
201 apply(erule exE)+ |
|
202 apply(erule conjE)+ |
|
203 apply(perm_simp) |
|
204 apply(rule assms(5)) |
|
205 apply assumption |
|
206 apply clarify |
|
207 apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2) |
|
208 apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs) |
|
209 apply (simp add: fresh_star_def supp_atom) |
|
210 done |
|
211 |
|
212 lemma strong_exhaust2: |
79 fixes c::"'a::fs" |
213 fixes c::"'a::fs" |
80 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
214 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
81 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
215 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
82 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
216 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
83 and "\<And>assn1 trm1 assn2 trm2. |
217 and "\<And>assn1 trm1 assn2 trm2. |
84 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
218 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
85 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
219 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
86 shows "P" |
220 shows "P" |
87 apply(rule_tac y="y" in foo.exhaust(1)) |
221 apply (rule strong_exhaust1) |
88 apply(rule assms(1)) |
222 apply (erule assms) |
89 apply(assumption) |
223 apply (erule assms) |
90 apply(rule assms(2)) |
224 apply (erule assms) apply assumption |
91 apply(assumption) |
225 apply (erule assms) apply assumption |
92 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
226 apply(case_tac "x1 = x2") |
93 apply(erule exE) |
|
94 apply(erule conjE) |
|
95 apply(rule assms(3)) |
|
96 apply(perm_simp) |
|
97 apply(assumption) |
|
98 apply(simp) |
|
99 apply(drule supp_perm_eq[symmetric]) |
|
100 apply(perm_simp) |
|
101 apply(simp) |
|
102 apply(rule at_set_avoiding2) |
|
103 apply(simp add: finite_supp) |
|
104 apply(simp add: finite_supp) |
|
105 apply(simp add: finite_supp) |
|
106 apply(simp add: foo.fresh fresh_star_def) |
|
107 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg1))) \<sharp>* c \<and> supp ([bn assg1]lst. trm1) \<sharp>* q") |
|
108 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg2))) \<sharp>* c \<and> supp ([bn assg2]lst. trm2) \<sharp>* q") |
|
109 apply(erule exE)+ |
|
110 apply(erule conjE)+ |
|
111 apply(rule assms(4)) |
|
112 apply(simp add: set_eqvt union_eqvt) |
|
113 apply(simp add: tt1) |
|
114 apply(simp add: fresh_star_union) |
|
115 apply(rule conjI) |
|
116 apply(assumption) |
|
117 apply(rotate_tac 3) |
|
118 apply(assumption) |
|
119 apply(simp add: foo.eq_iff) |
|
120 apply(drule supp_perm_eq[symmetric])+ |
|
121 apply(simp add: tt1 uu1) |
|
122 apply(auto)[1] |
|
123 apply(rule at_set_avoiding2) |
|
124 apply(simp add: finite_supp) |
|
125 apply(simp add: finite_supp) |
|
126 apply(simp add: finite_supp) |
|
127 apply(simp add: Abs_fresh_star) |
|
128 apply(rule at_set_avoiding2) |
|
129 apply(simp add: finite_supp) |
|
130 apply(simp add: finite_supp) |
|
131 apply(simp add: finite_supp) |
|
132 apply(simp add: Abs_fresh_star) |
|
133 thm foo.eq_iff |
|
134 apply(subgoal_tac |
227 apply(subgoal_tac |
135 "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> supp ([[atom name1]]lst. trm1) \<sharp>* q") |
228 "\<exists>q. (q \<bullet> {atom x1, atom x2}) \<sharp>* c \<and> (supp (([[atom x1, atom x2]]lst. trm1), ([[atom x2]]lst. trm2))) \<sharp>* q") |
136 apply(subgoal_tac |
229 apply(erule exE)+ |
137 "\<exists>q. (q \<bullet> {atom name2}) \<sharp>* c \<and> supp ([[atom name2]]lst. trm2) \<sharp>* q") |
230 apply(erule conjE)+ |
138 apply(erule exE)+ |
231 apply(perm_simp) |
139 apply(erule conjE)+ |
|
140 apply(rule assms(5)) |
232 apply(rule assms(5)) |
|
233 apply assumption |
|
234 apply simp |
|
235 apply (rule Let2_rename) |
|
236 apply (simp only: supp_Pair) |
|
237 apply (simp only: fresh_star_Un_elim) |
|
238 apply (simp only: supp_Pair) |
|
239 apply (simp only: fresh_star_Un_elim) |
|
240 apply(rule at_set_avoiding2) |
|
241 apply(simp add: finite_supp) |
|
242 apply(simp add: finite_supp) |
|
243 apply(simp add: finite_supp) |
|
244 apply clarify |
|
245 apply (simp add: fresh_star_def) |
|
246 apply (simp add: fresh_def supp_Pair supp_Abs) |
|
247 |
|
248 apply(subgoal_tac |
|
249 "\<exists>q. (q \<bullet> {atom x2}) \<sharp>* c \<and> supp (([[atom x2]]lst. trm2), ([[atom x1, atom x2]]lst. trm1), (atom x1)) \<sharp>* q") |
|
250 apply(erule exE)+ |
|
251 apply(erule conjE)+ |
|
252 apply(rule assms(5)) |
141 apply(perm_simp) |
253 apply(perm_simp) |
142 apply(simp (no_asm) add: fresh_star_insert) |
254 apply(simp (no_asm) add: fresh_star_insert) |
143 apply(rule conjI) |
255 apply(rule conjI) |
144 apply(simp add: fresh_star_def) |
256 apply (simp add: fresh_star_def) |
145 apply(rotate_tac 3) |
257 apply(rotate_tac 2) |
146 apply(simp add: fresh_star_def) |
258 apply(simp add: fresh_star_def) |
147 apply(simp) |
259 apply(simp) |
148 apply(simp add: foo.eq_iff) |
260 apply (rule Let2_rename3) |
149 apply(drule supp_perm_eq[symmetric])+ |
261 apply (simp add: supp_Pair fresh_star_union) |
150 apply(simp add: atom_eqvt) |
262 apply (simp add: supp_Pair fresh_star_union) |
151 apply(rule conjI) |
263 apply (simp add: supp_Pair fresh_star_union) |
152 oops |
264 apply clarify |
153 |
265 apply (simp add: fresh_star_def supp_atom) |
|
266 apply(rule at_set_avoiding2) |
|
267 apply(simp add: finite_supp) |
|
268 apply(simp add: finite_supp) |
|
269 apply(simp add: finite_supp) |
|
270 apply(simp add: fresh_star_def) |
|
271 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
|
272 done |
154 |
273 |
155 end |
274 end |
156 |
275 |
157 |
276 |
158 |
277 |