Addition of infinite branching datatypes
authorlcp
Wed Jul 27 15:33:42 1994 +0200 (1994-07-27)
changeset 48852f7447d4f1b
parent 487 af83700cb771
child 489 0449a7f1add3
Addition of infinite branching datatypes
src/ZF/CardinalArith.ML
src/ZF/Cardinal_AC.ML
src/ZF/InfDatatype.ML
src/ZF/InfDatatype.thy
src/ZF/Makefile
src/ZF/README
src/ZF/ROOT.ML
src/ZF/Univ.ML
     1.1 --- a/src/ZF/CardinalArith.ML	Wed Jul 27 15:14:31 1994 +0200
     1.2 +++ b/src/ZF/CardinalArith.ML	Wed Jul 27 15:33:42 1994 +0200
     1.3 @@ -334,6 +334,10 @@
     1.4  by (rtac (subset_succI RS subset_imp_lepoll) 1);
     1.5  val nat_succ_eqpoll = result();
     1.6  
     1.7 +goalw CardinalArith.thy [InfCard_def] "InfCard(nat)";
     1.8 +by (fast_tac (ZF_cs addIs [Card_nat, le_refl, Card_is_Ord]) 1);
     1.9 +val InfCard_nat = result();
    1.10 +
    1.11  goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)";
    1.12  by (etac conjunct1 1);
    1.13  val InfCard_is_Card = result();
    1.14 @@ -635,3 +639,9 @@
    1.15  by (asm_simp_tac 
    1.16      (ZF_ss addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1);
    1.17  val Card_lt_csucc_iff = result();
    1.18 +
    1.19 +goalw CardinalArith.thy [InfCard_def]
    1.20 +    "!!K. InfCard(K) ==> InfCard(csucc(K))";
    1.21 +by (asm_simp_tac (ZF_ss addsimps [Card_csucc, Card_is_Ord, 
    1.22 +				  lt_csucc RS leI RSN (2,le_trans)]) 1);
    1.23 +val InfCard_csucc = result();
     2.1 --- a/src/ZF/Cardinal_AC.ML	Wed Jul 27 15:14:31 1994 +0200
     2.2 +++ b/src/ZF/Cardinal_AC.ML	Wed Jul 27 15:33:42 1994 +0200
     2.3 @@ -115,7 +115,7 @@
     2.4  by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
     2.5  val cardinal_UN_le = result();
     2.6  
     2.7 -
     2.8 +(*The same again, using csucc*)
     2.9  goal Cardinal_AC.thy
    2.10      "!!K. [| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |] ==> \
    2.11  \         |UN i:K. X(i)| < csucc(K)";
    2.12 @@ -123,3 +123,15 @@
    2.13      (ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 
    2.14  		     InfCard_is_Card, Card_cardinal]) 1);
    2.15  val cardinal_UN_lt_csucc = result();
    2.16 +
    2.17 +(*The same again, for a union of ordinals*)
    2.18 +goal Cardinal_AC.thy
    2.19 +    "!!K. [| InfCard(K);  ALL i:K. j(i) < csucc(K) |] ==> \
    2.20 +\         (UN i:K. j(i)) < csucc(K)";
    2.21 +by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);
    2.22 +by (assume_tac 1);
    2.23 +by (fast_tac (ZF_cs addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
    2.24 +by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 1);
    2.25 +by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
    2.26 +val cardinal_UN_Ord_lt_csucc = result();
    2.27 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/InfDatatype.ML	Wed Jul 27 15:33:42 1994 +0200
     3.3 @@ -0,0 +1,76 @@
     3.4 +(*  Title: 	ZF/InfDatatype.ML
     3.5 +    ID:         $Id$
     3.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1994  University of Cambridge
     3.8 +
     3.9 +Infinite-Branching Datatype Definitions
    3.10 +*)
    3.11 +
    3.12 +val fun_Limit_VfromE = 
    3.13 +    [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
    3.14 +	|> standard;
    3.15 +
    3.16 +goal InfDatatype.thy
    3.17 +    "!!K. [| f: K -> Vfrom(A,csucc(K));  InfCard(K)	\
    3.18 +\         |] ==> EX j. f: K -> Vfrom(A,j) & j < csucc(K)";
    3.19 +by (res_inst_tac [("x", "UN k:K. LEAST i. f`k : Vfrom(A,i)")] exI 1);
    3.20 +by (resolve_tac [conjI] 1);
    3.21 +by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2);
    3.22 +by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac);
    3.23 +by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);
    3.24 +by (resolve_tac [Pi_type] 1);
    3.25 +by (rename_tac "k" 2);
    3.26 +by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac);
    3.27 +by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1);
    3.28 +by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
    3.29 +by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
    3.30 +by (assume_tac 1);
    3.31 +val fun_Vfrom_csucc_lemma = result();
    3.32 +
    3.33 +goal InfDatatype.thy
    3.34 +    "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
    3.35 +by (safe_tac (ZF_cs addSDs [fun_Vfrom_csucc_lemma]));
    3.36 +by (resolve_tac [Vfrom RS ssubst] 1);
    3.37 +by (eresolve_tac [PiE] 1);
    3.38 +(*This level includes the function, and is below csucc(K)*)
    3.39 +by (res_inst_tac [("a1", "succ(succ(K Un j))")] (UN_I RS UnI2) 1);
    3.40 +by (eresolve_tac [subset_trans RS PowI] 2);
    3.41 +by (safe_tac (ZF_cs addSIs [Pair_in_Vfrom]));
    3.42 +by (fast_tac (ZF_cs addIs [i_subset_Vfrom RS subsetD]) 2);
    3.43 +by (eresolve_tac [[subset_refl, Un_upper2] MRS Vfrom_mono RS subsetD] 2);
    3.44 +by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, 
    3.45 +		      Limit_has_succ, Un_least_lt] 1));
    3.46 +by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS lt_csucc] 1);
    3.47 +by (assume_tac 1);
    3.48 +val fun_Vfrom_csucc = result();
    3.49 +
    3.50 +goal InfDatatype.thy
    3.51 +    "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
    3.52 +\         |] ==> f: Vfrom(A,csucc(K))";
    3.53 +by (REPEAT (ares_tac [fun_Vfrom_csucc RS subsetD] 1));
    3.54 +val fun_in_Vfrom_csucc = result();
    3.55 +
    3.56 +val fun_subset_Vfrom_csucc = 
    3.57 +	[Pi_mono, fun_Vfrom_csucc] MRS subset_trans |> standard;
    3.58 +
    3.59 +goal InfDatatype.thy
    3.60 +    "!!f. [| f: K -> B;  B <= Vfrom(A,csucc(K));  InfCard(K) \
    3.61 +\         |] ==> f: Vfrom(A,csucc(K))";
    3.62 +by (REPEAT (ares_tac [fun_subset_Vfrom_csucc RS subsetD] 1));
    3.63 +val fun_into_Vfrom_csucc = result();
    3.64 +
    3.65 +val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard;
    3.66 +
    3.67 +val Pair_in_Vfrom_csucc = Limit_csucc RSN (3, Pair_in_Vfrom_Limit) |> standard;
    3.68 +val Inl_in_Vfrom_csucc  = Limit_csucc RSN (2, Inl_in_Vfrom_Limit) |> standard;
    3.69 +val Inr_in_Vfrom_csucc  = Limit_csucc RSN (2, Inr_in_Vfrom_Limit) |> standard;
    3.70 +val zero_in_Vfrom_csucc = Limit_csucc RS zero_in_Vfrom_Limit |> standard;
    3.71 +val nat_into_Vfrom_csucc = Limit_csucc RSN (2, nat_into_Vfrom_Limit) 
    3.72 +			   |> standard;
    3.73 +
    3.74 +(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
    3.75 +val inf_datatype_intrs =  
    3.76 +    [fun_in_Vfrom_csucc, InfCard_nat, Pair_in_Vfrom_csucc, 
    3.77 +     Inl_in_Vfrom_csucc, Inr_in_Vfrom_csucc, 
    3.78 +     zero_in_Vfrom_csucc, A_into_Vfrom, nat_into_Vfrom_csucc] @ datatype_intrs;
    3.79 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/InfDatatype.thy	Wed Jul 27 15:33:42 1994 +0200
     4.3 @@ -0,0 +1,1 @@
     4.4 +InfDatatype = Datatype + Univ + Cardinal_AC
     5.1 --- a/src/ZF/Makefile	Wed Jul 27 15:14:31 1994 +0200
     5.2 +++ b/src/ZF/Makefile	Wed Jul 27 15:33:42 1994 +0200
     5.3 @@ -24,12 +24,12 @@
     5.4  	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
     5.5  	equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
     5.6  	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
     5.7 +	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
     5.8 +	QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML  \
     5.9  	OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \
    5.10  	Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
    5.11 -	Cardinal_AC.thy Cardinal_AC.ML \
    5.12 +	Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \
    5.13  	Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \
    5.14 -	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
    5.15 -	QUniv.thy QUniv.ML constructor.ML Datatype.ML  \
    5.16  	List.ML ListFn.thy ListFn.ML
    5.17  
    5.18  IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\
    5.19 @@ -46,7 +46,7 @@
    5.20  	   ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\
    5.21  	   ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\
    5.22  	   ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \
    5.23 -	   ex/Ntree.ML ex/Ntree.thy \
    5.24 +	   ex/Ntree.ML ex/Brouwer.ML \
    5.25  	   ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML
    5.26  
    5.27  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    5.28 @@ -62,7 +62,9 @@
    5.29  $(BIN)/FOL:
    5.30  	cd ../FOL;  $(MAKE)
    5.31  
    5.32 -test:   ex/ROOT.ML  $(BIN)/ZF  $(IMP_FILES) $(EX_FILES)
    5.33 +#Directory IMP also tests the system
    5.34 +#Load ex/ROOT.ML last since it creates the file "test"
    5.35 +test:   $(BIN)/ZF  $(IMP_FILES) $(EX_FILES)
    5.36  	case "$(COMP)" in \
    5.37  	poly*)	echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML"; quit();' | \
    5.38  			$(COMP) $(BIN)/ZF ;;\
     6.1 --- a/src/ZF/README	Wed Jul 27 15:14:31 1994 +0200
     6.2 +++ b/src/ZF/README	Wed Jul 27 15:33:42 1994 +0200
     6.3 @@ -9,9 +9,38 @@
     6.4  
     6.5  Makefile -- compiles the files under Poly/ML or SML of New Jersey
     6.6  
     6.7 +IMP -- subdirectory containing a semantics equivalence proof between
     6.8 +operational and denotational definitions of a simple programming language.
     6.9 +To execute, enter an ML image containing ZF and type:   use "IMP/ROOT.ML";
    6.10 +
    6.11  ex -- subdirectory containing examples.  To execute them, enter an ML image
    6.12  containing ZF and type:    use "ex/ROOT.ML";
    6.13  
    6.14 +Isabelle/ZF formalizes the greater part of elementary set theory, including
    6.15 +relations, functions, injections, surjections, ordinals and cardinals.
    6.16 +Results proved include Cantor's Theorem, the Recursion Theorem, the
    6.17 +Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
    6.18 +
    6.19 +Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
    6.20 +computational notions.  It supports inductive definitions of
    6.21 +infinite-branching trees for any cardinality of branching.
    6.22 +
    6.23 +Useful references for Isabelle/ZF:
    6.24 +
    6.25 +	Lawrence C. Paulson,
    6.26 +	Set theory for verification: I. From foundations to functions.
    6.27 +	J. Automated Reasoning 11 (1993), 353-389.
    6.28 +
    6.29 +	Lawrence C. Paulson,
    6.30 +	Set theory for verification: II. Induction and recursion.
    6.31 +	Report 312, Computer Lab (1993).
    6.32 +
    6.33 +	Lawrence C. Paulson,
    6.34 +	A fixedpoint approach to implementing (co)inductive definitions.  
    6.35 +	In: A. Bundy (editor),
    6.36 +	CADE-12: 12th International Conference on Automated Deduction,
    6.37 +	(Springer LNAI 814, 1994), 148-161.
    6.38 +
    6.39  Useful references on ZF set theory:
    6.40  
    6.41  	Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
    6.42 @@ -20,3 +49,7 @@
    6.43  
    6.44  	Keith J. Devlin,
    6.45  	Fundamentals of Contemporary Set Theory (Springer, 1979)
    6.46 +
    6.47 +	Kenneth Kunen
    6.48 +	Set Theory: An Introduction to Independence Proofs
    6.49 +	(North-Holland, 1980)
     7.1 --- a/src/ZF/ROOT.ML	Wed Jul 27 15:14:31 1994 +0200
     7.2 +++ b/src/ZF/ROOT.ML	Wed Jul 27 15:33:42 1994 +0200
     7.3 @@ -28,7 +28,7 @@
     7.4  
     7.5  print_depth 1;
     7.6  
     7.7 -use_thy "Cardinal_AC";
     7.8 +use_thy "InfDatatype";
     7.9  use_thy "ListFn";
    7.10  
    7.11  (*printing functions are inherited from FOL*)
     8.1 --- a/src/ZF/Univ.ML	Wed Jul 27 15:14:31 1994 +0200
     8.2 +++ b/src/ZF/Univ.ML	Wed Jul 27 15:33:42 1994 +0200
     8.3 @@ -85,6 +85,8 @@
     8.4  by (rtac Un_upper1 1);
     8.5  val A_subset_Vfrom = result();
     8.6  
     8.7 +val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard;
     8.8 +
     8.9  goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
    8.10  by (rtac (Vfrom RS ssubst) 1);
    8.11  by (fast_tac ZF_cs 1);
    8.12 @@ -249,7 +251,9 @@
    8.13      [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans 
    8.14  	|> standard;
    8.15  
    8.16 -val nat_into_Vfrom_Limit = standard (nat_subset_Vfrom_Limit RS subsetD);
    8.17 +goal Univ.thy "!!i. [| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
    8.18 +by (REPEAT (ares_tac [nat_subset_Vfrom_Limit RS subsetD] 1));
    8.19 +val nat_into_Vfrom_Limit = result();
    8.20  
    8.21  (** Closure under disjoint union **)
    8.22