# HG changeset patch # User paulson # Date 1026652483 -7200 # Node ID c9cfe1638bf2bee9f023617aa5574b0059abccd6 # Parent d19cdbd8b559546eb20c8a53cafb54b45b8c42f6 improved presentation markup diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Arith.thy --- a/src/ZF/Arith.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Arith.thy Sun Jul 14 15:14:43 2002 +0200 @@ -87,7 +87,7 @@ lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard] -(** natify: coercion to "nat" **) +subsection{*@{text natify}, the Coercion to @{term nat}*} lemma pred_succ_eq [simp]: "pred(succ(y)) = y" by (unfold pred_def, auto) @@ -163,7 +163,7 @@ by (simp add: div_def) -(*** Typing rules ***) +subsection{*Typing rules*} (** Addition **) @@ -218,7 +218,7 @@ done -(*** Addition ***) +subsection{*Addition*} (*Natify has weakened this law, compared with the older approach*) lemma add_0_natify [simp]: "0 #+ m = natify(m)" @@ -308,7 +308,7 @@ by (drule add_lt_elim1_natify, auto) -(*** Monotonicity of Addition ***) +subsection{*Monotonicity of Addition*} (*strict, in 1st argument; proof is by rule induction on 'less than'. Still need j:nat, for consider j = omega. Then we can have i m #- n < m" @@ -131,7 +131,7 @@ done -(*** Division ***) +subsection{*Division*} lemma raw_div_type: "[| m:nat; n:nat |] ==> raw_div (m, n) : nat" apply (unfold raw_div_def) @@ -196,7 +196,9 @@ done -(*** Further facts about mod (mainly for mutilated chess board) ***) +subsection{*Further Facts about Remainder*} + +text{*(mainly for mutilated chess board)*} lemma mod_succ_lemma: "[| 0"}*} lemma add_le_self: "m:nat ==> m le (m #+ n)" apply (simp (no_asm_simp)) @@ -333,7 +335,7 @@ done -(** Cancellation laws for common factors in comparisons **) +subsection{*Cancellation Laws for Common Factors in Comparisons*} lemma mult_less_cancel_lemma: "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0 (k#*m) mod (k#*n) = k #* (m mod n)" @@ -492,7 +494,8 @@ "[| m: nat; n: nat |] ==> (m (EX k: nat. n = succ(m#+k))" by (auto intro: less_imp_succ_add) -(* on nat *) + +subsubsection{*More Lemmas About Difference*} lemma diff_is_0_lemma: "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n" diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Bool.thy --- a/src/ZF/Bool.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Bool.thy Sun Jul 14 15:14:43 2002 +0200 @@ -112,7 +112,7 @@ lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type or_type xor_type -(*** Laws for 'not' ***) +subsection{*Laws About 'not' *} lemma not_not [simp]: "a:bool ==> not(not(a)) = a" by (elim boolE, auto) @@ -123,7 +123,7 @@ lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)" by (elim boolE, auto) -(*** Laws about 'and' ***) +subsection{*Laws About 'and' *} lemma and_absorb [simp]: "a: bool ==> a and a = a" by (elim boolE, auto) @@ -138,7 +138,7 @@ (a or b) and c = (a and c) or (b and c)" by (elim boolE, auto) -(** binary 'or' **) +subsection{*Laws About 'or' *} lemma or_absorb [simp]: "a: bool ==> a or a = a" by (elim boolE, auto) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Cardinal.thy Sun Jul 14 15:14:43 2002 +0200 @@ -44,7 +44,7 @@ "lesspoll" :: "[i,i] => o" (infixl "\" 50) "LEAST " :: "[pttrn, o] => i" ("(3\_./ _)" [0, 10] 10) -(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***) +subsection{*The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 *} (** Lemma: Banach's Decomposition Theorem **) @@ -168,7 +168,7 @@ done -(*** lesspoll: contributions by Krzysztof Grabczewski ***) +subsection{*lesspoll: contributions by Krzysztof Grabczewski *} lemma lesspoll_not_refl: "~ (i \ i)" by (simp add: lesspoll_def) @@ -270,7 +270,7 @@ apply (rule the_0, blast) done -lemma Ord_Least: "Ord(LEAST x. P(x))" +lemma Ord_Least [intro,simp,TC]: "Ord(LEAST x. P(x))" apply (rule_tac P = "EX i. Ord(i) & P(i)" in case_split_thm) (*case_tac method not available yet; needs "inductive"*) apply safe @@ -466,7 +466,7 @@ done -(*** The finite cardinals ***) +subsection{*The finite cardinals *} lemma cons_lepoll_consD: "[| cons(u,A) \ cons(v,B); u~:A; v~:B |] ==> A \ B" @@ -585,7 +585,7 @@ done -(*** The first infinite cardinal: Omega, or nat ***) +subsection{*The first infinite cardinal: Omega, or nat *} (*This implies Kunen's Lemma 10.6*) lemma lt_not_lepoll: "[| n ~ i \ n" @@ -622,7 +622,7 @@ done -(*** Towards Cardinal Arithmetic ***) +subsection{*Towards Cardinal Arithmetic *} (** Congruence laws for successor, cardinal addition and multiplication **) (*Congruence law for cons under equipollence*) @@ -699,8 +699,9 @@ done -(*** Lemmas by Krzysztof Grabczewski. New proofs using cons_lepoll_cons. - Could easily generalise from succ to cons. ***) +subsection{*Lemmas by Krzysztof Grabczewski*} + +(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*) (*If A has at most n+1 elements and a:A then A-{a} has at most n.*) lemma Diff_sing_lepoll: @@ -903,6 +904,8 @@ apply (blast intro: Fin_into_Finite)+ done +lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite] + (*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" apply (unfold Finite_def) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/CardinalArith.thy Sun Jul 14 15:14:43 2002 +0200 @@ -88,7 +88,7 @@ done -(*** Cardinal addition ***) +subsection{*Cardinal addition*} text{*Note: Could omit proving the algebraic laws for cardinal addition and multiplication. On finite cardinals these operations coincide with @@ -214,7 +214,7 @@ done -(*** Cardinal multiplication ***) +subsection{*Cardinal multiplication*} (** Cardinal multiplication is commutative **) @@ -301,7 +301,7 @@ apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq) done -(*** Some inequalities for multiplication ***) +subsection{*Some inequalities for multiplication*} lemma prod_square_lepoll: "A \ A*A" apply (unfold lepoll_def inj_def) @@ -356,7 +356,7 @@ apply (blast intro: prod_lepoll_mono subset_imp_lepoll) done -(*** Multiplication of finite cardinals is "ordinary" multiplication ***) +subsection{*Multiplication of finite cardinals is "ordinary" multiplication*} lemma prod_succ_eqpoll: "succ(A)*B \ B + A*B" apply (unfold eqpoll_def) @@ -396,7 +396,7 @@ by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) -(*** Infinite Cardinals are Limit Ordinals ***) +subsection{*Infinite Cardinals are Limit Ordinals*} (*This proof is modelled upon one assuming nat<=A, with injection lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z @@ -623,6 +623,15 @@ apply (simp add: cmult_def [symmetric] InfCard_csquare_eq) done +lemma InfCard_square_eqpoll: "InfCard(K) ==> K \ K \ K" +apply (rule well_ord_InfCard_square_eq) + apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) +apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) +done + +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) **) lemma InfCard_le_cmult_eq: "[| InfCard(K); L le K; 0 K |*| L = K" @@ -672,8 +681,9 @@ might be InfCard(K) ==> |list(K)| = K. *) -(*** For every cardinal number there exists a greater one - [Kunen's Theorem 10.16, which would be trivial using AC] ***) +subsection{*For Every Cardinal Number There Exists A Greater One} + +text{*This result is Kunen's Theorem 10.16, which would be trivial using AC*} lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))" apply (unfold jump_cardinal_def) @@ -730,7 +740,7 @@ apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl]) done -(*** Basic properties of successor cardinals ***) +subsection{*Basic Properties of Successor Cardinals*} lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)" apply (unfold csucc_def) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Cardinal_AC.thy Sun Jul 14 15:14:43 2002 +0200 @@ -10,7 +10,7 @@ theory Cardinal_AC = CardinalArith + Zorn: -(*** Strengthened versions of existing theorems about cardinals ***) +subsection{*Strengthened Forms of Existing Theorems on Cardinals*} lemma cardinal_eqpoll: "|A| eqpoll A" apply (rule AC_well_ord [THEN exE]) @@ -65,7 +65,7 @@ done -(*** Other applications of AC ***) +subsection{*Other Applications of AC*} lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B" apply (rule cardinal_eqpoll diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Epsilon.thy --- a/src/ZF/Epsilon.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Epsilon.thy Sun Jul 14 15:14:43 2002 +0200 @@ -34,7 +34,7 @@ "rec(k,a,b) == recursor(a,b,k)" -(*** Basic closure properties ***) +subsection{*Basic Closure Properties*} lemma arg_subset_eclose: "A <= eclose(A)" apply (unfold eclose_def) @@ -77,7 +77,7 @@ by (rule arg_in_eclose_sing [THEN eclose_induct], blast) -(*** Leastness of eclose ***) +subsection{*Leastness of @{term eclose}*} (** eclose(A) is the least transitive set including A as a subset. **) @@ -117,7 +117,7 @@ done -(*** Epsilon recursion ***) +subsection{*Epsilon Recursion*} (*Unused...*) lemma mem_eclose_trans: "[| A: eclose(B); B: eclose(C) |] ==> A: eclose(C)" @@ -205,7 +205,7 @@ dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD]) done -(*** Rank ***) +subsection{*Rank*} (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) lemma rank: "rank(a) = (UN y:a. succ(rank(y)))" @@ -309,7 +309,7 @@ done -(*** Corollaries of leastness ***) +subsection{*Corollaries of Leastness*} lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)" apply (rule Transset_eclose [THEN eclose_least]) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Finite.thy --- a/src/ZF/Finite.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Finite.thy Sun Jul 14 15:14:43 2002 +0200 @@ -41,7 +41,7 @@ type_intros Fin.intros -subsection {* Finite powerset operator *} +subsection {* Finite Powerset Operator *} lemma Fin_mono: "A<=B ==> Fin(A) <= Fin(B)" apply (unfold Fin.defs) @@ -132,7 +132,7 @@ done -(*** Finite function space ***) +subsection{*Finite Function Space*} lemma FiniteFun_mono: "[| A<=C; B<=D |] ==> A -||> B <= C -||> D" diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Fixedpt.thy --- a/src/ZF/Fixedpt.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Fixedpt.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,11 +3,11 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Least and greatest fixed points; the Knaster-Tarski Theorem - Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb *) +header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*} + theory Fixedpt = equalities: constdefs @@ -23,7 +23,7 @@ "gfp(D,h) == Union({X: Pow(D). X <= h(X)})" -(*** Monotone operators ***) +subsection{*Monotone Operators*} lemma bnd_monoI: "[| h(D)<=D; @@ -124,7 +124,7 @@ apply (erule lfp_unfold) done -(*** General induction rule for least fixedpoints ***) +subsection{*General Induction Rule for Least Fixedpoints*} lemma Collect_is_pre_fixedpt: "[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) |] @@ -243,7 +243,7 @@ done -(*** Coinduction rules for greatest fixed points ***) +subsection{*Coinduction Rules for Greatest Fixed Points*} (*weak version*) lemma weak_coinduct: "[| a: X; X <= h(X); X <= D |] ==> a : gfp(D,h)" diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Inductive.thy --- a/src/ZF/Inductive.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Inductive.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory. *) +header{*Inductive and Coinductive Definitions*} + theory Inductive = Fixedpt + mono + QPair files "ind_syntax.ML" @@ -18,11 +19,4 @@ setup IndCases.setup setup DatatypeTactics.setup - -(*belongs to theory ZF*) -declare bspec [dest?] - -(*belongs to theory upair*) -declare UnI1 [elim?] UnI2 [elim?] - end diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/InfDatatype.thy --- a/src/ZF/InfDatatype.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/InfDatatype.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Infinite-branching datatype definitions *) +header{*Infinite-Branching Datatype Definitions*} + theory InfDatatype = Datatype + Univ + Finite + Cardinal_AC: lemmas fun_Limit_VfromE = diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/IsaMakefile Sun Jul 14 15:14:43 2002 +0200 @@ -43,7 +43,7 @@ Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ - Trancl.thy Univ.thy Update.thy \ + Trancl.thy Univ.thy \ WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \ ind_syntax.ML mono.thy pair.thy simpdata.ML \ thy_syntax.ML upair.thy diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/List.thy --- a/src/ZF/List.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/List.thy Sun Jul 14 15:14:43 2002 +0200 @@ -439,6 +439,8 @@ apply (erule rev_type [THEN list.induct], simp_all) done +lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1] + (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Main.thy --- a/src/ZF/Main.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Main.thy Sun Jul 14 15:14:43 2002 +0200 @@ -1,15 +1,8 @@ -(*$Id$ - theory Main includes everything except AC*) - -theory Main = Update + List + EquivClass + IntDiv + CardinalArith: +(*$Id$*) -(* belongs to theory Trancl *) -lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl] - and trancl_induct = trancl_induct [case_names initial step, induct set: trancl] - and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1] - and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1] +header{*Theory Main: Everything Except AC*} - +theory Main = List + IntDiv + CardinalArith: (*The theory of "iterates" logically belongs to Nat, but can't go there because primrec isn't available into after Datatype. The only theories defined @@ -48,29 +41,9 @@ by (induct n rule: nat_induct, simp_all) -(* belongs to theory Cardinal *) -declare Ord_Least [intro,simp,TC] - - -(* belongs to theory List *) -lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1] - (* belongs to theory IntDiv *) lemmas posDivAlg_induct = posDivAlg_induct [consumes 2] and negDivAlg_induct = negDivAlg_induct [consumes 2] -(* belongs to theory CardinalArith *) - -lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite] - -lemma InfCard_square_eqpoll: "InfCard(K) ==> K \ K \ K" -apply (rule well_ord_InfCard_square_eq) - apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) -apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) -done - -lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)" -by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord]) - end diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Nat.thy --- a/src/ZF/Nat.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Nat.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Natural numbers in Zermelo-Fraenkel Set Theory *) +header{*The Natural numbers As a Least Fixed Point*} + theory Nat = OrdQuant + Bool + mono: constdefs @@ -75,7 +76,7 @@ lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard] -(** Injectivity properties and induction **) +subsection{*Injectivity Properties and Induction*} (*Mathematical induction*) lemma nat_induct: @@ -139,7 +140,7 @@ by (blast dest!: lt_nat_in_nat) -(** Variations on mathematical induction **) +subsection{*Variations on Mathematical Induction*} (*complete induction*) @@ -226,8 +227,7 @@ lemma nat_cases: "[|k=0 ==> P; !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P" -apply (insert nat_cases_disj [of k], blast) -done +by (insert nat_cases_disj [of k], blast) (** nat_case **) @@ -250,9 +250,10 @@ done +subsection{*Recursion on the Natural Numbers*} -(** nat_rec -- used to define eclose and transrec, then obsolete - rec, from arith.ML, has fewer typing conditions **) +(** nat_rec is used to define eclose and transrec, then becomes obsolete. + The operator rec, from arith.thy, has fewer typing conditions **) lemma nat_rec_0: "nat_rec(0,a,b) = a" apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Order.thy --- a/src/ZF/Order.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Order.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,12 +3,12 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Orders in Zermelo-Fraenkel Set Theory - Results from the book "Set Theory: an Introduction to Independence Proofs" by Kenneth Kunen. Chapter 1, section 6. *) +header{*Partial and Total Orderings: Basic Definitions and Properties*} + theory Order = WF + Perm: constdefs @@ -48,9 +48,8 @@ ord_iso :: "[i,i,i,i]=>i" ("(\_, _\ \/ \_, _\)" 51) -(** Basic properties of the definitions **) +subsection{*Immediate Consequences of the Definitions*} -(*needed?*) lemma part_ord_Imp_asym: "part_ord(A,r) ==> asym(r Int A*A)" by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast) @@ -109,6 +108,8 @@ by (unfold trans_on_def pred_def, blast) +subsection{*Restricting an Ordering's Domain*} + (** The ordering's properties hold over all subsets of its domain [including initial segments of the form pred(A,x,r) **) @@ -165,6 +166,8 @@ done +subsection{*Empty and Unit Domains*} + (** Relations over the Empty Set **) lemma irrefl_0: "irrefl(0,r)" @@ -209,6 +212,10 @@ done +subsection{*Order-Isomorphisms*} + +text{*Suppes calls them "similarities"*} + (** Order-preserving (monotone) maps **) lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B" @@ -221,9 +228,6 @@ apply (force intro: apply_type dest: wf_on_not_refl)+ done - -(** Order-isomorphisms -- or similarities, as Suppes calls them **) - lemma ord_isoI: "[| f: bij(A, B); !!x y. [| x:A; y:A |] ==> : r <-> : s |] @@ -342,7 +346,7 @@ done -(*** Main results of Kunen, Chapter 1 section 6 ***) +subsection{*Main results of Kunen, Chapter 1 section 6*} (*Inductive argument for Kunen's Lemma 6.1, etc. Simple proof from Halmos, page 72*) @@ -456,7 +460,7 @@ well_ord_is_linear well_ord_ord_iso ord_iso_sym) done -(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **) +subsection{*Towards Kunen's Theorem 6.3: Linearity of the Similarity Relation*} lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B" by (unfold ord_iso_map_def, blast) @@ -564,8 +568,8 @@ apply (simp add: domain_ord_iso_map_cases) done -(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) -lemma well_ord_trichotomy: +text{*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*} +theorem well_ord_trichotomy: "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) | (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | @@ -585,7 +589,9 @@ done -(*** Properties of converse(r), by Krzysztof Grabczewski ***) +subsection{*Miscellaneous Results by Krzysztof Grabczewski*} + +(** Properties of converse(r) **) lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))" by (unfold irrefl_def, blast) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/OrderArith.thy --- a/src/ZF/OrderArith.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/OrderArith.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Towards ordinal arithmetic. Also useful with wfrec. *) +header{*Combining Orderings: Foundations of Ordinal Arithmetic*} + theory OrderArith = Order + Sum + Ordinal: constdefs @@ -32,29 +33,25 @@ "measure(A,f) == {: A*A. f(x) < f(y)}" -(**** Addition of relations -- disjoint sum ****) +subsection{*Addition of Relations -- Disjoint Sum*} (** Rewrite rules. Can be used to obtain introduction rules **) lemma radd_Inl_Inr_iff [iff]: " : radd(A,r,B,s) <-> a:A & b:B" -apply (unfold radd_def, blast) -done +by (unfold radd_def, blast) lemma radd_Inl_iff [iff]: " : radd(A,r,B,s) <-> a':A & a:A & :r" -apply (unfold radd_def, blast) -done +by (unfold radd_def, blast) lemma radd_Inr_iff [iff]: " : radd(A,r,B,s) <-> b':B & b:B & :s" -apply (unfold radd_def, blast) -done +by (unfold radd_def, blast) lemma radd_Inr_Inl_iff [iff]: " : radd(A,r,B,s) <-> False" -apply (unfold radd_def, blast) -done +by (unfold radd_def, blast) (** Elimination Rule **) @@ -64,8 +61,7 @@ !!x' x. [| p'=Inl(x'); p=Inl(x); : r; x':A; x:A |] ==> Q; !!y' y. [| p'=Inr(y'); p=Inr(y); : s; y':B; y:B |] ==> Q |] ==> Q" -apply (unfold radd_def, blast) -done +by (unfold radd_def, blast) (** Type checking **) @@ -80,8 +76,7 @@ lemma linear_radd: "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))" -apply (unfold linear_def, blast) -done +by (unfold linear_def, blast) (** Well-foundedness **) @@ -119,7 +114,8 @@ lemma sum_bij: "[| f: bij(A,C); g: bij(B,D) |] ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)" -apply (rule_tac d = "case (%x. Inl (converse (f) `x), %y. Inr (converse (g) `y))" in lam_bijective) +apply (rule_tac d = "case (%x. Inl (converse(f)`x), %y. Inr(converse(g)`y))" + in lam_bijective) apply (typecheck add: bij_is_inj inj_is_fun) apply (auto simp add: left_inverse_bij right_inverse_bij) done @@ -156,11 +152,10 @@ "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" -apply (rule sum_assoc_bij [THEN ord_isoI], auto) -done +by (rule sum_assoc_bij [THEN ord_isoI], auto) -(**** Multiplication of relations -- lexicographic product ****) +subsection{*Multiplication of Relations -- Lexicographic Product*} (** Rewrite rule. Can be used to obtain introduction rules **) @@ -169,23 +164,19 @@ (: r & a':A & a:A & b': B & b: B) | (: s & a'=a & a:A & b': B & b: B)" -apply (unfold rmult_def, blast) -done +by (unfold rmult_def, blast) lemma rmultE: "[| <, > : rmult(A,r,B,s); [| : r; a':A; a:A; b':B; b:B |] ==> Q; [| : s; a:A; a'=a; b':B; b:B |] ==> Q |] ==> Q" -apply blast -done +by blast (** Type checking **) lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)" -apply (unfold rmult_def) -apply (rule Collect_subset) -done +by (unfold rmult_def, rule Collect_subset) lemmas field_rmult = rmult_type [THEN field_rel_subset] @@ -193,8 +184,7 @@ lemma linear_rmult: "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" -apply (simp add: linear_def, blast) -done +by (simp add: linear_def, blast) (** Well-foundedness **) @@ -289,33 +279,28 @@ lemma sum_prod_distrib_bij: "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) : bij((A+B)*C, (A*C)+(B*C))" -apply (rule_tac d = "case (%., %.) " - in lam_bijective) -apply auto -done +by (rule_tac d = "case (%., %.) " + in lam_bijective, auto) lemma sum_prod_distrib_ord_iso: "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" -apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto) -done +by (rule sum_prod_distrib_bij [THEN ord_isoI], auto) (** Associativity **) lemma prod_assoc_bij: "(lam <, z>:(A*B)*C. >) : bij((A*B)*C, A*(B*C))" -apply (rule_tac d = "%>. <, z>" in lam_bijective, auto) -done +by (rule_tac d = "%>. <, z>" in lam_bijective, auto) lemma prod_assoc_ord_iso: "(lam <, z>:(A*B)*C. >) : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" -apply (rule prod_assoc_bij [THEN ord_isoI], auto) -done +by (rule prod_assoc_bij [THEN ord_isoI], auto) -(**** Inverse image of a relation ****) +subsection{*Inverse Image of a Relation*} (** Rewrite rule **) @@ -325,8 +310,7 @@ (** Type checking **) lemma rvimage_type: "rvimage(A,f,r) <= A*A" -apply (unfold rvimage_def) -apply (rule Collect_subset) +apply (unfold rvimage_def, rule Collect_subset) done lemmas field_rvimage = rvimage_type [THEN field_rel_subset] @@ -410,8 +394,7 @@ lemma ord_iso_rvimage_eq: "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A" -apply (unfold ord_iso_def rvimage_def, blast) -done +by (unfold ord_iso_def rvimage_def, blast) (** The "measure" relation is useful with wfrec **) @@ -424,12 +407,10 @@ done lemma wf_measure [iff]: "wf(measure(A,f))" -apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage) -done +by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage) lemma measure_iff [iff]: " : measure(A,f) <-> x:A & y:A & f(x)i" @@ -108,7 +108,7 @@ apply (rule lamI [THEN imageI], assumption+) done -(*** Unfolding of ordermap ***) +subsubsection{*Unfolding of ordermap *} (*Useful for cardinality reasoning; see CardinalArith.ML*) lemma ordermap_eq_image: @@ -145,7 +145,7 @@ *) -(*** Showing that ordermap, ordertype yield ordinals ***) +subsubsection{*Showing that ordermap, ordertype yield ordinals *} lemma Ord_ordermap: "[| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)" @@ -170,7 +170,7 @@ done -(*** ordermap preserves the orderings in both directions ***) +subsubsection{*ordermap preserves the orderings in both directions *} lemma ordermap_mono: "[| : r; wf[A](r); w: A; x: A |] @@ -199,7 +199,7 @@ simp add: mem_not_refl) done -(*** Isomorphisms involving ordertype ***) +subsubsection{*Isomorphisms involving ordertype *} lemma ordertype_ord_iso: "well_ord(A,r) @@ -227,7 +227,7 @@ apply (erule ordertype_ord_iso [THEN ord_iso_sym]) done -(*** Basic equalities for ordertype ***) +subsubsection{*Basic equalities for ordertype *} (*Ordertype of Memrel*) lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j" @@ -255,7 +255,7 @@ ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *) lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq] -(*** A fundamental unfolding law for ordertype. ***) +subsubsection{*A fundamental unfolding law for ordertype. *} (*Ordermap returns the same result if applied to an initial segment*) lemma ordermap_pred_eq_ordermap: @@ -332,7 +332,7 @@ subsection{*Ordinal Addition*} -(*** Order Type calculations for radd ***) +subsubsection{*Order Type calculations for radd *} (** Addition with 0 **) @@ -398,7 +398,7 @@ done -(*** ordify: trivial coercion to an ordinal ***) +subsubsection{*ordify: trivial coercion to an ordinal *} lemma Ord_ordify [iff, TC]: "Ord(ordify(x))" by (simp add: ordify_def) @@ -408,7 +408,7 @@ by (simp add: ordify_def) -(*** Basic laws for ordinal addition ***) +subsubsection{*Basic laws for ordinal addition *} lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))" by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd @@ -552,7 +552,7 @@ done -(*** Ordinal addition with successor -- via associativity! ***) +subsubsection{*Ordinal addition with successor -- via associativity! *} lemma oadd_assoc: "(i++j)++k = i++(j++k)" apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify) @@ -599,7 +599,8 @@ lemma oadd_Limit: "Limit(j) ==> i++j = (UN k:j. i++k)" apply (frule Limit_has_0 [THEN ltD]) -apply (simp (no_asm_simp) add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] Union_eq_UN [symmetric] Limit_Union_eq) +apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] + Union_eq_UN [symmetric] Limit_Union_eq) done lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0" @@ -634,8 +635,8 @@ apply (rule le_trans) apply (rule_tac [2] le_implies_UN_le_UN) apply (erule_tac [2] bspec) -prefer 2 apply assumption -apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord) + prefer 2 apply assumption +apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord) done lemma oadd_le_mono1: "k le j ==> k++i le j++i" @@ -752,7 +753,7 @@ apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel) done -(*** A useful unfolding law ***) +subsubsection{*A useful unfolding law *} lemma pred_Pair_eq: "[| a:A; b:B |] ==> pred(A*B, , rmult(A,r,B,s)) = @@ -779,10 +780,12 @@ rmult(i,Memrel(i),j,Memrel(j))) = raw_oadd (j**i', j')" apply (unfold raw_oadd_def omult_def) -apply (simp (no_asm_simp) add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 well_ord_Memrel) +apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 + well_ord_Memrel) apply (rule trans) -apply (rule_tac [2] ordertype_ord_iso [THEN sum_ord_iso_cong, THEN ordertype_eq]) -apply (rule_tac [3] ord_iso_refl) + apply (rule_tac [2] ordertype_ord_iso + [THEN sum_ord_iso_cong, THEN ordertype_eq]) + apply (rule_tac [3] ord_iso_refl) apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq]) apply (elim SigmaE sumE ltE ssubst) apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel @@ -807,7 +810,7 @@ apply (rule ltI) prefer 2 apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2) -apply (simp (no_asm_simp) add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2) +apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2) apply (rule bexI) prefer 2 apply (blast elim!: ltE) apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric]) @@ -824,7 +827,7 @@ apply (blast intro: omult_oadd_lt [THEN ltD] ltI) done -(*** Basic laws for ordinal multiplication ***) +subsubsection{*Basic laws for ordinal multiplication *} (** Ordinal multiplication by zero **) @@ -886,7 +889,8 @@ apply (rule prod_ord_iso_cong [OF ord_iso_refl ordertype_ord_iso [THEN ord_iso_sym]]) apply (blast intro: well_ord_rmult well_ord_Memrel)+ -apply (rule prod_assoc_ord_iso [THEN ord_iso_sym, THEN ordertype_eq, THEN trans]) +apply (rule prod_assoc_ord_iso + [THEN ord_iso_sym, THEN ordertype_eq, THEN trans]) apply (rule_tac [2] ordertype_eq) apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl]) apply (blast intro: well_ord_rmult well_ord_Memrel Ord_ordertype)+ @@ -905,7 +909,7 @@ Union_eq_UN [symmetric] Limit_Union_eq) -(*** Ordering/monotonicity properties of ordinal multiplication ***) +subsubsection{*Ordering/monotonicity properties of ordinal multiplication *} (*As a special case we have "[| 0 0 < i**j" *) lemma lt_omult1: "[| k k < i**j" diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Ordinal.thy --- a/src/ZF/Ordinal.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Ordinal.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Ordinals in Zermelo-Fraenkel Set Theory *) +header{*Transitive Sets and Ordinals*} + theory Ordinal = WF + Bool + equalities: constdefs @@ -35,9 +36,9 @@ "op le" :: "[i,i] => o" (infixl "\" 50) (*less-than or equals*) -(*** Rules for Transset ***) +subsection{*Rules for Transset*} -(** Three neat characterisations of Transset **) +subsubsection{*Three Neat Characterisations of Transset*} lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)" by (unfold Transset_def, blast) @@ -50,7 +51,7 @@ lemma Transset_iff_Union_subset: "Transset(A) <-> Union(A) <= A" by (unfold Transset_def, blast) -(** Consequences of downwards closure **) +subsubsection{*Consequences of Downwards Closure*} lemma Transset_doubleton_D: "[| Transset(C); {a,b}: C |] ==> a:C & b: C" @@ -70,7 +71,7 @@ "[| Transset(C); A*B <= C; a: A |] ==> B <= C" by (blast dest: Transset_Pair_D) -(** Closure properties **) +subsubsection{*Closure Properties*} lemma Transset_0: "Transset(0)" by (unfold Transset_def, blast) @@ -109,7 +110,7 @@ by (rule Transset_Inter_family, auto) -(*** Natural Deduction rules for Ord ***) +subsection{*Lemmas for Ordinals*} lemma OrdI: "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)" @@ -122,7 +123,6 @@ "[| Ord(i); j:i |] ==> Transset(j) " by (unfold Ord_def, blast) -(*** Lemmas for ordinals ***) lemma Ord_in_Ord: "[| Ord(i); j:i |] ==> Ord(j)" by (unfold Ord_def Transset_def, blast) @@ -147,7 +147,7 @@ by (blast dest: OrdmemD) -(*** The construction of ordinals: 0, succ, Union ***) +subsection{*The Construction of Ordinals: 0, succ, Union*} lemma Ord_0 [iff,TC]: "Ord(0)" by (blast intro: OrdI Transset_0) @@ -180,7 +180,7 @@ apply (blast intro: Ord_in_Ord)+ done -(*** < is 'less than' for ordinals ***) +subsection{*< is 'less Than' for Ordinals*} lemma ltI: "[| i:j; Ord(j) |] ==> i : Memrel(A) <-> a:b & a:A & b:A" @@ -311,7 +311,7 @@ by (unfold Transset_def, blast) -(*** Transfinite induction ***) +subsection{*Transfinite Induction*} (*Epsilon induction over a transitive set*) lemma Transset_induct: @@ -339,7 +339,7 @@ (*** Fundamental properties of the epsilon ordering (< on ordinals) ***) -(** Proving that < is a linear ordering on the ordinals **) +subsubsection{*Proving That < is a Linear Ordering on the Ordinals*} lemma Ord_linear [rule_format]: "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)" @@ -374,7 +374,7 @@ lemma not_lt_imp_le: "[| ~ i j le i" by (rule_tac i = "i" and j = "j" in Ord_linear2, auto) -(** Some rewrite rules for <, le **) +subsubsection{*Some Rewrite Rules for <, le*} lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i x j le i" by (blast intro: not_lt_imp_le dest: lt_irrefl) -(** Transitive laws **) +subsubsection{*Transitivity Laws*} lemma lt_trans1: "[| i le j; j i i le i Un j" by (rule Un_upper1 [THEN subset_imp_le], auto) @@ -539,7 +539,7 @@ by (blast intro: Ord_trans) -(*** Results about limits ***) +subsection{*Results about Limits*} lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))" apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) @@ -612,7 +612,7 @@ by (blast intro: Ord_trans) -(*** Limit ordinals -- general properties ***) +subsection{*Limit Ordinals -- General Properties*} lemma Limit_Union_eq: "Limit(i) ==> Union(i) = i" apply (unfold Limit_def) @@ -666,7 +666,7 @@ by (blast elim!: leE) -(** Traditional 3-way case analysis on ordinals **) +subsubsection{*Traditional 3-Way Case Analysis on Ordinals*} lemma Ord_cases_disj: "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)" by (blast intro!: non_succ_LimitI Ord_0_lt) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Perm.thy --- a/src/ZF/Perm.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Perm.thy Sun Jul 14 15:14:43 2002 +0200 @@ -9,6 +9,8 @@ -- Lemmas for the Schroeder-Bernstein Theorem *) +header{*Injections, Surjections, Bijections, Composition*} + theory Perm = mono + func: constdefs @@ -35,6 +37,8 @@ "bij(A,B) == inj(A,B) Int surj(A,B)" +subsection{*Surjections*} + (** Surjective function space **) lemma surj_is_fun: "f: surj(A,B) ==> f: A->B" @@ -77,6 +81,8 @@ done +subsection{*Injections*} + (** Injective function space **) lemma inj_is_fun: "f: inj(A,B) ==> f: A->B" @@ -109,7 +115,7 @@ apply (simp_all add: lam_type) done -(** Bijections **) +subsection{*Bijections*} lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)" apply (unfold bij_def) @@ -141,7 +147,7 @@ done -(** Identity function **) +subsection{*Identity Function*} lemma idI [intro!]: "a:A ==> : id(A)" apply (unfold id_def) @@ -225,7 +231,7 @@ lemma right_inverse_bij: "[| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b" by (force simp add: bij_def surj_range) -(** Converses of injections, surjections, bijections **) +subsection{*Converses of Injections, Surjections, Bijections*} lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)" apply (rule f_imp_injective) @@ -247,7 +253,7 @@ -(** Composition of two relations **) +subsection{*Composition of Two Relations*} (*The inductive definition package could derive these theorems for (r O s)*) @@ -270,7 +276,7 @@ by blast -(** Domain and Range -- see Suppes, section 3.1 **) +subsection{*Domain and Range -- see Suppes, Section 3.1*} (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*) lemma range_comp: "range(r O s) <= range(r)" @@ -289,7 +295,7 @@ by blast -(** Other results **) +subsection{*Other Results*} lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)" by blast @@ -315,7 +321,7 @@ by blast -(** Composition preserves functions, injections, and surjections **) +subsection{*Composition Preserves Functions, Injections, and Surjections*} lemma comp_function: "[| function(g); function(f) |] ==> function(f O g)" by (unfold function_def, blast) @@ -367,14 +373,15 @@ done -(** Dual properties of inj and surj -- useful for proofs from +subsection{*Dual Properties of @{term inj} and @{term surj}*} + +text{*Useful for proofs from D Pastre. Automatic theorem proving in set theory. - Artificial Intelligence, 10:1--27, 1978. **) + Artificial Intelligence, 10:1--27, 1978.*} lemma comp_mem_injD1: "[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)" -apply (unfold inj_def, force) -done +by (unfold inj_def, force) lemma comp_mem_injD2: "[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)" @@ -400,7 +407,7 @@ apply (blast intro: apply_funtype) done -(** inverses of composition **) +subsubsection{*Inverses of Composition*} (*left inverse of composition; one inclusion is f: A->B ==> id(A) <= converse(f) O f *) @@ -421,7 +428,7 @@ done -(** Proving that a function is a bijection **) +subsubsection{*Proving that a Function is a Bijection*} lemma comp_eq_id_iff: "[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)" @@ -448,7 +455,9 @@ by (simp add: fg_imp_bijective comp_eq_id_iff left_inverse_lemma right_inverse_lemma) -(** Unions of functions -- cf similar theorems on func.ML **) +subsubsection{*Unions of Functions*} + +text{*See similar theorems in func.thy*} (*Theorem by KG, proof by LCP*) lemma inj_disjoint_Un: @@ -479,7 +488,7 @@ done -(** Restrictions as surjections and bijections *) +subsubsection{*Restrictions as Surjections and Bijections*} lemma surj_image: "f: Pi(A,B) ==> f: surj(A, f``A)" @@ -508,7 +517,7 @@ done -(*** Lemmas for Ramsey's Theorem ***) +subsubsection{*Lemmas for Ramsey's Theorem*} lemma inj_weaken_type: "[| f: inj(A,B); B<=D |] ==> f: inj(A,D)" apply (unfold inj_def) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/QPair.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,21 +3,24 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Quine-inspired ordered pairs and disjoint sums, for non-well-founded data -structures in ZF. Does not precisely follow Quine's construction. Thanks -to Thomas Forster for suggesting this approach! - -W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, -1966. - Many proofs are borrowed from pair.thy and sum.thy Do we EVER have rank(a) < rank() ? Perhaps if the latter rank is not a limit ordinal? *) +header{*Quine-Inspired Ordered Pairs and Disjoint Sums*} + theory QPair = Sum + mono: +text{*For non-well-founded data +structures in ZF. Does not precisely follow Quine's construction. Thanks +to Thomas Forster for suggesting this approach! + +W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, +1966. +*} + constdefs QPair :: "[i, i] => i" ("<(_;/ _)>") " == a+b" @@ -62,7 +65,7 @@ print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *} -(**** Quine ordered pairing ****) +subsection{*Quine ordered pairing*} (** Lemmas for showing that uniquely determines a and b **) @@ -83,8 +86,8 @@ by blast -(*** QSigma: Disjoint union of a family of sets - Generalizes Cartesian product ***) +subsubsection{*QSigma: Disjoint union of a family of sets + Generalizes Cartesian product*} lemma QSigmaI [intro!]: "[| a:A; b:B(a) |] ==> : QSigma(A,B)" by (simp add: QSigma_def) @@ -95,8 +98,7 @@ "[| c: QSigma(A,B); !!x y.[| x:A; y:B(x); c= |] ==> P |] ==> P" -apply (simp add: QSigma_def, blast) -done +by (simp add: QSigma_def, blast) (** Elimination rules for :A*B -- introducing no eigenvariables **) @@ -104,8 +106,7 @@ "[| c: QSigma(A,B); !!x y.[| x:A; y:B(x); c= |] ==> P |] ==> P" -apply (simp add: QSigma_def, blast) -done +by (simp add: QSigma_def, blast) lemma QSigmaE2 [elim!]: "[| : QSigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" @@ -129,7 +130,7 @@ by blast -(*** Projections: qfst, qsnd ***) +subsubsection{*Projections: qfst, qsnd*} lemma qfst_conv [simp]: "qfst() = a" by (simp add: qfst_def, blast) @@ -147,7 +148,7 @@ by auto -(*** Eliminator - qsplit ***) +subsubsection{*Eliminator: qsplit*} (*A META-equality, so that it applies to higher types as well...*) lemma qsplit [simp]: "qsplit(%x y. c(x,y), ) == c(a,b)" @@ -166,7 +167,7 @@ done -(*** qsplit for predicates: result type o ***) +subsubsection{*qsplit for predicates: result type o*} lemma qsplitI: "R(a,b) ==> qsplit(R, )" by (simp add: qsplit_def) @@ -176,14 +177,13 @@ "[| qsplit(R,z); z:QSigma(A,B); !!x y. [| z = ; R(x,y) |] ==> P |] ==> P" -apply (simp add: qsplit_def, auto) -done +by (simp add: qsplit_def, auto) lemma qsplitD: "qsplit(R,) ==> R(a,b)" by (simp add: qsplit_def) -(*** qconverse ***) +subsubsection{*qconverse*} lemma qconverseI [intro!]: ":r ==> :qconverse(r)" by (simp add: qconverse_def, blast) @@ -195,8 +195,7 @@ "[| yx : qconverse(r); !!x y. [| yx=; :r |] ==> P |] ==> P" -apply (simp add: qconverse_def, blast) -done +by (simp add: qconverse_def, blast) lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" by blast @@ -211,7 +210,7 @@ by blast -(**** The Quine-inspired notion of disjoint sum ****) +subsection{*The Quine-inspired notion of disjoint sum*} lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def @@ -230,8 +229,7 @@ !!x. [| x:A; u=QInl(x) |] ==> P; !!y. [| y:B; u=QInr(y) |] ==> P |] ==> P" -apply (simp add: qsum_defs, blast) -done +by (simp add: qsum_defs, blast) (** Injection and freeness equivalences, for rewriting **) @@ -268,8 +266,7 @@ lemma qsum_iff: "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))" -apply blast -done +by blast lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D" by blast @@ -279,7 +276,7 @@ apply blast done -(*** Eliminator -- qcase ***) +subsubsection{*Eliminator -- qcase*} lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)" by (simp add: qsum_defs ) @@ -293,8 +290,7 @@ !!x. x: A ==> c(x): C(QInl(x)); !!y. y: B ==> d(y): C(QInr(y)) |] ==> qcase(c,d,u) : C(u)" -apply (simp add: qsum_defs , auto) -done +by (simp add: qsum_defs , auto) (** Rules for the Part primitive **) @@ -311,7 +307,7 @@ by blast -(*** Monotonicity ***) +subsubsection{*Monotonicity*} lemma QPair_mono: "[| a<=c; b<=d |] ==> <= " by (simp add: QPair_def sum_mono) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/QUniv.thy --- a/src/ZF/QUniv.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/QUniv.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,10 +3,9 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -A small universe for lazy recursive types *) -(** Properties involving Transset and Sum **) +header{*A Small Universe for Lazy Recursive Types*} theory QUniv = Univ + QPair + mono + equalities: @@ -27,6 +26,8 @@ "quniv(A) == Pow(univ(eclose(A)))" +subsection{*Properties involving Transset and Sum*} + lemma Transset_includes_summands: "[| Transset(C); A+B <= C |] ==> A <= C & B <= C" apply (simp add: sum_def Un_subset_iff) @@ -39,7 +40,7 @@ apply (blast dest: Transset_Pair_D) done -(** Introduction and elimination rules avoid tiresome folding/unfolding **) +subsection{*Introduction and Elimination Rules*} lemma qunivI: "X <= univ(eclose(A)) ==> X : quniv(A)" by (simp add: quniv_def) @@ -52,7 +53,7 @@ apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono]) done -(*** Closure properties ***) +subsection{*Closure Properties*} lemma univ_eclose_subset_quniv: "univ(eclose(A)) <= quniv(A)" apply (simp add: quniv_def Transset_iff_Pow [symmetric]) @@ -90,7 +91,7 @@ "[| a <= univ(A); b <= univ(A) |] ==> <= univ(A)" by (simp add: QPair_def sum_subset_univ) -(** Quine disjoint sum **) +subsection{*Quine Disjoint Sum*} lemma QInl_subset_univ: "a <= univ(A) ==> QInl(a) <= univ(A)" apply (unfold QInl_def) @@ -108,7 +109,7 @@ apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ]) done -(*** Closure for Quine-inspired products and sums ***) +subsection{*Closure for Quine-Inspired Products and Sums*} (*Quine ordered pairs*) lemma QPair_in_quniv: @@ -135,7 +136,7 @@ by (blast intro: QPair_in_quniv dest: quniv_QPair_D) -(** Quine disjoint sum **) +subsection{*Quine Disjoint Sum*} lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) : quniv(A)" by (simp add: QInl_def zero_in_quniv QPair_in_quniv) @@ -149,7 +150,7 @@ lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv] -(*** The natural numbers ***) +subsection{*The Natural Numbers*} lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv] @@ -161,7 +162,7 @@ lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard] -(*** Intersecting with Vfrom... ***) +(*Intersecting with Vfrom...*) lemma QPair_Int_Vfrom_succ_subset: "Transset(X) ==> @@ -170,7 +171,9 @@ product_Int_Vfrom_subset [THEN subset_trans] Sigma_mono [OF Int_lower1 subset_refl]) -(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****) +subsection{*"Take-Lemma" Rules*} + +(*for proving a=b by coinduction and c: quniv(A)*) (*Rule for level i -- preserving the level, not decreasing it*) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Sum.thy --- a/src/ZF/Sum.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Sum.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,12 +3,14 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Disjoint sums in Zermelo-Fraenkel Set Theory -"Part" primitive for simultaneous recursive type definitions *) +header{*Disjoint Sums*} + theory Sum = Bool + equalities: +text{*And the "Part" primitive for simultaneous recursive type definitions*} + global constdefs @@ -30,7 +32,7 @@ local -(*** Rules for the Part primitive ***) +subsection{*Rules for the @{term Part} Primitive*} lemma Part_iff: "a : Part(A,h) <-> a:A & (EX y. a=h(y))" @@ -56,7 +58,7 @@ done -(*** Rules for Disjoint Sums ***) +subsection{*Rules for Disjoint Sums*} lemmas sum_defs = sum_def Inl_def Inr_def case_def @@ -130,7 +132,7 @@ by (simp add: sum_def, blast) -(*** Eliminator -- case ***) +subsection{*The Eliminator: @{term case}*} lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)" by (simp add: sum_defs) @@ -165,7 +167,7 @@ by auto -(*** More rules for Part(A,h) ***) +subsection{*More Rules for @{term "Part(A,h)"}*} lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)" by blast diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Trancl.thy --- a/src/ZF/Trancl.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Trancl.thy Sun Jul 14 15:14:43 2002 +0200 @@ -1,12 +1,12 @@ -(* Title: ZF/trancl.thy +(* Title: ZF/Trancl.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -1. General Properties of relations -2. Transitive closure of a relation *) +header{*Relations: Their General Properties and Transitive Closure*} + theory Trancl = Fixedpt + Perm + mono: constdefs @@ -56,8 +56,7 @@ lemma symI: "[| !!x y.: r ==> : r |] ==> sym(r)" -apply (unfold sym_def, blast) -done +by (unfold sym_def, blast) lemma antisymI: "[| sym(r); : r |] ==> : r" by (unfold sym_def, blast) @@ -66,8 +65,7 @@ lemma antisymI: "[| !!x y.[| : r; : r |] ==> x=y |] ==> antisym(r)" -apply (simp add: antisym_def, blast) -done +by (simp add: antisym_def, blast) lemma antisymE: "[| antisym(r); : r; : r |] ==> x=y" by (simp add: antisym_def, blast) @@ -365,6 +363,12 @@ apply (auto simp add: trancl_converse) done +lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl] + and trancl_induct = trancl_induct [case_names initial step, induct set: trancl] + and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1] + and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1] + + ML {* val refl_def = thm "refl_def"; diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Univ.thy --- a/src/ZF/Univ.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Univ.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,14 +3,14 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -The cumulative hierarchy and a small universe for recursive types - Standard notation for Vset(i) is V(i), but users might want V for a variable NOTE: univ(A) could be a translation; would simplify many proofs! But Ind_Syntax.univ refers to the constant "Univ.univ" *) +header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*} + theory Univ = Epsilon + Cardinal: constdefs @@ -35,6 +35,8 @@ "univ(A) == Vfrom(A,nat)" +subsection{*Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}*} + text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*} lemma Vfrom: "Vfrom(A,i) = A Un (\j\i. Pow(Vfrom(A,j)))" by (subst Vfrom_def [THEN def_transrec], simp) @@ -87,7 +89,7 @@ done -subsection{* Basic closure properties *} +subsection{* Basic Closure Properties *} lemma zero_in_Vfrom: "y:x ==> 0 \ Vfrom(A,x)" by (subst Vfrom, blast) @@ -128,7 +130,7 @@ apply (rule Vfrom_mono [OF subset_refl subset_succI]) done -subsection{* 0, successor and limit equations fof Vfrom *} +subsection{* 0, Successor and Limit Equations for @{term Vfrom} *} lemma Vfrom_0: "Vfrom(A,0) = A" by (subst Vfrom, blast) @@ -169,7 +171,7 @@ apply (subst Vfrom, blast) done -subsection{* Vfrom applied to Limit ordinals *} +subsection{* @{term Vfrom} applied to Limit Ordinals *} (*NB. limit ordinals are non-empty: Vfrom(A,0) = A = A Un (\y\0. Vfrom(A,y)) *) @@ -235,7 +237,7 @@ lemma nat_into_VLimit: "[| n: nat; Limit(i) |] ==> n \ Vfrom(A,i)" by (blast intro: nat_subset_VLimit [THEN subsetD]) -subsubsection{* Closure under disjoint union *} +subsubsection{* Closure under Disjoint Union *} lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard] @@ -261,7 +263,7 @@ -subsection{* Properties assuming Transset(A) *} +subsection{* Properties assuming @{term "Transset(A)"} *} lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))" apply (rule_tac a=i in eps_induct) @@ -324,7 +326,7 @@ apply (blast intro: Limit_has_0 Limit_has_succ VfromI) done -subsubsection{* products *} +subsubsection{* Products *} lemma prod_in_Vfrom: "[| a \ Vfrom(A,j); b \ Vfrom(A,j); Transset(A) |] @@ -342,7 +344,7 @@ apply (blast intro: prod_in_Vfrom Limit_has_succ) done -subsubsection{* Disjoint sums, aka Quine ordered pairs *} +subsubsection{* Disjoint Sums, or Quine Ordered Pairs *} lemma sum_in_Vfrom: "[| a \ Vfrom(A,j); b \ Vfrom(A,j); Transset(A); 1:j |] @@ -361,7 +363,7 @@ apply (blast intro: sum_in_Vfrom Limit_has_succ) done -subsubsection{* function space! *} +subsubsection{* Function Space! *} lemma fun_in_Vfrom: "[| a \ Vfrom(A,j); b \ Vfrom(A,j); Transset(A) |] ==> @@ -399,7 +401,7 @@ by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI) -subsection{* The set Vset(i) *} +subsection{* The Set @{term "Vset(i)"} *} lemma Vset: "Vset(i) = (\j\i. Pow(Vset(j)))" by (subst Vfrom, blast) @@ -407,7 +409,7 @@ lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard] lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard] -subsubsection{* Characterisation of the elements of Vset(i) *} +subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *} lemma VsetD [rule_format]: "Ord(i) ==> \b. b \ Vset(i) --> rank(b) < i" apply (erule trans_induct) @@ -454,7 +456,7 @@ apply (simp add: Vset_succ) done -subsubsection{* Reasoning about sets in terms of their elements' ranks *} +subsubsection{* Reasoning about Sets in Terms of Their Elements' Ranks *} lemma arg_subset_Vset_rank: "a <= Vset(rank(a))" apply (rule subsetI) @@ -468,7 +470,7 @@ apply (blast intro: Ord_rank) done -subsubsection{* Set up an environment for simplification *} +subsubsection{* Set Up an Environment for Simplification *} lemma rank_Inl: "rank(a) < rank(Inl(a))" apply (unfold Inl_def) @@ -482,7 +484,7 @@ lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2 -subsubsection{* Recursion over Vset levels! *} +subsubsection{* Recursion over Vset Levels! *} text{*NOT SUITABLE FOR REWRITING: recursive!*} lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))" @@ -515,7 +517,7 @@ done -subsection{* univ(A) *} +subsection{* The Datatype Universe: @{term "univ(A)"} *} lemma univ_mono: "A<=B ==> univ(A) <= univ(B)" apply (unfold univ_def) @@ -528,7 +530,7 @@ apply (erule Transset_Vfrom) done -subsubsection{* univ(A) as a limit *} +subsubsection{* The Set @{term"univ(A)"} as a Limit *} lemma univ_eq_UN: "univ(A) = (\i\nat. Vfrom(A,i))" apply (unfold univ_def) @@ -559,7 +561,7 @@ apply (blast elim: equalityCE) done -subsubsection{* Closure properties *} +subsection{* Closure Properties for @{term "univ(A)"}*} lemma zero_in_univ: "0 \ univ(A)" apply (unfold univ_def) @@ -576,7 +578,7 @@ lemmas A_into_univ = A_subset_univ [THEN subsetD, standard] -subsubsection{* Closure under unordered and ordered pairs *} +subsubsection{* Closure under Unordered and Ordered Pairs *} lemma singleton_in_univ: "a: univ(A) ==> {a} \ univ(A)" apply (unfold univ_def) @@ -607,7 +609,7 @@ done -subsubsection{* The natural numbers *} +subsubsection{* The Natural Numbers *} lemma nat_subset_univ: "nat <= univ(A)" apply (unfold univ_def) @@ -617,7 +619,7 @@ text{* n:nat ==> n:univ(A) *} lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard] -subsubsection{* instances for 1 and 2 *} +subsubsection{* Instances for 1 and 2 *} lemma one_in_univ: "1 \ univ(A)" apply (unfold univ_def) @@ -636,7 +638,7 @@ lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard] -subsubsection{* Closure under disjoint union *} +subsubsection{* Closure under Disjoint Union *} lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \ univ(A)" apply (unfold univ_def) @@ -669,7 +671,7 @@ subsection{* Finite Branching Closure Properties *} -subsubsection{* Closure under finite powerset *} +subsubsection{* Closure under Finite Powerset *} lemma Fin_Vfrom_lemma: "[| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j n -> Vfrom(A,i) <= Vfrom(A,i)" @@ -710,7 +712,7 @@ done -subsubsection{* Closure under finite function space *} +subsubsection{* Closure under Finite Function Space *} text{*General but seldom-used version; normally the domain is fixed*} lemma FiniteFun_VLimit1: @@ -749,7 +751,7 @@ subsection{** For QUniv. Properties of Vfrom analogous to the "take-lemma" **} -subsection{* Intersecting a*b with Vfrom... *} +text{* Intersecting a*b with Vfrom... *} text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*} lemma doubleton_in_Vfrom_D: diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/WF.thy --- a/src/ZF/WF.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/WF.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,8 +3,6 @@ Author: Tobias Nipkow and Lawrence C Paulson Copyright 1994 University of Cambridge -Well-founded Recursion - Derived first for transitive relations, and finally for arbitrary WF relations via wf_trancl and trans_trancl. @@ -17,6 +15,8 @@ a mess. *) +header{*Well-Founded Recursion*} + theory WF = Trancl + mono + equalities: constdefs @@ -45,7 +45,7 @@ "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)" -(*** Well-founded relations ***) +subsection{*Well-Founded Relations*} (** Equivalences between wf and wf_on **) @@ -153,7 +153,7 @@ done -(*** Properties of well-founded relations ***) +subsection{*Basic Properties of Well-Founded Relations*} lemma wf_not_refl: "wf(r) ==> ~: r" by (erule_tac a=a in wf_induct, blast) @@ -260,7 +260,7 @@ apply (blast dest: transD intro: is_recfun_equal) done -(*** Main Existence Lemma ***) +subsection{*Recursion: Main Existence Lemma*} lemma is_recfun_functional: "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g" @@ -304,7 +304,7 @@ done -(*** Unfolding wftrec ***) +subsection{*Unfolding @{term "wftrec(r,a,H)"}*} lemma the_recfun_cut: "[| wf(r); trans(r); :r |] diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/ZF.ML --- a/src/ZF/ZF.ML Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/ZF.ML Sun Jul 14 15:14:43 2002 +0200 @@ -504,11 +504,6 @@ by (best_tac cantor_cs 1); qed "cantor"; -(*Lemma for the inductive definition in theory Zorn*) -Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"; -by (Blast_tac 1); -qed "Union_in_Pow"; - Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))"; by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1); qed "atomize_ball"; diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/Zorn.thy --- a/src/ZF/Zorn.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/Zorn.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,16 +3,15 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Based upon the article - Abrial & Laffitte, - Towards the Mechanization of the Proofs of Some - Classical Theorems of Set Theory. - -Union_in_Pow is proved in ZF.ML *) +header{*Zorn's Lemma*} + theory Zorn = OrderArith + AC + Inductive: +text{*Based upon the unpublished article ``Towards the Mechanization of the +Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*} + constdefs Subset_rel :: "i=>i" "Subset_rel(A) == {z: A*A . EX x y. z= & x<=y & x~=y}" @@ -31,11 +30,17 @@ increasing :: "i=>i" "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}" -(** We could make the inductive definition conditional on next: increasing(S) + +(*Lemma for the inductive definition below*) +lemma Union_in_Pow: "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)" +by blast + + +text{*We could make the inductive definition conditional on + @{term "next \ increasing(S)"} but instead we make this a side-condition of an introduction rule. Thus the induction rule lets us assume that condition! Many inductive proofs - are therefore unconditional. -**) + are therefore unconditional.*} consts "TFin" :: "[i,i]=>i" @@ -52,16 +57,17 @@ type_intros CollectD1 [THEN apply_funtype] Union_in_Pow -(*** Section 1. Mathematical Preamble ***) +subsection{*Mathematical Preamble *} lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)" by blast -lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B" +lemma Inter_lemma0: + "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B" by blast -(*** Section 2. The Transfinite Construction ***) +subsection{*The Transfinite Construction *} lemma increasingD1: "f: increasing(A) ==> f: Pow(A)->Pow(A)" apply (unfold increasing_def) @@ -83,11 +89,10 @@ !!x. [| x : TFin(S,next); P(x); next: increasing(S) |] ==> P(next`x); !!Y. [| Y <= TFin(S,next); ALL y:Y. P(y) |] ==> P(Union(Y)) |] ==> P(n)" -apply (erule TFin.induct, blast+) -done +by (erule TFin.induct, blast+) -(*** Section 3. Some Properties of the Transfinite Construction ***) +subsection{*Some Properties of the Transfinite Construction *} lemmas increasing_trans = subset_trans [OF _ increasingD2, OF _ _ TFin_is_subset] @@ -170,8 +175,10 @@ done -(*** Section 4. Hausdorff's Theorem: every set contains a maximal chain ***) -(*** NB: We assume the partial ordering is <=, the subset relation! **) +subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain*} + +text{*NOTE: We assume the partial ordering is @{text "\"}, the subset +relation!*} (** Defining the "next" operation for Hausdorff's Theorem **) @@ -242,10 +249,11 @@ choice_super [THEN super_subset_chain [THEN subsetD]]) apply (unfold chain_def) apply (rule CollectI, blast, safe) -apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE], fast+) (*Blast_tac's slow*) +apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+) + (*Blast_tac's slow*) done -lemma Hausdorff: "EX c. c : maxchain(S)" +theorem Hausdorff: "EX c. c : maxchain(S)" apply (rule AC_Pi_Pow [THEN exE]) apply (rule Hausdorff_next_exists [THEN bexE], assumption) apply (rename_tac ch "next") @@ -266,14 +274,15 @@ done -(*** Section 5. Zorn's Lemma: if all chains in S have upper bounds in S - then S contains a maximal element ***) +subsection{*Zorn's Lemma*} + +text{*If all chains in S have upper bounds in S, + then S contains a maximal element *} (*Used in the proof of Zorn's Lemma*) lemma chain_extend: "[| c: chain(A); z: A; ALL x:c. x<=z |] ==> cons(z,c) : chain(A)" -apply (unfold chain_def, blast) -done +by (unfold chain_def, blast) lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z" apply (rule Hausdorff [THEN exE]) @@ -292,7 +301,7 @@ done -(*** Section 6. Zermelo's Theorem: every set can be well-ordered ***) +subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*} (*Lemma 5*) lemma TFin_well_lemma5: @@ -393,7 +402,7 @@ done (*The wellordering theorem*) -lemma AC_well_ord: "EX r. well_ord(S,r)" +theorem AC_well_ord: "EX r. well_ord(S,r)" apply (rule AC_Pi_Pow [THEN exE]) apply (rule Zermelo_next_exists [THEN bexE], assumption) apply (rule exI) diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/equalities.thy --- a/src/ZF/equalities.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/equalities.thy Sun Jul 14 15:14:43 2002 +0200 @@ -3,15 +3,15 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge - -Basic equations (and inclusions) involving union, intersection, -converse, domain, range, etc. - -Thanks also to Philippe de Groote. *) +header{*Basic Equalities and Inclusions*} + theory equalities = pair: +text{*These cover union, intersection, converse, domain, range, etc. Philippe +de Groote proved many of the inclusions.*} + (*FIXME: move to ZF.thy or even to FOL.thy??*) lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))" by blast @@ -54,10 +54,11 @@ lemma the_eq_0 [simp]: "(THE x. False) = 0" by (blast intro: the_0) -text {* \medskip Bounded quantifiers. +subsection{*Bounded Quantifiers*} +text {* \medskip The following are not added to the default simpset because - (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *} + (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*} lemma ball_Un: "(\x \ A\B. P(x)) <-> (\x \ A. P(x)) & (\x \ B. P(x))"; by blast @@ -71,7 +72,7 @@ lemma bex_UN: "(\z \ (UN x:A. B(x)). P(z)) <-> (\x\A. \z\B(x). P(z))" by blast -(*** converse ***) +subsection{*Converse of a Relation*} lemma converse_iff [iff]: ": converse(r) <-> :r" by (unfold converse_def, blast) @@ -105,7 +106,7 @@ by blast -(** cons; Finite Sets **) +subsection{*Finite Set Constructions Using @{term cons}*} lemma cons_subsetI: "[| a:C; B<=C |] ==> cons(a,B) <= C" by blast @@ -154,7 +155,7 @@ by blast -(*** succ ***) +(** succ **) lemma subset_succI: "i <= succ(i)" by blast @@ -166,14 +167,13 @@ lemma succ_subsetE: "[| succ(i) <= j; [| i:j; i<=j |] ==> P |] ==> P" -apply (unfold succ_def, blast) -done +by (unfold succ_def, blast) lemma succ_subset_iff: "succ(a) <= B <-> (a <= B & a : B)" by (unfold succ_def, blast) -(*** Binary Intersection ***) +subsection{*Binary Intersection*} (** Intersection is the greatest lower bound of two sets **) @@ -225,7 +225,7 @@ lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B" by blast -(*** Binary Union ***) +subsection{*Binary Union*} (** Union is the least upper bound of two sets *) @@ -277,7 +277,7 @@ lemma Un_eq_Union: "A Un B = Union({A, B})" by blast -(*** Set difference ***) +subsection{*Set Difference*} lemma Diff_subset: "A-B <= A" by blast @@ -354,7 +354,7 @@ by (blast elim!: equalityE) -(*** Big Union and Intersection ***) +subsection{*Big Union and Intersection*} (** Big Union is the least upper bound of a set **) @@ -424,7 +424,7 @@ "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))" by force -(*** Unions and Intersections of Families ***) +subsection{*Unions and Intersections of Families*} lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))" by (blast elim!: equalityE) @@ -739,7 +739,7 @@ by blast -(*** Image of a set under a function/relation ***) +subsection{*Image of a Set under a Function or Relation*} lemma image_iff: "b : r``A <-> (EX x:A. :r)" by (unfold image_def, blast) @@ -784,7 +784,7 @@ by blast -(*** Inverse image of a set under a function/relation ***) +subsection{*Inverse Image of a Set under a Function or Relation*} lemma vimage_iff: "a : r-``B <-> (EX y:B. :r)" @@ -868,7 +868,8 @@ apply (unfold Inter_def, blast) done -(** Pow **) + +subsection{*Powerset Operator*} lemma Pow_0 [simp]: "Pow(0) = {0}" by blast @@ -897,7 +898,8 @@ lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))" by blast -(*** RepFun ***) + +subsection{*RepFun*} lemma RepFun_subset: "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B" by blast @@ -910,7 +912,7 @@ apply blast done -(*** Collect ***) +subsection{*Collect*} lemma Collect_subset: "Collect(A,P) <= A" by blast diff -r d19cdbd8b559 -r c9cfe1638bf2 src/ZF/upair.thy --- a/src/ZF/upair.thy Sun Jul 14 15:11:21 2002 +0200 +++ b/src/ZF/upair.thy Sun Jul 14 15:14:43 2002 +0200 @@ -18,6 +18,9 @@ setup TypeCheck.setup declare atomize_ball [symmetric, rulify] +(*belongs to theory ZF*) +declare bspec [dest?] + (*** Lemmas about power sets ***) lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *) @@ -54,6 +57,9 @@ lemma UnI2: "c : B ==> c : A Un B" by simp +(*belongs to theory upair*) +declare UnI1 [elim?] UnI2 [elim?] + lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" apply simp apply blast