--- 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<omega,
@@ -402,7 +402,7 @@
by auto
-(*** Multiplication [the simprocs need these laws] ***)
+subsection{*Multiplication*}
lemma mult_0 [simp]: "0 #* m = 0"
by (simp add: mult_def)
--- a/src/ZF/ArithSimp.thy Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/ArithSimp.thy Sun Jul 14 15:14:43 2002 +0200
@@ -10,7 +10,7 @@
theory ArithSimp = Arith
files "arith_data.ML":
-(*** Difference ***)
+subsection{*Difference*}
lemma diff_self_eq_0: "m #- m = 0"
apply (subgoal_tac "natify (m) #- natify (m) = 0")
@@ -60,7 +60,7 @@
done
-(*** Remainder ***)
+subsection{*Remainder*}
(*We need m:nat even with natify*)
lemma div_termination: "[| 0<n; n le m; m:nat |] ==> 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<n; m:nat; n:nat |]
@@ -258,7 +260,7 @@
by (cut_tac n = "0" in mod2_add_more, auto)
-(**** Additional theorems about "le" ****)
+subsection{*Additional theorems about @{text "\<le>"}*}
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<n)"
@@ -408,7 +410,7 @@
done
-(** Distributive law for remainder (mod) **)
+subsection{*More Lemmas about Remainder*}
lemma mult_mod_distrib_raw:
"[| k:nat; m:nat; n:nat |] ==> (k#*m) mod (k#*n) = k #* (m mod n)"
@@ -492,7 +494,8 @@
"[| m: nat; n: nat |] ==> (m<n) <-> (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"
--- 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)
--- 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 "\<prec>" 50)
"LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [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 \<prec> 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) \<lesssim> cons(v,B); u~:A; v~:B |] ==> A \<lesssim> 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:nat |] ==> ~ i \<lesssim> 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)
--- 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 \<lesssim> 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 \<approx> 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 \<times> K \<approx> 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<L |] ==> 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)
--- 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
--- 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])
--- 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"
--- 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)"
--- 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
--- 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 =
--- 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
--- 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. ***)
--- 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 \<times> K \<approx> 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
--- 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])
--- 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" ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 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 |] ==> <x, y> : r <-> <f`x, f`y> : 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)
--- 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) == {<x,y>: 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]:
"<Inl(a), Inr(b)> : 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]:
"<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r"
-apply (unfold radd_def, blast)
-done
+by (unfold radd_def, blast)
lemma radd_Inr_iff [iff]:
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s"
-apply (unfold radd_def, blast)
-done
+by (unfold radd_def, blast)
lemma radd_Inr_Inl_iff [iff]:
"<Inr(b), Inl(a)> : 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); <x',x>: r; x':A; x:A |] ==> Q;
!!y' y. [| p'=Inr(y'); p=Inr(y); <y',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 @@
(<a',a>: r & a':A & a:A & b': B & 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:
"[| <<a',b'>, <a,b>> : rmult(A,r,B,s);
[| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q;
[| <b',b>: 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 <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
: bij((A+B)*C, (A*C)+(B*C))"
-apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) "
- in lam_bijective)
-apply auto
-done
+by (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) "
+ in lam_bijective, auto)
lemma sum_prod_distrib_ord_iso:
"(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), 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 <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
-apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
-done
+by (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
lemma prod_assoc_ord_iso:
"(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)
: 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]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
-apply (simp (no_asm) add: measure_def)
-done
+by (simp (no_asm) add: measure_def)
ML {*
val measure_def = thm "measure_def";
--- a/src/ZF/OrderType.thy Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/OrderType.thy Sun Jul 14 15:14:43 2002 +0200
@@ -3,16 +3,16 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory
-
-The order type of a well-ordering is the least ordinal isomorphic to it.
-
-Ordinal arithmetic is traditionally defined in terms of order types, as here.
-But a definition by transfinite recursion would be much simpler!
*)
+header{*Order Types and Ordinal Arithmetic*}
+
theory OrderType = OrderArith + OrdQuant + Nat:
+text{*The order type of a well-ordering is the least ordinal isomorphic to it.
+Ordinal arithmetic is traditionally defined in terms of order types, as it is
+here. But a definition by transfinite recursion would be much simpler!*}
+
constdefs
ordermap :: "[i,i]=>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:
"[| <w,x>: 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, <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<i; 0<j |] ==> 0 < i**j" *)
lemma lt_omult1: "[| k<i; 0<j |] ==> k < i**j"
--- 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 "\<le>" 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<j"
by (unfold lt_def, blast)
@@ -263,7 +263,7 @@
lemmas le0D = le0_iff [THEN iffD1, dest!]
-(*** Natural Deduction rules for Memrel ***)
+subsection{*Natural Deduction Rules for Memrel*}
(*The lemmas MemrelI/E give better speed than [iff] here*)
lemma Memrel_iff [simp]: "<a,b> : 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; Ord(i); Ord(j) |] ==> 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<j"
by (unfold lt_def, blast)
@@ -398,7 +398,7 @@
by (blast intro: Ord_0_lt)
-(*** Results about less-than or equals ***)
+subsection{*Results about Less-Than or Equals*}
(** For ordinals, j<=i (subset) implies j le i (less-than or equals) **)
@@ -425,7 +425,7 @@
lemma all_lt_imp_le: "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> 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<k |] ==> i<k"
by (blast elim!: leE intro: lt_trans)
@@ -477,7 +477,7 @@
apply (simp add: lt_def)
done
-(** Union and Intersection **)
+subsubsection{*Union and Intersection*}
lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> 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)
--- 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 ==> <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)
--- 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(<a;b>) ? 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> == a+b"
@@ -62,7 +65,7 @@
print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
-(**** Quine ordered pairing ****)
+subsection{*Quine ordered pairing*}
(** Lemmas for showing that <a;b> 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) |] ==> <a;b> : QSigma(A,B)"
by (simp add: QSigma_def)
@@ -95,8 +98,7 @@
"[| c: QSigma(A,B);
!!x y.[| x:A; y:B(x); c=<x;y> |] ==> P
|] ==> P"
-apply (simp add: QSigma_def, blast)
-done
+by (simp add: QSigma_def, blast)
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
@@ -104,8 +106,7 @@
"[| c: QSigma(A,B);
!!x y.[| x:A; y:B(x); c=<x;y> |] ==> P
|] ==> P"
-apply (simp add: QSigma_def, blast)
-done
+by (simp add: QSigma_def, blast)
lemma QSigmaE2 [elim!]:
"[| <a;b>: 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;b>) = 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), <a;b>) == 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, <a;b>)"
by (simp add: qsplit_def)
@@ -176,14 +177,13 @@
"[| qsplit(R,z); z:QSigma(A,B);
!!x y. [| z = <x;y>; R(x,y) |] ==> P
|] ==> P"
-apply (simp add: qsplit_def, auto)
-done
+by (simp add: qsplit_def, auto)
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
by (simp add: qsplit_def)
-(*** qconverse ***)
+subsubsection{*qconverse*}
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
by (simp add: qconverse_def, blast)
@@ -195,8 +195,7 @@
"[| yx : qconverse(r);
!!x y. [| yx=<y;x>; <x;y>: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 |] ==> <a;b> <= <c;d>"
by (simp add: QPair_def sum_mono)
--- 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) |] ==> <a;b> <= 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 <a;b> with Vfrom... ***)
+(*Intersecting <a;b> 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*)
--- 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
--- 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.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
-apply (unfold sym_def, blast)
-done
+by (unfold sym_def, blast)
lemma antisymI: "[| sym(r); <x,y>: r |] ==> <y,x>: r"
by (unfold sym_def, blast)
@@ -66,8 +65,7 @@
lemma antisymI:
"[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> antisym(r)"
-apply (simp add: antisym_def, blast)
-done
+by (simp add: antisym_def, blast)
lemma antisymE: "[| antisym(r); <x,y>: r; <y,x>: 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";
--- 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 (\<Union>j\<in>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 \<in> 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 (\<Union>y\<in>0. Vfrom(A,y)) *)
@@ -235,7 +237,7 @@
lemma nat_into_VLimit: "[| n: nat; Limit(i) |] ==> n \<in> 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 \<in> Vfrom(A,j); b \<in> 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 \<in> Vfrom(A,j); b \<in> 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 \<in> Vfrom(A,j); b \<in> 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) = (\<Union>j\<in>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) ==> \<forall>b. b \<in> 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) = (\<Union>i\<in>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 \<in> 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} \<in> 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 \<in> 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) \<in> 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<i"
@@ -693,7 +695,7 @@
apply (rule Limit_nat [THEN Fin_VLimit])
done
-subsubsection{* Closure under finite powers: functions from a natural number *}
+subsubsection{* Closure under Finite Powers: Functions from a Natural Number *}
lemma nat_fun_VLimit:
"[| n: nat; Limit(i) |] ==> 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:
--- 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) ==> <a,a> ~: 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); <b,a>:r |]
--- 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";
--- 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 & 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 \<in> 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 "\<subseteq>"}, 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)
--- 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: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
by blast
@@ -71,7 +72,7 @@
lemma bex_UN: "(\<exists>z \<in> (UN x:A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
by blast
-(*** converse ***)
+subsection{*Converse of a Relation*}
lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>: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. <x,b>: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. <a,y>: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
--- 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