dedicated theory for group closure
authorhaftmann
Fri Dec 08 19:25:47 2017 +0000 (17 months ago)
changeset 6716522a5822f52f7
parent 67164 39f57f0757f1
child 67166 a77d54ef718b
dedicated theory for group closure
src/HOL/Computational_Algebra/Computational_Algebra.thy
src/HOL/Computational_Algebra/Group_Closure.thy
     1.1 --- a/src/HOL/Computational_Algebra/Computational_Algebra.thy	Fri Dec 08 17:57:29 2017 +0100
     1.2 +++ b/src/HOL/Computational_Algebra/Computational_Algebra.thy	Fri Dec 08 19:25:47 2017 +0000
     1.3 @@ -8,6 +8,7 @@
     1.4    Formal_Power_Series
     1.5    Fraction_Field
     1.6    Fundamental_Theorem_Algebra
     1.7 +  Group_Closure
     1.8    Normalized_Fraction
     1.9    Nth_Powers
    1.10    Polynomial_FPS
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Computational_Algebra/Group_Closure.thy	Fri Dec 08 19:25:47 2017 +0000
     2.3 @@ -0,0 +1,210 @@
     2.4 +(*  Title:      HOL/Computational_Algebra/Field_as_Ring.thy
     2.5 +    Author:     Johannes Hoelzl, TU Muenchen
     2.6 +    Author:     Florian Haftmann, TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +theory Group_Closure
    2.10 +imports
    2.11 +  Main
    2.12 +begin
    2.13 +
    2.14 +context ab_group_add
    2.15 +begin
    2.16 +
    2.17 +inductive_set group_closure :: "'a set \<Rightarrow> 'a set" for S
    2.18 +  where base: "s \<in> insert 0 S \<Longrightarrow> s \<in> group_closure S"
    2.19 +| diff: "s \<in> group_closure S \<Longrightarrow> t \<in> group_closure S \<Longrightarrow> s - t \<in> group_closure S"
    2.20 +
    2.21 +lemma zero_in_group_closure [simp]:
    2.22 +  "0 \<in> group_closure S"
    2.23 +  using group_closure.base [of 0 S] by simp
    2.24 +
    2.25 +lemma group_closure_minus_iff [simp]:
    2.26 +  "- s \<in> group_closure S \<longleftrightarrow> s \<in> group_closure S"
    2.27 +  using group_closure.diff [of 0 S s] group_closure.diff [of 0 S "- s"] by auto
    2.28 +
    2.29 +lemma group_closure_add:
    2.30 +  "s + t \<in> group_closure S" if "s \<in> group_closure S" and "t \<in> group_closure S"
    2.31 +  using that group_closure.diff [of s S "- t"] by auto
    2.32 +
    2.33 +lemma group_closure_empty [simp]:
    2.34 +  "group_closure {} = {0}"
    2.35 +  by (rule ccontr) (auto elim: group_closure.induct)
    2.36 +
    2.37 +lemma group_closure_insert_zero [simp]:
    2.38 +  "group_closure (insert 0 S) = group_closure S"
    2.39 +  by (auto elim: group_closure.induct intro: group_closure.intros)
    2.40 +
    2.41 +end
    2.42 +
    2.43 +context comm_ring_1
    2.44 +begin
    2.45 +
    2.46 +lemma group_closure_scalar_mult_left:
    2.47 +  "of_nat n * s \<in> group_closure S" if "s \<in> group_closure S"
    2.48 +  using that by (induction n) (auto simp add: algebra_simps intro: group_closure_add)
    2.49 +
    2.50 +lemma group_closure_scalar_mult_right:
    2.51 +  "s * of_nat n \<in> group_closure S" if "s \<in> group_closure S"
    2.52 +  using that group_closure_scalar_mult_left [of s S n] by (simp add: ac_simps)
    2.53 +
    2.54 +end
    2.55 +
    2.56 +lemma group_closure_abs_iff [simp]:
    2.57 +  "\<bar>s\<bar> \<in> group_closure S \<longleftrightarrow> s \<in> group_closure S" for s :: int
    2.58 +  by (simp add: abs_if)
    2.59 +
    2.60 +lemma group_closure_mult_left:
    2.61 +  "s * t \<in> group_closure S" if "s \<in> group_closure S" for s t :: int
    2.62 +proof -
    2.63 +  from that group_closure_scalar_mult_right [of s S "nat \<bar>t\<bar>"]
    2.64 +    have "s * int (nat \<bar>t\<bar>) \<in> group_closure S"
    2.65 +    by (simp only:)
    2.66 +  then show ?thesis
    2.67 +    by (cases "t \<ge> 0") simp_all
    2.68 +qed
    2.69 +
    2.70 +lemma group_closure_mult_right:
    2.71 +  "s * t \<in> group_closure S" if "t \<in> group_closure S" for s t :: int
    2.72 +  using that group_closure_mult_left [of t S s] by (simp add: ac_simps)
    2.73 +
    2.74 +context idom
    2.75 +begin
    2.76 +
    2.77 +lemma group_closure_mult_all_eq:
    2.78 +  "group_closure (times k ` S) = times k ` group_closure S"
    2.79 +proof (rule; rule)
    2.80 +  fix s
    2.81 +  have *: "k * a + k * b = k * (a + b)"
    2.82 +    "k * a - k * b = k * (a - b)" for a b
    2.83 +    by (simp_all add: algebra_simps)
    2.84 +  assume "s \<in> group_closure (times k ` S)"
    2.85 +  then show "s \<in> times k ` group_closure S"
    2.86 +    by induction (auto simp add: * image_iff intro: group_closure.base group_closure.diff bexI [of _ 0])
    2.87 +next
    2.88 +  fix s
    2.89 +  assume "s \<in> times k ` group_closure S"
    2.90 +  then obtain r where r: "r \<in> group_closure S" and s: "s = k * r"
    2.91 +    by auto
    2.92 +  from r have "k * r \<in> group_closure (times k ` S)"
    2.93 +    by (induction arbitrary: s) (auto simp add: algebra_simps intro: group_closure.intros)
    2.94 +  with s show "s \<in> group_closure (times k ` S)"
    2.95 +    by simp
    2.96 +qed
    2.97 +
    2.98 +end
    2.99 +
   2.100 +lemma Gcd_group_closure_eq_Gcd:
   2.101 +  "Gcd (group_closure S) = Gcd S" for S :: "int set"
   2.102 +proof (rule associated_eqI)
   2.103 +  have "Gcd S dvd s" if "s \<in> group_closure S" for s
   2.104 +    using that by induction auto
   2.105 +  then show "Gcd S dvd Gcd (group_closure S)"
   2.106 +    by auto
   2.107 +  have "Gcd (group_closure S) dvd s" if "s \<in> S" for s
   2.108 +  proof -
   2.109 +    from that have "s \<in> group_closure S"
   2.110 +      by (simp add: group_closure.base)
   2.111 +    then show ?thesis
   2.112 +      by (rule Gcd_dvd)
   2.113 +  qed
   2.114 +  then show "Gcd (group_closure S) dvd Gcd S"
   2.115 +    by auto
   2.116 +qed simp_all
   2.117 +
   2.118 +lemma group_closure_sum:
   2.119 +  fixes S :: "int set"
   2.120 +  assumes X: "finite X" "X \<noteq> {}" "X \<subseteq> S"
   2.121 +  shows "(\<Sum>x\<in>X. a x * x) \<in> group_closure S"
   2.122 +  using X by (induction X rule: finite_ne_induct)
   2.123 +    (auto intro: group_closure_mult_right group_closure.base group_closure_add)
   2.124 +
   2.125 +lemma Gcd_group_closure_in_group_closure:
   2.126 +  "Gcd (group_closure S) \<in> group_closure S" for S :: "int set"
   2.127 +proof (cases "S \<subseteq> {0}")
   2.128 +  case True
   2.129 +  then have "S = {} \<or> S = {0}"
   2.130 +    by auto
   2.131 +  then show ?thesis
   2.132 +    by auto
   2.133 +next
   2.134 +  case False
   2.135 +  then obtain s where s: "s \<noteq> 0" "s \<in> S"
   2.136 +    by auto
   2.137 +  then have s': "\<bar>s\<bar> \<noteq> 0" "\<bar>s\<bar> \<in> group_closure S"
   2.138 +    by (auto intro: group_closure.base)
   2.139 +  define m where "m = (LEAST n. n > 0 \<and> int n \<in> group_closure S)"
   2.140 +  have "m > 0 \<and> int m \<in> group_closure S"
   2.141 +    unfolding m_def
   2.142 +    apply (rule LeastI [of _ "nat \<bar>s\<bar>"])
   2.143 +    using s'
   2.144 +    by simp
   2.145 +  then have m: "int m \<in> group_closure S" and "0 < m"
   2.146 +    by auto
   2.147 +
   2.148 +  have "Gcd (group_closure S) = int m"
   2.149 +  proof (rule associated_eqI)
   2.150 +    from m show "Gcd (group_closure S) dvd int m"
   2.151 +      by (rule Gcd_dvd)
   2.152 +    show "int m dvd Gcd (group_closure S)"
   2.153 +    proof (rule Gcd_greatest)
   2.154 +      fix s
   2.155 +      assume s: "s \<in> group_closure S"
   2.156 +      show "int m dvd s"
   2.157 +      proof (rule ccontr)
   2.158 +        assume "\<not> int m dvd s"
   2.159 +        then have *: "0 < s mod int m"
   2.160 +          using \<open>0 < m\<close> le_less by fastforce
   2.161 +        have "m \<le> nat (s mod int m)"
   2.162 +        proof (subst m_def, rule Least_le, rule)
   2.163 +          from * show "0 < nat (s mod int m)"
   2.164 +            by simp
   2.165 +          from minus_div_mult_eq_mod [symmetric, of s "int m"]
   2.166 +          have "s mod int m = s - s div int m * int m"
   2.167 +            by auto
   2.168 +          also have "s - s div int m * int m \<in> group_closure S"
   2.169 +            by (auto intro: group_closure.diff s group_closure_mult_right m)
   2.170 +          finally  show "int (nat (s mod int m)) \<in> group_closure S"
   2.171 +            by simp
   2.172 +        qed
   2.173 +        with * have "int m \<le> s mod int m"
   2.174 +          by simp
   2.175 +        moreover have "s mod int m < int m"
   2.176 +          using \<open>0 < m\<close> by simp
   2.177 +        ultimately show False
   2.178 +          by auto
   2.179 +      qed
   2.180 +    qed
   2.181 +  qed simp_all
   2.182 +  with m show ?thesis
   2.183 +    by simp
   2.184 +qed
   2.185 +
   2.186 +lemma Gcd_in_group_closure:
   2.187 +  "Gcd S \<in> group_closure S" for S :: "int set"
   2.188 +  using Gcd_group_closure_in_group_closure [of S]
   2.189 +  by (simp add: Gcd_group_closure_eq_Gcd)
   2.190 +
   2.191 +lemma group_closure_eq:
   2.192 +  "group_closure S = range (times (Gcd S))" for S :: "int set"
   2.193 +proof (auto intro: Gcd_in_group_closure group_closure_mult_left)
   2.194 +  fix s
   2.195 +  assume "s \<in> group_closure S"
   2.196 +  then show "s \<in> range (times (Gcd S))"
   2.197 +  proof induction
   2.198 +    case (base s)
   2.199 +    then have "Gcd S dvd s"
   2.200 +      by (auto intro: Gcd_dvd)
   2.201 +    then obtain t where "s = Gcd S * t" ..
   2.202 +    then show ?case
   2.203 +      by auto
   2.204 +  next
   2.205 +    case (diff s t)
   2.206 +    moreover have "Gcd S * a - Gcd S * b = Gcd S * (a - b)" for a b
   2.207 +      by (simp add: algebra_simps)
   2.208 +    ultimately show ?case
   2.209 +      by auto
   2.210 +  qed
   2.211 +qed
   2.212 +
   2.213 +end