equal
deleted
inserted
replaced
51 quotient_type |
51 quotient_type |
52 'a gperm = "('a \<times> 'a) list" / partial: "perm_eq" |
52 'a gperm = "('a \<times> 'a) list" / partial: "perm_eq" |
53 by (rule perm_eq_equivp) |
53 by (rule perm_eq_equivp) |
54 |
54 |
55 definition perm_add_raw where |
55 definition perm_add_raw where |
56 "perm_add_raw p q = map (map_pair id (perm_apply p)) q @ [a\<leftarrow>p. fst a \<notin> fst ` set q]" |
56 "perm_add_raw p q = map (map_prod id (perm_apply p)) q @ [a\<leftarrow>p. fst a \<notin> fst ` set q]" |
57 |
57 |
58 lemma perm_apply_del[simp]: |
58 lemma perm_apply_del[simp]: |
59 "e \<noteq> b \<Longrightarrow> perm_apply [a\<leftarrow>l. fst a \<noteq> b] e = perm_apply l e" |
59 "e \<noteq> b \<Longrightarrow> perm_apply [a\<leftarrow>l. fst a \<noteq> b] e = perm_apply l e" |
60 "e \<noteq> b \<Longrightarrow> e \<noteq> c \<Longrightarrow> perm_apply [a\<leftarrow>l . fst a \<noteq> b \<and> fst a \<noteq> c] e = perm_apply l e" |
60 "e \<noteq> b \<Longrightarrow> e \<noteq> c \<Longrightarrow> perm_apply [a\<leftarrow>l . fst a \<noteq> b \<and> fst a \<noteq> c] e = perm_apply l e" |
61 by (induct l) auto |
61 by (induct l) auto |
144 by (metis length_map nth_eq_iff_index_eq nth_map snd_conv) |
144 by (metis length_map nth_eq_iff_index_eq nth_map snd_conv) |
145 |
145 |
146 lemma valid_perm_add_minus: "valid_perm a \<Longrightarrow> perm_apply (map swap_pair a) (perm_apply a e) = e" |
146 lemma valid_perm_add_minus: "valid_perm a \<Longrightarrow> perm_apply (map swap_pair a) (perm_apply a e) = e" |
147 apply (auto simp add: filter_map_swap_pair filter_eq_nil filter_rev_eq_nil perm_apply_def split: list.split) |
147 apply (auto simp add: filter_map_swap_pair filter_eq_nil filter_rev_eq_nil perm_apply_def split: list.split) |
148 apply (metis filter_eq_nil(2) neq_Nil_conv valid_perm_def) |
148 apply (metis filter_eq_nil(2) neq_Nil_conv valid_perm_def) |
149 apply (metis hd.simps hd_in_set image_eqI list.simps(2) member_project project_set snd_conv) |
149 apply (metis list.sel(1) hd_in_set image_eqI list.simps(2) member_project project_set snd_conv) |
150 apply (frule filter_fst_eq(1)) |
150 apply (frule filter_fst_eq(1)) |
151 apply (frule filter_fst_eq(2)) |
151 apply (frule filter_fst_eq(2)) |
152 apply (auto simp add: swap_pair_def) |
152 apply (auto simp add: swap_pair_def) |
153 apply (erule valid_perm_lookup_fst_eq_snd) |
153 apply (erule valid_perm_lookup_fst_eq_snd) |
154 apply assumption+ |
154 apply assumption+ |
160 |
160 |
161 lemma uminus_perm_raw_rsp[simp]: |
161 lemma uminus_perm_raw_rsp[simp]: |
162 "perm_eq x y \<Longrightarrow> perm_eq (map swap_pair x) (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_prod[simp]: |
166 "fst ` map_pair f g ` set l = f ` fst ` set l" |
166 "fst ` map_prod f g ` set l = f ` fst ` set l" |
167 "snd ` map_pair f g ` set l = g ` snd ` set l" |
167 "snd ` map_prod f g ` set l = g ` snd ` set l" |
168 by (induct l) auto |
168 by (induct l) auto |
169 |
169 |
170 lemma fst_diff[simp]: |
170 lemma fst_diff[simp]: |
171 shows "fst ` {xa \<in> set x. fst xa \<notin> fst ` set y} = fst ` set x - fst ` set y" |
171 shows "fst ` {xa \<in> set x. fst xa \<notin> fst ` set y} = fst ` set x - fst ` set y" |
172 by auto |
172 by auto |