author haftmann Fri Dec 08 19:25:47 2017 +0000 (17 months ago) changeset 67165 22a5822f52f7 parent 67164 39f57f0757f1 child 67166 a77d54ef718b
dedicated theory for group closure
```     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.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.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
```