248 unfolding Diff_eqvt[symmetric] |
248 unfolding Diff_eqvt[symmetric] |
249 apply(erule_tac [!] exE) |
249 apply(erule_tac [!] exE) |
250 apply(rule_tac [!] x="p \<bullet> pa" in exI) |
250 apply(rule_tac [!] x="p \<bullet> pa" in exI) |
251 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) |
251 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) |
252 |
252 |
|
253 |
|
254 section {* Strengthening the equivalence *} |
|
255 |
|
256 lemma disjoint_right_eq: |
|
257 assumes a: "A \<union> B1 = A \<union> B2" |
|
258 and b: "A \<inter> B1 = {}" "A \<inter> B2 = {}" |
|
259 shows "B1 = B2" |
|
260 using a b |
|
261 by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2) |
|
262 |
|
263 lemma supp_property_set: |
|
264 assumes a: "(as, x) \<approx>set (op =) supp p (as', x')" |
|
265 shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
|
266 proof - |
|
267 from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas) |
|
268 then have *: "p \<bullet> (supp x - as) = (supp x - as)" |
|
269 by (simp add: atom_set_perm_eq) |
|
270 have "(supp x' - as') \<union> (supp x' \<inter> as') = supp x'" by auto |
|
271 also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas) |
|
272 also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt) |
|
273 also have "\<dots> = p \<bullet> ((supp x - as) \<union> (supp x \<inter> as))" by auto |
|
274 also have "\<dots> = (p \<bullet> (supp x - as)) \<union> (p \<bullet> (supp x \<inter> as))" by (simp add: union_eqvt) |
|
275 also have "\<dots> = (supp x - as) \<union> (p \<bullet> (supp x \<inter> as))" using * by simp |
|
276 also have "\<dots> = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" using a by (simp add: alphas) |
|
277 finally have "(supp x' - as') \<union> (supp x' \<inter> as') = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" . |
|
278 moreover |
|
279 have "(supp x' - as') \<inter> (supp x' \<inter> as') = {}" by auto |
|
280 moreover |
|
281 have "(supp x - as) \<inter> (supp x \<inter> as) = {}" by auto |
|
282 then have "p \<bullet> ((supp x - as) \<inter> (supp x \<inter> as) = {})" by (simp add: permute_bool_def) |
|
283 then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp) |
|
284 then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp |
|
285 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas) |
|
286 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
|
287 by (auto dest: disjoint_right_eq) |
|
288 qed |
|
289 |
|
290 lemma supp_property_res: |
|
291 assumes a: "(as, x) \<approx>res (op =) supp p (as', x')" |
|
292 shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
|
293 proof - |
|
294 from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas) |
|
295 then have *: "p \<bullet> (supp x - as) = (supp x - as)" |
|
296 by (simp add: atom_set_perm_eq) |
|
297 have "(supp x' - as') \<union> (supp x' \<inter> as') = supp x'" by auto |
|
298 also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas) |
|
299 also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt) |
|
300 also have "\<dots> = p \<bullet> ((supp x - as) \<union> (supp x \<inter> as))" by auto |
|
301 also have "\<dots> = (p \<bullet> (supp x - as)) \<union> (p \<bullet> (supp x \<inter> as))" by (simp add: union_eqvt) |
|
302 also have "\<dots> = (supp x - as) \<union> (p \<bullet> (supp x \<inter> as))" using * by simp |
|
303 also have "\<dots> = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" using a by (simp add: alphas) |
|
304 finally have "(supp x' - as') \<union> (supp x' \<inter> as') = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" . |
|
305 moreover |
|
306 have "(supp x' - as') \<inter> (supp x' \<inter> as') = {}" by auto |
|
307 moreover |
|
308 have "(supp x - as) \<inter> (supp x \<inter> as) = {}" by auto |
|
309 then have "p \<bullet> ((supp x - as) \<inter> (supp x \<inter> as) = {})" by (simp add: permute_bool_def) |
|
310 then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp) |
|
311 then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp |
|
312 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas) |
|
313 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
|
314 by (auto dest: disjoint_right_eq) |
|
315 qed |
|
316 |
|
317 lemma supp_property_list: |
|
318 assumes a: "(as, x) \<approx>lst (op =) supp p (as', x')" |
|
319 shows "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'" |
|
320 proof - |
|
321 from a have "(supp x - set as) \<sharp>* p" by (auto simp only: alphas) |
|
322 then have *: "p \<bullet> (supp x - set as) = (supp x - set as)" |
|
323 by (simp add: atom_set_perm_eq) |
|
324 have "(supp x' - set as') \<union> (supp x' \<inter> set as') = supp x'" by auto |
|
325 also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas) |
|
326 also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt) |
|
327 also have "\<dots> = p \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))" by auto |
|
328 also have "\<dots> = (p \<bullet> (supp x - set as)) \<union> (p \<bullet> (supp x \<inter> set as))" by (simp add: union_eqvt) |
|
329 also have "\<dots> = (supp x - set as) \<union> (p \<bullet> (supp x \<inter> set as))" using * by simp |
|
330 also have "\<dots> = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" using a by (simp add: alphas) |
|
331 finally |
|
332 have "(supp x' - set as') \<union> (supp x' \<inter> set as') = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" . |
|
333 moreover |
|
334 have "(supp x' - set as') \<inter> (supp x' \<inter> set as') = {}" by auto |
|
335 moreover |
|
336 have "(supp x - set as) \<inter> (supp x \<inter> set as) = {}" by auto |
|
337 then have "p \<bullet> ((supp x - set as) \<inter> (supp x \<inter> set as) = {})" by (simp add: permute_bool_def) |
|
338 then have "(p \<bullet> (supp x - set as)) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" by (perm_simp) (simp) |
|
339 then have "(supp x - set as) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using * by simp |
|
340 then have "(supp x' - set as') \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using a by (simp add: alphas) |
|
341 ultimately show "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'" |
|
342 by (auto dest: disjoint_right_eq) |
|
343 qed |
|
344 |
|
345 |
|
346 |
|
347 section {* Quotient types *} |
|
348 |
253 quotient_type |
349 quotient_type |
254 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
350 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
255 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
351 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
256 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
352 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
257 apply(rule_tac [!] equivpI) |
353 apply(rule_tac [!] equivpI) |
548 assumes a: "(p \<bullet> bs) \<sharp>* x" |
644 assumes a: "(p \<bullet> bs) \<sharp>* x" |
549 and b: "finite bs" |
645 and b: "finite bs" |
550 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
646 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
551 proof - |
647 proof - |
552 from b set_renaming_perm |
648 from b set_renaming_perm |
553 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
649 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
|
650 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
554 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
651 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
555 apply(rule perm_supp_eq[symmetric]) |
652 apply(rule perm_supp_eq[symmetric]) |
556 using a ** |
653 using a ** |
557 unfolding Abs_fresh_star_iff |
654 unfolding Abs_fresh_star_iff |
558 unfolding fresh_star_def |
655 unfolding fresh_star_def |
559 by auto |
656 by auto |
560 also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp |
657 also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp |
561 finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: *) |
658 finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: ***) |
562 then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis |
659 then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis |
563 qed |
660 qed |
564 |
661 |
565 lemma Abs_rename_res: |
662 lemma Abs_rename_res: |
566 fixes x::"'a::fs" |
663 fixes x::"'a::fs" |
567 assumes a: "(p \<bullet> bs) \<sharp>* x" |
664 assumes a: "(p \<bullet> bs) \<sharp>* x" |
568 and b: "finite bs" |
665 and b: "finite bs" |
569 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
666 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
570 proof - |
667 proof - |
571 from b set_renaming_perm |
668 from b set_renaming_perm |
572 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
669 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
|
670 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
573 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
671 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
574 apply(rule perm_supp_eq[symmetric]) |
672 apply(rule perm_supp_eq[symmetric]) |
575 using a ** |
673 using a ** |
576 unfolding Abs_fresh_star_iff |
674 unfolding Abs_fresh_star_iff |
577 unfolding fresh_star_def |
675 unfolding fresh_star_def |
578 by auto |
676 by auto |
579 also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp |
677 also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp |
580 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: *) |
678 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: ***) |
581 then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis |
679 then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis |
582 qed |
680 qed |
583 |
681 |
584 lemma Abs_rename_lst: |
682 lemma Abs_rename_lst: |
585 fixes x::"'a::fs" |
683 fixes x::"'a::fs" |
586 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
684 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
587 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
685 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
588 proof - |
686 proof - |
589 from a list_renaming_perm |
687 from a list_renaming_perm |
590 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast |
688 obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast |
|
689 have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt) |
591 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
690 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
592 apply(rule perm_supp_eq[symmetric]) |
691 apply(rule perm_supp_eq[symmetric]) |
593 using a ** |
692 using a ** |
594 unfolding Abs_fresh_star_iff |
693 unfolding Abs_fresh_star_iff |
595 unfolding fresh_star_def |
694 unfolding fresh_star_def |
596 by auto |
695 by auto |
597 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
696 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
598 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: *) |
697 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: ***) |
599 then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis |
698 then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis |
600 qed |
699 qed |
601 |
700 |
602 |
701 |
603 text {* for deep recursive binders *} |
702 text {* for deep recursive binders *} |
604 |
703 |