# HG changeset patch
# User paulson
# Date 916225029 -3600
# Node ID 5e4871c5136b52978116788c6f279f71dcbc0a18
# Parent  5347c9a228973bfd161726c9a4f273dce7f38847
datatype package improvements

diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -328,11 +328,10 @@
 by (res_inst_tac 
      [("f3", "lam b:y-a. THE c. c: s(u) & a <= c & b:c")]
      (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
-by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (rtac CollectI 1);
+by (simp_tac (simpset() addsimps [inj_def]) 1);
+by (rtac conjI 1);
 by (rtac lam_type 1);
-by (forward_tac [ex1_superset_a RS theI] 1
-        THEN REPEAT (Fast_tac 1));
+by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (Fast_tac 1));
 by (Asm_simp_tac 1);
 by (Clarify_tac 1);
 by (rtac cons_eqE 1);
@@ -387,17 +386,16 @@
 \     ==> {v:s(u). a <= v} lepoll {v:Pow(x). v eqpoll m}";
 by (res_inst_tac [("f3","lam w:{v:s(u). a <= v}. w Int (x - {u})")] 
         (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
-by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (rtac CollectI 1);
+by (simp_tac (simpset() addsimps [inj_def]) 1);
+by (rtac conjI 1);
 by (rtac lam_type 1);
 by (rtac CollectI 1);
 by (Fast_tac 1);
 by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1));
-by (simp_tac (simpset() delsimps ball_simps) 1);
 by (REPEAT (resolve_tac [ballI, impI] 1));
-(** LEVEL 9 **)
-by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1
-        THEN REPEAT (assume_tac 1));
+(** LEVEL 8 **)
+by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1);
+by (EVERY (map Blast_tac [4,3,2,1]));
 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
 by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1));
 by (etac ex1_two_eq 1);
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/AC/WO1_AC.ML
--- a/src/ZF/AC/WO1_AC.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/AC/WO1_AC.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -56,9 +56,9 @@
 by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 2);
 by (resolve_tac [eqpoll_sym RS eqpoll_trans] 1);
 by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 1);
-by (resolve_tac [cadd_def RS def_imp_eq RS subst] 1);
+by (fold_tac [cadd_def]);
 by (resolve_tac [Card_cardinal RSN (2, Inf_Card_is_InfCard) RS 
-                        InfCard_cdouble_eq RS ssubst] 1);
+		 InfCard_cdouble_eq RS ssubst] 1);
 by (rtac eqpoll_refl 2);
 by (rtac notI 1);
 by (etac notE 1);
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Cardinal.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -8,8 +8,6 @@
 This theory does NOT assume the Axiom of Choice
 *)
 
-open Cardinal;
-
 (*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
 
 (** Lemma: Banach's Decomposition Theorem **)
@@ -457,11 +455,9 @@
 by (rtac ballI 1);
 by (eres_inst_tac [("n","n")] natE 1);
 by (asm_simp_tac (simpset() addsimps [lepoll_def, inj_def, 
-                                  succI1 RS Pi_empty2]) 1);
+				      succI1 RS Pi_empty2]) 1);
 by (blast_tac (claset() addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
-qed "nat_lepoll_imp_le_lemma";
-
-bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
+qed_spec_mp "nat_lepoll_imp_le";
 
 Goal "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
 by (rtac iffI 1);
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Coind/Language.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -18,11 +18,12 @@
 consts
   Exp   :: i                    (* Datatype of expressions *)
   ExVar :: i                    (* Abstract type of variables *)
-datatype <= "univ(Const Un ExVar)"
-  "Exp" = e_const("c:Const")
-        | e_var("x:ExVar")
-        | e_fn("x:ExVar","e:Exp")
-        | e_fix("x1:ExVar","x2:ExVar","e:Exp")
-        | e_app("e1:Exp","e2:Exp")
+
+datatype
+  "Exp" = e_const ("c:Const")
+        | e_var ("x:ExVar")
+        | e_fn ("x:ExVar","e:Exp")
+        | e_fix ("x1:ExVar","x2:ExVar","e:Exp")
+        | e_app ("e1:Exp","e2:Exp")
 
 end
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Coind/Types.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -9,18 +9,20 @@
 consts
   Ty :: i                       (* Datatype of types *)
   TyConst :: i          (* Abstract type of type constants *)
-datatype <= "univ(TyConst)"
-  "Ty" = t_const("tc:TyConst")
-       | t_fun("t1:Ty","t2:Ty")
+
+datatype
+  "Ty" = t_const ("tc:TyConst")
+       | t_fun ("t1:Ty","t2:Ty")
   
 
 (* Definition of type environments and associated operators *)
 
 consts
   TyEnv :: i
-datatype <= "univ(Ty Un ExVar)"
+
+datatype
   "TyEnv" = te_emp
-          | te_owr("te:TyEnv","x:ExVar","t:Ty") 
+          | te_owr ("te:TyEnv","x:ExVar","t:Ty") 
 
 consts
   te_dom :: i => i
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Coind/Values.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -10,11 +10,12 @@
 
 consts
   Val, ValEnv, Val_ValEnv  :: i
-codatatype <= "quniv(Const Un ExVar Un Exp)"
-    "Val" = v_const("c:Const")
-          | v_clos("x:ExVar","e:Exp","ve:ValEnv")
+
+codatatype
+    "Val" = v_const ("c:Const")
+          | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
   and
-    "ValEnv" = ve_mk("m:PMap(ExVar,Val)")
+    "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
   monos      "[map_mono]"
   type_intrs "[A_into_univ, mapQU]"
 
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Datatype.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -15,8 +15,9 @@
        Pair_in_univ, Inl_in_univ, Inr_in_univ, 
        zero_in_univ, A_into_univ, nat_into_univ, UnCI];
 
-  (*Needed for mutual recursion*)
-  val elims = [make_elim InlD, make_elim InrD];
+
+  val elims = [make_elim InlD, make_elim InrD,   (*for mutual recursion*)
+	       SigmaE, sumE];			 (*allows * and + in spec*)
   end;
 
 
@@ -36,7 +37,8 @@
        QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
        zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
-  val elims = [make_elim QInlD, make_elim QInrD];
+  val elims = [make_elim QInlD, make_elim QInrD,   (*for mutual recursion*)
+	       QSigmaE, qsumE];			   (*allows * and + in spec*)
   end;
 
 structure CoData_Package = 
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/IMP/Com.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -78,7 +78,7 @@
 (** Commands **)
 consts  com :: i
 
-datatype <= "univ(loc Un aexp Un bexp)"
+datatype 
   "com" = skip
         | asgt  ("x:loc", "a:aexp")             (infixl 60)
         | semic ("c0:com", "c1:com")            ("_; _"  [60, 60] 10)
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Integ/Bin.ML
--- a/src/ZF/Integ/Bin.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Integ/Bin.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -77,7 +77,7 @@
 by (rename_tac "w'" 3);
 by (induct_tac "w'" 3);
 by Auto_tac;
-bind_thm ("bin_add_type", result() RS bspec);
+qed_spec_mp "bin_add_type";
 Addsimps [bin_add_type];
 
 Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
@@ -169,8 +169,7 @@
 by (rtac ballI 1);
 by (induct_tac "wa" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
-bind_thm("integ_of_add", result() RS bspec);
-
+qed_spec_mp "integ_of_add";
 Addsimps [integ_of_add];
 
 
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/List.ML
--- a/src/ZF/List.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/List.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -34,11 +34,11 @@
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
 by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
-                            Pair_in_univ]) 1);
+				Pair_in_univ]) 1);
 qed "list_univ";
 
 (*These two theorems justify datatypes involving list(nat), list(A), ...*)
-bind_thm ("list_subset_univ", ([list_mono, list_univ] MRS subset_trans));
+bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans);
 
 Goal "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)";
 by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
@@ -177,6 +177,7 @@
 by (induct_tac "l" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
+Addsimps [map_ident];
 
 Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
 by (induct_tac "l" 1);
@@ -203,7 +204,7 @@
 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
 
 (* c : list(Collect(B,P)) ==> c : list(B) *)
-bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
+bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD);
 
 Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
 by (induct_tac "l" 1);
@@ -222,13 +223,9 @@
 by (ALLGOALS Asm_simp_tac);
 qed "length_app";
 
-(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
-   Used for rewriting below*)
-val add_commute_succ = nat_succI RSN (2,add_commute);
-
 Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
 by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
 qed "length_rev";
 
 Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
@@ -244,22 +241,19 @@
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
-qed "drop_length_Cons_lemma";
-bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec));
+qed_spec_mp "drop_length_Cons";
 
-Goal "l: list(A) ==> ALL i: length(l).  EX z zs. drop(i,l) = Cons(z,zs)";
+Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (rtac conjI 1);
+by Safe_tac;
 by (etac drop_length_Cons 1);
-by (rtac ballI 1);
 by (rtac natE 1);
 by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
 by (assume_tac 1);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type])));
-qed "drop_length_lemma";
-bind_thm ("drop_length", (drop_length_lemma RS bspec));
+qed_spec_mp "drop_length";
 
 
 (*** theorems about app ***)
@@ -268,6 +262,7 @@
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_right_Nil";
+Addsimps [app_right_Nil];
 
 Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
 by (induct_tac "xs" 1);
@@ -292,18 +287,20 @@
 *)
 Goal "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
 by (etac list.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
 qed "rev_app_distrib";
 
 Goal "l: list(A) ==> rev(rev(l))=l";
 by (induct_tac "l" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
 qed "rev_rev_ident";
+Addsimps [rev_rev_ident];
 
 Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
 by (induct_tac "ls" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps 
-       [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
+by (ALLGOALS
+    (asm_simp_tac (simpset() addsimps 
+		   [map_app_distrib, flat_app_distrib, rev_app_distrib])));
 qed "rev_flat";
 
 
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/OrdQuant.ML
--- a/src/ZF/OrdQuant.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/OrdQuant.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -5,8 +5,6 @@
 Quantifiers and union operator for ordinals. 
 *)
 
-open OrdQuant;
-
 (*** universal quantifier for ordinals ***)
 
 qed_goalw "oallI" thy [oall_def]
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/QPair.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -122,11 +122,9 @@
 (*** Eliminator - qsplit ***)
 
 (*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "qsplit" thy [qsplit_def]
-    "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
- (fn _ => [ (Simp_tac 1),
-            (rtac reflexive_thm 1) ]);
-
+Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)";
+by (Simp_tac 1);
+qed "qsplit";
 Addsimps [qsplit];
 
 qed_goal "qsplit_type" thy
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/QUniv.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -8,8 +8,20 @@
 
 QUniv = Univ + QPair + mono + equalities +
 
+(*Disjoint sums as a datatype*)
+rep_datatype 
+  elim		sumE
+  induct	TrueI
+  case_eqns	case_Inl, case_Inr
+
+(*Variant disjoint sums as a datatype*)
+rep_datatype 
+  elim		qsumE
+  induct	TrueI
+  case_eqns	qcase_QInl, qcase_QInr
+
 constdefs
   quniv :: i => i
-  "quniv(A) == Pow(univ(eclose(A)))"
+   "quniv(A) == Pow(univ(eclose(A)))"
 
 end
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ROOT.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -28,10 +28,10 @@
 use_thy "Fixedpt";
 use     "Tools/inductive_package";
 use_thy "Inductive";
-use "Tools/induct_tacs";
-use "Tools/primrec_package";
+use     "Tools/induct_tacs";
+use     "Tools/primrec_package";
 use_thy "QUniv";
-use "Tools/datatype_package";
+use     "Tools/datatype_package";
 use_thy "Datatype";
 use_thy "InfDatatype";
 use_thy "List";
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Resid/Redex.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -13,8 +13,6 @@
   "redexes" = Var ("n: nat")            
             | Fun ("t: redexes")
             | App ("b:bool" ,"f:redexes" , "a:redexes")
-  type_intrs "[bool_into_univ]"
-  
 
 
 consts
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Resid/Substitution.ML
--- a/src/ZF/Resid/Substitution.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Resid/Substitution.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -107,13 +107,13 @@
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [lift_rec_Var,
 				       lift_rec_Fun, lift_rec_App])));
-bind_thm ("lift_rec_type", result() RS bspec);
+qed_spec_mp "lift_rec_type";
 
 Goal "v:redexes ==>  ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
 by (etac redexes.induct 1);
 by (ALLGOALS(asm_simp_tac 
     (simpset() addsimps [subst_Var, lift_rec_type])));
-bind_thm ("subst_type", result() RS bspec RS bspec);
+qed_spec_mp "subst_type";
 
 
 Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Resid/Terms.ML
--- a/src/ZF/Resid/Terms.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Resid/Terms.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -30,13 +30,12 @@
 Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
 by (etac lambda.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
-bind_thm ("liftL_type", result() RS bspec);
+qed_spec_mp "liftL_type";
 
 Goal "v:lambda ==>  ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
 by (etac lambda.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
-qed "substL_typea";
-bind_thm ("substL_type", result() RS bspec RS bspec);
+qed_spec_mp "substL_type";
 
 
 (* ------------------------------------------------------------------------- *)
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -19,7 +19,7 @@
     recursor_eqns : thm list,          (*equations for the recursor*)
     free_iffs  : thm list,             (*freeness rewrite rules*)
     free_SEs   : thm list,             (*freeness destruct rules*)
-    mk_free    : string -> thm};      (*makes freeness theorems*)
+    mk_free    : string -> thm};       (*function to make freeness theorems*)
 
 
 signature DATATYPE_ARG =
@@ -302,7 +302,7 @@
 	   (cterm_of (sign_of thy1) (mk_case_eqn arg)))
 	(case_tacsf con_def);
 
-  val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
+  val free_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
 
   val case_eqns = 
       map prove_case_eqn 
@@ -353,10 +353,7 @@
   val constructors =
       map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
 
-  val free_iffs = con_iffs @ 
-    [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
-
-  val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
+  val free_SEs = Ind_Syntax.mk_free_SEs free_iffs;
 
   val {elim, induct, mutual_induct, ...} = ind_result
 
@@ -366,7 +363,7 @@
       prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
                   con_defs s
 	(fn prems => [cut_facts_tac prems 1, 
-		      fast_tac (ZF_cs addSEs free_SEs) 1]);
+		      fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
 
   val simps = case_eqns @ recursor_eqns;
 
@@ -413,11 +410,12 @@
 		  monos, type_intrs, type_elims) thy =
   let val sign = sign_of thy
       val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
+      val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
       val dom_sum = 
           if sdom = "" then
-	      Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "Fixedpt.lfp") rec_tms
+	      Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") 
+	                             (rec_tms, con_ty_lists)
           else readtm sign Ind_Syntax.iT sdom
-      and con_ty_lists	= Ind_Syntax.read_constructs sign scon_ty_lists
   in 
       add_datatype_i (dom_sum, rec_tms, con_ty_lists, 
 		      monos, type_intrs, type_elims) thy
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -111,7 +111,9 @@
 	if exh then #exhaustion (datatype_info_sg sign tn)
 	       else #induct  (datatype_info_sg sign tn)
     val (Const("op :",_) $ Var(ixn,_) $ _) = 
-	FOLogic.dest_Trueprop (hd (prems_of rule))
+        (case prems_of rule of
+	     [] => error "induction is not available for this datatype"
+	   | major::_ => FOLogic.dest_Trueprop major)
     val ind_vname = Syntax.string_of_vname ixn
     val vname' = (*delete leading question mark*)
 	String.substring (ind_vname, 1, size ind_vname-1)
@@ -139,9 +141,11 @@
 	map (head_of o const_of o FOLogic.dest_Trueprop o
 	     #prop o rep_thm) case_eqns;
 
-    val Const ("op :", _) $ _ $ Const(big_rec_name, _) =
+    val Const ("op :", _) $ _ $ data =
 	FOLogic.dest_Trueprop (hd (prems_of elim));	
     
+    val Const(big_rec_name, _) = head_of data;
+
     val simps = case_eqns @ recursor_eqns;
 
     val dt_info =
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Tools/typechk.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -29,5 +29,6 @@
   drawback: does not simplify conjunctions*)
 fun type_auto_tac tyrls hyps = SELECT_GOAL
     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
-           ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
+           ORELSE ares_tac [TrueI,refl,reflexive_thm,iff_refl,
+			    ballI,allI,conjI,impI] 1));
 
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/WF.ML
--- a/src/ZF/WF.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/WF.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -203,8 +203,8 @@
 
 (** r-``{a} is the set of everything under a in r **)
 
-bind_thm ("underI", (vimage_singleton_iff RS iffD2));
-bind_thm ("underD", (vimage_singleton_iff RS iffD1));
+bind_thm ("underI", vimage_singleton_iff RS iffD2);
+bind_thm ("underD", vimage_singleton_iff RS iffD1);
 
 (** is_recfun **)
 
@@ -223,7 +223,7 @@
 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   spec RS mp  instantiates induction hypotheses*)
 fun indhyp_tac hyps =
-    resolve_tac (TrueI::refl::hyps) ORELSE' 
+    resolve_tac (TrueI::refl::reflexive_thm::hyps) ORELSE' 
     (cut_facts_tac hyps THEN'
        DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
                         eresolve_tac [underD, transD, spec RS mp]));
@@ -238,8 +238,7 @@
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (rewtac restrict_def);
 by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
-qed "is_recfun_equal_lemma";
-bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
+qed_spec_mp "is_recfun_equal";
 
 val prems as [wfr,transr,recf,recg,_] = goal WF.thy
     "[| wf(r);  trans(r);       \
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/BT.ML
--- a/src/ZF/ex/BT.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/BT.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -8,6 +8,17 @@
 
 Addsimps bt.intrs;
 
+Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
+by (induct_tac "l" 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs)));
+qed_spec_mp "Br_neq_left";
+
+(*Proving a freeness theorem*)
+val Br_iff = bt.mk_free "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'";
+
+(*An elimination rule, for type-checking*)
+val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
+
 (**  Lemmas to justify using "bt" in other recursive type definitions **)
 
 Goalw bt.defs "A<=B ==> bt(A) <= bt(B)";
@@ -26,7 +37,7 @@
 bind_thm ("bt_subset_univ", [bt_mono, bt_univ] MRS subset_trans);
 
 
-(*Type checking -- proved by induction, as usual*)
+(*Type checking for recursor -- example only; not really needed*)
 val major::prems = goal BT.thy
     "[| t: bt(A);    \
 \       c: C(Lf);       \
@@ -58,14 +69,13 @@
 Goal "t: bt(A) ==> bt_reflect(t) : bt(A)";
 by (induct_tac "t" 1);
 by Auto_tac;
-by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
 qed "bt_reflect_type";
 
 
 (** BT simplification **)
 
 
-Addsimps [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
+Addsimps [n_nodes_type, n_leaves_type, bt_reflect_type];
 
 
 (*** theorems about n_leaves ***)
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/BT.thy
--- a/src/ZF/ex/BT.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/BT.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -6,18 +6,18 @@
 Binary trees
 *)
 
-BT = Datatype +
+BT = Main +
+consts
+    bt          :: i=>i
+
+datatype
+  "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
+
 consts
     n_nodes     :: i=>i
     n_leaves    :: i=>i
     bt_reflect  :: i=>i
 
-    bt          :: i=>i
-
-datatype
-  "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
-  
-
 primrec
   "n_nodes(Lf) = 0"
   "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/Ntree.ML
--- a/src/ZF/ex/Ntree.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Ntree.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -9,8 +9,6 @@
 Based upon ex/Term.ML
 *)
 
-open Ntree;
-
 (** ntree **)
 
 Goal "ntree(A) = A * (UN n: nat. n -> ntree(A))";
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/Primrec.ML
--- a/src/ZF/ex/Primrec.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Primrec.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -70,8 +70,7 @@
 by (etac (succ_leI RS lt_trans1) 2);
 by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
 by Auto_tac;
-qed "lt_ack2_lemma";
-bind_thm ("lt_ack2", (lt_ack2_lemma RS bspec));
+qed_spec_mp "lt_ack2";
 
 (*PROPERTY A 5-, the single-step lemma*)
 Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/Ramsey.ML
--- a/src/ZF/ex/Ramsey.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Ramsey.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -103,11 +103,7 @@
 (*proving the condition*)
 by (Asm_simp_tac 1);
 by (etac Atleast_superset 1 THEN Fast_tac 1);
-qed "pigeon2_lemma";
-
-(* [| m:nat;  n:nat;  Atleast(m #+ n #- succ(0), A Un B) |] ==> 
-   Atleast(m,A) | Atleast(n,B) *)
-bind_thm ("pigeon2", (pigeon2_lemma RS bspec RS spec RS spec RS mp));
+qed_spec_mp "pigeon2";
 
 
 (**** Ramsey's Theorem ****)
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/TF.thy
--- a/src/ZF/ex/TF.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/TF.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -8,6 +8,15 @@
 
 TF = List +
 consts
+  tree, forest, tree_forest    :: i=>i
+
+datatype
+  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
+and
+  "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
+
+
+consts
   map      :: [i=>i, i] => i
   size     :: i=>i
   preorder :: i=>i
@@ -15,13 +24,6 @@
   of_list  :: i=>i
   reflect  :: i=>i
 
-  tree, forest, tree_forest    :: i=>i
-
-datatype
-  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
-and
-  "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
-
 primrec
   "list_of_TF (Tcons(x,f))  = [Tcons(x,f)]"
   "list_of_TF (Fnil)        = []"
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Term.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -7,8 +7,6 @@
 Illustrates the list functor (essentially the same type as in Trees & Forests)
 *)
 
-open Term;
-
 Goal "term(A) = A * list(term(A))";
 let open term;  val rew = rewrite_rule con_defs in  
 by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
@@ -121,7 +119,7 @@
 
 (** term_map **)
 
-bind_thm ("term_map", (term_map_def RS def_term_rec));
+bind_thm ("term_map", term_map_def RS def_term_rec);
 
 val prems = Goalw [term_map_def]
     "[| t: term(A);  !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
@@ -136,7 +134,7 @@
 
 (** term_size **)
 
-bind_thm ("term_size", (term_size_def RS def_term_rec));
+bind_thm ("term_size", term_size_def RS def_term_rec);
 
 Goalw [term_size_def] "t: term(A) ==> term_size(t) : nat";
 by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
@@ -145,7 +143,7 @@
 
 (** reflect **)
 
-bind_thm ("reflect", (reflect_def RS def_term_rec));
+bind_thm ("reflect", reflect_def RS def_term_rec);
 
 Goalw [reflect_def] "t: term(A) ==> reflect(t) : term(A)";
 by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
@@ -153,41 +151,53 @@
 
 (** preorder **)
 
-bind_thm ("preorder", (preorder_def RS def_term_rec));
+bind_thm ("preorder", preorder_def RS def_term_rec);
 
 Goalw [preorder_def]
     "t: term(A) ==> preorder(t) : list(A)";
 by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
 qed "preorder_type";
 
+(** postorder **)
+
+bind_thm ("postorder", postorder_def RS def_term_rec);
+
+Goalw [postorder_def]
+    "t: term(A) ==> postorder(t) : list(A)";
+by (REPEAT (ares_tac [term_rec_simple_type] 1));
+by (Asm_simp_tac 1);
+qed "postorder_type";
+
 
 (** Term simplification **)
 
 val term_typechecks =
     [term.Apply_I, term_map_type, term_map_type2, term_size_type, 
-     reflect_type, preorder_type];
+     reflect_type, preorder_type, postorder_type];
 
 (*map_type2 and term_map_type2 instantiate variables*)
 simpset_ref() := simpset()
-      addsimps [term_rec, term_map, term_size, reflect, preorder]
+      addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]
       setSolver type_auto_tac (list_typechecks@term_typechecks);
 
 
 (** theorems about term_map **)
 
+Addsimps [thm "List.map_compose"];  (*there is also TF.map_compose*)
+
 Goal "t: term(A) ==> term_map(%u. u, t) = t";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_ident]) 1);
+by (Asm_simp_tac 1);
 qed "term_map_ident";
 
 Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps []) 1);
 qed "term_map_compose";
 
 Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym]) 1);
 qed "term_map_reflect";
 
 
@@ -195,18 +205,17 @@
 
 Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps []) 1);
 qed "term_size_term_map";
 
 Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose,
-                                    list_add_rev]) 1);
+by (asm_simp_tac(simpset() addsimps [rev_map_distrib RS sym, list_add_rev]) 1);
 qed "term_size_reflect";
 
 Goal "t: term(A) ==> term_size(t) = length(preorder(t))";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [length_flat, map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps [length_flat]) 1);
 qed "term_size_length";
 
 
@@ -214,8 +223,7 @@
 
 Goal "t: term(A) ==> reflect(reflect(t)) = t";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib, map_compose,
-                                    map_ident, rev_rev_ident]) 1);
+by (asm_simp_tac (simpset() addsimps [rev_map_distrib]) 1);
 qed "reflect_reflect_ident";
 
 
@@ -223,9 +231,14 @@
 
 Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
 by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_compose, map_flat]) 1);
+by (asm_simp_tac (simpset() addsimps [map_flat]) 1);
 qed "preorder_term_map";
 
-(** preorder(reflect(t)) = rev(postorder(t)) **)
+Goal "t: term(A) ==> preorder(reflect(t)) = rev(postorder(t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac(simpset() addsimps [rev_app_distrib, rev_flat, 
+				     rev_map_distrib RS sym]) 1);
+qed "preorder_reflect_eq_rev_postorder";
+
 
 writeln"Reached end of file.";
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ex/Term.thy
--- a/src/ZF/ex/Term.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Term.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -9,12 +9,6 @@
 
 Term = List +
 consts
-  term_rec  :: [i, [i,i,i]=>i] => i
-  term_map  :: [i=>i, i] => i
-  term_size :: i=>i
-  reflect   :: i=>i
-  preorder  :: i=>i
-
   term      :: i=>i
 
 datatype
@@ -26,6 +20,14 @@
     type_intrs  "[list_univ RS subsetD]"
 *)
 
+consts
+  term_rec  :: [i, [i,i,i]=>i] => i
+  term_map  :: [i=>i, i] => i
+  term_size :: i=>i
+  reflect   :: i=>i
+  preorder  :: i=>i
+  postorder :: i=>i
+
 defs
   term_rec_def
    "term_rec(t,d) == 
@@ -39,4 +41,6 @@
 
   preorder_def  "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
 
+  postorder_def "postorder(t) == term_rec(t, %x zs rs. flat(rs) @ [x])"
+
 end
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ind_syntax.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -107,17 +107,32 @@
 and quniv       = Const("QUniv.quniv", iT-->iT);
 
 (*Make a datatype's domain: form the union of its set parameters*)
-fun union_params rec_tm =
+fun union_params (rec_tm, cs) =
   let val (_,args) = strip_comb rec_tm
-  in  case (filter (fn arg => type_of arg = iT) args) of
-         []    => empty
-       | iargs => fold_bal (app Un) iargs
+      fun is_ind arg = (type_of arg = iT)
+  in  case filter is_ind (args @ cs) of
+         []     => empty
+       | u_args => fold_bal (app Un) u_args
   end;
 
-(*Previously these both did    replicate (length rec_tms);  however now
-  [q]univ itself constitutes the sum domain for mutual recursion!*)
-fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
-  | data_domain true  rec_tms = quniv $ union_params (hd rec_tms);
+(*univ or quniv constitutes the sum domain for mutual recursion;
+  it is applied to the datatype parameters and to Consts occurring in the
+  definition other than Nat.nat and the datatype sets themselves.
+  FIXME: could insert all constant set expressions, e.g. nat->nat.*)
+fun data_domain co (rec_tms, con_ty_lists) = 
+    let val rec_names = (*nat doesn't have to be added*)
+	    "Nat.nat" :: map (#1 o dest_Const o head_of) rec_tms
+	val u = if co then quniv else univ
+	fun is_OK (Const(a,T)) = not (a mem_string rec_names)
+	  | is_OK _            = false
+	val add_term_consts_2 =
+	    foldl_aterms (fn (cs, Const c) => Const c ins cs | (cs, _) => cs);
+	fun fourth (_, name, args, prems) = prems
+	fun add_consts_in_cts cts = 
+	    foldl (foldl add_term_consts_2) ([], map fourth (flat cts));
+	val cs = filter is_OK (add_consts_in_cts con_ty_lists)
+    in  u $ union_params (hd rec_tms, cs)  end;
+
 
 (*Could go to FOL, but it's hardly general*)
 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
@@ -141,3 +156,6 @@
 
 end;
 
+
+(*For convenient access by the user*)
+val trace_induct = Ind_Syntax.trace;
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/pair.ML
--- a/src/ZF/pair.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/pair.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -135,10 +135,9 @@
 (*** Eliminator - split ***)
 
 (*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
- (fn _ => [ (Simp_tac 1),
-            (rtac reflexive_thm 1) ]);
-
+Goalw [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)";
+by (Simp_tac 1);
+qed "split";
 Addsimps [split];
 
 qed_goal "split_type" thy
diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/thy_syntax.ML
--- a/src/ZF/thy_syntax.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/thy_syntax.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -140,7 +140,7 @@
   (("elim" $$-- ident) -- 
    ("induct" $$-- ident) --
    ("case_eqns" $$-- list1 ident) -- 
-   ("recursor_eqns" $$-- list1 ident)) >> mk_rep_dt_string;
+   optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
 
 
 (** primrec **)