new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
authorpaulson
Thu Jan 13 17:36:58 2000 +0100 (2000-01-13)
changeset 812768c6159440f1
parent 8126 6244be18fa55
child 8128 3a5864b465e2
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
from directory AC
src/ZF/Arith.ML
src/ZF/Cardinal.ML
src/ZF/CardinalArith.ML
src/ZF/Epsilon.ML
src/ZF/Nat.ML
src/ZF/OrderType.ML
src/ZF/Ordinal.ML
src/ZF/ROOT.ML
src/ZF/Univ.ML
src/ZF/ex/Limit.ML
src/ZF/ex/Limit.thy
src/ZF/func.ML
src/ZF/thy_syntax.ML
src/ZF/upair.ML
     1.1 --- a/src/ZF/Arith.ML	Thu Jan 13 17:36:02 2000 +0100
     1.2 +++ b/src/ZF/Arith.ML	Thu Jan 13 17:36:58 2000 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    Also, rec(m, 0, %z w.z) is pred(m).   
     1.5  *)
     1.6  
     1.7 -Addsimps [rec_type, nat_0_le, nat_le_refl];
     1.8 +Addsimps [rec_type, nat_0_le];
     1.9  val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
    1.10  
    1.11  Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
    1.12 @@ -348,16 +348,16 @@
    1.13  by (etac complete_induct 1);
    1.14  by (excluded_middle_tac "succ(x)<n" 1);
    1.15  (* case succ(x) < n *)
    1.16 -by (asm_simp_tac (simpset() addsimps [mod_less, nat_le_refl RS lt_trans,
    1.17 -                                     succ_neq_self]) 2);
    1.18 +by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans, 
    1.19 +				      succ_neq_self]) 2);
    1.20  by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
    1.21  (* case n le succ(x) *)
    1.22  by (asm_full_simp_tac
    1.23 -     (simpset() addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1);
    1.24 +     (simpset() addsimps [not_lt_iff_le, nat_into_Ord]) 1);
    1.25  by (etac leE 1);
    1.26 -by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ, 
    1.27 -                                     mod_geq]) 1);
    1.28 -by (asm_simp_tac (simpset() addsimps [mod_less, diff_self_eq_0]) 1);
    1.29 +(*equality case*)
    1.30 +by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
    1.31 +by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ]) 1);
    1.32  qed "mod_succ";
    1.33  
    1.34  Goal "[| 0<n;  m:nat;  n:nat |] ==> m mod n < n";
    1.35 @@ -411,7 +411,7 @@
    1.36  by (ftac lt_nat_in_nat 1);
    1.37  by (assume_tac 1);
    1.38  by (etac succ_lt_induct 1);
    1.39 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
    1.40 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_into_Ord, leI])));
    1.41  qed "add_lt_mono1";
    1.42  
    1.43  (*strict, in both arguments*)
     2.1 --- a/src/ZF/Cardinal.ML	Thu Jan 13 17:36:02 2000 +0100
     2.2 +++ b/src/ZF/Cardinal.ML	Thu Jan 13 17:36:58 2000 +0100
     2.3 @@ -142,8 +142,7 @@
     2.4  by (Blast_tac 1);
     2.5  qed "lesspoll_imp_lepoll";
     2.6  
     2.7 -Goalw [lepoll_def]
     2.8 -        "[| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
     2.9 +Goalw [lepoll_def] "[| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
    2.10  by (blast_tac (claset() addIs [well_ord_rvimage]) 1);
    2.11  qed "lepoll_well_ord";
    2.12  
    2.13 @@ -303,13 +302,16 @@
    2.14  qed "Card_is_Ord";
    2.15  
    2.16  Goal "Card(K) ==> K le |K|";
    2.17 -by (asm_simp_tac (simpset() addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);
    2.18 +by (asm_simp_tac (simpset() addsimps [Card_is_Ord, Card_cardinal_eq]) 1);
    2.19  qed "Card_cardinal_le";
    2.20  
    2.21  Goalw [cardinal_def] "Ord(|A|)";
    2.22  by (rtac Ord_Least 1);
    2.23  qed "Ord_cardinal";
    2.24  
    2.25 +Addsimps [Ord_cardinal];
    2.26 +AddSIs [Ord_cardinal];
    2.27 +
    2.28  (*The cardinals are the initial ordinals*)
    2.29  Goal "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j eqpoll K)";
    2.30  by (safe_tac (claset() addSIs [CardI, Card_is_Ord]));
    2.31 @@ -513,6 +515,16 @@
    2.32  by (asm_simp_tac (simpset() addsimps [lesspoll_def]) 1);
    2.33  qed "lepoll_succ_disj";
    2.34  
    2.35 +Goalw [lesspoll_def] "[| A lesspoll i; Ord(i) |] ==> |A| < i";
    2.36 +by (Clarify_tac 1);
    2.37 +by (forward_tac [lepoll_cardinal_le] 1);
    2.38 +by (assume_tac 1);
    2.39 +by (blast_tac (claset() addIs [well_ord_Memrel,
    2.40 +			       well_ord_cardinal_eqpoll RS eqpoll_sym]
    2.41 +                        addDs [lepoll_well_ord] 
    2.42 +                        addSEs [leE]) 1);
    2.43 +qed "lesspoll_cardinal_lt";
    2.44 +
    2.45  
    2.46  (*** The first infinite cardinal: Omega, or nat ***)
    2.47  
    2.48 @@ -778,3 +790,7 @@
    2.49  by (blast_tac (claset() addDs [ordertype_eq_n] 
    2.50                         addSIs [nat_well_ord_converse_Memrel]) 1);
    2.51  qed "Finite_well_ord_converse";
    2.52 +
    2.53 +Goalw [Finite_def] "n:nat ==> Finite(n)";
    2.54 +by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
    2.55 +qed "nat_into_Finite";
     3.1 --- a/src/ZF/CardinalArith.ML	Thu Jan 13 17:36:02 2000 +0100
     3.2 +++ b/src/ZF/CardinalArith.ML	Thu Jan 13 17:36:58 2000 +0100
     3.3 @@ -402,7 +402,7 @@
     3.4  				      Un_absorb, Un_least_mem_iff, ltD]) 1);
     3.5  by (safe_tac (claset() addSEs [mem_irrefl] 
     3.6                         addSIs [Un_upper1_le, Un_upper2_le]));
     3.7 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2, Ord_succ])));
     3.8 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2])));
     3.9  qed "csquareD";
    3.10  
    3.11  Goalw [pred_def]
    3.12 @@ -540,7 +540,7 @@
    3.13      REPEAT (ares_tac [cmult_le_self, InfCard_is_Card] 2));
    3.14  by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1);
    3.15  by (resolve_tac [cmult_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1));
    3.16 -by (asm_simp_tac (simpset() addsimps [InfCard_csquare_eq]) 1);
    3.17 +by (asm_full_simp_tac (simpset() addsimps [InfCard_csquare_eq]) 1);
    3.18  qed "InfCard_le_cmult_eq";
    3.19  
    3.20  (*Corollary 10.13 (1), for cardinal multiplication*)
    3.21 @@ -570,7 +570,7 @@
    3.22      REPEAT (ares_tac [cadd_le_self, InfCard_is_Card] 2));
    3.23  by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1);
    3.24  by (resolve_tac [cadd_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1));
    3.25 -by (asm_simp_tac (simpset() addsimps [InfCard_cdouble_eq]) 1);
    3.26 +by (asm_full_simp_tac (simpset() addsimps [InfCard_cdouble_eq]) 1);
    3.27  qed "InfCard_le_cadd_eq";
    3.28  
    3.29  Goal "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L";
    3.30 @@ -736,6 +736,14 @@
    3.31  	 		        Un_upper2 RS Fin_mono RS subsetD]) 1);
    3.32  qed "Finite_Un";
    3.33  
    3.34 +Goal "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))";
    3.35 +by (asm_full_simp_tac (simpset() addsimps [Finite_Fin_iff]) 1);
    3.36 +by (rtac Fin_UnionI 1);
    3.37 +by (etac Fin.induct 1);
    3.38 +by (Simp_tac 1);
    3.39 +by (blast_tac (claset() addIs [Fin.consI, impOfSubs Fin_mono]) 1);
    3.40 +qed "Finite_Union";
    3.41 +
    3.42  
    3.43  (** Removing elements from a finite set decreases its cardinality **)
    3.44  
    3.45 @@ -756,7 +764,7 @@
    3.46  by (blast_tac (claset() addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] 
    3.47                          addSEs [mem_irrefl]
    3.48                          addSDs [Finite_imp_well_ord]) 1);
    3.49 -by (blast_tac (claset() addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1);
    3.50 +by (blast_tac (claset() addIs [Card_cardinal, Card_is_Ord]) 1);
    3.51  by (rtac notI 1);
    3.52  by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1);
    3.53  by (assume_tac 1);
    3.54 @@ -778,8 +786,7 @@
    3.55  
    3.56  Goal "[| Finite(A);  a:A |] ==> |A-{a}| < |A|";
    3.57  by (rtac succ_leE 1);
    3.58 -by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, 
    3.59 -				      Ord_cardinal RS le_refl]) 1);
    3.60 +by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff]) 1);
    3.61  qed "Finite_imp_cardinal_Diff";
    3.62  
    3.63  
     4.1 --- a/src/ZF/Epsilon.ML	Thu Jan 13 17:36:02 2000 +0100
     4.2 +++ b/src/ZF/Epsilon.ML	Thu Jan 13 17:36:58 2000 +0100
     4.3 @@ -234,6 +234,7 @@
     4.4  by (Blast_tac 1);
     4.5  by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
     4.6  qed "rank_succ";
     4.7 +Addsimps [rank_0, rank_succ];
     4.8  
     4.9  Goal "rank(Union(A)) = (UN x:A. rank(x))";
    4.10  by (rtac equalityI 1);
    4.11 @@ -265,6 +266,23 @@
    4.12  by (rtac (consI1 RS consI2 RS rank_lt) 1);
    4.13  qed "rank_pair2";
    4.14  
    4.15 +(*Not clear how to remove the P(a) condition, since the "then" part
    4.16 +  must refer to "a"*)
    4.17 +Goal "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)";
    4.18 +by (asm_simp_tac (simpset() addsimps [the_0, the_equality2]) 1);
    4.19 +qed "the_equality_if";
    4.20 +
    4.21 +(*The premise is needed not just to fix i but to ensure f~=0*)
    4.22 +Goalw [apply_def] "i : domain(f) ==> rank(f`i) < rank(f)";
    4.23 +by (Clarify_tac 1);
    4.24 +by (subgoal_tac "rank(y) < rank(f)" 1);
    4.25 +by (blast_tac (claset() addIs [lt_trans, rank_lt, rank_pair2]) 2);
    4.26 +by (subgoal_tac "0 < rank(f)" 1);
    4.27 +by (etac (Ord_rank RS Ord_0_le RS lt_trans1) 2);
    4.28 +by (asm_simp_tac (simpset() addsimps [the_equality_if]) 1);
    4.29 +qed "rank_apply";
    4.30 +
    4.31 +
    4.32  (*** Corollaries of leastness ***)
    4.33  
    4.34  Goal "A:B ==> eclose(A)<=eclose(B)";
     5.1 --- a/src/ZF/Nat.ML	Thu Jan 13 17:36:02 2000 +0100
     5.2 +++ b/src/ZF/Nat.ML	Thu Jan 13 17:36:58 2000 +0100
     5.3 @@ -74,6 +74,8 @@
     5.4  by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
     5.5  qed "nat_into_Ord";
     5.6  
     5.7 +Addsimps [nat_into_Ord];
     5.8 +
     5.9  (* i: nat ==> 0 le i; same thing as 0<succ(i)  *)
    5.10  bind_thm ("nat_0_le", nat_into_Ord RS Ord_0_le);
    5.11  
     6.1 --- a/src/ZF/OrderType.ML	Thu Jan 13 17:36:02 2000 +0100
     6.2 +++ b/src/ZF/OrderType.ML	Thu Jan 13 17:36:58 2000 +0100
     6.3 @@ -858,8 +858,8 @@
     6.4  Goal "[| Ord(i);  0<j |] ==> i le j**i";
     6.5  by (ftac lt_Ord2 1);
     6.6  by (eres_inst_tac [("i","i")] trans_induct3 1);
     6.7 -by (asm_simp_tac (simpset() addsimps [omult_0, Ord_0 RS le_refl]) 1);
     6.8 -by (asm_simp_tac (simpset() addsimps [omult_succ, succ_le_iff]) 1);
     6.9 +by (Asm_simp_tac 1);
    6.10 +by (asm_simp_tac (simpset() addsimps [omult_succ]) 1);
    6.11  by (etac lt_trans1 1);
    6.12  by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 
    6.13      rtac oadd_lt_mono2 2);
    6.14 @@ -869,7 +869,7 @@
    6.15  by (rtac le_implies_UN_le_UN 2);
    6.16  by (Blast_tac 2);
    6.17  by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
    6.18 -                                     Limit_is_Ord RS le_refl]) 1);
    6.19 +                                     Limit_is_Ord]) 1);
    6.20  qed "omult_le_self2";
    6.21  
    6.22  
    6.23 @@ -880,7 +880,7 @@
    6.24  by (REPEAT_SOME assume_tac);
    6.25  by (ALLGOALS
    6.26      (best_tac (claset() addDs [omult_lt_mono2] 
    6.27 -                       addss (simpset() addsimps [lt_not_refl]))));
    6.28 +                        addss (simpset() addsimps [lt_not_refl]))));
    6.29  qed "omult_inject";
    6.30  
    6.31  
     7.1 --- a/src/ZF/Ordinal.ML	Thu Jan 13 17:36:02 2000 +0100
     7.2 +++ b/src/ZF/Ordinal.ML	Thu Jan 13 17:36:58 2000 +0100
     7.3 @@ -142,7 +142,7 @@
     7.4  bind_thm ("Ord_1", Ord_0 RS Ord_succ);
     7.5  
     7.6  Goal "Ord(succ(i)) <-> Ord(i)";
     7.7 -by (blast_tac (claset() addIs [Ord_succ] addDs [Ord_succD]) 1);
     7.8 +by (blast_tac (claset() addIs [Ord_succ]) 1);
     7.9  qed "Ord_succ_iff";
    7.10  
    7.11  Addsimps [Ord_0, Ord_succ_iff];
    7.12 @@ -246,7 +246,7 @@
    7.13  (** le is less than or equals;  recall  i le j  abbrevs  i<succ(j) !! **)
    7.14  
    7.15  Goalw [lt_def] "i le j <-> i<j | (i=j & Ord(j))";
    7.16 -by (blast_tac (claset() addSIs [Ord_succ] addSDs [Ord_succD]) 1);
    7.17 +by (Blast_tac 1);
    7.18  qed "le_iff";
    7.19  
    7.20  (*Equivalently, i<j ==> i < succ(j)*)
    7.21 @@ -260,6 +260,14 @@
    7.22  
    7.23  val le_refl = refl RS le_eqI;
    7.24  
    7.25 +Goal "i le i <-> Ord(i)";
    7.26 +by (asm_simp_tac (simpset() addsimps [lt_not_refl, le_iff]) 1);
    7.27 +qed "le_refl_iff";
    7.28 +
    7.29 +Addsimps [le_refl_iff];
    7.30 +AddSIs [le_refl];
    7.31 +AddSDs [le_refl_iff RS iffD1];
    7.32 +
    7.33  val [prem] = Goal "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
    7.34  by (rtac (disjCI RS (le_iff RS iffD2)) 1);
    7.35  by (etac prem 1);
    7.36 @@ -277,12 +285,11 @@
    7.37  qed "le_anti_sym";
    7.38  
    7.39  Goal "i le 0 <-> i=0";
    7.40 -by (blast_tac (claset() addSIs [Ord_0 RS le_refl] addSEs [leE]) 1);
    7.41 +by (blast_tac (claset() addSEs [leE]) 1);
    7.42  qed "le0_iff";
    7.43  
    7.44  bind_thm ("le0D", le0_iff RS iffD1);
    7.45  
    7.46 -AddIs [le_refl];
    7.47  AddSDs [le0D];
    7.48  Addsimps [le0_iff];
    7.49  
    7.50 @@ -479,13 +486,12 @@
    7.51  qed "le_imp_subset";
    7.52  
    7.53  Goal "j le i <-> j<=i & Ord(i) & Ord(j)";
    7.54 -by (blast_tac (claset() addDs [Ord_succD, subset_imp_le, le_imp_subset]
    7.55 -                       addEs [ltE]) 1);
    7.56 +by (blast_tac (claset() addDs [subset_imp_le, le_imp_subset] addEs [ltE]) 1);
    7.57  qed "le_subset_iff";
    7.58  
    7.59  Goal "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
    7.60  by (simp_tac (simpset() addsimps [le_iff]) 1);
    7.61 -by (blast_tac (claset() addIs [Ord_succ] addDs [Ord_succD]) 1);
    7.62 +by (Blast_tac 1);
    7.63  qed "le_succ_iff";
    7.64  
    7.65  (*Just a variant of subset_imp_le*)
    7.66 @@ -519,7 +525,7 @@
    7.67  Goal "succ(i) le j ==> i<j";
    7.68  by (rtac (not_le_iff_lt RS iffD1) 1);
    7.69  by (blast_tac le_cs 3);
    7.70 -by (ALLGOALS (blast_tac (claset() addEs [ltE, make_elim Ord_succD])));
    7.71 +by (ALLGOALS (blast_tac (claset() addEs [ltE])));
    7.72  qed "succ_leE";
    7.73  
    7.74  Goal "succ(i) le j <-> i<j";
    7.75 @@ -680,8 +686,7 @@
    7.76  (** Traditional 3-way case analysis on ordinals **)
    7.77  
    7.78  Goal "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)";
    7.79 -by (blast_tac (claset() addSIs [non_succ_LimitI, Ord_0_lt]
    7.80 -                      addSDs [Ord_succD]) 1);
    7.81 +by (blast_tac (claset() addSIs [non_succ_LimitI, Ord_0_lt]) 1);
    7.82  qed "Ord_cases_disj";
    7.83  
    7.84  val major::prems = Goal
     8.1 --- a/src/ZF/ROOT.ML	Thu Jan 13 17:36:02 2000 +0100
     8.2 +++ b/src/ZF/ROOT.ML	Thu Jan 13 17:36:58 2000 +0100
     8.3 @@ -44,6 +44,8 @@
     8.4  (*the all-in-one theory*)
     8.5  use_thy "Main";
     8.6  
     8.7 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     8.8 +
     8.9  print_depth 8;
    8.10  
    8.11  Goal "True";  (*leave subgoal package empty*)
     9.1 --- a/src/ZF/Univ.ML	Thu Jan 13 17:36:02 2000 +0100
     9.2 +++ b/src/ZF/Univ.ML	Thu Jan 13 17:36:58 2000 +0100
     9.3 @@ -6,8 +6,6 @@
     9.4  The cumulative hierarchy and a small universe for recursive types
     9.5  *)
     9.6  
     9.7 -open Univ;
     9.8 -
     9.9  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    9.10  Goal "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
    9.11  by (stac (Vfrom_def RS def_transrec) 1);
    9.12 @@ -445,6 +443,7 @@
    9.13  by (assume_tac 1);
    9.14  qed "VsetI";
    9.15  
    9.16 +(*Merely a lemma for the result following*)
    9.17  Goal "Ord(i) ==> b : Vset(i) <-> rank(b) < i";
    9.18  by (rtac iffI 1);
    9.19  by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
    9.20 @@ -454,6 +453,10 @@
    9.21  by (rtac (Vfrom_rank_eq RS subst) 1);
    9.22  by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
    9.23  qed "Vset_rank_iff";
    9.24 +Addsimps [Vset_rank_iff];
    9.25 +
    9.26 +(*This is rank(rank(a)) = rank(a) *)
    9.27 +Addsimps [Ord_rank RS rank_of_Ord];
    9.28  
    9.29  Goal "Ord(i) ==> rank(Vset(i)) = i";
    9.30  by (stac rank 1);
    9.31 @@ -501,8 +504,9 @@
    9.32  (*NOT SUITABLE FOR REWRITING: recursive!*)
    9.33  Goalw [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
    9.34  by (stac transrec 1);
    9.35 -by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
    9.36 -                              VsetI RS beta, le_refl]) 1);
    9.37 +by (Simp_tac 1);
    9.38 +by (rtac (refl RS lam_cong RS subst_context) 1);
    9.39 +by (Asm_full_simp_tac 1);
    9.40  qed "Vrec";
    9.41  
    9.42  (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
    9.43 @@ -517,8 +521,9 @@
    9.44  Goalw [Vrecursor_def]
    9.45       "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)";
    9.46  by (stac transrec 1);
    9.47 -by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
    9.48 -                              VsetI RS beta, le_refl]) 1);
    9.49 +by (Simp_tac 1);
    9.50 +by (rtac (refl RS lam_cong RS subst_context) 1);
    9.51 +by (Asm_full_simp_tac 1);
    9.52  qed "Vrecursor";
    9.53  
    9.54  (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
    10.1 --- a/src/ZF/ex/Limit.ML	Thu Jan 13 17:36:02 2000 +0100
    10.2 +++ b/src/ZF/ex/Limit.ML	Thu Jan 13 17:36:58 2000 +0100
    10.3 @@ -1514,7 +1514,7 @@
    10.4  (* All theorems assume variables m and n are natural numbers. *)
    10.5  
    10.6  Goal "m:nat ==> e_less(DD,ee,m,succ(m)) = ee`m O id(set(DD`m))";
    10.7 -by (asm_simp_tac(simpset() addsimps[e_less_le,e_less_eq]) 1);
    10.8 +by (asm_simp_tac(simpset() addsimps[e_less_le, e_less_eq]) 1);
    10.9  qed "e_less_succ";
   10.10  
   10.11  val prems = goal Limit.thy  (* e_less_succ_emb *)
    11.1 --- a/src/ZF/ex/Limit.thy	Thu Jan 13 17:36:02 2000 +0100
    11.2 +++ b/src/ZF/ex/Limit.thy	Thu Jan 13 17:36:58 2000 +0100
    11.3 @@ -17,7 +17,7 @@
    11.4      Laboratory, 1995.
    11.5  *)
    11.6  
    11.7 -Limit  =  Perm + Arith +
    11.8 +Limit  =  Main +
    11.9  
   11.10  consts
   11.11  
    12.1 --- a/src/ZF/func.ML	Thu Jan 13 17:36:02 2000 +0100
    12.2 +++ b/src/ZF/func.ML	Thu Jan 13 17:36:58 2000 +0100
    12.3 @@ -124,6 +124,12 @@
    12.4  by (blast_tac (claset() addIs prems addSDs [pi_prem RS Pi_memberD]) 1);
    12.5  qed "Pi_type";
    12.6  
    12.7 +(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
    12.8 +Goal "(f : Pi(A, %x. {y:B(x). P(x,y)})) \
    12.9 +\     <->  f : Pi(A,B) & (ALL x: A. P(x, f`x))";
   12.10 +by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1);
   12.11 +qed "Pi_Collect_iff";
   12.12 +
   12.13  
   12.14  (** Elimination of membership in a function **)
   12.15  
    13.1 --- a/src/ZF/thy_syntax.ML	Thu Jan 13 17:36:02 2000 +0100
    13.2 +++ b/src/ZF/thy_syntax.ML	Thu Jan 13 17:36:58 2000 +0100
    13.3 @@ -124,7 +124,7 @@
    13.4      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
    13.5      val construct = name -- string_list -- opt_mixfix;
    13.6    in optional ("<=" $$-- string) "\"\"" --
    13.7 -     enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
    13.8 +     enum1 "and" (name --$$ "=" -- enum1 "|" construct) --
    13.9       optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
   13.10       >> mk_params
   13.11  end;
    14.1 --- a/src/ZF/upair.ML	Thu Jan 13 17:36:02 2000 +0100
    14.2 +++ b/src/ZF/upair.ML	Thu Jan 13 17:36:58 2000 +0100
    14.3 @@ -203,24 +203,23 @@
    14.4  AddIs [the_equality];
    14.5  
    14.6  (* Only use this if you already know EX!x. P(x) *)
    14.7 -qed_goal "the_equality2" thy
    14.8 -    "!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
    14.9 - (fn _ => [ (Blast_tac 1) ]);
   14.10 +Goal "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a";
   14.11 +by (Blast_tac 1);
   14.12 +qed "the_equality2";
   14.13  
   14.14 -qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
   14.15 - (fn [major]=>
   14.16 -  [ (rtac (major RS ex1E) 1),
   14.17 -    (resolve_tac [major RS the_equality2 RS ssubst] 1),
   14.18 -    (REPEAT (assume_tac 1)) ]);
   14.19 +Goal "EX! x. P(x) ==> P(THE x. P(x))";
   14.20 +by (etac ex1E 1);
   14.21 +by (rtac (the_equality RS ssubst) 1);
   14.22 +by (REPEAT (Blast_tac 1));
   14.23 +qed "theI";
   14.24  
   14.25  (*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
   14.26    (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
   14.27  
   14.28  (*If it's "undefined", it's zero!*)
   14.29 -qed_goalw "the_0" thy [the_def]
   14.30 -    "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
   14.31 - (fn _ => [ (blast_tac (claset() addSEs [ReplaceE]) 1) ]);
   14.32 -
   14.33 +Goalw  [the_def] "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0";
   14.34 +by (blast_tac (claset() addSEs [ReplaceE]) 1);
   14.35 +qed "the_0";
   14.36  
   14.37  (*Easier to apply than theI: conclusion has only one occurrence of P*)
   14.38  val prems =