# HG changeset patch
# User lcp
# Date 775316022 -7200
# Node ID 52f7447d4f1bf5a5c1fcd57d02944436f906a619
# Parent  af83700cb771bf5483844e2fe5a0fb6971697e50
Addition of infinite branching datatypes

diff -r af83700cb771 -r 52f7447d4f1b src/ZF/CardinalArith.ML
--- 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();
diff -r af83700cb771 -r 52f7447d4f1b src/ZF/Cardinal_AC.ML
--- 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();
+
diff -r af83700cb771 -r 52f7447d4f1b src/ZF/InfDatatype.ML
--- /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;
+
diff -r af83700cb771 -r 52f7447d4f1b src/ZF/InfDatatype.thy
--- /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
diff -r af83700cb771 -r 52f7447d4f1b src/ZF/Makefile
--- 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 ;;\
diff -r af83700cb771 -r 52f7447d4f1b src/ZF/README
--- 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)
diff -r af83700cb771 -r 52f7447d4f1b src/ZF/ROOT.ML
--- 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*)
diff -r af83700cb771 -r 52f7447d4f1b src/ZF/Univ.ML
--- 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 **)