--- 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;