--- a/src/ZF/AC.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/AC.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-The Axiom of Choice
+*)
-This definition comes from Halmos (1960), page 59.
-*)
+header{*The Axiom of Choice*}
theory AC = Main:
+text{*This definition comes from Halmos (1960), page 59.*}
axioms AC: "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
(*The same as AC, but no premise a \<in> A*)
--- a/src/ZF/Arith.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Arith.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,6 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Arithmetic operators and their definitions
-
-Proofs about elementary arithmetic: addition, multiplication, etc.
*)
(*"Difference" is subtraction of natural numbers.
@@ -14,8 +11,12 @@
Also, rec(m, 0, %z w.z) is pred(m).
*)
+header{*Arithmetic Operators and Their Definitions*}
+
theory Arith = Univ:
+text{*Proofs about elementary arithmetic: addition, multiplication, etc.*}
+
constdefs
pred :: "i=>i" (*inverse of succ*)
"pred(y) == THE x. y = succ(x)"
--- a/src/ZF/ArithSimp.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/ArithSimp.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
-Arithmetic with simplification
*)
+header{*Arithmetic with simplification*}
+
theory ArithSimp = Arith
files "arith_data.ML":
--- a/src/ZF/Bool.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Bool.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,10 +3,9 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Booleans in Zermelo-Fraenkel Set Theory
+*)
-2 is equal to bool, but serves a different purpose
-*)
+header{*Booleans in Zermelo-Fraenkel Set Theory*}
theory Bool = pair:
@@ -18,6 +17,8 @@
"1" == "succ(0)"
"2" == "succ(1)"
+text{*2 is equal to bool, but is used as a number rather than a type.*}
+
constdefs
bool :: i
"bool == {0,1}"
--- a/src/ZF/Cardinal.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Cardinal.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,10 +3,9 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Cardinals in Zermelo-Fraenkel Set Theory
+*)
-This theory does NOT assume the Axiom of Choice
-*)
+header{*Cardinal Numbers Without the Axiom of Choice*}
theory Cardinal = OrderType + Finite + Nat + Sum:
--- a/src/ZF/CardinalArith.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/CardinalArith.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,9 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Cardinal arithmetic -- WITHOUT the Axiom of Choice
+*)
-Note: Could omit proving the algebraic laws for cardinal addition and
-multiplication. On finite cardinals these operations coincide with
-addition and multiplication of natural numbers; on infinite cardinals they
-coincide with union (maximum). Either way we get most laws for free.
-*)
+header{*Cardinal Arithmetic Without the Axiom of Choice*}
theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
@@ -94,6 +90,11 @@
(*** Cardinal addition ***)
+text{*Note: Could omit proving the algebraic laws for cardinal addition and
+multiplication. On finite cardinals these operations coincide with
+addition and multiplication of natural numbers; on infinite cardinals they
+coincide with union (maximum). Either way we get most laws for free.*}
+
(** Cardinal addition is commutative **)
lemma sum_commute_eqpoll: "A+B \<approx> B+A"
--- a/src/ZF/Cardinal_AC.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,11 +3,11 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Cardinal Arithmetic WITH the Axiom of Choice
-
These results help justify infinite-branching datatypes
*)
+header{*Cardinal Arithmetic Using AC*}
+
theory Cardinal_AC = CardinalArith + Zorn:
(*** Strengthened versions of existing theorems about cardinals ***)
--- a/src/ZF/Constructible/Formula.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy Tue Jul 09 23:05:26 2002 +0200
@@ -523,11 +523,6 @@
subsubsection{*The subset relation*}
-lemma lt_length_in_nat:
- "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
-apply (frule lt_nat_in_nat, typecheck)
-done
-
constdefs subset_fm :: "[i,i]=>i"
"subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
--- a/src/ZF/Datatype.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Datatype.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
*)
+header{*Datatype and CoDatatype Definitions*}
+
theory Datatype = Inductive + Univ + QUniv
files
"Tools/datatype_package.ML"
--- a/src/ZF/Epsilon.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Epsilon.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Epsilon induction and recursion
*)
+header{*Epsilon Induction and Recursion*}
+
theory Epsilon = Nat + mono:
constdefs
--- a/src/ZF/Finite.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Finite.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Finite powerset operator; finite function space
-
prove X:Fin(A) ==> |X| < nat
prove: b: Fin(A) ==> inj(b,b) <= surj(b,b)
*)
+header{*Finite Powerset Operator and Finite Function Space*}
+
theory Finite = Inductive + Epsilon + Nat:
(*The natural numbers as a datatype*)