for infinite datatypes with arbitrary index sets

--- a/src/ZF/CardinalArith.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/CardinalArith.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -619,6 +619,11 @@
 
 val lt_csucc = csucc_basic RS conjunct2 |> standard;
 
+goal CardinalArith.thy "!!K. Ord(K) ==> 0 < csucc(K)";
+by (resolve_tac [[Ord_0_le, lt_csucc] MRS lt_trans1] 1);
+by (REPEAT (assume_tac 1));
+val Ord_0_lt_csucc = result();
+
 goalw CardinalArith.thy [csucc_def]
     "!!K L. [| Card(L);  K<L |] ==> csucc(K) le L";
 by (rtac Least_le 1);
@@ -650,3 +655,5 @@
 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();
+
+val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard;

--- a/src/ZF/Cardinal_AC.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/Cardinal_AC.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -4,6 +4,8 @@
     Copyright   1994  University of Cambridge
 
 Cardinal arithmetic WITH the Axiom of Choice
+
+These results help justify infinite-branching datatypes
 *)
 
 open Cardinal_AC;
@@ -135,15 +137,34 @@
 by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
 val cardinal_UN_Ord_lt_csucc = result();
 
+
+(*Saves checking Ord(j) below*)
+goal Ordinal.thy "!!i j. [| i <= j;  j<k;  Ord(i) |] ==> i<k";
+by (resolve_tac [subset_imp_le RS lt_trans1] 1);
+by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
+val lt_subset_trans = result();
+
 goal Cardinal_AC.thy
-    "!!K. [| InfCard(K);  |I| le K;  ALL i:I. j(i) < csucc(K) |] ==> \
-\         (UN i:I. j(i)) < csucc(K)";
+    "!!K. [| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |] ==> \
+\         (UN w:W. j(w)) < csucc(K)";
+by (excluded_middle_tac "W=0" 1);
+by (asm_simp_tac
+    (ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, 
+		     Card_is_Ord, Ord_0_lt_csucc]) 2);
 by (asm_full_simp_tac
     (ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
-by (eresolve_tac [exE] 1);
-by (resolve_tac [lt_trans1] 1);
-by (resolve_tac [cardinal_UN_Ord_lt_csucc] 2);
+by (safe_tac eq_cs);
+by (eresolve_tac [notE] 1);
+by (res_inst_tac [("j1", "%i. j(if(i: range(f), converse(f)`i, x))")]
+    (cardinal_UN_Ord_lt_csucc RSN (2,lt_subset_trans)) 1);
 by (assume_tac 2);
+by (resolve_tac [UN_least] 1);
+by (res_inst_tac [("x1", "f`xa")] (UN_upper RSN (2,subset_trans)) 1);
+by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
+by (asm_simp_tac 
+    (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse]) 1);
+by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2);
+by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type]
+		        setloop split_tac [expand_if]) 1);
+val le_UN_Ord_lt_csucc = result();
 
-val ?cardinal_UN_Ord_lt_csucc = result();
-

--- a/src/ZF/InfDatatype.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/InfDatatype.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -70,72 +70,89 @@
 	|> standard;
 
 goal InfDatatype.thy
-    "!!K. [| f: I -> Vfrom(A,csucc(K));  |I| le K;  InfCard(K)	\
-\         |] ==> EX j. f: I -> Vfrom(A,j) & j < csucc(K)";
-by (res_inst_tac [("x", "UN x:I. LEAST i. f`x : Vfrom(A,i)")] exI 1);
+    "!!K. [| f: W -> Vfrom(A,csucc(K));  |W| le K;  InfCard(K)	\
+\         |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)";
+by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : 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 (resolve_tac [le_UN_Ord_lt_csucc] 2);
+by (rtac ballI 4  THEN
+    eresolve_tac [fun_Limit_VfromE] 4 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 (rename_tac "w" 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 (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : 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_Vcsucc_lemma = result();
 
 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_Vcsucc_lemma = result();
+    "!!K. [| W <= Vfrom(A,csucc(K));  |W| le K;  InfCard(K)	\
+\         |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)";
+by (asm_full_simp_tac (ZF_ss addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1);
+val subset_Vcsucc = result();
 
+(*Version for arbitrary index sets*)
 goal InfDatatype.thy
-    "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
-by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma]));
+    "!!K. [| |W| le K;  W <= Vfrom(A,csucc(K));  InfCard(K) |] ==> \
+\         W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
+by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
 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 (res_inst_tac [("a1", "succ(succ(j Un ja))")] (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 (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 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_Vcsucc = result();
 
 goal InfDatatype.thy
+    "!!K. [| f: W -> Vfrom(A, csucc(K));  |W| le K;  InfCard(K);	\
+\            W <= Vfrom(A,csucc(K)) 					\
+\         |] ==> f: Vfrom(A,csucc(K))";
+by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
+val fun_in_Vcsucc = result();
+
+goal InfDatatype.thy
+    "!!K. [| W <= Vfrom(A,csucc(K));  B <= Vfrom(A,csucc(K));	\
+\            |W| le K;  InfCard(K)				\
+\         |] ==> W -> B <= Vfrom(A, csucc(K))";
+by (REPEAT (ares_tac [[Pi_mono, fun_Vcsucc] MRS subset_trans] 1));
+val fun_subset_Vcsucc = result();
+
+goal InfDatatype.thy
+    "!!f. [| f: W -> B;  W <= Vfrom(A,csucc(K));  B <= Vfrom(A,csucc(K)); \
+\            |W| le K;  InfCard(K) 					  \
+\         |] ==> f: Vfrom(A,csucc(K))";
+by (DEPTH_SOLVE (ares_tac [fun_subset_Vcsucc RS subsetD] 1));
+val fun_into_Vcsucc = result();
+
+(*Version where K itself is the index set*)
+goal InfDatatype.thy
+    "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
+by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
+by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le,
+		      i_subset_Vfrom,
+		      lt_csucc RS leI RS le_imp_subset RS subset_trans] 1));
+val Card_fun_Vcsucc = result();
+
+goal InfDatatype.thy
     "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
 \         |] ==> f: Vfrom(A,csucc(K))";
-by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
-val fun_in_Vcsucc = result();
+by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
+val Card_fun_in_Vcsucc = result();
 
-val fun_subset_Vcsucc = 
-	[Pi_mono, fun_Vcsucc] MRS subset_trans |> standard;
+val Card_fun_subset_Vcsucc = 
+	[Pi_mono, Card_fun_Vcsucc] 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_Vcsucc RS subsetD] 1));
-val fun_into_Vcsucc = result();
-
-val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard;
+by (REPEAT (ares_tac [Card_fun_subset_Vcsucc RS subsetD] 1));
+val Card_fun_into_Vcsucc = result();
 
 val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
 val Inl_in_Vcsucc  = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
@@ -145,7 +162,7 @@
 
 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
 val inf_datatype_intrs =  
-    [fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc, 
+    [Card_fun_in_Vcsucc, fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc, 
      Inl_in_Vcsucc, Inr_in_Vcsucc, 
      zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc] @ datatype_intrs;
 

--- a/src/ZF/Perm.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/Perm.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -135,6 +135,14 @@
 by (fast_tac (ZF_cs addIs [id_inj,id_surj]) 1);
 val id_bij = result();
 
+goalw Perm.thy [id_def] "A <= B <-> id(A) : A->B";
+by (safe_tac ZF_cs);
+by (fast_tac (ZF_cs addSIs [lam_type]) 1);
+by (dtac apply_type 1);
+by (assume_tac 1);
+by (asm_full_simp_tac ZF_ss 1);
+val subset_iff_id = result();
+
 
 (*** Converse of a function ***)
 

--- a/src/ZF/equalities.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/equalities.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -200,6 +200,10 @@
 by (fast_tac eq_cs 1);
 val Inter_eq_INT = result();
 
+goal ZF.thy "(UN i:0. A(i)) = 0";
+by (fast_tac eq_cs 1);
+val UN_0 = result();
+
 (*Halmos, Naive Set Theory, page 35.*)
 goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
 by (fast_tac eq_cs 1);

--- a/src/ZF/func.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/func.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -71,6 +71,13 @@
 by (REPEAT (assume_tac 1));
 val apply_equality = result();
 
+(*Applying a function outside its domain yields 0*)
+goalw ZF.thy [apply_def]
+    "!!a b f. [| a ~: domain(f);  f: Pi(A,B) |] ==> f`a = 0";
+by (rtac the_0 1);
+by (fast_tac ZF_cs 1);
+val apply_0 = result();
+
 val prems = goal ZF.thy
     "[| f: Pi(A,B);   c: f;   !!x. [| x:A;  c = <x,f`x> |] ==> P  \
 \    |] ==> P";
@@ -338,9 +345,14 @@
 by (fast_tac ZF_cs 1);
 val domain_of_fun = result();
 
+goal ZF.thy "!!f. [| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
+by (etac (apply_Pair RS rangeI) 1);
+by (assume_tac 1);
+val apply_rangeI = result();
+
 val [major] = goal ZF.thy "f : Pi(A,B) ==> f : A->range(f)";
 by (rtac (major RS Pi_type) 1);
-by (etac (major RS apply_Pair RS rangeI) 1);
+by (etac (major RS apply_rangeI) 1);
 val range_of_fun = result();
 
 (*** Extensions of functions ***)