new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
from directory AC

--- a/src/ZF/Arith.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/Arith.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -14,7 +14,7 @@
   Also, rec(m, 0, %z w.z) is pred(m).   
 *)
 
-Addsimps [rec_type, nat_0_le, nat_le_refl];
+Addsimps [rec_type, nat_0_le];
 val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
 
 Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
@@ -348,16 +348,16 @@
 by (etac complete_induct 1);
 by (excluded_middle_tac "succ(x)<n" 1);
 (* case succ(x) < n *)
-by (asm_simp_tac (simpset() addsimps [mod_less, nat_le_refl RS lt_trans,
-                                     succ_neq_self]) 2);
+by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans, 
+				      succ_neq_self]) 2);
 by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
 (* case n le succ(x) *)
 by (asm_full_simp_tac
-     (simpset() addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1);
+     (simpset() addsimps [not_lt_iff_le, nat_into_Ord]) 1);
 by (etac leE 1);
-by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ, 
-                                     mod_geq]) 1);
-by (asm_simp_tac (simpset() addsimps [mod_less, diff_self_eq_0]) 1);
+(*equality case*)
+by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
+by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ]) 1);
 qed "mod_succ";
 
 Goal "[| 0<n;  m:nat;  n:nat |] ==> m mod n < n";
@@ -411,7 +411,7 @@
 by (ftac lt_nat_in_nat 1);
 by (assume_tac 1);
 by (etac succ_lt_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_into_Ord, leI])));
 qed "add_lt_mono1";
 
 (*strict, in both arguments*)

--- a/src/ZF/Cardinal.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/Cardinal.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -142,8 +142,7 @@
 by (Blast_tac 1);
 qed "lesspoll_imp_lepoll";
 
-Goalw [lepoll_def]
-        "[| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
+Goalw [lepoll_def] "[| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
 by (blast_tac (claset() addIs [well_ord_rvimage]) 1);
 qed "lepoll_well_ord";
 
@@ -303,13 +302,16 @@
 qed "Card_is_Ord";
 
 Goal "Card(K) ==> K le |K|";
-by (asm_simp_tac (simpset() addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [Card_is_Ord, Card_cardinal_eq]) 1);
 qed "Card_cardinal_le";
 
 Goalw [cardinal_def] "Ord(|A|)";
 by (rtac Ord_Least 1);
 qed "Ord_cardinal";
 
+Addsimps [Ord_cardinal];
+AddSIs [Ord_cardinal];
+
 (*The cardinals are the initial ordinals*)
 Goal "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j eqpoll K)";
 by (safe_tac (claset() addSIs [CardI, Card_is_Ord]));
@@ -513,6 +515,16 @@
 by (asm_simp_tac (simpset() addsimps [lesspoll_def]) 1);
 qed "lepoll_succ_disj";
 
+Goalw [lesspoll_def] "[| A lesspoll i; Ord(i) |] ==> |A| < i";
+by (Clarify_tac 1);
+by (forward_tac [lepoll_cardinal_le] 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [well_ord_Memrel,
+			       well_ord_cardinal_eqpoll RS eqpoll_sym]
+                        addDs [lepoll_well_ord] 
+                        addSEs [leE]) 1);
+qed "lesspoll_cardinal_lt";
+
 
 (*** The first infinite cardinal: Omega, or nat ***)
 
@@ -778,3 +790,7 @@
 by (blast_tac (claset() addDs [ordertype_eq_n] 
                        addSIs [nat_well_ord_converse_Memrel]) 1);
 qed "Finite_well_ord_converse";
+
+Goalw [Finite_def] "n:nat ==> Finite(n)";
+by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
+qed "nat_into_Finite";

--- a/src/ZF/CardinalArith.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/CardinalArith.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -402,7 +402,7 @@
 				      Un_absorb, Un_least_mem_iff, ltD]) 1);
 by (safe_tac (claset() addSEs [mem_irrefl] 
                        addSIs [Un_upper1_le, Un_upper2_le]));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2, Ord_succ])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2])));
 qed "csquareD";
 
 Goalw [pred_def]
@@ -540,7 +540,7 @@
     REPEAT (ares_tac [cmult_le_self, InfCard_is_Card] 2));
 by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1);
 by (resolve_tac [cmult_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1));
-by (asm_simp_tac (simpset() addsimps [InfCard_csquare_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [InfCard_csquare_eq]) 1);
 qed "InfCard_le_cmult_eq";
 
 (*Corollary 10.13 (1), for cardinal multiplication*)
@@ -570,7 +570,7 @@
     REPEAT (ares_tac [cadd_le_self, InfCard_is_Card] 2));
 by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1);
 by (resolve_tac [cadd_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1));
-by (asm_simp_tac (simpset() addsimps [InfCard_cdouble_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [InfCard_cdouble_eq]) 1);
 qed "InfCard_le_cadd_eq";
 
 Goal "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L";
@@ -736,6 +736,14 @@
 	 		        Un_upper2 RS Fin_mono RS subsetD]) 1);
 qed "Finite_Un";
 
+Goal "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))";
+by (asm_full_simp_tac (simpset() addsimps [Finite_Fin_iff]) 1);
+by (rtac Fin_UnionI 1);
+by (etac Fin.induct 1);
+by (Simp_tac 1);
+by (blast_tac (claset() addIs [Fin.consI, impOfSubs Fin_mono]) 1);
+qed "Finite_Union";
+
 
 (** Removing elements from a finite set decreases its cardinality **)
 
@@ -756,7 +764,7 @@
 by (blast_tac (claset() addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] 
                         addSEs [mem_irrefl]
                         addSDs [Finite_imp_well_ord]) 1);
-by (blast_tac (claset() addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1);
+by (blast_tac (claset() addIs [Card_cardinal, Card_is_Ord]) 1);
 by (rtac notI 1);
 by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1);
 by (assume_tac 1);
@@ -778,8 +786,7 @@
 
 Goal "[| Finite(A);  a:A |] ==> |A-{a}| < |A|";
 by (rtac succ_leE 1);
-by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, 
-				      Ord_cardinal RS le_refl]) 1);
+by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff]) 1);
 qed "Finite_imp_cardinal_Diff";
 
 

--- a/src/ZF/Epsilon.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/Epsilon.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -234,6 +234,7 @@
 by (Blast_tac 1);
 by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
 qed "rank_succ";
+Addsimps [rank_0, rank_succ];
 
 Goal "rank(Union(A)) = (UN x:A. rank(x))";
 by (rtac equalityI 1);
@@ -265,6 +266,23 @@
 by (rtac (consI1 RS consI2 RS rank_lt) 1);
 qed "rank_pair2";
 
+(*Not clear how to remove the P(a) condition, since the "then" part
+  must refer to "a"*)
+Goal "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)";
+by (asm_simp_tac (simpset() addsimps [the_0, the_equality2]) 1);
+qed "the_equality_if";
+
+(*The premise is needed not just to fix i but to ensure f~=0*)
+Goalw [apply_def] "i : domain(f) ==> rank(f`i) < rank(f)";
+by (Clarify_tac 1);
+by (subgoal_tac "rank(y) < rank(f)" 1);
+by (blast_tac (claset() addIs [lt_trans, rank_lt, rank_pair2]) 2);
+by (subgoal_tac "0 < rank(f)" 1);
+by (etac (Ord_rank RS Ord_0_le RS lt_trans1) 2);
+by (asm_simp_tac (simpset() addsimps [the_equality_if]) 1);
+qed "rank_apply";
+
+
 (*** Corollaries of leastness ***)
 
 Goal "A:B ==> eclose(A)<=eclose(B)";

--- a/src/ZF/Nat.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/Nat.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -74,6 +74,8 @@
 by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
 qed "nat_into_Ord";
 
+Addsimps [nat_into_Ord];
+
 (* i: nat ==> 0 le i; same thing as 0<succ(i)  *)
 bind_thm ("nat_0_le", nat_into_Ord RS Ord_0_le);
 

--- a/src/ZF/OrderType.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/OrderType.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -858,8 +858,8 @@
 Goal "[| Ord(i);  0<j |] ==> i le j**i";
 by (ftac lt_Ord2 1);
 by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (asm_simp_tac (simpset() addsimps [omult_0, Ord_0 RS le_refl]) 1);
-by (asm_simp_tac (simpset() addsimps [omult_succ, succ_le_iff]) 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [omult_succ]) 1);
 by (etac lt_trans1 1);
 by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 
     rtac oadd_lt_mono2 2);
@@ -869,7 +869,7 @@
 by (rtac le_implies_UN_le_UN 2);
 by (Blast_tac 2);
 by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
-                                     Limit_is_Ord RS le_refl]) 1);
+                                     Limit_is_Ord]) 1);
 qed "omult_le_self2";
 
 
@@ -880,7 +880,7 @@
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS
     (best_tac (claset() addDs [omult_lt_mono2] 
-                       addss (simpset() addsimps [lt_not_refl]))));
+                        addss (simpset() addsimps [lt_not_refl]))));
 qed "omult_inject";
 
 

--- a/src/ZF/Ordinal.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/Ordinal.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -142,7 +142,7 @@
 bind_thm ("Ord_1", Ord_0 RS Ord_succ);
 
 Goal "Ord(succ(i)) <-> Ord(i)";
-by (blast_tac (claset() addIs [Ord_succ] addDs [Ord_succD]) 1);
+by (blast_tac (claset() addIs [Ord_succ]) 1);
 qed "Ord_succ_iff";
 
 Addsimps [Ord_0, Ord_succ_iff];
@@ -246,7 +246,7 @@
 (** le is less than or equals;  recall  i le j  abbrevs  i<succ(j) !! **)
 
 Goalw [lt_def] "i le j <-> i<j | (i=j & Ord(j))";
-by (blast_tac (claset() addSIs [Ord_succ] addSDs [Ord_succD]) 1);
+by (Blast_tac 1);
 qed "le_iff";
 
 (*Equivalently, i<j ==> i < succ(j)*)
@@ -260,6 +260,14 @@
 
 val le_refl = refl RS le_eqI;
 
+Goal "i le i <-> Ord(i)";
+by (asm_simp_tac (simpset() addsimps [lt_not_refl, le_iff]) 1);
+qed "le_refl_iff";
+
+Addsimps [le_refl_iff];
+AddSIs [le_refl];
+AddSDs [le_refl_iff RS iffD1];
+
 val [prem] = Goal "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
 by (rtac (disjCI RS (le_iff RS iffD2)) 1);
 by (etac prem 1);
@@ -277,12 +285,11 @@
 qed "le_anti_sym";
 
 Goal "i le 0 <-> i=0";
-by (blast_tac (claset() addSIs [Ord_0 RS le_refl] addSEs [leE]) 1);
+by (blast_tac (claset() addSEs [leE]) 1);
 qed "le0_iff";
 
 bind_thm ("le0D", le0_iff RS iffD1);
 
-AddIs [le_refl];
 AddSDs [le0D];
 Addsimps [le0_iff];
 
@@ -479,13 +486,12 @@
 qed "le_imp_subset";
 
 Goal "j le i <-> j<=i & Ord(i) & Ord(j)";
-by (blast_tac (claset() addDs [Ord_succD, subset_imp_le, le_imp_subset]
-                       addEs [ltE]) 1);
+by (blast_tac (claset() addDs [subset_imp_le, le_imp_subset] addEs [ltE]) 1);
 qed "le_subset_iff";
 
 Goal "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
 by (simp_tac (simpset() addsimps [le_iff]) 1);
-by (blast_tac (claset() addIs [Ord_succ] addDs [Ord_succD]) 1);
+by (Blast_tac 1);
 qed "le_succ_iff";
 
 (*Just a variant of subset_imp_le*)
@@ -519,7 +525,7 @@
 Goal "succ(i) le j ==> i<j";
 by (rtac (not_le_iff_lt RS iffD1) 1);
 by (blast_tac le_cs 3);
-by (ALLGOALS (blast_tac (claset() addEs [ltE, make_elim Ord_succD])));
+by (ALLGOALS (blast_tac (claset() addEs [ltE])));
 qed "succ_leE";
 
 Goal "succ(i) le j <-> i<j";
@@ -680,8 +686,7 @@
 (** Traditional 3-way case analysis on ordinals **)
 
 Goal "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)";
-by (blast_tac (claset() addSIs [non_succ_LimitI, Ord_0_lt]
-                      addSDs [Ord_succD]) 1);
+by (blast_tac (claset() addSIs [non_succ_LimitI, Ord_0_lt]) 1);
 qed "Ord_cases_disj";
 
 val major::prems = Goal

--- a/src/ZF/ROOT.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/ROOT.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -44,6 +44,8 @@
 (*the all-in-one theory*)
 use_thy "Main";
 
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
+
 print_depth 8;
 
 Goal "True";  (*leave subgoal package empty*)

--- a/src/ZF/Univ.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/Univ.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -6,8 +6,6 @@
 The cumulative hierarchy and a small universe for recursive types
 *)
 
-open Univ;
-
 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
 Goal "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
 by (stac (Vfrom_def RS def_transrec) 1);
@@ -445,6 +443,7 @@
 by (assume_tac 1);
 qed "VsetI";
 
+(*Merely a lemma for the result following*)
 Goal "Ord(i) ==> b : Vset(i) <-> rank(b) < i";
 by (rtac iffI 1);
 by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
@@ -454,6 +453,10 @@
 by (rtac (Vfrom_rank_eq RS subst) 1);
 by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
 qed "Vset_rank_iff";
+Addsimps [Vset_rank_iff];
+
+(*This is rank(rank(a)) = rank(a) *)
+Addsimps [Ord_rank RS rank_of_Ord];
 
 Goal "Ord(i) ==> rank(Vset(i)) = i";
 by (stac rank 1);
@@ -501,8 +504,9 @@
 (*NOT SUITABLE FOR REWRITING: recursive!*)
 Goalw [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
 by (stac transrec 1);
-by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
-                              VsetI RS beta, le_refl]) 1);
+by (Simp_tac 1);
+by (rtac (refl RS lam_cong RS subst_context) 1);
+by (Asm_full_simp_tac 1);
 qed "Vrec";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
@@ -517,8 +521,9 @@
 Goalw [Vrecursor_def]
      "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)";
 by (stac transrec 1);
-by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
-                              VsetI RS beta, le_refl]) 1);
+by (Simp_tac 1);
+by (rtac (refl RS lam_cong RS subst_context) 1);
+by (Asm_full_simp_tac 1);
 qed "Vrecursor";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)

--- a/src/ZF/ex/Limit.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/ex/Limit.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -1514,7 +1514,7 @@
 (* All theorems assume variables m and n are natural numbers. *)
 
 Goal "m:nat ==> e_less(DD,ee,m,succ(m)) = ee`m O id(set(DD`m))";
-by (asm_simp_tac(simpset() addsimps[e_less_le,e_less_eq]) 1);
+by (asm_simp_tac(simpset() addsimps[e_less_le, e_less_eq]) 1);
 qed "e_less_succ";
 
 val prems = goal Limit.thy  (* e_less_succ_emb *)

--- a/src/ZF/ex/Limit.thy	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/ex/Limit.thy	Thu Jan 13 17:36:58 2000 +0100
@@ -17,7 +17,7 @@
     Laboratory, 1995.
 *)
 
-Limit  =  Perm + Arith +
+Limit  =  Main +
 
 consts
 

--- a/src/ZF/func.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/func.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -124,6 +124,12 @@
 by (blast_tac (claset() addIs prems addSDs [pi_prem RS Pi_memberD]) 1);
 qed "Pi_type";
 
+(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
+Goal "(f : Pi(A, %x. {y:B(x). P(x,y)})) \
+\     <->  f : Pi(A,B) & (ALL x: A. P(x, f`x))";
+by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1);
+qed "Pi_Collect_iff";
+
 
 (** Elimination of membership in a function **)
 

--- a/src/ZF/thy_syntax.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/thy_syntax.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -124,7 +124,7 @@
     val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
     val construct = name -- string_list -- opt_mixfix;
   in optional ("<=" $$-- string) "\"\"" --
-     enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
+     enum1 "and" (name --$$ "=" -- enum1 "|" construct) --
      optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
      >> mk_params
 end;

--- a/src/ZF/upair.ML	Thu Jan 13 17:36:02 2000 +0100
+++ b/src/ZF/upair.ML	Thu Jan 13 17:36:58 2000 +0100
@@ -203,24 +203,23 @@
 AddIs [the_equality];
 
 (* Only use this if you already know EX!x. P(x) *)
-qed_goal "the_equality2" thy
-    "!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a";
+by (Blast_tac 1);
+qed "the_equality2";
 
-qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
- (fn [major]=>
-  [ (rtac (major RS ex1E) 1),
-    (resolve_tac [major RS the_equality2 RS ssubst] 1),
-    (REPEAT (assume_tac 1)) ]);
+Goal "EX! x. P(x) ==> P(THE x. P(x))";
+by (etac ex1E 1);
+by (rtac (the_equality RS ssubst) 1);
+by (REPEAT (Blast_tac 1));
+qed "theI";
 
 (*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
   (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
 
 (*If it's "undefined", it's zero!*)
-qed_goalw "the_0" thy [the_def]
-    "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
- (fn _ => [ (blast_tac (claset() addSEs [ReplaceE]) 1) ]);
-
+Goalw  [the_def] "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0";
+by (blast_tac (claset() addSEs [ReplaceE]) 1);
+qed "the_0";
 
 (*Easier to apply than theI: conclusion has only one occurrence of P*)
 val prems =