78 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
78 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
79 |
79 |
80 notation |
80 notation |
81 alpha_abs ("_ \<approx>abs _") |
81 alpha_abs ("_ \<approx>abs _") |
82 |
82 |
83 lemma test1: |
83 lemma alpha_abs_swap: |
84 assumes a1: "a \<notin> (supp x) - bs" |
84 assumes a1: "a \<notin> (supp x) - bs" |
85 and a2: "b \<notin> (supp x) - bs" |
85 and a2: "b \<notin> (supp x) - bs" |
86 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
86 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
87 apply(simp) |
87 apply(simp) |
88 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
88 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
89 apply(simp add: alpha_gen) |
89 apply(simp add: alpha_gen) |
90 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
90 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
91 apply(simp add: swap_set_fresh[OF a1 a2]) |
91 apply(simp add: swap_set_not_in[OF a1 a2]) |
92 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
92 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
93 using a1 a2 |
93 using a1 a2 |
94 apply(simp add: fresh_star_def fresh_def) |
94 apply(simp add: fresh_star_def fresh_def) |
95 apply(blast) |
95 apply(blast) |
96 apply(simp add: supp_swap) |
96 apply(simp add: supp_swap) |
97 done |
97 done |
98 |
98 |
99 fun |
99 fun |
100 s_test |
100 supp_abs_fun |
101 where |
101 where |
102 "s_test (bs, x) = (supp x) - bs" |
102 "supp_abs_fun (bs, x) = (supp x) - bs" |
103 |
103 |
104 lemma s_test_lemma: |
104 lemma supp_abs_fun_lemma: |
105 assumes a: "x \<approx>abs y" |
105 assumes a: "x \<approx>abs y" |
106 shows "s_test x = s_test y" |
106 shows "supp_abs_fun x = supp_abs_fun y" |
107 using a |
107 using a |
108 apply(induct rule: alpha_abs.induct) |
108 apply(induct rule: alpha_abs.induct) |
109 apply(simp add: alpha_gen) |
109 apply(simp add: alpha_gen) |
110 done |
110 done |
111 |
111 |
112 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
112 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
113 apply(rule equivpI) |
113 apply(rule equivpI) |
114 unfolding reflp_def symp_def transp_def |
114 unfolding reflp_def symp_def transp_def |
115 apply(simp_all) |
115 apply(simp_all) |
171 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
171 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
172 |
172 |
173 lemma permute_ABS [simp]: |
173 lemma permute_ABS [simp]: |
174 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
174 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
175 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
175 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
176 apply(lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"]) |
176 by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"]) |
177 done |
|
178 |
177 |
179 instance |
178 instance |
180 apply(default) |
179 apply(default) |
181 apply(induct_tac [!] x rule: abs_induct) |
180 apply(induct_tac [!] x rule: abs_induct) |
182 apply(simp_all) |
181 apply(simp_all) |
183 done |
182 done |
184 |
183 |
185 end |
184 end |
186 |
185 |
187 lemma test1_lifted: |
186 quotient_definition |
|
187 "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
|
188 as |
|
189 "supp_abs_fun" |
|
190 |
|
191 lemma supp_Abs_fun_simp: |
|
192 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
|
193 by (lifting supp_abs_fun.simps(1)) |
|
194 |
|
195 lemma supp_Abs_fun_eqvt: |
|
196 shows "(p \<bullet> supp_Abs_fun) = supp_Abs_fun" |
|
197 apply(subst permute_fun_def) |
|
198 apply(subst expand_fun_eq) |
|
199 apply(rule allI) |
|
200 apply(induct_tac x rule: abs_induct) |
|
201 apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) |
|
202 done |
|
203 |
|
204 lemma supp_Abs_fun_fresh: |
|
205 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)" |
|
206 apply(rule fresh_fun_eqvt_app) |
|
207 apply(simp add: supp_Abs_fun_eqvt) |
|
208 apply(simp) |
|
209 done |
|
210 |
|
211 lemma Abs_swap: |
188 assumes a1: "a \<notin> (supp x) - bs" |
212 assumes a1: "a \<notin> (supp x) - bs" |
189 and a2: "b \<notin> (supp x) - bs" |
213 and a2: "b \<notin> (supp x) - bs" |
190 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
214 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
191 using a1 a2 |
215 using a1 a2 by (lifting alpha_abs_swap) |
192 apply(lifting test1) |
|
193 done |
|
194 |
216 |
195 lemma Abs_supports: |
217 lemma Abs_supports: |
196 shows "((supp x) - as) supports (Abs as x)" |
218 shows "((supp x) - as) supports (Abs as x)" |
197 unfolding supports_def |
219 unfolding supports_def |
198 apply(clarify) |
220 apply(clarify) |
199 apply(simp (no_asm)) |
221 apply(simp (no_asm)) |
200 apply(subst test1_lifted[symmetric]) |
222 apply(subst Abs_swap[symmetric]) |
201 apply(simp_all) |
223 apply(simp_all) |
202 done |
224 done |
203 |
225 |
204 quotient_definition |
226 lemma supp_Abs_subset1: |
205 "s_test_lifted :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
|
206 as |
|
207 "s_test" |
|
208 |
|
209 lemma s_test_lifted_simp: |
|
210 shows "s_test_lifted (Abs bs x) = (supp x) - bs" |
|
211 apply(lifting s_test.simps(1)) |
|
212 done |
|
213 |
|
214 lemma s_test_lifted_eqvt: |
|
215 shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)" |
|
216 apply(induct ab rule: abs_induct) |
|
217 apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt) |
|
218 done |
|
219 |
|
220 lemma fresh_f_empty_supp: |
|
221 assumes a: "\<forall>p. p \<bullet> f = f" |
|
222 shows "a \<sharp> x \<Longrightarrow> a \<sharp> (f x)" |
|
223 apply(simp add: fresh_def) |
|
224 apply(simp add: supp_def) |
|
225 apply(simp add: permute_fun_app_eq) |
|
226 apply(simp add: a) |
|
227 apply(rule finite_subset) |
|
228 prefer 2 |
|
229 apply(assumption) |
|
230 apply(auto) |
|
231 done |
|
232 |
|
233 |
|
234 lemma s_test_fresh_lemma: |
|
235 shows "(a \<sharp> Abs bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abs bs x))" |
|
236 apply(rule fresh_f_empty_supp) |
|
237 apply(rule allI) |
|
238 apply(subst permute_fun_def) |
|
239 apply(simp add: s_test_lifted_eqvt) |
|
240 apply(simp) |
|
241 done |
|
242 |
|
243 |
|
244 lemma supp_finite_set: |
|
245 fixes S::"atom set" |
|
246 assumes "finite S" |
|
247 shows "supp S = S" |
|
248 apply(rule finite_supp_unique) |
|
249 apply(simp add: supports_def) |
|
250 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
251 apply(metis) |
|
252 apply(rule assms) |
|
253 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
254 done |
|
255 |
|
256 lemma s_test_subset: |
|
257 fixes x::"'a::fs" |
227 fixes x::"'a::fs" |
258 shows "((supp x) - as) \<subseteq> (supp (Abs as x))" |
228 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
259 apply(rule subsetI) |
229 apply(simp add: supp_conv_fresh) |
260 apply(rule contrapos_pp) |
230 apply(auto) |
261 apply(assumption) |
231 apply(drule_tac supp_Abs_fun_fresh) |
262 unfolding fresh_def[symmetric] |
232 apply(simp only: supp_Abs_fun_simp) |
263 thm s_test_fresh_lemma |
233 apply(simp add: fresh_def) |
264 apply(drule_tac s_test_fresh_lemma) |
234 apply(simp add: supp_finite_atom_set finite_supp) |
265 apply(simp only: s_test_lifted_simp) |
235 done |
266 apply(simp add: fresh_def) |
236 |
267 apply(subgoal_tac "finite (supp x - as)") |
237 lemma supp_Abs_subset2: |
268 apply(simp add: supp_finite_set) |
238 fixes x::"'a::fs" |
269 apply(simp add: finite_supp) |
239 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
270 done |
240 apply(rule supp_is_subset) |
|
241 apply(rule Abs_supports) |
|
242 apply(simp add: finite_supp) |
|
243 done |
271 |
244 |
272 lemma supp_Abs: |
245 lemma supp_Abs: |
273 fixes x::"'a::fs" |
246 fixes x::"'a::fs" |
274 shows "supp (Abs as x) = (supp x) - as" |
247 shows "supp (Abs as x) = (supp x) - as" |
275 apply(rule subset_antisym) |
248 apply(rule_tac subset_antisym) |
276 apply(rule supp_is_subset) |
249 apply(rule supp_Abs_subset2) |
277 apply(rule Abs_supports) |
250 apply(rule supp_Abs_subset1) |
278 apply(simp add: finite_supp) |
251 done |
279 apply(rule s_test_subset) |
|
280 done |
|
281 |
252 |
282 instance abs :: (fs) fs |
253 instance abs :: (fs) fs |
283 apply(default) |
254 apply(default) |
284 apply(induct_tac x rule: abs_induct) |
255 apply(induct_tac x rule: abs_induct) |
285 apply(simp add: supp_Abs) |
256 apply(simp add: supp_Abs) |
286 apply(simp add: finite_supp) |
257 apply(simp add: finite_supp) |
287 done |
258 done |
288 |
259 |
289 lemma fresh_abs: |
260 lemma Abs_fresh_iff: |
290 fixes x::"'a::fs" |
261 fixes x::"'a::fs" |
291 shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))" |
262 shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))" |
|
263 apply(simp add: fresh_def) |
|
264 apply(simp add: supp_Abs) |
|
265 apply(auto) |
|
266 done |
|
267 |
|
268 lemma Abs_eq_iff: |
|
269 shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
|
270 by (lifting alpha_abs.simps(1)) |
|
271 |
|
272 |
|
273 |
|
274 (* |
|
275 below is a construction site for showing that in the |
|
276 single-binder case, the old and new alpha equivalence |
|
277 coincide |
|
278 *) |
|
279 |
|
280 fun |
|
281 alpha1 |
|
282 where |
|
283 "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))" |
|
284 |
|
285 notation |
|
286 alpha1 ("_ \<approx>abs1 _") |
|
287 |
|
288 lemma |
|
289 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
|
290 shows "({a}, x) \<approx>abs ({b}, y)" |
|
291 using a |
|
292 apply(simp) |
|
293 apply(erule disjE) |
|
294 apply(simp) |
|
295 apply(rule exI) |
|
296 apply(rule alpha_gen_refl) |
|
297 apply(simp) |
|
298 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
299 apply(simp add: alpha_gen) |
292 apply(simp add: fresh_def) |
300 apply(simp add: fresh_def) |
293 apply(simp add: supp_Abs) |
301 apply(rule conjI) |
294 apply(auto) |
302 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1]) |
|
303 apply(rule trans) |
|
304 apply(simp add: Diff_eqvt supp_eqvt) |
|
305 apply(subst swap_set_not_in) |
|
306 back |
|
307 apply(simp) |
|
308 apply(simp) |
|
309 apply(simp add: permute_set_eq) |
|
310 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1]) |
|
311 apply(simp add: permute_self) |
|
312 apply(simp add: Diff_eqvt supp_eqvt) |
|
313 apply(simp add: permute_set_eq) |
|
314 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
|
315 apply(simp add: fresh_star_def fresh_def) |
|
316 apply(blast) |
|
317 apply(simp add: supp_swap) |
295 done |
318 done |
296 |
319 |
297 lemma abs_eq: |
|
298 shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
|
299 apply(lifting alpha_abs.simps(1)) |
|
300 done |
|
301 |
320 |
302 end |
321 end |
303 |
322 |