--- a/src/ZF/CardinalArith.ML Wed Jul 27 15:14:31 1994 +0200
+++ b/src/ZF/CardinalArith.ML Wed Jul 27 15:33:42 1994 +0200
@@ -334,6 +334,10 @@
by (rtac (subset_succI RS subset_imp_lepoll) 1);
val nat_succ_eqpoll = result();
+goalw CardinalArith.thy [InfCard_def] "InfCard(nat)";
+by (fast_tac (ZF_cs addIs [Card_nat, le_refl, Card_is_Ord]) 1);
+val InfCard_nat = result();
+
goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)";
by (etac conjunct1 1);
val InfCard_is_Card = result();
@@ -635,3 +639,9 @@
by (asm_simp_tac
(ZF_ss addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1);
val Card_lt_csucc_iff = result();
+
+goalw CardinalArith.thy [InfCard_def]
+ "!!K. InfCard(K) ==> InfCard(csucc(K))";
+by (asm_simp_tac (ZF_ss addsimps [Card_csucc, Card_is_Ord,
+ lt_csucc RS leI RSN (2,le_trans)]) 1);
+val InfCard_csucc = result();
--- a/src/ZF/Cardinal_AC.ML Wed Jul 27 15:14:31 1994 +0200
+++ b/src/ZF/Cardinal_AC.ML Wed Jul 27 15:33:42 1994 +0200
@@ -115,7 +115,7 @@
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
val cardinal_UN_le = result();
-
+(*The same again, using csucc*)
goal Cardinal_AC.thy
"!!K. [| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] ==> \
\ |UN i:K. X(i)| < csucc(K)";
@@ -123,3 +123,15 @@
(ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le,
InfCard_is_Card, Card_cardinal]) 1);
val cardinal_UN_lt_csucc = result();
+
+(*The same again, for a union of ordinals*)
+goal Cardinal_AC.thy
+ "!!K. [| InfCard(K); ALL i:K. j(i) < csucc(K) |] ==> \
+\ (UN i:K. j(i)) < csucc(K)";
+by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);
+by (assume_tac 1);
+by (fast_tac (ZF_cs addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
+by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 1);
+by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
+val cardinal_UN_Ord_lt_csucc = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/InfDatatype.ML Wed Jul 27 15:33:42 1994 +0200
@@ -0,0 +1,76 @@
+(* Title: ZF/InfDatatype.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Infinite-Branching Datatype Definitions
+*)
+
+val fun_Limit_VfromE =
+ [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
+ |> standard;
+
+goal InfDatatype.thy
+ "!!K. [| f: K -> Vfrom(A,csucc(K)); InfCard(K) \
+\ |] ==> EX j. f: K -> Vfrom(A,j) & j < csucc(K)";
+by (res_inst_tac [("x", "UN k:K. LEAST i. f`k : Vfrom(A,i)")] exI 1);
+by (resolve_tac [conjI] 1);
+by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2);
+by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac);
+by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);
+by (resolve_tac [Pi_type] 1);
+by (rename_tac "k" 2);
+by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac);
+by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1);
+by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
+by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
+by (assume_tac 1);
+val fun_Vfrom_csucc_lemma = result();
+
+goal InfDatatype.thy
+ "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
+by (safe_tac (ZF_cs addSDs [fun_Vfrom_csucc_lemma]));
+by (resolve_tac [Vfrom RS ssubst] 1);
+by (eresolve_tac [PiE] 1);
+(*This level includes the function, and is below csucc(K)*)
+by (res_inst_tac [("a1", "succ(succ(K Un j))")] (UN_I RS UnI2) 1);
+by (eresolve_tac [subset_trans RS PowI] 2);
+by (safe_tac (ZF_cs addSIs [Pair_in_Vfrom]));
+by (fast_tac (ZF_cs addIs [i_subset_Vfrom RS subsetD]) 2);
+by (eresolve_tac [[subset_refl, Un_upper2] MRS Vfrom_mono RS subsetD] 2);
+by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit,
+ Limit_has_succ, Un_least_lt] 1));
+by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS lt_csucc] 1);
+by (assume_tac 1);
+val fun_Vfrom_csucc = result();
+
+goal InfDatatype.thy
+ "!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \
+\ |] ==> f: Vfrom(A,csucc(K))";
+by (REPEAT (ares_tac [fun_Vfrom_csucc RS subsetD] 1));
+val fun_in_Vfrom_csucc = result();
+
+val fun_subset_Vfrom_csucc =
+ [Pi_mono, fun_Vfrom_csucc] MRS subset_trans |> standard;
+
+goal InfDatatype.thy
+ "!!f. [| f: K -> B; B <= Vfrom(A,csucc(K)); InfCard(K) \
+\ |] ==> f: Vfrom(A,csucc(K))";
+by (REPEAT (ares_tac [fun_subset_Vfrom_csucc RS subsetD] 1));
+val fun_into_Vfrom_csucc = result();
+
+val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard;
+
+val Pair_in_Vfrom_csucc = Limit_csucc RSN (3, Pair_in_Vfrom_Limit) |> standard;
+val Inl_in_Vfrom_csucc = Limit_csucc RSN (2, Inl_in_Vfrom_Limit) |> standard;
+val Inr_in_Vfrom_csucc = Limit_csucc RSN (2, Inr_in_Vfrom_Limit) |> standard;
+val zero_in_Vfrom_csucc = Limit_csucc RS zero_in_Vfrom_Limit |> standard;
+val nat_into_Vfrom_csucc = Limit_csucc RSN (2, nat_into_Vfrom_Limit)
+ |> standard;
+
+(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
+val inf_datatype_intrs =
+ [fun_in_Vfrom_csucc, InfCard_nat, Pair_in_Vfrom_csucc,
+ Inl_in_Vfrom_csucc, Inr_in_Vfrom_csucc,
+ zero_in_Vfrom_csucc, A_into_Vfrom, nat_into_Vfrom_csucc] @ datatype_intrs;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/InfDatatype.thy Wed Jul 27 15:33:42 1994 +0200
@@ -0,0 +1,1 @@
+InfDatatype = Datatype + Univ + Cardinal_AC
--- a/src/ZF/Makefile Wed Jul 27 15:14:31 1994 +0200
+++ b/src/ZF/Makefile Wed Jul 27 15:33:42 1994 +0200
@@ -24,12 +24,12 @@
ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
+ Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
+ QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML \
OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \
Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
- Cardinal_AC.thy Cardinal_AC.ML \
+ Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \
Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \
- Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
- QUniv.thy QUniv.ML constructor.ML Datatype.ML \
List.ML ListFn.thy ListFn.ML
IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\
@@ -46,7 +46,7 @@
ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\
ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\
ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \
- ex/Ntree.ML ex/Ntree.thy \
+ ex/Ntree.ML ex/Brouwer.ML \
ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
#Uses cp rather than make_database because Poly/ML allows only 3 levels
@@ -62,7 +62,9 @@
$(BIN)/FOL:
cd ../FOL; $(MAKE)
-test: ex/ROOT.ML $(BIN)/ZF $(IMP_FILES) $(EX_FILES)
+#Directory IMP also tests the system
+#Load ex/ROOT.ML last since it creates the file "test"
+test: $(BIN)/ZF $(IMP_FILES) $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML"; quit();' | \
$(COMP) $(BIN)/ZF ;;\
--- a/src/ZF/README Wed Jul 27 15:14:31 1994 +0200
+++ b/src/ZF/README Wed Jul 27 15:33:42 1994 +0200
@@ -9,9 +9,38 @@
Makefile -- compiles the files under Poly/ML or SML of New Jersey
+IMP -- subdirectory containing a semantics equivalence proof between
+operational and denotational definitions of a simple programming language.
+To execute, enter an ML image containing ZF and type: use "IMP/ROOT.ML";
+
ex -- subdirectory containing examples. To execute them, enter an ML image
containing ZF and type: use "ex/ROOT.ML";
+Isabelle/ZF formalizes the greater part of elementary set theory, including
+relations, functions, injections, surjections, ordinals and cardinals.
+Results proved include Cantor's Theorem, the Recursion Theorem, the
+Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
+
+Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
+computational notions. It supports inductive definitions of
+infinite-branching trees for any cardinality of branching.
+
+Useful references for Isabelle/ZF:
+
+ Lawrence C. Paulson,
+ Set theory for verification: I. From foundations to functions.
+ J. Automated Reasoning 11 (1993), 353-389.
+
+ Lawrence C. Paulson,
+ Set theory for verification: II. Induction and recursion.
+ Report 312, Computer Lab (1993).
+
+ Lawrence C. Paulson,
+ A fixedpoint approach to implementing (co)inductive definitions.
+ In: A. Bundy (editor),
+ CADE-12: 12th International Conference on Automated Deduction,
+ (Springer LNAI 814, 1994), 148-161.
+
Useful references on ZF set theory:
Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
@@ -20,3 +49,7 @@
Keith J. Devlin,
Fundamentals of Contemporary Set Theory (Springer, 1979)
+
+ Kenneth Kunen
+ Set Theory: An Introduction to Independence Proofs
+ (North-Holland, 1980)
--- a/src/ZF/ROOT.ML Wed Jul 27 15:14:31 1994 +0200
+++ b/src/ZF/ROOT.ML Wed Jul 27 15:33:42 1994 +0200
@@ -28,7 +28,7 @@
print_depth 1;
-use_thy "Cardinal_AC";
+use_thy "InfDatatype";
use_thy "ListFn";
(*printing functions are inherited from FOL*)
--- a/src/ZF/Univ.ML Wed Jul 27 15:14:31 1994 +0200
+++ b/src/ZF/Univ.ML Wed Jul 27 15:33:42 1994 +0200
@@ -85,6 +85,8 @@
by (rtac Un_upper1 1);
val A_subset_Vfrom = result();
+val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard;
+
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
by (rtac (Vfrom RS ssubst) 1);
by (fast_tac ZF_cs 1);
@@ -249,7 +251,9 @@
[nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans
|> standard;
-val nat_into_Vfrom_Limit = standard (nat_subset_Vfrom_Limit RS subsetD);
+goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n : Vfrom(A,i)";
+by (REPEAT (ares_tac [nat_subset_Vfrom_Limit RS subsetD] 1));
+val nat_into_Vfrom_Limit = result();
(** Closure under disjoint union **)