Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Hoare_Examples.thy Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Sym_Groups.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Sym_Groups
  imports Cycles Solvable_Groups

begin

section \<open>Symmetric Groups\<close>

subsection \<open>Definitions\<close>

abbreviation inv' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
  where "inv' f \ Hilbert_Choice.inv f"

definition sym_group :: "nat \ (nat \ nat) monoid"
  where "sym_group n = \ carrier = { p. p permutes {1..n} }, mult = (\), one = id \"

definition alt_group :: "nat \ (nat \ nat) monoid"
  where "alt_group n = (sym_group n) \ carrier := { p. p permutes {1..n} \ evenperm p } \"

definition sign_img :: "int monoid"
  where "sign_img = \ carrier = { -1, 1 }, mult = (*), one = 1 \"

subsection \<open>Basic Properties\<close>

lemma sym_group_carrier: "p \ carrier (sym_group n) \ p permutes {1..n}"
  unfolding sym_group_def by simp

lemma sym_group_mult: "mult (sym_group n) = (\)"
  unfolding sym_group_def by simp

lemma sym_group_one: "one (sym_group n) = id"
  unfolding sym_group_def by simp

lemma sym_group_carrier': "p \ carrier (sym_group n) \ permutation p"
  unfolding sym_group_carrier permutation_permutes by auto

lemma alt_group_carrier: "p \ carrier (alt_group n) \ p permutes {1..n} \ evenperm p"
  unfolding alt_group_def by auto

lemma alt_group_mult: "mult (alt_group n) = (\)"
  unfolding alt_group_def using sym_group_mult by simp

lemma alt_group_one: "one (alt_group n) = id"
  unfolding alt_group_def using sym_group_one by simp

lemma alt_group_carrier': "p \ carrier (alt_group n) \ permutation p"
  unfolding alt_group_carrier permutation_permutes by auto

lemma sym_group_is_group: "group (sym_group n)"
  using permutes_inv permutes_inv_o(2)
  by (auto intro!: groupI
         simp add: sym_group_def permutes_compose
                   permutes_id comp_assoc, blast)

lemma sign_img_is_group: "group sign_img"
  unfolding sign_img_def by (unfold_locales, auto simp add: Units_def)

lemma sym_group_inv_closed:
  assumes "p \ carrier (sym_group n)" shows "inv' p \ carrier (sym_group n)"
  using assms permutes_inv sym_group_def by auto

lemma alt_group_inv_closed:
  assumes "p \ carrier (alt_group n)" shows "inv' p \ carrier (alt_group n)"
  using evenperm_inv[OF alt_group_carrier'] permutes_inv assms alt_group_carrier by auto

lemma sym_group_inv_equality [simp]:
  assumes "p \ carrier (sym_group n)" shows "inv\<^bsub>(sym_group n)\<^esub> p = inv' p"
proof -
  have "inv' p \ p = id"
    using assms permutes_inv_o(2) sym_group_def by auto
  hence "(inv' p) \\<^bsub>(sym_group n)\<^esub> p = one (sym_group n)"
    by (simp add: sym_group_def)
  thus ?thesis  using group.inv_equality[OF sym_group_is_group]
    by (simp add: assms sym_group_inv_closed)
qed

lemma sign_is_hom: "sign \ hom (sym_group n) sign_img"
  unfolding hom_def sign_img_def sym_group_mult using sym_group_carrier'[of _ n]
  by (auto simp add: sign_compose, meson sign_def)

lemma sign_group_hom: "group_hom (sym_group n) sign_img sign"
  using group_hom.intro[OF sym_group_is_group sign_img_is_group] sign_is_hom
  by (simp add: group_hom_axioms_def)

lemma sign_is_surj:
  assumes "n \ 2" shows "sign ` (carrier (sym_group n)) = carrier sign_img"
proof -
  have "swapidseq (Suc 0) (Fun.swap (1 :: nat) 2 id)"
    using comp_Suc[OF id, of "1 :: nat" "2"] by auto
  hence "sign (Fun.swap (1 :: nat) 2 id) = (-1 :: int)"
    by (simp add: sign_swap_id)
  moreover have "Fun.swap (1 :: nat) 2 id \ carrier (sym_group n)" and "id \ carrier (sym_group n)"
    using assms permutes_swap_id[of "1 :: nat" "{1..n}" 2] permutes_id
    unfolding sym_group_carrier by auto
  ultimately have "carrier sign_img \ sign ` (carrier (sym_group n))"
    using sign_id mk_disjoint_insert unfolding sign_img_def by fastforce
  moreover have "sign ` (carrier (sym_group n)) \ carrier sign_img"
    using sign_is_hom unfolding hom_def by auto
  ultimately show ?thesis
    by blast
qed

lemma alt_group_is_sign_kernel:
  "carrier (alt_group n) = kernel (sym_group n) sign_img sign"
  unfolding alt_group_def sym_group_def sign_img_def kernel_def sign_def by auto

lemma alt_group_is_subgroup: "subgroup (carrier (alt_group n)) (sym_group n)"
  using group_hom.subgroup_kernel[OF sign_group_hom]
  unfolding alt_group_is_sign_kernel by blast

lemma alt_group_is_group: "group (alt_group n)"
  using group.subgroup_imp_group[OF sym_group_is_group alt_group_is_subgroup]
  by (simp add: alt_group_def)

lemma sign_iso:
  assumes "n \ 2" shows "(sym_group n) Mod (carrier (alt_group n)) \ sign_img"
  using group_hom.FactGroup_iso[OF sign_group_hom sign_is_surj[OF assms]]
  unfolding alt_group_is_sign_kernel .

lemma alt_group_inv_equality:
  assumes "p \ carrier (alt_group n)" shows "inv\<^bsub>(alt_group n)\<^esub> p = inv' p"
proof -
  have "inv' p \ p = id"
    using assms permutes_inv_o(2) alt_group_def by auto
  hence "(inv' p) \\<^bsub>(alt_group n)\<^esub> p = one (alt_group n)"
    by (simp add: alt_group_def sym_group_def)
  thus ?thesis  using group.inv_equality[OF alt_group_is_group]
    by (simp add: assms alt_group_inv_closed)
qed

lemma sym_group_card_carrier: "card (carrier (sym_group n)) = fact n"
  using card_permutations[of "{1..n}" n] unfolding sym_group_def by simp

lemma alt_group_card_carrier:
  assumes "n \ 2" shows "2 * card (carrier (alt_group n)) = fact n"
proof -
  have "card (rcosets\<^bsub>sym_group n\<^esub> (carrier (alt_group n))) = 2"
    using iso_same_card[OF sign_iso[OF assms]] unfolding FactGroup_def sign_img_def by auto
  thus ?thesis
    using group.lagrange[OF sym_group_is_group alt_group_is_subgroup, of n]
    unfolding order_def sym_group_card_carrier by simp
qed

subsection \<open>Transposition Sequences\<close>

text \<open>In order to prove that the Alternating Group can be generated by 3-cycles, we need
      a stronger decomposition of permutations as transposition sequences than the one
      proposed at Permutations.thy. \<close>

inductive swapidseq_ext :: "'a set \ nat \ ('a \ 'a) \ bool"
  where
    empty:  "swapidseq_ext {} 0 id"
  | single: "\ swapidseq_ext S n p; a \ S \ \ swapidseq_ext (insert a S) n p"
  | comp:   "\ swapidseq_ext S n p; a \ b \ \
               swapidseq_ext (insert a (insert b S)) (Suc n) ((Fun.swap a b id) \<circ> p)"

lemma swapidseq_ext_finite:
  assumes "swapidseq_ext S n p" shows "finite S"
  using assms by (induction) (auto)

lemma swapidseq_ext_zero:
  assumes "finite S" shows "swapidseq_ext S 0 id"
  using assms empty by (induct set: "finite", fastforce, simp add: single)

lemma swapidseq_ext_imp_swapidseq:
  assumes "swapidseq_ext S n p" shows "swapidseq n p"
  using assms by (induction, simp, simp, meson comp_Suc)

lemma swapidseq_ext_zero_imp_id:
  assumes "swapidseq_ext S 0 p" shows "p = id"
proof -
  have "\ swapidseq_ext S n p; n = 0 \ \ p = id" for n
    by (induction rule: swapidseq_ext.induct, auto)
  thus ?thesis
    using assms by simp
qed

lemma swapidseq_ext_finite_expansion:
  assumes "finite B" and "swapidseq_ext A n p" shows "swapidseq_ext (A \ B) n p"
  using assms
proof (induct set: "finite", simp)
  case (insert b B) show ?case
    using insert single[OF insert(3), of b] by (metis Un_insert_right insert_absorb)
qed

lemma swapidseq_ext_backwards:
  assumes "swapidseq_ext A (Suc n) p"
  shows "\a b A' p'. a \ b \ A = (insert a (insert b A')) \
                     swapidseq_ext A' n p' \<and> p = (Fun.swap a b id) \<circ> p'"
proof -
  { fix A n k and p :: "'a \ 'a"
    assume "swapidseq_ext A n p" "n = Suc k"
    hence "\a b A' p'. a \ b \ A = (insert a (insert b A')) \
                       swapidseq_ext A' k p' \<and> p = (Fun.swap a b id) \<circ> p'"
    proof (induction, simp)
      case single thus ?case
        by (metis Un_insert_right insert_iff insert_is_Un swapidseq_ext.single)
    next
      case comp thus ?case
        by blast
    qed }
  thus ?thesis
    using assms by simp
qed

lemma swapidseq_ext_backwards':
  assumes "swapidseq_ext A (Suc n) p"
  shows "\a b A' p'. a \ A \ b \ A \ a \ b \ swapidseq_ext A n p' \ p = (Fun.swap a b id) \ p'"
  using swapidseq_ext_backwards[OF assms] swapidseq_ext_finite_expansion
  by (metis Un_insert_left assms insertI1 sup.idem sup_commute swapidseq_ext_finite)

lemma swapidseq_ext_endswap:
  assumes "swapidseq_ext S n p" "a \ b"
  shows "swapidseq_ext (insert a (insert b S)) (Suc n) (p \ (Fun.swap a b id))"
  using assms
proof (induction n arbitrary: S p a b)
  case 0 hence "p = id"
    using swapidseq_ext_zero_imp_id by blast
  thus ?case
    using 0 by (metis comp_id id_comp swapidseq_ext.comp)
next
  case (Suc n)
  then obtain c d S' and p' :: "'a \ 'a"
    where cd: "c \ d" and S: "S = (insert c (insert d S'))" "swapidseq_ext S' n p'"
      and p: "p = (Fun.swap c d id) \ p'"
    using swapidseq_ext_backwards[OF Suc(2)] by blast
  hence "swapidseq_ext (insert a (insert b S')) (Suc n) (p' \ (Fun.swap a b id))"
    by (simp add: Suc.IH Suc.prems(2))
  hence "swapidseq_ext (insert c (insert d (insert a (insert b S')))) (Suc (Suc n))
                 ((Fun.swap c d id) \<circ> p' \<circ> (Fun.swap a b id))"
    by (metis cd fun.map_comp swapidseq_ext.comp)
  thus ?case
    by (metis S(1) p insert_commute)
qed

lemma swapidseq_ext_extension:
  assumes "swapidseq_ext A n p" and "swapidseq_ext B m q" and "A \ B = {}"
  shows "swapidseq_ext (A \ B) (n + m) (p \ q)"
  using assms(1,3)
proof (induction, simp add: assms(2))
  case single show ?case
    using swapidseq_ext.single[OF single(3)] single(2,4) by auto
next
  case comp show ?case
    using swapidseq_ext.comp[OF comp(3,2)] comp(4)
    by (metis Un_insert_left add_Suc insert_disjoint(1) o_assoc)
qed

lemma swapidseq_ext_of_cycles:
  assumes "cycle cs" shows "swapidseq_ext (set cs) (length cs - 1) (cycle_of_list cs)"
  using assms
proof (induct cs rule: cycle_of_list.induct)
  case (1 i j cs) show ?case
    using comp[OF 1(1), of i j] 1(2) by (simp add: o_def)
next
  case "2_1" show ?case
    by (simp, metis eq_id_iff empty)
next
  case ("2_2" v) show ?case
    using single[OF empty, of v] by (simp, metis eq_id_iff)
qed

lemma cycle_decomp_imp_swapidseq_ext:
  assumes "cycle_decomp S p" shows "\n. swapidseq_ext S n p"
  using assms
proof (induction)
  case empty show ?case
    using swapidseq_ext.empty by blast
next
  case (comp I p cs)
  then obtain m where m: "swapidseq_ext I m p" by blast
  hence "swapidseq_ext (set cs) (length cs - 1) (cycle_of_list cs)"
    using comp.hyps(2) swapidseq_ext_of_cycles by blast
  thus ?case using swapidseq_ext_extension m
    using comp.hyps(3) by blast
qed

lemma swapidseq_ext_of_permutation:
  assumes "p permutes S" and "finite S" shows "\n. swapidseq_ext S n p"
  using cycle_decomp_imp_swapidseq_ext[OF cycle_decomposition[OF assms]] .

lemma split_swapidseq_ext:
  assumes "k \ n" and "swapidseq_ext S n p"
  obtains q r U V where "swapidseq_ext U (n - k) q" and "swapidseq_ext V k r" and "p = q \ r" and "U \ V = S"
proof -
  from assms
  have "\q r U V. swapidseq_ext U (n - k) q \ swapidseq_ext V k r \ p = q \ r \ U \ V = S"
   (is "\q r U V. ?split k q r U V")
  proof (induct k rule: inc_induct)
    case base thus ?case
      by (metis diff_self_eq_0 id_o sup_bot.left_neutral empty)
  next
    case (step m)
    then obtain q r U V
      where q: "swapidseq_ext U (n - Suc m) q" and r: "swapidseq_ext V (Suc m) r"
        and p: "p = q \ r" and S: "U \ V = S"
      by blast
    obtain a b r' V'
      where "a \ b" and r': "V = (insert a (insert b V'))" "swapidseq_ext V' m r'" "r = (Fun.swap a b id) \ r'"
      using swapidseq_ext_backwards[OF r] by blast
    have "swapidseq_ext (insert a (insert b U)) (n - m) (q \ (Fun.swap a b id))"
      using swapidseq_ext_endswap[OF q \<open>a \<noteq> b\<close>] step(2) by (metis Suc_diff_Suc)
    hence "?split m (q \ (Fun.swap a b id)) r' (insert a (insert b U)) V'"
      using r' S unfolding p by fastforce
    thus ?case by blast
  qed
  thus ?thesis
    using that by blast
qed

subsection \<open>Unsolvability of Symmetric Groups\<close>

text \<open>We show that symmetric groups (\<^term>\<open>sym_group n\<close>) are unsolvable for \<^term>\<open>n \<ge> 5\<close>.\<close>

abbreviation three_cycles :: "nat \ (nat \ nat) set"
  where "three_cycles n \
           { cycle_of_list cs | cs. cycle cs \<and> length cs = 3 \<and> set cs \<subseteq> {1..n} }"

lemma stupid_lemma:
  assumes "length cs = 3" shows "cs = [ (cs ! 0), (cs ! 1), (cs ! 2) ]"
  using assms by (auto intro!: nth_equalityI)
    (metis Suc_lessI less_2_cases not_less_eq nth_Cons_0
           nth_Cons_Suc numeral_2_eq_2 numeral_3_eq_3)

lemma three_cycles_incl: "three_cycles n \ carrier (alt_group n)"
proof
  fix p assume "p \ three_cycles n"
  then obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \ {1..n}"
    by auto
  obtain a b c where cs_def: "cs = [ a, b, c ]"
    using stupid_lemma[OF cs(3)] by auto
  have "swapidseq (Suc (Suc 0)) ((Fun.swap a b id) \ (Fun.swap b c id))"
    using comp_Suc[OF comp_Suc[OF id], of b c a b] cs(2) unfolding cs_def by simp
  hence "evenperm p"
    using cs(1) unfolding cs_def by (simp add: evenperm_unique)
  thus "p \ carrier (alt_group n)"
    using permutes_subset[OF cycle_permutes cs(4)]
    unfolding alt_group_carrier cs(1) by simp
qed

lemma alt_group_carrier_as_three_cycles:
  "carrier (alt_group n) = generate (alt_group n) (three_cycles n)"
proof -
  interpret A: group "alt_group n"
    using alt_group_is_group by simp

  show ?thesis
  proof
    show "generate (alt_group n) (three_cycles n) \ carrier (alt_group n)"
      using A.generate_subgroup_incl[OF three_cycles_incl A.subgroup_self] .
  next
    show "carrier (alt_group n) \ generate (alt_group n) (three_cycles n)"
    proof
      { fix q :: "nat \ nat" and a b c
        assume "a \ b" "b \ c" "{ a, b, c } \ {1..n}"
        have "cycle_of_list [a, b, c] \ generate (alt_group n) (three_cycles n)"
        proof (cases)
          assume "c = a"
          hence "cycle_of_list [ a, b, c ] = id"
            by (simp add: swap_commute)
          thus "cycle_of_list [ a, b, c ] \ generate (alt_group n) (three_cycles n)"
            using one[of "alt_group n"] unfolding alt_group_one by simp
        next
          assume "c \ a"
          have "distinct [a, b, c]"
            using \<open>a \<noteq> b\<close> and \<open>b \<noteq> c\<close> and \<open>c \<noteq> a\<close> by auto
          with \<open>{ a, b, c } \<subseteq> {1..n}\<close>
          show "cycle_of_list [ a, b, c ] \ generate (alt_group n) (three_cycles n)"
            by (intro incl, fastforce)
        qed } note aux_lemma1 = this

      { fix S :: "nat set" and q :: "nat \ nat"
        assume seq: "swapidseq_ext S (Suc (Suc 0)) q" and S: "S \ {1..n}"
        have "q \ generate (alt_group n) (three_cycles n)"
        proof -
          obtain a b q' where ab: "a \ b" "a \ S" "b \ S"
            and q': "swapidseq_ext S (Suc 0) q'" "q = (Fun.swap a b id) \<circ> q'"
            using swapidseq_ext_backwards'[OF seq] by auto
          obtain c d where cd: "c \ d" "c \ S" "d \ S"
            and q: "q = (Fun.swap a b id) \ (Fun.swap c d id)"
            using swapidseq_ext_backwards'[OF q'(1)]
                  swapidseq_ext_zero_imp_id
            unfolding q'(2)
            by fastforce

          consider (eq) "b = c" | (ineq) "b \ c" by auto
          thus ?thesis
          proof cases
            case eq then have "q = cycle_of_list [ a, b, d ]"
              unfolding q by simp
            moreover have "{ a, b, d } \ {1..n}"
              using ab cd S by blast
            ultimately show ?thesis
              using aux_lemma1[OF ab(1)] cd(1) eq by simp
          next
            case ineq
            hence "q = cycle_of_list [ a, b, c ] \ cycle_of_list [ b, c, d ]"
              unfolding q by (simp add: comp_swap)
            moreover have "{ a, b, c } \ {1..n}" and "{ b, c, d } \ {1..n}"
              using ab cd S by blast+
            ultimately show ?thesis
              using eng[OF aux_lemma1[OF ab(1) ineq] aux_lemma1[OF ineq cd(1)]]
              unfolding alt_group_mult by simp
          qed
        qed } note aux_lemma2 = this

      fix p assume "p \ carrier (alt_group n)" then have p: "p permutes {1..n}" "evenperm p"
        unfolding alt_group_carrier by auto
      obtain m where m: "swapidseq_ext {1..n} m p"
        using swapidseq_ext_of_permutation[OF p(1)] by auto
      have "even m"
        using swapidseq_ext_imp_swapidseq[OF m] p(2) evenperm_unique by blast
      then obtain k where k: "m = 2 * k"
        by auto
      show "p \ generate (alt_group n) (three_cycles n)"
        using m unfolding k
      proof (induct k arbitrary: p)
        case 0 then have "p = id"
          using swapidseq_ext_zero_imp_id by simp
        show ?case
          using generate.one[of "alt_group n" "three_cycles n"]
          unfolding alt_group_one \<open>p = id\<close> .
      next
        case (Suc m)
        have arith: "2 * (Suc m) - (Suc (Suc 0)) = 2 * m" and "Suc (Suc 0) \ 2 * Suc m"
          by auto
        then obtain q r U V
          where q: "swapidseq_ext U (2 * m) q" and r: "swapidseq_ext V (Suc (Suc 0)) r"
            and p: "p = q \ r" and UV: "U \ V = {1..n}"
          using split_swapidseq_ext[OF _ Suc(2), of "Suc (Suc 0)"] unfolding arith by metis
        have "swapidseq_ext {1..n} (2 * m) q"
          using UV q swapidseq_ext_finite_expansion[OF swapidseq_ext_finite[OF r] q] by simp
        thus ?case
          using eng[OF Suc(1) aux_lemma2[OF r], of q] UV unfolding alt_group_mult p by blast
      qed
    qed
  qed
qed

theorem derived_alt_group_const:
  assumes "n \ 5" shows "derived (alt_group n) (carrier (alt_group n)) = carrier (alt_group n)"
proof
  show "derived (alt_group n) (carrier (alt_group n)) \ carrier (alt_group n)"
    using group.derived_in_carrier[OF alt_group_is_group] by simp
next
  { fix p assume "p \ three_cycles n" have "p \ derived (alt_group n) (carrier (alt_group n))"
    proof -
      obtain cs where cs: "p = cycle_of_list cs" "cycle cs" "length cs = 3" "set cs \ {1..n}"
        using \<open>p \<in> three_cycles n\<close> by auto
      then obtain a b c where cs_def: "cs = [ a, b, c ]"
        using stupid_lemma[OF cs(3)] by blast
      have "card (set cs) = 3"
        using cs(2-3)
        by (simp add: distinct_card)

      have "set cs \ {1..n}"
        using assms cs(3) unfolding sym[OF distinct_card[OF cs(2)]] by auto
      then obtain d where d: "d \ set cs" "d \ {1..n}"
        using cs(4) by blast

      hence "cycle (d # cs)" and "length (d # cs) = 4" and "card {1..n} = n"
        using cs(2-3) by auto
      hence "set (d # cs) \ {1..n}"
        using assms unfolding sym[OF distinct_card[OF \<open>cycle (d # cs)\<close>]]
        by (metis Suc_n_not_le_n eval_nat_numeral(3))
      then obtain e where e: "e \ set (d # cs)" "e \ {1..n}"
        using d cs(4) by (metis insert_subset list.simps(15) subsetI subset_antisym)

      define q where "q = (Fun.swap d e id) \ (Fun.swap b c id)"
      hence "bij q"
        by (simp add: bij_comp)
      moreover have "q b = c" and "q c = b"
        using d(1) e(1) unfolding q_def cs_def by simp+
      moreover have "q a = a"
        using d(1) e(1) cs(2) unfolding q_def cs_def by auto
      ultimately have "q \ p \ (inv' q) = cycle_of_list [ a, c, b ]"
        using conjugation_of_cycle[OF cs(2), of q]
        unfolding sym[OF cs(1)] unfolding cs_def by simp
      also have " ... = p \ p"
        using cs(2) unfolding cs(1) cs_def
        by (auto, metis comp_id comp_swap swap_commute swap_triple)
      finally have "q \ p \ (inv' q) = p \ p" .
      moreover have "bij p"
        unfolding cs(1) cs_def by (simp add: bij_comp)
      ultimately have p: "q \ p \ (inv' q) \ (inv' p) = p"
        by (simp add: bijection.intro bijection.inv_comp_right comp_assoc)

      have "swapidseq (Suc (Suc 0)) q"
        using comp_Suc[OF comp_Suc[OF id], of b c d e] e(1) cs(2)  unfolding q_def cs_def by auto
      hence "evenperm q"
        using even_Suc_Suc_iff evenperm_unique by blast
      moreover have "q permutes { d, e, b, c }"
        unfolding q_def by (simp add: permutes_compose permutes_swap_id)
      hence "q permutes {1..n}"
        using cs(4) d(2) e(2) permutes_subset unfolding cs_def by fastforce
      ultimately have "q \ carrier (alt_group n)"
        unfolding alt_group_carrier by simp
      moreover have "p \ carrier (alt_group n)"
        using \<open>p \<in> three_cycles n\<close> three_cycles_incl by blast
      ultimately have "p \ derived_set (alt_group n) (carrier (alt_group n))"
        using p alt_group_inv_equality unfolding alt_group_mult
        by (metis (no_types, lifting) UN_iff singletonI)
      thus "p \ derived (alt_group n) (carrier (alt_group n))"
        unfolding derived_def by (rule incl)
    qed } note aux_lemma = this

  interpret A: group "alt_group n"
    using alt_group_is_group .

  have "generate (alt_group n) (three_cycles n) \ derived (alt_group n) (carrier (alt_group n))"
    using A.generate_subgroup_incl[OF _ A.derived_is_subgroup] aux_lemma by (meson subsetI)
  thus "carrier (alt_group n) \ derived (alt_group n) (carrier (alt_group n))"
    using alt_group_carrier_as_three_cycles by simp
qed

corollary alt_group_is_unsolvable:
  assumes "n \ 5" shows "\ solvable (alt_group n)"
proof (rule ccontr)
  assume "\ \ solvable (alt_group n)"
  then obtain m where "(derived (alt_group n) ^^ m) (carrier (alt_group n)) = { id }"
    using group.solvable_iff_trivial_derived_seq[OF alt_group_is_group] unfolding alt_group_one by blast
  moreover have "(derived (alt_group n) ^^ m) (carrier (alt_group n)) = carrier (alt_group n)"
    using derived_alt_group_const[OF assms] by (induct m) (auto)
  ultimately have card_eq_1: "card (carrier (alt_group n)) = 1"
    by simp
  have ge_2: "n \ 2"
    using assms by simp
  moreover have "2 = fact n"
    using alt_group_card_carrier[OF ge_2] unfolding card_eq_1
    by (metis fact_2 mult.right_neutral of_nat_fact)
  ultimately have "n = 2"
      by (metis antisym_conv fact_ge_self)
  thus False
    using assms by simp
qed

corollary sym_group_is_unsolvable:
  assumes "n \ 5" shows "\ solvable (sym_group n)"
proof -
  interpret Id: group_hom "alt_group n" "sym_group n" id
    using group.canonical_inj_is_hom[OF sym_group_is_group alt_group_is_subgroup] alt_group_def by simp
  show ?thesis
    using Id.inj_hom_imp_solvable alt_group_is_unsolvable[OF assms] by auto
qed

end

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.