Theory HOL-Computational_Algebra.Group_Closure
theory Group_Closure
imports
Main
begin
context ab_group_add
begin
inductive_set group_closure :: "'a set ⇒ 'a set" for S
where base: "s ∈ insert 0 S ⟹ s ∈ group_closure S"
| diff: "s ∈ group_closure S ⟹ t ∈ group_closure S ⟹ s - t ∈ group_closure S"
lemma zero_in_group_closure [simp]:
"0 ∈ group_closure S"
using group_closure.base [of 0 S] by simp
lemma group_closure_minus_iff [simp]:
"- s ∈ group_closure S ⟷ s ∈ group_closure S"
using group_closure.diff [of 0 S s] group_closure.diff [of 0 S "- s"] by auto
lemma group_closure_add:
"s + t ∈ group_closure S" if "s ∈ group_closure S" and "t ∈ group_closure S"
using that group_closure.diff [of s S "- t"] by auto
lemma group_closure_empty [simp]:
"group_closure {} = {0}"
by (rule ccontr) (auto elim: group_closure.induct)
lemma group_closure_insert_zero [simp]:
"group_closure (insert 0 S) = group_closure S"
by (auto elim: group_closure.induct intro: group_closure.intros)
end
context comm_ring_1
begin
lemma group_closure_scalar_mult_left:
"of_nat n * s ∈ group_closure S" if "s ∈ group_closure S"
using that by (induction n) (auto simp add: algebra_simps intro: group_closure_add)
lemma group_closure_scalar_mult_right:
"s * of_nat n ∈ group_closure S" if "s ∈ group_closure S"
using that group_closure_scalar_mult_left [of s S n] by (simp add: ac_simps)
end
lemma group_closure_abs_iff [simp]:
"¦s¦ ∈ group_closure S ⟷ s ∈ group_closure S" for s :: int
by (simp add: abs_if)
lemma group_closure_mult_left:
"s * t ∈ group_closure S" if "s ∈ group_closure S" for s t :: int
proof -
from that group_closure_scalar_mult_right [of s S "nat ¦t¦"]
have "s * int (nat ¦t¦) ∈ group_closure S"
by (simp only:)
then show ?thesis
by (cases "t ≥ 0") simp_all
qed
lemma group_closure_mult_right:
"s * t ∈ group_closure S" if "t ∈ group_closure S" for s t :: int
using that group_closure_mult_left [of t S s] by (simp add: ac_simps)
context idom
begin
lemma group_closure_mult_all_eq:
"group_closure (times k ` S) = times k ` group_closure S"
proof (rule; rule)
fix s
have *: "k * a + k * b = k * (a + b)"
"k * a - k * b = k * (a - b)" for a b
by (simp_all add: algebra_simps)
assume "s ∈ group_closure (times k ` S)"
then show "s ∈ times k ` group_closure S"
by induction (auto simp add: * image_iff intro: group_closure.base group_closure.diff bexI [of _ 0])
next
fix s
assume "s ∈ times k ` group_closure S"
then obtain r where r: "r ∈ group_closure S" and s: "s = k * r"
by auto
from r have "k * r ∈ group_closure (times k ` S)"
by (induction arbitrary: s) (auto simp add: algebra_simps intro: group_closure.intros)
with s show "s ∈ group_closure (times k ` S)"
by simp
qed
end
lemma Gcd_group_closure_eq_Gcd:
"Gcd (group_closure S) = Gcd S" for S :: "int set"
proof (rule associated_eqI)
have "Gcd S dvd s" if "s ∈ group_closure S" for s
using that by induction auto
then show "Gcd S dvd Gcd (group_closure S)"
by auto
have "Gcd (group_closure S) dvd s" if "s ∈ S" for s
proof -
from that have "s ∈ group_closure S"
by (simp add: group_closure.base)
then show ?thesis
by (rule Gcd_dvd)
qed
then show "Gcd (group_closure S) dvd Gcd S"
by auto
qed simp_all
lemma group_closure_sum:
fixes S :: "int set"
assumes X: "finite X" "X ≠ {}" "X ⊆ S"
shows "(∑x∈X. a x * x) ∈ group_closure S"
using X by (induction X rule: finite_ne_induct)
(auto intro: group_closure_mult_right group_closure.base group_closure_add)
lemma Gcd_group_closure_in_group_closure:
"Gcd (group_closure S) ∈ group_closure S" for S :: "int set"
proof (cases "S ⊆ {0}")
case True
then have "S = {} ∨ S = {0}"
by auto
then show ?thesis
by auto
next
case False
then obtain s where s: "s ≠ 0" "s ∈ S"
by auto
then have s': "¦s¦ ≠ 0" "¦s¦ ∈ group_closure S"
by (auto intro: group_closure.base)
define m where "m = (LEAST n. n > 0 ∧ int n ∈ group_closure S)"
have "m > 0 ∧ int m ∈ group_closure S"
unfolding m_def
apply (rule LeastI [of _ "nat ¦s¦"])
using s'
by simp
then have m: "int m ∈ group_closure S" and "0 < m"
by auto
have "Gcd (group_closure S) = int m"
proof (rule associated_eqI)
from m show "Gcd (group_closure S) dvd int m"
by (rule Gcd_dvd)
show "int m dvd Gcd (group_closure S)"
proof (rule Gcd_greatest)
fix s
assume s: "s ∈ group_closure S"
show "int m dvd s"
proof (rule ccontr)
assume "¬ int m dvd s"
then have *: "0 < s mod int m"
using ‹0 < m› le_less by fastforce
have "m ≤ nat (s mod int m)"
proof (subst m_def, rule Least_le, rule)
from * show "0 < nat (s mod int m)"
by simp
from minus_div_mult_eq_mod [symmetric, of s "int m"]
have "s mod int m = s - s div int m * int m"
by auto
also have "s - s div int m * int m ∈ group_closure S"
by (auto intro: group_closure.diff s group_closure_mult_right m)
finally show "int (nat (s mod int m)) ∈ group_closure S"
by simp
qed
with * have "int m ≤ s mod int m"
by simp
moreover have "s mod int m < int m"
using ‹0 < m› by simp
ultimately show False
by auto
qed
qed
qed simp_all
with m show ?thesis
by simp
qed
lemma Gcd_in_group_closure:
"Gcd S ∈ group_closure S" for S :: "int set"
using Gcd_group_closure_in_group_closure [of S]
by (simp add: Gcd_group_closure_eq_Gcd)
lemma group_closure_eq:
"group_closure S = range (times (Gcd S))" for S :: "int set"
proof (auto intro: Gcd_in_group_closure group_closure_mult_left)
fix s
assume "s ∈ group_closure S"
then show "s ∈ range (times (Gcd S))"
proof induction
case (base s)
then have "Gcd S dvd s"
by (auto intro: Gcd_dvd)
then obtain t where "s = Gcd S * t" ..
then show ?case
by auto
next
case (diff s t)
moreover have "Gcd S * a - Gcd S * b = Gcd S * (a - b)" for a b
by (simp add: algebra_simps)
ultimately show ?case
by auto
qed
qed
end