First distributed version of Group and Ring theory.
--- a/src/HOL/Algebra/CRing.thy Mon Mar 10 16:21:06 2003 +0100
+++ b/src/HOL/Algebra/CRing.thy Mon Mar 10 17:25:34 2003 +0100
@@ -7,7 +7,8 @@
header {* The algebraic hierarchy of rings as axiomatic classes *}
-theory Ring = Group
+theory CRing = Group
+files ("ringsimp.ML"):
section {* The Algebraic Hierarchy of Rings *}
@@ -17,49 +18,18 @@
zero :: 'a ("\<zero>\<index>")
add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
+ minus :: "['a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
locale cring = abelian_monoid R +
assumes a_abelian_group: "abelian_group (| carrier = carrier R,
mult = add R, one = zero R, m_inv = a_inv R |)"
+ and minus_def: "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
-ML {*
- thm "cring.l_distr"
-*}
-
(*
-locale cring = struct R +
- assumes a_group: "abelian_group (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- and m_monoid: "abelian_monoid (| carrier = carrier R - {zero R},
- mult = mult R, one = one R |)"
- and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
- ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
-
-locale field = struct R +
- assumes a_group: "abelian_group (| carrier = carrier R,
- mult = add R, one = zero R, m_inv = a_inv R |)"
- and m_group: "monoid (| carrier = carrier R - {zero R},
- mult = mult R, one = one R |)"
- and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
- ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
-*)
-(*
- a_assoc: "(a + b) + c = a + (b + c)"
- l_zero: "0 + a = a"
- l_neg: "(-a) + a = 0"
- a_comm: "a + b = b + a"
-
- m_assoc: "(a * b) * c = a * (b * c)"
- l_one: "1 * a = a"
-
- l_distr: "(a + b) * c = a * c + b * c"
-
- m_comm: "a * b = b * a"
-
-- {* Definition of derived operations *}
minus_def: "a - b = a + (-b)"
@@ -108,171 +78,154 @@
mult = add R, one = zero R, m_inv = a_inv R |)"
by (simp add: abelian_group_def)
-lemma (in cring) a_assoc:
- "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
- ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
- using semigroup.m_assoc [OF a_semigroup]
- by simp
+lemmas (in cring) a_closed [intro, simp] =
+ magma.m_closed [OF a_magma, simplified]
+
+lemmas (in cring) zero_closed [intro, simp] =
+ l_one.one_closed [OF a_l_one, simplified]
+
+lemmas (in cring) a_inv_closed [intro, simp] =
+ group.inv_closed [OF a_group, simplified]
+
+lemma (in cring) minus_closed [intro, simp]:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y \<in> carrier R"
+ by (simp add: minus_def)
+
+lemmas (in cring) a_l_cancel [simp] = group.l_cancel [OF a_group, simplified]
-lemma (in cring) l_zero:
- "x \<in> carrier R ==> \<zero> \<oplus> x = x"
- using l_one.l_one [OF a_l_one]
+lemmas (in cring) a_r_cancel [simp] = group.r_cancel [OF a_group, simplified]
+
+lemmas (in cring) a_assoc = semigroup.m_assoc [OF a_semigroup, simplified]
+
+lemmas (in cring) l_zero [simp] = l_one.l_one [OF a_l_one, simplified]
+
+lemmas (in cring) l_neg = group.l_inv [OF a_group, simplified]
+
+lemmas (in cring) a_comm = abelian_semigroup.m_comm [OF a_abelian_semigroup,
+ simplified]
+
+lemmas (in cring) a_lcomm =
+ abelian_semigroup.m_lcomm [OF a_abelian_semigroup, simplified]
+
+lemma (in cring) r_zero [simp]:
+ "x \<in> carrier R ==> x \<oplus> \<zero> = x"
+ using group.r_one [OF a_group]
by simp
-lemma (in cring) l_neg:
- "x \<in> carrier R ==> (\<ominus> x) \<oplus> x = \<zero>"
- using group.l_inv [OF a_group]
+lemma (in cring) r_neg:
+ "x \<in> carrier R ==> x \<oplus> (\<ominus> x) = \<zero>"
+ using group.r_inv [OF a_group]
+ by simp
+
+lemmas (in cring) minus_zero [simp] = group.inv_one [OF a_group, simplified]
+
+lemma (in cring) minus_minus [simp]:
+ "x \<in> carrier R ==> \<ominus> (\<ominus> x) = x"
+ using group.inv_inv [OF a_group, simplified]
by simp
-lemma (in cring) a_comm:
- "[| x \<in> carrier R; y \<in> carrier R |]
- ==> x \<oplus> y = y \<oplus> x"
- using abelian_semigroup.m_comm [OF a_abelian_semigroup]
+lemma (in cring) minus_add:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> y"
+ using abelian_group.inv_mult [OF a_abelian_group]
by simp
+lemmas (in cring) a_ac = a_assoc a_comm a_lcomm
+subsection {* Normaliser for Commutative Rings *}
-
+lemma (in cring) r_neg2:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
+proof -
+ assume G: "x \<in> carrier R" "y \<in> carrier R"
+ then have "(x \<oplus> \<ominus> x) \<oplus> y = y" by (simp only: r_neg l_zero)
+ with G show ?thesis by (simp add: a_ac)
qed
- l_zero: "0 + a = a"
- l_neg: "(-a) + a = 0"
- a_comm: "a + b = b + a"
-
- m_assoc: "(a * b) * c = a * (b * c)"
- l_one: "1 * a = a"
-
- l_distr: "(a + b) * c = a * c + b * c"
-
- m_comm: "a * b = b * a"
-text {* Normaliser for Commutative Rings *}
-
-use "order.ML"
-
-method_setup ring =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *}
- {* computes distributive normal form in rings *}
-
-subsection {* Rings and the summation operator *}
-
-(* Basic facts --- move to HOL!!! *)
-
-lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)"
-by simp
-
-lemma natsum_Suc [simp]:
- "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)"
-by (simp add: atMost_Suc)
-
-lemma natsum_Suc2:
- "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)"
-proof (induct n)
- case 0 show ?case by simp
-next
- case Suc thus ?case by (simp add: assoc)
+lemma (in cring) r_neg1:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<oplus> (x \<oplus> y) = y"
+proof -
+ assume G: "x \<in> carrier R" "y \<in> carrier R"
+ then have "(\<ominus> x \<oplus> x) \<oplus> y = y" by (simp only: l_neg l_zero)
+ with G show ?thesis by (simp add: a_ac)
qed
-lemma natsum_cong [cong]:
- "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==>
- setsum f {..j} = setsum g {..k}"
-by (induct j) auto
-
-lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)"
-by (induct n) simp_all
-
-lemma natsum_add [simp]:
- "!!f::nat=>'a::plus_ac0.
- setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"
-by (induct n) (simp_all add: plus_ac0)
-
-(* Facts specific to rings *)
-
-instance ring < plus_ac0
-proof
- fix x y z
- show "(x::'a::ring) + y = y + x" by (rule a_comm)
- show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
- show "0 + (x::'a::ring) = x" by (rule l_zero)
+lemma (in cring) r_distr:
+ "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
+ ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
+proof -
+ assume G: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+ then have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z" by (simp add: m_comm)
+ also from G have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
+ also from G have "... = z \<otimes> x \<oplus> z \<otimes> y" by (simp add: m_comm)
+ finally show ?thesis .
qed
-ML {*
- local
- val lhss =
- [read_cterm (sign_of (the_context ()))
- ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
- read_cterm (sign_of (the_context ()))
- ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
- read_cterm (sign_of (the_context ()))
- ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
- read_cterm (sign_of (the_context ()))
- ("- ?t::'a::ring", TVar (("'z", 0), []))
- ];
- fun proc sg _ t =
- let val rew = Tactic.prove sg [] []
- (HOLogic.mk_Trueprop
- (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
- (fn _ => simp_tac ring_ss 1)
- |> mk_meta_eq;
- val (t', u) = Logic.dest_equals (Thm.prop_of rew);
- in if t' aconv u
- then None
- else Some rew
- end;
- in
- val ring_simproc = mk_simproc "ring" lhss proc;
- end;
+text {*
+ The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
*}
-ML_setup {* Addsimprocs [ring_simproc] *}
-
-lemma natsum_ldistr:
- "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
-by (induct n) simp_all
-
-lemma natsum_rdistr:
- "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"
-by (induct n) simp_all
-
-subsection {* Integral Domains *}
+lemma (in cring) l_null [simp]:
+ "x \<in> carrier R ==> \<zero> \<otimes> x = \<zero>"
+proof -
+ assume R: "x \<in> carrier R"
+ then have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = (\<zero> \<oplus> \<zero>) \<otimes> x"
+ by (simp add: l_distr del: l_zero r_zero)
+ also from R have "... = \<zero> \<otimes> x \<oplus> \<zero>" by simp
+ finally have "\<zero> \<otimes> x \<oplus> \<zero> \<otimes> x = \<zero> \<otimes> x \<oplus> \<zero>" .
+ with R show ?thesis by (simp del: r_zero)
+qed
-declare one_not_zero [simp]
-
-lemma zero_not_one [simp]:
- "0 ~= (1::'a::domain)"
-by (rule not_sym) simp
+lemma (in cring) r_null [simp]:
+ "x \<in> carrier R ==> x \<otimes> \<zero> = \<zero>"
+proof -
+ assume R: "x \<in> carrier R"
+ then have "x \<otimes> \<zero> = \<zero> \<otimes> x" by (simp add: ac)
+ also from R have "... = \<zero>" by simp
+ finally show ?thesis .
+qed
-lemma integral_iff: (* not by default a simp rule! *)
- "(a * b = (0::'a::domain)) = (a = 0 | b = 0)"
-proof
- assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral)
-next
- assume "a = 0 | b = 0" then show "a * b = 0" by auto
+lemma (in cring) l_minus:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> \<ominus> x \<otimes> y = \<ominus> (x \<otimes> y)"
+proof -
+ assume R: "x \<in> carrier R" "y \<in> carrier R"
+ then have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = (\<ominus> x \<oplus> x) \<otimes> y" by (simp add: l_distr)
+ also from R have "... = \<zero>" by (simp add: l_neg l_null)
+ finally have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y = \<zero>" .
+ with R have "(\<ominus> x) \<otimes> y \<oplus> x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) = \<zero> \<oplus> \<ominus> (x \<otimes> y)" by simp
+ with R show ?thesis by (simp add: a_assoc r_neg )
qed
-(*
-lemma "(a::'a::ring) - (a - b) = b" apply simp
- simproc seems to fail on this example (fixed with new term order)
-*)
-(*
-lemma bug: "(b::'a::ring) - (b - a) = a" by simp
- simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
-*)
-lemma m_lcancel:
- assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
-proof
- assume eq: "a * b = a * c"
- then have "a * (b - c) = 0" by simp
- then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
- with prem have "b - c = 0" by auto
- then have "b = b - (b - c)" by simp
- also have "b - (b - c) = c" by simp
- finally show "b = c" .
-next
- assume "b = c" then show "a * b = a * c" by simp
+lemma (in cring) r_minus:
+ "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<otimes> \<ominus> y = \<ominus> (x \<otimes> y)"
+proof -
+ assume R: "x \<in> carrier R" "y \<in> carrier R"
+ then have "x \<otimes> \<ominus> y = \<ominus> y \<otimes> x" by (simp add: ac)
+ also from R have "... = \<ominus> (y \<otimes> x)" by (simp add: l_minus)
+ also from R have "... = \<ominus> (x \<otimes> y)" by (simp add: ac)
+ finally show ?thesis .
qed
-lemma m_rcancel:
- "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
-by (simp add: m_lcancel)
+lemmas (in cring) cring_simprules =
+ a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
+ a_assoc l_zero l_neg a_comm m_assoc l_one l_distr m_comm minus_def
+ r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
+ a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
+
+use "ringsimp.ML"
+
+method_setup algebra =
+ {* Method.ctxt_args cring_normalise *}
+ {* computes distributive normal form in commutative rings (locales version) *}
+
+lemma
+ includes cring R + cring S
+ shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
+ a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^sub>2 d = d \<otimes>\<^sub>2 c"
+ by algebra
+
+lemma
+ includes cring
+ shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
+ by algebra
end
--- a/src/HOL/Algebra/Group.thy Mon Mar 10 16:21:06 2003 +0100
+++ b/src/HOL/Algebra/Group.thy Mon Mar 10 17:25:34 2003 +0100
@@ -20,14 +20,6 @@
subsection {* Definitions *}
-(* The following may be unnecessary. *)
-text {*
- We write groups additively. This simplifies notation for rings.
- All rings have an additive inverse, only fields have a
- multiplicative one. This definitions reduces the need for
- qualifiers.
-*}
-
record 'a semigroup =
carrier :: "'a set"
mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
@@ -104,6 +96,14 @@
then show "y \<otimes> x = z \<otimes> x" by simp
qed
+lemma (in group) inv_one [simp]:
+ "inv \<one> = \<one>"
+proof -
+ have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
+ moreover have "... = \<one>" by (simp add: r_inv)
+ finally show ?thesis .
+qed
+
lemma (in group) inv_inv [simp]:
"x \<in> carrier G ==> inv (inv x) = x"
proof -
@@ -112,7 +112,7 @@
with x show ?thesis by simp
qed
-lemma (in group) inv_mult:
+lemma (in group) inv_mult_group:
"[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
proof -
assume G: "x \<in> carrier G" "y \<in> carrier G"
@@ -245,21 +245,21 @@
constdefs
DirProdSemigroup ::
- "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
+ "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
=> ('a \<times> 'b) semigroup"
(infixr "\<times>\<^sub>s" 80)
"G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
DirProdMonoid ::
- "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
+ "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
(infixr "\<times>\<^sub>m" 80)
"G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
mult = mult (G \<times>\<^sub>s H),
one = (one G, one H) |)"
DirProdGroup ::
- "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
+ "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
(infixr "\<times>\<^sub>g" 80)
"G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
mult = mult (G \<times>\<^sub>m H),
@@ -409,4 +409,8 @@
locale abelian_group = abelian_monoid + group
+lemma (in abelian_group) inv_mult:
+ "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
+ by (simp add: ac inv_mult_group)
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/ringsimp.ML Mon Mar 10 17:25:34 2003 +0100
@@ -0,0 +1,87 @@
+(*
+ Title: Normalisation method for locale cring
+ Id: $Id$
+ Author: Clemens Ballarin
+ Copyright: TU Muenchen
+*)
+
+local
+
+(*** Lexicographic path order on terms.
+
+ See Baader & Nipkow, Term rewriting, CUP 1998.
+ Without variables. Const, Var, Bound, Free and Abs are treated all as
+ constants.
+
+ f_ord maps strings to integers and serves two purposes:
+ - Predicate on constant symbols. Those that are not recognised by f_ord
+ must be mapped to ~1.
+ - Order on the recognised symbols. These must be mapped to distinct
+ integers >= 0.
+
+***)
+
+fun dest_hd f_ord (Const (a, T)) =
+ let val ord = f_ord a in
+ if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
+ end
+ | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
+ | dest_hd _ (Var v) = ((1, v), 1)
+ | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
+ | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
+
+fun term_lpo f_ord (s, t) =
+ let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
+ if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
+ then case hd_ord f_ord (f, g) of
+ GREATER =>
+ if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+ then GREATER else LESS
+ | EQUAL =>
+ if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+ then list_ord (term_lpo f_ord) (ss, ts)
+ else LESS
+ | LESS => LESS
+ else GREATER
+ end
+and hd_ord f_ord (f, g) = case (f, g) of
+ (Abs (_, T, t), Abs (_, U, u)) =>
+ (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
+ | (_, _) => prod_ord (prod_ord int_ord
+ (prod_ord Term.indexname_ord Term.typ_ord)) int_ord
+ (dest_hd f_ord f, dest_hd f_ord g)
+
+in
+
+(*** Term order for commutative rings ***)
+
+fun ring_ord a =
+ find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
+ "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
+
+fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
+
+val cring_ss = HOL_ss settermless termless_ring;
+
+fun cring_normalise ctxt = let
+ fun filter t = case HOLogic.dest_Trueprop t of
+ Const ("CRing.cring_axioms", _) $ Free (s, _) => [s]
+ | _ => []
+ handle TERM _ => [];
+ val insts = flat (map (filter o #prop o rep_thm)
+ (ProofContext.prems_of ctxt));
+val _ = warning ("Rings in proof context: " ^ implode insts);
+ val simps =
+ flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
+ insts);
+ in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
+ end;
+
+(*
+val ring_ss = HOL_basic_ss settermless termless_ring addsimps
+ [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
+ r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
+ a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
+*)
+
+end;
\ No newline at end of file