210 then (\<lambda>c. if a = c then b else if b = c then a else c) |
210 then (\<lambda>c. if a = c then b else if b = c then a else c) |
211 else id)" |
211 else id)" |
212 unfolding swap_def |
212 unfolding swap_def |
213 apply (rule Abs_perm_inverse) |
213 apply (rule Abs_perm_inverse) |
214 apply (rule permI) |
214 apply (rule permI) |
215 apply (auto simp add: bij_def inj_on_def surj_def)[1] |
215 apply (auto simp: bij_def inj_on_def surj_def)[1] |
216 apply (rule MOST_rev_mp [OF MOST_neq(1) [of a]]) |
216 apply (rule MOST_rev_mp [OF MOST_neq(1) [of a]]) |
217 apply (rule MOST_rev_mp [OF MOST_neq(1) [of b]]) |
217 apply (rule MOST_rev_mp [OF MOST_neq(1) [of b]]) |
218 apply (simp) |
218 apply (simp) |
219 apply (simp) |
219 apply (simp) |
220 done |
220 done |
252 assumes "a \<noteq> b" and "c \<noteq> b" |
252 assumes "a \<noteq> b" and "c \<noteq> b" |
253 assumes "sort_of a = sort_of b" "sort_of b = sort_of c" |
253 assumes "sort_of a = sort_of b" "sort_of b = sort_of c" |
254 shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)" |
254 shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)" |
255 using assms |
255 using assms |
256 by (rule_tac Rep_perm_ext) |
256 by (rule_tac Rep_perm_ext) |
257 (auto simp add: Rep_perm_simps fun_eq_iff) |
257 (auto simp: Rep_perm_simps fun_eq_iff) |
258 |
258 |
259 |
259 |
260 section {* Permutation Types *} |
260 section {* Permutation Types *} |
261 |
261 |
262 text {* |
262 text {* |
465 |
465 |
466 lemma swap_set_not_in: |
466 lemma swap_set_not_in: |
467 assumes a: "a \<notin> S" "b \<notin> S" |
467 assumes a: "a \<notin> S" "b \<notin> S" |
468 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
468 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
469 unfolding permute_set_def |
469 unfolding permute_set_def |
470 using a by (auto simp add: swap_atom) |
470 using a by (auto simp: swap_atom) |
471 |
471 |
472 lemma swap_set_in: |
472 lemma swap_set_in: |
473 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
473 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
474 shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S" |
474 shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S" |
475 unfolding permute_set_def |
475 unfolding permute_set_def |
476 using a by (auto simp add: swap_atom) |
476 using a by (auto simp: swap_atom) |
477 |
477 |
478 lemma swap_set_in_eq: |
478 lemma swap_set_in_eq: |
479 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
479 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
480 shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}" |
480 shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}" |
481 unfolding permute_set_def |
481 unfolding permute_set_def |
482 using a by (auto simp add: swap_atom) |
482 using a by (auto simp: swap_atom) |
483 |
483 |
484 lemma swap_set_both_in: |
484 lemma swap_set_both_in: |
485 assumes a: "a \<in> S" "b \<in> S" |
485 assumes a: "a \<in> S" "b \<in> S" |
486 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
486 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
487 unfolding permute_set_def |
487 unfolding permute_set_def |
488 using a by (auto simp add: swap_atom) |
488 using a by (auto simp: swap_atom) |
489 |
489 |
490 lemma mem_permute_iff: |
490 lemma mem_permute_iff: |
491 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
491 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
492 unfolding permute_set_def |
492 unfolding permute_set_def |
493 by auto |
493 by auto |
862 by (simp add: perm_eq_iff) |
862 by (simp add: perm_eq_iff) |
863 |
863 |
864 lemma swap_eqvt [eqvt]: |
864 lemma swap_eqvt [eqvt]: |
865 shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)" |
865 shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)" |
866 unfolding permute_perm_def |
866 unfolding permute_perm_def |
867 by (auto simp add: swap_atom perm_eq_iff) |
867 by (auto simp: swap_atom perm_eq_iff) |
868 |
868 |
869 lemma uminus_eqvt [eqvt]: |
869 lemma uminus_eqvt [eqvt]: |
870 fixes p q::"perm" |
870 fixes p q::"perm" |
871 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
871 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
872 unfolding permute_perm_def |
872 unfolding permute_perm_def |
967 by (auto) |
967 by (auto) |
968 |
968 |
969 lemma Collect_eqvt [eqvt]: |
969 lemma Collect_eqvt [eqvt]: |
970 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}" |
970 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}" |
971 unfolding permute_set_eq permute_fun_def |
971 unfolding permute_set_eq permute_fun_def |
972 by (auto simp add: permute_bool_def) |
972 by (auto simp: permute_bool_def) |
973 |
973 |
974 lemma inter_eqvt [eqvt]: |
974 lemma inter_eqvt [eqvt]: |
975 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
975 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
976 unfolding Int_def by simp |
976 unfolding Int_def by simp |
977 |
977 |
1499 shows "supp p = {a. p \<bullet> a \<noteq> a}" |
1499 shows "supp p = {a. p \<bullet> a \<noteq> a}" |
1500 apply (rule finite_supp_unique) |
1500 apply (rule finite_supp_unique) |
1501 apply (rule supports_perm) |
1501 apply (rule supports_perm) |
1502 apply (rule finite_perm_lemma) |
1502 apply (rule finite_perm_lemma) |
1503 apply (simp add: perm_swap_eq swap_eqvt) |
1503 apply (simp add: perm_swap_eq swap_eqvt) |
1504 apply (auto simp add: perm_eq_iff swap_atom) |
1504 apply (auto simp: perm_eq_iff swap_atom) |
1505 done |
1505 done |
1506 |
1506 |
1507 lemma fresh_perm: |
1507 lemma fresh_perm: |
1508 shows "a \<sharp> p \<longleftrightarrow> p \<bullet> a = a" |
1508 shows "a \<sharp> p \<longleftrightarrow> p \<bullet> a = a" |
1509 unfolding fresh_def |
1509 unfolding fresh_def |
1510 by (simp add: supp_perm) |
1510 by (simp add: supp_perm) |
1511 |
1511 |
1512 lemma supp_swap: |
1512 lemma supp_swap: |
1513 shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})" |
1513 shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})" |
1514 by (auto simp add: supp_perm swap_atom) |
1514 by (auto simp: supp_perm swap_atom) |
1515 |
1515 |
1516 lemma fresh_swap: |
1516 lemma fresh_swap: |
1517 shows "a \<sharp> (b \<rightleftharpoons> c) \<longleftrightarrow> (sort_of b \<noteq> sort_of c) \<or> b = c \<or> (a \<sharp> b \<and> a \<sharp> c)" |
1517 shows "a \<sharp> (b \<rightleftharpoons> c) \<longleftrightarrow> (sort_of b \<noteq> sort_of c) \<or> b = c \<or> (a \<sharp> b \<and> a \<sharp> c)" |
1518 by (simp add: fresh_def supp_swap supp_atom) |
1518 by (simp add: fresh_def supp_swap supp_atom) |
1519 |
1519 |
1529 fixes p q::perm |
1529 fixes p q::perm |
1530 assumes "a \<sharp> p" "a \<sharp> q" |
1530 assumes "a \<sharp> p" "a \<sharp> q" |
1531 shows "a \<sharp> (p + q)" |
1531 shows "a \<sharp> (p + q)" |
1532 using assms |
1532 using assms |
1533 unfolding fresh_def |
1533 unfolding fresh_def |
1534 by (auto simp add: supp_perm) |
1534 by (auto simp: supp_perm) |
1535 |
1535 |
1536 lemma supp_plus_perm: |
1536 lemma supp_plus_perm: |
1537 fixes p q::perm |
1537 fixes p q::perm |
1538 shows "supp (p + q) \<subseteq> supp p \<union> supp q" |
1538 shows "supp (p + q) \<subseteq> supp p \<union> supp q" |
1539 by (auto simp add: supp_perm) |
1539 by (auto simp: supp_perm) |
1540 |
1540 |
1541 lemma fresh_minus_perm: |
1541 lemma fresh_minus_perm: |
1542 fixes p::perm |
1542 fixes p::perm |
1543 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
1543 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
1544 unfolding fresh_def |
1544 unfolding fresh_def |
1723 shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs" |
1723 shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs" |
1724 by (simp add: fresh_def supp_Cons) |
1724 by (simp add: fresh_def supp_Cons) |
1725 |
1725 |
1726 lemma supp_append: |
1726 lemma supp_append: |
1727 shows "supp (xs @ ys) = supp xs \<union> supp ys" |
1727 shows "supp (xs @ ys) = supp xs \<union> supp ys" |
1728 by (induct xs) (auto simp add: supp_Nil supp_Cons) |
1728 by (induct xs) (auto simp: supp_Nil supp_Cons) |
1729 |
1729 |
1730 lemma fresh_append: |
1730 lemma fresh_append: |
1731 shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys" |
1731 shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys" |
1732 by (induct xs) (simp_all add: fresh_Nil fresh_Cons) |
1732 by (induct xs) (simp_all add: fresh_Nil fresh_Cons) |
1733 |
1733 |
1734 lemma supp_rev: |
1734 lemma supp_rev: |
1735 shows "supp (rev xs) = supp xs" |
1735 shows "supp (rev xs) = supp xs" |
1736 by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil) |
1736 by (induct xs) (auto simp: supp_append supp_Cons supp_Nil) |
1737 |
1737 |
1738 lemma fresh_rev: |
1738 lemma fresh_rev: |
1739 shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs" |
1739 shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs" |
1740 by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) |
1740 by (induct xs) (auto simp: fresh_append fresh_Cons fresh_Nil) |
1741 |
1741 |
1742 lemma supp_removeAll: |
1742 lemma supp_removeAll: |
1743 fixes x::"atom" |
1743 fixes x::"atom" |
1744 shows "supp (removeAll x xs) = supp xs - {x}" |
1744 shows "supp (removeAll x xs) = supp xs - {x}" |
1745 by (induct xs) |
1745 by (induct xs) |
1746 (auto simp add: supp_Nil supp_Cons supp_atom) |
1746 (auto simp: supp_Nil supp_Cons supp_atom) |
1747 |
1747 |
1748 lemma supp_of_atom_list: |
1748 lemma supp_of_atom_list: |
1749 fixes as::"atom list" |
1749 fixes as::"atom list" |
1750 shows "supp as = set as" |
1750 shows "supp as = set as" |
1751 by (induct as) |
1751 by (induct as) |
2009 lemma fresh_minus_atom_set: |
2009 lemma fresh_minus_atom_set: |
2010 fixes S::"atom set" |
2010 fixes S::"atom set" |
2011 assumes "finite S" |
2011 assumes "finite S" |
2012 shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)" |
2012 shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)" |
2013 unfolding fresh_def |
2013 unfolding fresh_def |
2014 by (auto simp add: supp_finite_atom_set assms) |
2014 by (auto simp: supp_finite_atom_set assms) |
2015 |
2015 |
2016 lemma Union_supports_set: |
2016 lemma Union_supports_set: |
2017 shows "(\<Union>x \<in> S. supp x) supports S" |
2017 shows "(\<Union>x \<in> S. supp x) supports S" |
2018 proof - |
2018 proof - |
2019 { fix a b |
2019 { fix a b |
2027 |
2027 |
2028 lemma Union_of_finite_supp_sets: |
2028 lemma Union_of_finite_supp_sets: |
2029 fixes S::"('a::fs set)" |
2029 fixes S::"('a::fs set)" |
2030 assumes fin: "finite S" |
2030 assumes fin: "finite S" |
2031 shows "finite (\<Union>x\<in>S. supp x)" |
2031 shows "finite (\<Union>x\<in>S. supp x)" |
2032 using fin by (induct) (auto simp add: finite_supp) |
2032 using fin by (induct) (auto simp: finite_supp) |
2033 |
2033 |
2034 lemma Union_included_in_supp: |
2034 lemma Union_included_in_supp: |
2035 fixes S::"('a::fs set)" |
2035 fixes S::"('a::fs set)" |
2036 assumes fin: "finite S" |
2036 assumes fin: "finite S" |
2037 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
2037 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
2187 by (simp only: supp_of_multisets Union_finite_multiset) |
2187 by (simp only: supp_of_multisets Union_finite_multiset) |
2188 |
2188 |
2189 lemma supp_of_multiset_union: |
2189 lemma supp_of_multiset_union: |
2190 fixes M N::"('a::fs) multiset" |
2190 fixes M N::"('a::fs) multiset" |
2191 shows "supp (M + N) = supp M \<union> supp N" |
2191 shows "supp (M + N) = supp M \<union> supp N" |
2192 by (auto simp add: supp_of_multisets) |
2192 by (auto simp: supp_of_multisets) |
2193 |
2193 |
2194 lemma supp_empty_mset [simp]: |
2194 lemma supp_empty_mset [simp]: |
2195 shows "supp {#} = {}" |
2195 shows "supp {#} = {}" |
2196 unfolding supp_def |
2196 unfolding supp_def |
2197 by simp |
2197 by simp |
2272 by (simp add: supp_def) |
2272 by (simp add: supp_def) |
2273 |
2273 |
2274 lemma supp_finfun_update: |
2274 lemma supp_finfun_update: |
2275 shows "supp (finfun_update f x y) \<subseteq> supp(f, x, y)" |
2275 shows "supp (finfun_update f x y) \<subseteq> supp(f, x, y)" |
2276 using fresh_finfun_update |
2276 using fresh_finfun_update |
2277 by (auto simp add: fresh_def supp_Pair) |
2277 by (auto simp: fresh_def supp_Pair) |
2278 |
2278 |
2279 instance finfun :: (fs, fs) fs |
2279 instance finfun :: (fs, fs) fs |
2280 apply(default) |
2280 apply(default) |
2281 apply(induct_tac x rule: finfun_weak_induct) |
2281 apply(induct_tac x rule: finfun_weak_induct) |
2282 apply(simp add: supp_finfun_const finite_supp) |
2282 apply(simp add: supp_finfun_const finite_supp) |
2324 where |
2324 where |
2325 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
2325 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
2326 |
2326 |
2327 lemma fresh_star_supp_conv: |
2327 lemma fresh_star_supp_conv: |
2328 shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x" |
2328 shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x" |
2329 by (auto simp add: fresh_star_def fresh_def) |
2329 by (auto simp: fresh_star_def fresh_def) |
2330 |
2330 |
2331 lemma fresh_star_perm_set_conv: |
2331 lemma fresh_star_perm_set_conv: |
2332 fixes p::"perm" |
2332 fixes p::"perm" |
2333 assumes fresh: "as \<sharp>* p" |
2333 assumes fresh: "as \<sharp>* p" |
2334 and fin: "finite as" |
2334 and fin: "finite as" |
2341 assumes fresh: "as \<sharp>* bs" |
2341 assumes fresh: "as \<sharp>* bs" |
2342 and fin: "finite as" "finite bs" |
2342 and fin: "finite as" "finite bs" |
2343 shows "bs \<sharp>* as" |
2343 shows "bs \<sharp>* as" |
2344 using fresh |
2344 using fresh |
2345 unfolding fresh_star_def fresh_def |
2345 unfolding fresh_star_def fresh_def |
2346 by (auto simp add: supp_finite_atom_set fin) |
2346 by (auto simp: supp_finite_atom_set fin) |
2347 |
2347 |
2348 lemma atom_fresh_star_disjoint: |
2348 lemma atom_fresh_star_disjoint: |
2349 assumes fin: "finite bs" |
2349 assumes fin: "finite bs" |
2350 shows "as \<sharp>* bs \<longleftrightarrow> (as \<inter> bs = {})" |
2350 shows "as \<sharp>* bs \<longleftrightarrow> (as \<inter> bs = {})" |
2351 |
2351 |
2352 unfolding fresh_star_def fresh_def |
2352 unfolding fresh_star_def fresh_def |
2353 by (auto simp add: supp_finite_atom_set fin) |
2353 by (auto simp: supp_finite_atom_set fin) |
2354 |
2354 |
2355 |
2355 |
2356 lemma fresh_star_Pair: |
2356 lemma fresh_star_Pair: |
2357 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
2357 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
2358 by (auto simp add: fresh_star_def fresh_Pair) |
2358 by (auto simp: fresh_star_def fresh_Pair) |
2359 |
2359 |
2360 lemma fresh_star_list: |
2360 lemma fresh_star_list: |
2361 shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys" |
2361 shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys" |
2362 and "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs" |
2362 and "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs" |
2363 and "as \<sharp>* []" |
2363 and "as \<sharp>* []" |
2364 by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append) |
2364 by (auto simp: fresh_star_def fresh_Nil fresh_Cons fresh_append) |
2365 |
2365 |
2366 lemma fresh_star_set: |
2366 lemma fresh_star_set: |
2367 fixes xs::"('a::fs) list" |
2367 fixes xs::"('a::fs) list" |
2368 shows "as \<sharp>* set xs \<longleftrightarrow> as \<sharp>* xs" |
2368 shows "as \<sharp>* set xs \<longleftrightarrow> as \<sharp>* xs" |
2369 unfolding fresh_star_def |
2369 unfolding fresh_star_def |
2379 shows "as \<sharp>* fset S \<longleftrightarrow> as \<sharp>* S" |
2379 shows "as \<sharp>* fset S \<longleftrightarrow> as \<sharp>* S" |
2380 by (simp add: fresh_star_def fresh_def) |
2380 by (simp add: fresh_star_def fresh_def) |
2381 |
2381 |
2382 lemma fresh_star_Un: |
2382 lemma fresh_star_Un: |
2383 shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)" |
2383 shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)" |
2384 by (auto simp add: fresh_star_def) |
2384 by (auto simp: fresh_star_def) |
2385 |
2385 |
2386 lemma fresh_star_insert: |
2386 lemma fresh_star_insert: |
2387 shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)" |
2387 shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)" |
2388 by (auto simp add: fresh_star_def) |
2388 by (auto simp: fresh_star_def) |
2389 |
2389 |
2390 lemma fresh_star_Un_elim: |
2390 lemma fresh_star_Un_elim: |
2391 "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)" |
2391 "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)" |
2392 unfolding fresh_star_def |
2392 unfolding fresh_star_def |
2393 apply(rule) |
2393 apply(rule) |
2438 lemma smaller_supp: |
2438 lemma smaller_supp: |
2439 assumes a: "a \<in> supp p" |
2439 assumes a: "a \<in> supp p" |
2440 shows "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p" |
2440 shows "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p" |
2441 proof - |
2441 proof - |
2442 have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subseteq> supp p" |
2442 have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subseteq> supp p" |
2443 unfolding supp_perm by (auto simp add: swap_atom) |
2443 unfolding supp_perm by (auto simp: swap_atom) |
2444 moreover |
2444 moreover |
2445 have "a \<notin> supp ((p \<bullet> a \<rightleftharpoons> a) + p)" by (simp add: supp_perm) |
2445 have "a \<notin> supp ((p \<bullet> a \<rightleftharpoons> a) + p)" by (simp add: supp_perm) |
2446 then have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<noteq> supp p" using a by auto |
2446 then have "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<noteq> supp p" using a by auto |
2447 ultimately |
2447 ultimately |
2448 show "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p" by auto |
2448 show "supp ((p \<bullet> a \<rightleftharpoons> a) + p) \<subset> supp p" by auto |
2467 } |
2467 } |
2468 moreover |
2468 moreover |
2469 { assume "supp p \<noteq> {}" |
2469 { assume "supp p \<noteq> {}" |
2470 then obtain a where a0: "a \<in> supp p" by blast |
2470 then obtain a where a0: "a \<in> supp p" by blast |
2471 then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" |
2471 then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" |
2472 using as by (auto simp add: supp_atom supp_perm swap_atom) |
2472 using as by (auto simp: supp_atom supp_perm swap_atom) |
2473 let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p" |
2473 let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p" |
2474 have a2: "supp ?q \<subset> supp p" using a0 smaller_supp by simp |
2474 have a2: "supp ?q \<subset> supp p" using a0 smaller_supp by simp |
2475 then have "P ?q" using ih by simp |
2475 then have "P ?q" using ih by simp |
2476 moreover |
2476 moreover |
2477 have "supp ?q \<subseteq> S" using as a2 by simp |
2477 have "supp ?q \<subseteq> S" using as a2 by simp |
2515 proof - |
2515 proof - |
2516 { assume "supp p \<subseteq> {b}" |
2516 { assume "supp p \<subseteq> {b}" |
2517 then have "p = 0" |
2517 then have "p = 0" |
2518 by (induct p rule: perm_struct_induct) (simp_all) |
2518 by (induct p rule: perm_struct_induct) (simp_all) |
2519 } |
2519 } |
2520 then show "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" by (auto simp add: supp_zero_perm) |
2520 then show "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" by (auto simp: supp_zero_perm) |
2521 qed |
2521 qed |
2522 |
2522 |
2523 lemma supp_perm_pair: |
2523 lemma supp_perm_pair: |
2524 fixes p::"perm" |
2524 fixes p::"perm" |
2525 shows "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" |
2525 shows "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" |
2526 proof - |
2526 proof - |
2527 { assume "supp p \<subseteq> {a, b}" |
2527 { assume "supp p \<subseteq> {a, b}" |
2528 then have "p = 0 \<or> p = (b \<rightleftharpoons> a)" |
2528 then have "p = 0 \<or> p = (b \<rightleftharpoons> a)" |
2529 apply (induct p rule: perm_struct_induct) |
2529 apply (induct p rule: perm_struct_induct) |
2530 apply (auto simp add: swap_cancel supp_zero_perm supp_swap) |
2530 apply (auto simp: swap_cancel supp_zero_perm supp_swap) |
2531 apply (simp add: swap_commute) |
2531 apply (simp add: swap_commute) |
2532 done |
2532 done |
2533 } |
2533 } |
2534 then show "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" |
2534 then show "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" |
2535 by (auto simp add: supp_zero_perm supp_swap split: if_splits) |
2535 by (auto simp: supp_zero_perm supp_swap split: if_splits) |
2536 qed |
2536 qed |
2537 |
2537 |
2538 lemma supp_perm_eq: |
2538 lemma supp_perm_eq: |
2539 assumes "(supp x) \<sharp>* p" |
2539 assumes "(supp x) \<sharp>* p" |
2540 shows "p \<bullet> x = x" |
2540 shows "p \<bullet> x = x" |
2677 then obtain y where "y \<notin> (As \<union> p \<bullet> Xs \<union> supp p)" "sort_of y = sort_of x" |
2677 then obtain y where "y \<notin> (As \<union> p \<bullet> Xs \<union> supp p)" "sort_of y = sort_of x" |
2678 by (rule obtain_atom) |
2678 by (rule obtain_atom) |
2679 hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "y \<notin> supp p" "sort_of y = sort_of x" |
2679 hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "y \<notin> supp p" "sort_of y = sort_of x" |
2680 by simp_all |
2680 by simp_all |
2681 hence py: "p \<bullet> y = y" "x \<noteq> y" using `x \<in> As` |
2681 hence py: "p \<bullet> y = y" "x \<noteq> y" using `x \<in> As` |
2682 by (auto simp add: supp_perm) |
2682 by (auto simp: supp_perm) |
2683 let ?q = "(x \<rightleftharpoons> y) + p" |
2683 let ?q = "(x \<rightleftharpoons> y) + p" |
2684 have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)" |
2684 have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)" |
2685 unfolding insert_eqvt |
2685 unfolding insert_eqvt |
2686 using `p \<bullet> x = x` `sort_of y = sort_of x` |
2686 using `p \<bullet> x = x` `sort_of y = sort_of x` |
2687 using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs` |
2687 using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs` |
2726 apply(erule_tac c="(c, x)" in at_set_avoiding) |
2726 apply(erule_tac c="(c, x)" in at_set_avoiding) |
2727 apply(simp add: supp_Pair) |
2727 apply(simp add: supp_Pair) |
2728 apply(rule_tac x="p" in exI) |
2728 apply(rule_tac x="p" in exI) |
2729 apply(simp add: fresh_star_Pair) |
2729 apply(simp add: fresh_star_Pair) |
2730 apply(rule fresh_star_supp_conv) |
2730 apply(rule fresh_star_supp_conv) |
2731 apply(auto simp add: fresh_star_def) |
2731 apply(auto simp: fresh_star_def) |
2732 done |
2732 done |
2733 |
2733 |
2734 lemma at_set_avoiding3: |
2734 lemma at_set_avoiding3: |
2735 assumes "finite xs" |
2735 assumes "finite xs" |
2736 and "finite (supp c)" "finite (supp x)" |
2736 and "finite (supp c)" "finite (supp x)" |
2740 apply(erule_tac c="(c, x)" in at_set_avoiding) |
2740 apply(erule_tac c="(c, x)" in at_set_avoiding) |
2741 apply(simp add: supp_Pair) |
2741 apply(simp add: supp_Pair) |
2742 apply(rule_tac x="p" in exI) |
2742 apply(rule_tac x="p" in exI) |
2743 apply(simp add: fresh_star_Pair) |
2743 apply(simp add: fresh_star_Pair) |
2744 apply(rule fresh_star_supp_conv) |
2744 apply(rule fresh_star_supp_conv) |
2745 apply(auto simp add: fresh_star_def) |
2745 apply(auto simp: fresh_star_def) |
2746 done |
2746 done |
2747 |
2747 |
2748 lemma at_set_avoiding2_atom: |
2748 lemma at_set_avoiding2_atom: |
2749 assumes "finite (supp c)" "finite (supp x)" |
2749 assumes "finite (supp c)" "finite (supp x)" |
2750 and b: "a \<sharp> x" |
2750 and b: "a \<sharp> x" |
2779 by (metis empty_subsetI insert(3) supp_swap) |
2779 by (metis empty_subsetI insert(3) supp_swap) |
2780 { assume 1: "q \<bullet> a = p \<bullet> a" |
2780 { assume 1: "q \<bullet> a = p \<bullet> a" |
2781 have "\<forall>b \<in> (insert a bs). q \<bullet> b = p \<bullet> b" using 1 * by simp |
2781 have "\<forall>b \<in> (insert a bs). q \<bullet> b = p \<bullet> b" using 1 * by simp |
2782 moreover |
2782 moreover |
2783 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2783 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2784 using ** by (auto simp add: insert_eqvt) |
2784 using ** by (auto simp: insert_eqvt) |
2785 ultimately |
2785 ultimately |
2786 have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast |
2786 have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast |
2787 } |
2787 } |
2788 moreover |
2788 moreover |
2789 { assume 2: "q \<bullet> a \<noteq> p \<bullet> a" |
2789 { assume 2: "q \<bullet> a \<noteq> p \<bullet> a" |
2790 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2790 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2791 have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def |
2791 have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def |
2792 by (auto simp add: swap_atom) |
2792 by (auto simp: swap_atom) |
2793 moreover |
2793 moreover |
2794 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2794 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2795 using ** |
2795 using ** |
2796 apply (auto simp add: supp_perm insert_eqvt) |
2796 apply (auto simp: supp_perm insert_eqvt) |
2797 apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs") |
2797 apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs") |
2798 apply(auto)[1] |
2798 apply(auto)[1] |
2799 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2799 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2800 apply(blast) |
2800 apply(blast) |
2801 apply(simp) |
2801 apply(simp) |
2802 done |
2802 done |
2803 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2803 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2804 unfolding supp_swap by auto |
2804 unfolding supp_swap by auto |
2805 moreover |
2805 moreover |
2806 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2806 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2807 using ** by (auto simp add: insert_eqvt) |
2807 using ** by (auto simp: insert_eqvt) |
2808 ultimately |
2808 ultimately |
2809 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2809 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2810 unfolding q'_def using supp_plus_perm by blast |
2810 unfolding q'_def using supp_plus_perm by blast |
2811 } |
2811 } |
2812 ultimately |
2812 ultimately |
2821 proof - |
2821 proof - |
2822 have "finite (bs \<inter> supp p)" by (simp add: finite_supp) |
2822 have "finite (bs \<inter> supp p)" by (simp add: finite_supp) |
2823 then obtain q |
2823 then obtain q |
2824 where *: "\<forall>b \<in> bs \<inter> supp p. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> (bs \<inter> supp p) \<union> (p \<bullet> (bs \<inter> supp p))" |
2824 where *: "\<forall>b \<in> bs \<inter> supp p. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> (bs \<inter> supp p) \<union> (p \<bullet> (bs \<inter> supp p))" |
2825 using set_renaming_perm by blast |
2825 using set_renaming_perm by blast |
2826 from ** have "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by (auto simp add: inter_eqvt) |
2826 from ** have "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by (auto simp: inter_eqvt) |
2827 moreover |
2827 moreover |
2828 have "\<forall>b \<in> bs - supp p. q \<bullet> b = p \<bullet> b" |
2828 have "\<forall>b \<in> bs - supp p. q \<bullet> b = p \<bullet> b" |
2829 apply(auto) |
2829 apply(auto) |
2830 apply(subgoal_tac "b \<notin> supp q") |
2830 apply(subgoal_tac "b \<notin> supp q") |
2831 apply(simp add: fresh_def[symmetric]) |
2831 apply(simp add: fresh_def[symmetric]) |
2848 by (blast) |
2848 by (blast) |
2849 { assume 1: "a \<in> set bs" |
2849 { assume 1: "a \<in> set bs" |
2850 have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto) |
2850 have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto) |
2851 then have "\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b" using * by simp |
2851 then have "\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b" using * by simp |
2852 moreover |
2852 moreover |
2853 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt) |
2853 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp: insert_eqvt) |
2854 ultimately |
2854 ultimately |
2855 have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast |
2855 have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast |
2856 } |
2856 } |
2857 moreover |
2857 moreover |
2858 { assume 2: "a \<notin> set bs" |
2858 { assume 2: "a \<notin> set bs" |
2859 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2859 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2860 have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" |
2860 have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" |
2861 unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp add: swap_atom) |
2861 unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp: swap_atom) |
2862 moreover |
2862 moreover |
2863 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2863 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2864 using ** |
2864 using ** |
2865 apply (auto simp add: supp_perm insert_eqvt) |
2865 apply (auto simp: supp_perm insert_eqvt) |
2866 apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs") |
2866 apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs") |
2867 apply(auto)[1] |
2867 apply(auto)[1] |
2868 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2868 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2869 apply(blast) |
2869 apply(blast) |
2870 apply(simp) |
2870 apply(simp) |
2871 done |
2871 done |
2872 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" |
2872 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" |
2873 unfolding supp_swap by auto |
2873 unfolding supp_swap by auto |
2874 moreover |
2874 moreover |
2875 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2875 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2876 using ** by (auto simp add: insert_eqvt) |
2876 using ** by (auto simp: insert_eqvt) |
2877 ultimately |
2877 ultimately |
2878 have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2878 have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2879 unfolding q'_def using supp_plus_perm by blast |
2879 unfolding q'_def using supp_plus_perm by blast |
2880 } |
2880 } |
2881 ultimately |
2881 ultimately |
2948 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2948 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
2949 by (simp_all add: fresh_at_base) |
2949 by (simp_all add: fresh_at_base) |
2950 |
2950 |
2951 |
2951 |
2952 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2952 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ctxt => fn ctrm => |
2953 let |
2953 case term_of ctrm of @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => |
2954 fun first_is_neg lhs rhs [] = NONE |
2954 let |
2955 | first_is_neg lhs rhs (thm::thms) = |
2955 |
|
2956 fun first_is_neg lhs rhs [] = NONE |
|
2957 | first_is_neg lhs rhs (thm::thms) = |
2956 (case Thm.prop_of thm of |
2958 (case Thm.prop_of thm of |
2957 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2959 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2958 (if l = lhs andalso r = rhs then SOME(thm) |
2960 (if l = lhs andalso r = rhs then SOME(thm) |
2959 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2961 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2960 else first_is_neg lhs rhs thms) |
2962 else first_is_neg lhs rhs thms) |
2961 | _ => first_is_neg lhs rhs thms) |
2963 | _ => first_is_neg lhs rhs thms) |
2962 |
2964 |
2963 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2965 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2964 val prems = Simplifier.prems_of ctxt |
2966 val prems = Simplifier.prems_of ctxt |
2965 |> filter (fn thm => case Thm.prop_of thm of |
2967 |> filter (fn thm => case Thm.prop_of thm of |
2966 _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false) |
2968 _ $ (Const (@{const_name fresh}, ty) $ (_ $ a) $ b) => |
2967 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |
2969 (let |
2968 |> map HOLogic.conj_elims |
2970 val atms = a :: HOLogic.strip_tuple b |
2969 |> flat |
2971 in |
2970 in |
2972 member (op=) atms lhs andalso member (op=) atms rhs |
2971 case term_of ctrm of |
2973 end) |
2972 @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => |
2974 | _ => false) |
2973 (case first_is_neg lhs rhs prems of |
2975 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |
2974 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
2976 |> map HOLogic.conj_elims |
2975 | NONE => NONE) |
2977 |> flat |
2976 | _ => NONE |
2978 |
2977 end |
2979 |
|
2980 in |
|
2981 case first_is_neg lhs rhs prems of |
|
2982 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
|
2983 | NONE => NONE |
|
2984 end |
|
2985 | _ => NONE |
2978 *} |
2986 *} |
2979 |
2987 |
2980 |
2988 |
2981 instance at_base < fs |
2989 instance at_base < fs |
2982 proof qed (simp add: supp_at_base) |
2990 proof qed (simp add: supp_at_base) |
3023 |
3031 |
3024 lemma obtain_fresh': |
3032 lemma obtain_fresh': |
3025 assumes fin: "finite (supp x)" |
3033 assumes fin: "finite (supp x)" |
3026 obtains a::"'a::at_base" where "atom a \<sharp> x" |
3034 obtains a::"'a::at_base" where "atom a \<sharp> x" |
3027 using obtain_at_base[where X="supp x"] |
3035 using obtain_at_base[where X="supp x"] |
3028 by (auto simp add: fresh_def fin) |
3036 by (auto simp: fresh_def fin) |
3029 |
3037 |
3030 lemma obtain_fresh: |
3038 lemma obtain_fresh: |
3031 fixes x::"'b::fs" |
3039 fixes x::"'b::fs" |
3032 obtains a::"'a::at_base" where "atom a \<sharp> x" |
3040 obtains a::"'a::at_base" where "atom a \<sharp> x" |
3033 by (rule obtain_fresh') (auto simp add: finite_supp) |
3041 by (rule obtain_fresh') (auto simp: finite_supp) |
3034 |
3042 |
3035 lemma supp_finite_set_at_base: |
3043 lemma supp_finite_set_at_base: |
3036 assumes a: "finite S" |
3044 assumes a: "finite S" |
3037 shows "supp S = atom ` S" |
3045 shows "supp S = atom ` S" |
3038 apply(simp add: supp_of_finite_sets[OF a]) |
3046 apply(simp add: supp_of_finite_sets[OF a]) |
3264 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3272 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3265 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3273 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3266 shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3274 shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3267 proof - |
3275 proof - |
3268 from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b" |
3276 from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b" |
3269 by (auto simp add: fresh_Pair) |
3277 by (auto simp: fresh_Pair) |
3270 show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3278 show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3271 proof (intro exI allI impI) |
3279 proof (intro exI allI impI) |
3272 fix a :: 'a |
3280 fix a :: 'a |
3273 assume a3: "atom a \<sharp> h" |
3281 assume a3: "atom a \<sharp> h" |
3274 show "h a = h b" |
3282 show "h a = h b" |
3304 next |
3312 next |
3305 fix x y |
3313 fix x y |
3306 assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3314 assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3307 assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y" |
3315 assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y" |
3308 from a x y show "x = y" |
3316 from a x y show "x = y" |
3309 by (auto simp add: fresh_Pair) |
3317 by (auto simp: fresh_Pair) |
3310 qed |
3318 qed |
3311 |
3319 |
3312 text {* packaging the freshness lemma into a function *} |
3320 text {* packaging the freshness lemma into a function *} |
3313 |
3321 |
3314 definition |
3322 definition |
3339 lemma Fresh_apply': |
3347 lemma Fresh_apply': |
3340 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3348 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3341 assumes a: "atom a \<sharp> h" "atom a \<sharp> h a" |
3349 assumes a: "atom a \<sharp> h" "atom a \<sharp> h a" |
3342 shows "Fresh h = h a" |
3350 shows "Fresh h = h a" |
3343 apply (rule Fresh_apply) |
3351 apply (rule Fresh_apply) |
3344 apply (auto simp add: fresh_Pair intro: a) |
3352 apply (auto simp: fresh_Pair intro: a) |
3345 done |
3353 done |
3346 |
3354 |
3347 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
3355 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ctxt => fn ctrm => |
3348 let |
3356 let |
3349 val _ $ h = term_of ctrm |
3357 val _ $ h = term_of ctrm |