114 unfolding supp_eqvt[symmetric] |
114 unfolding supp_eqvt[symmetric] |
115 unfolding Diff_eqvt[symmetric] |
115 unfolding Diff_eqvt[symmetric] |
116 apply(erule_tac [!] exE) |
116 apply(erule_tac [!] exE) |
117 apply(rule_tac [!] x="p \<bullet> pa" in exI) |
117 apply(rule_tac [!] x="p \<bullet> pa" in exI) |
118 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) |
118 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) |
119 |
|
120 lemma alphas_abs_swap1: |
|
121 assumes a1: "a \<notin> (supp x) - bs" |
|
122 and a2: "b \<notin> (supp x) - bs" |
|
123 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
|
124 and "(bs, x) \<approx>abs_res ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
|
125 using a1 a2 |
|
126 unfolding alphas_abs |
|
127 unfolding alphas |
|
128 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
|
129 unfolding fresh_star_def fresh_def |
|
130 unfolding swap_set_not_in[OF a1 a2] |
|
131 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
132 (auto simp add: supp_perm swap_atom) |
|
133 |
|
134 lemma alphas_abs_swap2: |
|
135 assumes a1: "a \<notin> (supp x) - (set bs)" |
|
136 and a2: "b \<notin> (supp x) - (set bs)" |
|
137 shows "(bs, x) \<approx>abs_lst ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
|
138 using a1 a2 |
|
139 unfolding alphas_abs |
|
140 unfolding alphas |
|
141 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
|
142 unfolding fresh_star_def fresh_def |
|
143 unfolding swap_set_not_in[OF a1 a2] |
|
144 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
145 (auto simp add: supp_perm swap_atom) |
|
146 |
119 |
147 fun |
120 fun |
148 aux_set |
121 aux_set |
149 where |
122 where |
150 "aux_set (bs, x) = (supp x) - bs" |
123 "aux_set (bs, x) = (supp x) - bs" |
225 |
198 |
226 lemma abs_inducts: |
199 lemma abs_inducts: |
227 shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1" |
200 shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1" |
228 and "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2" |
201 and "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2" |
229 and "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3" |
202 and "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3" |
230 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) |
203 by (lifting prod.induct[where 'a="atom set" and 'b="'a"] |
231 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) |
204 prod.induct[where 'a="atom set" and 'b="'a"] |
232 apply(lifting prod.induct[where 'a="atom list" and 'b="'a"]) |
205 prod.induct[where 'a="atom list" and 'b="'a"]) |
|
206 |
|
207 lemma abs_eq_iff: |
|
208 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
|
209 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
|
210 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
|
211 apply(simp_all) |
|
212 apply(lifting alphas_abs) |
233 done |
213 done |
234 |
214 |
235 instantiation abs_gen :: (pt) pt |
215 instantiation abs_gen :: (pt) pt |
236 begin |
216 begin |
237 |
217 |
295 |
275 |
296 end |
276 end |
297 |
277 |
298 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst |
278 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst |
299 |
279 |
|
280 lemma abs_swap1: |
|
281 assumes a1: "a \<notin> (supp x) - bs" |
|
282 and a2: "b \<notin> (supp x) - bs" |
|
283 shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
284 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
285 unfolding abs_eq_iff |
|
286 unfolding alphas_abs |
|
287 unfolding alphas |
|
288 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
|
289 unfolding fresh_star_def fresh_def |
|
290 unfolding swap_set_not_in[OF a1 a2] |
|
291 using a1 a2 |
|
292 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
293 (auto simp add: supp_perm swap_atom) |
|
294 |
|
295 lemma abs_swap2: |
|
296 assumes a1: "a \<notin> (supp x) - (set bs)" |
|
297 and a2: "b \<notin> (supp x) - (set bs)" |
|
298 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
299 unfolding abs_eq_iff |
|
300 unfolding alphas_abs |
|
301 unfolding alphas |
|
302 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
|
303 unfolding fresh_star_def fresh_def |
|
304 unfolding swap_set_not_in[OF a1 a2] |
|
305 using a1 a2 |
|
306 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
307 (auto simp add: supp_perm swap_atom) |
|
308 |
|
309 lemma abs_supports: |
|
310 shows "((supp x) - as) supports (Abs as x)" |
|
311 and "((supp x) - as) supports (Abs_res as x)" |
|
312 and "((supp x) - (set bs)) supports (Abs_lst bs x)" |
|
313 unfolding supports_def |
|
314 unfolding permute_abs |
|
315 by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric]) |
300 |
316 |
301 quotient_definition |
317 quotient_definition |
302 "supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set" |
318 "supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set" |
303 is |
319 is |
304 "aux_set" |
320 "aux_set" |
315 |
331 |
316 lemma aux_supps: |
332 lemma aux_supps: |
317 shows "supp_gen (Abs bs x) = (supp x) - bs" |
333 shows "supp_gen (Abs bs x) = (supp x) - bs" |
318 and "supp_res (Abs_res bs x) = (supp x) - bs" |
334 and "supp_res (Abs_res bs x) = (supp x) - bs" |
319 and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
335 and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
320 apply(lifting aux_set.simps) |
336 by (lifting aux_set.simps aux_set.simps aux_list.simps) |
321 apply(lifting aux_set.simps) |
|
322 apply(lifting aux_list.simps) |
|
323 done |
|
324 |
337 |
325 lemma aux_supp_eqvt[eqvt]: |
338 lemma aux_supp_eqvt[eqvt]: |
326 shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)" |
339 shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)" |
327 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
340 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
328 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
341 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
340 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
353 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
341 apply(rule_tac [!] fresh_fun_eqvt_app) |
354 apply(rule_tac [!] fresh_fun_eqvt_app) |
342 apply(simp_all add: eqvts_raw) |
355 apply(simp_all add: eqvts_raw) |
343 done |
356 done |
344 |
357 |
345 lemma abs_swap1: |
|
346 assumes a1: "a \<notin> (supp x) - bs" |
|
347 and a2: "b \<notin> (supp x) - bs" |
|
348 shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
349 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
350 using a1 a2 |
|
351 apply(lifting alphas_abs_swap1(1)) |
|
352 apply(lifting alphas_abs_swap1(2)) |
|
353 done |
|
354 |
|
355 lemma abs_swap2: |
|
356 assumes a1: "a \<notin> (supp x) - (set bs)" |
|
357 and a2: "b \<notin> (supp x) - (set bs)" |
|
358 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
359 using a1 a2 by (lifting alphas_abs_swap2) |
|
360 |
|
361 lemma abs_supports: |
|
362 shows "((supp x) - as) supports (Abs as x)" |
|
363 and "((supp x) - as) supports (Abs_res as x)" |
|
364 and "((supp x) - (set bs)) supports (Abs_lst bs x)" |
|
365 unfolding supports_def |
|
366 unfolding permute_abs |
|
367 by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric]) |
|
368 |
|
369 lemma supp_abs_subset1: |
358 lemma supp_abs_subset1: |
370 assumes a: "finite (supp x)" |
359 assumes a: "finite (supp x)" |
371 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
360 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
372 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
361 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
373 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)" |
362 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)" |
427 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
416 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
428 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
417 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
429 unfolding fresh_def |
418 unfolding fresh_def |
430 unfolding supp_abs |
419 unfolding supp_abs |
431 by auto |
420 by auto |
432 |
|
433 lemma abs_eq_iff: |
|
434 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
|
435 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
|
436 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
|
437 apply(simp_all) |
|
438 apply(lifting alphas_abs) |
|
439 done |
|
440 |
421 |
441 |
422 |
442 section {* BELOW is stuff that may or may not be needed *} |
423 section {* BELOW is stuff that may or may not be needed *} |
443 |
424 |
444 (* support of concrete atom sets *) |
425 (* support of concrete atom sets *) |