better document preparation
authorpaulson
Tue Jul 09 23:05:26 2002 +0200 (2002-07-09)
changeset 13328703de709a64b
parent 13327 be7105a066d3
child 13329 53c4ec15cae0
better document preparation
src/ZF/AC.thy
src/ZF/Arith.thy
src/ZF/ArithSimp.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Constructible/Formula.thy
src/ZF/Datatype.thy
src/ZF/Epsilon.thy
src/ZF/Finite.thy
     1.1 --- a/src/ZF/AC.thy	Tue Jul 09 23:03:21 2002 +0200
     1.2 +++ b/src/ZF/AC.thy	Tue Jul 09 23:05:26 2002 +0200
     1.3 @@ -3,13 +3,13 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -The Axiom of Choice
     1.8 +*)
     1.9  
    1.10 -This definition comes from Halmos (1960), page 59.
    1.11 -*)
    1.12 +header{*The Axiom of Choice*}
    1.13  
    1.14  theory AC = Main:
    1.15  
    1.16 +text{*This definition comes from Halmos (1960), page 59.*}
    1.17  axioms AC: "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    1.18  
    1.19  (*The same as AC, but no premise a \<in> A*)
     2.1 --- a/src/ZF/Arith.thy	Tue Jul 09 23:03:21 2002 +0200
     2.2 +++ b/src/ZF/Arith.thy	Tue Jul 09 23:05:26 2002 +0200
     2.3 @@ -3,9 +3,6 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1992  University of Cambridge
     2.6  
     2.7 -Arithmetic operators and their definitions
     2.8 -
     2.9 -Proofs about elementary arithmetic: addition, multiplication, etc.
    2.10  *)
    2.11  
    2.12  (*"Difference" is subtraction of natural numbers.
    2.13 @@ -14,8 +11,12 @@
    2.14    Also, rec(m, 0, %z w.z) is pred(m).   
    2.15  *)
    2.16  
    2.17 +header{*Arithmetic Operators and Their Definitions*} 
    2.18 +
    2.19  theory Arith = Univ:
    2.20  
    2.21 +text{*Proofs about elementary arithmetic: addition, multiplication, etc.*}
    2.22 +
    2.23  constdefs
    2.24    pred   :: "i=>i"    (*inverse of succ*)
    2.25      "pred(y) == THE x. y = succ(x)"
     3.1 --- a/src/ZF/ArithSimp.thy	Tue Jul 09 23:03:21 2002 +0200
     3.2 +++ b/src/ZF/ArithSimp.thy	Tue Jul 09 23:05:26 2002 +0200
     3.3 @@ -3,9 +3,10 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   2000  University of Cambridge
     3.6  
     3.7 -Arithmetic with simplification
     3.8  *)
     3.9  
    3.10 +header{*Arithmetic with simplification*}
    3.11 +
    3.12  theory ArithSimp = Arith
    3.13  files "arith_data.ML":
    3.14  
     4.1 --- a/src/ZF/Bool.thy	Tue Jul 09 23:03:21 2002 +0200
     4.2 +++ b/src/ZF/Bool.thy	Tue Jul 09 23:05:26 2002 +0200
     4.3 @@ -3,10 +3,9 @@
     4.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5      Copyright   1992  University of Cambridge
     4.6  
     4.7 -Booleans in Zermelo-Fraenkel Set Theory 
     4.8 +*)
     4.9  
    4.10 -2 is equal to bool, but serves a different purpose
    4.11 -*)
    4.12 +header{*Booleans in Zermelo-Fraenkel Set Theory*}
    4.13  
    4.14  theory Bool = pair:
    4.15  
    4.16 @@ -18,6 +17,8 @@
    4.17     "1"  == "succ(0)"
    4.18     "2"  == "succ(1)"
    4.19  
    4.20 +text{*2 is equal to bool, but is used as a number rather than a type.*}
    4.21 +
    4.22  constdefs
    4.23    bool        :: i
    4.24      "bool == {0,1}"
     5.1 --- a/src/ZF/Cardinal.thy	Tue Jul 09 23:03:21 2002 +0200
     5.2 +++ b/src/ZF/Cardinal.thy	Tue Jul 09 23:05:26 2002 +0200
     5.3 @@ -3,10 +3,9 @@
     5.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.5      Copyright   1994  University of Cambridge
     5.6  
     5.7 -Cardinals in Zermelo-Fraenkel Set Theory 
     5.8 +*)
     5.9  
    5.10 -This theory does NOT assume the Axiom of Choice
    5.11 -*)
    5.12 +header{*Cardinal Numbers Without the Axiom of Choice*}
    5.13  
    5.14  theory Cardinal = OrderType + Finite + Nat + Sum:
    5.15  
     6.1 --- a/src/ZF/CardinalArith.thy	Tue Jul 09 23:03:21 2002 +0200
     6.2 +++ b/src/ZF/CardinalArith.thy	Tue Jul 09 23:05:26 2002 +0200
     6.3 @@ -3,13 +3,9 @@
     6.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.5      Copyright   1994  University of Cambridge
     6.6  
     6.7 -Cardinal arithmetic -- WITHOUT the Axiom of Choice
     6.8 +*)
     6.9  
    6.10 -Note: Could omit proving the algebraic laws for cardinal addition and
    6.11 -multiplication.  On finite cardinals these operations coincide with
    6.12 -addition and multiplication of natural numbers; on infinite cardinals they
    6.13 -coincide with union (maximum).  Either way we get most laws for free.
    6.14 -*)
    6.15 +header{*Cardinal Arithmetic Without the Axiom of Choice*}
    6.16  
    6.17  theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
    6.18  
    6.19 @@ -94,6 +90,11 @@
    6.20  
    6.21  (*** Cardinal addition ***)
    6.22  
    6.23 +text{*Note: Could omit proving the algebraic laws for cardinal addition and
    6.24 +multiplication.  On finite cardinals these operations coincide with
    6.25 +addition and multiplication of natural numbers; on infinite cardinals they
    6.26 +coincide with union (maximum).  Either way we get most laws for free.*}
    6.27 +
    6.28  (** Cardinal addition is commutative **)
    6.29  
    6.30  lemma sum_commute_eqpoll: "A+B \<approx> B+A"
     7.1 --- a/src/ZF/Cardinal_AC.thy	Tue Jul 09 23:03:21 2002 +0200
     7.2 +++ b/src/ZF/Cardinal_AC.thy	Tue Jul 09 23:05:26 2002 +0200
     7.3 @@ -3,11 +3,11 @@
     7.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.5      Copyright   1994  University of Cambridge
     7.6  
     7.7 -Cardinal Arithmetic WITH the Axiom of Choice
     7.8 -
     7.9  These results help justify infinite-branching datatypes
    7.10  *)
    7.11  
    7.12 +header{*Cardinal Arithmetic Using AC*}
    7.13 +
    7.14  theory Cardinal_AC = CardinalArith + Zorn:
    7.15  
    7.16  (*** Strengthened versions of existing theorems about cardinals ***)
     8.1 --- a/src/ZF/Constructible/Formula.thy	Tue Jul 09 23:03:21 2002 +0200
     8.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Jul 09 23:05:26 2002 +0200
     8.3 @@ -523,11 +523,6 @@
     8.4  
     8.5  subsubsection{*The subset relation*}
     8.6  
     8.7 -lemma lt_length_in_nat:
     8.8 -   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
     8.9 -apply (frule lt_nat_in_nat, typecheck) 
    8.10 -done
    8.11 -
    8.12  constdefs subset_fm :: "[i,i]=>i"
    8.13      "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
    8.14  
     9.1 --- a/src/ZF/Datatype.thy	Tue Jul 09 23:03:21 2002 +0200
     9.2 +++ b/src/ZF/Datatype.thy	Tue Jul 09 23:05:26 2002 +0200
     9.3 @@ -3,9 +3,10 @@
     9.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.5      Copyright   1997  University of Cambridge
     9.6  
     9.7 -(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
     9.8  *)
     9.9  
    9.10 +header{*Datatype and CoDatatype Definitions*}
    9.11 +
    9.12  theory Datatype = Inductive + Univ + QUniv
    9.13    files
    9.14      "Tools/datatype_package.ML"
    10.1 --- a/src/ZF/Epsilon.thy	Tue Jul 09 23:03:21 2002 +0200
    10.2 +++ b/src/ZF/Epsilon.thy	Tue Jul 09 23:05:26 2002 +0200
    10.3 @@ -3,9 +3,10 @@
    10.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.5      Copyright   1993  University of Cambridge
    10.6  
    10.7 -Epsilon induction and recursion
    10.8  *)
    10.9  
   10.10 +header{*Epsilon Induction and Recursion*}
   10.11 +
   10.12  theory Epsilon = Nat + mono:
   10.13  
   10.14  constdefs
    11.1 --- a/src/ZF/Finite.thy	Tue Jul 09 23:03:21 2002 +0200
    11.2 +++ b/src/ZF/Finite.thy	Tue Jul 09 23:05:26 2002 +0200
    11.3 @@ -3,13 +3,13 @@
    11.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.5      Copyright   1994  University of Cambridge
    11.6  
    11.7 -Finite powerset operator; finite function space
    11.8 -
    11.9  prove X:Fin(A) ==> |X| < nat
   11.10  
   11.11  prove:  b: Fin(A) ==> inj(b,b) <= surj(b,b)
   11.12  *)
   11.13  
   11.14 +header{*Finite Powerset Operator and Finite Function Space*}
   11.15 +
   11.16  theory Finite = Inductive + Epsilon + Nat:
   11.17  
   11.18  (*The natural numbers as a datatype*)