108 by (simp add: Rep_perm_inject) |
108 by (simp add: Rep_perm_inject) |
109 |
109 |
110 lift_definition mk_perm :: "atom gperm \<Rightarrow> perm" is |
110 lift_definition mk_perm :: "atom gperm \<Rightarrow> perm" is |
111 "\<lambda>p. if sort_respecting p then p else 0" by simp |
111 "\<lambda>p. if sort_respecting p then p else 0" by simp |
112 |
112 |
113 (*lemma sort_respecting_Rep_perm [simp, intro]: |
|
114 "sort_respecting (Rep_perm p)" |
|
115 using Rep_perm [of p] by simp*) |
|
116 |
|
117 lemma Rep_perm_mk_perm [simp]: |
113 lemma Rep_perm_mk_perm [simp]: |
118 "Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)" |
114 "Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)" |
119 by (simp add: mk_perm_def Abs_perm_inverse) |
115 by (simp add: mk_perm_def Abs_perm_inverse) |
120 |
116 |
121 (*lemma mk_perm_Rep_perm [simp, code abstype]: |
|
122 "mk_perm (Rep_perm dxs) = dxs" |
|
123 by (simp add: mk_perm_def Rep_perm_inverse)*) |
|
124 |
|
125 instance perm :: size .. |
117 instance perm :: size .. |
|
118 |
|
119 |
|
120 subsection {* Permutations form a (multiplicative) group *} |
126 |
121 |
127 instantiation perm :: group_add |
122 instantiation perm :: group_add |
128 begin |
123 begin |
129 |
124 |
130 lift_definition zero_perm :: "perm" is "0" by simp |
125 lift_definition zero_perm :: "perm" is "0" by simp |
155 apply default |
150 apply default |
156 unfolding minus_perm_def |
151 unfolding minus_perm_def |
157 by (transfer, simp add: add_assoc)+ |
152 by (transfer, simp add: add_assoc)+ |
158 |
153 |
159 end |
154 end |
|
155 |
|
156 |
|
157 section {* Implementation of swappings *} |
160 |
158 |
161 lift_definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm" ("'(_ \<rightleftharpoons> _')") |
159 lift_definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm" ("'(_ \<rightleftharpoons> _')") |
162 is "(\<lambda>a b. (if sort_of a = sort_of b then mk_perm (gswap a b) else 0))" . |
160 is "(\<lambda>a b. (if sort_of a = sort_of b then mk_perm (gswap a b) else 0))" . |
163 |
161 |
164 lemma sort_respecting_swap [simp]: |
162 lemma sort_respecting_swap [simp]: |
1011 lemma finite_eqvt [eqvt]: |
1009 lemma finite_eqvt [eqvt]: |
1012 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1010 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1013 unfolding finite_def |
1011 unfolding finite_def |
1014 by (perm_simp) (rule refl) |
1012 by (perm_simp) (rule refl) |
1015 |
1013 |
|
1014 lemma Let_eqvt [eqvt]: |
|
1015 "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)" |
|
1016 unfolding Let_def permute_fun_app_eq .. |
1016 |
1017 |
1017 subsubsection {* Equivariance for product operations *} |
1018 subsubsection {* Equivariance for product operations *} |
1018 |
1019 |
1019 lemma fst_eqvt [eqvt]: |
1020 lemma fst_eqvt [eqvt]: |
1020 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |
1021 shows "p \<bullet> (fst x) = fst (p \<bullet> x)" |
2719 lemma fresh_star_atom_at_base: |
2720 lemma fresh_star_atom_at_base: |
2720 fixes b::"'a::at_base" |
2721 fixes b::"'a::at_base" |
2721 shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b" |
2722 shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b" |
2722 by (simp add: fresh_star_def fresh_atom_at_base) |
2723 by (simp add: fresh_star_def fresh_atom_at_base) |
2723 |
2724 |
|
2725 lemma if_fresh_at_base [simp]: |
|
2726 shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s" |
|
2727 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
|
2728 by (simp_all add: fresh_at_base) |
|
2729 |
|
2730 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm => |
|
2731 let |
|
2732 fun first_is_neg lhs rhs [] = NONE |
|
2733 | first_is_neg lhs rhs (thm::thms) = |
|
2734 (case Thm.prop_of thm of |
|
2735 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
|
2736 (if l = lhs andalso r = rhs then SOME(thm) |
|
2737 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
|
2738 else NONE) |
|
2739 | _ => first_is_neg lhs rhs thms) |
|
2740 |
|
2741 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
|
2742 val prems = Simplifier.prems_of ss |
|
2743 |> filter (fn thm => case Thm.prop_of thm of |
|
2744 _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false) |
|
2745 |> map (simplify (HOL_basic_ss addsimps simp_thms)) |
|
2746 |> map HOLogic.conj_elims |
|
2747 |> flat |
|
2748 in |
|
2749 case term_of ctrm of |
|
2750 @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => |
|
2751 (case first_is_neg lhs rhs prems of |
|
2752 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
|
2753 | NONE => NONE) |
|
2754 | _ => NONE |
|
2755 end |
|
2756 *} |
|
2757 |
|
2758 |
2724 instance at_base < fs |
2759 instance at_base < fs |
2725 proof qed (simp add: supp_at_base) |
2760 proof qed (simp add: supp_at_base) |
2726 |
2761 |
2727 lemma at_base_infinite [simp]: |
2762 lemma at_base_infinite [simp]: |
2728 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |
2763 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |