258 and b: "A \<inter> B1 = {}" "A \<inter> B2 = {}" |
258 and b: "A \<inter> B1 = {}" "A \<inter> B2 = {}" |
259 shows "B1 = B2" |
259 shows "B1 = B2" |
260 using a b |
260 using a b |
261 by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2) |
261 by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2) |
262 |
262 |
263 lemma supp_property_set: |
|
264 assumes a: "(as, x) \<approx>set (op =) supp p (as', x')" |
|
265 shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
|
266 proof - |
|
267 from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas) |
|
268 then have *: "p \<bullet> (supp x - as) = (supp x - as)" |
|
269 by (simp add: atom_set_perm_eq) |
|
270 have "(supp x' - as') \<union> (supp x' \<inter> as') = supp x'" by auto |
|
271 also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas) |
|
272 also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt) |
|
273 also have "\<dots> = p \<bullet> ((supp x - as) \<union> (supp x \<inter> as))" by auto |
|
274 also have "\<dots> = (p \<bullet> (supp x - as)) \<union> (p \<bullet> (supp x \<inter> as))" by (simp add: union_eqvt) |
|
275 also have "\<dots> = (supp x - as) \<union> (p \<bullet> (supp x \<inter> as))" using * by simp |
|
276 also have "\<dots> = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" using a by (simp add: alphas) |
|
277 finally have "(supp x' - as') \<union> (supp x' \<inter> as') = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" . |
|
278 moreover |
|
279 have "(supp x' - as') \<inter> (supp x' \<inter> as') = {}" by auto |
|
280 moreover |
|
281 have "(supp x - as) \<inter> (supp x \<inter> as) = {}" by auto |
|
282 then have "p \<bullet> ((supp x - as) \<inter> (supp x \<inter> as) = {})" by (simp add: permute_bool_def) |
|
283 then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp) |
|
284 then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp |
|
285 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas) |
|
286 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
|
287 by (auto dest: disjoint_right_eq) |
|
288 qed |
|
289 |
|
290 lemma supp_property_res: |
263 lemma supp_property_res: |
291 assumes a: "(as, x) \<approx>res (op =) supp p (as', x')" |
264 assumes a: "(as, x) \<approx>res (op =) supp p (as', x')" |
292 shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
265 shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
293 proof - |
266 proof - |
294 from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas) |
267 from a have "(supp x - as) \<sharp>* p" by (auto simp only: alphas) |
312 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas) |
285 then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas) |
313 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
286 ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'" |
314 by (auto dest: disjoint_right_eq) |
287 by (auto dest: disjoint_right_eq) |
315 qed |
288 qed |
316 |
289 |
317 lemma supp_property_list: |
290 lemma alpha_abs_res_stronger1_aux: |
318 assumes a: "(as, x) \<approx>lst (op =) supp p (as', x')" |
|
319 shows "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'" |
|
320 proof - |
|
321 from a have "(supp x - set as) \<sharp>* p" by (auto simp only: alphas) |
|
322 then have *: "p \<bullet> (supp x - set as) = (supp x - set as)" |
|
323 by (simp add: atom_set_perm_eq) |
|
324 have "(supp x' - set as') \<union> (supp x' \<inter> set as') = supp x'" by auto |
|
325 also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas) |
|
326 also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt) |
|
327 also have "\<dots> = p \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))" by auto |
|
328 also have "\<dots> = (p \<bullet> (supp x - set as)) \<union> (p \<bullet> (supp x \<inter> set as))" by (simp add: union_eqvt) |
|
329 also have "\<dots> = (supp x - set as) \<union> (p \<bullet> (supp x \<inter> set as))" using * by simp |
|
330 also have "\<dots> = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" using a by (simp add: alphas) |
|
331 finally |
|
332 have "(supp x' - set as') \<union> (supp x' \<inter> set as') = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" . |
|
333 moreover |
|
334 have "(supp x' - set as') \<inter> (supp x' \<inter> set as') = {}" by auto |
|
335 moreover |
|
336 have "(supp x - set as) \<inter> (supp x \<inter> set as) = {}" by auto |
|
337 then have "p \<bullet> ((supp x - set as) \<inter> (supp x \<inter> set as) = {})" by (simp add: permute_bool_def) |
|
338 then have "(p \<bullet> (supp x - set as)) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" by (perm_simp) (simp) |
|
339 then have "(supp x - set as) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using * by simp |
|
340 then have "(supp x' - set as') \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using a by (simp add: alphas) |
|
341 ultimately show "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'" |
|
342 by (auto dest: disjoint_right_eq) |
|
343 qed |
|
344 |
|
345 lemma alpha_abs_res_stronger1: |
|
346 fixes x::"'a::fs" |
|
347 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
291 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
348 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" |
292 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" |
349 proof - |
293 proof - |
350 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
294 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
351 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
295 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
374 have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas) |
318 have "(as, x) \<approx>res (op =) supp p (as', x')" using asm 1 a by (simp add: alphas) |
375 ultimately |
319 ultimately |
376 show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast |
320 show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast |
377 qed |
321 qed |
378 |
322 |
|
323 lemma alpha_abs_res_stronger1: |
|
324 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" |
|
325 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |
|
326 using alpha_abs_res_stronger1_aux[OF asm] by auto |
|
327 |
379 lemma alpha_abs_set_stronger1: |
328 lemma alpha_abs_set_stronger1: |
380 fixes x::"'a::fs" |
|
381 assumes asm: "(as, x) \<approx>set (op =) supp p' (as', x')" |
329 assumes asm: "(as, x) \<approx>set (op =) supp p' (as', x')" |
382 shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |
330 shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" |
383 proof - |
331 proof - |
384 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
332 from asm have 0: "(supp x - as) \<sharp>* p'" by (auto simp only: alphas) |
385 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
333 then have #: "p' \<bullet> (supp x - as) = (supp x - as)" |
419 have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas) |
367 have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas) |
420 ultimately |
368 ultimately |
421 show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast |
369 show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast |
422 qed |
370 qed |
423 |
371 |
424 |
372 lemma alpha_abs_lst_stronger1: |
|
373 assumes asm: "(as, x) \<approx>lst (op =) supp p' (as', x')" |
|
374 shows "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'" |
|
375 proof - |
|
376 from asm have 0: "(supp x - set as) \<sharp>* p'" by (auto simp only: alphas) |
|
377 then have #: "p' \<bullet> (supp x - set as) = (supp x - set as)" |
|
378 by (simp add: atom_set_perm_eq) |
|
379 obtain p where *: "\<forall>b \<in> (supp x \<union> set as). p \<bullet> b = p' \<bullet> b" |
|
380 and **: "supp p \<subseteq> (supp x \<union> set as) \<union> p' \<bullet> (supp x \<union> set as)" |
|
381 using set_renaming_perm2 by blast |
|
382 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast |
|
383 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto |
|
384 from * have "\<forall>b \<in> set as. p \<bullet> b = p' \<bullet> b" by blast |
|
385 then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto) |
|
386 have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt) |
|
387 from 0 have 1: "(supp x - set as) \<sharp>* p" using * |
|
388 by (auto simp add: fresh_star_def fresh_perm) |
|
389 then have 2: "(supp x - set as) \<inter> supp p = {}" |
|
390 by (auto simp add: fresh_star_def fresh_def) |
|
391 have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto |
|
392 have "supp p \<subseteq> supp x \<union> set as \<union> p' \<bullet> supp x \<union> p' \<bullet> set as" using ** using union_eqvt by blast |
|
393 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> |
|
394 (p' \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))) \<union> p' \<bullet> set as" using b by simp |
|
395 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> |
|
396 ((p' \<bullet> (supp x - set as)) \<union> (p' \<bullet> (supp x \<inter> set as))) \<union> p' \<bullet> set as" by (simp add: union_eqvt) |
|
397 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> |
|
398 (p' \<bullet> (supp x \<inter> set as)) \<union> p' \<bullet> set as" using # by auto |
|
399 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> ((supp x \<inter> set as) \<union> set as)" |
|
400 using union_eqvt by auto |
|
401 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> set as" |
|
402 by (metis Int_commute Un_commute sup_inf_absorb) |
|
403 also have "\<dots> = (supp x - set as) \<union> set as \<union> p' \<bullet> set as" by blast |
|
404 finally have "supp p \<subseteq> (supp x - set as) \<union> set as \<union> p' \<bullet> set as" . |
|
405 then have "supp p \<subseteq> set as \<union> p' \<bullet> set as" using 2 by blast |
|
406 moreover |
|
407 have "(as, x) \<approx>lst (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas) |
|
408 ultimately |
|
409 show "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'" using zc by blast |
|
410 qed |
|
411 |
|
412 lemma alphas_abs_stronger: |
|
413 shows "(as, x) \<approx>abs_set (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')" |
|
414 and "(as, x) \<approx>abs_res (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')" |
|
415 and "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow> |
|
416 (\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')" |
|
417 apply(rule iffI) |
|
418 apply(auto simp add: alphas_abs alpha_abs_set_stronger1)[1] |
|
419 apply(auto simp add: alphas_abs)[1] |
|
420 apply(rule iffI) |
|
421 apply(auto simp add: alphas_abs alpha_abs_res_stronger1)[1] |
|
422 apply(auto simp add: alphas_abs)[1] |
|
423 apply(rule iffI) |
|
424 apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1] |
|
425 apply(auto simp add: alphas_abs)[1] |
|
426 done |
425 |
427 |
426 section {* Quotient types *} |
428 section {* Quotient types *} |
427 |
429 |
428 quotient_type |
430 quotient_type |
429 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
431 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
471 lemma Abs_eq_iff: |
473 lemma Abs_eq_iff: |
472 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))" |
474 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))" |
473 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
475 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
474 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
476 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
475 by (lifting alphas_abs) |
477 by (lifting alphas_abs) |
|
478 |
|
479 lemma Abs_eq_iff2: |
|
480 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
|
481 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
|
482 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
|
483 (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)" |
|
484 by (lifting alphas_abs_stronger) |
476 |
485 |
477 lemma Abs_exhausts: |
486 lemma Abs_exhausts: |
478 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1" |
487 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1" |
479 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2" |
488 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2" |
480 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3" |
489 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3" |