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"]) |
233 done |
|
234 |
206 |
235 instantiation abs_gen :: (pt) pt |
207 instantiation abs_gen :: (pt) pt |
236 begin |
208 begin |
237 |
209 |
238 quotient_definition |
210 quotient_definition |
315 |
287 |
316 lemma aux_supps: |
288 lemma aux_supps: |
317 shows "supp_gen (Abs bs x) = (supp x) - bs" |
289 shows "supp_gen (Abs bs x) = (supp x) - bs" |
318 and "supp_res (Abs_res bs x) = (supp x) - bs" |
290 and "supp_res (Abs_res bs x) = (supp x) - bs" |
319 and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
291 and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
320 apply(lifting aux_set.simps) |
292 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 |
293 |
325 lemma aux_supp_eqvt[eqvt]: |
294 lemma aux_supp_eqvt[eqvt]: |
326 shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)" |
295 shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)" |
327 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
296 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
328 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
297 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)" |
309 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
341 apply(rule_tac [!] fresh_fun_eqvt_app) |
310 apply(rule_tac [!] fresh_fun_eqvt_app) |
342 apply(simp_all add: eqvts_raw) |
311 apply(simp_all add: eqvts_raw) |
343 done |
312 done |
344 |
313 |
|
314 lemma abs_eq_iff: |
|
315 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
|
316 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
|
317 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
|
318 apply(simp_all) |
|
319 apply(lifting alphas_abs) |
|
320 done |
|
321 |
345 lemma abs_swap1: |
322 lemma abs_swap1: |
346 assumes a1: "a \<notin> (supp x) - bs" |
323 assumes a1: "a \<notin> (supp x) - bs" |
347 and a2: "b \<notin> (supp x) - bs" |
324 and a2: "b \<notin> (supp x) - bs" |
348 shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
325 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)" |
326 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
350 using a1 a2 |
327 unfolding abs_eq_iff |
351 apply(lifting alphas_abs_swap1(1)) |
328 unfolding alphas_abs |
352 apply(lifting alphas_abs_swap1(2)) |
329 unfolding alphas |
353 done |
330 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
|
331 unfolding fresh_star_def fresh_def |
|
332 unfolding swap_set_not_in[OF a1 a2] |
|
333 using a1 a2 |
|
334 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
335 (auto simp add: supp_perm swap_atom) |
354 |
336 |
355 lemma abs_swap2: |
337 lemma abs_swap2: |
356 assumes a1: "a \<notin> (supp x) - (set bs)" |
338 assumes a1: "a \<notin> (supp x) - (set bs)" |
357 and a2: "b \<notin> (supp x) - (set bs)" |
339 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)" |
340 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) |
341 unfolding abs_eq_iff |
|
342 unfolding alphas_abs |
|
343 unfolding alphas |
|
344 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
|
345 unfolding fresh_star_def fresh_def |
|
346 unfolding swap_set_not_in[OF a1 a2] |
|
347 using a1 a2 |
|
348 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
349 (auto simp add: supp_perm swap_atom) |
360 |
350 |
361 lemma abs_supports: |
351 lemma abs_supports: |
362 shows "((supp x) - as) supports (Abs as x)" |
352 shows "((supp x) - as) supports (Abs as x)" |
363 and "((supp x) - as) supports (Abs_res as x)" |
353 and "((supp x) - as) supports (Abs_res as x)" |
364 and "((supp x) - (set bs)) supports (Abs_lst bs x)" |
354 and "((supp x) - (set bs)) supports (Abs_lst bs x)" |
427 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
417 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)" |
418 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 |
419 unfolding fresh_def |
430 unfolding supp_abs |
420 unfolding supp_abs |
431 by auto |
421 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 |
422 |
441 |
423 |
442 section {* BELOW is stuff that may or may not be needed *} |
424 section {* BELOW is stuff that may or may not be needed *} |
443 |
425 |
444 (* support of concrete atom sets *) |
426 (* support of concrete atom sets *) |