# HG changeset patch
# User lcp
# Date 749382841 -3600
# Node ID 0b033d50ca1c70826f15871feec3fbb7e9acea86
# Parent  6c6d2f6e318590ded5fb0b3606b91fc97d2f627f
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
called expandshort

diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Bin.ML
--- a/src/ZF/ex/Bin.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/Bin.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -14,18 +14,7 @@
 	  [(["Plus", "Minus"],	"i"),
 	   (["op $$"],		"[i,i]=>i")])];
   val rec_styp = "i";
-  val ext = Some (NewSext {
-	     mixfix =
-	      [Infixl("$$", "[i,i] => i", 60)],
-	     xrules = [],
-	     parse_ast_translation = [],
-	     parse_preproc = None,
-	     parse_postproc = None,
-	     parse_translation = [],
-	     print_translation = [],
-	     print_preproc = None,
-	     print_postproc = None,
-	     print_ast_translation = []});
+  val ext = Some (Syntax.simple_sext [Infixl("$$", "[i,i] => i", 60)]);
   val sintrs = 
 	  ["Plus : bin",
 	   "Minus : bin",
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Comb.ML
--- a/src/ZF/ex/Comb.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/Comb.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -19,18 +19,7 @@
 	  [(["K","S"],	"i"),
 	   (["op #"],	"[i,i]=>i")])];
   val rec_styp = "i";
-  val ext = Some (NewSext {
-	     mixfix =
-	      [Infixl("#", "[i,i] => i", 90)],
-	     xrules = [],
-	     parse_ast_translation = [],
-	     parse_preproc = None,
-	     parse_postproc = None,
-	     parse_translation = [],
-	     print_translation = [],
-	     print_preproc = None,
-	     print_postproc = None,
-	     print_ast_translation = []});
+  val ext = Some (Syntax.simple_sext [Infixl("#", "[i,i] => i", 90)]);
   val sintrs = 
 	  ["K : comb",
 	   "S : comb",
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Contract0.ML
--- a/src/ZF/ex/Contract0.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/Contract0.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -1,7 +1,7 @@
 (*  Title: 	ZF/ex/contract.ML
     ID:         $Id$
-    Author: 	Tobias Nipkow & Lawrence C Paulson
-    Copyright   1992  University of Cambridge
+    Author: 	Lawrence C Paulson
+    Copyright   1993  University of Cambridge
 
 For ex/contract.thy.
 *)
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Contract0.thy
--- a/src/ZF/ex/Contract0.thy	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/Contract0.thy	Thu Sep 30 10:54:01 1993 +0100
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/ex/contract.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow & Lawrence C Paulson
+    Author: 	Lawrence C Paulson
     Copyright   1993  University of Cambridge
 
 Inductive definition of (1-step) contractions and (mult-step) reductions
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Integ.ML
--- a/src/ZF/ex/Integ.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/Integ.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -185,7 +185,7 @@
     "n: nat ==> znegative($~ $# succ(n))";
 by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
 by (REPEAT 
-    (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
+    (resolve_tac [refl, exI, conjI, nat_0_in_succ,
 		  refl RS intrelI RS imageI, consI1, nnat, nat_0I,
 		  nat_succI] 1));
 val znegative_zminus_znat = result();
@@ -377,7 +377,7 @@
 by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
 val zmult_0 = result();
 
-goalw Integ.thy [integ_def,znat_def,one_def]
+goalw Integ.thy [integ_def,znat_def]
     "!!z. z : integ ==> $#1 $* z = z";
 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
 by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/LList.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -55,10 +55,10 @@
 goal LList.thy
    "!!i. i : nat ==> 	\
 \        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
-be complete_induct 1;
-br ballI 1;
-be LList.elim 1;
-bws ([QInl_def,QInr_def]@LList.con_defs);
+by (etac complete_induct 1);
+by (rtac ballI 1);
+by (etac LList.elim 1);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
 by (fast_tac quniv_cs 1);
 by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
 by (fast_tac quniv_cs 1);
@@ -66,9 +66,9 @@
 val llist_quniv_lemma = result();
 
 goal LList.thy "llist(quniv(A)) <= quniv(A)";
-br subsetI 1;
-br quniv_Int_Vfrom 1;
-be (LList.dom_subset RS subsetD) 1;
+by (rtac subsetI 1);
+by (rtac quniv_Int_Vfrom 1);
+by (etac (LList.dom_subset RS subsetD) 1);
 by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
 val llist_quniv = result();
 
@@ -102,20 +102,20 @@
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList_Eq.thy
    "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
-be trans_induct 1;
+by (etac trans_induct 1);
 by (safe_tac subset_cs);
-be LList_Eq.elim 1;
+by (etac LList_Eq.elim 1);
 by (safe_tac (subset_cs addSEs [QPair_inject]));
-bws LList.con_defs;
+by (rewrite_goals_tac LList.con_defs);
 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
 (*0 case*)
 by (fast_tac lleq_cs 1);
 (*succ(j) case*)
-bw QInr_def;
+by (rewtac QInr_def);
 by (fast_tac lleq_cs 1);
 (*Limit(i) case*)
-be (Limit_Vfrom_eq RS ssubst) 1;
-br (Int_UN_distrib RS ssubst) 1;
+by (etac (Limit_Vfrom_eq RS ssubst) 1);
+by (rtac (Int_UN_distrib RS ssubst) 1);
 by (fast_tac lleq_cs 1);
 val lleq_Int_Vset_subset_lemma = result();
 
@@ -125,15 +125,15 @@
 
 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
 val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
-br (prem RS qconverseI RS LList_Eq.co_induct) 1;
-br (LList_Eq.dom_subset RS qconverse_type) 1;
+by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
+by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
 by (safe_tac qconverse_cs);
-be LList_Eq.elim 1;
+by (etac LList_Eq.elim 1);
 by (ALLGOALS (fast_tac qconverse_cs));
 val lleq_symmetric = result();
 
 goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
-br equalityI 1;
+by (rtac equalityI 1);
 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
      ORELSE etac lleq_symmetric 1));
 val lleq_implies_equal = result();
@@ -141,9 +141,9 @@
 val [eqprem,lprem] = goal LList_Eq.thy
     "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
 by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
-br (lprem RS RepFunI RS (eqprem RS subst)) 1;
+by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
 by (safe_tac qpair_cs);
-be LList.elim 1;
+by (etac LList.elim 1);
 by (ALLGOALS (fast_tac qpair_cs));
 val equal_llist_implies_leq = result();
 
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/ListN.ML
--- a/src/ZF/ex/ListN.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/ListN.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -41,3 +41,9 @@
 by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
 val listn_image_eq = result();
 
+goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac ListN.bnd_mono 1));
+by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
+val listn_mono = result();
+
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Primrec0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Primrec0.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -0,0 +1,414 @@
+(*  Title: 	ZF/ex/primrec
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Primitive Recursive Functions
+
+Proof adopted from
+Nora Szasz, 
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+*)
+
+open Primrec0;
+
+val pr0_typechecks = 
+    nat_typechecks @ List.intrs @ 
+    [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
+
+(** Useful special cases of evaluation ***)
+
+val pr0_ss = arith_ss 
+    addsimps List.case_eqns
+    addsimps [list_rec_Nil, list_rec_Cons, 
+	      drop_0, drop_Nil, drop_succ_Cons,
+	      map_Nil, map_Cons]
+    setsolver (type_auto_tac pr0_typechecks);
+
+goalw Primrec0.thy [SC_def]
+    "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
+by (asm_simp_tac pr0_ss 1);
+val SC = result();
+
+goalw Primrec0.thy [CONST_def]
+    "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
+by (asm_simp_tac pr0_ss 1);
+val CONST = result();
+
+goalw Primrec0.thy [PROJ_def]
+    "!!l. [| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
+by (asm_simp_tac pr0_ss 1);
+val PROJ_0 = result();
+
+goalw Primrec0.thy [COMP_def]
+    "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
+by (asm_simp_tac pr0_ss 1);
+val COMP_1 = result();
+
+goalw Primrec0.thy [PREC_def]
+    "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
+by (asm_simp_tac pr0_ss 1);
+val PREC_0 = result();
+
+goalw Primrec0.thy [PREC_def]
+    "!!l. [| x:nat;  l: list(nat) |] ==>  \
+\         PREC(f,g) ` (Cons(succ(x),l)) = \
+\         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
+by (asm_simp_tac pr0_ss 1);
+val PREC_succ = result();
+
+(*** Inductive definition of the PR functions ***)
+
+structure Primrec = Inductive_Fun
+ (val thy = Primrec0.thy;
+  val rec_doms = [("primrec", "list(nat)->nat")];
+  val ext = None
+  val sintrs = 
+      ["SC : primrec",
+       "k: nat ==> CONST(k) : primrec",
+       "i: nat ==> PROJ(i) : primrec",
+       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
+       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
+  val monos = [list_mono];
+  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
+  val type_intrs = pr0_typechecks
+  val type_elims = []);
+
+(* c: primrec ==> c: list(nat) -> nat *)
+val primrec_into_fun = Primrec.dom_subset RS subsetD;
+
+val pr_ss = pr0_ss 
+    setsolver (type_auto_tac ([primrec_into_fun] @ 
+			      pr0_typechecks @ Primrec.intrs));
+
+goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac pr_ss));
+val ACK_in_primrec = result();
+
+val ack_typechecks =
+    [ACK_in_primrec, primrec_into_fun RS apply_type,
+     add_type, list_add_type, naturals_are_ordinals] @ 
+    nat_typechecks @ List.intrs @ Primrec.intrs;
+
+(*strict typechecking for the Ackermann proof; instantiates no vars*)
+fun tc_tac rls =
+    REPEAT
+      (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
+
+goal Primrec.thy "!!i j. [| i:nat;  j:nat |] ==>  ack(i,j): nat";
+by (tc_tac []);
+val ack_type = result();
+
+(** Ackermann's function cases **)
+
+(*PROPERTY A 1*)
+goalw Primrec0.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
+by (asm_simp_tac (pr0_ss addsimps [SC]) 1);
+val ack_0 = result();
+
+(*PROPERTY A 2*)
+goalw Primrec0.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
+by (asm_simp_tac (pr0_ss addsimps [CONST,PREC_0]) 1);
+val ack_succ_0 = result();
+
+(*PROPERTY A 3*)
+(*Could be proved in Primrec0, like the previous two cases, but using
+  primrec_into_fun makes type-checking easier!*)
+goalw Primrec.thy [ACK_def]
+    "!!i j. [| i:nat;  j:nat |] ==> \
+\           ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
+by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
+val ack_succ_succ = result();
+
+val ack_ss = 
+    pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, 
+		    ack_type, naturals_are_ordinals];
+
+(*PROPERTY A 4*)
+goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j : ack(i,j)";
+by (etac nat_induct 1);
+by (asm_simp_tac ack_ss 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","j")] nat_induct 1);
+by (ALLGOALS (asm_simp_tac ack_ss));
+by (rtac ([succI1, asm_rl,naturals_are_ordinals] MRS Ord_trans) 1);
+by (rtac (succ_mem_succI RS Ord_trans1) 3);
+by (etac bspec 5);
+by (ALLGOALS (asm_simp_tac ack_ss));
+val less_ack2_lemma = result();
+val less_ack2 = standard (less_ack2_lemma RS bspec);
+
+(*PROPERTY A 5-, the single-step lemma*)
+goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(i, succ(j))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [less_ack2])));
+val ack_less_ack_succ2 = result();
+
+(*PROPERTY A 5, monotonicity for < *)
+goal Primrec.thy "!!i j k. [| j:k; i:nat; k:nat |] ==> ack(i,j) : ack(i,k)";
+by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
+by (assume_tac 1);
+by (etac succ_less_induct 1);
+by (assume_tac 1);
+by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
+by (REPEAT (ares_tac ([ack_less_ack_succ2, ack_type] @ pr0_typechecks) 1));
+val ack_less_mono2 = result();
+
+(*PROPERTY A 5', monotonicity for <= *)
+goal Primrec.thy
+    "!!i j k. [| j<=k; i:nat; j:nat; k:nat |] ==> ack(i,j) <= ack(i,k)";
+by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_less_mono_imp_mono 1);
+by (REPEAT (ares_tac [ack_less_mono2, ack_type, Ord_nat] 1));
+val ack_mono2 = result();
+
+(*PROPERTY A 6*)
+goal Primrec.thy
+    "!!i j. [| i:nat;  j:nat |] ==> ack(i, succ(j)) <= ack(succ(i), j)";
+by (nat_ind_tac "j" [] 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [subset_refl])));
+by (rtac ack_mono2 1);
+by (rtac (less_ack2 RS Ord_succ_subsetI RS subset_trans) 1);
+by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type] @ pr0_typechecks) 1));
+val ack2_leq_ack1 = result();
+
+(*PROPERTY A 7-, the single-step lemma*)
+goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(succ(i),j)";
+by (rtac (ack_less_mono2 RS Ord_trans2) 1);
+by (rtac (ack2_leq_ack1 RS member_succI) 4);
+by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type, succI1] @ 
+		      pr0_typechecks) 1));
+val ack_less_ack_succ1 = result();
+
+(*PROPERTY A 7, monotonicity for < *)
+goal Primrec.thy "!!i j k. [| i:j; j:nat; k:nat |] ==> ack(i,k) : ack(j,k)";
+by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
+by (assume_tac 1);
+by (etac succ_less_induct 1);
+by (assume_tac 1);
+by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
+by (REPEAT (ares_tac ([ack_less_ack_succ1, ack_type] @ pr0_typechecks) 1));
+val ack_less_mono1 = result();
+
+(*PROPERTY A 7', monotonicity for <= *)
+goal Primrec.thy
+    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> ack(i,k) <= ack(j,k)";
+by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_less_mono_imp_mono 1);
+by (REPEAT (ares_tac [ack_less_mono1, ack_type, Ord_nat] 1));
+val ack_mono1 = result();
+
+(*PROPERTY A 8*)
+goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac ack_ss));
+val ack_1 = result();
+
+(*PROPERTY A 9*)
+goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
+val ack_2 = result();
+
+(*PROPERTY A 10*)
+goal Primrec.thy
+    "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
+\               ack(i1, ack(i2,j)) : ack(succ(succ(i1#+i2)), j)";
+by (rtac Ord_trans2 1);
+by (rtac (ack2_leq_ack1 RS member_succI) 2);
+by (asm_simp_tac ack_ss 1);
+by (rtac ([ack_mono1 RS member_succI, ack_less_mono2] MRS Ord_trans1) 1);
+by (rtac add_leq_self 1);
+by (tc_tac []);
+by (rtac (add_commute RS ssubst) 1);
+by (rtac (add_less_succ_self RS ack_less_mono1) 3);
+by (tc_tac []);
+val ack_nest_bound = result();
+
+(*PROPERTY A 11*)
+goal Primrec.thy
+    "!!i1 i2. [| i1:nat; i2:nat |] ==> \
+\             EX k:nat. ALL j:nat. ack(i1,j) #+ ack(i2,j) : ack(k,j)";
+by (rtac (Ord_trans RS ballI RS bexI) 1);
+by (res_inst_tac [("i1.0", "succ(1)"), ("i2.0", "i1#+i2")] ack_nest_bound 2);
+by (rtac (ack_2 RS ssubst) 1);
+by (tc_tac []);
+by (rtac (member_succI RS succI2 RS succI2) 1);
+by (rtac (add_leq_self RS ack_mono1 RS add_mono) 1);
+by (tc_tac []);
+by (rtac (add_commute RS ssubst) 1);
+by (rtac (add_leq_self RS ack_mono1) 3);
+by (tc_tac []);
+val ack_add_bound = result();
+
+(*PROPERTY A 12 -- note quantifier nesting
+  Article uses existential quantifier but the ALF proof used a concrete
+  expression, namely k#+4. *)
+goal Primrec.thy
+    "!!k. k: nat ==> \
+\         EX k':nat. ALL i:nat. ALL j:nat. i : ack(k,j) --> i#+j : ack(k',j)";
+by (res_inst_tac [("i1.1", "k"), ("i2.1", "0")] (ack_add_bound RS bexE) 1);
+by (rtac (Ord_trans RS impI RS ballI RS ballI RS bexI) 3);
+by (etac bspec 4);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [add_less_mono])));
+val ack_add_bound2 = result();
+
+(*** MAIN RESULT ***)
+
+val ack2_ss =
+    ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, 
+		     naturals_are_ordinals];
+
+goalw Primrec.thy [SC_def]
+    "!!l. l: list(nat) ==> SC ` l : ack(1, list_add(l))";
+by (etac List.elim 1);
+by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
+by (asm_simp_tac (ack2_ss addsimps 
+		  [ack_1, add_less_succ_self RS succ_mem_succI]) 1);
+val SC_case = result();
+
+(*PROPERTY A 4'?? Extra lemma needed for CONST case, constant functions*)
+goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i : ack(i,j)";
+by (etac nat_induct 1);
+by (asm_simp_tac (ack_ss addsimps [nat_0_in_succ]) 1);
+by (etac ([succ_mem_succI, ack_less_ack_succ1] MRS Ord_trans1) 1);
+by (tc_tac []);
+val less_ack1 = result();
+
+goalw Primrec.thy [CONST_def]
+    "!!l. [| l: list(nat);  k: nat |] ==> CONST(k) ` l : ack(k, list_add(l))";
+by (asm_simp_tac (ack2_ss addsimps [less_ack1]) 1);
+val CONST_case = result();
+
+goalw Primrec.thy [PROJ_def]
+    "!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l : ack(0, list_add(l))";
+by (asm_simp_tac ack2_ss 1);
+by (etac List.induct 1);
+by (asm_simp_tac (ack2_ss addsimps [nat_0_in_succ]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","x")] natE 1);
+by (asm_simp_tac (ack2_ss addsimps [add_less_succ_self]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (etac (bspec RS Ord_trans2) 1);
+by (assume_tac 1);
+by (rtac (add_commute RS ssubst) 1);
+by (rtac (add_less_succ_self RS succ_mem_succI) 3);
+by (tc_tac [list_add_type]);
+val PROJ_case_lemma = result();
+val PROJ_case = PROJ_case_lemma RS bspec;
+
+(** COMP case **)
+
+goal Primrec.thy
+ "!!fs. fs : list({f: primrec .					\
+\              	   EX kf:nat. ALL l:list(nat). 			\
+\		    	      f`l : ack(kf, list_add(l))})	\
+\      ==> EX k:nat. ALL l: list(nat). 				\
+\                list_add(map(%f. f ` l, fs)) : ack(k, list_add(l))";
+by (etac List.induct 1);
+by (DO_GOAL [res_inst_tac [("x","0")] bexI,
+	     asm_simp_tac (ack2_ss addsimps [less_ack1,nat_0_in_succ]),
+	     resolve_tac nat_typechecks] 1);
+by (safe_tac ZF_cs);
+by (asm_simp_tac ack2_ss 1);
+by (res_inst_tac [("i1.1", "kf"), ("i2.1", "k")] (ack_add_bound RS bexE) 1
+    THEN REPEAT (assume_tac 1));
+by (rtac (ballI RS bexI) 1);
+by (etac (bspec RS add_less_mono RS Ord_trans) 1);
+by (REPEAT (FIRSTGOAL (etac bspec)));
+by (tc_tac [list_add_type]);
+val COMP_map_lemma = result();
+
+goalw Primrec.thy [COMP_def]
+ "!!g. [| g: primrec;  kg: nat;					\
+\         ALL l:list(nat). g`l : ack(kg, list_add(l));		\
+\         fs : list({f: primrec .				\
+\                    EX kf:nat. ALL l:list(nat). 		\
+\		    	f`l : ack(kf, list_add(l))}) 		\
+\      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l : ack(k, list_add(l))";
+by (asm_simp_tac ZF_ss 1);
+by (forward_tac [list_CollectD] 1);
+by (etac (COMP_map_lemma RS bexE) 1);
+by (rtac (ballI RS bexI) 1);
+by (etac (bspec RS Ord_trans) 1);
+by (rtac Ord_trans 2);
+by (rtac ack_nest_bound 3);
+by (etac (bspec RS ack_less_mono2) 2);
+by (tc_tac [map_type]);
+val COMP_case = result();
+
+(** PREC case **)
+
+goalw Primrec.thy [PREC_def]
+ "!!f g. [| f: primrec;  kf: nat;					\
+\           g: primrec;  kg: nat;					\
+\           ALL l:list(nat). f`l #+ list_add(l) : ack(kf, list_add(l));	\
+\           ALL l:list(nat). g`l #+ list_add(l) : ack(kg, list_add(l));	\
+\           l: list(nat)						\
+\        |] ==> PREC(f,g)`l #+ list_add(l) : ack(succ(kf#+kg), list_add(l))";
+by (etac List.elim 1);
+by (asm_simp_tac (ack2_ss addsimps [[succI1, less_ack2] MRS Ord_trans]) 1);
+by (asm_simp_tac ack2_ss 1);
+be ssubst 1;  (*get rid of the needless assumption*)
+by (eres_inst_tac [("n","a")] nat_induct 1);
+by (asm_simp_tac ack2_ss 1);
+by (rtac Ord_trans 1);
+by (etac bspec 1);
+by (assume_tac 1);
+by (rtac ack_less_mono1 1);
+by (rtac add_less_succ_self 1);
+by (tc_tac [list_add_type]);
+(*ind step -- level 13*)
+by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
+by (rtac (succ_mem_succI RS Ord_trans1) 1);
+by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] Ord_trans1 1);
+by (etac bspec 2);
+by (rtac (subset_refl RS add_mono RS member_succI) 1);
+by (tc_tac []);
+by (asm_simp_tac (ack2_ss addsimps [add_leq_self2]) 1);
+by (asm_simp_tac ack2_ss 1);
+(*final part of the simplification*)
+by (rtac (member_succI RS Ord_trans1) 1);
+by (rtac (add_leq_self2 RS ack_mono1) 1);
+by (etac ack_less_mono2 8);
+by (tc_tac []);
+val PREC_case_lemma = result();
+
+goal Primrec.thy
+ "!!f g. [| f: primrec;  kf: nat;				\
+\           g: primrec;  kg: nat;				\
+\           ALL l:list(nat). f`l : ack(kf, list_add(l));	\
+\           ALL l:list(nat). g`l : ack(kg, list_add(l)) 	\
+\        |] ==> EX k:nat. ALL l: list(nat). 			\
+\		    PREC(f,g)`l: ack(k, list_add(l))";
+by (etac (ack_add_bound2 RS bexE) 1);
+by (etac (ack_add_bound2 RS bexE) 1);
+by (rtac (ballI RS bexI) 1);
+by (rtac ([add_leq_self RS member_succI, PREC_case_lemma] MRS Ord_trans1) 1);
+by (DEPTH_SOLVE
+    (SOMEGOAL
+     (FIRST' [test_assume_tac,
+	      match_tac (ballI::ack_typechecks),
+	      eresolve_tac [bspec, bspec RS bspec RS mp]])));
+val PREC_case = result();
+
+goal Primrec.thy
+    "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l : ack(k, list_add(l))";
+by (etac Primrec.induct 1);
+by (safe_tac ZF_cs);
+by (DEPTH_SOLVE
+    (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
+		       bexI, ballI] @ nat_typechecks) 1));
+val ack_bounds_primrec = result();
+
+goal Primrec.thy
+    "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
+by (rtac notI 1);
+by (etac (ack_bounds_primrec RS bexE) 1);
+by (rtac mem_anti_refl 1);
+by (dres_inst_tac [("x", "[x]")] bspec 1);
+by (asm_simp_tac ack2_ss 1);
+by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
+val ack_not_primrec = result();
+
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Primrec0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Primrec0.thy	Thu Sep 30 10:54:01 1993 +0100
@@ -0,0 +1,46 @@
+(*  Title: 	ZF/ex/primrec.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Primitive Recursive Functions
+
+Proof adopted from
+Nora Szasz, 
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+*)
+
+Primrec0 = ListFn +
+consts
+    SC      :: "i"
+    CONST   :: "i=>i"
+    PROJ    :: "i=>i"
+    COMP    :: "[i,i]=>i"
+    PREC    :: "[i,i]=>i"
+    primrec :: "i"
+    ACK	    :: "i=>i"
+    ack	    :: "[i,i]=>i"
+
+translations
+  "ack(x,y)"  == "ACK(x) ` [y]"
+
+rules
+
+  SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
+
+  CONST_def "CONST(k) == lam l:list(nat).k"
+
+  PROJ_def  "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))"
+
+  COMP_def  "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
+
+  (*Note that g is applied first to PREC(f,g)`y and then to y!*)
+  PREC_def  "PREC(f,g) == \
+\            lam l:list(nat). list_case(0, \
+\                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+  
+  ACK_def   "ACK(i) == rec(i, SC, \
+\                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
+
+end
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Prop.ML
--- a/src/ZF/ex/Prop.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/Prop.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -16,19 +16,9 @@
 	   (["Var"],	"i=>i"),
 	   (["op =>"],	"[i,i]=>i")])];
   val rec_styp = "i";
-  val ext = Some (NewSext {
-	     mixfix =
-	      [Mixfix("#_", "i => i", "Var", [100], 100),
-	       Infixr("=>", "[i,i] => i", 90)],
-	     xrules = [],
-	     parse_ast_translation = [],
-	     parse_preproc = None,
-	     parse_postproc = None,
-	     parse_translation = [],
-	     print_translation = [],
-	     print_preproc = None,
-	     print_postproc = None,
-	     print_ast_translation = []});
+  val ext = Some (Syntax.simple_sext
+		    [Mixfix("#_", "i => i", "Var", [100], 100),
+		     Infixr("=>", "[i,i] => i", 90)]);
   val sintrs = 
 	  ["Fls : prop",
 	   "n: nat ==> #n : prop",
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/PropLog.ML
--- a/src/ZF/ex/PropLog.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/PropLog.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -190,9 +190,10 @@
 by (rtac (expand_if RS iffD2) 1);
 by (rtac (major RS Prop.induct) 1);
 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
-by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
-			   weaken_right, Imp_Fls]
-                    addSEs [Fls_Imp]) 1);
+by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1, 
+			    Fls_Imp RS weaken_left_Un2]));
+by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
+				     weaken_right, Imp_Fls])));
 val hyps_thms_if = result();
 
 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
@@ -264,7 +265,7 @@
 val [major] = goal PropThms.thy
     "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
 by (rtac (major RS Prop.induct) 1);
-by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I] 
+by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I, cons_iff]
 		  setloop (split_tac [expand_if])) 2);
 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
 val hyps_finite = result();
@@ -324,5 +325,3 @@
 val thms_iff = result();
 
 writeln"Reached end of file.";
-
-
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/ROOT.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -6,7 +6,7 @@
 Executes all examples for Zermelo-Fraenkel Set Theory
 *)
 
-ZF_build_completed;	(*Cause examples to fail if ZF did*)
+ZF_build_completed;	(*Make examples fail if ZF did*)
 
 writeln"Root file for ZF Set Theory examples";
 proof_timing := true;
@@ -36,6 +36,8 @@
 time_use     "ex/enum.ML";
 
 (** Inductive definitions **)
+(*mapping a relation over a list*)
+time_use     "ex/rmap.ML";
 (*completeness of propositional logic*)
 time_use     "ex/prop.ML";
 time_use_thy "ex/prop-log";
@@ -46,6 +48,7 @@
 time_use     "ex/comb.ML";
 time_use_thy "ex/contract";
 time_use     "ex/parcontract.ML";
+time_use_thy "ex/primrec";
 
 (** Co-Datatypes **)
 time_use     "ex/llist.ML";
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Rmap.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Rmap.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -0,0 +1,82 @@
+(*  Title: 	ZF/ex/rmap
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+structure Rmap = Inductive_Fun
+ (val thy = List.thy addconsts [(["rmap"],"i=>i")];
+  val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
+  val sintrs = 
+      ["<Nil,Nil> : rmap(r)",
+
+       "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
+\       <Cons(x,xs), Cons(y,ys)> : rmap(r)"];
+  val monos = [];
+  val con_defs = [];
+  val type_intrs = [domainI,rangeI] @ List.intrs @ [SigmaI]
+  val type_elims = [SigmaE2]);
+
+goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac Rmap.bnd_mono 1));
+by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
+		      basic_monos) 1));
+val rmap_mono = result();
+
+val rmap_induct = standard 
+    (Rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
+
+val Nil_rmap_case = Rmap.mk_cases List.con_defs "<Nil,zs> : rmap(r)"
+and Cons_rmap_case = Rmap.mk_cases List.con_defs "<Cons(x,xs),zs> : rmap(r)";
+
+val rmap_cs = ZF_cs addIs  Rmap.intrs
+		    addSEs [Nil_rmap_case, Cons_rmap_case];
+
+goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
+by (rtac (Rmap.dom_subset RS subset_trans) 1);
+by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
+		      Sigma_mono, list_mono] 1));
+val rmap_rel_type = result();
+
+goal Rmap.thy
+    "!!r. [| ALL x:A. EX y. <x,y>: r;  xs: list(A) |] ==> \
+\         EX y. <xs, y> : rmap(r)";
+by (etac List.induct 1);
+by (ALLGOALS (fast_tac rmap_cs));
+val rmap_total = result();
+
+goal Rmap.thy
+    "!!r. [| ALL x y z. <x,y>: r --> <x,z>: r --> y=z;    \
+\            <xs, ys> : rmap(r) |] ==>                    \
+\          ALL zs. <xs, zs> : rmap(r) --> ys=zs";
+by (etac rmap_induct 1);
+by (ALLGOALS (fast_tac rmap_cs));
+val rmap_functional_lemma = result();
+val rmap_functional = standard (rmap_functional_lemma RS spec RS mp);
+
+(** If f is a function then rmap(f) behaves as expected. **)
+
+goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)";
+by (etac PiE 1);
+by (rtac PiI 1);
+by (etac rmap_rel_type 1);
+by (rtac (rmap_total RS ex_ex1I) 1);
+by (assume_tac 2);
+by (fast_tac (ZF_cs addSEs [bspec RS ex1E]) 1);
+by (rtac rmap_functional 1);
+by (REPEAT (assume_tac 2));
+by (fast_tac (ZF_cs addSEs [bspec RS ex1_equalsE]) 1);
+val rmap_fun_type = result();
+
+goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil";
+by (fast_tac (rmap_cs addIs [the_equality]) 1);
+val rmap_Nil = result();
+
+goal Rmap.thy "!!f. [| f: A->B;  x: A;  xs: list(A) |] ==> \
+\                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
+by (rtac apply_equality 1);
+by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ Rmap.intrs) 1));
+val rmap_Cons = result();
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/Term.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -16,7 +16,7 @@
   val ext = None
   val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
   val monos = [list_mono];
-  val type_intrs = [SigmaI,Pair_in_univ, list_univ RS subsetD, A_into_univ];
+  val type_intrs = [list_univ RS subsetD] @ data_typechecks;
   val type_elims = []);
 
 val [ApplyI] = Term.intrs;
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/bin.ML
--- a/src/ZF/ex/bin.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/bin.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -14,18 +14,7 @@
 	  [(["Plus", "Minus"],	"i"),
 	   (["op $$"],		"[i,i]=>i")])];
   val rec_styp = "i";
-  val ext = Some (NewSext {
-	     mixfix =
-	      [Infixl("$$", "[i,i] => i", 60)],
-	     xrules = [],
-	     parse_ast_translation = [],
-	     parse_preproc = None,
-	     parse_postproc = None,
-	     parse_translation = [],
-	     print_translation = [],
-	     print_preproc = None,
-	     print_postproc = None,
-	     print_ast_translation = []});
+  val ext = Some (Syntax.simple_sext [Infixl("$$", "[i,i] => i", 60)]);
   val sintrs = 
 	  ["Plus : bin",
 	   "Minus : bin",
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/comb.ML
--- a/src/ZF/ex/comb.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/comb.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -19,18 +19,7 @@
 	  [(["K","S"],	"i"),
 	   (["op #"],	"[i,i]=>i")])];
   val rec_styp = "i";
-  val ext = Some (NewSext {
-	     mixfix =
-	      [Infixl("#", "[i,i] => i", 90)],
-	     xrules = [],
-	     parse_ast_translation = [],
-	     parse_preproc = None,
-	     parse_postproc = None,
-	     parse_translation = [],
-	     print_translation = [],
-	     print_preproc = None,
-	     print_postproc = None,
-	     print_ast_translation = []});
+  val ext = Some (Syntax.simple_sext [Infixl("#", "[i,i] => i", 90)]);
   val sintrs = 
 	  ["K : comb",
 	   "S : comb",
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/contract0.ML
--- a/src/ZF/ex/contract0.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/contract0.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -1,7 +1,7 @@
 (*  Title: 	ZF/ex/contract.ML
     ID:         $Id$
-    Author: 	Tobias Nipkow & Lawrence C Paulson
-    Copyright   1992  University of Cambridge
+    Author: 	Lawrence C Paulson
+    Copyright   1993  University of Cambridge
 
 For ex/contract.thy.
 *)
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/contract0.thy
--- a/src/ZF/ex/contract0.thy	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/contract0.thy	Thu Sep 30 10:54:01 1993 +0100
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/ex/contract.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow & Lawrence C Paulson
+    Author: 	Lawrence C Paulson
     Copyright   1993  University of Cambridge
 
 Inductive definition of (1-step) contractions and (mult-step) reductions
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/integ.ML
--- a/src/ZF/ex/integ.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/integ.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -185,7 +185,7 @@
     "n: nat ==> znegative($~ $# succ(n))";
 by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
 by (REPEAT 
-    (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
+    (resolve_tac [refl, exI, conjI, nat_0_in_succ,
 		  refl RS intrelI RS imageI, consI1, nnat, nat_0I,
 		  nat_succI] 1));
 val znegative_zminus_znat = result();
@@ -377,7 +377,7 @@
 by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
 val zmult_0 = result();
 
-goalw Integ.thy [integ_def,znat_def,one_def]
+goalw Integ.thy [integ_def,znat_def]
     "!!z. z : integ ==> $#1 $* z = z";
 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
 by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/listn.ML
--- a/src/ZF/ex/listn.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/listn.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -41,3 +41,9 @@
 by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
 val listn_image_eq = result();
 
+goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac ListN.bnd_mono 1));
+by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
+val listn_mono = result();
+
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/llist.ML
--- a/src/ZF/ex/llist.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/llist.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -55,10 +55,10 @@
 goal LList.thy
    "!!i. i : nat ==> 	\
 \        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
-be complete_induct 1;
-br ballI 1;
-be LList.elim 1;
-bws ([QInl_def,QInr_def]@LList.con_defs);
+by (etac complete_induct 1);
+by (rtac ballI 1);
+by (etac LList.elim 1);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
 by (fast_tac quniv_cs 1);
 by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
 by (fast_tac quniv_cs 1);
@@ -66,9 +66,9 @@
 val llist_quniv_lemma = result();
 
 goal LList.thy "llist(quniv(A)) <= quniv(A)";
-br subsetI 1;
-br quniv_Int_Vfrom 1;
-be (LList.dom_subset RS subsetD) 1;
+by (rtac subsetI 1);
+by (rtac quniv_Int_Vfrom 1);
+by (etac (LList.dom_subset RS subsetD) 1);
 by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
 val llist_quniv = result();
 
@@ -102,20 +102,20 @@
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList_Eq.thy
    "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
-be trans_induct 1;
+by (etac trans_induct 1);
 by (safe_tac subset_cs);
-be LList_Eq.elim 1;
+by (etac LList_Eq.elim 1);
 by (safe_tac (subset_cs addSEs [QPair_inject]));
-bws LList.con_defs;
+by (rewrite_goals_tac LList.con_defs);
 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
 (*0 case*)
 by (fast_tac lleq_cs 1);
 (*succ(j) case*)
-bw QInr_def;
+by (rewtac QInr_def);
 by (fast_tac lleq_cs 1);
 (*Limit(i) case*)
-be (Limit_Vfrom_eq RS ssubst) 1;
-br (Int_UN_distrib RS ssubst) 1;
+by (etac (Limit_Vfrom_eq RS ssubst) 1);
+by (rtac (Int_UN_distrib RS ssubst) 1);
 by (fast_tac lleq_cs 1);
 val lleq_Int_Vset_subset_lemma = result();
 
@@ -125,15 +125,15 @@
 
 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
 val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
-br (prem RS qconverseI RS LList_Eq.co_induct) 1;
-br (LList_Eq.dom_subset RS qconverse_type) 1;
+by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
+by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
 by (safe_tac qconverse_cs);
-be LList_Eq.elim 1;
+by (etac LList_Eq.elim 1);
 by (ALLGOALS (fast_tac qconverse_cs));
 val lleq_symmetric = result();
 
 goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
-br equalityI 1;
+by (rtac equalityI 1);
 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
      ORELSE etac lleq_symmetric 1));
 val lleq_implies_equal = result();
@@ -141,9 +141,9 @@
 val [eqprem,lprem] = goal LList_Eq.thy
     "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
 by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
-br (lprem RS RepFunI RS (eqprem RS subst)) 1;
+by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
 by (safe_tac qpair_cs);
-be LList.elim 1;
+by (etac LList.elim 1);
 by (ALLGOALS (fast_tac qpair_cs));
 val equal_llist_implies_leq = result();
 
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/misc.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -62,7 +62,7 @@
 \    X - lfp(X, %W. X - g``(Y - f``W)) ";
 by (res_inst_tac [("P", "%u. ?v = X-u")] 
      (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
-by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, Diff_subset,
+by (simp_tac (ZF_ss addsimps [subset_refl, double_complement,
 			     gfun RS fun_is_rel RS image_subset]) 1);
 val Banach_last_equation = result();
 
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/primrec0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/primrec0.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -0,0 +1,414 @@
+(*  Title: 	ZF/ex/primrec
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Primitive Recursive Functions
+
+Proof adopted from
+Nora Szasz, 
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+*)
+
+open Primrec0;
+
+val pr0_typechecks = 
+    nat_typechecks @ List.intrs @ 
+    [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
+
+(** Useful special cases of evaluation ***)
+
+val pr0_ss = arith_ss 
+    addsimps List.case_eqns
+    addsimps [list_rec_Nil, list_rec_Cons, 
+	      drop_0, drop_Nil, drop_succ_Cons,
+	      map_Nil, map_Cons]
+    setsolver (type_auto_tac pr0_typechecks);
+
+goalw Primrec0.thy [SC_def]
+    "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
+by (asm_simp_tac pr0_ss 1);
+val SC = result();
+
+goalw Primrec0.thy [CONST_def]
+    "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
+by (asm_simp_tac pr0_ss 1);
+val CONST = result();
+
+goalw Primrec0.thy [PROJ_def]
+    "!!l. [| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
+by (asm_simp_tac pr0_ss 1);
+val PROJ_0 = result();
+
+goalw Primrec0.thy [COMP_def]
+    "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
+by (asm_simp_tac pr0_ss 1);
+val COMP_1 = result();
+
+goalw Primrec0.thy [PREC_def]
+    "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
+by (asm_simp_tac pr0_ss 1);
+val PREC_0 = result();
+
+goalw Primrec0.thy [PREC_def]
+    "!!l. [| x:nat;  l: list(nat) |] ==>  \
+\         PREC(f,g) ` (Cons(succ(x),l)) = \
+\         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
+by (asm_simp_tac pr0_ss 1);
+val PREC_succ = result();
+
+(*** Inductive definition of the PR functions ***)
+
+structure Primrec = Inductive_Fun
+ (val thy = Primrec0.thy;
+  val rec_doms = [("primrec", "list(nat)->nat")];
+  val ext = None
+  val sintrs = 
+      ["SC : primrec",
+       "k: nat ==> CONST(k) : primrec",
+       "i: nat ==> PROJ(i) : primrec",
+       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
+       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
+  val monos = [list_mono];
+  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
+  val type_intrs = pr0_typechecks
+  val type_elims = []);
+
+(* c: primrec ==> c: list(nat) -> nat *)
+val primrec_into_fun = Primrec.dom_subset RS subsetD;
+
+val pr_ss = pr0_ss 
+    setsolver (type_auto_tac ([primrec_into_fun] @ 
+			      pr0_typechecks @ Primrec.intrs));
+
+goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac pr_ss));
+val ACK_in_primrec = result();
+
+val ack_typechecks =
+    [ACK_in_primrec, primrec_into_fun RS apply_type,
+     add_type, list_add_type, naturals_are_ordinals] @ 
+    nat_typechecks @ List.intrs @ Primrec.intrs;
+
+(*strict typechecking for the Ackermann proof; instantiates no vars*)
+fun tc_tac rls =
+    REPEAT
+      (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
+
+goal Primrec.thy "!!i j. [| i:nat;  j:nat |] ==>  ack(i,j): nat";
+by (tc_tac []);
+val ack_type = result();
+
+(** Ackermann's function cases **)
+
+(*PROPERTY A 1*)
+goalw Primrec0.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
+by (asm_simp_tac (pr0_ss addsimps [SC]) 1);
+val ack_0 = result();
+
+(*PROPERTY A 2*)
+goalw Primrec0.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
+by (asm_simp_tac (pr0_ss addsimps [CONST,PREC_0]) 1);
+val ack_succ_0 = result();
+
+(*PROPERTY A 3*)
+(*Could be proved in Primrec0, like the previous two cases, but using
+  primrec_into_fun makes type-checking easier!*)
+goalw Primrec.thy [ACK_def]
+    "!!i j. [| i:nat;  j:nat |] ==> \
+\           ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
+by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
+val ack_succ_succ = result();
+
+val ack_ss = 
+    pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, 
+		    ack_type, naturals_are_ordinals];
+
+(*PROPERTY A 4*)
+goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j : ack(i,j)";
+by (etac nat_induct 1);
+by (asm_simp_tac ack_ss 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","j")] nat_induct 1);
+by (ALLGOALS (asm_simp_tac ack_ss));
+by (rtac ([succI1, asm_rl,naturals_are_ordinals] MRS Ord_trans) 1);
+by (rtac (succ_mem_succI RS Ord_trans1) 3);
+by (etac bspec 5);
+by (ALLGOALS (asm_simp_tac ack_ss));
+val less_ack2_lemma = result();
+val less_ack2 = standard (less_ack2_lemma RS bspec);
+
+(*PROPERTY A 5-, the single-step lemma*)
+goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(i, succ(j))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [less_ack2])));
+val ack_less_ack_succ2 = result();
+
+(*PROPERTY A 5, monotonicity for < *)
+goal Primrec.thy "!!i j k. [| j:k; i:nat; k:nat |] ==> ack(i,j) : ack(i,k)";
+by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
+by (assume_tac 1);
+by (etac succ_less_induct 1);
+by (assume_tac 1);
+by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
+by (REPEAT (ares_tac ([ack_less_ack_succ2, ack_type] @ pr0_typechecks) 1));
+val ack_less_mono2 = result();
+
+(*PROPERTY A 5', monotonicity for <= *)
+goal Primrec.thy
+    "!!i j k. [| j<=k; i:nat; j:nat; k:nat |] ==> ack(i,j) <= ack(i,k)";
+by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_less_mono_imp_mono 1);
+by (REPEAT (ares_tac [ack_less_mono2, ack_type, Ord_nat] 1));
+val ack_mono2 = result();
+
+(*PROPERTY A 6*)
+goal Primrec.thy
+    "!!i j. [| i:nat;  j:nat |] ==> ack(i, succ(j)) <= ack(succ(i), j)";
+by (nat_ind_tac "j" [] 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [subset_refl])));
+by (rtac ack_mono2 1);
+by (rtac (less_ack2 RS Ord_succ_subsetI RS subset_trans) 1);
+by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type] @ pr0_typechecks) 1));
+val ack2_leq_ack1 = result();
+
+(*PROPERTY A 7-, the single-step lemma*)
+goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) : ack(succ(i),j)";
+by (rtac (ack_less_mono2 RS Ord_trans2) 1);
+by (rtac (ack2_leq_ack1 RS member_succI) 4);
+by (REPEAT (ares_tac ([naturals_are_ordinals, ack_type, succI1] @ 
+		      pr0_typechecks) 1));
+val ack_less_ack_succ1 = result();
+
+(*PROPERTY A 7, monotonicity for < *)
+goal Primrec.thy "!!i j k. [| i:j; j:nat; k:nat |] ==> ack(i,k) : ack(j,k)";
+by (forward_tac [Ord_nat RSN (3,Ord_trans)] 1);
+by (assume_tac 1);
+by (etac succ_less_induct 1);
+by (assume_tac 1);
+by (rtac (naturals_are_ordinals RSN (3,Ord_trans)) 2);
+by (REPEAT (ares_tac ([ack_less_ack_succ1, ack_type] @ pr0_typechecks) 1));
+val ack_less_mono1 = result();
+
+(*PROPERTY A 7', monotonicity for <= *)
+goal Primrec.thy
+    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> ack(i,k) <= ack(j,k)";
+by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_less_mono_imp_mono 1);
+by (REPEAT (ares_tac [ack_less_mono1, ack_type, Ord_nat] 1));
+val ack_mono1 = result();
+
+(*PROPERTY A 8*)
+goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac ack_ss));
+val ack_1 = result();
+
+(*PROPERTY A 9*)
+goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
+val ack_2 = result();
+
+(*PROPERTY A 10*)
+goal Primrec.thy
+    "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
+\               ack(i1, ack(i2,j)) : ack(succ(succ(i1#+i2)), j)";
+by (rtac Ord_trans2 1);
+by (rtac (ack2_leq_ack1 RS member_succI) 2);
+by (asm_simp_tac ack_ss 1);
+by (rtac ([ack_mono1 RS member_succI, ack_less_mono2] MRS Ord_trans1) 1);
+by (rtac add_leq_self 1);
+by (tc_tac []);
+by (rtac (add_commute RS ssubst) 1);
+by (rtac (add_less_succ_self RS ack_less_mono1) 3);
+by (tc_tac []);
+val ack_nest_bound = result();
+
+(*PROPERTY A 11*)
+goal Primrec.thy
+    "!!i1 i2. [| i1:nat; i2:nat |] ==> \
+\             EX k:nat. ALL j:nat. ack(i1,j) #+ ack(i2,j) : ack(k,j)";
+by (rtac (Ord_trans RS ballI RS bexI) 1);
+by (res_inst_tac [("i1.0", "succ(1)"), ("i2.0", "i1#+i2")] ack_nest_bound 2);
+by (rtac (ack_2 RS ssubst) 1);
+by (tc_tac []);
+by (rtac (member_succI RS succI2 RS succI2) 1);
+by (rtac (add_leq_self RS ack_mono1 RS add_mono) 1);
+by (tc_tac []);
+by (rtac (add_commute RS ssubst) 1);
+by (rtac (add_leq_self RS ack_mono1) 3);
+by (tc_tac []);
+val ack_add_bound = result();
+
+(*PROPERTY A 12 -- note quantifier nesting
+  Article uses existential quantifier but the ALF proof used a concrete
+  expression, namely k#+4. *)
+goal Primrec.thy
+    "!!k. k: nat ==> \
+\         EX k':nat. ALL i:nat. ALL j:nat. i : ack(k,j) --> i#+j : ack(k',j)";
+by (res_inst_tac [("i1.1", "k"), ("i2.1", "0")] (ack_add_bound RS bexE) 1);
+by (rtac (Ord_trans RS impI RS ballI RS ballI RS bexI) 3);
+by (etac bspec 4);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [add_less_mono])));
+val ack_add_bound2 = result();
+
+(*** MAIN RESULT ***)
+
+val ack2_ss =
+    ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, 
+		     naturals_are_ordinals];
+
+goalw Primrec.thy [SC_def]
+    "!!l. l: list(nat) ==> SC ` l : ack(1, list_add(l))";
+by (etac List.elim 1);
+by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
+by (asm_simp_tac (ack2_ss addsimps 
+		  [ack_1, add_less_succ_self RS succ_mem_succI]) 1);
+val SC_case = result();
+
+(*PROPERTY A 4'?? Extra lemma needed for CONST case, constant functions*)
+goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i : ack(i,j)";
+by (etac nat_induct 1);
+by (asm_simp_tac (ack_ss addsimps [nat_0_in_succ]) 1);
+by (etac ([succ_mem_succI, ack_less_ack_succ1] MRS Ord_trans1) 1);
+by (tc_tac []);
+val less_ack1 = result();
+
+goalw Primrec.thy [CONST_def]
+    "!!l. [| l: list(nat);  k: nat |] ==> CONST(k) ` l : ack(k, list_add(l))";
+by (asm_simp_tac (ack2_ss addsimps [less_ack1]) 1);
+val CONST_case = result();
+
+goalw Primrec.thy [PROJ_def]
+    "!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l : ack(0, list_add(l))";
+by (asm_simp_tac ack2_ss 1);
+by (etac List.induct 1);
+by (asm_simp_tac (ack2_ss addsimps [nat_0_in_succ]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","x")] natE 1);
+by (asm_simp_tac (ack2_ss addsimps [add_less_succ_self]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (etac (bspec RS Ord_trans2) 1);
+by (assume_tac 1);
+by (rtac (add_commute RS ssubst) 1);
+by (rtac (add_less_succ_self RS succ_mem_succI) 3);
+by (tc_tac [list_add_type]);
+val PROJ_case_lemma = result();
+val PROJ_case = PROJ_case_lemma RS bspec;
+
+(** COMP case **)
+
+goal Primrec.thy
+ "!!fs. fs : list({f: primrec .					\
+\              	   EX kf:nat. ALL l:list(nat). 			\
+\		    	      f`l : ack(kf, list_add(l))})	\
+\      ==> EX k:nat. ALL l: list(nat). 				\
+\                list_add(map(%f. f ` l, fs)) : ack(k, list_add(l))";
+by (etac List.induct 1);
+by (DO_GOAL [res_inst_tac [("x","0")] bexI,
+	     asm_simp_tac (ack2_ss addsimps [less_ack1,nat_0_in_succ]),
+	     resolve_tac nat_typechecks] 1);
+by (safe_tac ZF_cs);
+by (asm_simp_tac ack2_ss 1);
+by (res_inst_tac [("i1.1", "kf"), ("i2.1", "k")] (ack_add_bound RS bexE) 1
+    THEN REPEAT (assume_tac 1));
+by (rtac (ballI RS bexI) 1);
+by (etac (bspec RS add_less_mono RS Ord_trans) 1);
+by (REPEAT (FIRSTGOAL (etac bspec)));
+by (tc_tac [list_add_type]);
+val COMP_map_lemma = result();
+
+goalw Primrec.thy [COMP_def]
+ "!!g. [| g: primrec;  kg: nat;					\
+\         ALL l:list(nat). g`l : ack(kg, list_add(l));		\
+\         fs : list({f: primrec .				\
+\                    EX kf:nat. ALL l:list(nat). 		\
+\		    	f`l : ack(kf, list_add(l))}) 		\
+\      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l : ack(k, list_add(l))";
+by (asm_simp_tac ZF_ss 1);
+by (forward_tac [list_CollectD] 1);
+by (etac (COMP_map_lemma RS bexE) 1);
+by (rtac (ballI RS bexI) 1);
+by (etac (bspec RS Ord_trans) 1);
+by (rtac Ord_trans 2);
+by (rtac ack_nest_bound 3);
+by (etac (bspec RS ack_less_mono2) 2);
+by (tc_tac [map_type]);
+val COMP_case = result();
+
+(** PREC case **)
+
+goalw Primrec.thy [PREC_def]
+ "!!f g. [| f: primrec;  kf: nat;					\
+\           g: primrec;  kg: nat;					\
+\           ALL l:list(nat). f`l #+ list_add(l) : ack(kf, list_add(l));	\
+\           ALL l:list(nat). g`l #+ list_add(l) : ack(kg, list_add(l));	\
+\           l: list(nat)						\
+\        |] ==> PREC(f,g)`l #+ list_add(l) : ack(succ(kf#+kg), list_add(l))";
+by (etac List.elim 1);
+by (asm_simp_tac (ack2_ss addsimps [[succI1, less_ack2] MRS Ord_trans]) 1);
+by (asm_simp_tac ack2_ss 1);
+be ssubst 1;  (*get rid of the needless assumption*)
+by (eres_inst_tac [("n","a")] nat_induct 1);
+by (asm_simp_tac ack2_ss 1);
+by (rtac Ord_trans 1);
+by (etac bspec 1);
+by (assume_tac 1);
+by (rtac ack_less_mono1 1);
+by (rtac add_less_succ_self 1);
+by (tc_tac [list_add_type]);
+(*ind step -- level 13*)
+by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
+by (rtac (succ_mem_succI RS Ord_trans1) 1);
+by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] Ord_trans1 1);
+by (etac bspec 2);
+by (rtac (subset_refl RS add_mono RS member_succI) 1);
+by (tc_tac []);
+by (asm_simp_tac (ack2_ss addsimps [add_leq_self2]) 1);
+by (asm_simp_tac ack2_ss 1);
+(*final part of the simplification*)
+by (rtac (member_succI RS Ord_trans1) 1);
+by (rtac (add_leq_self2 RS ack_mono1) 1);
+by (etac ack_less_mono2 8);
+by (tc_tac []);
+val PREC_case_lemma = result();
+
+goal Primrec.thy
+ "!!f g. [| f: primrec;  kf: nat;				\
+\           g: primrec;  kg: nat;				\
+\           ALL l:list(nat). f`l : ack(kf, list_add(l));	\
+\           ALL l:list(nat). g`l : ack(kg, list_add(l)) 	\
+\        |] ==> EX k:nat. ALL l: list(nat). 			\
+\		    PREC(f,g)`l: ack(k, list_add(l))";
+by (etac (ack_add_bound2 RS bexE) 1);
+by (etac (ack_add_bound2 RS bexE) 1);
+by (rtac (ballI RS bexI) 1);
+by (rtac ([add_leq_self RS member_succI, PREC_case_lemma] MRS Ord_trans1) 1);
+by (DEPTH_SOLVE
+    (SOMEGOAL
+     (FIRST' [test_assume_tac,
+	      match_tac (ballI::ack_typechecks),
+	      eresolve_tac [bspec, bspec RS bspec RS mp]])));
+val PREC_case = result();
+
+goal Primrec.thy
+    "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l : ack(k, list_add(l))";
+by (etac Primrec.induct 1);
+by (safe_tac ZF_cs);
+by (DEPTH_SOLVE
+    (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
+		       bexI, ballI] @ nat_typechecks) 1));
+val ack_bounds_primrec = result();
+
+goal Primrec.thy
+    "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
+by (rtac notI 1);
+by (etac (ack_bounds_primrec RS bexE) 1);
+by (rtac mem_anti_refl 1);
+by (dres_inst_tac [("x", "[x]")] bspec 1);
+by (asm_simp_tac ack2_ss 1);
+by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
+val ack_not_primrec = result();
+
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/primrec0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/primrec0.thy	Thu Sep 30 10:54:01 1993 +0100
@@ -0,0 +1,46 @@
+(*  Title: 	ZF/ex/primrec.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Primitive Recursive Functions
+
+Proof adopted from
+Nora Szasz, 
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+*)
+
+Primrec0 = ListFn +
+consts
+    SC      :: "i"
+    CONST   :: "i=>i"
+    PROJ    :: "i=>i"
+    COMP    :: "[i,i]=>i"
+    PREC    :: "[i,i]=>i"
+    primrec :: "i"
+    ACK	    :: "i=>i"
+    ack	    :: "[i,i]=>i"
+
+translations
+  "ack(x,y)"  == "ACK(x) ` [y]"
+
+rules
+
+  SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
+
+  CONST_def "CONST(k) == lam l:list(nat).k"
+
+  PROJ_def  "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))"
+
+  COMP_def  "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
+
+  (*Note that g is applied first to PREC(f,g)`y and then to y!*)
+  PREC_def  "PREC(f,g) == \
+\            lam l:list(nat). list_case(0, \
+\                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+  
+  ACK_def   "ACK(i) == rec(i, SC, \
+\                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
+
+end
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/prop.ML
--- a/src/ZF/ex/prop.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/prop.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -16,19 +16,9 @@
 	   (["Var"],	"i=>i"),
 	   (["op =>"],	"[i,i]=>i")])];
   val rec_styp = "i";
-  val ext = Some (NewSext {
-	     mixfix =
-	      [Mixfix("#_", "i => i", "Var", [100], 100),
-	       Infixr("=>", "[i,i] => i", 90)],
-	     xrules = [],
-	     parse_ast_translation = [],
-	     parse_preproc = None,
-	     parse_postproc = None,
-	     parse_translation = [],
-	     print_translation = [],
-	     print_preproc = None,
-	     print_postproc = None,
-	     print_ast_translation = []});
+  val ext = Some (Syntax.simple_sext
+		    [Mixfix("#_", "i => i", "Var", [100], 100),
+		     Infixr("=>", "[i,i] => i", 90)]);
   val sintrs = 
 	  ["Fls : prop",
 	   "n: nat ==> #n : prop",
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/proplog.ML
--- a/src/ZF/ex/proplog.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/proplog.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -190,9 +190,10 @@
 by (rtac (expand_if RS iffD2) 1);
 by (rtac (major RS Prop.induct) 1);
 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
-by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
-			   weaken_right, Imp_Fls]
-                    addSEs [Fls_Imp]) 1);
+by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1, 
+			    Fls_Imp RS weaken_left_Un2]));
+by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2, 
+				     weaken_right, Imp_Fls])));
 val hyps_thms_if = result();
 
 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
@@ -264,7 +265,7 @@
 val [major] = goal PropThms.thy
     "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
 by (rtac (major RS Prop.induct) 1);
-by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I] 
+by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I, cons_iff]
 		  setloop (split_tac [expand_if])) 2);
 by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
 val hyps_finite = result();
@@ -324,5 +325,3 @@
 val thms_iff = result();
 
 writeln"Reached end of file.";
-
-
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/rmap.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/rmap.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -0,0 +1,82 @@
+(*  Title: 	ZF/ex/rmap
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+structure Rmap = Inductive_Fun
+ (val thy = List.thy addconsts [(["rmap"],"i=>i")];
+  val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
+  val sintrs = 
+      ["<Nil,Nil> : rmap(r)",
+
+       "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
+\       <Cons(x,xs), Cons(y,ys)> : rmap(r)"];
+  val monos = [];
+  val con_defs = [];
+  val type_intrs = [domainI,rangeI] @ List.intrs @ [SigmaI]
+  val type_elims = [SigmaE2]);
+
+goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac Rmap.bnd_mono 1));
+by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
+		      basic_monos) 1));
+val rmap_mono = result();
+
+val rmap_induct = standard 
+    (Rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
+
+val Nil_rmap_case = Rmap.mk_cases List.con_defs "<Nil,zs> : rmap(r)"
+and Cons_rmap_case = Rmap.mk_cases List.con_defs "<Cons(x,xs),zs> : rmap(r)";
+
+val rmap_cs = ZF_cs addIs  Rmap.intrs
+		    addSEs [Nil_rmap_case, Cons_rmap_case];
+
+goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
+by (rtac (Rmap.dom_subset RS subset_trans) 1);
+by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
+		      Sigma_mono, list_mono] 1));
+val rmap_rel_type = result();
+
+goal Rmap.thy
+    "!!r. [| ALL x:A. EX y. <x,y>: r;  xs: list(A) |] ==> \
+\         EX y. <xs, y> : rmap(r)";
+by (etac List.induct 1);
+by (ALLGOALS (fast_tac rmap_cs));
+val rmap_total = result();
+
+goal Rmap.thy
+    "!!r. [| ALL x y z. <x,y>: r --> <x,z>: r --> y=z;    \
+\            <xs, ys> : rmap(r) |] ==>                    \
+\          ALL zs. <xs, zs> : rmap(r) --> ys=zs";
+by (etac rmap_induct 1);
+by (ALLGOALS (fast_tac rmap_cs));
+val rmap_functional_lemma = result();
+val rmap_functional = standard (rmap_functional_lemma RS spec RS mp);
+
+(** If f is a function then rmap(f) behaves as expected. **)
+
+goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)";
+by (etac PiE 1);
+by (rtac PiI 1);
+by (etac rmap_rel_type 1);
+by (rtac (rmap_total RS ex_ex1I) 1);
+by (assume_tac 2);
+by (fast_tac (ZF_cs addSEs [bspec RS ex1E]) 1);
+by (rtac rmap_functional 1);
+by (REPEAT (assume_tac 2));
+by (fast_tac (ZF_cs addSEs [bspec RS ex1_equalsE]) 1);
+val rmap_fun_type = result();
+
+goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil";
+by (fast_tac (rmap_cs addIs [the_equality]) 1);
+val rmap_Nil = result();
+
+goal Rmap.thy "!!f. [| f: A->B;  x: A;  xs: list(A) |] ==> \
+\                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
+by (rtac apply_equality 1);
+by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ Rmap.intrs) 1));
+val rmap_Cons = result();
diff -r 6c6d2f6e3185 -r 0b033d50ca1c src/ZF/ex/term.ML
--- a/src/ZF/ex/term.ML	Thu Sep 30 10:26:38 1993 +0100
+++ b/src/ZF/ex/term.ML	Thu Sep 30 10:54:01 1993 +0100
@@ -16,7 +16,7 @@
   val ext = None
   val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
   val monos = [list_mono];
-  val type_intrs = [SigmaI,Pair_in_univ, list_univ RS subsetD, A_into_univ];
+  val type_intrs = [list_univ RS subsetD] @ data_typechecks;
   val type_elims = []);
 
 val [ApplyI] = Term.intrs;