2575 fixes a::"'a::at_base" |
2575 fixes a::"'a::at_base" |
2576 shows "supp a = {atom a}" |
2576 shows "supp a = {atom a}" |
2577 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
2577 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
2578 |
2578 |
2579 lemma fresh_at_base: |
2579 lemma fresh_at_base: |
2580 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b" |
2580 shows "sort_of a \<noteq> sort_of (atom b) \<Longrightarrow> a \<sharp> b" |
2581 unfolding fresh_def by (simp add: supp_at_base) |
2581 and "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b" |
2582 |
2582 unfolding fresh_def |
|
2583 apply(simp_all add: supp_at_base) |
|
2584 apply(metis) |
|
2585 done |
|
2586 |
2583 lemma fresh_atom_at_base: |
2587 lemma fresh_atom_at_base: |
2584 fixes b::"'a::at_base" |
2588 fixes b::"'a::at_base" |
2585 shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b" |
2589 shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b" |
2586 by (simp add: fresh_def supp_at_base supp_atom) |
2590 by (simp add: fresh_def supp_at_base supp_atom) |
2587 |
2591 |
2681 |
2685 |
2682 definition |
2686 definition |
2683 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
2687 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
2684 where |
2688 where |
2685 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
2689 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
2686 |
|
2687 |
2690 |
2688 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0" |
2691 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0" |
2689 unfolding flip_def by (rule swap_self) |
2692 unfolding flip_def by (rule swap_self) |
2690 |
2693 |
2691 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)" |
2694 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)" |
2839 unfolding atom_def by (simp add: Rep_inject) |
2842 unfolding atom_def by (simp add: Rep_inject) |
2840 show "p \<bullet> atom a = atom (p \<bullet> a)" |
2843 show "p \<bullet> atom a = atom (p \<bullet> a)" |
2841 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
2844 unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) |
2842 qed |
2845 qed |
2843 |
2846 |
|
2847 lemma at_class_sort: |
|
2848 fixes s :: atom_sort |
|
2849 fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a" |
|
2850 fixes a::"'a" |
|
2851 assumes type: "type_definition Rep Abs {a. sort_of a = s}" |
|
2852 assumes atom_def: "\<And>a. atom a = Rep a" |
|
2853 shows "sort_of (atom a) = s" |
|
2854 using atom_def type |
|
2855 unfolding type_definition_def by simp |
|
2856 |
|
2857 |
2844 setup {* Sign.add_const_constraint |
2858 setup {* Sign.add_const_constraint |
2845 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
2859 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
2846 setup {* Sign.add_const_constraint |
2860 setup {* Sign.add_const_constraint |
2847 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
2861 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
2848 |
|
2849 |
|
2850 |
2862 |
2851 section {* The freshness lemma according to Andy Pitts *} |
2863 section {* The freshness lemma according to Andy Pitts *} |
2852 |
2864 |
2853 lemma freshness_lemma: |
2865 lemma freshness_lemma: |
2854 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
2866 fixes h :: "'a::at \<Rightarrow> 'b::pt" |