|
1 theory Abs_equiv |
|
2 imports Abs |
|
3 begin |
|
4 |
|
5 (* |
|
6 below is a construction site for showing that in the |
|
7 single-binder case, the old and new alpha equivalence |
|
8 coincide |
|
9 *) |
|
10 |
|
11 fun |
|
12 alpha1 |
|
13 where |
|
14 "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
|
15 |
|
16 notation |
|
17 alpha1 ("_ \<approx>abs1 _") |
|
18 |
|
19 fun |
|
20 alpha2 |
|
21 where |
|
22 "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))" |
|
23 |
|
24 notation |
|
25 alpha2 ("_ \<approx>abs2 _") |
|
26 |
|
27 lemma alpha_old_new: |
|
28 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
|
29 shows "({a}, x) \<approx>abs ({b}, y)" |
|
30 using a |
|
31 apply(simp) |
|
32 apply(erule disjE) |
|
33 apply(simp) |
|
34 apply(rule exI) |
|
35 apply(rule alpha_gen_refl) |
|
36 apply(simp) |
|
37 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
38 apply(simp add: alpha_gen) |
|
39 apply(simp add: fresh_def) |
|
40 apply(rule conjI) |
|
41 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1]) |
|
42 apply(rule trans) |
|
43 apply(simp add: Diff_eqvt supp_eqvt) |
|
44 apply(subst swap_set_not_in) |
|
45 back |
|
46 apply(simp) |
|
47 apply(simp) |
|
48 apply(simp add: permute_set_eq) |
|
49 apply(rule conjI) |
|
50 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1]) |
|
51 apply(simp add: permute_self) |
|
52 apply(simp add: Diff_eqvt supp_eqvt) |
|
53 apply(simp add: permute_set_eq) |
|
54 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
|
55 apply(simp add: fresh_star_def fresh_def) |
|
56 apply(blast) |
|
57 apply(simp add: supp_swap) |
|
58 apply(simp add: eqvts) |
|
59 done |
|
60 |
|
61 |
|
62 lemma perm_induct_test: |
|
63 fixes P :: "perm => bool" |
|
64 assumes fin: "finite (supp p)" |
|
65 assumes zero: "P 0" |
|
66 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
|
67 assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
|
68 shows "P p" |
|
69 using fin |
|
70 apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct) |
|
71 oops |
|
72 |
|
73 lemma ii: |
|
74 assumes "\<forall>x \<in> A. p \<bullet> x = x" |
|
75 shows "p \<bullet> A = A" |
|
76 using assms |
|
77 apply(auto) |
|
78 apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff) |
|
79 apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure) |
|
80 done |
|
81 |
|
82 |
|
83 |
|
84 lemma alpha_abs_Pair: |
|
85 shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2)) |
|
86 \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))" |
|
87 apply(simp add: alpha_gen) |
|
88 apply(simp add: fresh_star_def) |
|
89 apply(simp add: ball_Un Un_Diff) |
|
90 apply(rule iffI) |
|
91 apply(simp) |
|
92 defer |
|
93 apply(simp) |
|
94 apply(rule conjI) |
|
95 apply(clarify) |
|
96 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
97 apply(rule sym) |
|
98 apply(rule ii) |
|
99 apply(simp add: fresh_def supp_perm) |
|
100 apply(clarify) |
|
101 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
102 apply(simp add: fresh_def supp_perm) |
|
103 apply(rule sym) |
|
104 apply(rule ii) |
|
105 apply(simp) |
|
106 done |
|
107 |
|
108 |
|
109 lemma yy: |
|
110 assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" |
|
111 shows "S1 = S2" |
|
112 using assms |
|
113 apply (metis insert_Diff_single insert_absorb) |
|
114 done |
|
115 |
|
116 lemma kk: |
|
117 assumes a: "p \<bullet> x = y" |
|
118 shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y" |
|
119 using a |
|
120 apply(auto) |
|
121 apply(rule_tac p="- p" in permute_boolE) |
|
122 apply(simp add: mem_eqvt supp_eqvt) |
|
123 done |
|
124 |
|
125 lemma ww: |
|
126 assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b" |
|
127 shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x" |
|
128 apply(subgoal_tac "(supp x) supports x") |
|
129 apply(simp add: supports_def) |
|
130 using assms |
|
131 apply - |
|
132 apply(drule_tac x="a" in spec) |
|
133 defer |
|
134 apply(rule supp_supports) |
|
135 apply(auto) |
|
136 apply(rotate_tac 1) |
|
137 apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolI) |
|
138 apply(simp add: mem_eqvt supp_eqvt) |
|
139 done |
|
140 |
|
141 lemma alpha_abs_sym: |
|
142 assumes a: "({a}, x) \<approx>abs ({b}, y)" |
|
143 shows "({b}, y) \<approx>abs ({a}, x)" |
|
144 using a |
|
145 apply(simp) |
|
146 apply(erule exE) |
|
147 apply(rule_tac x="- p" in exI) |
|
148 apply(simp add: alpha_gen) |
|
149 apply(simp add: fresh_star_def fresh_minus_perm) |
|
150 apply (metis permute_minus_cancel(2)) |
|
151 done |
|
152 |
|
153 lemma alpha_abs_trans: |
|
154 assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)" |
|
155 assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)" |
|
156 shows "({a1}, x1) \<approx>abs ({a3}, x3)" |
|
157 using a b |
|
158 apply(simp) |
|
159 apply(erule exE)+ |
|
160 apply(rule_tac x="pa + p" in exI) |
|
161 apply(simp add: alpha_gen) |
|
162 apply(simp add: fresh_star_def fresh_plus_perm) |
|
163 done |
|
164 |
|
165 lemma alpha_equal: |
|
166 assumes a: "({a}, x) \<approx>abs ({a}, y)" |
|
167 shows "(a, x) \<approx>abs1 (a, y)" |
|
168 using a |
|
169 apply(simp) |
|
170 apply(erule exE) |
|
171 apply(simp add: alpha_gen) |
|
172 apply(erule conjE)+ |
|
173 apply(case_tac "a \<notin> supp x") |
|
174 apply(simp) |
|
175 apply(subgoal_tac "supp x \<sharp>* p") |
|
176 apply(drule supp_perm_eq) |
|
177 apply(simp) |
|
178 apply(simp) |
|
179 apply(simp) |
|
180 apply(case_tac "a \<notin> supp y") |
|
181 apply(simp) |
|
182 apply(drule supp_perm_eq) |
|
183 apply(clarify) |
|
184 apply(simp (no_asm_use)) |
|
185 apply(simp) |
|
186 apply(simp) |
|
187 apply(drule yy) |
|
188 apply(simp) |
|
189 apply(simp) |
|
190 apply(simp) |
|
191 apply(case_tac "a \<sharp> p") |
|
192 apply(subgoal_tac "supp y \<sharp>* p") |
|
193 apply(drule supp_perm_eq) |
|
194 apply(clarify) |
|
195 apply(simp (no_asm_use)) |
|
196 apply(metis) |
|
197 apply(auto simp add: fresh_star_def)[1] |
|
198 apply(frule_tac kk) |
|
199 apply(drule_tac x="a" in bspec) |
|
200 apply(simp) |
|
201 apply(simp add: fresh_def) |
|
202 apply(simp add: supp_perm) |
|
203 apply(subgoal_tac "((p \<bullet> a) \<sharp> p)") |
|
204 apply(simp add: fresh_def supp_perm) |
|
205 apply(simp add: fresh_star_def) |
|
206 done |
|
207 |
|
208 lemma alpha_unequal: |
|
209 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b" |
|
210 shows "(a, x) \<approx>abs1 (b, y)" |
|
211 using a |
|
212 apply - |
|
213 apply(subgoal_tac "a \<notin> supp x - {a}") |
|
214 apply(subgoal_tac "b \<notin> supp x - {a}") |
|
215 defer |
|
216 apply(simp add: alpha_gen) |
|
217 apply(simp) |
|
218 apply(drule_tac abs_swap1) |
|
219 apply(assumption) |
|
220 apply(simp only: insert_eqvt empty_eqvt swap_atom_simps) |
|
221 apply(simp only: abs_eq_iff) |
|
222 apply(drule alphas_abs_sym) |
|
223 apply(rotate_tac 4) |
|
224 apply(drule_tac alpha_abs_trans) |
|
225 apply(assumption) |
|
226 apply(drule alpha_equal) |
|
227 apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolE) |
|
228 apply(simp add: fresh_eqvt) |
|
229 apply(simp add: fresh_def) |
|
230 done |
|
231 |
|
232 lemma alpha_new_old: |
|
233 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" |
|
234 shows "(a, x) \<approx>abs1 (b, y)" |
|
235 using a |
|
236 apply(case_tac "a=b") |
|
237 apply(simp only: alpha_equal) |
|
238 apply(drule alpha_unequal) |
|
239 apply(simp) |
|
240 apply(simp) |
|
241 apply(simp) |
|
242 done |
|
243 |
|
244 end |