# HG changeset patch # User paulson # Date 1086704550 -7200 # Node ID ca000a495448d088bca9a6673f26385cdbc99312 # Parent e0e2361b9a30b225b516d0a50b7098d7eca7528d Groups, Rings and supporting lemmas diff -r e0e2361b9a30 -r ca000a495448 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/Cardinal.thy Tue Jun 08 16:22:30 2004 +0200 @@ -789,6 +789,9 @@ lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard] +lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A Int B)" +by (blast intro: subset_Finite) + lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard] lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))" @@ -890,6 +893,10 @@ intro: Un_upper1 [THEN Fin_mono, THEN subsetD] Un_upper2 [THEN Fin_mono, THEN subsetD]) +lemma Finite_Un_iff [simp]: "Finite(A Un B) <-> (Finite(A) & Finite(B))" +by (blast intro: subset_Finite Finite_Un) + +text{*The converse must hold too.*} lemma Finite_Union: "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))" apply (simp add: Finite_Fin_iff) apply (rule Fin_UnionI) diff -r e0e2361b9a30 -r ca000a495448 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/CardinalArith.thy Tue Jun 08 16:22:30 2004 +0200 @@ -26,14 +26,15 @@ lam :K*K. , rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" - (*This def is more complex than Kunen's but it more easily proved to - be a cardinal*) jump_cardinal :: "i=>i" + --{*This def is more complex than Kunen's but it more easily proved to + be a cardinal*} "jump_cardinal(K) == \X\Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" - (*needed because jump_cardinal(K) might not be the successor of K*) csucc :: "i=>i" + --{*needed because @{term "jump_cardinal(K)"} might not be the successor + of @{term K}*} "csucc(K) == LEAST L. Card(L) & K Card(K(x))) ==> Card(\x\A. K(x))" +lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\x\A. K(x))" by (blast intro: Card_Union) lemma Card_OUN [simp,intro,TC]: @@ -82,8 +82,7 @@ apply (fast intro!: le_imp_lepoll ltI leI) done -lemma lesspoll_lemma: - "[| ~ A \ B; C \ B |] ==> A - C \ 0" +lemma lesspoll_lemma: "[| ~ A \ B; C \ B |] ==> A - C \ 0" apply (unfold lesspoll_def) apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll] intro!: eqpollI elim: notE @@ -98,7 +97,7 @@ addition and multiplication of natural numbers; on infinite cardinals they coincide with union (maximum). Either way we get most laws for free.*} -(** Cardinal addition is commutative **) +subsubsection{*Cardinal addition is commutative*} lemma sum_commute_eqpoll: "A+B \ B+A" apply (unfold eqpoll_def) @@ -112,7 +111,7 @@ apply (rule sum_commute_eqpoll [THEN cardinal_cong]) done -(** Cardinal addition is associative **) +subsubsection{*Cardinal addition is associative*} lemma sum_assoc_eqpoll: "(A+B)+C \ A+(B+C)" apply (unfold eqpoll_def) @@ -135,7 +134,7 @@ apply (blast intro: well_ord_radd ) done -(** 0 is the identity for addition **) +subsubsection{*0 is the identity for addition*} lemma sum_0_eqpoll: "0+A \ A" apply (unfold eqpoll_def) @@ -148,7 +147,7 @@ apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq) done -(** Addition by another cardinal **) +subsubsection{*Addition by another cardinal*} lemma sum_lepoll_self: "A \ A+B" apply (unfold lepoll_def inj_def) @@ -167,7 +166,7 @@ apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord) done -(** Monotonicity of addition **) +subsubsection{*Monotonicity of addition*} lemma sum_lepoll_mono: "[| A \ C; B \ D |] ==> A + B \ C + D" @@ -188,7 +187,7 @@ apply (blast intro: sum_lepoll_mono subset_imp_lepoll) done -(** Addition of finite cardinals is "ordinary" addition **) +subsubsection{*Addition of finite cardinals is "ordinary" addition*} lemma sum_succ_eqpoll: "succ(A)+B \ succ(A+B)" apply (unfold eqpoll_def) @@ -219,7 +218,7 @@ subsection{*Cardinal multiplication*} -(** Cardinal multiplication is commutative **) +subsubsection{*Cardinal multiplication is commutative*} (*Easier to prove the two directions separately*) lemma prod_commute_eqpoll: "A*B \ B*A" @@ -234,7 +233,7 @@ apply (rule prod_commute_eqpoll [THEN cardinal_cong]) done -(** Cardinal multiplication is associative **) +subsubsection{*Cardinal multiplication is associative*} lemma prod_assoc_eqpoll: "(A*B)*C \ A*(B*C)" apply (unfold eqpoll_def) @@ -257,7 +256,7 @@ apply (blast intro: well_ord_rmult) done -(** Cardinal multiplication distributes over addition **) +subsubsection{*Cardinal multiplication distributes over addition*} lemma sum_prod_distrib_eqpoll: "(A+B)*C \ (A*C)+(B*C)" apply (unfold eqpoll_def) @@ -280,7 +279,7 @@ apply (blast intro: well_ord_rmult)+ done -(** Multiplication by 0 yields 0 **) +subsubsection{*Multiplication by 0 yields 0*} lemma prod_0_eqpoll: "0*A \ 0" apply (unfold eqpoll_def) @@ -291,7 +290,7 @@ lemma cmult_0 [simp]: "0 |*| i = 0" by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong]) -(** 1 is the identity for multiplication **) +subsubsection{*1 is the identity for multiplication*} lemma prod_singleton_eqpoll: "{x}*A \ A" apply (unfold eqpoll_def) @@ -321,7 +320,7 @@ apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) done -(** Multiplication by a non-zero cardinal **) +subsubsection{*Multiplication by a non-zero cardinal*} lemma prod_lepoll_self: "b: B ==> A \ A*B" apply (unfold lepoll_def inj_def) @@ -338,7 +337,7 @@ apply (blast intro: prod_lepoll_self ltD) done -(** Monotonicity of multiplication **) +subsubsection{*Monotonicity of multiplication*} lemma prod_lepoll_mono: "[| A \ C; B \ D |] ==> A * B \ C * D" @@ -480,7 +479,7 @@ apply (rule pred_subset) done -(** Establishing the well-ordering **) +subsubsection{*Establishing the well-ordering*} lemma csquare_lam_inj: "Ord(K) ==> (lam :K*K. ) : inj(K*K, K*K*K)" @@ -494,7 +493,7 @@ apply (blast intro: well_ord_rmult well_ord_Memrel) done -(** Characterising initial segments of the well-ordering **) +subsubsection{*Characterising initial segments of the well-ordering*} lemma csquareD: "[| <, > : csquare_rel(K); x x le z & y le z" @@ -536,7 +535,7 @@ subset_Un_iff2 [THEN iff_sym] OrdmemD) done -(** The cardinality of initial segments **) +subsubsection{*The cardinality of initial segments*} lemma ordermap_z_lt: "[| Limit(K); x @@ -635,7 +634,7 @@ lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)" by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord]) -(** Toward's Kunen's Corollary 10.13 (1) **) +subsubsection{*Toward's Kunen's Corollary 10.13 (1)*} lemma InfCard_le_cmult_eq: "[| InfCard(K); L le K; 0 K |*| L = K" apply (rule le_anti_sym) @@ -784,7 +783,7 @@ lt_csucc [THEN leI, THEN [2] le_trans]) -(** Removing elements from a finite set decreases its cardinality **) +subsubsection{*Removing elements from a finite set decreases its cardinality*} lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A --> ~ cons(x,A) \ A" apply (erule Fin_induct) @@ -794,7 +793,7 @@ apply (blast dest!: cons_lepoll_consD, blast) done -lemma Finite_imp_cardinal_cons: +lemma Finite_imp_cardinal_cons [simp]: "[| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)" apply (unfold cardinal_def) apply (rule Least_equality) @@ -825,8 +824,35 @@ apply (simp add: Finite_imp_succ_cardinal_Diff) done +lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| : nat" +apply (erule Finite_induct) +apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons) +done -(** Theorems by Krzysztof Grabczewski, proofs by lcp **) +lemma card_Un_Int: + "[|Finite(A); Finite(B)|] ==> |A| #+ |B| = |A Un B| #+ |A Int B|" +apply (erule Finite_induct, simp) +apply (simp add: Finite_Int cons_absorb Un_cons Int_cons_left) +done + +lemma card_Un_disjoint: + "[|Finite(A); Finite(B); A Int B = 0|] ==> |A Un B| = |A| #+ |B|" +by (simp add: Finite_Un card_Un_Int) + +lemma card_partition [rule_format]: + "Finite(C) ==> + Finite (\ C) --> + (\c\C. |c| = k) --> + (\c1 \ C. \c2 \ C. c1 \ c2 --> c1 \ c2 = 0) --> + k #* |C| = |\ C|" +apply (erule Finite_induct, auto) +apply (subgoal_tac " x \ \B = 0") +apply (auto simp add: card_Un_disjoint Finite_Union + subset_Finite [of _ "\ (cons(x,F))"]) +done + + +subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*} lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard] @@ -845,11 +871,6 @@ lemma Ord_nat_subset_into_Card: "[| Ord(i); i <= nat |] ==> Card(i)" by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) -lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| : nat" -apply (erule Finite_induct) -apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons) -done - lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1" apply (rule succ_inject) apply (rule_tac b = "|A|" in trans) @@ -867,7 +888,6 @@ lemma cardinal_lt_imp_Diff_not_0 [rule_format]: "Finite(B) ==> ALL A. |B|<|A| --> A - B ~= 0" apply (erule Finite_induct, auto) -apply (simp_all add: Finite_imp_cardinal_cons) apply (case_tac "Finite (A)") apply (subgoal_tac [2] "Finite (cons (x, B))") apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite) diff -r e0e2361b9a30 -r ca000a495448 src/ZF/Finite.thy --- a/src/ZF/Finite.thy Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/Finite.thy Tue Jun 08 16:22:30 2004 +0200 @@ -3,8 +3,6 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -prove X:Fin(A) ==> |X| < nat - prove: b: Fin(A) ==> inj(b,b) <= surj(b,b) *) @@ -199,6 +197,17 @@ apply (blast dest: FiniteFun_is_fun range_of_fun range_type apply_equality)+ done + +subsection{*The Contents of a Singleton Set*} + +constdefs + contents :: "i=>i" + "contents(X) == THE x. X = {x}" + +lemma contents_eq [simp]: "contents ({x}) = x" +by (simp add: contents_def) + + ML {* val Fin_intros = thms "Fin.intros"; diff -r e0e2361b9a30 -r ca000a495448 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/IsaMakefile Tue Jun 08 16:22:30 2004 +0200 @@ -146,9 +146,9 @@ ZF-ex: ZF $(LOG)/ZF-ex.gz $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \ - ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy \ + ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy ex/Group.thy\ ex/Limit.thy ex/LList.thy ex/Primes.thy \ - ex/NatSum.thy ex/Ramsey.thy ex/misc.thy + ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy @$(ISATOOL) usedir $(OUT)/ZF ex diff -r e0e2361b9a30 -r ca000a495448 src/ZF/Perm.thy --- a/src/ZF/Perm.thy Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/Perm.thy Tue Jun 08 16:22:30 2004 +0200 @@ -221,12 +221,15 @@ lemma left_inverse [simp]: "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a" by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun) +lemma left_inverse_eq: + "[|f \ inj(A,B); f ` x = y; x \ A|] ==> converse(f) ` y = x" +by auto + lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard] lemma right_inverse_lemma: "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b" -apply (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) -done +by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse? No: they would not imply that converse(f) was a function! *) diff -r e0e2361b9a30 -r ca000a495448 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/ZF.thy Tue Jun 08 16:22:30 2004 +0200 @@ -36,8 +36,7 @@ RepFun :: "[i, i => i] => i" Collect :: "[i, i => o] => i" - -text {*Descriptions *} +text{*Definite descriptions -- via Replace over the set "1"*} consts The :: "(i => o) => i" (binder "THE " 10) If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10) @@ -49,7 +48,6 @@ "if(P,a,b)" => "If(P,a,b)" - text {*Finite Sets *} consts Upair :: "[i, i] => i" @@ -227,6 +225,7 @@ replacement: "(\x\A. \y z. P(x,y) & P(x,z) --> y=z) ==> b \ PrimReplace(A,P) <-> (\x\A. P(x,b))" + defs (* Derived form of replacement, restricting P to its functional part. @@ -258,8 +257,7 @@ Un_def: "A Un B == Union(Upair(A,B))" Int_def: "A Int B == Inter(Upair(A,B))" - (* Definite descriptions -- via Replace over the set "1" *) - + (* definite descriptions *) the_def: "The(P) == Union({y . x \ {0}, P(y)})" if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b" diff -r e0e2361b9a30 -r ca000a495448 src/ZF/equalities.thy --- a/src/ZF/equalities.thy Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/equalities.thy Tue Jun 08 16:22:30 2004 +0200 @@ -763,6 +763,13 @@ lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)" by blast +lemma image_UN: "r `` (\x\A. B(x)) = (\x\A. r `` B(x))" +by blast + +lemma Collect_image_eq: + "{z \ Sigma(A,B). P(z)} `` C = (\x \ A. {y \ B(x). x \ C & P()})" +by blast + lemma image_Int_subset: "r``(A Int B) \ (r``A) Int (r``B)" by blast diff -r e0e2361b9a30 -r ca000a495448 src/ZF/ex/ROOT.ML --- a/src/ZF/ex/ROOT.ML Sun Jun 06 18:36:36 2004 +0200 +++ b/src/ZF/ex/ROOT.ML Tue Jun 08 16:22:30 2004 +0200 @@ -7,6 +7,7 @@ *) time_use_thy "misc"; +time_use_thy "Ring"; (*abstract algebra*) time_use_thy "Commutation"; (*abstract Church-Rosser theory*) time_use_thy "Primes"; (*GCD theory*) time_use_thy "NatSum"; (*Summing integers, squares, cubes, etc.*) diff -r e0e2361b9a30 -r ca000a495448 src/ZF/ex/Ring.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/ex/Ring.thy Tue Jun 08 16:22:30 2004 +0200 @@ -0,0 +1,338 @@ +(* Title: ZF/ex/Ring.thy + Id: $Id$ + +*) + +header {* Rings *} + +theory Ring = Group: + +(*First, we must simulate a record declaration: +record ring = monoid + + add :: "[i, i] => i" (infixl "\\" 65) + zero :: i ("\\") +*) + +constdefs + add_field :: "i => i" + "add_field(M) == fst(snd(snd(snd(M))))" + + ring_add :: "[i, i, i] => i" (infixl "\\" 65) + "ring_add(M,x,y) == add_field(M) ` " + + zero :: "i => i" ("\\") + "zero(M) == fst(snd(snd(snd(snd(M)))))" + + +lemma add_field_eq [simp]: "add_field() = A" + by (simp add: add_field_def) + +lemma add_eq [simp]: "ring_add(, x, y) = A ` " + by (simp add: ring_add_def) + +lemma zero_eq [simp]: "zero() = Z" + by (simp add: zero_def) + + +text {* Derived operations. *} + +constdefs (structure R) + a_inv :: "[i,i] => i" ("\\ _" [81] 80) + "a_inv(R) == m_inv ()" + + minus :: "[i,i,i] => i" (infixl "\\" 65) + "\x \ carrier(R); y \ carrier(R)\ \ x \ y == x \ (\ y)" + +locale abelian_monoid = struct G + + assumes a_comm_monoid: + "comm_monoid ()" + +text {* + The following definition is redundant but simple to use. +*} + +locale abelian_group = abelian_monoid + + assumes a_comm_group: + "comm_group ()" + +locale ring = abelian_group R + monoid R + + assumes l_distr: "\x \ carrier(R); y \ carrier(R); z \ carrier(R)\ + \ (x \ y) \ z = x \ z \ y \ z" + and r_distr: "\x \ carrier(R); y \ carrier(R); z \ carrier(R)\ + \ z \ (x \ y) = z \ x \ z \ y" + +locale cring = ring + comm_monoid R + +locale "domain" = cring + + assumes one_not_zero [simp]: "\ \ \" + and integral: "\a \ b = \; a \ carrier(R); b \ carrier(R)\ \ + a = \ | b = \" + + +subsection {* Basic Properties *} + +lemma (in abelian_monoid) a_monoid: + "monoid ()" +apply (insert a_comm_monoid) +apply (simp add: comm_monoid_def) +done + +lemma (in abelian_group) a_group: + "group ()" +apply (insert a_comm_group) +apply (simp add: comm_group_def group_def) +done + + +lemma (in abelian_monoid) l_zero [simp]: + "x \ carrier(G) \ \ \ x = x" +apply (insert monoid.l_one [OF a_monoid]) +apply (simp add: ring_add_def) +done + +lemma (in abelian_monoid) zero_closed [intro, simp]: + "\ \ carrier(G)" +by (rule monoid.one_closed [OF a_monoid, simplified]) + +lemma (in abelian_group) a_inv_closed [intro, simp]: + "x \ carrier(G) \ \ x \ carrier(G)" +by (simp add: a_inv_def group.inv_closed [OF a_group, simplified]) + +lemma (in abelian_monoid) a_closed [intro, simp]: + "[| x \ carrier(G); y \ carrier(G) |] ==> x \ y \ carrier(G)" +by (rule monoid.m_closed [OF a_monoid, + simplified, simplified ring_add_def [symmetric]]) + +lemma (in abelian_group) minus_closed [intro, simp]: + "\x \ carrier(G); y \ carrier(G)\ \ x \ y \ carrier(G)" +by (simp add: minus_def) + +lemma (in abelian_group) a_l_cancel [simp]: + "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\ + \ (x \ y = x \ z) <-> (y = z)" +by (rule group.l_cancel [OF a_group, + simplified, simplified ring_add_def [symmetric]]) + +lemma (in abelian_group) a_r_cancel [simp]: + "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\ + \ (y \ x = z \ x) <-> (y = z)" +by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]]) + +lemma (in abelian_monoid) a_assoc: + "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\ + \ (x \ y) \ z = x \ (y \ z)" +by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]]) + +lemma (in abelian_group) l_neg: + "x \ carrier(G) \ \ x \ x = \" +by (simp add: a_inv_def + group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]]) + +lemma (in abelian_monoid) a_comm: + "\x \ carrier(G); y \ carrier(G)\ \ x \ y = y \ x" +by (rule comm_monoid.m_comm [OF a_comm_monoid, + simplified, simplified ring_add_def [symmetric]]) + +lemma (in abelian_monoid) a_lcomm: + "\x \ carrier(G); y \ carrier(G); z \ carrier(G)\ + \ x \ (y \ z) = y \ (x \ z)" +by (rule comm_monoid.m_lcomm [OF a_comm_monoid, + simplified, simplified ring_add_def [symmetric]]) + +lemma (in abelian_monoid) r_zero [simp]: + "x \ carrier(G) \ x \ \ = x" + using monoid.r_one [OF a_monoid] + by (simp add: ring_add_def [symmetric]) + +lemma (in abelian_group) r_neg: + "x \ carrier(G) \ x \ (\ x) = \" + using group.r_inv [OF a_group] + by (simp add: a_inv_def ring_add_def [symmetric]) + +lemma (in abelian_group) minus_zero [simp]: + "\ \ = \" + by (simp add: a_inv_def + group.inv_one [OF a_group, simplified ]) + +lemma (in abelian_group) minus_minus [simp]: + "x \ carrier(G) \ \ (\ x) = x" + using group.inv_inv [OF a_group, simplified] + by (simp add: a_inv_def) + +lemma (in abelian_group) minus_add: + "\x \ carrier(G); y \ carrier(G)\ \ \ (x \ y) = \ x \ \ y" + using comm_group.inv_mult [OF a_comm_group] + by (simp add: a_inv_def ring_add_def [symmetric]) + +lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm + +text {* + The following proofs are from Jacobson, Basic Algebra I, pp.~88--89 +*} + +lemma (in ring) l_null [simp]: + "x \ carrier(R) \ \ \ x = \" +proof - + assume R: "x \ carrier(R)" + then have "\ \ x \ \ \ x = (\ \ \) \ x" + by (blast intro: l_distr [THEN sym]) + also from R have "... = \ \ x \ \" by simp + finally have "\ \ x \ \ \ x = \ \ x \ \" . + with R show ?thesis by (simp del: r_zero) +qed + +lemma (in ring) r_null [simp]: + "x \ carrier(R) \ x \ \ = \" +proof - + assume R: "x \ carrier(R)" + then have "x \ \ \ x \ \ = x \ (\ \ \)" + by (simp add: r_distr del: l_zero r_zero) + also from R have "... = x \ \ \ \" by simp + finally have "x \ \ \ x \ \ = x \ \ \ \" . + with R show ?thesis by (simp del: r_zero) +qed + +lemma (in ring) l_minus: + "\x \ carrier(R); y \ carrier(R)\ \ \ x \ y = \ (x \ y)" +proof - + assume R: "x \ carrier(R)" "y \ carrier(R)" + then have "(\ x) \ y \ x \ y = (\ x \ x) \ y" by (simp add: l_distr) + also from R have "... = \" by (simp add: l_neg l_null) + finally have "(\ x) \ y \ x \ y = \" . + with R have "(\ x) \ y \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp + with R show ?thesis by (simp add: a_assoc r_neg) +qed + +lemma (in ring) r_minus: + "\x \ carrier(R); y \ carrier(R)\ \ x \ \ y = \ (x \ y)" +proof - + assume R: "x \ carrier(R)" "y \ carrier(R)" + then have "x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr) + also from R have "... = \" by (simp add: l_neg r_null) + finally have "x \ (\ y) \ x \ y = \" . + with R have "x \ (\ y) \ x \ y \ \ (x \ y) = \ \ \ (x \ y)" by simp + with R show ?thesis by (simp add: a_assoc r_neg) +qed + +lemma (in ring) minus_eq: + "\x \ carrier(R); y \ carrier(R)\ \ x \ y = x \ \ y" + by (simp only: minus_def) + + +lemma (in ring) l_null [simp]: + "x \ carrier(R) \ \ \ x = \" +proof - + assume R: "x \ carrier(R)" + then have "\ \ x \ \ \ x = (\ \ \) \ x" + by (simp add: l_distr del: l_zero r_zero) + also from R have "... = \ \ x \ \" by simp + finally have "\ \ x \ \ \ x = \ \ x \ \" . + with R show ?thesis by (simp del: r_zero) +qed + +lemma (in ring) r_null [simp]: + "x \ carrier(R) \ x \ \ = \" +proof - + assume R: "x \ carrier(R)" + then have "x \