10 |
10 |
11 fun |
11 fun |
12 alpha_set |
12 alpha_set |
13 where |
13 where |
14 alpha_set[simp del]: |
14 alpha_set[simp del]: |
15 "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow> |
15 "alpha_set (bs, x) R f p (cs, y) \<longleftrightarrow> |
16 f x - bs = f y - cs \<and> |
16 f x - bs = f y - cs \<and> |
17 (f x - bs) \<sharp>* pi \<and> |
17 (f x - bs) \<sharp>* p \<and> |
18 R (pi \<bullet> x) y \<and> |
18 R (p \<bullet> x) y \<and> |
19 pi \<bullet> bs = cs" |
19 p \<bullet> bs = cs" |
20 |
20 |
21 fun |
21 fun |
22 alpha_res |
22 alpha_res |
23 where |
23 where |
24 alpha_res[simp del]: |
24 alpha_res[simp del]: |
25 "alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow> |
25 "alpha_res (bs, x) R f p (cs, y) \<longleftrightarrow> |
26 f x - bs = f y - cs \<and> |
26 f x - bs = f y - cs \<and> |
27 (f x - bs) \<sharp>* pi \<and> |
27 (f x - bs) \<sharp>* p \<and> |
28 R (pi \<bullet> x) y" |
28 R (p \<bullet> x) y" |
29 |
29 |
30 fun |
30 fun |
31 alpha_lst |
31 alpha_lst |
32 where |
32 where |
33 alpha_lst[simp del]: |
33 alpha_lst[simp del]: |
34 "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow> |
34 "alpha_lst (bs, x) R f p (cs, y) \<longleftrightarrow> |
35 f x - set bs = f y - set cs \<and> |
35 f x - set bs = f y - set cs \<and> |
36 (f x - set bs) \<sharp>* pi \<and> |
36 (f x - set bs) \<sharp>* p \<and> |
37 R (pi \<bullet> x) y \<and> |
37 R (p \<bullet> x) y \<and> |
38 pi \<bullet> bs = cs" |
38 p \<bullet> bs = cs" |
39 |
39 |
40 lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps |
40 lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps |
41 |
41 |
42 notation |
42 notation |
43 alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and |
43 alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and |
86 shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)" |
85 shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)" |
87 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
86 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
88 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
87 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
89 unfolding alphas fresh_star_def |
88 unfolding alphas fresh_star_def |
90 using a |
89 using a |
91 by (auto simp add: fresh_minus_perm) |
90 by (auto simp add: fresh_minus_perm) |
92 |
91 |
93 lemma alpha_trans: |
92 lemma alpha_trans: |
94 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
93 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
95 shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)" |
94 shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)" |
96 and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)" |
95 and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)" |
106 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
105 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
107 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
106 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
108 apply(auto intro!: alpha_sym) |
107 apply(auto intro!: alpha_sym) |
109 apply(drule_tac [!] a) |
108 apply(drule_tac [!] a) |
110 apply(rule_tac [!] p="p" in permute_boolE) |
109 apply(rule_tac [!] p="p" in permute_boolE) |
111 apply(perm_simp add: permute_minus_cancel b) |
110 apply(simp_all add: b permute_self) |
112 apply(assumption) |
|
113 apply(perm_simp add: permute_minus_cancel b) |
|
114 apply(assumption) |
|
115 apply(perm_simp add: permute_minus_cancel b) |
|
116 apply(assumption) |
|
117 done |
111 done |
118 |
112 |
119 lemma alpha_set_trans_eqvt: |
113 lemma alpha_set_trans_eqvt: |
120 assumes b: "(cs, y) \<approx>set R f q (ds, z)" |
114 assumes b: "(cs, y) \<approx>set R f q (ds, z)" |
121 and a: "(bs, x) \<approx>set R f p (cs, y)" |
115 and a: "(bs, x) \<approx>set R f p (cs, y)" |
122 and d: "q \<bullet> R = R" |
116 and d: "q \<bullet> R = R" |
123 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
117 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
124 shows "(bs, x) \<approx>set R f (q + p) (ds, z)" |
118 shows "(bs, x) \<approx>set R f (q + p) (ds, z)" |
125 apply(rule alpha_trans) |
119 apply(rule alpha_trans(1)[OF _ a b]) |
126 defer |
|
127 apply(rule a) |
|
128 apply(rule b) |
|
129 apply(drule c) |
120 apply(drule c) |
130 apply(rule_tac p="q" in permute_boolE) |
121 apply(rule_tac p="q" in permute_boolE) |
131 apply(perm_simp add: permute_minus_cancel d) |
122 apply(simp add: d permute_self) |
132 apply(assumption) |
|
133 apply(rotate_tac -1) |
123 apply(rotate_tac -1) |
134 apply(drule_tac p="q" in permute_boolI) |
124 apply(drule_tac p="q" in permute_boolI) |
135 apply(perm_simp add: permute_minus_cancel d) |
125 apply(simp add: d permute_self permute_eqvt[symmetric]) |
136 apply(simp add: permute_eqvt[symmetric]) |
|
137 done |
126 done |
138 |
127 |
139 lemma alpha_res_trans_eqvt: |
128 lemma alpha_res_trans_eqvt: |
140 assumes b: "(cs, y) \<approx>res R f q (ds, z)" |
129 assumes b: "(cs, y) \<approx>res R f q (ds, z)" |
141 and a: "(bs, x) \<approx>res R f p (cs, y)" |
130 and a: "(bs, x) \<approx>res R f p (cs, y)" |
142 and d: "q \<bullet> R = R" |
131 and d: "q \<bullet> R = R" |
143 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
132 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
144 shows "(bs, x) \<approx>res R f (q + p) (ds, z)" |
133 shows "(bs, x) \<approx>res R f (q + p) (ds, z)" |
145 apply(rule alpha_trans) |
134 apply(rule alpha_trans(2)[OF _ a b]) |
146 defer |
|
147 apply(rule a) |
|
148 apply(rule b) |
|
149 apply(drule c) |
135 apply(drule c) |
150 apply(rule_tac p="q" in permute_boolE) |
136 apply(rule_tac p="q" in permute_boolE) |
151 apply(perm_simp add: permute_minus_cancel d) |
137 apply(simp add: d permute_self) |
152 apply(assumption) |
|
153 apply(rotate_tac -1) |
138 apply(rotate_tac -1) |
154 apply(drule_tac p="q" in permute_boolI) |
139 apply(drule_tac p="q" in permute_boolI) |
155 apply(perm_simp add: permute_minus_cancel d) |
140 apply(simp add: d permute_self permute_eqvt[symmetric]) |
156 apply(simp add: permute_eqvt[symmetric]) |
|
157 done |
141 done |
158 |
142 |
159 lemma alpha_lst_trans_eqvt: |
143 lemma alpha_lst_trans_eqvt: |
160 assumes b: "(cs, y) \<approx>lst R f q (ds, z)" |
144 assumes b: "(cs, y) \<approx>lst R f q (ds, z)" |
161 and a: "(bs, x) \<approx>lst R f p (cs, y)" |
145 and a: "(bs, x) \<approx>lst R f p (cs, y)" |
162 and d: "q \<bullet> R = R" |
146 and d: "q \<bullet> R = R" |
163 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
147 and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)" |
164 shows "(bs, x) \<approx>lst R f (q + p) (ds, z)" |
148 shows "(bs, x) \<approx>lst R f (q + p) (ds, z)" |
165 apply(rule alpha_trans) |
149 apply(rule alpha_trans(3)[OF _ a b]) |
166 defer |
|
167 apply(rule a) |
|
168 apply(rule b) |
|
169 apply(drule c) |
150 apply(drule c) |
170 apply(rule_tac p="q" in permute_boolE) |
151 apply(rule_tac p="q" in permute_boolE) |
171 apply(perm_simp add: permute_minus_cancel d) |
152 apply(simp add: d permute_self) |
172 apply(assumption) |
|
173 apply(rotate_tac -1) |
153 apply(rotate_tac -1) |
174 apply(drule_tac p="q" in permute_boolI) |
154 apply(drule_tac p="q" in permute_boolI) |
175 apply(perm_simp add: permute_minus_cancel d) |
155 apply(simp add: d permute_self permute_eqvt[symmetric]) |
176 apply(simp add: permute_eqvt[symmetric]) |
|
177 done |
156 done |
178 |
157 |
179 lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt |
158 lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt |
180 |
159 |
181 |
160 |
455 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)" |
434 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)" |
456 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
435 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
457 |
436 |
458 section {* Quotient types *} |
437 section {* Quotient types *} |
459 |
438 |
460 (* FIXME: The three could be defined together, but due to bugs |
|
461 introduced by the lifting package it doesn't work anymore *) |
|
462 quotient_type |
439 quotient_type |
463 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
440 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
464 apply(rule_tac [!] equivpI) |
441 apply(rule equivpI) |
465 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
442 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
466 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
443 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
467 |
444 |
468 quotient_type |
445 quotient_type |
469 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
446 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
470 apply(rule_tac [!] equivpI) |
447 apply(rule equivpI) |
471 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
448 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
472 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
449 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
473 |
450 |
474 quotient_type |
451 quotient_type |
475 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
452 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
535 unfolding Abs_eq_iff alphas |
512 unfolding Abs_eq_iff alphas |
536 apply (rule_tac x="0::perm" in exI) |
513 apply (rule_tac x="0::perm" in exI) |
537 apply (simp add: fresh_star_zero) |
514 apply (simp add: fresh_star_zero) |
538 using asm by blast |
515 using asm by blast |
539 |
516 |
540 lemma Abs_exhausts: |
517 lemma Abs_exhausts[cases type]: |
541 shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1" |
518 shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1" |
542 and "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2" |
519 and "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2" |
543 and "(\<And>bs (x::'a::pt). y3 = [bs]lst. x \<Longrightarrow> P3) \<Longrightarrow> P3" |
520 and "(\<And>bs (x::'a::pt). y3 = [bs]lst. x \<Longrightarrow> P3) \<Longrightarrow> P3" |
544 by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] |
521 by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] |
545 prod.exhaust[where 'a="atom set" and 'b="'a"] |
522 prod.exhaust[where 'a="atom set" and 'b="'a"] |
546 prod.exhaust[where 'a="atom list" and 'b="'a"]) |
523 prod.exhaust[where 'a="atom list" and 'b="'a"]) |
547 |
524 |
548 |
|
549 instantiation abs_set :: (pt) pt |
525 instantiation abs_set :: (pt) pt |
550 begin |
526 begin |
551 |
527 |
552 quotient_definition |
528 quotient_definition |
553 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set" |
529 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set" |
649 unfolding supports_def |
625 unfolding supports_def |
650 unfolding permute_Abs |
626 unfolding permute_Abs |
651 by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric]) |
627 by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric]) |
652 |
628 |
653 function |
629 function |
654 supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" |
630 supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" and |
|
631 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" and |
|
632 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set" |
655 where |
633 where |
656 "supp_set ([as]set. x) = supp x - as" |
634 "supp_set ([as]set. x) = supp x - as" |
657 apply(case_tac x rule: Abs_exhausts(1)) |
635 | "supp_res ([as]res. x) = supp x - as" |
|
636 | "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
|
637 apply(simp_all add: Abs_eq_iff alphas_abs alphas) |
|
638 apply(case_tac x) |
|
639 apply(case_tac a) |
658 apply(simp) |
640 apply(simp) |
659 apply(simp add: Abs_eq_iff alphas_abs alphas) |
641 apply(case_tac b) |
|
642 apply(case_tac a) |
|
643 apply(simp) |
|
644 apply(case_tac ba) |
|
645 apply(simp) |
660 done |
646 done |
661 |
647 |
662 termination supp_set |
648 termination |
663 by lexicographic_order |
|
664 |
|
665 function |
|
666 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" |
|
667 where |
|
668 "supp_res ([as]res. x) = supp x - as" |
|
669 apply(case_tac x rule: Abs_exhausts(2)) |
|
670 apply(simp) |
|
671 apply(simp add: Abs_eq_iff alphas_abs alphas) |
|
672 done |
|
673 |
|
674 termination supp_res |
|
675 by lexicographic_order |
|
676 |
|
677 function |
|
678 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set" |
|
679 where |
|
680 "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
|
681 apply(case_tac x rule: Abs_exhausts(3)) |
|
682 apply(simp) |
|
683 apply(simp add: Abs_eq_iff alphas_abs alphas) |
|
684 done |
|
685 |
|
686 termination supp_lst |
|
687 by lexicographic_order |
649 by lexicographic_order |
688 |
650 |
689 lemma supp_funs_eqvt[eqvt]: |
651 lemma supp_funs_eqvt[eqvt]: |
690 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)" |
652 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)" |
691 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
653 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
692 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
654 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
693 apply(case_tac x rule: Abs_exhausts(1)) |
655 apply(case_tac x) |
694 apply(simp add: supp_eqvt Diff_eqvt) |
656 apply(simp) |
695 apply(case_tac y rule: Abs_exhausts(2)) |
657 apply(case_tac y) |
696 apply(simp add: supp_eqvt Diff_eqvt) |
658 apply(simp) |
697 apply(case_tac z rule: Abs_exhausts(3)) |
659 apply(case_tac z) |
698 apply(simp add: supp_eqvt Diff_eqvt set_eqvt) |
660 apply(simp) |
699 done |
661 done |
700 |
662 |
701 lemma Abs_fresh_aux: |
663 lemma Abs_fresh_aux: |
702 shows "a \<sharp> [bs]set. x \<Longrightarrow> a \<sharp> supp_set ([bs]set. x)" |
664 shows "a \<sharp> [bs]set. x \<Longrightarrow> a \<sharp> supp_set ([bs]set. x)" |
703 and "a \<sharp> [bs]res. x \<Longrightarrow> a \<sharp> supp_res ([bs]res. x)" |
665 and "a \<sharp> [bs]res. x \<Longrightarrow> a \<sharp> supp_res ([bs]res. x)" |
848 and z::"'c::fs" |
809 and z::"'c::fs" |
849 and a b::"'b::at" |
810 and a b::"'b::at" |
850 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
811 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
851 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
812 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
852 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
813 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
853 apply - |
|
854 apply(auto) |
814 apply(auto) |
855 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric]) |
815 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric]) |
856 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
816 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
857 apply(drule_tac x="aa" in spec) |
817 apply(drule_tac x="aa" in spec) |
858 apply(simp) |
818 apply(simp) |
859 apply(subst Abs1_eq_iff_fresh(1)) |
819 apply(subst Abs1_eq_iff_fresh(1)) |
860 apply(auto simp add: fresh_Pair)[1] |
820 apply(auto simp add: fresh_Pair)[2] |
861 apply(assumption) |
|
862 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric]) |
821 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric]) |
863 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
822 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
864 apply(drule_tac x="aa" in spec) |
823 apply(drule_tac x="aa" in spec) |
865 apply(simp) |
824 apply(simp) |
866 apply(subst Abs1_eq_iff_fresh(2)) |
825 apply(subst Abs1_eq_iff_fresh(2)) |
867 apply(auto simp add: fresh_Pair)[1] |
826 apply(auto simp add: fresh_Pair)[2] |
868 apply(assumption) |
|
869 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric]) |
827 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric]) |
870 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
828 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
871 apply(drule_tac x="aa" in spec) |
829 apply(drule_tac x="aa" in spec) |
872 apply(simp) |
830 apply(simp) |
873 apply(subst Abs1_eq_iff_fresh(3)) |
831 apply(subst Abs1_eq_iff_fresh(3)) |
874 apply(auto simp add: fresh_Pair)[1] |
832 apply(auto simp add: fresh_Pair)[2] |
875 apply(assumption) |
|
876 done |
833 done |
877 |
834 |
878 lemma Abs1_eq_iff: |
835 lemma Abs1_eq_iff: |
879 fixes x y::"'a::fs" |
836 fixes x y::"'a::fs" |
880 and a b::"'b::at" |
837 and a b::"'b::at" |
884 proof - |
841 proof - |
885 { assume "a = b" |
842 { assume "a = b" |
886 then have "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
843 then have "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
887 } |
844 } |
888 moreover |
845 moreover |
889 { assume *: "a \<noteq> b" and **: "Abs_set {atom a} x = Abs_set {atom b} y" |
846 { assume *: "a \<noteq> b" and **: "[{atom a}]set. x = [{atom b}]set. y" |
890 have #: "atom a \<sharp> Abs_set {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
847 have #: "atom a \<sharp> [{atom b}]set. y" by (simp add: **[symmetric] Abs_fresh_iff) |
891 have "Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_set {atom b} y)" by (simp) |
848 have "[{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp) |
892 also have "\<dots> = Abs_set {atom b} y" |
849 also have "\<dots> = [{atom b}]set. y" |
893 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
850 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
894 also have "\<dots> = Abs_set {atom a} x" using ** by simp |
851 also have "\<dots> = [{atom a}]set. x" using ** by simp |
895 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
852 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
896 } |
853 } |
897 moreover |
854 moreover |
898 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" |
855 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" |
899 have "Abs_set {atom a} x = Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp |
856 have "[{atom a}]set. x = [{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp |
900 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_set {atom b} y" by (simp add: permute_set_def assms) |
857 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp add: permute_set_def assms) |
901 also have "\<dots> = Abs_set {atom b} y" |
858 also have "\<dots> = [{atom b}]set. y" |
902 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
859 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
903 finally have "Abs_set {atom a} x = Abs_set {atom b} y" . |
860 finally have "[{atom a}]set. x = [{atom b}]set. y" . |
904 } |
861 } |
905 ultimately |
862 ultimately |
906 show "Abs_set {atom a} x = Abs_set {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
863 show "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
907 by blast |
864 by blast |
908 next |
865 next |
909 { assume "a = b" |
866 { assume "a = b" |
910 then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
867 then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
911 } |
868 } |