section ‹Algebra› text ‹ In this section, we develop the necessary algebra for developing the theory of Coxeter systems, including groups, quotient groups, free groups, group presentations, and words in a group over a set of generators. › theory Algebra imports Prelim begin subsection ‹Miscellaneous algebra facts› lemma times2_conv_add: "(j::nat) + j = 2*j" by (induct j) auto lemma (in comm_semiring_1) odd_n0: "odd m ⟹ m≠0" using dvd_0_right by fast lemma (in semigroup_add) add_assoc4: "a + b + c + d = a + (b + c + d)" using add.assoc by simp lemmas (in monoid_add) sum_list_map_cong = arg_cong[OF map_cong, OF refl, of _ _ _ sum_list] context group_add begin lemma map_uminus_order2: "∀s∈set ss. s+s=0 ⟹ map (uminus) ss = ss" by (induct ss) (auto simp add: minus_unique) lemma uminus_sum_list: "- sum_list as = sum_list (map uminus (rev as))" by (induct as) (auto simp add: minus_add) lemma uminus_sum_list_order2: "∀s∈set ss. s+s=0 ⟹ - sum_list ss = sum_list (rev ss)" using uminus_sum_list map_uminus_order2 by simp end (* context group_add *) subsection ‹The type of permutations of a type› text ‹ Here we construct a type consisting of all bijective functions on a type. This is the prototypical example of a group, where the group operation is composition, and every group can be embedded into such a type. It is for this purpose that we construct this type, so that we may confer upon suitable subsets of types that are not of class @{class group_add} the properties of that class, via a suitable injective correspondence to this permutation type. › typedef 'a permutation = "{f::'a⇒'a. bij f}" morphisms permutation Abs_permutation by fast setup_lifting type_definition_permutation abbreviation permutation_apply :: "'a permutation ⇒ 'a ⇒ 'a " (infixr "→" 90) where "p → a ≡ permutation p a" abbreviation permutation_image :: "'a permutation ⇒ 'a set ⇒ 'a set" (infixr "`→" 90) where "p `→ A ≡ permutation p ` A" lemma permutation_eq_image: "a `→ A = a `→ B ⟹ A=B" using permutation[of a] inj_eq_image[OF bij_is_inj] by auto instantiation permutation :: (type) zero begin lift_definition zero_permutation :: "'a permutation" is "id::'a⇒'a" by simp instance .. end instantiation permutation :: (type) plus begin lift_definition plus_permutation :: "'a permutation ⇒ 'a permutation ⇒ 'a permutation" is "comp" using bij_comp by fast instance .. end lemma plus_permutation_abs_eq: "bij f ⟹ bij g ⟹ Abs_permutation f + Abs_permutation g = Abs_permutation (f∘g)" by (simp add: plus_permutation.abs_eq eq_onp_same_args) instance permutation :: (type) semigroup_add proof fix a b c :: "'a permutation" show "a + b + c = a + (b + c)" using comp_assoc[of "permutation a" "permutation b" "permutation c"] by transfer simp qed instance permutation :: (type) monoid_add proof fix a :: "'a permutation" show "0 + a = a" by transfer simp show "a + 0 = a" by transfer simp qed instantiation permutation :: (type) uminus begin lift_definition uminus_permutation :: "'a permutation ⇒ 'a permutation" is "λf. the_inv f" using bij_betw_the_inv_into by fast instance .. end instantiation permutation :: (type) minus begin lift_definition minus_permutation :: "'a permutation ⇒ 'a permutation ⇒ 'a permutation" is "λf g. f ∘ (the_inv g)" using bij_betw_the_inv_into bij_comp by fast instance .. end lemma minus_permutation_abs_eq: "bij f ⟹ bij g ⟹ Abs_permutation f - Abs_permutation g = Abs_permutation (f ∘ the_inv g)" by (simp add: minus_permutation.abs_eq eq_onp_same_args) instance permutation :: (type) group_add proof fix a b :: "'a permutation" show "- a + a = 0" using the_inv_leftinv[of "permutation a"] by transfer simp show "a + - b = a - b" by transfer simp qed subsection ‹Natural action of @{typ nat} on types of class @{class monoid_add}› subsubsection ‹Translation from class @{class power}.› text ‹ Here we translate the @{class power} class to apply to types of class @{class monoid_add}. › context monoid_add begin sublocale nataction: power 0 plus . sublocale add_mult_translate: monoid_mult 0 plus by unfold_locales (auto simp add: add.assoc) abbreviation nataction :: "'a ⇒ nat ⇒ 'a" (infix "+^" 80) where "a+^n ≡ nataction.power a n" lemmas nataction_2 = add_mult_translate.power2_eq_square lemmas nataction_Suc2 = add_mult_translate.power_Suc2 lemma alternating_sum_list_conv_nataction: "sum_list (alternating_list (2*n) s t) = (s+t)+^n" by (induct n) (auto simp add: nataction_Suc2[THEN sym]) lemma nataction_add_flip: "(a+b)+^(Suc n) = a + (b+a)+^n + b" using nataction_Suc2 add.assoc by (induct n arbitrary: a b) auto end (* context monoid_add *) lemma (in group_add) nataction_add_eq0_flip: assumes "(a+b)+^n = 0" shows "(b+a)+^n = 0" proof (cases n) case (Suc k) with assms show ?thesis using nataction_add_flip add.assoc[of "-a" "a+b" "(a+b)+^k"] by simp qed simp subsubsection ‹Additive order of an element› context monoid_add begin definition add_order :: "'a ⇒ nat" where "add_order a ≡ if (∃n>0. a+^n = 0) then (LEAST n. n>0 ∧ a+^n = 0) else 0" lemma add_order: "a+^(add_order a) = 0" using LeastI_ex[of "λn. n>0 ∧ a+^n = 0"] add_order_def by simp lemma add_order_least: "n>0 ⟹ a+^n = 0 ⟹ add_order a ≤ n" using Least_le[of "λn. n>0 ∧ a+^n = 0"] add_order_def by simp lemma add_order_equality: "⟦ n>0; a+^n = 0; (⋀m. m>0 ⟹ a+^m = 0 ⟹ n≤m) ⟧ ⟹ add_order a = n" using Least_equality[of "λn. n>0 ∧ a+^n = 0"] add_order_def by auto lemma add_order0: "add_order 0 = 1" using add_order_equality by simp lemma add_order_gt0: "(add_order a > 0) = (∃n>0. a+^n = 0)" using LeastI_ex[of "λn. n>0 ∧ a+^n = 0"] add_order_def by simp lemma add_order_eq0: "add_order a = 0 ⟹ n>0 ⟹ a+^n ≠ 0" using add_order_gt0 by force lemma less_add_order_eq_0: assumes "a+^k = 0" "k < add_order a" shows "k = 0" proof (cases "k=0") case False moreover with assms(1) have "∃n>0. a+^n = 0" by fast ultimately show ?thesis using assms add_order_def not_less_Least[of k "λn. n>0 ∧ a+^n = 0"] by auto qed simp lemma less_add_order_eq_0_contra: "k>0 ⟹ k < add_order a ⟹ a+^k ≠ 0" using less_add_order_eq_0 by fast lemma add_order_relator: "add_order (a+^(add_order a)) = 1" using add_order by (auto intro: add_order_equality) abbreviation pair_relator_list :: "'a ⇒ 'a ⇒ 'a list" where "pair_relator_list s t ≡ alternating_list (2*add_order (s+t)) s t" abbreviation pair_relator_halflist :: "'a ⇒ 'a ⇒ 'a list" where "pair_relator_halflist s t ≡ alternating_list (add_order (s+t)) s t" abbreviation pair_relator_halflist2 :: "'a ⇒ 'a ⇒ 'a list" where "pair_relator_halflist2 s t ≡ (if even (add_order (s+t)) then pair_relator_halflist s t else pair_relator_halflist t s)" lemma sum_list_pair_relator_list: "sum_list (pair_relator_list s t) = 0" by (auto simp add: add_order alternating_sum_list_conv_nataction) end (* context monoid_add *) context group_add begin lemma add_order_add_eq1: "add_order (s+t) = 1 ⟹ t = -s" using add_order[of "s+t"] by (simp add: minus_unique) lemma add_order_add_sym: "add_order (t+s) = add_order (s+t)" proof (cases "add_order (t+s) = 0" "add_order (s+t) = 0" rule: two_cases) case one thus ?thesis using add_order nataction_add_eq0_flip[of s t] add_order_eq0 by auto next case other thus ?thesis using add_order nataction_add_eq0_flip[of t s] add_order_eq0 by auto next case neither thus ?thesis using add_order[of "s+t"] add_order[of "t+s"] nataction_add_eq0_flip[of s t] nataction_add_eq0_flip[of t s] add_order_least[of "add_order (s+t)"] add_order_least[of "add_order (t+s)"] by fastforce qed simp lemma pair_relator_halflist_append: "pair_relator_halflist s t @ pair_relator_halflist2 s t = pair_relator_list s t" using alternating_list_split[of "add_order (s+t)" "add_order (s+t)" s t] by (auto simp add: times2_conv_add add_order_add_sym) lemma rev_pair_relator_list: "rev (pair_relator_list s t) = pair_relator_list t s" by (simp add:rev_alternating_list add_order_add_sym) lemma pair_relator_halflist2_conv_rev_pair_relator_halflist: "pair_relator_halflist2 s t = rev (pair_relator_halflist t s)" by (auto simp add: add_order_add_sym rev_alternating_list) end (* context group_add *) subsection ‹Partial sums of a list› text ‹ Here we construct a list that collects the results of adding the elements of a given list together one-by-one. › context monoid_add begin primrec sums :: "'a list ⇒ 'a list" where "sums [] = [0]" | "sums (x#xs) = 0 # map ((+) x) (sums xs)" lemma length_sums: "length (sums xs) = Suc (length xs)" by (induct xs) auto lemma sums_snoc: "sums (xs@[x]) = sums xs @ [sum_list (xs@[x])]" by (induct xs) (auto simp add: add.assoc) lemma sums_append2: "sums (xs@ys) = butlast (sums xs) @ map ((+) (sum_list xs)) (sums ys)" proof (induct ys rule: rev_induct) case Nil show ?case by (cases xs rule: rev_cases) (auto simp add: sums_snoc) next case (snoc y ys) thus ?case using sums_snoc[of "xs@ys"] by (simp add: sums_snoc) qed lemma sums_Cons_conv_append_tl: "sums (x#xs) = 0 # x # map ((+) x) (tl (sums xs))" by (cases xs) auto lemma pullback_sums_map_middle2: "map F (sums xs) = ds@[d,e]@es ⟹ ∃as a bs. xs = as@[a]@bs ∧ map F (sums as) = ds@[d] ∧ d = F (sum_list as) ∧ e = F (sum_list (as@[a]))" proof (induct xs es rule: list_induct2_snoc) case (Nil2 xs) show ?case proof (cases xs rule: rev_cases) case Nil with Nil2 show ?thesis by simp next case (snoc ys y) have ys: "xs = ys@[y]" by fact with Nil2(1) have y: "map F (sums ys) = ds@[d]" "e = F (sum_list (ys@[y]))" by (auto simp add: sums_snoc) show ?thesis proof (cases ys rule: rev_cases) case Nil with ys y have "xs = []@[y]@[]" "map F (sums []) = ds@[d]" "d = F (sum_list [])" "e = F (sum_list ([]@[y]))" by auto thus ?thesis by fast next case (snoc zs z) with y(1) have z: "map F (sums zs) = ds" "d = F (sum_list (zs@[z]))" by (auto simp add: sums_snoc) from z(1) ys y snoc have "xs = (zs@[z])@[y]@[]" "map F (sums (zs@[z])) = ds@[d]" "e = F (sum_list ((zs@[z])@[y]))" by auto with z(2) show ?thesis by fast qed qed next case snoc thus ?case by (fastforce simp add: sums_snoc) qed simp lemma pullback_sums_map_middle3: "map F (sums xs) = ds@[d,e,f]@fs ⟹ ∃as a b bs. xs = as@[a,b]@bs ∧ d = F (sum_list as) ∧ e = F (sum_list (as@[a])) ∧ f = F (sum_list (as@[a,b]))" proof (induct xs fs rule: list_induct2_snoc) case (Nil2 xs) show ?case proof (cases xs rule: rev_cases) case Nil with Nil2 show ?thesis by simp next case (snoc ys y) with Nil2 have y: "map F (sums ys) = ds@[d,e]" "f = F (sum_list (ys@[y]))" by (auto simp add: sums_snoc) from y(1) obtain as a bs where asabs: "ys = as@[a]@bs" "map F (sums as) = ds@[d]" "d = F (sum_list as)" "e = F (sum_list (as@[a]))" using pullback_sums_map_middle2[of F ys ds] by fastforce have "bs = []" proof- from y(1) asabs(1,2) have "Suc (length bs) = Suc 0" by (auto simp add: sums_append2 map_butlast length_sums[THEN sym]) thus ?thesis by fast qed with snoc asabs(1) y(2) have "xs = as@[a,y]@[]" "f = F (sum_list (as@[a,y]))" by auto with asabs(3,4) show ?thesis by fast qed next case snoc thus ?case by (fastforce simp add: sums_snoc) qed simp lemma pullback_sums_map_double_middle2: assumes "map F (sums xs) = ds@[d,e]@es@[f,g]@gs" shows "∃as a bs b cs. xs = as@[a]@bs@[b]@cs ∧ d = F (sum_list as) ∧ e = F (sum_list (as@[a])) ∧ f = F (sum_list (as@[a]@bs)) ∧ g = F (sum_list (as@[a]@bs@[b]))" proof- from assms obtain As b cs where Asbcs: "xs = As@[b]@cs" "map F (sums As) = ds@[d,e]@es@[f]" "f = F (sum_list As)" "g = F (sum_list (As@[b]))" using pullback_sums_map_middle2[of F xs "ds@[d,e]@es"] by fastforce from Asbcs show ?thesis using pullback_sums_map_middle2[of F As ds d e "es@[f]"] by fastforce qed end (* context monoid_add *) subsection ‹Sums of alternating lists› lemma (in group_add) uminus_sum_list_alternating_order2: "s+s=0 ⟹ t+t=0 ⟹ - sum_list (alternating_list n s t) = sum_list (if even n then alternating_list n t s else alternating_list n s t)" using uminus_sum_list_order2 set_alternating_list[of n] rev_alternating_list[of n s] by fastforce context monoid_add begin lemma alternating_order2_cancel_1left: "s+s=0 ⟹ sum_list (s # (alternating_list (Suc n) s t)) = sum_list (alternating_list n t s)" using add.assoc[of s s] alternating_list_Suc_Cons[of n s] by simp lemma alternating_order2_cancel_2left: "s+s=0 ⟹ t+t=0 ⟹ sum_list (t # s # (alternating_list (Suc (Suc n)) s t)) = sum_list (alternating_list n s t)" using alternating_order2_cancel_1left[of s "Suc n"] alternating_order2_cancel_1left[of t n] by simp lemma alternating_order2_even_cancel_right: assumes st : "s+s=0" "t+t=0" and even_n: "even n" shows "m ≤ n ⟹ sum_list (alternating_list n s t @ alternating_list m t s) = sum_list (alternating_list (n-m) s t)" proof (induct n arbitrary: m rule: nat_even_induct, rule even_n) case (SucSuc k) with st show ?case using alternating_order2_cancel_2left[of t s] by (cases m rule: nat_cases_2Suc) auto qed simp end (* context monoid_add *) subsection ‹Conjugation in @{class group_add}› subsubsection ‹Abbreviations and basic facts› context group_add begin abbreviation lconjby :: "'a⇒'a⇒'a" where "lconjby x y ≡ x+y-x" abbreviation rconjby :: "'a⇒'a⇒'a" where "rconjby x y ≡ -x+y+x" lemma lconjby_add: "lconjby (x+y) z = lconjby x (lconjby y z)" by (auto simp add: algebra_simps) lemma rconjby_add: "rconjby (x+y) z = rconjby y (rconjby x z)" by (simp add: minus_add add.assoc[THEN sym]) lemma add_rconjby: "rconjby x y + rconjby x z = rconjby x (y+z)" by (simp add: add.assoc) lemma lconjby_uminus: "lconjby x (-y) = - lconjby x y" using minus_unique[of "lconjby x y", THEN sym] by (simp add: algebra_simps) lemma rconjby_uminus: "rconjby x (-y) = - rconjby x y" using minus_unique[of "rconjby x y"] add_assoc4[of "rconjby x y" "-x" "-y" x] by simp lemma lconjby_rconjby: "lconjby x (rconjby x y) = y" by (simp add: algebra_simps) lemma rconjby_lconjby: "rconjby x (lconjby x y) = y" by (simp add: algebra_simps) lemma lconjby_inj: "inj (lconjby x)" using rconjby_lconjby by (fast intro: inj_on_inverseI) lemma rconjby_inj: "inj (rconjby x)" using lconjby_rconjby by (fast intro: inj_on_inverseI) lemma lconjby_surj: "surj (lconjby x)" using lconjby_rconjby surjI[of "lconjby x"] by fast lemma lconjby_bij: "bij (lconjby x)" unfolding bij_def using lconjby_inj lconjby_surj by fast lemma the_inv_lconjby: "the_inv (lconjby x) = (rconjby x)" using bij_betw_f_the_inv_into_f[OF lconjby_bij, of _ x] lconjby_rconjby by (force intro: inj_onD[OF lconjby_inj, of x]) lemma lconjby_eq_conv_rconjby_eq: "w = lconjby x y ⟹ y = rconjby x w" using the_inv_lconjby the_inv_into_f_f[OF lconjby_inj] by force lemma rconjby_order2: "s+s = 0 ⟹ rconjby x s + rconjby x s = 0" by (simp add: add_rconjby) lemma rconjby_order2_eq_lconjby: assumes "s+s=0" shows "rconjby s = lconjby s" proof- have "rconjby s = lconjby (-s)" by simp with assms show ?thesis using minus_unique by simp qed lemma lconjby_alternating_list_order2: assumes "s+s=0" "t+t=0" shows "lconjby (sum_list (alternating_list k s t)) (if even k then s else t) = sum_list (alternating_list (Suc (2*k)) s t)" proof (induct k rule: nat_induct_step2) case (SucSuc m) have "lconjby (sum_list (alternating_list (Suc (Suc m)) s t)) (if even (Suc (Suc m)) then s else t) = s + t + lconjby (sum_list (alternating_list m s t)) (if even m then s else t) - t - s" using alternating_list_SucSuc_ConsCons[of m s t] by (simp add: algebra_simps) also from assms SucSuc have "… = sum_list (alternating_list (Suc (2*Suc (Suc m))) s t)" using alternating_list_SucSuc_ConsCons[of "Suc (2*m)" s t] sum_list.append[of "alternating_list (Suc (2*Suc m)) s t" "[t]"] by (simp add: algebra_simps) finally show ?case by fast qed (auto simp add: assms(1) algebra_simps) end (* context group_add *) subsubsection ‹The conjugation sequence› text ‹ Given a list in @{class group_add}, we create a new list by conjugating each term by all the previous terms. This sequence arises in Coxeter systems. › context group_add begin primrec lconjseq :: "'a list ⇒ 'a list" where "lconjseq [] = []" | "lconjseq (x#xs) = x # (map (lconjby x) (lconjseq xs))" lemma length_lconjseq: "length (lconjseq xs) = length xs" by (induct xs) auto lemma lconjseq_snoc: "lconjseq (xs@[x]) = lconjseq xs @ [lconjby (sum_list xs) x]" by (induct xs) (auto simp add: lconjby_add) lemma lconjseq_append: "lconjseq (xs@ys) = lconjseq xs @ (map (lconjby (sum_list xs)) (lconjseq ys))" proof (induct ys rule: rev_induct) case (snoc y ys) thus ?case using lconjseq_snoc[of "xs@ys"] lconjseq_snoc[of ys] by (simp add: lconjby_add) qed simp lemma lconjseq_alternating_order2_repeats': fixes s t :: 'a defines altst: "altst ≡ λn. alternating_list n s t" and altts: "altts ≡ λn. alternating_list n t s" assumes st : "s+s=0" "t+t=0" "(s+t)+^k = 0" shows "map (lconjby (sum_list (altst k))) (lconjseq (if even k then altst m else altts m)) = lconjseq (altst m)" proof (induct m) case (Suc j) with altst altts have "map (lconjby (sum_list (altst k))) (lconjseq (if even k then altst (Suc j) else altts (Suc j))) = lconjseq (altst j) @ [lconjby (sum_list (altst k @ (if even k then altst j else altts j))) (if even k then (if even j then s else t) else (if even j then t else s))]" by (auto simp add: lconjseq_snoc lconjby_add) also from altst altts st(1,2) have "… = lconjseq (altst j) @ [sum_list (altst (Suc (2*(k+j))))]" using lconjby_alternating_list_order2[of s t "k+j"] by (cases "even k") (auto simp add: alternating_list_append[of k]) finally show ?case using altst st by (auto simp add: alternating_list_append(1)[THEN sym] alternating_sum_list_conv_nataction lconjby_alternating_list_order2 lconjseq_snoc ) qed (simp add: altst altts) lemma lconjseq_alternating_order2_repeats: fixes s t :: 'a and k :: nat defines altst: "altst ≡ λn. alternating_list n s t" and altts: "altts ≡ λn. alternating_list n t s" assumes st: "s+s=0" "t+t=0" "(s+t)+^k = 0" shows "lconjseq (altst (2*k)) = lconjseq (altst k) @ lconjseq (altst k)" proof- from altst altts have "lconjseq (altst (2*k)) = lconjseq (altst k) @ map (lconjby (sum_list (altst k))) (lconjseq (if even k then altst k else altts k))" using alternating_list_append[THEN sym, of k k s t] by (auto simp add: times2_conv_add lconjseq_append) with altst altts st show ?thesis using lconjseq_alternating_order2_repeats'[of s t k k] by auto qed lemma even_count_lconjseq_alternating_order2: fixes s t :: 'a assumes "s+s=0" "t+t=0" "(s+t)+^k = 0" shows "even (count_list (lconjseq (alternating_list (2*k) s t)) x)" proof- define xs where xs: "xs ≡ lconjseq (alternating_list (2*k) s t)" with assms obtain as where "xs = as@as" using lconjseq_alternating_order2_repeats by fast hence "count_list xs x = 2 * (count_list as x)" by (simp add: count_list_append times2_conv_add) with xs show ?thesis by simp qed lemma order2_hd_in_lconjseq_deletion: shows "s+s=0 ⟹ s ∈ set (lconjseq ss) ⟹ ∃as b bs. ss = as@[b]@bs ∧ sum_list (s#ss) = sum_list (as@bs)" proof (induct ss arbitrary: s rule: rev_induct) case (snoc t ts) show ?case proof (cases "s ∈ set (lconjseq ts)") case True with snoc(1,2) obtain as b bs where asbbs: "ts = as @[b]@bs" "sum_list (s#ts) = sum_list (as@bs)" by fastforce from asbbs(2) have "sum_list (s#ts@[t]) = sum_list (as@(bs@[t]))" using sum_list.append[of "s#ts" "[t]"] sum_list.append[of "as@bs" "[t]"] by simp with asbbs(1) show ?thesis by fastforce next case False with snoc(3) have s: "s = lconjby (sum_list ts) t" by (simp add: lconjseq_snoc) with snoc(2) have "t+t=0" using lconjby_eq_conv_rconjby_eq[of s "sum_list ts" t] rconjby_order2[of s "sum_list ts"] by simp moreover from s have "sum_list (s#ts@[t]) = sum_list ts + t + t" using add.assoc[of "sum_list ts + t - sum_list ts" "sum_list ts"] by (simp add: algebra_simps) ultimately have "sum_list (s#ts@[t]) = sum_list (ts@[])" by (simp add: algebra_simps) thus ?thesis by fast qed qed simp end (* context group_add *) subsubsection ‹The action on signed @{class group_add} elements› text ‹ Here we construct an action of a group on itself by conjugation, where group elements are endowed with an auxiliary sign by pairing with a boolean element. In multiple applications of this action, the auxiliary sign helps keep track of how many times the elements conjugating and being conjugated are the same. This action arises in exploring reduced expressions of group elements as words in a set of generators of order two (in particular, in a Coxeter group). › type_synonym 'a signed = "'a×bool" definition signed_funaction :: "('a⇒'a⇒'a) ⇒ 'a ⇒ 'a signed ⇒ 'a signed" where "signed_funaction f s x ≡ map_prod (f s) (λb. b ≠ (fst x = s)) x" ― ‹so the sign of @{term x} is flipped precisely when its first component is equal to @{term s}› context group_add begin abbreviation "signed_lconjaction ≡ signed_funaction lconjby" abbreviation "signed_rconjaction ≡ signed_funaction rconjby" lemmas signed_lconjactionD = signed_funaction_def[of lconjby] lemmas signed_rconjactionD = signed_funaction_def[of rconjby] abbreviation signed_lconjpermutation :: "'a ⇒ 'a signed permutation" where "signed_lconjpermutation s ≡ Abs_permutation (signed_lconjaction s)" abbreviation signed_list_lconjaction :: "'a list ⇒ 'a signed ⇒ 'a signed" where "signed_list_lconjaction ss ≡ foldr signed_lconjaction ss" lemma signed_lconjaction_fst: "fst (signed_lconjaction s x) = lconjby s (fst x)" using signed_lconjactionD by simp lemma signed_lconjaction_rconjaction: "signed_lconjaction s (signed_rconjaction s x) = x" proof- obtain a::'a and b::bool where "x = (a,b)" by fastforce thus ?thesis using signed_lconjactionD signed_rconjactionD injD[OF rconjby_inj, of s a] lconjby_rconjby[of s a] by auto qed lemma signed_rconjaction_by_order2_eq_lconjaction: "s+s=0 ⟹ signed_rconjaction s = signed_lconjaction s" using signed_funaction_def[of lconjby s] signed_funaction_def[of rconjby s] rconjby_order2_eq_lconjby[of s] by auto lemma inj_signed_lconjaction: "inj (signed_lconjaction s)" proof (rule injI) fix x y assume 1: "signed_lconjaction s x = signed_lconjaction s y" moreover obtain a1 a2 :: 'a and b1 b2 :: bool where xy: "x = (a1,b1)" "y = (a2,b2)" by fastforce ultimately show "x=y" using injD[OF lconjby_inj, of s a1 a2] signed_lconjactionD by (cases "a1=s" "a2=s" rule: two_cases) auto qed lemma surj_signed_lconjaction: "surj (signed_lconjaction s)" using signed_lconjaction_rconjaction[THEN sym] by fast lemma bij_signed_lconjaction: "bij (signed_lconjaction s)" using inj_signed_lconjaction surj_signed_lconjaction by (fast intro: bijI) lemma the_inv_signed_lconjaction: "the_inv (signed_lconjaction s) = signed_rconjaction s" proof fix x show "the_inv (signed_lconjaction s) x = signed_rconjaction s x" proof (rule the_inv_into_f_eq, rule inj_signed_lconjaction) show "signed_lconjaction s (signed_rconjaction s x) = x" using signed_lconjaction_rconjaction by fast qed (simp add: surj_signed_lconjaction) qed lemma the_inv_signed_lconjaction_by_order2: "s+s=0 ⟹ the_inv (signed_lconjaction s) = signed_lconjaction s" using the_inv_signed_lconjaction signed_rconjaction_by_order2_eq_lconjaction by simp lemma signed_list_lconjaction_fst: "fst (signed_list_lconjaction ss x) = lconjby (sum_list ss) (fst x)" using signed_lconjaction_fst lconjby_add by (induct ss) auto lemma signed_list_lconjaction_snd: shows "∀s∈set ss. s+s=0 ⟹ snd (signed_list_lconjaction ss x) = (if even (count_list (lconjseq (rev ss)) (fst x)) then snd x else ¬snd x)" proof (induct ss) case (Cons s ss) hence prevcase: "snd (signed_list_lconjaction ss x) = (if even (count_list (lconjseq (rev ss)) (fst x)) then snd x else ¬ snd x)" by simp have 1: "snd (signed_list_lconjaction (s # ss) x) = snd (signed_lconjaction s (signed_list_lconjaction ss x))" by simp show ?case proof (cases "fst (signed_list_lconjaction ss x) = s") case True with 1 prevcase have "snd (signed_list_lconjaction (s # ss) x) = (if even (count_list (lconjseq (rev ss)) (fst x)) then ¬ snd x else snd x)" by (simp add: signed_lconjactionD) with True Cons(2) show ?thesis by (simp add: signed_list_lconjaction_fst lconjby_eq_conv_rconjby_eq uminus_sum_list_order2[THEN sym] lconjseq_snoc count_list_snoc ) next case False hence "rconjby (sum_list ss) (lconjby (sum_list ss) (fst x)) ≠ rconjby (sum_list ss) s" by (simp add: signed_list_lconjaction_fst) with Cons(2) have "count_list (lconjseq (rev (s#ss))) (fst x) = count_list (lconjseq (rev ss)) (fst x)" by (simp add: rconjby_lconjby uminus_sum_list_order2[THEN sym] lconjseq_snoc count_list_snoc ) moreover from False 1 prevcase have "snd (signed_list_lconjaction (s # ss) x) = (if even (count_list (lconjseq (rev ss)) (fst x)) then snd x else ¬ snd x)" by (simp add: signed_lconjactionD) ultimately show ?thesis by simp qed qed simp end (* context group_add *) subsection ‹Cosets› subsubsection ‹Basic facts› lemma set_zero_plus' [simp]: "(0::'a::monoid_add) +o C = C" ― ‹lemma @{text "Set_Algebras.set_zero_plus"} is restricted to types of class @{class comm_monoid_add}; here is a version in @{class monoid_add}.› by (auto simp add: elt_set_plus_def) lemma lcoset_0: "(w::'a::monoid_add) +o 0 = {w}" using elt_set_plus_def[of w] by simp lemma lcoset_refl: "(0::'a::monoid_add) ∈ A ⟹ a ∈ a +o A" using elt_set_plus_def by force lemma lcoset_eq_reps_subset: "(a::'a::group_add) +o A ⊆ a +o B ⟹ A ⊆ B" using elt_set_plus_def[of a] by auto lemma lcoset_eq_reps: "(a::'a::group_add) +o A = a +o B ⟹ A = B" using lcoset_eq_reps_subset[of a A B] lcoset_eq_reps_subset[of a B A] by auto lemma lcoset_inj_on: "inj ((+o) (a::'a::group_add))" using lcoset_eq_reps inj_onI[of UNIV "(+o) a"] by auto lemma lcoset_conv_set: "(a::'g::group_add) ∈ b +o A ⟹ -b + a ∈ A" by (auto simp add: elt_set_plus_def) subsubsection ‹The supset order on cosets› lemma supset_lbound_lcoset_shift: "supset_lbound_of X Y B ⟹ ordering.lbound_of (⊇) (a +o X) (a +o Y) (a +o B)" using ordering.lbound_of_def[OF supset_poset, of X Y B] by (fast intro: ordering.lbound_ofI supset_poset) lemma supset_glbound_in_of_lcoset_shift: fixes P :: "'a::group_add set set" assumes "supset_glbound_in_of P X Y B" shows "supset_glbound_in_of ((+o) a ` P) (a +o X) (a +o Y) (a +o B)" using ordering.glbound_in_ofD_in[OF supset_poset, OF assms] ordering.glbound_in_ofD_lbound[OF supset_poset, OF assms] supset_lbound_lcoset_shift[of X Y B a] supset_lbound_lcoset_shift[of "a +o X" "a +o Y" _ "-a"] ordering.glbound_in_ofD_glbound[OF supset_poset, OF assms] ordering.glbound_in_ofI[ OF supset_poset, of "a +o B" "(+o) a ` P" "a +o X" "a +o Y" ] by (fastforce simp add: set_plus_rearrange2) subsubsection ‹The afforded partition› definition lcoset_rel :: "'a::{uminus,plus} set ⇒ ('a×'a) set" where "lcoset_rel A ≡ {(x,y). -x + y ∈ A}" lemma lcoset_relI: "-x+y ∈ A ⟹ (x,y) ∈ lcoset_rel A" using lcoset_rel_def by fast subsection ‹Groups› text ‹We consider groups as closed sets in a type of class @{class group_add}.› subsubsection ‹Locale definition and basic facts› locale Group = fixes G :: "'g::group_add set" assumes nonempty : "G ≠ {}" and diff_closed: "⋀g h. g ∈ G ⟹ h ∈ G ⟹ g - h ∈ G" begin abbreviation Subgroup :: "'g set ⇒ bool" where "Subgroup H ≡ Group H ∧ H ⊆ G" lemma SubgroupD1: "Subgroup H ⟹ Group H" by fast lemma zero_closed : "0 ∈ G" proof- from nonempty obtain g where "g ∈ G" by fast hence "g - g ∈ G" using diff_closed by fast thus ?thesis by simp qed lemma uminus_closed: "g∈G ⟹ -g∈G" using zero_closed diff_closed[of 0 g] by simp lemma add_closed: "g∈G ⟹ h∈G ⟹ g+h ∈ G" using uminus_closed[of h] diff_closed[of g "-h"] by simp lemma uminus_add_closed: "g ∈ G ⟹ h ∈ G ⟹ -g + h ∈ G" using uminus_closed add_closed by fast lemma lconjby_closed: "g∈G ⟹ x∈G ⟹ lconjby g x ∈ G" using add_closed diff_closed by fast lemma lconjby_set_closed: "g∈G ⟹ A⊆G ⟹ lconjby g ` A ⊆ G" using lconjby_closed by fast lemma set_lconjby_subset_closed: "H⊆G ⟹ A⊆G ⟹ (⋃h∈H. lconjby h ` A) ⊆ G" using lconjby_set_closed[of _ A] by fast lemma sum_list_map_closed: "set (map f as) ⊆ G ⟹ (∑a←as. f a) ∈ G" using zero_closed add_closed by (induct as) auto lemma sum_list_closed: "set as ⊆ G ⟹ sum_list as ∈ G" using sum_list_map_closed by force end (* context Group *) subsubsection ‹Sets with a suitable binary operation› text ‹ We have chosen to only consider groups in types of class @{class group_add} so that we can take advantage of all the algebra lemmas already proven in @{theory HOL.Groups}, as well as constructs like @{const sum_list}. The following locale builds a bridge between this restricted view of groups and the usual notion of a binary operation on a set satisfying the group axioms, by constructing an injective map into type @{type permutation} (which is of class @{class group_add} with respect to the composition operation) that respects the group operation. This bridge will be necessary to define quotient groups, in particular. › locale BinOpSetGroup = fixes G :: "'a set" and binop :: "'a⇒'a⇒'a" and e :: "'a" assumes closed : "g∈G ⟹ h∈G ⟹ binop g h ∈ G" and assoc : "⟦ g∈G; h∈G; k∈G ⟧ ⟹ binop (binop g h) k = binop g (binop h k)" and identity: "e∈G" "g∈G ⟹ binop g e = g" "g∈G ⟹ binop e g = g" and inverses: "g∈G ⟹ ∃h∈G. binop g h = e ∧ binop h g = e" begin lemma unique_identity1: "g∈G ⟹ ∀x∈G. binop g x = x ⟹ g = e" using identity(1,2) by auto lemma unique_inverse: assumes "g∈G" shows "∃!h. h∈G ∧ binop g h = e ∧ binop h g = e" proof (rule ex_ex1I) from assms show "∃h. h ∈ G ∧ binop g h = e ∧ binop h g = e" using inverses by fast next fix h k assume "h∈G ∧ binop g h = e ∧ binop h g = e" "k∈G ∧ binop g k = e ∧ binop k g = e" hence h: "h∈G" "binop g h = e" "binop h g = e" and k: "k∈G" "binop g k = e" "binop k g = e" by auto from assms h(1,3) k(1,2) show "h=k" using identity(2,3) assoc by force qed abbreviation "G_perm g ≡ restrict1 (binop g) G" definition Abs_G_perm :: "'a ⇒ 'a permutation" where "Abs_G_perm g ≡ Abs_permutation (G_perm g)" abbreviation "𝔭 ≡ Abs_G_perm" ― ‹the injection into type @{type permutation}› abbreviation "𝔦𝔭 ≡ the_inv_into G 𝔭" ― ‹the reverse correspondence› abbreviation "pG ≡ 𝔭`G" ― ‹the resulting @{const Group} of type @{type permutation}› lemma G_perm_comp: "g∈G ⟹ h∈G ⟹ G_perm g ∘ G_perm h = G_perm (binop g h)" using closed by (auto simp add: assoc) definition the_inverse :: "'a ⇒ 'a" where "the_inverse g ≡ (THE h. h∈G ∧ binop g h = e ∧ binop h g = e)" abbreviation "𝔦 ≡ the_inverse" lemma the_inverseD: assumes "g∈G" shows "𝔦 g ∈ G" "binop g (𝔦 g) = e" "binop (𝔦 g) g = e" using assms theI'[OF unique_inverse] unfolding the_inverse_def by auto lemma binop_G_comp_binop_𝔦G: "g∈G ⟹ x∈G ⟹ binop g (binop (𝔦 g) x) = x" using the_inverseD(1) assoc[of g "𝔦 g" x] by (simp add: identity(3) the_inverseD(2)) lemma bij_betw_binop_G: assumes "g∈G" shows "bij_betw (binop g) G G" unfolding bij_betw_def proof show "inj_on (binop g) G" proof (rule inj_onI) fix h k assume hk: "h∈G" "k∈G" "binop g h = binop g k" with assms have "binop (binop (𝔦 g) g) h = binop (binop (𝔦 g) g) k" using the_inverseD(1) by (simp add: assoc) with assms hk(1,2) show "h=k" using the_inverseD(3) identity by simp qed show "binop g ` G = G" proof from assms show "binop g ` G ⊆ G" using closed by fast from assms show "binop g ` G ⊇ G" using binop_G_comp_binop_𝔦G[THEN sym] the_inverseD(1) closed by fast qed qed lemma the_inv_into_G_binop_G: assumes "g∈G" "x∈G" shows "the_inv_into G (binop g) x = binop (𝔦 g) x" proof (rule the_inv_into_f_eq) from assms(1) show "inj_on (binop g) G" using bij_betw_imp_inj_on[OF bij_betw_binop_G] by fast from assms show "binop g (binop (𝔦 g) x) = x" using binop_G_comp_binop_𝔦G by fast from assms show "binop (𝔦 g) x ∈ G" using closed the_inverseD(1) by fast qed lemma restrict1_the_inv_into_G_binop_G: "g∈G ⟹ restrict1 (the_inv_into G (binop g)) G = G_perm (𝔦 g)" using the_inv_into_G_binop_G by auto lemma bij_G_perm: "g∈G ⟹ bij (G_perm g)" using set_permutation_bij_restrict1 bij_betw_binop_G by fast lemma G_perm_apply: "g∈G ⟹ x∈G ⟹ 𝔭 g → x = binop g x" using Abs_G_perm_def Abs_permutation_inverse bij_G_perm by fastforce lemma G_perm_apply_identity: "g∈G ⟹ 𝔭 g → e = g" using G_perm_apply identity(1,2) by simp lemma the_inv_G_perm: "g∈G ⟹ the_inv (G_perm g) = G_perm (𝔦 g)" using set_permutation_the_inv_restrict1 bij_betw_binop_G restrict1_the_inv_into_G_binop_G by fastforce lemma Abs_G_perm_diff: "g∈G ⟹ h∈G ⟹ 𝔭 g - 𝔭 h = 𝔭 (binop g (𝔦 h))" using Abs_G_perm_def minus_permutation_abs_eq[OF bij_G_perm bij_G_perm] the_inv_G_perm G_perm_comp the_inverseD(1) by simp lemma Group: "Group pG" using identity(1) Abs_G_perm_diff the_inverseD(1) closed by unfold_locales auto lemma inj_on_𝔭_G: "inj_on 𝔭 G" proof (rule inj_onI) fix x y assume xy: "x∈G" "y∈G" "𝔭 x = 𝔭 y" hence "Abs_permutation (G_perm (binop x (𝔦 y))) = Abs_permutation id" using Abs_G_perm_diff Abs_G_perm_def by (fastforce simp add: zero_permutation.abs_eq) moreover from xy(1,2) have 1: "binop x (𝔦 y) ∈ G" using bij_id closed the_inverseD(1) by fast ultimately have 2: "G_perm (binop x (𝔦 y)) = id" using Abs_permutation_inject[of "G_perm (binop x (𝔦 y))"] bij_G_perm bij_id by simp have "∀z∈G. binop (binop x (𝔦 y)) z = z" proof fix z assume "z∈G" thus "binop (binop x (𝔦 y)) z = z" using fun_cong[OF 2, of z] by simp qed with xy(1,2) have "binop x (binop (𝔦 y) y) = y" using unique_identity1[OF 1] the_inverseD(1) by (simp add: assoc) with xy(1,2) show "x = y" using the_inverseD(3) identity(2) by simp qed lemma homs: "⋀g h. g∈G ⟹ h∈G ⟹ 𝔭 (binop g h) = 𝔭 g + 𝔭 h" "⋀x y. x∈pG ⟹ y∈pG ⟹ binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)" proof- show 1: "⋀g h. g∈G ⟹ h∈G ⟹ 𝔭 (binop g h) = 𝔭 g + 𝔭 h" using Abs_G_perm_def G_perm_comp plus_permutation_abs_eq[OF bij_G_perm bij_G_perm] by simp show "⋀x y. x∈pG ⟹ y∈pG ⟹ binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)" proof- fix x y assume "x∈pG" "y∈pG" moreover hence "𝔦𝔭 (𝔭 (binop (𝔦𝔭 x) (𝔦𝔭 y))) = 𝔦𝔭 (x + y)" using 1 the_inv_into_into[OF inj_on_𝔭_G] f_the_inv_into_f[OF inj_on_𝔭_G] by simp ultimately show "binop (𝔦𝔭 x) (𝔦𝔭 y) = 𝔦𝔭 (x+y)" using the_inv_into_into[OF inj_on_𝔭_G] closed the_inv_into_f_f[OF inj_on_𝔭_G] by simp qed qed lemmas inv_correspondence_into = the_inv_into_into[OF inj_on_𝔭_G, of _ G, simplified] lemma inv_correspondence_conv_apply: "x ∈ pG ⟹ 𝔦𝔭 x = x→e" using G_perm_apply_identity inj_on_𝔭_G by (auto intro: the_inv_into_f_eq) end (* context BinOpSetGroup *) subsubsection ‹Cosets of a @{const Group}› context Group begin lemma lcoset_refl: "a ∈ a +o G" using lcoset_refl zero_closed by fast lemma lcoset_el_reduce: assumes "a ∈ G" shows "a +o G = G" proof (rule seteqI) fix x assume "x ∈ a +o G" from this obtain g where "g∈G" "x = a+g" using elt_set_plus_def[of a] by auto with assms show "x∈G" by (simp add: add_closed) next fix x assume "x∈G" with assms have "-a + x ∈ G" by (simp add: uminus_add_closed) thus "x ∈ a +o G" using elt_set_plus_def by force qed lemma lcoset_el_reduce0: "0 ∈ a +o G ⟹ a +o G = G" using elt_set_plus_def[of a G] minus_unique uminus_closed[of "-a"] lcoset_el_reduce by fastforce lemma lcoset_subgroup_imp_eq_reps: "Group H ⟹ w +o H ⊆ w' +o G ⟹ w' +o G = w +o G" using Group.lcoset_refl[of H w] lcoset_conv_set[of w] lcoset_el_reduce set_plus_rearrange2[of w' "-w'+w" G] by force lemma lcoset_closed: "a∈G ⟹ A⊆G ⟹ a +o A ⊆ G" using elt_set_plus_def[of a] add_closed by auto lemma lcoset_rel_sym: "sym (lcoset_rel G)" proof (rule symI) fix a b show "(a,b) ∈ lcoset_rel G ⟹ (b,a) ∈ lcoset_rel G" using uminus_closed minus_add[of "-a" b] lcoset_rel_def[of G] by fastforce qed lemma lcoset_rel_trans: "trans (lcoset_rel G)" proof (rule transI) fix x y z assume xy: "(x,y) ∈ lcoset_rel G" and yz: "(y,z) ∈ lcoset_rel G" from this obtain g g' where "g∈G" "-x+y = g" "g'∈G" "-y+z = g'" using lcoset_rel_def[of G] by fast thus "(x, z) ∈ lcoset_rel G" using add.assoc[of g "-y" z] add_closed lcoset_rel_def[of G] by auto qed abbreviation LCoset_rel :: "'g set ⇒ ('g×'g) set" where "LCoset_rel H ≡ lcoset_rel H ∩ (G×G)" lemma refl_on_LCoset_rel: "0∈H ⟹ refl_on G (LCoset_rel H)" using lcoset_rel_def by (fastforce intro: refl_onI) lemmas subgroup_refl_on_LCoset_rel = refl_on_LCoset_rel[OF Group.zero_closed, OF SubgroupD1] lemmas LCoset_rel_quotientI = quotientI[of _ G "LCoset_rel _"] lemmas LCoset_rel_quotientE = quotientE[of _ G "LCoset_rel _"] lemma lcoset_subgroup_rel_equiv: "Subgroup H ⟹ equiv G (LCoset_rel H)" using Group.lcoset_rel_sym sym_sym sym_Int Group.lcoset_rel_trans trans_sym trans_Int subgroup_refl_on_LCoset_rel by (blast intro: equivI) lemma trivial_LCoset: "H⊆G ⟹ H = LCoset_rel H `` {0}" using zero_closed unfolding lcoset_rel_def by auto end (* context Group *) subsubsection ‹The @{const Group} generated by a set› inductive_set genby :: "'a::group_add set ⇒ 'a set" ("⟨_⟩") for S :: "'a set" where genby_0_closed : "0∈⟨S⟩" ― ‹just in case @{term S} is empty› | genby_genset_closed: "s∈S ⟹ s∈⟨S⟩" | genby_diff_closed : "w∈⟨S⟩ ⟹ w'∈⟨S⟩ ⟹ w - w' ∈ ⟨S⟩" lemma genby_Group: "Group ⟨S⟩" using genby_0_closed genby_diff_closed by unfold_locales fast lemmas genby_uminus_closed = Group.uminus_closed [OF genby_Group] lemmas genby_add_closed = Group.add_closed [OF genby_Group] lemmas genby_uminus_add_closed = Group.uminus_add_closed [OF genby_Group] lemmas genby_lcoset_refl = Group.lcoset_refl [OF genby_Group] lemmas genby_lcoset_el_reduce = Group.lcoset_el_reduce [OF genby_Group] lemmas genby_lcoset_el_reduce0 = Group.lcoset_el_reduce0 [OF genby_Group] lemmas genby_lcoset_closed = Group.lcoset_closed [OF genby_Group] lemmas genby_lcoset_subgroup_imp_eq_reps = Group.lcoset_subgroup_imp_eq_reps[OF genby_Group, OF genby_Group] lemma genby_genset_subset: "S ⊆ ⟨S⟩" using genby_genset_closed by fast lemma genby_uminus_genset_subset: "uminus ` S ⊆ ⟨S⟩" using genby_genset_subset genby_uminus_closed by auto lemma genby_in_sum_list_lists: fixes S defines S_sum_lists: "S_sum_lists ≡ (⋃ss∈lists (S ∪ uminus ` S). {sum_list ss})" shows "w ∈ ⟨S⟩ ⟹ w ∈ S_sum_lists" proof (erule genby.induct) have "0 = sum_list []" by simp with S_sum_lists show "0 ∈ S_sum_lists" by blast next fix s assume "s∈S" hence "[s] ∈ lists (S ∪ uminus ` S)" by simp moreover have "s = sum_list [s]" by simp ultimately show "s ∈ S_sum_lists" using S_sum_lists by blast next fix w w' assume ww': "w ∈ S_sum_lists" "w' ∈ S_sum_lists" with S_sum_lists obtain ss ts where ss: "ss ∈ lists (S ∪ uminus ` S)" "w = sum_list ss" and ts: "ts ∈ lists (S ∪ uminus ` S)" "w' = sum_list ts" by fastforce from ss(2) ts(2) have "w-w' = sum_list (ss @ map uminus (rev ts))" by (simp add: diff_conv_add_uminus uminus_sum_list) moreover from ss(1) ts(1) have "ss @ map uminus (rev ts) ∈ lists (S ∪ uminus ` S)" by fastforce ultimately show "w - w' ∈ S_sum_lists" using S_sum_lists by fast qed lemma sum_list_lists_in_genby: "ss ∈ lists (S ∪ uminus ` S) ⟹ sum_list ss ∈ ⟨S⟩" proof (induct ss) case Nil show ?case using genby_0_closed by simp next case (Cons s ss) thus ?case using genby_genset_subset[of S] genby_uminus_genset_subset genby_add_closed[of s S "sum_list ss"] by auto qed lemma sum_list_lists_in_genby_sym: "uminus ` S ⊆ S ⟹ ss ∈ lists S ⟹ sum_list ss ∈ ⟨S⟩" using sum_list_lists_in_genby by fast lemma genby_eq_sum_lists: "⟨S⟩ = (⋃ss∈lists (S ∪ uminus ` S). {sum_list ss})" using genby_in_sum_list_lists sum_list_lists_in_genby by fast lemma genby_mono: "T ⊆ S ⟹ ⟨T⟩ ⊆ ⟨S⟩" using genby_eq_sum_lists[of T] genby_eq_sum_lists[of S] by force lemma (in Group) genby_closed: assumes "S ⊆ G" shows "⟨S⟩ ⊆ G" proof fix x show "x ∈ ⟨S⟩ ⟹ x ∈ G" proof (erule genby.induct, rule zero_closed) from assms show "⋀s. s∈S ⟹ s∈G" by fast show "⋀w w'. w∈G ⟹ w'∈G ⟹ w-w' ∈ G" using diff_closed by fast qed qed lemma (in Group) genby_subgroup: "S ⊆ G ⟹ Subgroup ⟨S⟩" using genby_closed genby_Group by simp lemma genby_sym_eq_sum_lists: "uminus ` S ⊆ S ⟹ ⟨S⟩ = (⋃ss∈lists S. {sum_list ss})" using lists_mono genby_eq_sum_lists[of S] by force lemma genby_empty': "w ∈ ⟨{}⟩ ⟹ w = 0" proof (erule genby.induct) qed auto lemma genby_order2': assumes "s+s=0" shows "w ∈ ⟨{s}⟩ ⟹ w = 0 ∨ w = s" proof (erule genby.induct) fix w w' assume "w = 0 ∨ w = s" "w' = 0 ∨ w' = s" with assms show "w - w' = 0 ∨ w - w' = s" by (cases "w'=0") (auto simp add: minus_unique) qed auto lemma genby_order2: "s+s=0 ⟹ ⟨{s}⟩ = {0,s}" using genby_order2'[of s] genby_0_closed genby_genset_closed by auto lemma genby_empty: "⟨{}⟩ = 0" using genby_empty' genby_0_closed by auto lemma genby_lcoset_order2: "s+s=0 ⟹ w +o ⟨{s}⟩ = {w,w+s}" using elt_set_plus_def[of w] by (auto simp add: genby_order2) lemma genby_lcoset_empty: "(w::'a::group_add) +o ⟨{}⟩ = {w}" proof- have "⟨{}::'a set⟩ = (0::'a set)" using genby_empty by fast thus ?thesis using lcoset_0 by simp qed lemma (in Group) genby_set_lconjby_set_lconjby_closed: fixes A :: "'g set" defines "S ≡ (⋃g∈G. lconjby g ` A)" assumes "g∈G" shows "x ∈ ⟨S⟩ ⟹ lconjby g x ∈ ⟨S⟩" proof (erule genby.induct) show "lconjby g 0 ∈ ⟨S⟩" using genby_0_closed by simp from assms show "⋀s. s ∈ S ⟹ lconjby g s ∈ ⟨S⟩" using add_closed genby_genset_closed[of _ S] by (force simp add: lconjby_add) next fix w w' assume ww': "lconjby g w ∈ ⟨S⟩" "lconjby g w' ∈ ⟨S⟩" have "lconjby g (w - w') = lconjby g w + lconjby g (-w')" by (simp add: algebra_simps) with ww' show "lconjby g (w - w') ∈ ⟨S⟩" using lconjby_uminus[of g] diff_conv_add_uminus[of _ "lconjby g w'"] genby_diff_closed by fastforce qed lemma (in Group) genby_set_lconjby_set_rconjby_closed: fixes A :: "'g set" defines "S ≡ (⋃g∈G. lconjby g ` A)" assumes "g∈G" "x ∈ ⟨S⟩" shows "rconjby g x ∈ ⟨S⟩" using assms uminus_closed genby_set_lconjby_set_lconjby_closed by fastforce subsubsection ‹Homomorphisms and isomorphisms› locale GroupHom = Group G for G :: "'g::group_add set" + fixes T :: "'g ⇒ 'h::group_add" assumes hom : "g ∈ G ⟹ g' ∈ G ⟹ T (g + g') = T g + T g'" and supp: "supp T ⊆ G" begin lemma im_zero: "T 0 = 0" using zero_closed hom[of 0 0] add_diff_cancel[of "T 0" "T 0"] by simp lemma im_uminus: "T (- g) = - T g" using im_zero hom[of g "- g"] uminus_closed[of g] minus_unique[of "T g"] uminus_closed[of "-g"] supp suppI_contra[of g T] suppI_contra[of "-g" T] by fastforce lemma im_uminus_add: "g ∈ G ⟹ g' ∈ G ⟹ T (-g + g') = - T g + T g'" by (simp add: uminus_closed hom im_uminus) lemma im_diff: "g ∈ G ⟹ g' ∈ G ⟹ T (g - g') = T g - T g'" using hom uminus_closed hom[of g "-g'"] im_uminus by simp lemma im_lconjby: "x ∈ G ⟹ g ∈ G ⟹ T (lconjby x g) = lconjby (T x) (T g)" using add_closed by (simp add: im_diff hom) lemma im_sum_list_map: "set (map f as) ⊆ G ⟹ T (∑a←as. f a) = (∑a←as. T (f a))" using hom im_zero sum_list_closed by (induct as) auto lemma comp: assumes "GroupHom H S" "T`G ⊆ H" shows "GroupHom G (S ∘ T)" proof fix g g' assume "g ∈ G" "g' ∈ G" with hom assms(2) show "(S ∘ T) (g + g') = (S ∘ T) g + (S ∘ T) g'" using GroupHom.hom[OF assms(1)] by fastforce next from supp have "⋀g. g ∉ G ⟹ (S ∘ T) g = 0" using suppI_contra GroupHom.im_zero[OF assms(1)] by fastforce thus "supp (S ∘ T) ⊆ G" using suppD_contra by fast qed end (* context GroupHom *) definition ker :: "('a⇒'b::zero) ⇒ 'a set" where "ker f = {a. f a = 0}" lemma ker_subset_ker_restrict0: "ker f ⊆ ker (restrict0 f A)" unfolding ker_def by auto context GroupHom begin abbreviation "Ker ≡ ker T ∩ G" lemma uminus_add_in_Ker_eq_eq_im: "g∈G ⟹ h∈G ⟹ (-g + h ∈ Ker) = (T g = T h)" using neg_equal_iff_equal by (simp add: uminus_add_closed ker_def im_uminus_add eq_neg_iff_add_eq_0) end (* context GroupHom *) locale UGroupHom = GroupHom UNIV T for T :: "'g::group_add ⇒ 'h::group_add" begin lemmas im_zero = im_zero lemmas im_uminus = im_uminus lemma hom: "T (g+g') = T g + T g'" using hom by simp lemma im_diff: "T (g - g') = T g - T g'" using im_diff by simp lemma im_lconjby: "T (lconjby x g) = lconjby (T x) (T g)" using im_lconjby by simp lemma restrict0: assumes "Group G" shows "GroupHom G (restrict0 T G)" proof (intro_locales, rule assms, unfold_locales) from hom show "⋀g g'. g ∈ G ⟹ g' ∈ G ⟹ restrict0 T G (g + g') = restrict0 T G g + restrict0 T G g'" using Group.add_closed[OF assms] by auto show "supp (restrict0 T G) ⊆ G" using supp_restrict0[of G T] by fast qed end (* context UGroupHom *) lemma UGroupHomI: assumes "⋀g g'. T (g + g') = T g + T g'" shows "UGroupHom T" using assms by unfold_locales auto locale GroupIso = GroupHom G T for G :: "'g::group_add set" and T :: "'g ⇒ 'h::group_add" + assumes inj_on: "inj_on T G" lemma (in GroupHom) isoI: assumes "⋀k. k∈G ⟹ T k = 0 ⟹ k=0" shows "GroupIso G T" proof (unfold_locales, rule inj_onI) fix x y from assms show "⟦ x∈G; y∈G; T x = T y ⟧ ⟹ x = y" using im_diff diff_closed by force qed text ‹ In a @{const BinOpSetGroup}, any map from the set into a type of class @{class group_add} that respects the binary operation induces a @{const GroupHom}. › abbreviation (in BinOpSetGroup) "lift_hom T ≡ restrict0 (T ∘ 𝔦𝔭) pG" lemma (in BinOpSetGroup) lift_hom: fixes T :: "'a ⇒ 'b::group_add" assumes "∀g∈G. ∀h∈G. T (binop g h) = T g + T h" shows "GroupHom pG (lift_hom T)" proof (intro_locales, rule Group, unfold_locales) from assms show "⋀x y. x∈pG ⟹ y∈pG ⟹ lift_hom T (x+y) = lift_hom T x + lift_hom T y" using Group.add_closed[OF Group] inv_correspondence_into by (simp add: homs(2)[THEN sym]) qed (rule supp_restrict0) subsubsection ‹Normal subgroups› definition rcoset_rel :: "'a::{minus,plus} set ⇒ ('a×'a) set" where "rcoset_rel A ≡ {(x,y). x-y ∈ A}" context Group begin lemma rcoset_rel_conv_lcoset_rel: "rcoset_rel G = map_prod uminus uminus ` (lcoset_rel G)" proof (rule set_eqI) fix x :: "'g×'g" obtain a b where ab: "x=(a,b)" by fastforce hence "(x ∈ rcoset_rel G) = (a-b ∈ G)" using rcoset_rel_def by auto also have "… = ( (-b,-a) ∈ lcoset_rel G )" using uminus_closed lcoset_rel_def by fastforce finally show "(x ∈ rcoset_rel G) = (x ∈ map_prod uminus uminus ` (lcoset_rel G))" using ab symD[OF lcoset_rel_sym] map_prod_def by force qed lemma rcoset_rel_sym: "sym (rcoset_rel G)" using rcoset_rel_conv_lcoset_rel map_prod_sym lcoset_rel_sym by simp abbreviation RCoset_rel :: "'g set ⇒ ('g×'g) set" where "RCoset_rel H ≡ rcoset_rel H ∩ (G×G)" definition normal :: "'g set ⇒ bool" where "normal H ≡ (∀g∈G. LCoset_rel H `` {g} = RCoset_rel H `` {g})" lemma normalI: assumes "Group H" "∀g∈G. ∀h∈H. ∃h'∈H. g+h = h'+g" "∀g∈G. ∀h∈H. ∃h'∈H. h+g = g+h'" shows "normal H" unfolding normal_def proof fix g assume g: "g∈G" show "LCoset_rel H `` {g} = RCoset_rel H `` {g}" proof (rule seteqI) fix x assume "x ∈ LCoset_rel H `` {g}" with g have x: "x∈G" "-g+x ∈ H" unfolding lcoset_rel_def by auto from g x(2) assms(2) obtain h where h: "h∈H" "g-x = -h" by (fastforce simp add: algebra_simps) with assms(1) g x(1) show "x ∈ RCoset_rel H `` {g}" using Group.uminus_closed unfolding rcoset_rel_def by simp next fix x assume "x ∈ RCoset_rel H `` {g}" with g have x: "x∈G" "g-x ∈ H" unfolding rcoset_rel_def by auto with assms(3) obtain h where h: "h∈H" "-g+x = -h" by (fastforce simp add: algebra_simps minus_add) with assms(1) g x(1) show "x ∈ LCoset_rel H `` {g}" using Group.uminus_closed unfolding lcoset_rel_def by simp qed qed lemma normal_lconjby_closed: "⟦ Subgroup H; normal H; g∈G; h∈H ⟧ ⟹ lconjby g h ∈ H" using lcoset_relI[of g "g+h" H] add_closed[of g h] normal_def[of H] symD[OF Group.rcoset_rel_sym, of H g "g+h"] rcoset_rel_def[of H] by auto lemma normal_rconjby_closed: "⟦ Subgroup H; normal H; g∈G; h∈H ⟧ ⟹ rconjby g h ∈ H" using normal_lconjby_closed[of H "-g" h] uminus_closed[of g] by auto abbreviation "normal_closure A ≡ ⟨⋃g∈G. lconjby g ` A⟩" lemma (in Group) normal_closure: assumes "A⊆G" shows "normal (normal_closure A)" proof (rule normalI, rule genby_Group) show "∀x∈G. ∀h∈⟨⋃g∈G. lconjby g ` A⟩. ∃h'∈⟨⋃g∈G. lconjby g ` A⟩. x + h = h' + x" proof fix x assume x: "x∈G" show "∀h∈⟨⋃g∈G. lconjby g ` A⟩. ∃h'∈⟨⋃g∈G. lconjby g ` A⟩. x + h = h' + x" proof (rule ballI, erule genby.induct) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. x + 0 = h + x" using genby_0_closed by force next fix s assume "s ∈ (⋃g∈G. lconjby g ` A)" from this obtain g a where ga: "g∈G" "a∈A" "s = lconjby g a" by fast from ga(3) have "x + s = lconjby x (lconjby g a) + x" by (simp add: algebra_simps) hence "x + s = lconjby (x+g) a + x" by (simp add: lconjby_add) with x ga(1,2) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. x + s = h + x" using add_closed by (blast intro: genby_genset_closed) next fix w w' assume w : "w ∈ ⟨⋃g∈G. lconjby g ` A⟩" "∃h ∈⟨⋃g∈G. lconjby g ` A⟩. x + w = h + x" and w': "w'∈ ⟨⋃g∈G. lconjby g ` A⟩" "∃h'∈⟨⋃g∈G. lconjby g ` A⟩. x + w' = h'+ x" from w(2) w'(2) obtain h h' where h : "h ∈ ⟨⋃g∈G. lconjby g ` A⟩" "x + w = h + x" and h': "h'∈ ⟨⋃g∈G. lconjby g ` A⟩" "x + w' = h'+ x" by fast have "x + (w - w') = x + w - (-x + (x + w'))" by (simp add: algebra_simps) also from h(2) h'(2) have "… = h + x + (-(h' + x) + x)" by (simp add: algebra_simps) also have "… = h + x + (-x + -h') + x" by (simp add: minus_add add.assoc) finally have "x + (w-w') = h - h' + x" using add.assoc[of "h+x" "-x" "-h'"] by simp with h(1) h'(1) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. x + (w - w') = h + x" using genby_diff_closed by fast qed qed show "∀x∈G. ∀h∈⟨⋃g∈G. lconjby g ` A⟩. ∃h'∈⟨⋃g∈G. lconjby g ` A⟩. h + x = x + h'" proof fix x assume x: "x∈G" show "∀h∈⟨⋃g∈G. lconjby g ` A⟩. ∃h'∈⟨⋃g∈G. lconjby g ` A⟩. h + x = x + h'" proof (rule ballI, erule genby.induct) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. 0 + x = x + h" using genby_0_closed by force next fix s assume "s ∈ (⋃g∈G. lconjby g ` A)" from this obtain g a where ga: "g∈G" "a∈A" "s = lconjby g a" by fast from ga(3) have "s + x = x + (((-x + g) + a) + -g) + x" by (simp add: algebra_simps) also have "… = x + (-x + g + a + -g + x)" by (simp add: add.assoc) finally have "s + x = x + lconjby (-x+g) a" by (simp add: algebra_simps lconjby_add) with x ga(1,2) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. s + x = x + h" using uminus_add_closed by (blast intro: genby_genset_closed) next fix w w' assume w : "w ∈ ⟨⋃g∈G. lconjby g ` A⟩" "∃h ∈⟨⋃g∈G. lconjby g ` A⟩. w + x = x + h" and w': "w'∈ ⟨⋃g∈G. lconjby g ` A⟩" "∃h'∈⟨⋃g∈G. lconjby g ` A⟩. w' + x = x + h'" from w(2) w'(2) obtain h h' where h : "h ∈ ⟨⋃g∈G. lconjby g ` A⟩" "w + x = x + h" and h': "h'∈ ⟨⋃g∈G. lconjby g ` A⟩" "w' + x = x + h'" by fast have "w - w' + x = w + x + (-x + -w') + x" by (simp add: algebra_simps) also from h(2) h'(2) have "… = x + h + (-h'+-x) + x" using minus_add[of w' x] minus_add[of x h'] by simp finally have "w - w' + x = x + (h - h')" by (simp add: algebra_simps) with h(1) h'(1) show "∃h∈⟨⋃g∈G. lconjby g ` A⟩. w - w' + x = x + h" using genby_diff_closed by fast qed qed qed end (* context Group *) subsubsection ‹Quotient groups› text ‹ Here we use the bridge built by @{const BinOpSetGroup} to make the quotient of a @{const Group} by a normal subgroup into a @{const Group} itself. › context Group begin lemma normal_quotient_add_well_defined: assumes "Subgroup H" "normal H" "g∈G" "g'∈G" shows "LCoset_rel H `` {g} + LCoset_rel H `` {g'} = LCoset_rel H `` {g+g'}" proof (rule seteqI) fix x assume "x ∈ LCoset_rel H `` {g} + LCoset_rel H `` {g'}" from this obtain y z where "y ∈ LCoset_rel H `` {g}" "z ∈ LCoset_rel H `` {g'}" "x = y+z" unfolding set_plus_def by fast with assms show "x ∈ LCoset_rel H `` {g + g'}" using lcoset_rel_def[of H] normal_lconjby_closed[of H g' "-g'+z"] Group.add_closed normal_rconjby_closed[of H g' "-g + y + (z - g')"] add.assoc[of "-g'" "-g"] add_closed lcoset_relI[of "g+g'" "y+z"] by (fastforce simp add: add.assoc minus_add) next fix x assume "x ∈ LCoset_rel H `` {g + g'}" moreover define h where "h ≡ -(g+g') + x" moreover hence "x = g + (g' + h)" using add.assoc[of "-g'" "-g" x] by (simp add: add.assoc minus_add) ultimately show "x ∈ LCoset_rel H `` {g} + LCoset_rel H `` {g'}" using assms(1,3,4) lcoset_rel_def[of H] add_closed refl_onD[OF subgroup_refl_on_LCoset_rel, of H] by force qed abbreviation "quotient_set H ≡ G // LCoset_rel H" lemma BinOpSetGroup_normal_quotient: assumes "Subgroup H" "normal H" shows "BinOpSetGroup (quotient_set H) (+) H" proof from assms(1) have H0: "H = LCoset_rel H `` {0}" using trivial_LCoset by auto from assms(1) show "H ∈ quotient_set H" using H0 zero_closed LCoset_rel_quotientI[of 0 H] by simp fix x assume "x ∈ quotient_set H" from this obtain gx where gx: "gx∈G" "x = LCoset_rel H `` {gx}" by (fast elim: LCoset_rel_quotientE) with assms(1,2) show "x+H = x" "H+x = x" using normal_quotient_add_well_defined[of H gx 0] normal_quotient_add_well_defined[of H 0 gx] H0 zero_closed by auto from gx(1) have "LCoset_rel H `` {-gx} ∈ quotient_set H" using uminus_closed by (fast intro: LCoset_rel_quotientI) moreover from assms(1,2) gx have "x + LCoset_rel H `` {-gx} = H" "LCoset_rel H `` {-gx} + x = H" using H0 uminus_closed normal_quotient_add_well_defined by auto ultimately show "∃x'∈quotient_set H. x + x' = H ∧ x' + x = H" by fast fix y assume "y ∈ quotient_set H" from this obtain gy where gy: "gy∈G" "y = LCoset_rel H `` {gy}" by (fast elim: LCoset_rel_quotientE) with assms gx show "x+y ∈ quotient_set H" using add_closed normal_quotient_add_well_defined by (auto intro: LCoset_rel_quotientI) qed (rule add.assoc) abbreviation "abs_lcoset_perm H ≡ BinOpSetGroup.Abs_G_perm (quotient_set H) (+)" abbreviation "abs_lcoset_perm_lift H g ≡ abs_lcoset_perm H (LCoset_rel H `` {g})" abbreviation "abs_lcoset_perm_lift_arg_permutation g H ≡ abs_lcoset_perm_lift H g" notation abs_lcoset_perm_lift_arg_permutation ("⌈_|_⌉" [51,51] 50) end (* context Group *) abbreviation "Group_abs_lcoset_perm_lift_arg_permutation G' g H ≡ Group.abs_lcoset_perm_lift_arg_permutation G' g H" notation Group_abs_lcoset_perm_lift_arg_permutation ("⌈_|_|_⌉" [51,51,51] 50) context Group begin lemmas lcoset_perm_def = BinOpSetGroup.Abs_G_perm_def[OF BinOpSetGroup_normal_quotient] lemmas lcoset_perm_comp = BinOpSetGroup.G_perm_comp[OF BinOpSetGroup_normal_quotient] lemmas bij_lcoset_perm = BinOpSetGroup.bij_G_perm[OF BinOpSetGroup_normal_quotient] lemma trivial_lcoset_perm: assumes "Subgroup H" "normal H" "h∈H" shows "restrict1 ((+) (LCoset_rel H `` {h})) (quotient_set H) = id" proof (rule ext, simp, rule impI) fix x assume x: "x ∈ quotient_set H" then obtain k where k: "k∈G" "x = LCoset_rel H `` {k}" by (blast elim: LCoset_rel_quotientE) with x have "LCoset_rel H `` {h} + x = LCoset_rel H `` {h+k}" using assms normal_quotient_add_well_defined by auto with assms k show "LCoset_rel H `` {h} + x = x" using add_closed[of h k] lcoset_relI[of k "h+k" H] normal_rconjby_closed[of H k h] eq_equiv_class_iff[OF lcoset_subgroup_rel_equiv, of H] by (auto simp add: add.assoc) qed definition quotient_group :: "'g set ⇒ 'g set permutation set" where "quotient_group H ≡ BinOpSetGroup.pG (quotient_set H) (+)" abbreviation "natural_quotient_hom H ≡ restrict0 (λg. ⌈g|H⌉) G" theorem quotient_group: "Subgroup H ⟹ normal H ⟹ Group (quotient_group H)" unfolding quotient_group_def using BinOpSetGroup.Group[OF BinOpSetGroup_normal_quotient] by auto lemma natural_quotient_hom: "Subgroup H ⟹ normal H ⟹ GroupHom G (natural_quotient_hom H)" using add_closed bij_lcoset_perm lcoset_perm_def supp_restrict0 normal_quotient_add_well_defined[THEN sym] LCoset_rel_quotientI[of _ H] by unfold_locales (force simp add: lcoset_perm_comp plus_permutation_abs_eq) lemma natural_quotient_hom_image: "natural_quotient_hom H ` G = quotient_group H" unfolding quotient_group_def by (force elim: LCoset_rel_quotientE intro: LCoset_rel_quotientI) lemma quotient_group_UN: "quotient_group H = (λg. ⌈g|H⌉) ` G" using natural_quotient_hom_image by auto lemma quotient_identity_rule: "⟦ Subgroup H; normal H; h∈H ⟧ ⟹ ⌈h|H⌉ = 0" using lcoset_perm_def by (simp add: trivial_lcoset_perm zero_permutation.abs_eq) lemma quotient_group_lift_to_quotient_set: "⟦ Subgroup H; normal H; g∈G ⟧ ⟹ (⌈g|H⌉) → H = LCoset_rel H `` {g}" using LCoset_rel_quotientI BinOpSetGroup.G_perm_apply_identity[ OF BinOpSetGroup_normal_quotient ] by simp end (* context Group *) subsubsection ‹The induced homomorphism on a quotient group› text ‹ A normal subgroup contained in the kernel of a homomorphism gives rise to a homomorphism on the quotient group by that subgroup. When the subgroup is the kernel itself (which is always normal), we obtain an isomorphism on the quotient. › context GroupHom begin lemma respects_Ker_lcosets: "H ⊆ Ker ⟹ T respects (LCoset_rel H)" using uminus_add_in_Ker_eq_eq_im unfolding lcoset_rel_def by (blast intro: congruentI) abbreviation "quotient_hom H ≡ BinOpSetGroup.lift_hom (quotient_set H) (+) (quotientfun T)" lemmas normal_subgroup_quotientfun_classrep_equality = quotientfun_classrep_equality[ OF subgroup_refl_on_LCoset_rel, OF _ respects_Ker_lcosets ] lemma quotient_hom_im: "⟦ Subgroup H; normal H; H ⊆ Ker; g∈G ⟧ ⟹ quotient_hom H (⌈g|H⌉) = T g" using quotient_group_def quotient_group_UN quotient_group_lift_to_quotient_set BinOpSetGroup.inv_correspondence_conv_apply[ OF BinOpSetGroup_normal_quotient ] normal_subgroup_quotientfun_classrep_equality by auto lemma quotient_hom: assumes "Subgroup H" "normal H" "H ⊆ Ker" shows "GroupHom (quotient_group H) (quotient_hom H)" unfolding quotient_group_def proof ( rule BinOpSetGroup.lift_hom, rule BinOpSetGroup_normal_quotient, rule assms(1), rule assms(2) ) from assms show "∀x ∈ quotient_set H. ∀y ∈ quotient_set H. quotientfun T (x + y) = quotientfun T x + quotientfun T y" using normal_quotient_add_well_defined normal_subgroup_quotientfun_classrep_equality add_closed hom by (fastforce elim: LCoset_rel_quotientE) qed end (* context GroupHom *) subsection ‹Free groups› subsubsection ‹Words in letters of @{type signed} type› paragraph ‹Definitions and basic fact› text ‹ We pair elements of some type with type @{typ bool}, where the @{typ bool} part of the pair indicates inversion. › abbreviation "pairtrue ≡ λs. (s,True)" abbreviation "pairfalse ≡ λs. (s,False)" abbreviation flip_signed :: "'a signed ⇒ 'a signed" where "flip_signed ≡ apsnd (λb. ¬b)" abbreviation nflipped_signed :: "'a signed ⇒ 'a signed ⇒ bool" where "nflipped_signed x y ≡ y ≠ flip_signed x" lemma flip_signed_order2: "flip_signed (flip_signed x) = x" using apsnd_conv[of "λb. ¬b" "fst x" "snd x"] by simp abbreviation charpair :: "'a::uminus set ⇒ 'a ⇒ 'a signed" where "charpair S s ≡ if s∈S then (s,True) else (-s,False)" lemma map_charpair_uniform: "ss∈lists S ⟹ map (charpair S) ss = map pairtrue ss" by (induct ss) auto lemma fst_set_map_charpair_un_uminus: fixes ss :: "'a::group_add list" shows "ss∈lists (S ∪ uminus ` S) ⟹ fst ` set (map (charpair S) ss) ⊆ S" by (induct ss) auto abbreviation apply_sign :: "('a⇒'b::uminus) ⇒ 'a signed ⇒ 'b" where "apply_sign f x ≡ (if snd x then f (fst x) else - f (fst x))" text ‹ A word in such pairs will be considered proper if it does not contain consecutive letters that have opposite signs (and so are considered inverse), since such consecutive letters would be cancelled in a group. › abbreviation proper_signed_list :: "'a signed list ⇒ bool" where "proper_signed_list ≡ binrelchain nflipped_signed" lemma proper_map_flip_signed: "proper_signed_list xs ⟹ proper_signed_list (map flip_signed xs)" by (induct xs rule: list_induct_CCons) auto lemma proper_rev_map_flip_signed: "proper_signed_list xs ⟹ proper_signed_list (rev (map flip_signed xs))" using proper_map_flip_signed binrelchain_sym_rev[of nflipped_signed] by fastforce lemma uniform_snd_imp_proper_signed_list: "snd ` set xs ⊆ {b} ⟹ proper_signed_list xs" proof (induct xs rule: list_induct_CCons) case CCons thus ?case by force qed auto lemma proper_signed_list_map_uniform_snd: "proper_signed_list (map (λs. (s,b)) as)" using uniform_snd_imp_proper_signed_list[of _ b] by force paragraph ‹Algebra› text ‹ Addition is performed by appending words and recursively removing any newly created adjacent pairs of inverse letters. Since we will only ever be adding proper words, we only need to care about newly created adjacent inverse pairs in the middle. › function prappend_signed_list :: "'a signed list ⇒ 'a signed list ⇒ 'a signed list" where "prappend_signed_list xs [] = xs" | "prappend_signed_list [] ys = ys" | "prappend_signed_list (xs@[x]) (y#ys) = ( if y = flip_signed x then prappend_signed_list xs ys else xs @ x # y # ys )" by (auto) (rule two_prod_lists_cases_snoc_Cons) termination by (relation "measure (λ(xs,ys). length xs + length ys)") auto lemma proper_prappend_signed_list: "proper_signed_list xs ⟹ proper_signed_list ys ⟹ proper_signed_list (prappend_signed_list xs ys)" proof (induct xs ys rule: list_induct2_snoc_Cons) case (snoc_Cons xs x y ys) show ?case proof (cases "y = flip_signed x") case True with snoc_Cons show ?thesis using binrelchain_append_reduce1[of nflipped_signed] binrelchain_Cons_reduce[of nflipped_signed y] by auto next case False with snoc_Cons(2,3) show ?thesis using binrelchain_join[of nflipped_signed] by simp qed qed auto lemma fully_prappend_signed_list: "prappend_signed_list (rev (map flip_signed xs)) xs = []" by (induct xs) auto lemma prappend_signed_list_single_Cons: "prappend_signed_list [x] (y#ys) = (if y = flip_signed x then ys else x#y#ys)" using prappend_signed_list.simps(3)[of "[]" x] by simp lemma prappend_signed_list_map_uniform_snd: "prappend_signed_list (map (λs. (s,b)) xs) (map (λs. (s,b)) ys) = map (λs. (s,b)) xs @ map (λs. (s,b)) ys" by (cases xs ys rule: two_lists_cases_snoc_Cons) auto lemma prappend_signed_list_assoc_conv_snoc2Cons: assumes "proper_signed_list (xs@[y])" "proper_signed_list (y#ys)" shows "prappend_signed_list (xs@[y]) ys = prappend_signed_list xs (y#ys)" proof (cases xs ys rule: two_lists_cases_snoc_Cons') case Nil1 with assms(2) show ?thesis by (simp add: prappend_signed_list_single_Cons) next case Nil2 with assms(1) show ?thesis using binrelchain_append_reduce2 by force next case (snoc_Cons as a b bs) with assms show ?thesis using prappend_signed_list.simps(3)[of "as@[a]"] binrelchain_append_reduce2[of nflipped_signed as "[a,y]"] by simp qed simp lemma prappend_signed_list_assoc: "⟦ proper_signed_list xs; proper_signed_list ys; proper_signed_list zs ⟧ ⟹ prappend_signed_list (prappend_signed_list xs ys) zs = prappend_signed_list xs (prappend_signed_list ys zs)" proof (induct xs ys zs rule: list_induct3_snoc_Conssnoc_Cons_pairwise) case (snoc_single_Cons xs x y z zs) thus ?case using prappend_signed_list.simps(3)[of "[]" y] prappend_signed_list.simps(3)[of "xs@[x]"] by (cases "y = flip_signed x" "z = flip_signed y" rule: two_cases) (auto simp add: flip_signed_order2 prappend_signed_list_assoc_conv_snoc2Cons ) next case (snoc_Conssnoc_Cons xs x y ys w z zs) thus ?case using binrelchain_Cons_reduce[of nflipped_signed y "ys@[w]"] binrelchain_Cons_reduce[of nflipped_signed z zs] binrelchain_append_reduce1[of nflipped_signed xs] binrelchain_append_reduce1[of nflipped_signed "y#ys"] binrelchain_Conssnoc_reduce[of nflipped_signed y ys] prappend_signed_list.simps(3)[of "y#ys"] prappend_signed_list.simps(3)[of "xs@x#y#ys"] by (cases "y = flip_signed x" "z = flip_signed w" rule: two_cases) auto qed auto lemma fst_set_prappend_signed_list: "fst ` set (prappend_signed_list xs ys) ⊆ fst ` (set xs ∪ set ys)" by (induct xs ys rule: list_induct2_snoc_Cons) auto lemma collapse_flipped_signed: "prappend_signed_list [(s,b)] [(s,¬b)] = []" using prappend_signed_list.simps(3)[of "[]" "(s,b)"] by simp subsubsection ‹The collection of proper signed lists as a type› text ‹ Here we create a type out of the collection of proper signed lists. This type will be of class @{class group_add}, with the empty list as zero, the modified append operation @{const prappend_signed_list} as addition, and inversion performed by flipping the signs of the elements in the list and then reversing the order. › paragraph ‹Type definition, instantiations, and instances› text ‹Here we define the type and instantiate it with respect to various type classes.› typedef 'a freeword = "{as::'a signed list. proper_signed_list as}" morphisms freeword Abs_freeword using binrelchain.simps(1) by fast text ‹ These two functions act as the natural injections of letters and words in the letter type into the @{type freeword} type. › abbreviation Abs_freeletter :: "'a ⇒ 'a freeword" where "Abs_freeletter s ≡ Abs_freeword [pairtrue s]" abbreviation Abs_freelist :: "'a list ⇒ 'a freeword" where "Abs_freelist as ≡ Abs_freeword (map pairtrue as)" abbreviation Abs_freelistfst :: "'a signed list ⇒ 'a freeword" where "Abs_freelistfst xs ≡ Abs_freelist (map fst xs)" setup_lifting type_definition_freeword instantiation freeword :: (type) zero begin lift_definition zero_freeword :: "'a freeword" is "[]::'a signed list" by simp instance .. end instantiation freeword :: (type) plus begin lift_definition plus_freeword :: "'a freeword ⇒ 'a freeword ⇒ 'a freeword" is "prappend_signed_list" using proper_prappend_signed_list by fast instance .. end instantiation freeword :: (type) uminus begin lift_definition uminus_freeword :: "'a freeword ⇒ 'a freeword" is "λxs. rev (map flip_signed xs)" by (rule proper_rev_map_flip_signed) instance .. end instantiation freeword :: (type) minus begin lift_definition minus_freeword :: "'a freeword ⇒ 'a freeword ⇒ 'a freeword" is "λxs ys. prappend_signed_list xs (rev (map flip_signed ys))" using proper_rev_map_flip_signed proper_prappend_signed_list by fast instance .. end instance freeword :: (type) semigroup_add proof fix a b c :: "'a freeword" show "a + b + c = a + (b + c)" using prappend_signed_list_assoc[of "freeword a" "freeword b" "freeword c"] by transfer simp qed instance freeword :: (type) monoid_add proof fix a b c :: "'a freeword" show "0 + a = a" by transfer simp show "a + 0 = a" by transfer simp qed instance freeword :: (type) group_add proof fix a b :: "'a freeword" show "- a + a = 0" using fully_prappend_signed_list[of "freeword a"] by transfer simp show "a + - b = a - b" by transfer simp qed paragraph ‹Basic algebra and transfer facts in the @{type freeword} type› text ‹ Here we record basic algebraic manipulations for the @{type freeword} type as well as various transfer facts for dealing with representations of elements of @{type freeword} type as lists of signed letters. › abbreviation Abs_freeletter_add :: "'a ⇒ 'a ⇒ 'a freeword" (infixl "[+]" 65) where "s [+] t ≡ Abs_freeletter s + Abs_freeletter t" lemma Abs_freeword_Cons: assumes "proper_signed_list (x#xs)" shows "Abs_freeword (x#xs) = Abs_freeword [x] + Abs_freeword xs" proof (cases xs) case Nil thus ?thesis using add_0_right[of "Abs_freeword [x]"] by (simp add: zero_freeword.abs_eq) next case (Cons y ys) with assms have "freeword (Abs_freeword (x#xs)) = freeword (Abs_freeword [x] + Abs_freeword xs)" by (simp add: plus_freeword.rep_eq Abs_freeword_inverse prappend_signed_list_single_Cons ) thus ?thesis using freeword_inject by fast qed lemma Abs_freelist_Cons: "Abs_freelist (x#xs) = Abs_freeletter x + Abs_freelist xs" using proper_signed_list_map_uniform_snd[of True "x#xs"] Abs_freeword_Cons by simp lemma plus_freeword_abs_eq: "proper_signed_list xs ⟹ proper_signed_list ys ⟹ Abs_freeword xs + Abs_freeword ys = Abs_freeword (prappend_signed_list xs ys)" using plus_freeword.abs_eq unfolding eq_onp_def by simp lemma Abs_freeletter_add: "s [+] t = Abs_freelist [s,t]" using Abs_freelist_Cons[of s "[t]"] by simp lemma uminus_freeword_Abs_eq: "proper_signed_list xs ⟹ - Abs_freeword xs = Abs_freeword (rev (map flip_signed xs))" using uminus_freeword.abs_eq unfolding eq_onp_def by simp lemma uminus_Abs_freeword_singleton: "- Abs_freeword [(s,b)] = Abs_freeword [(s,¬ b)]" using uminus_freeword_Abs_eq[of "[(s,b)]"] by simp lemma Abs_freeword_append_uniform_snd: "Abs_freeword (map (λs. (s,b)) (xs@ys)) = Abs_freeword (map (λs. (s,b)) xs) + Abs_freeword (map (λs. (s,b)) ys)" using proper_signed_list_map_uniform_snd[of b xs] proper_signed_list_map_uniform_snd[of b ys] plus_freeword_abs_eq prappend_signed_list_map_uniform_snd[of b xs ys] by force lemmas Abs_freelist_append = Abs_freeword_append_uniform_snd[of True] lemma Abs_freelist_append_append: "Abs_freelist (xs@ys@zs) = Abs_freelist xs + Abs_freelist ys + Abs_freelist zs" using Abs_freelist_append[of "xs@ys"] Abs_freelist_append by simp lemma Abs_freelist_inverse: "freeword (Abs_freelist as) = map pairtrue as" using proper_signed_list_map_uniform_snd Abs_freeword_inverse by fast lemma Abs_freeword_singleton_conv_apply_sign_freeletter: "Abs_freeword [x] = apply_sign Abs_freeletter x" by (cases x) (auto simp add: uminus_Abs_freeword_singleton) lemma Abs_freeword_conv_freeletter_sum_list: "proper_signed_list xs ⟹ Abs_freeword xs = (∑x←xs. apply_sign Abs_freeletter x)" proof (induct xs) case (Cons x xs) thus ?case using Abs_freeword_Cons[of x] binrelchain_Cons_reduce[of _ x] by (simp add: Abs_freeword_singleton_conv_apply_sign_freeletter) qed (simp add: zero_freeword.abs_eq) lemma freeword_conv_freeletter_sum_list: "x = (∑s←freeword x. apply_sign Abs_freeletter s)" using Abs_freeword_conv_freeletter_sum_list[of "freeword x"] freeword by (auto simp add: freeword_inverse) lemma Abs_freeletter_prod_conv_Abs_freeword: "snd x ⟹ Abs_freeletter (fst x) = Abs_freeword [x]" using prod_eqI[of x "pairtrue (fst x)"] by simp subsubsection ‹Lifts of functions on the letter type› text ‹ Here we lift functions on the letter type to type @{type freeword}. In particular, we are interested in the case where the function being lifted has codomain of class @{class group_add}. › paragraph ‹The universal property› text ‹ The universal property for free groups says that every function from the letter type to some @{class group_add} type gives rise to a unique homomorphism. › lemma extend_map_to_freeword_hom': fixes f :: "'a ⇒ 'b::group_add" defines h: "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)" defines g: "g::'a signed list ⇒ 'b ≡ λxs. sum_list (map h xs)" shows "g (prappend_signed_list xs ys) = g xs + g ys" proof (induct xs ys rule: list_induct2_snoc_Cons) case (snoc_Cons xs x y ys) show ?case proof (cases "y = flip_signed x") case True with h have "h y = - h x" using split_beta'[of "λs b. if b then f s else - (f s)"] by simp with g have "g (xs @ [x]) + g (y # ys) = g xs + g ys" by (simp add: algebra_simps) with True snoc_Cons show ?thesis by simp next case False with g show ?thesis using sum_list.append[of "map h (xs@[x])" "map h (y#ys)"] by simp qed qed (auto simp add: h g) lemma extend_map_to_freeword_hom1: fixes f :: "'a ⇒ 'b::group_add" defines "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)" defines "g::'a freeword ⇒ 'b ≡ λx. sum_list (map h (freeword x))" shows "g (Abs_freeletter s) = f s" using assms by (simp add: Abs_freeword_inverse) lemma extend_map_to_freeword_hom2: fixes f :: "'a ⇒ 'b::group_add" defines "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)" defines "g::'a freeword ⇒ 'b ≡ λx. sum_list (map h (freeword x))" shows "UGroupHom g" using assms by ( auto intro: UGroupHomI simp add: plus_freeword.rep_eq extend_map_to_freeword_hom' ) lemma uniqueness_of_extended_map_to_freeword_hom': fixes f :: "'a ⇒ 'b::group_add" defines h: "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)" defines g: "g::'a signed list ⇒ 'b ≡ λxs. sum_list (map h xs)" assumes singles: "⋀s. k [(s,True)] = f s" and adds : "⋀xs ys. proper_signed_list xs ⟹ proper_signed_list ys ⟹ k (prappend_signed_list xs ys) = k xs + k ys" shows "proper_signed_list xs ⟹ k xs = g xs" proof- have knil: "k [] = 0" using adds[of "[]" "[]"] add.assoc[of "k []" "k []" "- k []"] by simp have ksingle: "⋀x. k [x] = g [x]" proof- fix x :: "'a signed" obtain s b where x: "x = (s,b)" by fastforce show "k [x] = g [x]" proof (cases b) case False from adds x singles have "k (prappend_signed_list [x] [(s,True)]) = k [x] + f s" by simp moreover have "prappend_signed_list [(s,False)] [(s,True)] = []" using collapse_flipped_signed[of s False] by simp ultimately have "- f s = k [x] + f s + - f s" using x False knil by simp with x False g h show "k [x] = g [x]" by (simp add: algebra_simps) qed (simp add: x g h singles) qed show "proper_signed_list xs ⟹ k xs = g xs" proof (induct xs rule: list_induct_CCons) case (CCons x y xs) with g h show ?case using adds[of "[x]" "y#xs"] by (simp add: prappend_signed_list_single_Cons ksingle extend_map_to_freeword_hom' ) qed (auto simp add: g h knil ksingle) qed lemma uniqueness_of_extended_map_to_freeword_hom: fixes f :: "'a ⇒ 'b::group_add" defines "h::'a signed ⇒ 'b ≡ λ(s,b). if b then f s else - (f s)" defines "g::'a freeword ⇒ 'b ≡ λx. sum_list (map h (freeword x))" assumes k: "k ∘ Abs_freeletter = f" "UGroupHom k" shows "k = g" proof fix x::"'a freeword" define k' where k': "k' ≡ k ∘ Abs_freeword" have "k' (freeword x) = g x" unfolding h_def g_def proof (rule uniqueness_of_extended_map_to_freeword_hom') from k' k(1) show "⋀s. k' [pairtrue s] = f s" by auto show "⋀xs ys. proper_signed_list xs ⟹ proper_signed_list ys ⟹ k' (prappend_signed_list xs ys) = k' xs + k' ys" proof- fix xs ys :: "'a signed list" assume xsys: "proper_signed_list xs" "proper_signed_list ys" with k' show "k' (prappend_signed_list xs ys) = k' xs + k' ys" using UGroupHom.hom[OF k(2), of "Abs_freeword xs" "Abs_freeword ys"] by (simp add: plus_freeword_abs_eq) qed show "proper_signed_list (freeword x)" using freeword by fast qed with k' show "k x = g x" using freeword_inverse[of x] by simp qed theorem universal_property: fixes f :: "'a ⇒ 'b::group_add" shows "∃!g::'a freeword⇒'b. g ∘ Abs_freeletter = f ∧ UGroupHom g" proof define h where h: "h ≡ λ(s,b). if b then f s else - (f s)" define g where g: "g ≡ λx. sum_list (map h (freeword x))" from g h show "g ∘ Abs_freeletter = f ∧ UGroupHom g" using extend_map_to_freeword_hom1[of f] extend_map_to_freeword_hom2 by auto from g h show "⋀k. k ∘ Abs_freeletter = f ∧ UGroupHom k ⟹ k = g" using uniqueness_of_extended_map_to_freeword_hom by auto qed paragraph ‹Properties of homomorphisms afforded by the universal property› text ‹ The lift of a function on the letter set is the unique additive function on @{type freeword} that agrees with the original function on letters. › definition freeword_funlift :: "('a ⇒ 'b::group_add) ⇒ ('a freeword⇒'b::group_add)" where "freeword_funlift f ≡ (THE g. g ∘ Abs_freeletter = f ∧ UGroupHom g)" lemma additive_freeword_funlift: "UGroupHom (freeword_funlift f)" using theI'[OF universal_property, of f] unfolding freeword_funlift_def by simp lemma freeword_funlift_Abs_freeletter: "freeword_funlift f (Abs_freeletter s) = f s" using theI'[OF universal_property, of f] comp_apply[of "freeword_funlift f" Abs_freeletter] unfolding freeword_funlift_def by fastforce lemmas freeword_funlift_add = UGroupHom.hom [OF additive_freeword_funlift] lemmas freeword_funlift_0 = UGroupHom.im_zero [OF additive_freeword_funlift] lemmas freeword_funlift_uminus = UGroupHom.im_uminus [OF additive_freeword_funlift] lemmas freeword_funlift_diff = UGroupHom.im_diff [OF additive_freeword_funlift] lemmas freeword_funlift_lconjby = UGroupHom.im_lconjby [OF additive_freeword_funlift] lemma freeword_funlift_uminus_Abs_freeletter: "freeword_funlift f (Abs_freeword [(s,False)]) = - f s" using freeword_funlift_uminus[of f "Abs_freeword [(s,False)]"] uminus_freeword_Abs_eq[of "[(s,False)]"] freeword_funlift_Abs_freeletter[of f] by simp lemma freeword_funlift_Abs_freeword_singleton: "freeword_funlift f (Abs_freeword [x]) = apply_sign f x" proof- obtain s b where x: "x = (s,b)" by fastforce thus ?thesis using freeword_funlift_Abs_freeletter freeword_funlift_uminus_Abs_freeletter by (cases b) auto qed lemma freeword_funlift_Abs_freeword_Cons: assumes "proper_signed_list (x#xs)" shows "freeword_funlift f (Abs_freeword (x#xs)) = apply_sign f x + freeword_funlift f (Abs_freeword xs)" proof- from assms have "freeword_funlift f (Abs_freeword (x#xs)) = freeword_funlift f (Abs_freeword [x]) + freeword_funlift f (Abs_freeword xs)" using Abs_freeword_Cons[of x xs] freeword_funlift_add by simp thus ?thesis using freeword_funlift_Abs_freeword_singleton[of f x] by simp qed lemma freeword_funlift_Abs_freeword: "proper_signed_list xs ⟹ freeword_funlift f (Abs_freeword xs) = (∑x←xs. apply_sign f x)" proof (induct xs) case (Cons x xs) thus ?case using freeword_funlift_Abs_freeword_Cons[of _ _ f] binrelchain_Cons_reduce[of _ x xs] by simp qed (simp add: zero_freeword.abs_eq[THEN sym] freeword_funlift_0) lemma freeword_funlift_Abs_freelist: "freeword_funlift f (Abs_freelist xs) = (∑x←xs. f x)" proof (induct xs) case (Cons x xs) thus ?case using Abs_freelist_Cons[of x xs] by (simp add: freeword_funlift_add freeword_funlift_Abs_freeletter) qed (simp add: zero_freeword.abs_eq[THEN sym] freeword_funlift_0) lemma freeword_funlift_im': "proper_signed_list xs ⟹ fst ` set xs ⊆ S ⟹ freeword_funlift f (Abs_freeword xs) ∈ ⟨f`S⟩" proof (induct xs) case Nil have "Abs_freeword ([]::'a signed list) = (0::'a freeword)" using zero_freeword.abs_eq[THEN sym] by simp thus "freeword_funlift f (Abs_freeword ([]::'a signed list)) ∈ ⟨f`S⟩" using freeword_funlift_0[of f] genby_0_closed by simp next case (Cons x xs) define y where y: "y ≡ apply_sign f x" define z where z: "z ≡ freeword_funlift f (Abs_freeword xs)" from Cons(3) have "fst ` set xs ⊆ S" by simp with z Cons(1,2) have "z ∈ ⟨f`S⟩" using binrelchain_Cons_reduce by fast with y Cons(3) have "y + z ∈ ⟨f`S⟩" using genby_genset_closed[of _ "f`S"] genby_uminus_closed genby_add_closed[of y] by fastforce with Cons(2) y z show ?case using freeword_funlift_Abs_freeword_Cons subst[ OF sym, of "freeword_funlift f (Abs_freeword (x#xs))" "y+z" "λb. b∈⟨f`S⟩" ] by fast qed subsubsection ‹Free groups on a set› text ‹ We now take the free group on a set to be the set in the @{type freeword} type with letters restricted to the given set. › paragraph ‹Definition and basic facts› text ‹ Here we define the set of elements of the free group over a set of letters, and record basic facts about that set. › definition FreeGroup :: "'a set ⇒ 'a freeword set" where "FreeGroup S ≡ {x. fst ` set (freeword x) ⊆ S}" lemma FreeGroupI_transfer: "proper_signed_list xs ⟹ fst ` set xs ⊆ S ⟹ Abs_freeword xs ∈ FreeGroup S" using Abs_freeword_inverse unfolding FreeGroup_def by fastforce lemma FreeGroupD: "x ∈ FreeGroup S ⟹ fst ` set (freeword x) ⊆ S" using FreeGroup_def by fast lemma FreeGroupD_transfer: "proper_signed_list xs ⟹ Abs_freeword xs ∈ FreeGroup S ⟹ fst ` set xs ⊆ S" using Abs_freeword_inverse unfolding FreeGroup_def by fastforce lemma FreeGroupD_transfer': "Abs_freelist xs ∈ FreeGroup S ⟹ xs ∈ lists S" using proper_signed_list_map_uniform_snd FreeGroupD_transfer by fastforce lemma FreeGroup_0_closed: "0 ∈ FreeGroup S" proof- have "(0::'a freeword) = Abs_freeword []" using zero_freeword.abs_eq by fast moreover have "Abs_freeword [] ∈ FreeGroup S" using FreeGroupI_transfer[of "[]"] by simp ultimately show ?thesis by simp qed lemma FreeGroup_diff_closed: assumes "x ∈ FreeGroup S" "y ∈ FreeGroup S" shows "x-y ∈ FreeGroup S" proof- define xs where xs: "xs ≡ freeword x" define ys where ys: "ys ≡ freeword y" have "freeword (x-y) = prappend_signed_list (freeword x) (rev (map flip_signed (freeword y)))" by transfer simp hence "fst ` set (freeword (x-y)) ⊆ fst ` (set (freeword x) ∪ set (freeword y))" using fst_set_prappend_signed_list by force with assms show ?thesis unfolding FreeGroup_def by fast qed lemma FreeGroup_Group: "Group (FreeGroup S)" using FreeGroup_0_closed FreeGroup_diff_closed by unfold_locales fast lemmas FreeGroup_add_closed = Group.add_closed [OF FreeGroup_Group] lemmas FreeGroup_uminus_closed = Group.uminus_closed [OF FreeGroup_Group] lemmas FreeGroup_genby_set_lconjby_set_rconjby_closed = Group.genby_set_lconjby_set_rconjby_closed[OF FreeGroup_Group] lemma Abs_freelist_in_FreeGroup: "ss ∈ lists S ⟹ Abs_freelist ss ∈ FreeGroup S" using proper_signed_list_map_uniform_snd by (fastforce intro: FreeGroupI_transfer) lemma Abs_freeletter_in_FreeGroup_iff: "(Abs_freeletter s ∈ FreeGroup S) = (s∈S)" using Abs_freeword_inverse[of "[pairtrue s]"] unfolding FreeGroup_def by simp paragraph ‹Lifts of functions from the letter set to some type of class @{class group_add}› text ‹ We again obtain a universal property for functions from the (restricted) letter set to some type of class @{class group_add}. › abbreviation "res_freeword_funlift f S ≡ restrict0 (freeword_funlift f) (FreeGroup S)" lemma freeword_funlift_im: "x ∈ FreeGroup S ⟹ freeword_funlift f x ∈ ⟨f ` S⟩" using freeword[of x] freeword_funlift_im'[of "freeword x"] freeword_inverse[of x] unfolding FreeGroup_def by auto lemma freeword_funlift_surj': "ys ∈ lists (f`S ∪ uminus`f`S) ⟹ sum_list ys ∈ freeword_funlift f ` FreeGroup S" proof (induct ys) case Nil thus ?case using FreeGroup_0_closed freeword_funlift_0 by fastforce next case (Cons y ys) from this obtain x where x: "x ∈ FreeGroup S" "sum_list ys = freeword_funlift f x" by auto show "sum_list (y#ys) ∈ freeword_funlift f ` FreeGroup S" proof (cases "y ∈ f`S") case True from this obtain s where s: "s∈S" "y = f s" by fast from s(1) x(1) have "Abs_freeletter s + x ∈ FreeGroup S" using FreeGroupI_transfer[of _ S] FreeGroup_add_closed[of _ S] by force moreover from s(2) x(2) have "freeword_funlift f (Abs_freeletter s + x) = sum_list (y#ys)" using freeword_funlift_add[of f] freeword_funlift_Abs_freeletter by simp ultimately show ?thesis by force next case False with Cons(2) obtain s where s: "s∈S" "y = - f s" by auto from s(1) x(1) have "Abs_freeword [(s,False)] + x ∈ FreeGroup S" using FreeGroupI_transfer[of _ S] FreeGroup_add_closed[of _ S] by force moreover from s(2) x(2) have "freeword_funlift f (Abs_freeword [(s,False)] + x) = sum_list (y#ys)" using freeword_funlift_add[of f] freeword_funlift_uminus_Abs_freeletter by simp ultimately show ?thesis by force qed qed lemma freeword_funlift_surj: fixes f :: "'a ⇒ 'b::group_add" shows "freeword_funlift f ` FreeGroup S = ⟨f`S⟩" proof (rule seteqI) show "⋀a. a ∈ freeword_funlift f ` FreeGroup S ⟹ a ∈ ⟨f`S⟩" using freeword_funlift_im by auto next fix w assume "w∈⟨f`S⟩" from this obtain ys where ys: "ys ∈ lists (f`S ∪ uminus`f`S)" "w = sum_list ys" using genby_eq_sum_lists[of "f`S"] by auto thus "w ∈ freeword_funlift f ` FreeGroup S" using freeword_funlift_surj' by simp qed lemma hom_restrict0_freeword_funlift: "GroupHom (FreeGroup S) (res_freeword_funlift f S)" using UGroupHom.restrict0 additive_freeword_funlift FreeGroup_Group by auto lemma uniqueness_of_restricted_lift: assumes "GroupHom (FreeGroup S) T" "∀s∈S. T (Abs_freeletter s) = f s" shows "T = res_freeword_funlift f S" proof fix x define F where "F ≡ res_freeword_funlift f S" define u_Abs where "u_Abs ≡ λa::'a signed. apply_sign Abs_freeletter a" show "T x = F x" proof (cases "x ∈ FreeGroup S") case True have 1: "set (map u_Abs (freeword x)) ⊆ FreeGroup S" using u_Abs_def FreeGroupD[OF True] Abs_freeletter_in_FreeGroup_iff[of _ S] FreeGroup_uminus_closed by auto moreover from u_Abs_def have "x = (∑a←freeword x. u_Abs a)" using freeword_conv_freeletter_sum_list by fast ultimately have "T x = (∑a←freeword x. T (u_Abs a))" "F x = (∑a←freeword x. F (u_Abs a))" using F_def GroupHom.im_sum_list_map[OF assms(1), of u_Abs "freeword x"] GroupHom.im_sum_list_map[ OF hom_restrict0_freeword_funlift, of u_Abs "freeword x" S f ] by auto moreover have "∀a∈set (freeword x). T (u_Abs a) = F (u_Abs a)" proof fix a assume "a ∈ set (freeword x)" moreover define b where "b ≡ Abs_freeletter (fst a)" ultimately show "T (u_Abs a) = F (u_Abs a)" using F_def u_Abs_def True assms(2) FreeGroupD[of x S] GroupHom.im_uminus[OF assms(1)] Abs_freeletter_in_FreeGroup_iff[of "fst a" S] GroupHom.im_uminus[OF hom_restrict0_freeword_funlift, of b S f] freeword_funlift_Abs_freeletter[of f] by auto qed ultimately show ?thesis using F_def sum_list_map_cong[of "freeword x" "λs. T (u_Abs s)" "λs. F (u_Abs s)"] by simp next case False with assms(1) F_def show ?thesis using hom_restrict0_freeword_funlift GroupHom.supp suppI_contra[of x T] suppI_contra[of x F] by fastforce qed qed theorem FreeGroup_universal_property: fixes f :: "'a ⇒ 'b::group_add" shows "∃!T::'a freeword⇒'b. (∀s∈S. T (Abs_freeletter s) = f s) ∧ GroupHom (FreeGroup S) T" proof (rule ex1I, rule conjI) show "∀s∈S. res_freeword_funlift f S (Abs_freeletter s) = f s" using Abs_freeletter_in_FreeGroup_iff[of _ S] freeword_funlift_Abs_freeletter by auto show "⋀T. (∀s∈S. T (Abs_freeletter s) = f s) ∧ GroupHom (FreeGroup S) T ⟹ T = restrict0 (freeword_funlift f) (FreeGroup S)" using uniqueness_of_restricted_lift by auto qed (rule hom_restrict0_freeword_funlift) subsubsection ‹Group presentations› text ‹ We now define a group presentation to be the quotient of a free group by the subgroup generated by all conjugates of a set of relators. We are most concerned with lifting functions on the letter set to the free group and with the associated induced homomorphisms on the quotient. › paragraph ‹A first group presentation locale and basic facts› text ‹ Here we define a locale that provides a way to construct a group by providing sets of generators and relator words. › locale GroupByPresentation = fixes S :: "'a set" ― ‹the set of generators› and P :: "'a signed list set" ― ‹the set of relator words› assumes P_S: "ps∈P ⟹ fst ` set ps ⊆ S" and proper_P: "ps∈P ⟹ proper_signed_list ps" begin abbreviation "P' ≡ Abs_freeword ` P" ― ‹the set of relators› abbreviation "Q ≡ Group.normal_closure (FreeGroup S) P'" ― ‹the normal subgroup generated by relators inside the free group› abbreviation "G ≡ Group.quotient_group (FreeGroup S) Q" lemmas G_UN = Group.quotient_group_UN[OF FreeGroup_Group, of S Q] lemma P'_FreeS: "P' ⊆ FreeGroup S" using P_S proper_P by (blast intro: FreeGroupI_transfer) lemma relators: "P' ⊆ Q" using FreeGroup_0_closed genby_genset_subset by fastforce lemmas lconjby_P'_FreeS = Group.set_lconjby_subset_closed[ OF FreeGroup_Group _ P'_FreeS, OF basic_monos(1) ] lemmas Q_FreeS = Group.genby_closed[OF FreeGroup_Group lconjby_P'_FreeS] lemmas Q_subgroup_FreeS = Group.genby_subgroup[OF FreeGroup_Group lconjby_P'_FreeS] lemmas normal_Q = Group.normal_closure[OF FreeGroup_Group, OF P'_FreeS] lemmas natural_hom = Group.natural_quotient_hom[ OF FreeGroup_Group Q_subgroup_FreeS normal_Q ] lemmas natural_hom_image = Group.natural_quotient_hom_image[OF FreeGroup_Group, of S Q] end (* context GroupByPresentation *) paragraph ‹Functions on the quotient induced from lifted functions› text ‹ A function on the generator set into a type of class @{class group_add} lifts to a unique homomorphism on the free group. If this lift is trivial on relators, then it factors to a homomorphism of the group described by the generators and relators. › locale GroupByPresentationInducedFun = GroupByPresentation S P for S :: "'a set" and P :: "'a signed list set" ― ‹the set of relator words› + fixes f :: "'a ⇒ 'b::group_add" assumes lift_f_trivial_P: "ps∈P ⟹ freeword_funlift f (Abs_freeword ps) = 0" begin abbreviation "lift_f ≡ freeword_funlift f" definition induced_hom :: "'a freeword set permutation ⇒ 'b" where "induced_hom ≡ GroupHom.quotient_hom (FreeGroup S) (restrict0 lift_f (FreeGroup S)) Q" ― ‹the @{const restrict0} operation is really only necessary to make @{const GroupByPresentationInducedFun.induced_hom} a @{const GroupHom}› abbreviation "F ≡ induced_hom" lemma lift_f_trivial_P': "p∈P' ⟹ lift_f p = 0" using lift_f_trivial_P by fast lemma lift_f_trivial_lconjby_P': "p∈P' ⟹ lift_f (lconjby w p) = 0" using freeword_funlift_lconjby[of f] lift_f_trivial_P' by simp lemma lift_f_trivial_Q: "q∈Q ⟹ lift_f q = 0" proof (erule genby.induct, rule freeword_funlift_0) show "⋀s. s ∈ (⋃w ∈ FreeGroup S. lconjby w ` P') ⟹ lift_f s = 0" using lift_f_trivial_lconjby_P' by fast next fix w w' :: "'a freeword" assume ww': "lift_f w = 0" "lift_f w' = 0" have "lift_f (w - w') = lift_f w - lift_f w'" using freeword_funlift_diff[of f w] by simp with ww' show "lift_f (w-w') = 0" by simp qed lemma lift_f_ker_Q: "Q ⊆ ker lift_f" using lift_f_trivial_Q unfolding ker_def by auto lemma lift_f_Ker_Q: "Q ⊆ GroupHom.Ker (FreeGroup S) lift_f" using lift_f_ker_Q Q_FreeS by fast lemma restrict0_lift_f_Ker_Q: "Q ⊆ GroupHom.Ker (FreeGroup S) (restrict0 lift_f (FreeGroup S))" using lift_f_Ker_Q ker_subset_ker_restrict0 by fast lemma induced_hom_equality: "w ∈ FreeGroup S ⟹ F (⌈FreeGroup S|w|Q⌉) = lift_f w" ― ‹algebraic properties of the induced homomorphism could be proved using its properties as a group homomorphism, but it's generally easier to prove them using the algebraic properties of the lift via this lemma› unfolding induced_hom_def using GroupHom.quotient_hom_im hom_restrict0_freeword_funlift Q_subgroup_FreeS normal_Q restrict0_lift_f_Ker_Q by fastforce lemma hom_induced_hom: "GroupHom G F" unfolding induced_hom_def using GroupHom.quotient_hom hom_restrict0_freeword_funlift Q_subgroup_FreeS normal_Q restrict0_lift_f_Ker_Q by fast lemma induced_hom_Abs_freeletter_equality: "s∈S ⟹ F (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s" using Abs_freeletter_in_FreeGroup_iff[of s S] by (simp add: induced_hom_equality freeword_funlift_Abs_freeletter) lemma uniqueness_of_induced_hom': defines "q ≡ Group.natural_quotient_hom (FreeGroup S) Q" assumes "GroupHom G T" "∀s∈S. T (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s" shows "T ∘ q = F ∘ q" proof- from assms have "T∘q = res_freeword_funlift f S" using natural_hom natural_hom_image Abs_freeletter_in_FreeGroup_iff[of _ S] by (force intro: uniqueness_of_restricted_lift GroupHom.comp) moreover from q_def have "F ∘ q = res_freeword_funlift f S" using induced_hom_equality GroupHom.im_zero[OF hom_induced_hom] by auto ultimately show ?thesis by simp qed lemma uniqueness_of_induced_hom: assumes "GroupHom G T" "∀s∈S. T (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s" shows "T = F" proof fix x show "T x = F x" proof (cases "x∈G") case True define q where "q ≡ Group.natural_quotient_hom (FreeGroup S) Q" from True obtain w where "w ∈ FreeGroup S" "x = (⌈FreeGroup S|w|Q⌉)" using G_UN by fast with q_def have "T x = (T∘q) w" "F x = (F∘q) w" by auto with assms q_def show ?thesis using uniqueness_of_induced_hom' by simp next case False with assms(1) show ?thesis using hom_induced_hom GroupHom.supp suppI_contra[of x T] suppI_contra[of x F] by fastforce qed qed theorem induced_hom_universal_property: "∃!F. GroupHom G F ∧ (∀s∈S. F (⌈FreeGroup S|Abs_freeletter s|Q⌉) = f s)" using hom_induced_hom induced_hom_Abs_freeletter_equality uniqueness_of_induced_hom by blast lemma induced_hom_Abs_freelist_conv_sum_list: "ss∈lists S ⟹ F (⌈FreeGroup S|Abs_freelist ss|Q⌉) = (∑s←ss. f s)" by (simp add: Abs_freelist_in_FreeGroup induced_hom_equality freeword_funlift_Abs_freelist ) lemma induced_hom_surj: "F`G = ⟨f`S⟩" proof (rule seteqI) show "⋀x. x∈F`G ⟹ x∈⟨f`S⟩" using G_UN induced_hom_equality freeword_funlift_surj[of f S] by auto next fix x assume "x∈⟨f`S⟩" hence "x ∈ lift_f ` FreeGroup S" using freeword_funlift_surj[of f S] by fast thus "x ∈ F`G" using induced_hom_equality G_UN by force qed end (* context GroupByPresentationInducedFun *) paragraph ‹Groups affording a presentation› text ‹ The locale @{const GroupByPresentation} allows the construction of a @{const Group} out of any type from a set of generating letters and a set of relator words in (signed) letters. The following locale concerns the question of when the @{const Group} generated by a set in class @{class group_add} is isomorphic to a group presentation. › locale GroupWithGeneratorsRelators = fixes S :: "'g::group_add set" ― ‹the set of generators› and R :: "'g list set" ― ‹the set of relator words› assumes relators: "rs∈R ⟹ rs ∈ lists (S ∪ uminus ` S)" "rs∈R ⟹ sum_list rs = 0" "rs∈R ⟹ proper_signed_list (map (charpair S) rs)" begin abbreviation "P ≡ map (charpair S) ` R" abbreviation "P' ≡ GroupByPresentation.P' P" abbreviation "Q ≡ GroupByPresentation.Q S P" abbreviation "G ≡ GroupByPresentation.G S P" abbreviation "relator_freeword rs ≡ Abs_freeword (map (charpair S) rs)" ― ‹this maps R onto P'› abbreviation "freeliftid ≡ freeword_funlift id" abbreviation induced_id :: "'g freeword set permutation ⇒ 'g" where "induced_id ≡ GroupByPresentationInducedFun.induced_hom S P id" lemma GroupByPresentation_S_P: "GroupByPresentation S P" proof show "⋀ps. ps ∈ P ⟹ fst ` set ps ⊆ S" using fst_set_map_charpair_un_uminus relators(1) by fast show "⋀ps. ps ∈ P ⟹ proper_signed_list ps" using relators(3) by fast qed lemmas G_UN = GroupByPresentation.G_UN[OF GroupByPresentation_S_P] lemmas P'_FreeS = GroupByPresentation.P'_FreeS[OF GroupByPresentation_S_P] lemma freeliftid_trivial_relator_freeword_R: "rs∈R ⟹ freeliftid (relator_freeword rs) = 0" using relators(2,3) freeword_funlift_Abs_freeword[of "map (charpair S) rs" id] sum_list_map_cong[of rs "(apply_sign id) ∘ (charpair S)" id] by simp lemma freeliftid_trivial_P: "ps∈P ⟹ freeliftid (Abs_freeword ps) = 0" using freeliftid_trivial_relator_freeword_R by fast lemma GroupByPresentationInducedFun_S_P_id: "GroupByPresentationInducedFun S P id" by ( intro_locales, rule GroupByPresentation_S_P, unfold_locales, rule freeliftid_trivial_P ) lemma induced_id_Abs_freelist_conv_sum_list: "ss∈lists S ⟹ induced_id (⌈FreeGroup S|Abs_freelist ss|Q⌉) = sum_list ss" by (simp add: GroupByPresentationInducedFun.induced_hom_Abs_freelist_conv_sum_list[ OF GroupByPresentationInducedFun_S_P_id ] ) lemma lconj_relator_freeword_R: "⟦ rs∈R; proper_signed_list xs; fst ` set xs ⊆ S ⟧ ⟹ lconjby (Abs_freeword xs) (relator_freeword rs) ∈ Q" by (blast intro: genby_genset_closed FreeGroupI_transfer) lemma rconj_relator_freeword: assumes "rs∈R" "proper_signed_list xs" "fst ` set xs ⊆ S" shows "rconjby (Abs_freeword xs) (relator_freeword rs) ∈ Q" proof (rule genby_genset_closed, rule UN_I) show "- Abs_freeword xs ∈ FreeGroup S" using FreeGroupI_transfer[OF assms(2,3)] FreeGroup_uminus_closed by fast from assms(1) show "rconjby (Abs_freeword xs) (relator_freeword rs) ∈ lconjby (- Abs_freeword xs) ` Abs_freeword ` P" by simp qed lemma lconjby_Abs_freelist_relator_freeword: "⟦ rs∈R; xs∈lists S ⟧ ⟹ lconjby (Abs_freelist xs) (relator_freeword rs) ∈ Q" using proper_signed_list_map_uniform_snd by (force intro: lconj_relator_freeword_R) text ‹ Here we record that the lift of the identity map to the free group on @{term S} induces a homomorphic surjection onto the group generated by @{term S} from the group presentation on @{term S}, subject to the same relations as the elements of @{term S}. › theorem induced_id_hom_surj: "GroupHom G induced_id" "induced_id ` G = ⟨S⟩" using GroupByPresentationInducedFun.hom_induced_hom[ OF GroupByPresentationInducedFun_S_P_id ] GroupByPresentationInducedFun.induced_hom_surj[ OF GroupByPresentationInducedFun_S_P_id ] by auto end (* context GroupWithGeneratorsRelators *) locale GroupPresentation = GroupWithGeneratorsRelators S R for S :: "'g::group_add set" ― ‹the set of generators› and R :: "'g list set" ― ‹the set of relator words› + assumes induced_id_inj: "inj_on induced_id G" begin abbreviation "inv_induced_id ≡ the_inv_into G induced_id" lemma inv_induced_id_sum_list_S: "ss ∈ lists S ⟹ inv_induced_id (sum_list ss) = (⌈FreeGroup S|Abs_freelist ss|Q⌉)" using G_UN induced_id_inj induced_id_Abs_freelist_conv_sum_list Abs_freelist_in_FreeGroup by (blast intro: the_inv_into_f_eq) end (* GroupPresentation *) subsection ‹Words over a generating set› text ‹ Here we gather the necessary constructions and facts for studying a group generated by some set in terms of words in the generators. › context monoid_add begin abbreviation "word_for A a as ≡ as ∈ lists A ∧ sum_list as = a" definition reduced_word_for :: "'a set ⇒ 'a ⇒ 'a list ⇒ bool" where "reduced_word_for A a as ≡ is_arg_min length (word_for A a) as" abbreviation "reduced_word A as ≡ reduced_word_for A (sum_list as) as" abbreviation "reduced_words_for A a ≡ Collect (reduced_word_for A a)" abbreviation reduced_letter_set :: "'a set ⇒ 'a ⇒ 'a set" where "reduced_letter_set A a ≡ ⋃( set ` (reduced_words_for A a) )" ― ‹will be empty if @{term a} is not in the set generated by @{term A}› definition word_length :: "'a set ⇒ 'a ⇒ nat" where "word_length A a ≡ length (arg_min length (word_for A a))" lemma reduced_word_forI: assumes "as ∈ lists A" "sum_list as = a" "⋀bs. bs ∈ lists A ⟹ sum_list bs = a ⟹ length as ≤ length bs" shows "reduced_word_for A a as" using assms unfolding reduced_word_for_def by (force intro: is_arg_minI) lemma reduced_word_forI_compare: "⟦ reduced_word_for A a as; bs ∈ lists A; sum_list bs = a; length bs = length as ⟧ ⟹ reduced_word_for A a bs" using reduced_word_for_def is_arg_min_eq[of length] by fast lemma reduced_word_for_lists: "reduced_word_for A a as ⟹ as ∈ lists A" using reduced_word_for_def is_arg_minD1 by fast lemma reduced_word_for_sum_list: "reduced_word_for A a as ⟹ sum_list as = a" using reduced_word_for_def is_arg_minD1 by fast lemma reduced_word_for_minimal: "⟦ reduced_word_for A a as; bs ∈ lists A; sum_list bs = a ⟧ ⟹ length as ≤ length bs" using reduced_word_for_def is_arg_minD2[of length] by fastforce lemma reduced_word_for_length: "reduced_word_for A a as ⟹ length as = word_length A a" unfolding word_length_def reduced_word_for_def is_arg_min_def by (fastforce intro: arg_min_equality[THEN sym]) lemma reduced_word_for_eq_length: "reduced_word_for A a as ⟹ reduced_word_for A a bs ⟹ length as = length bs" using reduced_word_for_length by simp lemma reduced_word_for_arg_min: "as ∈ lists A ⟹ sum_list as = a ⟹ reduced_word_for A a (arg_min length (word_for A a))" using is_arg_min_arg_min_nat[of "word_for A a"] unfolding reduced_word_for_def by fast lemma nil_reduced_word_for_0: "reduced_word_for A 0 []" by (auto intro: reduced_word_forI) lemma reduced_word_for_0_imp_nil: "reduced_word_for A 0 as ⟹ as = []" using nil_reduced_word_for_0[of A] reduced_word_for_minimal[of A 0 as] unfolding reduced_word_for_def is_arg_min_def by (metis (mono_tags, hide_lams) length_0_conv length_greater_0_conv) lemma not_reduced_word_for: "⟦ bs ∈ lists A; sum_list bs = a; length bs < length as ⟧ ⟹ ¬ reduced_word_for A a as" using reduced_word_for_minimal by fastforce lemma reduced_word_for_imp_reduced_word: "reduced_word_for A a as ⟹ reduced_word A as" unfolding reduced_word_for_def is_arg_min_def by (fast intro: reduced_word_forI) lemma sum_list_zero_nreduced: "as ≠ [] ⟹ sum_list as = 0 ⟹ ¬ reduced_word A as" using not_reduced_word_for[of "[]"] by simp lemma order2_nreduced: "a+a=0 ⟹ ¬ reduced_word A [a,a]" using sum_list_zero_nreduced by simp lemma reduced_word_append_reduce_contra1: assumes "¬ reduced_word A as" shows "¬ reduced_word A (as@bs)" proof (cases "as ∈ lists A" "bs ∈ lists A" rule: two_cases) case both define cs where cs: "cs ≡ ARG_MIN length cs. cs ∈ lists A ∧ sum_list cs = sum_list as" with both(1) have "reduced_word_for A (sum_list as) cs" using reduced_word_for_def is_arg_min_arg_min_nat[of "word_for A (sum_list as)"] by auto with assms both show ?thesis using reduced_word_for_lists reduced_word_for_sum_list reduced_word_for_minimal[of A "sum_list as" cs as] reduced_word_forI_compare[of A "sum_list as" cs as] not_reduced_word_for[of "cs@bs" A "sum_list (as@bs)"] by fastforce next case one thus ?thesis using reduced_word_for_lists by fastforce next case other thus ?thesis using reduced_word_for_lists by fastforce next case neither thus ?thesis using reduced_word_for_lists by fastforce qed lemma reduced_word_append_reduce_contra2: assumes "¬ reduced_word A bs" shows "¬ reduced_word A (as@bs)" proof (cases "as ∈ lists A" "bs ∈ lists A" rule: two_cases) case both define cs where cs: "cs ≡ ARG_MIN length cs. cs ∈ lists A ∧ sum_list cs = sum_list bs" with both(2) have "reduced_word_for A (sum_list bs) cs" using reduced_word_for_def is_arg_min_arg_min_nat[of "word_for A (sum_list bs)" ] by auto with assms both show ?thesis using reduced_word_for_lists reduced_word_for_sum_list reduced_word_for_minimal[of A "sum_list bs" cs bs] reduced_word_forI_compare[of A "sum_list bs" cs bs] not_reduced_word_for[of "as@cs" A "sum_list (as@bs)"] by fastforce next case one thus ?thesis using reduced_word_for_lists by fastforce next case other thus ?thesis using reduced_word_for_lists by fastforce next case neither thus ?thesis using reduced_word_for_lists by fastforce qed lemma contains_nreduced_imp_nreduced: "¬ reduced_word A bs ⟹ ¬ reduced_word A (as@bs@cs)" using reduced_word_append_reduce_contra1 reduced_word_append_reduce_contra2 by fast lemma contains_order2_nreduced: "a+a=0 ⟹ ¬ reduced_word A (as@[a,a]@bs)" using order2_nreduced contains_nreduced_imp_nreduced by fast lemma reduced_word_Cons_reduce_contra: "¬ reduced_word A as ⟹ ¬ reduced_word A (a#as)" using reduced_word_append_reduce_contra2[of A as "[a]"] by simp lemma reduced_word_Cons_reduce: "reduced_word A (a#as) ⟹ reduced_word A as" using reduced_word_Cons_reduce_contra by fast lemma reduced_word_singleton: assumes "a∈A" "a≠0" shows "reduced_word A [a]" proof (rule reduced_word_forI) from assms(1) show "[a] ∈ lists A" by simp next fix bs assume bs: "bs ∈ lists A" "sum_list bs = sum_list [a]" with assms(2) show "length [a] ≤ length bs" by (cases bs) auto qed simp lemma el_reduced: assumes "0 ∉ A" "as ∈ lists A" "sum_list as ∈ A" "reduced_word A as" shows "length as = 1" proof- define n where n: "n ≡ length as" from assms(3) obtain a where "[a]∈lists A" "sum_list as = sum_list [a]" by auto with n assms(1,3,4) have "n≤1" "n>0" using reduced_word_for_minimal[of A _ as "[a]"] by auto hence "n = 1" by simp with n show ?thesis by fast qed lemma reduced_letter_set_0: "reduced_letter_set A 0 = {}" using reduced_word_for_0_imp_nil by simp lemma reduced_letter_set_subset: "reduced_letter_set A a ⊆ A" using reduced_word_for_lists by fast lemma reduced_word_forI_length: "⟦ as ∈ lists A; sum_list as = a; length as = word_length A a ⟧ ⟹ reduced_word_for A a as" using reduced_word_for_arg_min reduced_word_for_length reduced_word_forI_compare[of A a _ as] by fastforce lemma word_length_le: "as ∈ lists A ⟹ sum_list as = a ⟹ word_length A a ≤ length as" using reduced_word_for_arg_min reduced_word_for_length reduced_word_for_minimal[of A] by fastforce lemma reduced_word_forI_length': "⟦ as ∈ lists A; sum_list as = a; length as ≤ word_length A a ⟧ ⟹ reduced_word_for A a as" using word_length_le[of as A] reduced_word_forI_length[of as A] by fastforce lemma word_length_lt: "as ∈ lists A ⟹ sum_list as = a ⟹ ¬ reduced_word_for A a as ⟹ word_length A a < length as" using reduced_word_forI_length' by fastforce end (* context monoid_add *) lemma in_genby_reduced_letter_set: assumes "as ∈ lists A" "sum_list as = a" shows "a ∈ ⟨reduced_letter_set A a⟩" proof- define xs where xs: "xs ≡ arg_min length (word_for A a)" with assms have "xs ∈ lists (reduced_letter_set A a)" "sum_list xs = a" using reduced_word_for_arg_min[of as A] reduced_word_for_sum_list by auto thus ?thesis using genby_eq_sum_lists by force qed lemma reduced_word_for_genby_arg_min: fixes A :: "'a::group_add set" defines "B ≡ A ∪ uminus ` A" assumes "a∈⟨A⟩" shows "reduced_word_for B a (arg_min length (word_for B a))" using assms genby_eq_sum_lists[of A] reduced_word_for_arg_min[of _ B a] by auto lemma reduced_word_for_genby_sym_arg_min: assumes "uminus ` A ⊆ A" "a∈⟨A⟩" shows "reduced_word_for A a (arg_min length (word_for A a))" proof- from assms(1) have "A = A ∪ uminus ` A" by auto with assms(2) show ?thesis using reduced_word_for_genby_arg_min[of a A] by simp qed lemma in_genby_imp_in_reduced_letter_set: fixes A :: "'a::group_add set" defines "B ≡ A ∪ uminus ` A" assumes "a ∈ ⟨A⟩" shows "a ∈ ⟨reduced_letter_set B a⟩" using assms genby_eq_sum_lists[of A] in_genby_reduced_letter_set[of _ B] by auto lemma in_genby_sym_imp_in_reduced_letter_set: "uminus ` A ⊆ A ⟹ a ∈ ⟨A⟩ ⟹ a ∈ ⟨reduced_letter_set A a⟩" using in_genby_imp_in_reduced_letter_set by (fastforce simp add: Un_absorb2) end (* theory *)