93 by (simp add: sort_respecting_def) |
99 by (simp add: sort_respecting_def) |
94 |
100 |
95 typedef (open) perm = "{p::atom gperm. sort_respecting p}" |
101 typedef (open) perm = "{p::atom gperm. sort_respecting p}" |
96 by (auto intro: exI[of _ "0"]) |
102 by (auto intro: exI[of _ "0"]) |
97 |
103 |
|
104 setup_lifting type_definition_perm |
|
105 |
98 lemma perm_eq_rep: |
106 lemma perm_eq_rep: |
99 "p = q \<longleftrightarrow> Rep_perm p = Rep_perm q" |
107 "p = q \<longleftrightarrow> Rep_perm p = Rep_perm q" |
100 by (simp add: Rep_perm_inject) |
108 by (simp add: Rep_perm_inject) |
101 |
109 |
102 definition mk_perm :: "atom gperm \<Rightarrow> perm" where |
110 lift_definition mk_perm :: "atom gperm \<Rightarrow> perm" is |
103 "mk_perm p = Abs_perm (if sort_respecting p then p else 0)" |
111 "\<lambda>p. if sort_respecting p then p else 0" by simp |
104 |
112 |
105 lemma sort_respecting_Rep_perm [simp, intro]: |
113 (*lemma sort_respecting_Rep_perm [simp, intro]: |
106 "sort_respecting (Rep_perm p)" |
114 "sort_respecting (Rep_perm p)" |
107 using Rep_perm [of p] by simp |
115 using Rep_perm [of p] by simp*) |
108 |
116 |
109 lemma Rep_perm_mk_perm [simp]: |
117 lemma Rep_perm_mk_perm [simp]: |
110 "Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)" |
118 "Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)" |
111 by (simp add: mk_perm_def Abs_perm_inverse) |
119 by (simp add: mk_perm_def Abs_perm_inverse) |
112 |
120 |
113 lemma mk_perm_Rep_perm [simp, code abstype]: |
121 (*lemma mk_perm_Rep_perm [simp, code abstype]: |
114 "mk_perm (Rep_perm dxs) = dxs" |
122 "mk_perm (Rep_perm dxs) = dxs" |
115 by (simp add: mk_perm_def Rep_perm_inverse) |
123 by (simp add: mk_perm_def Rep_perm_inverse)*) |
116 |
124 |
117 instance perm :: size .. |
125 instance perm :: size .. |
118 |
126 |
119 instantiation perm :: group_add |
127 instantiation perm :: group_add |
120 begin |
128 begin |
121 |
129 |
122 definition "(0 :: perm) = mk_perm 0" |
130 lift_definition zero_perm :: "perm" is "0" by simp |
123 |
131 |
124 definition "uminus p = mk_perm (uminus (Rep_perm p))" |
132 lift_definition uminus_perm :: "perm \<Rightarrow> perm" is "uminus" |
125 |
133 unfolding sort_respecting_def |
126 definition "p + q = mk_perm ((Rep_perm p) + (Rep_perm q))" |
134 by transfer (auto, metis perm_apply_minus) |
|
135 |
|
136 lift_definition plus_perm :: "perm \<Rightarrow> perm \<Rightarrow> perm" is "plus" |
|
137 unfolding sort_respecting_def |
|
138 by transfer (simp add: perm_add_apply) |
127 |
139 |
128 definition "(p :: perm) - q = p + - q" |
140 definition "(p :: perm) - q = p + - q" |
129 |
|
130 lemma [simp]: |
|
131 "sort_respecting x \<Longrightarrow> sort_respecting y \<Longrightarrow> sort_respecting (x + y)" |
|
132 unfolding sort_respecting_def |
|
133 by descending (simp add: perm_add_apply) |
|
134 |
|
135 lemma [simp]: |
|
136 "sort_respecting y \<Longrightarrow> sort_respecting (- y)" |
|
137 unfolding sort_respecting_def |
|
138 by partiality_descending |
|
139 (auto, metis perm_apply_minus) |
|
140 |
141 |
141 lemma Rep_perm_0 [simp, code abstract]: |
142 lemma Rep_perm_0 [simp, code abstract]: |
142 "Rep_perm 0 = 0" |
143 "Rep_perm 0 = 0" |
143 by (simp add: zero_perm_def) |
144 by (metis (mono_tags) zero_perm.rep_eq) |
144 |
145 |
145 lemma Rep_perm_uminus [simp, code abstract]: |
146 lemma Rep_perm_uminus [simp, code abstract]: |
146 "Rep_perm (- p) = - (Rep_perm p)" |
147 "Rep_perm (- p) = - (Rep_perm p)" |
147 by (simp add: uminus_perm_def) |
148 by (metis uminus_perm.rep_eq) |
148 |
149 |
149 lemma Rep_perm_add [simp, code abstract]: |
150 lemma Rep_perm_add [simp, code abstract]: |
150 "Rep_perm (p + q) = (Rep_perm p) + (Rep_perm q)" |
151 "Rep_perm (p + q) = (Rep_perm p) + (Rep_perm q)" |
151 by (simp add: plus_perm_def) |
152 by (simp add: plus_perm.rep_eq) |
152 |
153 |
153 instance |
154 instance |
154 by default (auto simp add: perm_eq_rep add_assoc minus_perm_def) |
155 apply default |
|
156 unfolding minus_perm_def |
|
157 by (transfer, simp add: add_assoc)+ |
155 |
158 |
156 end |
159 end |
157 |
160 |
158 definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm" ("'(_ \<rightleftharpoons> _')") |
161 lift_definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm" ("'(_ \<rightleftharpoons> _')") |
159 where "swap a b = (if sort_of a = sort_of b then mk_perm (gswap a b) else 0)" |
162 is "(\<lambda>a b. (if sort_of a = sort_of b then mk_perm (gswap a b) else 0))" . |
160 |
163 |
161 lemma sort_respecting_swap [simp]: |
164 lemma sort_respecting_swap [simp]: |
162 "sort_of a = sort_of b \<Longrightarrow> sort_respecting (gswap a b)" |
165 "sort_of a = sort_of b \<Longrightarrow> sort_respecting (gswap a b)" |
163 unfolding sort_respecting_def |
166 unfolding sort_respecting_def |
164 by descending auto |
167 by transfer auto |
165 |
168 |
166 lemma Rep_swap [simp, code abstract]: |
169 lemma Rep_swap [simp, code abstract]: |
167 "Rep_perm (swap a b) = (if sort_of a = sort_of b then gswap a b else 0)" |
170 "Rep_perm (swap a b) = (if sort_of a = sort_of b then gswap a b else 0)" |
168 by (simp add: swap_def) |
171 by (simp add: swap_def) |
169 |
172 |
540 by (simp_all) |
543 by (simp_all) |
541 |
544 |
542 |
545 |
543 subsection {* Permutations for @{typ "'a fset"} *} |
546 subsection {* Permutations for @{typ "'a fset"} *} |
544 |
547 |
545 lemma permute_fset_rsp[quot_respect]: |
|
546 shows "(op = ===> list_eq ===> list_eq) permute permute" |
|
547 unfolding fun_rel_def |
|
548 by (simp add: set_eqvt[symmetric]) |
|
549 |
|
550 instantiation fset :: (pt) pt |
548 instantiation fset :: (pt) pt |
551 begin |
549 begin |
552 |
550 |
553 quotient_definition |
551 quotient_definition |
554 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
552 "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
555 is |
553 is |
556 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
554 "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list" |
557 |
555 by (simp add: set_eqvt[symmetric]) |
558 instance |
556 |
|
557 instance |
559 proof |
558 proof |
560 fix x :: "'a fset" and p q :: "perm" |
559 fix x :: "'a fset" and p q :: "perm" |
561 have lst: "\<And>l :: 'a list. 0 \<bullet> l = l" by simp |
560 have lst: "\<And>l :: 'a list. 0 \<bullet> l = l" by simp |
562 show "0 \<bullet> x = x" by (lifting lst) |
561 show "0 \<bullet> x = x" by (lifting lst) |
563 have lst: "\<And>p q :: perm. \<And>x :: 'a list. (p + q) \<bullet> x = p \<bullet> q \<bullet> x" by simp |
562 have lst: "\<And>p q :: perm. \<And>x :: 'a list. (p + q) \<bullet> x = p \<bullet> q \<bullet> x" by simp |
3165 |
3164 |
3166 section {* automatic equivariance procedure for inductive definitions *} |
3165 section {* automatic equivariance procedure for inductive definitions *} |
3167 |
3166 |
3168 use "nominal_eqvt.ML" |
3167 use "nominal_eqvt.ML" |
3169 |
3168 |
3170 |
3169 instantiation atom_sort :: ord begin |
3171 |
3170 |
|
3171 fun less_atom_sort where |
|
3172 "less_atom_sort (Sort s1 l1) (Sort s2 []) \<longleftrightarrow> s1 < s2" |
|
3173 | "less_atom_sort (Sort s1 []) (Sort s2 (h # t)) \<longleftrightarrow> s1 \<le> s2" |
|
3174 | "less_atom_sort (Sort s1 (h1 # t1)) (Sort s2 (h2 # t2)) \<longleftrightarrow> s1 < s2 \<or> s1 \<le> s2 \<and> ((less_atom_sort h1 h2) \<or> (h1 = h2 \<and> less_atom_sort (Sort s1 t1) (Sort s2 t2)))" |
|
3175 |
|
3176 definition less_eq_atom_sort where |
|
3177 less_eq_atom_sort_def: "less_eq_atom_sort (x :: atom_sort) y \<longleftrightarrow> x < y \<or> x = y" |
|
3178 |
|
3179 instance .. |
3172 |
3180 |
3173 end |
3181 end |
|
3182 |
|
3183 lemma less_st_less: "(Sort s1 l1) < (Sort s2 l2) \<longleftrightarrow> s1 < s2 \<or> s1 \<le> s2 \<and> l1 < l2" |
|
3184 by (induct l1 l2 rule: list_induct2') auto |
|
3185 |
|
3186 lemma not_as_le_as: "\<not>((x :: atom_sort) < x)" |
|
3187 apply (rule less_atom_sort.induct[of "\<lambda>x y. x = y \<longrightarrow> \<not>x < y" "x" "x", simplified]) .. |
|
3188 |
|
3189 instance atom_sort :: linorder |
|
3190 proof (default, auto simp add: less_eq_atom_sort_def not_as_le_as) |
|
3191 fix x y :: atom_sort |
|
3192 assume x: "x < y" "y < x" |
|
3193 then show False |
|
3194 by (induct x y rule: less_atom_sort.induct) (case_tac l1, auto) |
|
3195 with x show "x = y" |
|
3196 by (induct x y rule: less_atom_sort.induct) (case_tac l1, auto) |
|
3197 next |
|
3198 fix x y z :: atom_sort |
|
3199 assume "x < y" "y < z" |
|
3200 then show "x < z" |
|
3201 apply (induct x z arbitrary: y rule: less_atom_sort.induct) |
|
3202 apply (case_tac [!] y) apply auto |
|
3203 apply (case_tac [!] list2) apply auto |
|
3204 apply (case_tac l1) apply auto[2] |
|
3205 done |
|
3206 next |
|
3207 fix x y :: atom_sort |
|
3208 assume x: "\<not>x < y" "y \<noteq> x" |
|
3209 then show "y < x" |
|
3210 apply (induct x y rule: less_atom_sort.induct) |
|
3211 apply auto |
|
3212 apply (case_tac [!] l1) |
|
3213 apply auto |
|
3214 done |
|
3215 qed |
|
3216 |
|
3217 instantiation atom :: linorder begin |
|
3218 |
|
3219 definition less_eq_atom where |
|
3220 [simp]: "less_eq_atom x y \<longleftrightarrow> sort_of x < sort_of y \<or> sort_of x \<le> sort_of y \<and> nat_of x \<le> nat_of y" |
|
3221 |
|
3222 definition less_atom where |
|
3223 [simp]: "less_atom x y \<longleftrightarrow> sort_of x < sort_of y \<or> sort_of x \<le> sort_of y \<and> nat_of x < nat_of y" |
|
3224 |
|
3225 instance apply default |
|
3226 apply auto |
|
3227 apply (case_tac x, case_tac y) |
|
3228 apply auto |
|
3229 done |
|
3230 |
|
3231 end |
|
3232 |
|
3233 lemma [code]: |
|
3234 "gpermute p = perm_apply (dest_perm p)" |
|
3235 apply transfer |
|
3236 unfolding Rel_def |
|
3237 by (auto, metis perm_eq_def valid_dest_perm_raw_eq(2)) |
|
3238 |
|
3239 instantiation perm :: equal begin |
|
3240 |
|
3241 definition "equal_perm a b \<longleftrightarrow> Rep_perm a = Rep_perm b" |
|
3242 |
|
3243 instance |
|
3244 apply default |
|
3245 unfolding equal_perm_def perm_eq_rep .. |
|
3246 |
|
3247 end |
|
3248 |
|
3249 (* Test: export_code swap in SML *) |
|
3250 |
|
3251 end |