equal
deleted
inserted
replaced
34 |
34 |
35 lemma valid_perm_distinct_snd: "valid_perm a \<Longrightarrow> distinct (map snd a)" |
35 lemma valid_perm_distinct_snd: "valid_perm a \<Longrightarrow> distinct (map snd a)" |
36 by (metis valid_perm_def image_set length_map len_set_eq_distinct) |
36 by (metis valid_perm_def image_set length_map len_set_eq_distinct) |
37 |
37 |
38 definition |
38 definition |
39 perm_eq :: "('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> bool" (infix "\<approx>" 50) |
39 perm_eq :: "('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> bool" |
40 where |
40 where |
41 "x \<approx> y \<longleftrightarrow> valid_perm x \<and> valid_perm y \<and> (perm_apply x = perm_apply y)" |
41 "perm_eq x y \<longleftrightarrow> valid_perm x \<and> valid_perm y \<and> (perm_apply x = perm_apply y)" |
42 |
42 |
43 lemma perm_eq_sym[sym]: |
43 lemma perm_eq_sym[sym]: |
44 "x \<approx> y \<Longrightarrow> y \<approx> x" |
44 "perm_eq x y \<Longrightarrow> perm_eq y x" |
45 by (auto simp add: perm_eq_def) |
45 by (auto simp add: perm_eq_def) |
46 |
46 |
47 lemma perm_eq_equivp: |
47 lemma perm_eq_equivp: |
48 "part_equivp perm_eq" |
48 "part_equivp perm_eq" |
49 by (auto intro!: part_equivpI sympI transpI exI[of _ "[]"] simp add: perm_eq_def) |
49 by (auto intro!: part_equivpI sympI transpI exI[of _ "[]"] simp add: perm_eq_def) |
157 lemma perm_apply_minus: "valid_perm x \<Longrightarrow> perm_apply (map swap_pair x) a = b \<longleftrightarrow> perm_apply x b = a" |
157 lemma perm_apply_minus: "valid_perm x \<Longrightarrow> perm_apply (map swap_pair x) a = b \<longleftrightarrow> perm_apply x b = a" |
158 using valid_perm_add_minus[symmetric] valid_perm_minus |
158 using valid_perm_add_minus[symmetric] valid_perm_minus |
159 by (metis uminus_perm_raw_def) |
159 by (metis uminus_perm_raw_def) |
160 |
160 |
161 lemma uminus_perm_raw_rsp[simp]: |
161 lemma uminus_perm_raw_rsp[simp]: |
162 "x \<approx> y \<Longrightarrow> map swap_pair x \<approx> map swap_pair y" |
162 "perm_eq x y \<Longrightarrow> perm_eq (map swap_pair x) (map swap_pair y)" |
163 by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def) |
163 by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def) |
164 |
164 |
165 lemma fst_snd_map_pair[simp]: |
165 lemma fst_snd_map_pair[simp]: |
166 "fst ` map_pair f g ` set l = f ` fst ` set l" |
166 "fst ` map_pair f g ` set l = f ` fst ` set l" |
167 "snd ` map_pair f g ` set l = g ` snd ` set l" |
167 "snd ` map_pair f g ` set l = g ` snd ` set l" |
231 apply (simp add: image_Un[symmetric]) |
231 apply (simp add: image_Un[symmetric]) |
232 apply (auto simp add: perm_apply_subset valid_perm_def) |
232 apply (auto simp add: perm_apply_subset valid_perm_def) |
233 done |
233 done |
234 |
234 |
235 lemma perm_add_raw_rsp[simp]: |
235 lemma perm_add_raw_rsp[simp]: |
236 "x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> perm_add_raw x xa \<approx> perm_add_raw y ya" |
236 "perm_eq x y \<Longrightarrow> perm_eq xa ya \<Longrightarrow> perm_eq (perm_add_raw x xa) (perm_add_raw y ya)" |
237 by (simp add: fun_eq_iff perm_add_apply perm_eq_def) |
237 by (simp add: fun_eq_iff perm_add_apply perm_eq_def) |
238 |
238 |
239 lemma [simp]: |
239 lemma [simp]: |
240 "a \<approx> a \<longleftrightarrow> valid_perm a" |
240 "perm_eq a a \<longleftrightarrow> valid_perm a" |
241 by (simp_all add: perm_eq_def) |
241 by (simp_all add: perm_eq_def) |
242 |
242 |
243 instantiation gperm :: (type) group_add |
243 instantiation gperm :: (type) group_add |
244 begin |
244 begin |
245 |
245 |
274 lemma perm_apply_in_set: |
274 lemma perm_apply_in_set: |
275 "a \<noteq> b \<Longrightarrow> perm_apply y a = b \<Longrightarrow> (a, b) \<in> set y" |
275 "a \<noteq> b \<Longrightarrow> perm_apply y a = b \<Longrightarrow> (a, b) \<in> set y" |
276 by (induct y) (auto split: if_splits) |
276 by (induct y) (auto split: if_splits) |
277 |
277 |
278 lemma perm_eq_not_eq_same: |
278 lemma perm_eq_not_eq_same: |
279 "x \<approx> y \<Longrightarrow> {xa \<in> set x. fst xa \<noteq> snd xa} = {x \<in> set y. fst x \<noteq> snd x}" |
279 "perm_eq x y \<Longrightarrow> {xa \<in> set x. fst xa \<noteq> snd xa} = {x \<in> set y. fst x \<noteq> snd x}" |
280 unfolding perm_eq_def set_eq_iff |
280 unfolding perm_eq_def set_eq_iff |
281 apply auto |
281 apply auto |
282 apply (subgoal_tac "perm_apply x a = b") |
282 apply (subgoal_tac "perm_apply x a = b") |
283 apply (simp add: perm_apply_in_set) |
283 apply (simp add: perm_apply_in_set) |
284 apply (erule valid_perm_apply) |
284 apply (erule valid_perm_apply) |
313 lemma in_set_in_dpr3: |
313 lemma in_set_in_dpr3: |
314 "(dest_perm_raw x = dest_perm_raw y) \<Longrightarrow> valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> perm_apply x a = perm_apply y a" |
314 "(dest_perm_raw x = dest_perm_raw y) \<Longrightarrow> valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> perm_apply x a = perm_apply y a" |
315 by (metis in_set_in_dpr2 pair_perm_apply perm_apply_in_set valid_perm_def) |
315 by (metis in_set_in_dpr2 pair_perm_apply perm_apply_in_set valid_perm_def) |
316 |
316 |
317 lemma dest_perm_raw_eq[simp]: |
317 lemma dest_perm_raw_eq[simp]: |
318 "valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) = (x \<approx> y)" |
318 "valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) = perm_eq x y" |
319 apply (auto simp add: perm_eq_def) |
319 apply (auto simp add: perm_eq_def) |
320 apply (metis in_set_in_dpr3 fun_eq_iff) |
320 apply (metis in_set_in_dpr3 fun_eq_iff) |
321 unfolding dest_perm_raw_def |
321 unfolding dest_perm_raw_def |
322 by (rule sorted_distinct_set_unique) |
322 by (rule sorted_distinct_set_unique) |
323 (simp_all add: distinct_filter valid_perm_def perm_eq_not_eq_same[simplified perm_eq_def, simplified]) |
323 (simp_all add: distinct_filter valid_perm_def perm_eq_not_eq_same[simplified perm_eq_def, simplified]) |
369 "dest_perm_raw (dest_perm_raw p) = dest_perm_raw p" |
369 "dest_perm_raw (dest_perm_raw p) = dest_perm_raw p" |
370 unfolding dest_perm_raw_def |
370 unfolding dest_perm_raw_def |
371 by simp (rule sorted_sort_id[OF sorted_sort]) |
371 by simp (rule sorted_sort_id[OF sorted_sort]) |
372 |
372 |
373 lemma valid_dest_perm_raw_eq[simp]: |
373 lemma valid_dest_perm_raw_eq[simp]: |
374 "valid_perm p \<Longrightarrow> dest_perm_raw p \<approx> p" |
374 "valid_perm p \<Longrightarrow> perm_eq (dest_perm_raw p) p" |
375 "valid_perm p \<Longrightarrow> p \<approx> dest_perm_raw p" |
375 "valid_perm p \<Longrightarrow> perm_eq p (dest_perm_raw p)" |
376 by (simp_all add: dest_perm_raw_eq[symmetric]) |
376 by (simp_all add: dest_perm_raw_eq[symmetric]) |
377 |
377 |
378 lemma mk_perm_dest_perm[code abstype]: |
378 lemma mk_perm_dest_perm[code abstype]: |
379 "mk_perm (dest_perm p) = p" |
379 "mk_perm (dest_perm p) = p" |
380 by transfer |
380 by transfer |