(* 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"
apply (simp add: a_inv_def m_inv_def cring_class_ops_def)
apply (rule the_equality)
apply (simp_all add: eq_neg_iff_add_eq_0)
done
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)
apply (auto simp add: Units_def)
apply (rule_tac x="1 / x" in exI)
apply simp
done
lemma div_class: "(x::'a::field) \\<^bsub>cring_class_ops\<^esub> y = x / y"
apply (simp add: m_div_def m_inv_def class_simps)
apply (rule impI)
apply (rule ssubst [OF the_equality, of _ "1 / y"])
apply simp_all
apply (drule conjunct2)
apply (drule_tac f="\x. x / y" in arg_cong)
apply simp
done
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
¤ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
¤
|
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.
|
