Theory Commutative_Ring_Ex

theory Commutative_Ring_Ex
imports Reflective_Field
(*  Title:      HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
    Author:     Bernhard Haeupler, Stefan Berghofer
*)

section ‹Some examples demonstrating the ring and field methods›

theory Commutative_Ring_Ex
imports "../Reflective_Field"
begin

lemma "4 * (x::int) ^ 5 * y ^ 3 * x ^ 2 * 3 + x * z + 3 ^ 5 = 12 * x ^ 7 * y ^ 3 + z * x + 243"
  by ring

lemma (in cring)
  assumes "x ∈ carrier R" "y ∈ carrier R" "z ∈ carrier R"
  shows "«4» ⊗ x (^) (5::nat) ⊗ y (^) (3::nat) ⊗ x (^) (2::nat) ⊗ «3» ⊕ x ⊗ z ⊕ «3» (^) (5::nat) =
    «12» ⊗ x (^) (7::nat) ⊗ y (^) (3::nat) ⊕ z ⊗ x ⊕ «243»"
  by ring

lemma "((x::int) + y) ^ 2  = x ^ 2 + y ^ 2 + 2 * x * y"
  by ring

lemma (in cring)
  assumes "x ∈ carrier R" "y ∈ carrier R"
  shows "(x ⊕ y) (^) (2::nat)  = x (^) (2::nat) ⊕ y (^) (2::nat) ⊕ «2» ⊗ x ⊗ y"
  by ring

lemma "((x::int) + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x ^ 2 * y + 3 * y ^ 2 * x"
  by ring

lemma (in cring)
  assumes "x ∈ carrier R" "y ∈ carrier R"
  shows "(x ⊕ y) (^) (3::nat) =
    x (^) (3::nat) ⊕ y (^) (3::nat) ⊕ «3» ⊗ x (^) (2::nat) ⊗ y ⊕ «3» ⊗ y (^) (2::nat) ⊗ x"
  by ring

lemma "((x::int) - y) ^ 3 = x ^ 3 + 3 * x * y ^ 2 + (- 3) * y * x ^ 2 - y ^ 3"
  by ring

lemma (in cring)
  assumes "x ∈ carrier R" "y ∈ carrier R"
  shows "(x ⊖ y) (^) (3::nat) =
    x (^) (3::nat) ⊕ «3» ⊗ x ⊗ y (^) (2::nat) ⊕ (⊖ «3») ⊗ y ⊗ x (^) (2::nat) ⊖ y (^) (3::nat)"
  by ring

lemma "((x::int) - y) ^ 2 = x ^ 2 + y ^ 2 - 2 * x * y"
  by ring

lemma (in cring)
  assumes "x ∈ carrier R" "y ∈ carrier R"
  shows "(x ⊖ y) (^) (2::nat) = x (^) (2::nat) ⊕ y (^) (2::nat) ⊖ «2» ⊗ x ⊗ y"
  by ring

lemma " ((a::int) + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * b * c + 2 * a * c"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
  shows " (a ⊕ b ⊕ c) (^) (2::nat) =
    a (^) (2::nat) ⊕ b (^) (2::nat) ⊕ c (^) (2::nat) ⊕ «2» ⊗ a ⊗ b ⊕ «2» ⊗ b ⊗ c ⊕ «2» ⊗ a ⊗ c"
  by ring

lemma "((a::int) - b - c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 - 2 * a * b + 2 * b * c - 2 * a * c"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
  shows "(a ⊖ b ⊖ c) (^) (2::nat) =
    a (^) (2::nat) ⊕ b (^) (2::nat) ⊕ c (^) (2::nat) ⊖ «2» ⊗ a ⊗ b ⊕ «2» ⊗ b ⊗ c ⊖ «2» ⊗ a ⊗ c"
  by ring

lemma "(a::int) * b + a * c = a * (b + c)"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R"
  shows "a ⊗ b ⊕ a ⊗ c = a ⊗ (b ⊕ c)"
  by ring

lemma "(a::int) ^ 2 - b ^ 2 = (a - b) * (a + b)"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a (^) (2::nat) ⊖ b (^) (2::nat) = (a ⊖ b) ⊗ (a ⊕ b)"
  by ring

lemma "(a::int) ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2)"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a (^) (3::nat) ⊖ b (^) (3::nat) = (a ⊖ b) ⊗ (a (^) (2::nat) ⊕ a ⊗ b ⊕ b (^) (2::nat))"
  by ring

lemma "(a::int) ^ 3 + b ^ 3 = (a + b) * (a ^ 2 - a * b + b ^ 2)"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a (^) (3::nat) ⊕ b (^) (3::nat) = (a ⊕ b) ⊗ (a (^) (2::nat) ⊖ a ⊗ b ⊕ b (^) (2::nat))"
  by ring

lemma "(a::int) ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2)"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a (^) (4::nat) ⊖ b (^) (4::nat) = (a ⊖ b) ⊗ (a ⊕ b) ⊗ (a (^) (2::nat) ⊕ b (^) (2::nat))"
  by ring

lemma "(a::int) ^ 10 - b ^ 10 =
  (a - b) * (a ^ 9 + a ^ 8 * b + a ^ 7 * b ^ 2 + a ^ 6 * b ^ 3 + a ^ 5 * b ^ 4 +
    a ^ 4 * b ^ 5 + a ^ 3 * b ^ 6 + a ^ 2 * b ^ 7 + a * b ^ 8 + b ^ 9)"
  by ring

lemma (in cring)
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a (^) (10::nat) ⊖ b (^) (10::nat) =
  (a ⊖ b) ⊗ (a (^) (9::nat) ⊕ a (^) (8::nat) ⊗ b ⊕ a (^) (7::nat) ⊗ b (^) (2::nat) ⊕
    a (^) (6::nat) ⊗ b (^) (3::nat) ⊕ a (^) (5::nat) ⊗ b (^) (4::nat) ⊕
    a (^) (4::nat) ⊗ b (^) (5::nat) ⊕ a (^) (3::nat) ⊗ b (^) (6::nat) ⊕
    a (^) (2::nat) ⊗ b (^) (7::nat) ⊕ a ⊗ b (^) (8::nat) ⊕ b (^) (9::nat))"
  by ring

lemma "(x::'a::field) ≠ 0 ⟹ (1 - 1 / x) * x - x + 1 = 0"
  by field

lemma (in field)
  assumes "x ∈ carrier R"
  shows "x ≠ 𝟬 ⟹ (𝟭 ⊖ 𝟭 ⊘ x) ⊗ x ⊖ x ⊕ 𝟭 = 𝟬"
  by field

end