98 apply(drule sym) |
98 apply(drule sym) |
99 apply(simp add: mem_permute_iff) |
99 apply(simp add: mem_permute_iff) |
100 apply(simp add: mem_permute_iff) |
100 apply(simp add: mem_permute_iff) |
101 done |
101 done |
102 |
102 |
103 lemma yy1: |
103 lemma Abs_rename_set: |
104 assumes "(p \<bullet> bs) \<sharp>* bs" "finite bs" |
|
105 shows "p \<bullet> bs \<inter> bs = {}" |
|
106 using assms |
|
107 apply(auto simp add: fresh_star_def) |
|
108 apply(simp add: fresh_def supp_finite_atom_set) |
|
109 done |
|
110 |
|
111 lemma abs_rename_set: |
|
112 fixes x::"'a::fs" |
104 fixes x::"'a::fs" |
113 assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs" |
105 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
|
106 and b: "finite bs" |
114 shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" |
107 shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" |
115 using yy assms |
108 proof - |
116 apply - |
109 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) |
117 apply(drule_tac x="p" in meta_spec) |
110 with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
118 apply(drule_tac x="bs" in meta_spec) |
111 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
119 apply(auto simp add: yy1) |
112 apply(rule perm_supp_eq[symmetric]) |
120 apply(rule_tac x="q \<bullet> x" in exI) |
113 using a ** |
121 apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x") |
114 unfolding fresh_star_Pair |
122 apply(simp) |
115 unfolding Abs_fresh_star_iff |
123 apply(rule supp_perm_eq) |
116 unfolding fresh_star_def |
124 apply(rule fresh_star_supp_conv) |
117 by auto |
125 apply(simp add: fresh_star_def) |
118 also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp |
126 apply(simp add: Abs_fresh_iff) |
119 also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp |
127 apply(auto) |
120 finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" . |
128 done |
121 then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast |
129 |
122 qed |
130 lemma abs_rename_res: |
123 |
|
124 lemma Abs_rename_res: |
131 fixes x::"'a::fs" |
125 fixes x::"'a::fs" |
132 assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs" |
126 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
|
127 and b: "finite bs" |
133 shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" |
128 shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" |
134 using yy assms |
129 proof - |
135 apply - |
130 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) |
136 apply(drule_tac x="p" in meta_spec) |
131 with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
137 apply(drule_tac x="bs" in meta_spec) |
132 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
138 apply(auto simp add: yy1) |
133 apply(rule perm_supp_eq[symmetric]) |
139 apply(rule_tac x="q \<bullet> x" in exI) |
134 using a ** |
140 apply(subgoal_tac "(q \<bullet> ([bs]res. x)) = [bs]res. x") |
135 unfolding fresh_star_Pair |
141 apply(simp) |
136 unfolding Abs_fresh_star_iff |
142 apply(rule supp_perm_eq) |
137 unfolding fresh_star_def |
143 apply(rule fresh_star_supp_conv) |
138 by auto |
144 apply(simp add: fresh_star_def) |
139 also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp |
145 apply(simp add: Abs_fresh_iff) |
140 also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp |
146 apply(auto) |
141 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" . |
147 done |
142 then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast |
|
143 qed |
148 |
144 |
149 lemma zz0: |
145 lemma zz0: |
150 assumes "p \<bullet> bs = q \<bullet> bs" |
146 assumes "p \<bullet> bs = q \<bullet> bs" |
151 and a: "a \<in> set bs" |
147 and a: "a \<in> set bs" |
152 shows "p \<bullet> a = q \<bullet> a" |
148 shows "p \<bullet> a = q \<bullet> a" |
153 using assms |
149 using assms |
154 by (induct bs) (auto) |
150 by (induct bs) (auto) |
155 |
151 |
156 lemma zz: |
152 lemma zz: |
157 fixes bs::"atom list" |
153 fixes bs::"atom list" |
158 assumes "set bs \<inter> (p \<bullet> (set bs)) = {}" |
154 assumes "(p \<bullet> (set bs)) \<inter> (set bs) = {}" |
159 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
155 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
160 using assms |
156 using assms |
161 apply(induct bs) |
157 apply(induct bs) |
162 apply(simp add: permute_set_eq) |
158 apply(simp add: permute_set_eq) |
163 apply(rule_tac x="0" in exI) |
159 apply(rule_tac x="0" in exI) |
193 apply(simp) |
189 apply(simp) |
194 apply(simp add: fresh_permute_iff) |
190 apply(simp add: fresh_permute_iff) |
195 apply(auto simp add: fresh_def supp_of_atom_list)[1] |
191 apply(auto simp add: fresh_def supp_of_atom_list)[1] |
196 done |
192 done |
197 |
193 |
198 lemma zz1: |
194 lemma Abs_rename_list: |
199 assumes "(p \<bullet> (set bs)) \<sharp>* bs" |
|
200 shows "(set bs) \<inter> (p \<bullet> (set bs)) = {}" |
|
201 using assms |
|
202 apply(auto simp add: fresh_star_def) |
|
203 apply(simp add: fresh_def supp_of_atom_list) |
|
204 done |
|
205 |
|
206 lemma abs_rename_list: |
|
207 fixes x::"'a::fs" |
195 fixes x::"'a::fs" |
208 assumes "(p \<bullet> (set bs)) \<sharp>* x" "(p \<bullet> (set bs)) \<sharp>* bs" |
196 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
209 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
197 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
210 using zz assms |
198 proof - |
211 apply - |
199 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |
212 apply(drule_tac x="bs" in meta_spec) |
200 by (simp add: fresh_star_Pair fresh_star_set) |
213 apply(drule_tac x="p" in meta_spec) |
201 with zz obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis |
214 apply(drule_tac zz1) |
202 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
215 apply(auto) |
203 apply(rule perm_supp_eq[symmetric]) |
216 apply(rule_tac x="q \<bullet> x" in exI) |
204 using a ** |
217 apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x") |
205 unfolding fresh_star_Pair |
218 apply(simp) |
206 unfolding Abs_fresh_star_iff |
219 apply(rule supp_perm_eq) |
207 unfolding fresh_star_def |
220 apply(rule fresh_star_supp_conv) |
208 by auto |
221 apply(simp add: fresh_star_def) |
209 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
222 apply(simp add: Abs_fresh_iff) |
210 also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp |
223 apply(auto) |
211 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" . |
224 done |
212 then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast |
225 |
213 qed |
226 lemma fresh_star_list: |
|
227 shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys" |
|
228 and "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs" |
|
229 and "as \<sharp>* []" |
|
230 by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append) |
|
231 |
214 |
232 |
215 |
233 lemma test6: |
216 lemma test6: |
234 fixes c::"'a::fs" |
217 fixes c::"'a::fs" |
235 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
218 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
270 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
251 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
271 apply(erule exE) |
252 apply(erule exE) |
272 apply(rule assms(4)) |
253 apply(rule assms(4)) |
273 apply(simp only:) |
254 apply(simp only:) |
274 apply(simp only: foo.eq_iff) |
255 apply(simp only: foo.eq_iff) |
275 apply(insert abs_rename_list)[1] |
256 apply(insert Abs_rename_list)[1] |
276 apply(drule_tac x="p" in meta_spec) |
257 apply(drule_tac x="p" in meta_spec) |
277 apply(drule_tac x="bn assg1" in meta_spec) |
258 apply(drule_tac x="bn assg1" in meta_spec) |
278 apply(drule_tac x="trm1" in meta_spec) |
259 apply(drule_tac x="trm1" in meta_spec) |
279 apply(insert abs_rename_list)[1] |
260 apply(insert Abs_rename_list)[1] |
280 apply(drule_tac x="p" in meta_spec) |
261 apply(drule_tac x="p" in meta_spec) |
281 apply(drule_tac x="bn assg2" in meta_spec) |
262 apply(drule_tac x="bn assg2" in meta_spec) |
282 apply(drule_tac x="trm2" in meta_spec) |
263 apply(drule_tac x="trm2" in meta_spec) |
283 apply(drule meta_mp) |
264 apply(drule meta_mp) |
284 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
265 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
285 apply(drule meta_mp) |
266 apply(drule meta_mp) |
286 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
267 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
287 apply(drule meta_mp) |
|
288 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
|
289 apply(drule meta_mp) |
|
290 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
|
291 apply(erule exE)+ |
268 apply(erule exE)+ |
292 apply(rule exI)+ |
269 apply(rule exI)+ |
293 apply(perm_simp add: tt1) |
270 apply(perm_simp add: tt1) |
294 apply(rule conjI) |
271 apply(rule conjI) |
295 apply(simp add: fresh_star_prod fresh_star_union) |
272 apply(simp add: fresh_star_Pair fresh_star_Un) |
296 apply(erule conjE)+ |
273 apply(erule conjE)+ |
297 apply(rule conjI) |
274 apply(rule conjI) |
298 apply(assumption) |
275 apply(assumption) |
299 apply(rotate_tac 4) |
276 apply(rotate_tac 4) |
300 apply(assumption) |
277 apply(assumption) |
311 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
288 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
312 apply(erule exE) |
289 apply(erule exE) |
313 apply(rule assms(5)) |
290 apply(rule assms(5)) |
314 apply(simp only:) |
291 apply(simp only:) |
315 apply(simp only: foo.eq_iff) |
292 apply(simp only: foo.eq_iff) |
316 apply(insert abs_rename_list)[1] |
293 apply(insert Abs_rename_list)[1] |
317 apply(drule_tac x="p" in meta_spec) |
294 apply(drule_tac x="p" in meta_spec) |
318 apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec) |
295 apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec) |
319 apply(drule_tac x="trm1" in meta_spec) |
296 apply(drule_tac x="trm1" in meta_spec) |
320 apply(insert abs_rename_list)[1] |
297 apply(insert Abs_rename_list)[1] |
321 apply(drule_tac x="p" in meta_spec) |
298 apply(drule_tac x="p" in meta_spec) |
322 apply(drule_tac x="[atom name2]" in meta_spec) |
299 apply(drule_tac x="[atom name2]" in meta_spec) |
323 apply(drule_tac x="trm2" in meta_spec) |
300 apply(drule_tac x="trm2" in meta_spec) |
324 apply(drule meta_mp) |
301 apply(drule meta_mp) |
325 apply(simp only: union_eqvt fresh_star_prod set.simps set_append fresh_star_union, simp) |
302 apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp) |
326 apply(drule meta_mp) |
303 apply(auto)[1] |
327 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
304 apply(perm_simp) |
328 apply(drule meta_mp) |
305 apply(auto simp add: fresh_star_def)[1] |
329 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp) |
306 apply(perm_simp) |
330 apply(drule meta_mp) |
307 apply(auto simp add: fresh_star_def)[1] |
331 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp) |
308 apply(perm_simp) |
|
309 apply(auto simp add: fresh_star_def)[1] |
|
310 apply(drule meta_mp) |
|
311 apply(perm_simp) |
|
312 apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1] |
332 apply(erule exE)+ |
313 apply(erule exE)+ |
333 apply(rule exI)+ |
314 apply(rule exI)+ |
334 apply(perm_simp add: tt1) |
315 apply(perm_simp add: tt1) |
335 apply(rule conjI) |
316 apply(rule conjI) |
336 prefer 2 |
317 prefer 2 |
337 apply(rule conjI) |
318 apply(rule conjI) |
338 apply(assumption) |
319 apply(assumption) |
339 apply(assumption) |
320 apply(assumption) |
340 apply(simp add: fresh_star_prod) |
321 apply(simp add: fresh_star_Pair) |
341 apply(simp add: fresh_star_def) |
322 apply(simp add: fresh_star_def) |
342 apply(rule at_set_avoiding1) |
323 apply(rule at_set_avoiding1) |
343 apply(simp) |
324 apply(simp) |
344 apply(simp add: finite_supp) |
325 apply(simp add: finite_supp) |
345 done |
326 done |
346 |
|
347 |
|
348 |
327 |
349 lemma test5: |
328 lemma test5: |
350 fixes c::"'a::fs" |
329 fixes c::"'a::fs" |
351 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
330 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
352 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
331 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |