author paulson Tue Jul 09 23:05:26 2002 +0200 (2002-07-09) changeset 13328 703de709a64b parent 13327 be7105a066d3 child 13329 53c4ec15cae0
better document preparation
 src/ZF/AC.thy file | annotate | diff | revisions src/ZF/Arith.thy file | annotate | diff | revisions src/ZF/ArithSimp.thy file | annotate | diff | revisions src/ZF/Bool.thy file | annotate | diff | revisions src/ZF/Cardinal.thy file | annotate | diff | revisions src/ZF/CardinalArith.thy file | annotate | diff | revisions src/ZF/Cardinal_AC.thy file | annotate | diff | revisions src/ZF/Constructible/Formula.thy file | annotate | diff | revisions src/ZF/Datatype.thy file | annotate | diff | revisions src/ZF/Epsilon.thy file | annotate | diff | revisions src/ZF/Finite.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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.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*)
```