--- 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)
--- 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 <x,y>:K*K. <x Un y, x, y>,
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) ==
\<Union>X\<in>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<L"
syntax (xsymbols)
@@ -57,8 +58,7 @@
apply (blast intro: subset_imp_lepoll)
done
-lemma Card_UN:
- "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))"
+lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>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 \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
+lemma lesspoll_lemma: "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 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 \<approx> 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 \<approx> 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 \<approx> 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 \<lesssim> 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 \<lesssim> C; B \<lesssim> D |] ==> A + B \<lesssim> 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 \<approx> 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 \<approx> 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 \<approx> 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 \<approx> (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 \<approx> 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 \<approx> 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 \<lesssim> 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 \<lesssim> C; B \<lesssim> D |] ==> A * B \<lesssim> 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 <x,y>:K*K. <x Un y, x, y>) : 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:
"[| <<x,y>, <z,z>> : csquare_rel(K); x<K; y<K; z<K |] ==> 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<K; y<K; z=succ(x Un y) |] ==>
@@ -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<L |] ==> 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) \<lesssim> 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 (\<Union> C) -->
+ (\<forall>c\<in>C. |c| = k) -->
+ (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = 0) -->
+ k #* |C| = |\<Union> C|"
+apply (erule Finite_induct, auto)
+apply (subgoal_tac " x \<inter> \<Union>B = 0")
+apply (auto simp add: card_Un_disjoint Finite_Union
+ subset_Finite [of _ "\<Union> (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)
--- 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";
--- 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
--- 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 \<in> inj(A,B); f ` x = y; x \<in> 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! *)
--- 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: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>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 \<in> {0}, P(y)})"
if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b"
--- 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 `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))"
+by blast
+
+lemma Collect_image_eq:
+ "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})"
+by blast
+
lemma image_Int_subset: "r``(A Int B) \<subseteq> (r``A) Int (r``B)"
by blast
--- 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.*)
--- /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 "\<oplus>\<index>" 65)
+ zero :: i ("\<zero>\<index>")
+*)
+
+constdefs
+ add_field :: "i => i"
+ "add_field(M) == fst(snd(snd(snd(M))))"
+
+ ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65)
+ "ring_add(M,x,y) == add_field(M) ` <x,y>"
+
+ zero :: "i => i" ("\<zero>\<index>")
+ "zero(M) == fst(snd(snd(snd(snd(M)))))"
+
+
+lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
+ by (simp add: add_field_def)
+
+lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` <x,y>"
+ by (simp add: ring_add_def)
+
+lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
+ by (simp add: zero_def)
+
+
+text {* Derived operations. *}
+
+constdefs (structure R)
+ a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80)
+ "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
+
+ minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65)
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y == x \<oplus> (\<ominus> y)"
+
+locale abelian_monoid = struct G +
+ assumes a_comm_monoid:
+ "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
+
+text {*
+ The following definition is redundant but simple to use.
+*}
+
+locale abelian_group = abelian_monoid +
+ assumes a_comm_group:
+ "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
+
+locale ring = abelian_group R + monoid R +
+ assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
+ \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
+ and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
+ \<Longrightarrow> z \<cdot> (x \<oplus> y) = z \<cdot> x \<oplus> z \<cdot> y"
+
+locale cring = ring + comm_monoid R
+
+locale "domain" = cring +
+ assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>"
+ and integral: "\<lbrakk>a \<cdot> b = \<zero>; a \<in> carrier(R); b \<in> carrier(R)\<rbrakk> \<Longrightarrow>
+ a = \<zero> | b = \<zero>"
+
+
+subsection {* Basic Properties *}
+
+lemma (in abelian_monoid) a_monoid:
+ "monoid (<carrier(G), add_field(G), zero(G), 0>)"
+apply (insert a_comm_monoid)
+apply (simp add: comm_monoid_def)
+done
+
+lemma (in abelian_group) a_group:
+ "group (<carrier(G), add_field(G), zero(G), 0>)"
+apply (insert a_comm_group)
+apply (simp add: comm_group_def group_def)
+done
+
+
+lemma (in abelian_monoid) l_zero [simp]:
+ "x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> 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]:
+ "\<zero> \<in> carrier(G)"
+by (rule monoid.one_closed [OF a_monoid, simplified])
+
+lemma (in abelian_group) a_inv_closed [intro, simp]:
+ "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<in> carrier(G)"
+by (simp add: a_inv_def group.inv_closed [OF a_group, simplified])
+
+lemma (in abelian_monoid) a_closed [intro, simp]:
+ "[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)"
+by (rule monoid.m_closed [OF a_monoid,
+ simplified, simplified ring_add_def [symmetric]])
+
+lemma (in abelian_group) minus_closed [intro, simp]:
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<ominus> y \<in> carrier(G)"
+by (simp add: minus_def)
+
+lemma (in abelian_group) a_l_cancel [simp]:
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ \<Longrightarrow> (x \<oplus> y = x \<oplus> 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]:
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
+by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
+
+lemma (in abelian_monoid) a_assoc:
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
+by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
+
+lemma (in abelian_group) l_neg:
+ "x \<in> carrier(G) \<Longrightarrow> \<ominus> x \<oplus> x = \<zero>"
+by (simp add: a_inv_def
+ group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])
+
+lemma (in abelian_monoid) a_comm:
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<oplus> y = y \<oplus> x"
+by (rule comm_monoid.m_comm [OF a_comm_monoid,
+ simplified, simplified ring_add_def [symmetric]])
+
+lemma (in abelian_monoid) a_lcomm:
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
+ \<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> 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 \<in> carrier(G) \<Longrightarrow> x \<oplus> \<zero> = x"
+ using monoid.r_one [OF a_monoid]
+ by (simp add: ring_add_def [symmetric])
+
+lemma (in abelian_group) r_neg:
+ "x \<in> carrier(G) \<Longrightarrow> x \<oplus> (\<ominus> x) = \<zero>"
+ using group.r_inv [OF a_group]
+ by (simp add: a_inv_def ring_add_def [symmetric])
+
+lemma (in abelian_group) minus_zero [simp]:
+ "\<ominus> \<zero> = \<zero>"
+ by (simp add: a_inv_def
+ group.inv_one [OF a_group, simplified ])
+
+lemma (in abelian_group) minus_minus [simp]:
+ "x \<in> carrier(G) \<Longrightarrow> \<ominus> (\<ominus> x) = x"
+ using group.inv_inv [OF a_group, simplified]
+ by (simp add: a_inv_def)
+
+lemma (in abelian_group) minus_add:
+ "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> \<ominus> (x \<oplus> y) = \<ominus> x \<oplus> \<ominus> 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 \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
+proof -
+ assume R: "x \<in> carrier(R)"
+ then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
+ by (blast intro: l_distr [THEN sym])
+ also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
+ finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
+ with R show ?thesis by (simp del: r_zero)
+qed
+
+lemma (in ring) r_null [simp]:
+ "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
+proof -
+ assume R: "x \<in> carrier(R)"
+ then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)"
+ by (simp add: r_distr del: l_zero r_zero)
+ also from R have "... = x \<cdot> \<zero> \<oplus> \<zero>" by simp
+ finally have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> \<zero> \<oplus> \<zero>" .
+ with R show ?thesis by (simp del: r_zero)
+qed
+
+lemma (in ring) l_minus:
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)"
+proof -
+ assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
+ then have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = (\<ominus> x \<oplus> x) \<cdot> y" by (simp add: l_distr)
+ also from R have "... = \<zero>" by (simp add: l_neg l_null)
+ finally have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = \<zero>" .
+ with R have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
+ with R show ?thesis by (simp add: a_assoc r_neg)
+qed
+
+lemma (in ring) r_minus:
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)"
+proof -
+ assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
+ then have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = x \<cdot> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
+ also from R have "... = \<zero>" by (simp add: l_neg r_null)
+ finally have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = \<zero>" .
+ with R have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
+ with R show ?thesis by (simp add: a_assoc r_neg)
+qed
+
+lemma (in ring) minus_eq:
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y"
+ by (simp only: minus_def)
+
+
+lemma (in ring) l_null [simp]:
+ "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
+proof -
+ assume R: "x \<in> carrier(R)"
+ then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
+ by (simp add: l_distr del: l_zero r_zero)
+ also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
+ finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
+ with R show ?thesis by (simp del: r_zero)
+qed
+
+lemma (in ring) r_null [simp]:
+ "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
+proof -
+ assume R: "x \<in> carrier(R)"
+ then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)"
+ by (simp add: r_distr del: l_zero r_zero)
+ also from R have "... = x \<cdot> \<zero> \<oplus> \<zero>" by simp
+ finally have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> \<zero> \<oplus> \<zero>" .
+ with R show ?thesis by (simp del: r_zero)
+qed
+
+lemma (in ring) l_minus:
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)"
+proof -
+ assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
+ then have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = (\<ominus> x \<oplus> x) \<cdot> y" by (simp add: l_distr)
+ also from R have "... = \<zero>" by (simp add: l_neg l_null)
+ finally have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y = \<zero>" .
+ with R have "(\<ominus> x) \<cdot> y \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
+ with R show ?thesis by (simp add: a_assoc r_neg)
+qed
+
+lemma (in ring) r_minus:
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)"
+proof -
+ assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
+ then have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = x \<cdot> (\<ominus> y \<oplus> y)" by (simp add: r_distr)
+ also from R have "... = \<zero>" by (simp add: l_neg r_null)
+ finally have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y = \<zero>" .
+ with R have "x \<cdot> (\<ominus> y) \<oplus> x \<cdot> y \<oplus> \<ominus> (x \<cdot> y) = \<zero> \<oplus> \<ominus> (x \<cdot> y)" by simp
+ with R show ?thesis by (simp add: a_assoc r_neg)
+qed
+
+lemma (in ring) minus_eq:
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y"
+ by (simp only: minus_def)
+
+subsection {* Morphisms *}
+
+constdefs
+ ring_hom :: "[i,i] => i"
+ "ring_hom(R,S) ==
+ {h \<in> carrier(R) -> carrier(S).
+ (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
+ h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
+ h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
+ h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
+
+lemma ring_hom_memI:
+ assumes hom_type: "h \<in> carrier(R) \<rightarrow> carrier(S)"
+ and hom_mult: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
+ h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
+ and hom_add: "\<And>x y. \<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow>
+ h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
+ and hom_one: "h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
+ shows "h \<in> ring_hom(R,S)"
+by (auto simp add: ring_hom_def prems)
+
+lemma ring_hom_closed:
+ "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(S)"
+by (auto simp add: ring_hom_def)
+
+lemma ring_hom_mult:
+ "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
+ \<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
+by (simp add: ring_hom_def)
+
+lemma ring_hom_add:
+ "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
+ \<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
+by (simp add: ring_hom_def)
+
+lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
+by (simp add: ring_hom_def)
+
+locale ring_hom_cring = cring R + cring S + var h +
+ assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
+ notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
+ and hom_mult [simp] = ring_hom_mult [OF homh]
+ and hom_add [simp] = ring_hom_add [OF homh]
+ and hom_one [simp] = ring_hom_one [OF homh]
+
+lemma (in ring_hom_cring) hom_zero [simp]:
+ "h ` \<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>S\<^esub>"
+proof -
+ have "h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> h ` \<zero> = h ` \<zero>\<^bsub>R\<^esub> \<oplus>\<^bsub>S\<^esub> \<zero>\<^bsub>S\<^esub>"
+ by (simp add: hom_add [symmetric] del: hom_add)
+ then show ?thesis by (simp del: S.r_zero)
+qed
+
+lemma (in ring_hom_cring) hom_a_inv [simp]:
+ "x \<in> carrier(R) \<Longrightarrow> h ` (\<ominus>\<^bsub>R\<^esub> x) = \<ominus>\<^bsub>S\<^esub> h ` x"
+proof -
+ assume R: "x \<in> carrier(R)"
+ then have "h ` x \<oplus>\<^bsub>S\<^esub> h ` (\<ominus> x) = h ` x \<oplus>\<^bsub>S\<^esub> (\<ominus>\<^bsub>S\<^esub> (h ` x))"
+ by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
+ with R show ?thesis by simp
+qed
+
+lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)"
+apply (rule ring_hom_memI)
+apply (auto simp add: id_type)
+done
+
+end
+
--- a/src/ZF/func.thy Sun Jun 06 18:36:36 2004 +0200
+++ b/src/ZF/func.thy Tue Jun 08 16:22:30 2004 +0200
@@ -271,6 +271,10 @@
apply (blast intro: image_function)
done
+lemma image_eq_UN:
+ assumes f: "f \<in> Pi(A,B)" "C \<subseteq> A" shows "f``C = (\<Union>x\<in>C. {f ` x})"
+by (auto simp add: image_fun [OF f])
+
lemma Pi_image_cons:
"[| f: Pi(A,B); x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)"
by (blast dest: apply_equality apply_Pair)
--- a/src/ZF/upair.thy Sun Jun 06 18:36:36 2004 +0200
+++ b/src/ZF/upair.thy Tue Jun 08 16:22:30 2004 +0200
@@ -147,7 +147,7 @@
lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
-subsection{*Rules for Descriptions*}
+subsection{*Descriptions*}
lemma the_equality [intro]:
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"