Quelle Group_Closure.thy Sprache: Isabelle

(*  Title:      HOL/Computational_Algebra/Group_Closure.thy
    Author:     Johannes Hoelzl, TU Muenchen
    Author:     Florian Haftmann, TU Muenchen
*)

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 \<open>0 < m\<close> 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 \<open>0 < m\<close> 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

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.