Quelle Algebra_Aux.thy Sprache: Isabelle

(*  Title:      HOL/Decision_Procs/Algebra_Aux.thy
    Author:     Stefan Berghofer
*)

section \<open>Things that can be added to the Algebra library\<close>

theory Algebra_Aux
  imports "HOL-Algebra.Ring"
begin

definition of_natural :: "('a, 'm) ring_scheme \ nat \ 'a" (\\_\\<^sub>\\\)
  where "\n\\<^sub>\\<^bsub>R\<^esub> = ((\\<^bsub>R\<^esub>) \\<^bsub>R\<^esub> ^^ n) \\<^bsub>R\<^esub>"

definition of_integer :: "('a, 'm) ring_scheme \ int \ 'a" (\\_\\\)
  where "\i\\<^bsub>R\<^esub> = (if 0 \ i then \nat i\\<^sub>\\<^bsub>R\<^esub> else \\<^bsub>R\<^esub> \nat (- i)\\<^sub>\\<^bsub>R\<^esub>)"

context ring
begin

lemma of_nat_0 [simp]: "\0\\<^sub>\ = \"
  by (simp add: of_natural_def)

lemma of_nat_Suc [simp]: "\Suc n\\<^sub>\ = \ \ \n\\<^sub>\"
  by (simp add: of_natural_def)

lemma of_int_0 [simp]: "\0\ = \"
  by (simp add: of_integer_def)

lemma of_nat_closed [simp]: "\n\\<^sub>\ \ carrier R"
  by (induct n) simp_all

lemma of_int_closed [simp]: "\i\ \ carrier R"
  by (simp add: of_integer_def)

lemma of_int_minus [simp]: "\- i\ = \ \i\"
  by (simp add: of_integer_def)

lemma of_nat_add [simp]: "\m + n\\<^sub>\ = \m\\<^sub>\ \ \n\\<^sub>\"
  by (induct m) (simp_all add: a_ac)

lemma of_nat_diff [simp]: "n \ m \ \m - n\\<^sub>\ = \m\\<^sub>\ \ \n\\<^sub>\"
proof (induct m arbitrary: n)
  case 0
  then show ?case by (simp add: minus_eq)
next
  case Suc': (Suc m)
  show ?case
  proof (cases n)
    case 0
    then show ?thesis
      by (simp add: minus_eq)
  next
    case (Suc k)
    with Suc' have "\Suc m - Suc k\\<^sub>\ = \m\\<^sub>\ \ \k\\<^sub>\" by simp
    also have "\ = \ \ \ \ \ (\m\\<^sub>\ \ \k\\<^sub>\)"
      by (simp add: r_neg)
    also have "\ = \Suc m\\<^sub>\ \ \Suc k\\<^sub>\"
      by (simp add: minus_eq minus_add a_ac)
    finally show ?thesis using Suc by simp
  qed
qed

lemma of_int_add [simp]: "\i + j\ = \i\ \ \j\"
proof (cases "0 \ i")
  case True
  show ?thesis
  proof (cases "0 \ j")
    case True
    with \<open>0 \<le> i\<close> show ?thesis
      by (simp add: of_integer_def nat_add_distrib)
  next
    case False
    show ?thesis
    proof (cases "0 \ i + j")
      case True
      then have "\i + j\ = \nat (i - (- j))\\<^sub>\"
        by (simp add: of_integer_def)
      also from True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
      have "nat (i - (- j)) = nat i - nat (- j)"
        by (simp add: nat_diff_distrib)
      finally show ?thesis using True \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
        by (simp add: minus_eq of_integer_def)
    next
      case False
      then have "\i + j\ = \ \nat (- j - i)\\<^sub>\"
        by (simp add: of_integer_def) (simp only: diff_conv_add_uminus add_ac)
      also from False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
      have "nat (- j - i) = nat (- j) - nat i"
        by (simp add: nat_diff_distrib)
      finally show ?thesis using False \<open>0 \<le> i\<close> \<open>\<not> 0 \<le> j\<close>
        by (simp add: minus_eq minus_add a_ac of_integer_def)
    qed
  qed
next
  case False
  show ?thesis
  proof (cases "0 \ j")
    case True
    show ?thesis
    proof (cases "0 \ i + j")
      case True
      then have "\i + j\ = \nat (j - (- i))\\<^sub>\"
        by (simp add: of_integer_def add_ac)
      also from True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
      have "nat (j - (- i)) = nat j - nat (- i)"
        by (simp add: nat_diff_distrib)
      finally show ?thesis using True \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
        by (simp add: minus_eq minus_add a_ac of_integer_def)
    next
      case False
      then have "\i + j\ = \ \nat (- i - j)\\<^sub>\"
        by (simp add: of_integer_def)
      also from False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
      have "nat (- i - j) = nat (- i) - nat j"
        by (simp add: nat_diff_distrib)
      finally show ?thesis using False \<open>\<not> 0 \<le> i\<close> \<open>0 \<le> j\<close>
        by (simp add: minus_eq minus_add of_integer_def)
    qed
  next
    case False
    with \<open>\<not> 0 \<le> i\<close> show ?thesis
      by (simp add: of_integer_def nat_add_distrib minus_add diff_conv_add_uminus
          del: add_uminus_conv_diff uminus_add_conv_diff)
  qed
qed

lemma of_int_diff [simp]: "\i - j\ = \i\ \ \j\"
  by (simp only: diff_conv_add_uminus of_int_add) (simp add: minus_eq)

lemma of_nat_mult [simp]: "\i * j\\<^sub>\ = \i\\<^sub>\ \ \j\\<^sub>\"
  by (induct i) (simp_all add: l_distr)

lemma of_int_mult [simp]: "\i * j\ = \i\ \ \j\"
proof (cases "0 \ i")
  case True
  show ?thesis
  proof (cases "0 \ j")
    case True
    with \<open>0 \<le> i\<close> show ?thesis
      by (simp add: of_integer_def nat_mult_distrib zero_le_mult_iff)
  next
    case False
    with \<open>0 \<le> i\<close> show ?thesis
      by (simp add: of_integer_def zero_le_mult_iff
        minus_mult_right nat_mult_distrib r_minus
        del: minus_mult_right [symmetric])
  qed
next
  case False
  show ?thesis
  proof (cases "0 \ j")
    case True
    with \<open>\<not> 0 \<le> i\<close> show ?thesis
      by (simp add: of_integer_def zero_le_mult_iff
        minus_mult_left nat_mult_distrib l_minus
        del: minus_mult_left [symmetric])
  next
    case False
    with \<open>\<not> 0 \<le> i\<close> show ?thesis
      by (simp add: of_integer_def zero_le_mult_iff
        minus_mult_minus [of i j, symmetric] nat_mult_distrib
        l_minus r_minus
        del: minus_mult_minus
        minus_mult_left [symmetric] minus_mult_right [symmetric])
  qed
qed

lemma of_int_1 [simp]: "\1\ = \"
  by (simp add: of_integer_def)

lemma of_int_2: "\2\ = \ \ \"
  by (simp add: of_integer_def numeral_2_eq_2)

lemma minus_0_r [simp]: "x \ carrier R \ x \ \ = x"
  by (simp add: minus_eq)

lemma minus_0_l [simp]: "x \ carrier R \ \ \ x = \ x"
  by (simp add: minus_eq)

lemma eq_diff0:
  assumes "x \ carrier R" "y \ carrier R"
  shows "x \ y = \ \ x = y"
proof
  assume "x \ y = \"
  with assms have "x \ (\ y \ y) = y"
    by (simp add: minus_eq a_assoc [symmetric])
  with assms show "x = y" by (simp add: l_neg)
next
  assume "x = y"
  with assms show "x \ y = \" by (simp add: minus_eq r_neg)
qed

lemma power2_eq_square: "x \ carrier R \ x [^] (2::nat) = x \ x"
  by (simp add: numeral_eq_Suc)

lemma eq_neg_iff_add_eq_0:
  assumes "x \ carrier R" "y \ carrier R"
  shows "x = \ y \ x \ y = \"
proof
  assume "x = \ y"
  with assms show "x \ y = \" by (simp add: l_neg)
next
  assume "x \ y = \"
  with assms have "x \ (y \ \ y) = \ \ \ y"
    by (simp add: a_assoc [symmetric])
  with assms show "x = \ y"
    by (simp add: r_neg)
qed

lemma neg_equal_iff_equal:
  assumes x: "x \ carrier R" and y: "y \ carrier R"
  shows "\ x = \ y \ x = y"
proof
  assume "\ x = \ y"
  then have "\ (\ x) = \ (\ y)" by simp
  with x y show "x = y" by simp
next
  assume "x = y"
  then show "\ x = \ y" by simp
qed

lemma neg_equal_swap:
  assumes x: "x \ carrier R" and y: "y \ carrier R"
  shows "(\ x = y) = (x = \ y)"
  using assms neg_equal_iff_equal [of x "\ y"]
  by simp

lemma mult2: "x \ carrier R \ x \ x = \2\ \ x"
  by (simp add: of_int_2 l_distr)

end

lemma (in cring) of_int_power [simp]: "\i ^ n\ = \i\ [^] n"
  by (induct n) (simp_all add: m_ac)

definition cring_class_ops :: "'a::comm_ring_1 ring"
  where "cring_class_ops \ \carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\"

lemma cring_class: "cring cring_class_ops"
  apply unfold_locales
  apply (auto simp add: cring_class_ops_def ring_distribs Units_def)
  apply (rule_tac x="- x" in exI)
  apply simp
  done

lemma carrier_class: "x \ carrier cring_class_ops"
  by (simp add: cring_class_ops_def)

lemma zero_class: "\\<^bsub>cring_class_ops\<^esub> = 0"
  by (simp add: cring_class_ops_def)

lemma one_class: "\\<^bsub>cring_class_ops\<^esub> = 1"
  by (simp add: cring_class_ops_def)

lemma plus_class: "x \\<^bsub>cring_class_ops\<^esub> y = x + y"
  by (simp add: cring_class_ops_def)

lemma times_class: "x \\<^bsub>cring_class_ops\<^esub> y = x * y"
  by (simp add: cring_class_ops_def)

lemma uminus_class: "\\<^bsub>cring_class_ops\<^esub> x = - x"
proof -
  have "(THE y::'a. x + y = 0 \ y + x = 0) = - x"
    by (rule the_equality) (simp_all add: eq_neg_iff_add_eq_0)
  then show ?thesis
    by (simp add: a_inv_def m_inv_def cring_class_ops_def)
qed

lemma minus_class: "x \\<^bsub>cring_class_ops\<^esub> y = x - y"
  by (simp add: a_minus_def carrier_class plus_class uminus_class)

lemma power_class: "x [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
  by (induct n) (simp_all add: one_class times_class
    monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]
    monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]])

lemma of_nat_class: "\n\\<^sub>\\<^bsub>cring_class_ops\<^esub> = of_nat n"
  by (induct n) (simp_all add: cring_class_ops_def of_natural_def)

lemma of_int_class: "\i\\<^bsub>cring_class_ops\<^esub> = of_int i"
  by (simp add: of_integer_def of_nat_class uminus_class)

lemmas class_simps = zero_class one_class plus_class minus_class uminus_class
  times_class power_class of_nat_class of_int_class carrier_class

interpretation cring_class: cring "cring_class_ops::'a::comm_ring_1 ring"
  rewrites "(\\<^bsub>cring_class_ops\<^esub>::'a) = 0"
    and "(\\<^bsub>cring_class_ops\<^esub>::'a) = 1"
    and "(x::'a) \\<^bsub>cring_class_ops\<^esub> y = x + y"
    and "(x::'a) \\<^bsub>cring_class_ops\<^esub> y = x * y"
    and "\\<^bsub>cring_class_ops\<^esub> (x::'a) = - x"
    and "(x::'a) \\<^bsub>cring_class_ops\<^esub> y = x - y"
    and "(x::'a) [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    and "\n\\<^sub>\\<^bsub>cring_class_ops\<^esub> = of_nat n"
    and "((\i\\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i"
    and "(Int.of_int (numeral m)::'a) = numeral m"
  by (simp_all add: cring_class class_simps)

lemma (in domain) nat_pow_eq_0_iff [simp]:
  "a \ carrier R \ (a [^] (n::nat) = \) = (a = \ \ n \ 0)"
  by (induct n) (auto simp add: integral_iff)

lemma (in domain) square_eq_iff:
  assumes "x \ carrier R" "y \ carrier R"
  shows "(x \ x = y \ y) = (x = y \ x = \ y)"
proof
  assume "x \ x = y \ y"
  with assms have "(x \ y) \ (x \ y) = x \ y \ \ (x \ y) \ (y \ y \ \ (y \ y))"
    by (simp add: r_distr l_distr minus_eq r_minus m_comm a_ac)
  with assms show "x = y \ x = \ y"
    by (simp add: integral_iff eq_neg_iff_add_eq_0 eq_diff0 r_neg)
next
  assume "x = y \ x = \ y"
  with assms show "x \ x = y \ y"
    by (auto simp add: l_minus r_minus)
qed

definition m_div :: "('a, 'b) ring_scheme \ 'a \ 'a \ 'a" (infixl \\\\ 70)
  where "x \\<^bsub>G\<^esub> y = (if y = \\<^bsub>G\<^esub> then \\<^bsub>G\<^esub> else x \\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"

context field
begin

lemma inv_closed [simp]: "x \ carrier R \ x \ \ \ inv x \ carrier R"
  by (simp add: field_Units)

lemma l_inv [simp]: "x \ carrier R \ x \ \ \ inv x \ x = \"
  by (simp add: field_Units)

lemma r_inv [simp]: "x \ carrier R \ x \ \ \ x \ inv x = \"
  by (simp add: field_Units)

lemma inverse_unique:
  assumes a: "a \ carrier R"
    and b: "b \ carrier R"
    and ab: "a \ b = \"
  shows "inv a = b"
proof -
  from ab b have *: "a \ \"
    by (cases "a = \") simp_all
  with a have "inv a \ (a \ b) = inv a"
    by (simp add: ab)
  with a b * show ?thesis
    by (simp add: m_assoc [symmetric])
qed

lemma nonzero_inverse_inverse_eq: "a \ carrier R \ a \ \ \ inv (inv a) = a"
  by (rule inverse_unique) simp_all

lemma inv_1 [simp]: "inv \ = \"
  by (rule inverse_unique) simp_all

lemma nonzero_inverse_mult_distrib:
  assumes "a \ carrier R" "b \ carrier R"
    and "a \ \" "b \ \"
  shows "inv (a \ b) = inv b \ inv a"
proof -
  from assms have "a \ (b \ inv b) \ inv a = \"
    by simp
  with assms have eq: "a \ b \ (inv b \ inv a) = \"
    by (simp only: m_assoc m_closed inv_closed assms)
  from assms show ?thesis
    using inverse_unique [OF _ _ eq] by simp
qed

lemma nonzero_imp_inverse_nonzero:
  assumes "a \ carrier R" and "a \ \"
  shows "inv a \ \"
proof
  assume *: "inv a = \"
  from assms have **: "\ = a \ inv a"
    by simp
  also from assms have "\ = \" by (simp add: *)
  finally have "\ = \" .
  then show False by (simp add: eq_commute)
qed

lemma nonzero_divide_divide_eq_left:
  "a \ carrier R \ b \ carrier R \ c \ carrier R \ b \ \ \ c \ \ \
    a \<oslash> b \<oslash> c = a \<oslash> (b \<otimes> c)"
  by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)

lemma nonzero_times_divide_eq:
  "a \ carrier R \ b \ carrier R \ c \ carrier R \ d \ carrier R \
    b \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<otimes> (c \<oslash> d) = (a \<otimes> c) \<oslash> (b \<otimes> d)"
  by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)

lemma nonzero_divide_divide_eq:
  "a \ carrier R \ b \ carrier R \ c \ carrier R \ d \ carrier R \
    b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<oslash> (c \<oslash> d) = (a \<otimes> d) \<oslash> (b \<otimes> c)"
  by (simp add: m_div_def nonzero_inverse_mult_distrib
    nonzero_imp_inverse_nonzero nonzero_inverse_inverse_eq m_ac integral_iff)

lemma divide_1 [simp]: "x \ carrier R \ x \ \ = x"
  by (simp add: m_div_def)

lemma add_frac_eq:
  assumes "x \ carrier R" "y \ carrier R" "z \ carrier R" "w \ carrier R"
    and "y \ \" "z \ \"
  shows "x \ y \ w \ z = (x \ z \ w \ y) \ (y \ z)"
proof -
  from assms
  have "x \ y \ w \ z = x \ inv y \ (z \ inv z) \ w \ inv z \ (y \ inv y)"
    by (simp add: m_div_def)
  also from assms have "\ = (x \ z \ w \ y) \ (y \ z)"
    by (simp add: m_div_def nonzero_inverse_mult_distrib r_distr m_ac integral_iff del: r_inv)
  finally show ?thesis .
qed

lemma div_closed [simp]:
  "x \ carrier R \ y \ carrier R \ y \ \ \ x \ y \ carrier R"
  by (simp add: m_div_def)

lemma minus_divide_left [simp]:
  "a \ carrier R \ b \ carrier R \ b \ \ \ \ (a \ b) = \ a \ b"
  by (simp add: m_div_def l_minus)

lemma diff_frac_eq:
  assumes "x \ carrier R" "y \ carrier R" "z \ carrier R" "w \ carrier R"
    and "y \ \" "z \ \"
  shows "x \ y \ w \ z = (x \ z \ w \ y) \ (y \ z)"
  using assms by (simp add: minus_eq l_minus add_frac_eq)

lemma nonzero_mult_divide_mult_cancel_left [simp]:
  assumes "a \ carrier R" "b \ carrier R" "c \ carrier R"
    and "b \ \" "c \ \"
  shows "(c \ a) \ (c \ b) = a \ b"
proof -
  from assms have "(c \ a) \ (c \ b) = c \ a \ (inv b \ inv c)"
    by (simp add: m_div_def nonzero_inverse_mult_distrib integral_iff)
  also from assms have "\ = a \ inv b \ (inv c \ c)"
    by (simp add: m_ac)
  also from assms have "\ = a \ inv b"
    by simp
  finally show ?thesis
    using assms by (simp add: m_div_def)
qed

lemma times_divide_eq_left [simp]:
  "a \ carrier R \ b \ carrier R \ c \ carrier R \ c \ \ \
    (b \<oslash> c) \<otimes> a = b \<otimes> a \<oslash> c"
  by (simp add: m_div_def m_ac)

lemma times_divide_eq_right [simp]:
  "a \ carrier R \ b \ carrier R \ c \ carrier R \ c \ \ \
    a \<otimes> (b \<oslash> c) = a \<otimes> b \<oslash> c"
  by (simp add: m_div_def m_ac)

lemma nonzero_power_divide:
  "a \ carrier R \ b \ carrier R \ b \ \ \
    (a \<oslash> b) [^] (n::nat) = a [^] n \<oslash> b [^] n"
  by (induct n) (simp_all add: nonzero_divide_divide_eq_left)

lemma r_diff_distr:
  "x \ carrier R \ y \ carrier R \ z \ carrier R \
    z \<otimes> (x \<ominus> y) = z \<otimes> x \<ominus> z \<otimes> y"
  by (simp add: minus_eq r_distr r_minus)

lemma divide_zero_left [simp]: "a \ carrier R \ a \ \ \ \ \ a = \"
  by (simp add: m_div_def)

lemma divide_self: "a \ carrier R \ a \ \ \ a \ a = \"
  by (simp add: m_div_def)

lemma divide_eq_0_iff:
  assumes "a \ carrier R" "b \ carrier R"
    and "b \ \"
  shows "a \ b = \ \ a = \"
proof
  assume "a = \"
  with assms show "a \ b = \" by simp
next
  assume "a \ b = \"
  with assms have "b \ (a \ b) = b \ \" by simp
  also from assms have "b \ (a \ b) = b \ a \ b" by simp
  also from assms have "b \ a = a \ b" by (simp add: m_comm)
  also from assms have "a \ b \ b = a \ (b \ b)" by simp
  also from assms have "b \ b = \" by (simp add: divide_self)
  finally show "a = \" using assms by simp
qed

end

lemma field_class: "field (cring_class_ops::'a::field ring)"
  apply unfold_locales
    apply (simp_all add: cring_class_ops_def)
  using field_class.field_inverse by (force simp add: Units_def)

lemma div_class: "(x::'a::field) \\<^bsub>cring_class_ops\<^esub> y = x / y"
  by (simp add: carrier_class class_simps cring_class.comm_inv_char
      field_class.field_divide_inverse m_div_def)

interpretation field_class: field "cring_class_ops::'a::field ring"
  rewrites "(\\<^bsub>cring_class_ops\<^esub>::'a) = 0"
    and "(\\<^bsub>cring_class_ops\<^esub>::'a) = 1"
    and "(x::'a) \\<^bsub>cring_class_ops\<^esub> y = x + y"
    and "(x::'a) \\<^bsub>cring_class_ops\<^esub> y = x * y"
    and "\\<^bsub>cring_class_ops\<^esub> (x::'a) = - x"
    and "(x::'a) \\<^bsub>cring_class_ops\<^esub> y = x - y"
    and "(x::'a) [^]\<^bsub>cring_class_ops\<^esub> n = x ^ n"
    and "\n\\<^sub>\\<^bsub>cring_class_ops\<^esub> = of_nat n"
    and "((\i\\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i"
    and "(x::'a) \\<^bsub>cring_class_ops\<^esub> y = x / y"
    and "(Int.of_int (numeral m)::'a) = numeral m"
  by (simp_all add: field_class class_simps div_class)

end

quality100%

¤ 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.0.15Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Normalansicht

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.