# HG changeset patch
# User lcp
# Date 776687326 -7200
# Node ID abcc438e7c27f906f71007a20283bda6792557bc
# Parent  ab2c867829ec3dcdaff7165e44a20d26647e10f9
installation of new inductive/datatype sections

diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Acc.ML
--- a/src/ZF/ex/Acc.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Acc.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -9,21 +9,19 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-structure Acc = Inductive_Fun
- (val thy        = WF.thy |> add_consts [("acc","i=>i",NoSyn)]
-  val thy_name   = "Acc"
-  val rec_doms   = [("acc", "field(r)")]
-  val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
-  val monos      = [Pow_mono]
-  val con_defs   = []
-  val type_intrs = []
-  val type_elims = []);
+open Acc;
 
 (*The introduction rule must require  a:field(r)  
   Otherwise acc(r) would be a proper class!    *)
 
+(*The intended introduction rule*)
+val prems = goal Acc.thy
+    "[| !!b. <b,a>:r ==> b: acc(r);  a: field(r) |] ==> a: acc(r)";
+by (fast_tac (ZF_cs addIs (prems@acc.intrs)) 1);
+val accI = result();
+
 goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
-by (etac Acc.elim 1);
+by (etac acc.elim 1);
 by (fast_tac ZF_cs 1);
 val acc_downward = result();
 
@@ -31,12 +29,12 @@
     "[| a : acc(r);						\
 \       !!x. [| x: acc(r);  ALL y. <y,x>:r --> P(y) |] ==> P(x)	\
 \    |] ==> P(a)";
-by (rtac (major RS Acc.induct) 1);
+by (rtac (major RS acc.induct) 1);
 by (rtac indhyp 1);
 by (fast_tac ZF_cs 2);
-by (resolve_tac Acc.intrs 1);
+by (resolve_tac acc.intrs 1);
 by (assume_tac 2);
-by (fast_tac ZF_cs 1);
+be (Collect_subset RS Pow_mono RS subsetD) 1;
 val acc_induct = result();
 
 goal Acc.thy "wf[acc(r)](r)";
@@ -52,7 +50,7 @@
 by (rtac subsetI 1);
 by (etac (major RS wf_induct2) 1);
 by (rtac subset_refl 1);
-by (resolve_tac Acc.intrs 1);
+by (resolve_tac [accI] 1);
 by (assume_tac 2);
 by (fast_tac ZF_cs 1);
 val acc_wfD = result();
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Acc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Acc.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,23 @@
+(*  Title: 	ZF/ex/Acc.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of acc(r)
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
+*)
+
+Acc = WF + "inductive" +
+
+consts
+  "acc" :: "i=>i"
+
+inductive
+  domains "acc(r)" <= "field(r)"
+  intrs
+    vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
+  monos     "[Pow_mono]"
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/BT.ML
--- a/src/ZF/ex/BT.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/BT.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -1,44 +1,29 @@
-(*  Title: 	ZF/ex/bt.ML
+(*  Title: 	ZF/ex/BT.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Datatype definition of binary trees
 *)
 
-structure BT = Datatype_Fun
- (val thy = Univ.thy;
-  val thy_name = "BT";
-  val rec_specs = 
-      [("bt", "univ(A)",
-	  [(["Lf"],"i",NoSyn), 
-           (["Br"],"[i,i,i]=>i", NoSyn)])];
-  val rec_styp = "i=>i";
-  val sintrs = 
-	  ["Lf : bt(A)",
-	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
-  val monos = [];
-  val type_intrs = datatype_intrs
-  val type_elims = []);
-
-val [LfI, BrI] = BT.intrs;
+open BT;
 
 (*Perform induction on l, then prove the major premise using prems. *)
 fun bt_ind_tac a prems i = 
-    EVERY [res_inst_tac [("x",a)] BT.induct i,
+    EVERY [res_inst_tac [("x",a)] bt.induct i,
 	   rename_last_tac a ["1","2"] (i+2),
 	   ares_tac prems i];
 
 
 (**  Lemmas to justify using "bt" in other recursive type definitions **)
 
-goalw BT.thy BT.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
+goalw BT.thy bt.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
 by (rtac lfp_mono 1);
-by (REPEAT (rtac BT.bnd_mono 1));
+by (REPEAT (rtac bt.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
 val bt_mono = result();
 
-goalw BT.thy (BT.defs@BT.con_defs) "bt(univ(A)) <= univ(A)";
+goalw BT.thy (bt.defs@bt.con_defs) "bt(univ(A)) <= univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
@@ -47,3 +32,119 @@
 
 val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
 
+
+(** bt_rec -- by Vset recursion **)
+
+goalw BT.thy bt.con_defs "rank(l) < rank(Br(a,l,r))";
+by (simp_tac rank_ss 1);
+val rank_Br1 = result();
+
+goalw BT.thy bt.con_defs "rank(r) < rank(Br(a,l,r))";
+by (simp_tac rank_ss 1);
+val rank_Br2 = result();
+
+goal BT.thy "bt_rec(Lf,c,h) = c";
+by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (ZF_ss addsimps bt.case_eqns) 1);
+val bt_rec_Lf = result();
+
+goal BT.thy
+    "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
+by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1);
+val bt_rec_Br = result();
+
+(*Type checking -- proved by induction, as usual*)
+val prems = goal BT.thy
+    "[| t: bt(A);    \
+\       c: C(Lf);       \
+\       !!x y z r s. [| x:A;  y:bt(A);  z:bt(A);  r:C(y);  s:C(z) |] ==> \
+\		     h(x,y,z,r,s): C(Br(x,y,z))  \
+\    |] ==> bt_rec(t,c,h) : C(t)";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
+			    (prems@[bt_rec_Lf,bt_rec_Br]))));
+val bt_rec_type = result();
+
+(** Versions for use with definitions **)
+
+val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
+by (rewtac rew);
+by (rtac bt_rec_Lf 1);
+val def_bt_rec_Lf = result();
+
+val [rew] = goal BT.thy
+    "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
+by (rewtac rew);
+by (rtac bt_rec_Br 1);
+val def_bt_rec_Br = result();
+
+fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
+
+(** n_nodes **)
+
+val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
+
+val prems = goalw BT.thy [n_nodes_def] 
+    "xs: bt(A) ==> n_nodes(xs) : nat";
+by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
+val n_nodes_type = result();
+
+
+(** n_leaves **)
+
+val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
+
+val prems = goalw BT.thy [n_leaves_def] 
+    "xs: bt(A) ==> n_leaves(xs) : nat";
+by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
+val n_leaves_type = result();
+
+(** bt_reflect **)
+
+val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
+
+goalw BT.thy [bt_reflect_def] "!!xs. xs: bt(A) ==> bt_reflect(xs) : bt(A)";
+by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
+val bt_reflect_type = result();
+
+
+(** BT simplification **)
+
+
+val bt_typechecks =
+    bt.intrs @ [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
+
+val bt_ss = arith_ss 
+    addsimps bt.case_eqns
+    addsimps bt_typechecks
+    addsimps [bt_rec_Lf, bt_rec_Br, 
+	     n_nodes_Lf, n_nodes_Br,
+	     n_leaves_Lf, n_leaves_Br,
+	     bt_reflect_Lf, bt_reflect_Br];
+
+
+(*** theorems about n_leaves ***)
+
+val prems = goal BT.thy
+    "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
+val n_leaves_reflect = result();
+
+val prems = goal BT.thy
+    "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
+val n_leaves_nodes = result();
+
+(*** theorems about bt_reflect ***)
+
+val prems = goal BT.thy
+    "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+val bt_reflect_bt_reflect_ident = result();
+
+
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/BT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/BT.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,29 @@
+(*  Title: 	ZF/ex/bt-fn.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Binary trees
+*)
+
+BT = Univ +
+consts
+    bt_rec    	:: "[i, i, [i,i,i,i,i]=>i] => i"
+    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)")
+  
+rules
+  bt_rec_def
+    "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
+
+  n_nodes_def	"n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
+  n_leaves_def	"n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
+  bt_reflect_def "bt_reflect(t) == bt_rec(t,  Lf,  %x y z r s. Br(x,s,r))"
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Bin.ML
--- a/src/ZF/ex/Bin.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Bin.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -1,31 +1,456 @@
-(*  Title: 	ZF/ex/bin.ML
+(*  Title: 	ZF/ex/Bin.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1994  University of Cambridge
 
-Datatype of binary integers
+For Bin.thy.  Arithmetic on binary integers.
 *)
 
-(*Example of a datatype with an infix constructor*)
-structure Bin = Datatype_Fun
- (val thy = Univ.thy;
-  val thy_name = "Bin";
-  val rec_specs = 
-      [("bin", "univ(0)",
-	  [(["Plus", "Minus"],	"i", NoSyn),
-	   (["$$"],		"[i,i]=>i", Infixl 60)])];
-  val rec_styp = "i";
-  val sintrs = 
-	  ["Plus : bin",
-	   "Minus : bin",
-	   "[| w: bin;  b: bool |] ==> w$$b : bin"];
-  val monos = [];
-  val type_intrs = datatype_intrs @ [bool_into_univ];
-  val type_elims = []);
+open Bin;
 
 (*Perform induction on l, then prove the major premise using prems. *)
 fun bin_ind_tac a prems i = 
-    EVERY [res_inst_tac [("x",a)] Bin.induct i,
+    EVERY [res_inst_tac [("x",a)] bin.induct i,
 	   rename_last_tac a ["1"] (i+3),
 	   ares_tac prems i];
 
+
+(** bin_rec -- by Vset recursion **)
+
+goal Bin.thy "bin_rec(Plus,a,b,h) = a";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+val bin_rec_Plus = result();
+
+goal Bin.thy "bin_rec(Minus,a,b,h) = b";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+val bin_rec_Minus = result();
+
+goal Bin.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+val bin_rec_Bcons = result();
+
+(*Type checking*)
+val prems = goal Bin.thy
+    "[| w: bin;    \
+\       a: C(Plus);   b: C(Minus);       \
+\       !!w x r. [| w: bin;  x: bool;  r: C(w) |] ==> h(w,x,r): C(w$$x)  \
+\    |] ==> bin_rec(w,a,b,h) : C(w)";
+by (bin_ind_tac "w" prems 1);
+by (ALLGOALS 
+    (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus,
+					 bin_rec_Bcons]))));
+val bin_rec_type = result();
+
+(** Versions for use with definitions **)
+
+val [rew] = goal Bin.thy
+    "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Plus) = a";
+by (rewtac rew);
+by (rtac bin_rec_Plus 1);
+val def_bin_rec_Plus = result();
+
+val [rew] = goal Bin.thy
+    "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Minus) = b";
+by (rewtac rew);
+by (rtac bin_rec_Minus 1);
+val def_bin_rec_Minus = result();
+
+val [rew] = goal Bin.thy
+    "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(w$$x) = h(w,x,j(w))";
+by (rewtac rew);
+by (rtac bin_rec_Bcons 1);
+val def_bin_rec_Bcons = result();
+
+fun bin_recs def = map standard
+	([def] RL [def_bin_rec_Plus, def_bin_rec_Minus, def_bin_rec_Bcons]);
+
+(** Type checking **)
+
+val bin_typechecks0 = bin_rec_type :: bin.intrs;
+
+goalw Bin.thy [integ_of_bin_def]
+    "!!w. w: bin ==> integ_of_bin(w) : integ";
+by (typechk_tac (bin_typechecks0@integ_typechecks@
+		 nat_typechecks@[bool_into_nat]));
+val integ_of_bin_type = result();
+
+goalw Bin.thy [bin_succ_def]
+    "!!w. w: bin ==> bin_succ(w) : bin";
+by (typechk_tac (bin_typechecks0@bool_typechecks));
+val bin_succ_type = result();
+
+goalw Bin.thy [bin_pred_def]
+    "!!w. w: bin ==> bin_pred(w) : bin";
+by (typechk_tac (bin_typechecks0@bool_typechecks));
+val bin_pred_type = result();
+
+goalw Bin.thy [bin_minus_def]
+    "!!w. w: bin ==> bin_minus(w) : bin";
+by (typechk_tac ([bin_pred_type]@bin_typechecks0@bool_typechecks));
+val bin_minus_type = result();
+
+goalw Bin.thy [bin_add_def]
+    "!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin";
+by (typechk_tac ([bin_succ_type,bin_pred_type]@bin_typechecks0@
+		 bool_typechecks@ZF_typechecks));
+val bin_add_type = result();
+
+goalw Bin.thy [bin_mult_def]
+    "!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
+by (typechk_tac ([bin_minus_type,bin_add_type]@bin_typechecks0@
+		 bool_typechecks));
+val bin_mult_type = result();
+
+val bin_typechecks = bin_typechecks0 @
+    [integ_of_bin_type, bin_succ_type, bin_pred_type, 
+     bin_minus_type, bin_add_type, bin_mult_type];
+
+val bin_ss = integ_ss 
+    addsimps([bool_1I, bool_0I,
+	     bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ 
+	     bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
+
+val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
+                 [bool_subset_nat RS subsetD];
+
+(**** The carry/borrow functions, bin_succ and bin_pred ****)
+
+(** Lemmas **)
+
+goal Integ.thy 
+    "!!z v. [| z $+ v = z' $+ v';  \
+\       z: integ; z': integ;  v: integ; v': integ;  w: integ |]   \
+\    ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
+by (asm_simp_tac (integ_ss addsimps ([zadd_assoc RS sym])) 1);
+val zadd_assoc_cong = result();
+
+goal Integ.thy 
+    "!!z v w. [| z: integ;  v: integ;  w: integ |]   \
+\    ==> z $+ (v $+ w) = v $+ (z $+ w)";
+by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
+val zadd_assoc_swap = result();
+
+val zadd_cong = 
+    read_instantiate_sg (sign_of Integ.thy) [("t","op $+")] subst_context2;
+
+val zadd_kill = (refl RS zadd_cong);
+val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
+
+(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
+val zadd_assoc_znat = standard (znat_type RS zadd_assoc_swap);
+
+goal Integ.thy 
+    "!!z w. [| z: integ;  w: integ |]   \
+\    ==> w $+ (z $+ (w $+ z)) = w $+ (w $+ (z $+ z))";
+by (REPEAT (ares_tac [zadd_kill, zadd_assoc_swap] 1));
+val zadd_swap_pairs = result();
+
+
+val carry_ss = bin_ss addsimps 
+               (bin_recs bin_succ_def @ bin_recs bin_pred_def);
+
+goal Bin.thy
+    "!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
+by (etac boolE 1);
+by (ALLGOALS (asm_simp_tac (carry_ss addsimps [zadd_assoc])));
+by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1));
+val integ_of_bin_succ = result();
+
+goal Bin.thy
+    "!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
+by (etac boolE 1);
+by (ALLGOALS 
+    (asm_simp_tac 
+     (carry_ss addsimps [zadd_assoc RS sym,
+			zadd_zminus_inverse, zadd_zminus_inverse2])));
+by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1));
+val integ_of_bin_pred = result();
+
+(*These two results replace the definitions of bin_succ and bin_pred*)
+
+
+(*** bin_minus: (unary!) negation of binary integers ***)
+
+val bin_minus_ss =
+    bin_ss addsimps (bin_recs bin_minus_def @
+		    [integ_of_bin_succ, integ_of_bin_pred]);
+
+goal Bin.thy
+    "!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac (bin_minus_ss addsimps [zminus_0]) 1);
+by (simp_tac (bin_minus_ss addsimps [zadd_0_right]) 1);
+by (etac boolE 1);
+by (ALLGOALS 
+    (asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc])));
+val integ_of_bin_minus = result();
+
+
+(*** bin_add: binary addition ***)
+
+goalw Bin.thy [bin_add_def] "!!w. w: bin ==> bin_add(Plus,w) = w";
+by (asm_simp_tac bin_ss 1);
+val bin_add_Plus = result();
+
+goalw Bin.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)";
+by (asm_simp_tac bin_ss 1);
+val bin_add_Minus = result();
+
+goalw Bin.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x";
+by (simp_tac bin_ss 1);
+val bin_add_Bcons_Plus = result();
+
+goalw Bin.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)";
+by (simp_tac bin_ss 1);
+val bin_add_Bcons_Minus = result();
+
+goalw Bin.thy [bin_add_def]
+    "!!w y. [| w: bin;  y: bool |] ==> \
+\           bin_add(v$$x, w$$y) = \
+\           bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
+by (asm_simp_tac bin_ss 1);
+val bin_add_Bcons_Bcons = result();
+
+val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
+		    bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
+		    integ_of_bin_succ, integ_of_bin_pred];
+
+val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews);
+
+goal Bin.thy
+    "!!v. v: bin ==> \
+\         ALL w: bin. integ_of_bin(bin_add(v,w)) = \
+\                     integ_of_bin(v) $+ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac bin_add_ss 1);
+by (simp_tac bin_add_ss 1);
+by (rtac ballI 1);
+by (bin_ind_tac "wa" [] 1);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1);
+by (asm_simp_tac bin_add_ss 1);
+by (REPEAT (ares_tac (zadd_commute::typechecks) 1));
+by (etac boolE 1);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2);
+by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2));
+by (etac boolE 1);
+by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs])));
+by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
+		      typechecks) 1));
+val integ_of_bin_add_lemma = result();
+
+val integ_of_bin_add = integ_of_bin_add_lemma RS bspec;
+
+
+(*** bin_add: binary multiplication ***)
+
+val bin_mult_ss =
+    bin_ss addsimps (bin_recs bin_mult_def @ 
+		       [integ_of_bin_minus, integ_of_bin_add]);
+
+
+val major::prems = goal Bin.thy
+    "[| v: bin; w: bin |] ==>	\
+\    integ_of_bin(bin_mult(v,w)) = \
+\    integ_of_bin(v) $* integ_of_bin(w)";
+by (cut_facts_tac prems 1);
+by (bin_ind_tac "v" [major] 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1);
+by (etac boolE 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2);
+by (asm_simp_tac 
+    (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
+by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
+		      typechecks) 1));
+val integ_of_bin_mult = result();
+
+(**** Computations ****)
+
+(** extra rules for bin_succ, bin_pred **)
+
+val [bin_succ_Plus, bin_succ_Minus, _] = bin_recs bin_succ_def;
+val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
+
+goal Bin.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
+by (simp_tac carry_ss 1);
+val bin_succ_Bcons1 = result();
+
+goal Bin.thy "bin_succ(w$$0) = w$$1";
+by (simp_tac carry_ss 1);
+val bin_succ_Bcons0 = result();
+
+goal Bin.thy "bin_pred(w$$1) = w$$0";
+by (simp_tac carry_ss 1);
+val bin_pred_Bcons1 = result();
+
+goal Bin.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
+by (simp_tac carry_ss 1);
+val bin_pred_Bcons0 = result();
+
+(** extra rules for bin_minus **)
+
+val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
+
+goal Bin.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
+by (simp_tac bin_minus_ss 1);
+val bin_minus_Bcons1 = result();
+
+goal Bin.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
+by (simp_tac bin_minus_ss 1);
+val bin_minus_Bcons0 = result();
+
+(** extra rules for bin_add **)
+
+goal Bin.thy 
+    "!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
+by (asm_simp_tac bin_add_ss 1);
+val bin_add_Bcons_Bcons11 = result();
+
+goal Bin.thy 
+    "!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
+by (asm_simp_tac bin_add_ss 1);
+val bin_add_Bcons_Bcons10 = result();
+
+goal Bin.thy 
+    "!!w y.[| w: bin;  y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
+by (asm_simp_tac bin_add_ss 1);
+val bin_add_Bcons_Bcons0 = result();
+
+(** extra rules for bin_mult **)
+
+val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
+
+goal Bin.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
+by (simp_tac bin_mult_ss 1);
+val bin_mult_Bcons1 = result();
+
+goal Bin.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
+by (simp_tac bin_mult_ss 1);
+val bin_mult_Bcons0 = result();
+
+
+(*** The computation simpset ***)
+
+val bin_comp_ss = integ_ss 
+    addsimps [bin_succ_Plus, bin_succ_Minus,
+	     bin_succ_Bcons1, bin_succ_Bcons0,
+	     bin_pred_Plus, bin_pred_Minus,
+	     bin_pred_Bcons1, bin_pred_Bcons0,
+	     bin_minus_Plus, bin_minus_Minus,
+	     bin_minus_Bcons1, bin_minus_Bcons0,
+	     bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, 
+	     bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, 
+	     bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
+	     bin_mult_Plus, bin_mult_Minus,
+	     bin_mult_Bcons1, bin_mult_Bcons0]
+    setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
+
+(*** Examples of performing binary arithmetic by simplification ***)
+
+proof_timing := true;
+(*All runtimes below are on a SPARCserver 10*)
+
+(* 13+19 = 32 *)
+goal Bin.thy
+    "bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0";
+by (simp_tac bin_comp_ss 1);	(*0.6 secs*)
+result();
+
+bin_add(binary_of_int 13, binary_of_int 19);
+
+(* 1234+5678 = 6912 *)
+goal Bin.thy
+    "bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \
+\	     Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \
+\    Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0";
+by (simp_tac bin_comp_ss 1);	(*2.6 secs*)
+result();
+
+bin_add(binary_of_int 1234, binary_of_int 5678);
+
+(* 1359-2468 = ~1109 *)
+goal Bin.thy
+    "bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1,		\
+\	     Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = 	\
+\    Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1";
+by (simp_tac bin_comp_ss 1);	(*2.3 secs*)
+result();
+
+bin_add(binary_of_int 1359, binary_of_int ~2468);
+
+(* 93746-46375 = 47371 *)
+goal Bin.thy
+    "bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \
+\	     Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \
+\    Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1";
+by (simp_tac bin_comp_ss 1);	(*3.9 secs*)
+result();
+
+bin_add(binary_of_int 93746, binary_of_int ~46375);
+
+(* negation of 65745 *)
+goal Bin.thy
+    "bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \
+\    Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1";
+by (simp_tac bin_comp_ss 1);	(*0.6 secs*)
+result();
+
+bin_minus(binary_of_int 65745);
+
+(* negation of ~54321 *)
+goal Bin.thy
+    "bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \
+\    Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1";
+by (simp_tac bin_comp_ss 1);	(*0.7 secs*)
+result();
+
+bin_minus(binary_of_int ~54321);
+
+(* 13*19 = 247 *)
+goal Bin.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \
+\               Plus$$1$$1$$1$$1$$0$$1$$1$$1";
+by (simp_tac bin_comp_ss 1);	(*1.5 secs*)
+result();
+
+bin_mult(binary_of_int 13, binary_of_int 19);
+
+(* ~84 * 51 = ~4284 *)
+goal Bin.thy
+    "bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \
+\    Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0";
+by (simp_tac bin_comp_ss 1);	(*2.6 secs*)
+result();
+
+bin_mult(binary_of_int ~84, binary_of_int 51);
+
+(* 255*255 = 65025;  the worst case for 8-bit operands *)
+goal Bin.thy
+    "bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \
+\             Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \
+\        Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1";
+by (simp_tac bin_comp_ss 1);	(*9.8 secs*)
+result();
+
+bin_mult(binary_of_int 255, binary_of_int 255);
+
+(* 1359 * ~2468 = ~3354012 *)
+goal Bin.thy
+    "bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, 		\
+\	      Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = 	\
+\    Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0";
+by (simp_tac bin_comp_ss 1);	(*13.7 secs*)
+result();
+
+bin_mult(binary_of_int 1359, binary_of_int ~2468);
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Bin.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Bin.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,60 @@
+(*  Title: 	ZF/ex/Bin.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Arithmetic on binary integers.
+*)
+
+Bin = Integ + Univ + 
+consts
+  bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
+  integ_of_bin     :: "i=>i"
+  bin_succ         :: "i=>i"
+  bin_pred         :: "i=>i"
+  bin_minus        :: "i=>i"
+  bin_add,bin_mult :: "[i,i]=>i"
+
+  bin		   :: "i"
+
+datatype
+  "bin" = Plus
+        | Minus
+        | "$$" ("w: bin", "b: bool")    (infixl 60)
+  type_intrs "[bool_into_univ]"
+  
+rules
+
+  bin_rec_def
+      "bin_rec(z,a,b,h) == \
+\      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
+
+  integ_of_bin_def 
+      "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
+
+  bin_succ_def
+      "bin_succ(w0) == bin_rec(w0, Plus$$1, Plus, %w x r. cond(x, r$$0, w$$1))"
+
+  bin_pred_def
+      "bin_pred(w0) == \
+\	bin_rec(w0, Minus, Minus$$0, %w x r. cond(x, w$$0, r$$1))"
+
+  bin_minus_def
+      "bin_minus(w0) == \
+\	bin_rec(w0, Plus, Plus$$1, %w x r. cond(x, bin_pred(r$$0), r$$0))"
+
+  bin_add_def
+      "bin_add(v0,w0) == 			\
+\       bin_rec(v0, 				\
+\         lam w:bin. w,       		\
+\         lam w:bin. bin_pred(w),	\
+\         %v x r. lam w1:bin. 		\
+\	           bin_rec(w1, v$$x, bin_pred(v$$x),	\
+\		     %w y s. (r`cond(x and y, bin_succ(w), w)) \
+\		             $$ (x xor y)))    ` w0"
+
+  bin_mult_def
+      "bin_mult(v0,w) == 			\
+\       bin_rec(v0, Plus, bin_minus(w),		\
+\         %v x r. cond(x, bin_add(r$$0,w), r$$0))"
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Brouwer.ML
--- a/src/ZF/ex/Brouwer.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Brouwer.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -6,28 +6,16 @@
 Datatype definition of the Brouwer ordinals -- demonstrates infinite branching
 *)
 
-structure Brouwer = Datatype_Fun
- (val thy	= InfDatatype.thy;
-  val thy_name 	= "Brouwer";
-  val rec_specs = [("brouwer", "Vfrom(0, csucc(nat))",
-		    [(["Zero"], "i", NoSyn), 
-		     (["Suc","Lim"], "i=>i", NoSyn)])];
-  val rec_styp 	= "i";
-  val sintrs 	= ["Zero : brouwer",
-		   "b: brouwer ==> Suc(b): brouwer",
-	           "h: nat -> brouwer ==> Lim(h) : brouwer"];
-  val monos 	 = [Pi_mono];
-  val type_intrs = inf_datatype_intrs;
-  val type_elims = []);
-
-val [ZeroI, SucI, LimI] = Brouwer.intrs;
+open Brouwer;
 
 goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
-by (rtac (Brouwer.unfold RS trans) 1);
-bws Brouwer.con_defs;
-by (fast_tac (sum_cs addIs ([equalityI] @ inf_datatype_intrs)
- 	             addDs [Brouwer.dom_subset RS subsetD]
- 	             addEs [A_into_Vfrom, fun_into_Vfrom_csucc]) 1);
+by (rtac (brouwer.unfold RS trans) 1);
+bws brouwer.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+by (fast_tac (sum_cs addIs inf_datatype_intrs
+ 	             addDs [brouwer.dom_subset RS subsetD]
+ 	             addEs [fun_into_Vcsucc]) 1);
 val brouwer_unfold = result();
 
 (*A nicer induction rule than the standard one*)
@@ -38,7 +26,7 @@
 \	!!h. [| h: nat -> brouwer;  ALL i:nat. P(h`i)	\
 \            |] ==> P(Lim(h))				\
 \    |] ==> P(b)";
-by (rtac (major RS Brouwer.induct) 1);
+by (rtac (major RS brouwer.induct) 1);
 by (REPEAT_SOME (ares_tac prems));
 by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
 by (fast_tac (ZF_cs addDs [apply_type]) 1);
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Brouwer.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Brouwer.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,18 @@
+(*  Title: 	ZF/ex/Brouwer.thy
+    ID:         $ $
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Datatype definition of the Brouwer ordinals -- demonstrates infinite branching
+*)
+
+Brouwer = InfDatatype +
+consts
+  brouwer :: "i"
+ 
+datatype <= "Vfrom(0, csucc(nat))"
+  "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
+  monos	      "[Pi_mono]"
+  type_intrs  "inf_datatype_intrs"
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/CoUnit.ML
--- a/src/ZF/ex/CoUnit.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/CoUnit.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -1,105 +1,75 @@
-(*  Title: 	ZF/ex/counit.ML
+(*  Title: 	ZF/ex/CoUnit.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Trivial codatatype definitions, one of which goes wrong!
 
-Need to find sufficient conditions for codatatypes to work correctly!
+See discussion in 
+  L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
+  Report 334,  Cambridge University Computer Laboratory.  1994.
 *)
 
-(*This degenerate definition does not work well because the one constructor's
-  definition is trivial!  The same thing occurs with Aczel's Special Final
-  Coalgebra Theorem
-*)
-structure CoUnit = CoDatatype_Fun
- (val thy = QUniv.thy;
-  val thy_name = "CoUnit";
-  val rec_specs = 
-      [("counit", "quniv(0)",
-	  [(["Con"],	"i=>i", NoSyn)])];
-  val rec_styp = "i";
-  val sintrs = ["x: counit ==> Con(x) : counit"];
-  val monos = [];
-  val type_intrs = codatatype_intrs
-  val type_elims = codatatype_elims);
+open CoUnit;
   
-val [ConI] = CoUnit.intrs;
-
 (*USELESS because folding on Con(?xa) == ?xa fails*)
-val ConE = CoUnit.mk_cases CoUnit.con_defs "Con(x) : counit";
+val ConE = counit.mk_cases counit.con_defs "Con(x) : counit";
 
 (*Proving freeness results*)
-val Con_iff = CoUnit.mk_free "Con(x)=Con(y) <-> x=y";
+val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
 
 (*Should be a singleton, not everything!*)
 goal CoUnit.thy "counit = quniv(0)";
-by (rtac (CoUnit.dom_subset RS equalityI) 1);
+by (rtac (counit.dom_subset RS equalityI) 1);
 by (rtac subsetI 1);
-by (etac CoUnit.coinduct 1);
+by (etac counit.coinduct 1);
 by (rtac subset_refl 1);
-by (rewrite_goals_tac CoUnit.con_defs);
+by (rewrite_goals_tac counit.con_defs);
 by (fast_tac ZF_cs 1);
 val counit_eq_univ = result();
 
 
-(*****************************************************************)
-
 (*A similar example, but the constructor is non-degenerate and it works!
   The resulting set is a singleton.
 *)
 
-structure CoUnit2 = CoDatatype_Fun
- (val thy = QUniv.thy;
-  val thy_name = "CoUnit2";
-  val rec_specs = 
-      [("counit2", "quniv(0)",
-	  [(["Con2"],	"[i,i]=>i", NoSyn)])];
-  val rec_styp = "i";
-  val sintrs = ["[| x: counit2;  y: counit2 |] ==> Con2(x,y) : counit2"];
-  val monos = [];
-  val type_intrs = codatatype_intrs
-  val type_elims = codatatype_elims);
-
-val [Con2I] = CoUnit2.intrs;
-
-val Con2E = CoUnit2.mk_cases CoUnit2.con_defs "Con2(x,y) : counit2";
+val Con2E = counit2.mk_cases counit2.con_defs "Con2(x,y) : counit2";
 
 (*Proving freeness results*)
-val Con2_iff = CoUnit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
+val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
 
-goalw CoUnit2.thy CoUnit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
+goalw CoUnit.thy counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
 by (rtac bnd_monoI 1);
 by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
 val Con2_bnd_mono = result();
 
-goal CoUnit2.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
-by (rtac (singletonI RS CoUnit2.coinduct) 1);
+goal CoUnit.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
+by (rtac (singletonI RS counit2.coinduct) 1);
 by (rtac (qunivI RS singleton_subsetI) 1);
 by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
 by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
 val lfp_Con2_in_counit2 = result();
 
 (*Lemma for proving finality.  Borrowed from ex/llist_eq.ML!*)
-goal CoUnit2.thy
+goal CoUnit.thy
     "!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
 by (etac trans_induct 1);
 by (safe_tac subset_cs);
-by (etac CoUnit2.elim 1);
-by (etac CoUnit2.elim 1);
-by (rewrite_goals_tac CoUnit2.con_defs);
+by (etac counit2.elim 1);
+by (etac counit2.elim 1);
+by (rewrite_goals_tac counit2.con_defs);
 by (fast_tac lleq_cs 1);
 val counit2_Int_Vset_subset_lemma = result();
 
 val counit2_Int_Vset_subset = standard
 	(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
 
-goal CoUnit2.thy "!!x y. [| x: counit2;  y: counit2 |] ==> x=y";
+goal CoUnit.thy "!!x y. [| x: counit2;  y: counit2 |] ==> x=y";
 by (rtac equalityI 1);
 by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
 val counit2_implies_equal = result();
 
-goal CoUnit2.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
+goal CoUnit.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
 by (rtac equalityI 1);
 by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);
 by (rtac subsetI 1);
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/CoUnit.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/CoUnit.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,34 @@
+(*  Title: 	ZF/ex/CoUnit.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Trivial codatatype definitions, one of which goes wrong!
+
+See discussion in 
+  L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
+  Report 334,  Cambridge University Computer Laboratory.  1994.
+*)
+
+CoUnit = QUniv + "Datatype" +
+
+(*This degenerate definition does not work well because the one constructor's
+  definition is trivial!  The same thing occurs with Aczel's Special Final
+  Coalgebra Theorem
+*)
+consts
+  counit :: "i"
+codatatype
+  "counit" = Con ("x: counit")
+
+
+(*A similar example, but the constructor is non-degenerate and it works!
+  The resulting set is a singleton.
+*)
+
+consts
+  counit2 :: "i"
+codatatype
+  "counit2" = Con2 ("x: counit2", "y: counit2")
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Comb.ML
--- a/src/ZF/ex/Comb.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Comb.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -3,32 +3,234 @@
     Author: 	Lawrence C Paulson
     Copyright   1993  University of Cambridge
 
-Datatype definition of combinators S and K
+Combinatory Logic example: the Church-Rosser Theorem
+Curiously, combinators do not include free variables.
+
+Example taken from
+    J. Camilleri and T. F. Melham.
+    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
+    Report 265, University of Cambridge Computer Laboratory, 1992.
+
+HOL system proofs may be found in
+/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
+*)
+
+open Comb;
+
+val [_,_,comb_Ap] = comb.intrs;
+val Ap_E = comb.mk_cases comb.con_defs "p#q : comb";
+
+
+(*** Results about Contraction ***)
+
+val contract_induct = standard
+    (contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+
+(*For type checking: replaces a-1->b by a,b:comb *)
+val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
+val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
+val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
+
+goal Comb.thy "field(contract) = comb";
+by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
+val field_contract_eq = result();
+
+val reduction_refl = standard
+    (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
+
+val rtrancl_into_rtrancl2 = standard
+    (r_into_rtrancl RS (trans_rtrancl RS transD));
+
+val reduction_rls = [reduction_refl, contract.K, contract.S, 
+		     contract.K RS rtrancl_into_rtrancl2,
+		     contract.S RS rtrancl_into_rtrancl2,
+		     contract.Ap1 RS rtrancl_into_rtrancl2,
+		     contract.Ap2 RS rtrancl_into_rtrancl2];
+
+(*Example only: not used*)
+goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p";
+by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1));
+val reduce_I = result();
+
+goalw Comb.thy [I_def] "I: comb";
+by (REPEAT (ares_tac comb.intrs 1));
+val comb_I = result();
+
+(** Non-contraction results **)
 
-J. Camilleri and T. F. Melham.
-Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
-Report 265, University of Cambridge Computer Laboratory, 1992.
-*)
+(*Derive a case for each combinator constructor*)
+val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
+val S_contractE = contract.mk_cases comb.con_defs "S -1-> r";
+val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r";
+
+val contract_cs =
+    ZF_cs addSIs comb.intrs
+	  addIs  contract.intrs
+	  addSEs [contract_combD1,contract_combD2]     (*type checking*)
+	  addSEs [K_contractE, S_contractE, Ap_contractE]
+	  addSEs comb.free_SEs;
+
+goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
+by (fast_tac contract_cs 1);
+val I_contract_E = result();
+
+goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
+by (fast_tac contract_cs 1);
+val K1_contractD = result();
+
+goal Comb.thy "!!p r. [| p ---> q;  r: comb |] ==> p#r ---> q#r";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+val Ap_reduce1 = result();
+
+goal Comb.thy "!!p r. [| p ---> q;  r: comb |] ==> r#p ---> r#q";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+val Ap_reduce2 = result();
+
+(** Counterexample to the diamond property for -1-> **)
+
+goal Comb.thy "K#I#(I#I) -1-> I";
+by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
+val KIII_contract1 = result();
+
+goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
+by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
+val KIII_contract2 = result();
+
+goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
+by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
+val KIII_contract3 = result();
+
+goalw Comb.thy [diamond_def] "~ diamond(contract)";
+by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
+                    addSEs [I_contract_E]) 1);
+val not_diamond_contract = result();
+
 
 
-(*Example of a datatype with mixfix syntax for some constructors*)
-structure Comb = Datatype_Fun
- (val thy = Univ.thy;
-  val thy_name = "Comb";
-  val rec_specs = 
-      [("comb", "univ(0)",
-	  [(["K","S"],	"i", 		NoSyn),
-	   (["#"],	"[i,i]=>i", 	Infixl 90)])];
-  val rec_styp = "i";
-  val sintrs = 
-	  ["K : comb",
-	   "S : comb",
-	   "[| p: comb;  q: comb |] ==> p#q : comb"];
-  val monos = [];
-  val type_intrs = datatype_intrs;
-  val type_elims = []);
+(*** Results about Parallel Contraction ***)
+
+val parcontract_induct = standard
+    (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+
+(*For type checking: replaces a=1=>b by a,b:comb *)
+val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
+val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
+val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
+
+goal Comb.thy "field(parcontract) = comb";
+by (fast_tac (ZF_cs addIs [equalityI, parcontract.K] 
+	            addSEs [parcontract_combE2]) 1);
+val field_parcontract_eq = result();
+
+(*Derive a case for each combinator constructor*)
+val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
+val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r";
+val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r";
+
+val parcontract_cs =
+    ZF_cs addSIs comb.intrs
+	  addIs  parcontract.intrs
+	  addSEs [Ap_E, K_parcontractE, S_parcontractE, 
+		  Ap_parcontractE]
+	  addSEs [parcontract_combD1, parcontract_combD2]     (*type checking*)
+          addSEs comb.free_SEs;
+
+(*** Basic properties of parallel contraction ***)
+
+goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
+by (fast_tac parcontract_cs 1);
+val K1_parcontractD = result();
+
+goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
+by (fast_tac parcontract_cs 1);
+val S1_parcontractD = result();
+
+goal Comb.thy
+ "!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
+by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
+val S2_parcontractD = result();
+
+(*Church-Rosser property for parallel contraction*)
+goalw Comb.thy [diamond_def] "diamond(parcontract)";
+by (rtac (impI RS allI RS allI) 1);
+by (etac parcontract_induct 1);
+by (ALLGOALS 
+    (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
+val diamond_parcontract = result();
+
+(*** Transitive closure preserves the Church-Rosser property ***)
 
-val [K_comb,S_comb,Ap_comb] = Comb.intrs;
+goalw Comb.thy [diamond_def]
+    "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
+\    ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
+by (etac trancl_induct 1);
+by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
+by (slow_best_tac (ZF_cs addSDs [spec RS mp]
+		         addIs  [r_into_trancl, trans_trancl RS transD]) 1);
+val diamond_trancl_lemma = result();
+
+val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
+
+val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
+bw diamond_def;  (*unfold only in goal, not in premise!*)
+by (rtac (impI RS allI RS allI) 1);
+by (etac trancl_induct 1);
+by (ALLGOALS
+    (slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
+		          addEs [major RS diamond_lemmaE])));
+val diamond_trancl = result();
+
+
+(*** Equivalence of p--->q and p===>q ***)
+
+goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
+by (etac contract_induct 1);
+by (ALLGOALS (fast_tac (parcontract_cs)));
+val contract_imp_parcontract = result();
 
-val Ap_E = Comb.mk_cases Comb.con_defs "p#q : comb";
+goal Comb.thy "!!p q. p--->q ==> p===>q";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (fast_tac (parcontract_cs addIs [r_into_trancl]) 1);
+by (fast_tac (ZF_cs addIs [contract_imp_parcontract, 
+			   r_into_trancl, trans_trancl RS transD]) 1);
+val reduce_imp_parreduce = result();
+
 
+goal Comb.thy "!!p q. p=1=>q ==> p--->q";
+by (etac parcontract_induct 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (rtac (trans_rtrancl RS transD) 1);
+by (ALLGOALS 
+    (fast_tac 
+     (contract_cs addIs [Ap_reduce1, Ap_reduce2]
+                  addSEs [parcontract_combD1,parcontract_combD2])));
+val parcontract_imp_reduce = result();
+
+goal Comb.thy "!!p q. p===>q ==> p--->q";
+by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1);
+by (etac trancl_induct 1);
+by (etac parcontract_imp_reduce 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (etac parcontract_imp_reduce 1);
+val parreduce_imp_reduce = result();
+
+goal Comb.thy "p===>q <-> p--->q";
+by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
+val parreduce_iff_reduce = result();
+
+writeln"Reached end of file.";
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Comb.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Comb.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,82 @@
+(*  Title: 	ZF/ex/Comb.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson
+    Copyright   1994  University of Cambridge
+
+Combinatory Logic example: the Church-Rosser Theorem
+Curiously, combinators do not include free variables.
+
+Example taken from
+    J. Camilleri and T. F. Melham.
+    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
+    Report 265, University of Cambridge Computer Laboratory, 1992.
+*)
+
+
+Comb = Univ + "Datatype" +
+
+(** Datatype definition of combinators S and K, with infixed application **)
+consts comb :: "i"
+datatype (* <= "univ(0)" *)
+  "comb" = K
+         | S
+         | "#" ("p: comb", "q: comb")   (infixl 90)
+
+(** Inductive definition of contractions, -1->
+             and (multi-step) reductions, --->
+**)
+consts
+  contract  :: "i"
+  "-1->"    :: "[i,i] => o"    			(infixl 50)
+  "--->"    :: "[i,i] => o"    			(infixl 50)
+
+translations
+  "p -1-> q" == "<p,q> : contract"
+  "p ---> q" == "<p,q> : contract^*"
+
+inductive
+  domains   "contract" <= "comb*comb"
+  intrs
+    K     "[| p:comb;  q:comb |] ==> K#p#q -1-> p"
+    S     "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
+    Ap1   "[| p-1->q;  r:comb |] ==> p#r -1-> q#r"
+    Ap2   "[| p-1->q;  r:comb |] ==> r#p -1-> r#q"
+  type_intrs "comb.intrs"
+
+
+(** Inductive definition of parallel contractions, =1=>
+             and (multi-step) parallel reductions, ===>
+**)
+consts
+  parcontract :: "i"
+  "=1=>"    :: "[i,i] => o"    			(infixl 50)
+  "===>"    :: "[i,i] => o"    			(infixl 50)
+
+translations
+  "p =1=> q" == "<p,q> : parcontract"
+  "p ===> q" == "<p,q> : parcontract^+"
+
+inductive
+  domains   "parcontract" <= "comb*comb"
+  intrs
+    refl  "[| p:comb |] ==> p =1=> p"
+    K     "[| p:comb;  q:comb |] ==> K#p#q =1=> p"
+    S     "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
+    Ap    "[| p=1=>q;  r=1=>s |] ==> p#r =1=> q#s"
+  type_intrs "comb.intrs"
+
+
+(*Misc definitions*)
+consts
+  diamond   :: "i => o"
+  I         :: "i"
+
+rules
+
+  diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
+\                            (ALL y'. <x,y'>:r --> \
+\                                 (EX z. <y,z>:r & <y',z> : r))"
+
+  I_def       "I == S#K#K"
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Data.ML
--- a/src/ZF/ex/Data.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Data.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	ZF/ex/data.ML
+(*  Title: 	ZF/ex/Data.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -7,34 +7,29 @@
 It has four contructors, of arities 0-3, and two parameters A and B.
 *)
 
-structure Data = Datatype_Fun
- (val thy        = Univ.thy
-  val thy_name 	 = "Data"
-  val rec_specs  = [("data", "univ(A Un B)",
-                       [(["Con0"],   "i",	    NoSyn),
-                        (["Con1"],   "i=>i",	    NoSyn),
-                        (["Con2"],   "[i,i]=>i",    NoSyn),
-                        (["Con3"],   "[i,i,i]=>i",  NoSyn)])]
-  val rec_styp   = "[i,i]=>i"
-  val sintrs     = 
-          ["Con0 : data(A,B)",
-           "[| a: A |] ==> Con1(a) : data(A,B)",
-           "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
-           "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
-  val monos      = []
-  val type_intrs = datatype_intrs
-  val type_elims = datatype_elims);
+open Data;
 
+goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
+by (rtac (data.unfold RS trans) 1);
+bws data.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+(*for this direction, fast_tac is just too slow!*)
+by (safe_tac sum_cs);
+by (REPEAT_FIRST (swap_res_tac [refl, conjI, disjCI, exI]));
+by (REPEAT (fast_tac (sum_cs addIs datatype_intrs
+  		             addDs [data.dom_subset RS subsetD]) 1));
+val data_unfold = result();
 
 (**  Lemmas to justify using "data" in other recursive type definitions **)
 
-goalw Data.thy Data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
+goalw Data.thy data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
 by (rtac lfp_mono 1);
-by (REPEAT (rtac Data.bnd_mono 1));
+by (REPEAT (rtac data.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
 val data_mono = result();
 
-goalw Data.thy (Data.defs@Data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
+goalw Data.thy (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Data.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Data.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,21 @@
+(*  Title: 	ZF/ex/Data.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Sample datatype definition.  
+It has four contructors, of arities 0-3, and two parameters A and B.
+*)
+
+Data = Univ +
+
+consts
+  data :: "[i,i] => i"
+
+datatype
+  "data(A,B)" = Con0
+              | Con1 ("a: A")
+              | Con2 ("a: A", "b: B")
+              | Con3 ("a: A", "b: B", "d: data(A,B)")
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Enum.ML
--- a/src/ZF/ex/Enum.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Enum.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	ZF/ex/enum
+(*  Title: 	ZF/ex/Enum
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -8,26 +8,9 @@
 Can go up to at least 100 constructors, but it takes nearly 7 minutes...
 *)
 
-
-(*An enumeration type with 60 contructors!  -- takes about 150 seconds!*)
-fun mk_ids a 0 = []
-  | mk_ids a n = a :: mk_ids (bump_string a) (n-1);
-
-val consts = mk_ids "con1" 60;
+open Enum;
 
-structure Enum = Datatype_Fun
- (val thy = Univ.thy;
-  val thy_name = "Enum";
-  val rec_specs = 
-      [("enum", "univ(0)",
-	  [(consts, "i", NoSyn)])];
-  val rec_styp = "i";
-  val sintrs = map (fn const => const ^ " : enum") consts;
-  val monos = [];
-  val type_intrs = datatype_intrs
-  val type_elims = []);
-
-goal Enum.thy "con59 ~= con60";
-by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
+goal Enum.thy "C00 ~= C01";
+by (simp_tac (ZF_ss addsimps enum.free_iffs) 1);
 result();
 
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Enum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Enum.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,24 @@
+(*  Title: 	ZF/ex/Enum
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Example of a BIG enumeration type
+
+Can go up to at least 100 constructors, but it takes nearly 7 minutes...
+*)
+
+Enum = Univ + "Datatype" + 
+
+consts
+  enum :: "i"
+
+datatype
+  "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
+         | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
+         | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
+         | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
+         | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
+         | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
+  
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Equiv.ML
--- a/src/ZF/ex/Equiv.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Equiv.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -46,14 +46,15 @@
 (** Equivalence classes **)
 
 (*Lemma for the next result*)
-goalw Equiv.thy [equiv_def,trans_def,sym_def]
-    "!!A r. [| equiv(A,r);  <a,b>: r |] ==> r``{a} <= r``{b}";
+goalw Equiv.thy [trans_def,sym_def]
+    "!!A r. [| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}";
 by (fast_tac ZF_cs 1);
 val equiv_class_subset = result();
 
-goal Equiv.thy "!!A r. [| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}";
-by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
-by (rewrite_goals_tac [equiv_def,sym_def]);
+goalw Equiv.thy [equiv_def]
+    "!!A r. [| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}";
+by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
+by (rewrite_goals_tac [sym_def]);
 by (fast_tac ZF_cs 1);
 val equiv_class_eq = result();
 
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/LList.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -1,47 +1,35 @@
-(*  Title: 	ZF/ex/llist.ML
+(*  Title: 	ZF/ex/LList.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Codatatype definition of Lazy Lists
 *)
 
-structure LList = CoDatatype_Fun
- (val thy        = QUniv.thy
-  val thy_name   = "LList"
-  val rec_specs  = [("llist", "quniv(A)",
-                      [(["LNil"],   "i",	NoSyn), 
-                       (["LCons"],  "[i,i]=>i",	NoSyn)])]
-  val rec_styp   = "i=>i"
-  val sintrs     = ["LNil : llist(A)",
-                    "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
-  val monos      = []
-  val type_intrs = codatatype_intrs
-  val type_elims = codatatype_elims);
-
-val [LNilI, LConsI] = LList.intrs;
+open LList;
 
 (*An elimination rule, for type-checking*)
-val LConsE = LList.mk_cases LList.con_defs "LCons(a,l) : llist(A)";
+val LConsE = llist.mk_cases llist.con_defs "LCons(a,l) : llist(A)";
 
 (*Proving freeness results*)
-val LCons_iff      = LList.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
-val LNil_LCons_iff = LList.mk_free "~ LNil=LCons(a,l)";
+val LCons_iff      = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
+val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
 
 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
-by (rtac (LList.unfold RS trans) 1);
-bws LList.con_defs;
-by (fast_tac (qsum_cs addIs ([equalityI] @ codatatype_intrs)
-		      addDs [LList.dom_subset RS subsetD]
- 	              addEs [A_into_quniv]
-                      addSEs [QSigmaE]) 1);
+by (rtac (llist.unfold RS trans) 1);
+bws llist.con_defs;
+br equalityI 1;
+by (fast_tac qsum_cs 1);
+by (fast_tac (qsum_cs addIs codatatype_intrs
+		      addDs [llist.dom_subset RS subsetD]
+ 	              addSEs [QSigmaE]) 1);
 val llist_unfold = result();
 
 (*** Lemmas to justify using "llist" in other recursive type definitions ***)
 
-goalw LList.thy LList.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
+goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
 by (rtac gfp_mono 1);
-by (REPEAT (rtac LList.bnd_mono 1));
+by (REPEAT (rtac llist.bnd_mono 1));
 by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
 val llist_mono = result();
 
@@ -58,8 +46,8 @@
    "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
 by (etac trans_induct 1);
 by (rtac ballI 1);
-by (etac LList.elim 1);
-by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
+by (etac llist.elim 1);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
 (*LNil case*)
 by (fast_tac quniv_cs 1);
 (*LCons case*)
@@ -76,5 +64,140 @@
 val llist_subset_quniv = standard
     (llist_mono RS (llist_quniv RSN (2,subset_trans)));
 
-(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow
-   automatic association between theory name and filename. *)
+
+(*** Lazy List Equality: lleq ***)
+
+val lleq_cs = subset_cs
+	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+        addSEs [Ord_in_Ord, Pair_inject];
+
+(*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
+goal LList.thy
+   "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
+by (etac trans_induct 1);
+by (REPEAT (resolve_tac [allI, impI] 1));
+by (etac lleq.elim 1);
+by (rewrite_goals_tac (QInr_def::llist.con_defs));
+by (safe_tac lleq_cs);
+by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
+val lleq_Int_Vset_subset_lemma = result();
+
+val lleq_Int_Vset_subset = standard
+	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
+
+
+(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
+val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
+by (rtac (prem RS converseI RS lleq.coinduct) 1);
+by (rtac (lleq.dom_subset RS converse_type) 1);
+by (safe_tac converse_cs);
+by (etac lleq.elim 1);
+by (ALLGOALS (fast_tac qconverse_cs));
+val lleq_symmetric = result();
+
+goal LList.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
+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();
+
+val [eqprem,lprem] = goal LList.thy
+    "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
+by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] lleq.coinduct 1);
+by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
+by (safe_tac qpair_cs);
+by (etac llist.elim 1);
+by (ALLGOALS (fast_tac pair_cs));
+val equal_llist_implies_leq = result();
+
+
+(*** Lazy List Functions ***)
+
+(*Examples of coinduction for type-checking and to prove llist equations*)
+
+(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
+
+goalw LList.thy llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
+by (rtac bnd_monoI 1);
+by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
+by (REPEAT (ares_tac [subset_refl, A_subset_univ, 
+		      QInr_subset_univ, QPair_subset_univ] 1));
+val lconst_fun_bnd_mono = result();
+
+(* lconst(a) = LCons(a,lconst(a)) *)
+val lconst = standard 
+    ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski);
+
+val lconst_subset = lconst_def RS def_lfp_subset;
+
+val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper);
+
+goal LList.thy "!!a A. a : A ==> lconst(a) : quniv(A)";
+by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
+by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
+val lconst_in_quniv = result();
+
+goal LList.thy "!!a A. a:A ==> lconst(a): llist(A)";
+by (rtac (singletonI RS llist.coinduct) 1);
+by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
+by (fast_tac (ZF_cs addSIs [lconst]) 1);
+val lconst_type = result();
+
+(*** flip --- equations merely assumed; certain consequences proved ***)
+
+val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
+
+goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
+by (fast_tac (quniv_cs addSEs [boolE]) 1);
+val bool_Int_subset_univ = result();
+
+val flip_cs = quniv_cs addSIs [not_type]
+                       addIs  [bool_Int_subset_univ];
+
+(*Reasoning borrowed from lleq.ML; a similar proof works for all
+  "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
+goal LList.thy
+   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
+\                   univ(eclose(bool))";
+by (etac trans_induct 1);
+by (rtac ballI 1);
+by (etac llist.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 2);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
+(*LNil case*)
+by (fast_tac flip_cs 1);
+(*LCons case*)
+by (safe_tac flip_cs);
+by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
+val flip_llist_quniv_lemma = result();
+
+goal LList.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
+by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
+by (REPEAT (assume_tac 1));
+val flip_in_quniv = result();
+
+val [prem] = goal LList.thy "l : llist(bool) ==> flip(l): llist(bool)";
+by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
+       llist.coinduct 1);
+by (rtac (prem RS RepFunI) 1);
+by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
+by (etac RepFunE 1);
+by (etac llist.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_type = result();
+
+val [prem] = goal LList.thy
+    "l : llist(bool) ==> flip(flip(l)) = l";
+by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
+       (lleq.coinduct RS lleq_implies_equal) 1);
+by (rtac (prem RS RepFunI) 1);
+by (fast_tac (ZF_cs addSIs [flip_type]) 1);
+by (etac RepFunE 1);
+by (etac llist.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_flip = result();
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/LList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/LList.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,55 @@
+(*  Title: 	ZF/ex/LList.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Codatatype definition of Lazy Lists
+
+Equality for llist(A) as a greatest fixed point
+
+Functions for Lazy Lists
+
+STILL NEEDS:
+co_recursion for defining lconst, flip, etc.
+a typing rule for it, based on some notion of "productivity..."
+*)
+
+LList = QUniv + "Datatype" +
+
+consts
+  llist  :: "i=>i"
+
+codatatype
+  "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
+
+
+(*Coinductive definition of equality*)
+consts
+  lleq :: "i=>i"
+
+(*Previously used <*> in the domain and variant pairs as elements.  But
+  standard pairs work just as well.  To use variant pairs, must change prefix
+  a q/Q to the Sigma, Pair and converse rules.*)
+coinductive
+  domains "lleq(A)" <= "llist(A) * llist(A)"
+  intrs
+    LNil  "<LNil, LNil> : lleq(A)"
+    LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
+  type_intrs  "llist.intrs"
+
+
+(*Lazy list functions; flip is not definitional!*)
+consts
+  lconst   :: "i => i"
+  flip     :: "i => i"
+
+rules
+  lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
+
+  flip_LNil   "flip(LNil) = LNil"
+
+  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
+\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
+
+end
+
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/ListN.ML
--- a/src/ZF/ex/ListN.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/ListN.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -9,25 +9,15 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-structure ListN = Inductive_Fun
- (val thy        = ListFn.thy |> add_consts [("listn","i=>i",NoSyn)]
-  val thy_name   = "ListN"
-  val rec_doms   = [("listn", "nat*list(A)")]
-  val sintrs     = 
-          ["<0,Nil> : listn(A)",
-           "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
-  val monos      = []
-  val con_defs   = []
-  val type_intrs = nat_typechecks @ List.intrs 
-  val type_elims = []);
+open ListN;
 
 val listn_induct = standard 
-    (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
+    (listn.mutual_induct RS spec RS spec RSN (2,rev_mp));
 
 goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
-by (etac List.induct 1);
+by (etac list.induct 1);
 by (ALLGOALS (asm_simp_tac list_ss));
-by (REPEAT (ares_tac ListN.intrs 1));
+by (REPEAT (ares_tac listn.intrs 1));
 val list_into_listn = result();
 
 goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
@@ -42,9 +32,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)";
+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 (rtac listn.bnd_mono 1));
 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
 val listn_mono = result();
 
@@ -52,11 +42,11 @@
     "!!n l. [| <n,l> : listn(A);  <n',l'> : listn(A) |] ==> \
 \           <n#+n', l@l'> : listn(A)";
 by (etac listn_induct 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps ListN.intrs)));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps listn.intrs)));
 val listn_append = result();
 
-val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
-and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
+val Nil_listn_case = listn.mk_cases list.con_defs "<i,Nil> : listn(A)"
+and Cons_listn_case = listn.mk_cases list.con_defs "<i,Cons(x,l)> : listn(A)";
 
-val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
-and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";
+val zero_listn_case = listn.mk_cases list.con_defs "<0,l> : listn(A)"
+and succ_listn_case = listn.mk_cases list.con_defs "<succ(i),l> : listn(A)";
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/ListN.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/ListN.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,20 @@
+(*  Title: 	ZF/ex/ListN
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of lists of n elements
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
+*)
+
+ListN = List +
+consts	listn ::"i=>i"
+inductive
+  domains   "listn(A)" <= "nat*list(A)"
+  intrs
+    NilI  "<0,Nil> : listn(A)"
+    ConsI "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
+  type_intrs "nat_typechecks @ list.intrs"
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Ntree.ML
--- a/src/ZF/ex/Ntree.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Ntree.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -9,27 +9,16 @@
 Based upon ex/Term.ML
 *)
 
-structure Ntree = Datatype_Fun
- (val thy	= Univ.thy;
-  val thy_name 	= "Ntree";
-  val rec_specs = 
-      [("ntree", "univ(A)",
-	  [(["Branch"], "[i,i]=>i", NoSyn)])];
-  val rec_styp 	= "i=>i";
-  val sintrs 	= 
-	["[| a: A;  n: nat;  h: n -> ntree(A) |] ==> Branch(a,h) : ntree(A)"];
-  val monos 	= [Pi_mono];
-  val type_intrs = (nat_fun_univ RS subsetD) :: datatype_intrs;
-  val type_elims = []);
-
-val [BranchI] = Ntree.intrs;
+open Ntree;
 
 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
-by (rtac (Ntree.unfold RS trans) 1);
-bws Ntree.con_defs;
-by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
- 	             addDs [Ntree.dom_subset RS subsetD]
- 	             addEs [A_into_univ, nat_fun_into_univ]) 1);
+by (rtac (ntree.unfold RS trans) 1);
+bws ntree.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+by (fast_tac (sum_cs addIs datatype_intrs
+ 	             addDs [ntree.dom_subset RS subsetD]
+ 	             addEs [nat_fun_into_univ]) 1);
 val ntree_unfold = result();
 
 (*A nicer induction rule than the standard one*)
@@ -38,7 +27,8 @@
 \       !!x n h. [| x: A;  n: nat;  h: n -> ntree(A);  ALL i:n. P(h`i)  \
 \                |] ==> P(Branch(x,h))  \
 \    |] ==> P(t)";
-by (rtac (major RS Ntree.induct) 1);
+by (rtac (major RS ntree.induct) 1);
+by (etac UN_E 1);
 by (REPEAT_SOME (ares_tac prems));
 by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
 by (fast_tac (ZF_cs addDs [apply_type]) 1);
@@ -60,14 +50,14 @@
 
 (**  Lemmas to justify using "Ntree" in other recursive type definitions **)
 
-goalw Ntree.thy Ntree.defs "!!A B. A<=B ==> ntree(A) <= ntree(B)";
+goalw Ntree.thy ntree.defs "!!A B. A<=B ==> ntree(A) <= ntree(B)";
 by (rtac lfp_mono 1);
-by (REPEAT (rtac Ntree.bnd_mono 1));
+by (REPEAT (rtac ntree.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
 val ntree_mono = result();
 
 (*Easily provable by induction also*)
-goalw Ntree.thy (Ntree.defs@Ntree.con_defs) "ntree(univ(A)) <= univ(A)";
+goalw Ntree.thy (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
 by (safe_tac ZF_cs);
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Ntree.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Ntree.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,23 @@
+(*  Title: 	ZF/ex/Ntree.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Datatype definition n-ary branching trees
+Demonstrates a simple use of function space in a datatype definition
+   and also "nested" monotonicity theorems
+
+Based upon ex/Term.thy
+*)
+
+Ntree = InfDatatype +
+consts
+  ntree :: "i=>i"
+
+datatype
+  "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
+  monos	      "[[subset_refl, Pi_mono] MRS UN_mono]"
+  type_intrs  "[nat_fun_univ RS subsetD]"
+  type_elims  "[UN_E]"
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Primrec.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Primrec.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,379 @@
+(*  Title: 	ZF/ex/Primrec
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  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.
+
+See also E. Mendelson, Introduction to Mathematical Logic.
+(Van Nostrand, 1964), page 250, exercise 11.
+*)
+
+open Primrec;
+
+val pr_typechecks = 
+    nat_typechecks @ list.intrs @ 
+    [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
+
+(** Useful special cases of evaluation ***)
+
+val pr_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 pr_typechecks);
+
+goalw Primrec.thy [SC_def]
+    "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
+by (asm_simp_tac pr_ss 1);
+val SC = result();
+
+goalw Primrec.thy [CONST_def]
+    "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
+by (asm_simp_tac pr_ss 1);
+val CONST = result();
+
+goalw Primrec.thy [PROJ_def]
+    "!!l. [| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
+by (asm_simp_tac pr_ss 1);
+val PROJ_0 = result();
+
+goalw Primrec.thy [COMP_def]
+    "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
+by (asm_simp_tac pr_ss 1);
+val COMP_1 = result();
+
+goalw Primrec.thy [PREC_def]
+    "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
+by (asm_simp_tac pr_ss 1);
+val PREC_0 = result();
+
+goalw Primrec.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 pr_ss 1);
+val PREC_succ = result();
+
+(*** Inductive definition of the PR functions ***)
+
+(* c: primrec ==> c: list(nat) -> nat *)
+val primrec_into_fun = primrec.dom_subset RS subsetD;
+
+val pr_ss = pr_ss 
+    setsolver (type_auto_tac ([primrec_into_fun] @ 
+			      pr_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, nat_into_Ord] @ 
+    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 Primrec.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
+by (asm_simp_tac (pr_ss addsimps [SC]) 1);
+val ack_0 = result();
+
+(*PROPERTY A 2*)
+goalw Primrec.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
+by (asm_simp_tac (pr_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, nat_into_Ord];
+
+(*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 (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
+	     asm_simp_tac ack_ss] 1);
+by (DO_GOAL [etac (succ_leI RS lt_trans1),
+	     asm_simp_tac ack_ss] 1);
+val lt_ack2_lemma = result();
+val lt_ack2 = standard (lt_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 [lt_ack2])));
+val ack_lt_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 [lt_nat_in_nat] 1 THEN assume_tac 1);
+by (etac succ_lt_induct 1);
+by (assume_tac 1);
+by (rtac lt_trans 2);
+by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr_typechecks) 1));
+val ack_lt_mono2 = result();
+
+(*PROPERTY A 5', monotonicity for le *)
+goal Primrec.thy
+    "!!i j k. [| j le k;  i: nat;  k:nat |] ==> ack(i,j) le ack(i,k)";
+by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
+val ack_le_mono2 = result();
+
+(*PROPERTY A 6*)
+goal Primrec.thy
+    "!!i j. [| i:nat;  j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
+by (nat_ind_tac "j" [] 1);
+by (ALLGOALS (asm_simp_tac ack_ss));
+by (rtac ack_le_mono2 1);
+by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
+by (REPEAT (ares_tac (ack_typechecks) 1));
+val ack2_le_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_lt_mono2 RS lt_trans2) 1);
+by (rtac ack2_le_ack1 4);
+by (REPEAT (ares_tac ([nat_le_refl, ack_type] @ pr_typechecks) 1));
+val ack_lt_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 [lt_nat_in_nat] 1 THEN assume_tac 1);
+by (etac succ_lt_induct 1);
+by (assume_tac 1);
+by (rtac lt_trans 2);
+by (REPEAT (ares_tac ([ack_lt_ack_succ1, ack_type] @ pr_typechecks) 1));
+val ack_lt_mono1 = result();
+
+(*PROPERTY A 7', monotonicity for le *)
+goal Primrec.thy
+    "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
+by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
+val ack_le_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 (ack2_le_ack1 RSN (2,lt_trans2)) 1);
+by (asm_simp_tac ack_ss 1);
+by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
+by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
+by (tc_tac []);
+val ack_nest_bound = result();
+
+(*PROPERTY A 11*)
+goal Primrec.thy
+    "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
+\          ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
+by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
+by (asm_simp_tac (ack_ss addsimps [ack_2]) 1);
+by (rtac (ack_nest_bound RS lt_trans2) 2);
+by (asm_simp_tac ack_ss 5);
+by (rtac (add_le_mono RS leI RS leI) 1);
+by (REPEAT (ares_tac ([add_le_self, add_le_self2, ack_le_mono1] @
+                      ack_typechecks) 1));
+val ack_add_bound = result();
+
+(*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
+  used k#+4.  Quantified version must be nested EX k'. ALL i,j... *)
+goal Primrec.thy
+    "!!i j k. [| i < ack(k,j);  j:nat;  k:nat |] ==> \
+\             i#+j < ack(succ(succ(succ(succ(k)))), j)";
+by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
+by (rtac (ack_add_bound RS lt_trans2) 2);
+by (asm_simp_tac (ack_ss addsimps [add_0_right]) 5);
+by (REPEAT (ares_tac ([add_lt_mono, lt_ack2] @ ack_typechecks) 1));
+val ack_add_bound2 = result();
+
+(*** MAIN RESULT ***)
+
+val ack2_ss =
+    ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, nat_into_Ord];
+
+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_le_self]) 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_le]) 1);
+by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
+by (tc_tac []);
+val lt_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 [lt_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_le]) 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_le_self]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (etac (bspec RS lt_trans2) 1);
+by (rtac (add_le_self2 RS succ_leI) 2);
+by (tc_tac []);
+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 [lt_ack1, nat_0_le]),
+	     resolve_tac nat_typechecks] 1);
+by (safe_tac ZF_cs);
+by (asm_simp_tac ack2_ss 1);
+by (rtac (ballI RS bexI) 1);
+by (rtac (add_lt_mono RS lt_trans) 1);
+by (REPEAT (FIRSTGOAL (etac bspec)));
+by (rtac ack_add_bound 5);
+by (tc_tac []);
+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 lt_trans) 1);
+by (rtac lt_trans 2);
+by (rtac ack_nest_bound 3);
+by (etac (bspec RS ack_lt_mono2) 2);
+by (tc_tac [map_type]);
+val COMP_case = result();
+
+(** PREC case **)
+
+goalw Primrec.thy [PREC_def]
+ "!!f g. [| 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));	\
+\           f: primrec;  kf: nat;					\
+\           g: primrec;  kg: nat;					\
+\           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 [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (etac ssubst 1);  (*get rid of the needless assumption*)
+by (eres_inst_tac [("n","a")] nat_induct 1);
+(*base case*)
+by (DO_GOAL [asm_simp_tac ack2_ss, rtac lt_trans, etac bspec,
+	     assume_tac, rtac (add_le_self RS ack_lt_mono1),
+	     REPEAT o ares_tac (ack_typechecks)] 1);
+(*ind step*)
+by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
+by (rtac (succ_leI RS lt_trans1) 1);
+by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
+by (etac bspec 2);
+by (rtac (nat_le_refl RS add_le_mono) 1);
+by (tc_tac []);
+by (asm_simp_tac (ack2_ss addsimps [add_le_self2]) 1);
+(*final part of the simplification*)
+by (asm_simp_tac ack2_ss 1);
+by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
+by (etac ack_lt_mono2 5);
+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 (rtac (ballI RS bexI) 1);
+by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
+by (REPEAT
+    (SOMEGOAL
+     (FIRST' [test_assume_tac,
+	      match_tac (ack_typechecks),
+	      rtac (ack_add_bound2 RS ballI) THEN' etac bspec])));
+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 lt_irrefl 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 ab2c867829ec -r abcc438e7c27 src/ZF/ex/Primrec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Primrec.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,64 @@
+(*  Title: 	ZF/ex/Primrec.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  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.
+
+See also E. Mendelson, Introduction to Mathematical Logic.
+(Van Nostrand, 1964), page 250, exercise 11.
+*)
+
+Primrec = List +
+consts
+    primrec :: "i"
+    SC      :: "i"
+    CONST   :: "i=>i"
+    PROJ    :: "i=>i"
+    COMP    :: "[i,i]=>i"
+    PREC    :: "[i,i]=>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)])))"
+
+
+inductive
+  domains "primrec" <= "list(nat)->nat"
+  intrs
+    SC       "SC : primrec"
+    CONST    "k: nat ==> CONST(k) : primrec"
+    PROJ     "i: nat ==> PROJ(i) : primrec"
+    COMP     "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
+    PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
+  monos      "[list_mono]"
+  con_defs   "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
+  type_intrs "nat_typechecks @ list.intrs @   		        \
+\	      [lam_type, list_case_type, drop_type, map_type,   \
+\	      apply_type, rec_type]"
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/PropLog.ML
--- a/src/ZF/ex/PropLog.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/PropLog.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -17,20 +17,20 @@
 
 goal PropLog.thy "prop_rec(Fls,b,c,d) = b";
 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac Prop.con_defs);
+by (rewrite_goals_tac prop.con_defs);
 by (simp_tac rank_ss 1);
 val prop_rec_Fls = result();
 
 goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)";
 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac Prop.con_defs);
+by (rewrite_goals_tac prop.con_defs);
 by (simp_tac rank_ss 1);
 val prop_rec_Var = result();
 
 goal PropLog.thy "prop_rec(p=>q,b,c,d) = \
 \      d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac Prop.con_defs);
+by (rewrite_goals_tac prop.con_defs);
 by (simp_tac rank_ss 1);
 val prop_rec_Imp = result();
 
@@ -70,49 +70,34 @@
 val hyps_Imp = result();
 
 val prop_ss = prop_rec_ss 
-    addsimps Prop.intrs
+    addsimps prop.intrs
     addsimps [is_true_Fls, is_true_Var, is_true_Imp,
 	      hyps_Fls, hyps_Var, hyps_Imp];
 
 (*** Proof theory of propositional logic ***)
 
-structure PropThms = Inductive_Fun
- (val thy = PropLog.thy;
-  val thy_name = "PropThms";
-  val rec_doms = [("thms","prop")];
-  val sintrs = 
-      ["[| p:H;  p:prop |] ==> H |- p",
-       "[| p:prop;  q:prop |] ==> H |- p=>q=>p",
-       "[| p:prop;  q:prop;  r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r",
-       "p:prop ==> H |- ((p=>Fls) => Fls) => p",
-       "[| H |- p=>q;  H |- p;  p:prop;  q:prop |] ==> H |- q"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = Prop.intrs;
-  val type_elims = []);
-
-goalw PropThms.thy PropThms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
+goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
 by (rtac lfp_mono 1);
-by (REPEAT (rtac PropThms.bnd_mono 1));
+by (REPEAT (rtac thms.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
 val thms_mono = result();
 
-val thms_in_pl = PropThms.dom_subset RS subsetD;
+val thms_in_pl = thms.dom_subset RS subsetD;
 
-val [thms_H, thms_K, thms_S, thms_DN, weak_thms_MP] = PropThms.intrs;
+val ImpE = prop.mk_cases prop.con_defs "p=>q : prop";
 
-(*Modus Ponens rule -- this stronger version avoids typecheck*)
-goal PropThms.thy "!!p q H. [| H |- p=>q;  H |- p |] ==> H |- q";
-by (rtac weak_thms_MP 1);
+(*Stronger Modus Ponens rule: no typechecking!*)
+goal PropLog.thy "!!p q H. [| H |- p=>q;  H |- p |] ==> H |- q";
+by (rtac thms.MP 1);
 by (REPEAT (eresolve_tac [asm_rl, thms_in_pl, thms_in_pl RS ImpE] 1));
 val thms_MP = result();
 
 (*Rule is called I for Identity Combinator, not for Introduction*)
-goal PropThms.thy "!!p H. p:prop ==> H |- p=>p";
-by (rtac (thms_S RS thms_MP RS thms_MP) 1);
-by (rtac thms_K 5);
-by (rtac thms_K 4);
-by (REPEAT (ares_tac [ImpI] 1));
+goal PropLog.thy "!!p H. p:prop ==> H |- p=>p";
+by (rtac (thms.S RS thms_MP RS thms_MP) 1);
+by (rtac thms.K 5);
+by (rtac thms.K 4);
+by (REPEAT (ares_tac prop.intrs 1));
 val thms_I = result();
 
 (** Weakening, left and right **)
@@ -126,71 +111,71 @@
 val weaken_left_Un1  = Un_upper1 RS weaken_left;
 val weaken_left_Un2  = Un_upper2 RS weaken_left;
 
-goal PropThms.thy "!!H p q. [| H |- q;  p:prop |] ==> H |- p=>q";
-by (rtac (thms_K RS thms_MP) 1);
+goal PropLog.thy "!!H p q. [| H |- q;  p:prop |] ==> H |- p=>q";
+by (rtac (thms.K RS thms_MP) 1);
 by (REPEAT (ares_tac [thms_in_pl] 1));
 val weaken_right = result();
 
 (*The deduction theorem*)
-goal PropThms.thy "!!p q H. [| cons(p,H) |- q;  p:prop |] ==>  H |- p=>q";
-by (etac PropThms.induct 1);
-by (fast_tac (ZF_cs addIs [thms_I, thms_H RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_K RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_S RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_DN RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_S RS thms_MP RS thms_MP]) 1);
+goal PropLog.thy "!!p q H. [| cons(p,H) |- q;  p:prop |] ==>  H |- p=>q";
+by (etac thms.induct 1);
+by (fast_tac (ZF_cs addIs [thms_I, thms.H RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.K RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.S RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.DN RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.S RS thms_MP RS thms_MP]) 1);
 val deduction = result();
 
 
 (*The cut rule*)
-goal PropThms.thy "!!H p q. [| H|-p;  cons(p,H) |- q |] ==>  H |- q";
+goal PropLog.thy "!!H p q. [| H|-p;  cons(p,H) |- q |] ==>  H |- q";
 by (rtac (deduction RS thms_MP) 1);
 by (REPEAT (ares_tac [thms_in_pl] 1));
 val cut = result();
 
-goal PropThms.thy "!!H p. [| H |- Fls; p:prop |] ==> H |- p";
-by (rtac (thms_DN RS thms_MP) 1);
+goal PropLog.thy "!!H p. [| H |- Fls; p:prop |] ==> H |- p";
+by (rtac (thms.DN RS thms_MP) 1);
 by (rtac weaken_right 2);
-by (REPEAT (ares_tac (Prop.intrs@[consI1]) 1));
+by (REPEAT (ares_tac (prop.intrs@[consI1]) 1));
 val thms_FlsE = result();
 
 (* [| H |- p=>Fls;  H |- p;  q: prop |] ==> H |- q *)
 val thms_notE = standard (thms_MP RS thms_FlsE);
 
 (*Soundness of the rules wrt truth-table semantics*)
-goalw PropThms.thy [logcon_def] "!!H. H |- p ==> H |= p";
-by (etac PropThms.induct 1);
+goalw PropLog.thy [logcon_def] "!!H. H |- p ==> H |= p";
+by (etac thms.induct 1);
 by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
 by (ALLGOALS (asm_simp_tac prop_ss));
 val soundness = result();
 
 (*** Towards the completeness proof ***)
 
-val [premf,premq] = goal PropThms.thy
+val [premf,premq] = goal PropLog.thy
     "[| H |- p=>Fls; q: prop |] ==> H |- p=>q";
 by (rtac (premf RS thms_in_pl RS ImpE) 1);
 by (rtac deduction 1);
 by (rtac (premf RS weaken_left_cons RS thms_notE) 1);
-by (REPEAT (ares_tac [premq, consI1, thms_H] 1));
+by (REPEAT (ares_tac [premq, consI1, thms.H] 1));
 val Fls_Imp = result();
 
-val [premp,premq] = goal PropThms.thy
+val [premp,premq] = goal PropLog.thy
     "[| H |- p;  H |- q=>Fls |] ==> H |- (p=>q)=>Fls";
 by (cut_facts_tac ([premp,premq] RL [thms_in_pl]) 1);
 by (etac ImpE 1);
 by (rtac deduction 1);
 by (rtac (premq RS weaken_left_cons RS thms_MP) 1);
-by (rtac (consI1 RS thms_H RS thms_MP) 1);
+by (rtac (consI1 RS thms.H RS thms_MP) 1);
 by (rtac (premp RS weaken_left_cons) 2);
-by (REPEAT (ares_tac Prop.intrs 1));
+by (REPEAT (ares_tac prop.intrs 1));
 val Imp_Fls = result();
 
 (*Typical example of strengthening the induction formula*)
-val [major] = goal PropThms.thy 
+val [major] = goal PropLog.thy 
     "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
 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 (rtac (major RS prop.induct) 1);
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms.H])));
 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, 
@@ -198,7 +183,7 @@
 val hyps_thms_if = result();
 
 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
-val [premp,sat] = goalw PropThms.thy [logcon_def]
+val [premp,sat] = goalw PropLog.thy [logcon_def]
     "[| p: prop;  0 |= p |] ==> hyps(p,t) |- p";
 by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
     rtac (premp RS hyps_thms_if) 2);
@@ -207,46 +192,46 @@
 
 (*For proving certain theorems in our new propositional logic*)
 val thms_cs = 
-    ZF_cs addSIs [FlsI, VarI, ImpI, deduction]
-          addIs [thms_in_pl, thms_H, thms_H RS thms_MP];
+    ZF_cs addSIs (prop.intrs @ [deduction])
+          addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
 
 (*The excluded middle in the form of an elimination rule*)
-val prems = goal PropThms.thy
+val prems = goal PropLog.thy
     "[| p: prop;  q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
 by (rtac (deduction RS deduction) 1);
-by (rtac (thms_DN RS thms_MP) 1);
+by (rtac (thms.DN RS thms_MP) 1);
 by (ALLGOALS (best_tac (thms_cs addSIs prems)));
 val thms_excluded_middle = result();
 
 (*Hard to prove directly because it requires cuts*)
-val prems = goal PropThms.thy
+val prems = goal PropLog.thy
     "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p: prop |] ==> H |- q";
 by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
-by (REPEAT (resolve_tac (prems@Prop.intrs@[deduction,thms_in_pl]) 1));
+by (REPEAT (resolve_tac (prems@prop.intrs@[deduction,thms_in_pl]) 1));
 val thms_excluded_middle_rule = result();
 
 (*** Completeness -- lemmas for reducing the set of assumptions ***)
 
 (*For the case hyps(p,t)-cons(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-val [major] = goal PropThms.thy
+val [major] = goal PropLog.thy
     "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
-by (rtac (major RS Prop.induct) 1);
+by (rtac (major RS prop.induct) 1);
 by (simp_tac prop_ss 1);
 by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
-by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
+by (fast_tac (ZF_cs addSEs prop.free_SEs) 1);
 by (asm_simp_tac prop_ss 1);
 by (fast_tac ZF_cs 1);
 val hyps_Diff = result();
 
 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
   we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
-val [major] = goal PropThms.thy
+val [major] = goal PropLog.thy
     "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
-by (rtac (major RS Prop.induct) 1);
+by (rtac (major RS prop.induct) 1);
 by (simp_tac prop_ss 1);
 by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
-by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
+by (fast_tac (ZF_cs addSEs prop.free_SEs) 1);
 by (asm_simp_tac prop_ss 1);
 by (fast_tac ZF_cs 1);
 val hyps_cons = result();
@@ -263,26 +248,26 @@
 
 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
  could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
-val [major] = goal PropThms.thy
+val [major] = goal PropLog.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, cons_iff]
+by (rtac (major RS prop.induct) 1);
+by (asm_simp_tac (prop_ss addsimps (Fin.intrs @ [UN_I, cons_iff])
 		  setloop (split_tac [expand_if])) 2);
-by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin.emptyI, Fin_UnI])));
 val hyps_finite = result();
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
 
 (*Induction on the finite set of assumptions hyps(p,t0).
   We may repeatedly subtract assumptions until none are left!*)
-val [premp,sat] = goal PropThms.thy
+val [premp,sat] = goal PropLog.thy
     "[| p: prop;  0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
 by (rtac (premp RS hyps_finite RS Fin_induct) 1);
 by (simp_tac (prop_ss addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
 by (safe_tac ZF_cs);
 (*Case hyps(p,t)-cons(#v,Y) |- p *)
 by (rtac thms_excluded_middle_rule 1);
-by (etac VarI 3);
+by (etac prop.Var_I 3);
 by (rtac (cons_Diff_same RS weaken_left) 1);
 by (etac spec 1);
 by (rtac (cons_Diff_subset2 RS weaken_left) 1);
@@ -290,7 +275,7 @@
 by (etac spec 1);
 (*Case hyps(p,t)-cons(#v => Fls,Y) |- p *)
 by (rtac thms_excluded_middle_rule 1);
-by (etac VarI 3);
+by (etac prop.Var_I 3);
 by (rtac (cons_Diff_same RS weaken_left) 2);
 by (etac spec 2);
 by (rtac (cons_Diff_subset2 RS weaken_left) 1);
@@ -299,28 +284,28 @@
 val completeness_0_lemma = result();
 
 (*The base case for completeness*)
-val [premp,sat] = goal PropThms.thy "[| p: prop;  0 |= p |] ==> 0 |- p";
+val [premp,sat] = goal PropLog.thy "[| p: prop;  0 |= p |] ==> 0 |- p";
 by (rtac (Diff_cancel RS subst) 1);
 by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1);
 val completeness_0 = result();
 
 (*A semantic analogue of the Deduction Theorem*)
-goalw PropThms.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
+goalw PropLog.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
 by (simp_tac prop_ss 1);
 by (fast_tac ZF_cs 1);
 val logcon_Imp = result();
 
-goal PropThms.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
+goal PropLog.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
 by (etac Fin_induct 1);
 by (safe_tac (ZF_cs addSIs [completeness_0]));
 by (rtac (weaken_left_cons RS thms_MP) 1);
-by (fast_tac (ZF_cs addSIs [logcon_Imp,ImpI]) 1);
+by (fast_tac (ZF_cs addSIs (logcon_Imp::prop.intrs)) 1);
 by (fast_tac thms_cs 1);
 val completeness_lemma = result();
 
 val completeness = completeness_lemma RS bspec RS mp;
 
-val [finite] = goal PropThms.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop";
+val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop";
 by (fast_tac (ZF_cs addSEs [soundness, finite RS completeness, 
 			    thms_in_pl]) 1);
 val thms_iff = result();
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/PropLog.thy
--- a/src/ZF/ex/PropLog.thy	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/PropLog.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -1,26 +1,49 @@
-(*  Title: 	ZF/ex/prop-log.thy
+(*  Title: 	ZF/ex/PropLog.thy
     ID:         $Id$
     Author: 	Tobias Nipkow & Lawrence C Paulson
     Copyright   1993  University of Cambridge
 
-Inductive definition of propositional logic.
+Datatype definition of propositional logic formulae and inductive definition
+of the propositional tautologies.
 *)
 
-PropLog = Prop + Fin +
+PropLog = Finite + Univ +
+
+(** The datatype of propositions; note mixfix syntax **)
 consts
-  (*semantics*)
-  prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
-  is_true  :: "[i,i] => o"
-  "|="     :: "[i,i] => o"    			(infixl 50)
-  hyps     :: "[i,i] => i"
+  prop     :: "i"
 
-  (*proof theory*)
+datatype
+  "prop" = Fls
+         | Var ("n: nat")	                ("#_" [100] 100)
+         | "=>" ("p: prop", "q: prop")		(infixr 90)
+
+(** The proof system **)
+consts
   thms     :: "i => i"
   "|-"     :: "[i,i] => o"    			(infixl 50)
 
 translations
   "H |- p" == "p : thms(H)"
 
+inductive
+  domains "thms(H)" <= "prop"
+  intrs
+    H  "[| p:H;  p:prop |] ==> H |- p"
+    K  "[| p:prop;  q:prop |] ==> H |- p=>q=>p"
+    S  "[| p:prop;  q:prop;  r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
+    DN "p:prop ==> H |- ((p=>Fls) => Fls) => p"
+    MP "[| H |- p=>q;  H |- p;  p:prop;  q:prop |] ==> H |- q"
+  type_intrs "prop.intrs"
+
+
+(** The semantics **)
+consts
+  prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
+  is_true  :: "[i,i] => o"
+  "|="     :: "[i,i] => o"    			(infixl 50)
+  hyps     :: "[i,i] => i"
+
 rules
 
   prop_rec_def
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/ROOT.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -21,12 +21,12 @@
 time_use_thy "ex/Integ";
 (*Binary integer arithmetic*)
 use          "ex/twos_compl.ML";
-time_use_thy "ex/BinFn";
+time_use_thy "ex/Bin";
 
 (** Datatypes **)
-time_use_thy "ex/BT_Fn";	(*binary trees*)
-time_use_thy "ex/TermFn";	(*terms: recursion over the list functor*)
-time_use_thy "ex/TF_Fn";	(*trees/forests: mutual recursion*)
+time_use_thy "ex/BT";		(*binary trees*)
+time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
+time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
 time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
 time_use_thy "ex/Brouwer";	(*Brouwer ordinals: infinite-branching trees*)
 time_use_thy "ex/Data";		(*Sample datatype*)
@@ -35,16 +35,14 @@
 (** Inductive definitions **)
 time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
 time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
-(*two Coq examples by Ch. Paulin-Mohring*)
+(*two Coq examples by Christine Paulin-Mohring*)
 time_use_thy "ex/ListN";
 time_use_thy "ex/Acc";
-time_use_thy "ex/Contract0";	(*Contraction relation for combinatory logic*)
-time_use_thy "ex/ParContract";	(*Diamond property for combinatory logic*)
-time_use_thy "ex/Primrec0";
+time_use_thy "ex/Comb";		(*Combinatory Logic example*)
+time_use_thy "ex/Primrec";
 
 (** CoDatatypes **)
 time_use_thy "ex/LList";
-time_use_thy "ex/LListFn";
 time_use     "ex/CoUnit.ML";
 
 maketest"END: Root file for ZF Set Theory examples";
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Rmap.ML
--- a/src/ZF/ex/Rmap.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Rmap.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -1,43 +1,31 @@
-(*  Title: 	ZF/ex/rmap
+(*  Title: 	ZF/ex/Rmap
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Inductive definition of an operator to "map" a relation over a list
 *)
 
-structure Rmap = Inductive_Fun
- (val thy 	 = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
-  val thy_name	 = "Rmap";
-  val rec_doms	 = [("rmap", "list(domain(r))*list(range(r))")];
-  val sintrs	 = 
-      ["<Nil,Nil> : rmap(r)",
+open Rmap;
 
-       "[| <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
-  val type_elims = []);
-
-goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
+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 (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));
+    (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 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
+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 (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();
@@ -45,7 +33,7 @@
 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 (etac list.induct 1);
 by (ALLGOALS (fast_tac rmap_cs));
 val rmap_total = result();
 
@@ -79,5 +67,5 @@
 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));
+by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
 val rmap_Cons = result();
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Rmap.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Rmap.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,25 @@
+(*  Title: 	ZF/ex/Rmap
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+Rmap = List +
+
+consts
+  rmap :: "i=>i"
+
+inductive
+  domains "rmap(r)" <= "list(domain(r))*list(range(r))"
+  intrs
+    NilI  "<Nil,Nil> : rmap(r)"
+
+    ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
+\          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
+
+  type_intrs "[domainI,rangeI] @ list.intrs"
+
+end
+  
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/TF.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -4,39 +4,29 @@
     Copyright   1993  University of Cambridge
 
 Trees & forests, a mutually recursive type definition.
+
+Still needs
+
+"TF_reflect == (%z. TF_rec(z, %x ts r. Tcons(x,r), 0, 
+               %t ts r1 r2. TF_of_list(list_of_TF(r2) @ <r1,0>)))"
 *)
 
-structure TF = Datatype_Fun
- (val thy        = Univ.thy
-  val thy_name   = "TF"
-  val rec_specs  = [("tree", "univ(A)",
-                       [(["Tcons"],  "[i,i]=>i",  NoSyn)]),
-                    ("forest", "univ(A)",
-                       [(["Fnil"],   "i",         NoSyn),
-                        (["Fcons"],  "[i,i]=>i",  NoSyn)])]
-  val rec_styp   = "i=>i"
-  val sintrs     = 
-          ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
-           "Fnil : forest(A)",
-           "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
-  val monos      = []
-  val type_intrs = datatype_intrs
-  val type_elims = datatype_elims);
+open TF;
 
-val [TconsI, FnilI, FconsI] = TF.intrs;
+val [TconsI, FnilI, FconsI] = tree_forest.intrs;
 
 (** tree_forest(A) as the union of tree(A) and forest(A) **)
 
-goalw TF.thy (tl TF.defs) "tree(A) <= tree_forest(A)";
+goalw TF.thy (tl tree_forest.defs) "tree(A) <= tree_forest(A)";
 by (rtac Part_subset 1);
 val tree_subset_TF = result();
 
-goalw TF.thy (tl TF.defs) "forest(A) <= tree_forest(A)";
+goalw TF.thy (tl tree_forest.defs) "forest(A) <= tree_forest(A)";
 by (rtac Part_subset 1);
 val forest_subset_TF = result();
 
-goalw TF.thy (tl TF.defs) "tree(A) Un forest(A) = tree_forest(A)";
-by (rtac (TF.dom_subset RS Part_sum_equality) 1);
+goalw TF.thy (tl tree_forest.defs) "tree(A) Un forest(A) = tree_forest(A)";
+by (rtac (tree_forest.dom_subset RS Part_sum_equality) 1);
 val TF_equals_Un = result();
 
 (** NOT useful, but interesting... **)
@@ -44,30 +34,240 @@
 (*The (refl RS conjI RS exI RS exI) avoids considerable search!*)
 val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI]
                     addIs datatype_intrs
-                    addDs [TF.dom_subset RS subsetD]
-	            addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
+                    addDs [tree_forest.dom_subset RS subsetD]
+	            addSEs ([PartE] @ datatype_elims @ tree_forest.free_SEs);
 
-goalw TF.thy (tl TF.defs)
+goalw TF.thy (tl tree_forest.defs)
     "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
-by (rtac (TF.unfold RS trans) 1);
-by (rewrite_goals_tac TF.con_defs);
+by (rtac (tree_forest.unfold RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
 by (rtac equalityI 1);
 by (fast_tac unfold_cs 1);
 by (fast_tac unfold_cs 1);
 val tree_forest_unfold = result();
 
-val tree_forest_unfold' = rewrite_rule (tl TF.defs) tree_forest_unfold;
+val tree_forest_unfold' = rewrite_rule (tl tree_forest.defs) tree_forest_unfold;
 
 
-goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
+goalw TF.thy (tl tree_forest.defs)
+    "tree(A) = {Inl(x). x: A*forest(A)}";
 by (rtac (Part_Inl RS subst) 1);
 by (rtac (tree_forest_unfold' RS subst_context) 1);
 val tree_unfold = result();
 
-goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
+goalw TF.thy (tl tree_forest.defs)
+    "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
 by (rtac (Part_Inr RS subst) 1);
 by (rtac (tree_forest_unfold' RS subst_context) 1);
 val forest_unfold = result();
 
 
+(*** TF_rec -- by Vset recursion ***)
 
+(** conversion rules **)
+
+goal TF.thy "TF_rec(Tcons(a,f), b, c, d) = b(a, f, TF_rec(f,b,c,d))";
+by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
+by (simp_tac rank_ss 1);
+val TF_rec_Tcons = result();
+
+goal TF.thy "TF_rec(Fnil, b, c, d) = c";
+by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
+by (simp_tac rank_ss 1);
+val TF_rec_Fnil = result();
+
+goal TF.thy "TF_rec(Fcons(t,f), b, c, d) = \
+\      d(t, f, TF_rec(t, b, c, d), TF_rec(f, b, c, d))";
+by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
+by (simp_tac rank_ss 1);
+val TF_rec_Fcons = result();
+
+(*list_ss includes list operations as well as arith_ss*)
+val TF_rec_ss = list_ss addsimps
+  [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
+
+(** Type checking **)
+
+val major::prems = goal TF.thy
+    "[| z: tree_forest(A);  \
+\       !!x f r. [| x: A;  f: forest(A);  r: C(f) 		\
+\                 |] ==> b(x,f,r): C(Tcons(x,f));     	\
+\	c : C(Fnil);        					\
+\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: C(f) \
+\                     |] ==> d(t,f,r1,r2): C(Fcons(t,f))    	\
+\    |] ==> TF_rec(z,b,c,d) : C(z)";
+by (rtac (major RS tree_forest.induct) 1);
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
+val TF_rec_type = result();
+
+(*Mutually recursive version*)
+val prems = goal TF.thy
+    "[| !!x f r. [| x: A;  f: forest(A);  r: D(f) 		\
+\                 |] ==> b(x,f,r): C(Tcons(x,f));    	 	\
+\	c : D(Fnil);        					\
+\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: D(f) \
+\                     |] ==> d(t,f,r1,r2): D(Fcons(t,f))    	\
+\    |] ==> (ALL t:tree(A).    TF_rec(t,b,c,d)  : C(t)) &  	\
+\           (ALL f: forest(A). TF_rec(f,b,c,d) : D(f))";
+by (rewtac Ball_def);
+by (rtac tree_forest.mutual_induct 1);
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
+val tree_forest_rec_type = result();
+
+
+(** Versions for use with definitions **)
+
+val [rew] = goal TF.thy
+    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))";
+by (rewtac rew);
+by (rtac TF_rec_Tcons 1);
+val def_TF_rec_Tcons = result();
+
+val [rew] = goal TF.thy
+    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
+by (rewtac rew);
+by (rtac TF_rec_Fnil 1);
+val def_TF_rec_Fnil = result();
+
+val [rew] = goal TF.thy
+    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))";
+by (rewtac rew);
+by (rtac TF_rec_Fcons 1);
+val def_TF_rec_Fcons = result();
+
+fun TF_recs def = map standard 
+    	([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
+
+
+(** list_of_TF and TF_of_list **)
+
+val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] =
+	TF_recs list_of_TF_def;
+
+goalw TF.thy [list_of_TF_def]
+    "!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
+by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
+val list_of_TF_type = result();
+
+val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
+
+goalw TF.thy [TF_of_list_def] 
+    "!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
+by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
+val TF_of_list_type = result();
+
+
+(** TF_map **)
+
+val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def;
+
+val prems = goalw TF.thy [TF_map_def]
+    "[| !!x. x: A ==> h(x): B |] ==> \
+\      (ALL t:tree(A). TF_map(h,t) : tree(B)) &  \
+\      (ALL f: forest(A). TF_map(h,f) : forest(B))";
+by (REPEAT
+    (ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
+val TF_map_type = result();
+
+
+(** TF_size **)
+
+val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def;
+
+goalw TF.thy [TF_size_def]
+    "!!z A. z: tree_forest(A) ==> TF_size(z) : nat";
+by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
+val TF_size_type = result();
+
+
+(** TF_preorder **)
+
+val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] =
+	TF_recs TF_preorder_def;
+
+goalw TF.thy [TF_preorder_def]
+    "!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)";
+by (REPEAT (ares_tac ([TF_rec_type, app_type] @ list.intrs) 1));
+val TF_preorder_type = result();
+
+
+(** Term simplification **)
+
+val treeI = tree_subset_TF RS subsetD
+and forestI = forest_subset_TF RS subsetD;
+
+val TF_typechecks =
+    [TconsI, FnilI, FconsI, treeI, forestI,
+     list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
+
+val TF_rewrites =
+   [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
+    list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
+    TF_of_list_Nil,TF_of_list_Cons,
+    TF_map_Tcons, TF_map_Fnil, TF_map_Fcons,
+    TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
+    TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
+
+val TF_ss = list_ss addsimps TF_rewrites
+                    setsolver type_auto_tac (list_typechecks@TF_typechecks);
+
+(** theorems about list_of_TF and TF_of_list **)
+
+(*essentially the same as list induction*)
+val major::prems = goal TF.thy 
+    "[| f: forest(A);  	\
+\       R(Fnil);        \
+\       !!t f. [| t: tree(A);  f: forest(A);  R(f) |] ==> R(Fcons(t,f))  \
+\    |] ==> R(f)";
+by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
+by (REPEAT (ares_tac (TrueI::prems) 1));
+val forest_induct = result();
+
+goal TF.thy "!!f A. f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
+by (etac forest_induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val forest_iso = result();
+
+goal TF.thy
+    "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val tree_list_iso = result();
+
+(** theorems about TF_map **)
+
+goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val TF_map_ident = result();
+
+goal TF.thy
+ "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val TF_map_compose = result();
+
+(** theorems about TF_size **)
+
+goal TF.thy
+    "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val TF_size_TF_map = result();
+
+goal TF.thy
+    "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
+val TF_size_length = result();
+
+(** theorems about TF_preorder **)
+
+goal TF.thy "!!z A. z: tree_forest(A) ==> \
+\                      TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
+val TF_preorder_TF_map = result();
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/TF.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/TF.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,49 @@
+(*  Title: 	ZF/ex/TF.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Trees & forests, a mutually recursive type definition.
+*)
+
+TF = List +
+consts
+  TF_rec      :: "[i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i"
+  TF_map      :: "[i=>i, i] => i"
+  TF_size     :: "i=>i"
+  TF_preorder :: "i=>i"
+  list_of_TF  :: "i=>i"
+  TF_of_list  :: "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)")
+
+rules
+  TF_rec_def
+    "TF_rec(z,b,c,d) == Vrec(z,  			\
+\      %z r. tree_forest_case(%x f. b(x, f, r`f), 	\
+\                             c, 			\
+\		              %t f. d(t, f, r`t, r`f), z))"
+
+  list_of_TF_def
+    "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \
+\		             %t f r1 r2. Cons(t, r2))"
+
+  TF_of_list_def
+    "TF_of_list(f) == list_rec(f, Fnil,  %t f r. Fcons(t,r))"
+
+  TF_map_def
+    "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \
+\                           %t f r1 r2. Fcons(r1,r2))"
+
+  TF_size_def
+    "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
+
+  TF_preorder_def
+    "TF_preorder(z) == TF_rec(z, %x f r.Cons(x,r), Nil, %t f r1 r2. r1@r2)"
+
+end
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Term.ML	Fri Aug 12 12:28:46 1994 +0200
@@ -7,26 +7,16 @@
 Illustrates the list functor (essentially the same type as in Trees & Forests)
 *)
 
-structure Term = Datatype_Fun
- (val thy	= List.thy;
-  val thy_name	= "Term";
-  val rec_specs = 
-      [("term", "univ(A)",
-	  [(["Apply"], "[i,i]=>i", NoSyn)])];
-  val rec_styp	= "i=>i";
-  val sintrs	= ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
-  val monos	= [list_mono];
-  val type_intrs = (list_univ RS subsetD) :: datatype_intrs;
-  val type_elims = []);
-
-val [ApplyI] = Term.intrs;
+open Term;
 
 goal Term.thy "term(A) = A * list(term(A))";
-by (rtac (Term.unfold RS trans) 1);
-bws Term.con_defs;
-by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
- 	             addDs [Term.dom_subset RS subsetD]
- 	             addEs [A_into_univ, list_into_univ]) 1);
+by (rtac (term.unfold RS trans) 1);
+bws term.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+by (fast_tac (sum_cs addIs datatype_intrs
+ 	             addDs [term.dom_subset RS subsetD]
+ 	             addEs [list_into_univ]) 1);
 val term_unfold = result();
 
 (*Induction on term(A) followed by induction on List *)
@@ -36,33 +26,33 @@
 \       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  P(Apply(x,zs))  \
 \                 |] ==> P(Apply(x, Cons(z,zs)))  \
 \    |] ==> P(t)";
-by (rtac (major RS Term.induct) 1);
-by (etac List.induct 1);
+by (rtac (major RS term.induct) 1);
+by (etac list.induct 1);
 by (etac CollectE 2);
 by (REPEAT (ares_tac (prems@[list_CollectD]) 1));
 val term_induct2 = result();
 
 (*Induction on term(A) to prove an equation*)
-val major::prems = goal (merge_theories(Term.thy,ListFn.thy))
+val major::prems = goal Term.thy
     "[| t: term(A);  \
 \       !!x zs. [| x: A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==> \
 \               f(Apply(x,zs)) = g(Apply(x,zs))  \
 \    |] ==> f(t)=g(t)";
-by (rtac (major RS Term.induct) 1);
+by (rtac (major RS term.induct) 1);
 by (resolve_tac prems 1);
 by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1));
 val term_induct_eqn = result();
 
 (**  Lemmas to justify using "term" in other recursive type definitions **)
 
-goalw Term.thy Term.defs "!!A B. A<=B ==> term(A) <= term(B)";
+goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
 by (rtac lfp_mono 1);
-by (REPEAT (rtac Term.bnd_mono 1));
+by (REPEAT (rtac term.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
 val term_mono = result();
 
 (*Easily provable by induction also*)
-goalw Term.thy (Term.defs@Term.con_defs) "term(univ(A)) <= univ(A)";
+goalw Term.thy (term.defs@term.con_defs) "term(univ(A)) <= univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
 by (safe_tac ZF_cs);
@@ -75,3 +65,178 @@
 goal Term.thy "!!t A B. [| t: term(A);  A <= univ(B) |] ==> t: univ(B)";
 by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1));
 val term_into_univ = result();
+
+
+(*** term_rec -- by Vset recursion ***)
+
+(*Lemma: map works correctly on the underlying list of terms*)
+val [major,ordi] = goal list.thy
+    "[| l: list(A);  Ord(i) |] ==>  \
+\    rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
+by (rtac (major RS list.induct) 1);
+by (simp_tac list_ss 1);
+by (rtac impI 1);
+by (forward_tac [rank_Cons1 RS lt_trans] 1);
+by (dtac (rank_Cons2 RS lt_trans) 1);
+by (asm_simp_tac (list_ss addsimps [ordi, VsetI]) 1);
+val map_lemma = result();
+
+(*Typing premise is necessary to invoke map_lemma*)
+val [prem] = goal Term.thy
+    "ts: list(A) ==> \
+\    term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
+by (rtac (term_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac term.con_defs);
+val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma];
+by (simp_tac term_rec_ss 1);
+val term_rec = result();
+
+(*Slightly odd typing condition on r in the second premise!*)
+val major::prems = goal Term.thy
+    "[| t: term(A);					\
+\       !!x zs r. [| x: A;  zs: list(term(A)); 		\
+\                    r: list(UN t:term(A). C(t)) |]	\
+\                 ==> d(x, zs, r): C(Apply(x,zs))  	\
+\    |] ==> term_rec(t,d) : C(t)";
+by (rtac (major RS term.induct) 1);
+by (forward_tac [list_CollectD] 1);
+by (rtac (term_rec RS ssubst) 1);
+by (REPEAT (ares_tac prems 1));
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
+by (etac CollectE 1);
+by (REPEAT (ares_tac [list.Cons_I, UN_I] 1));
+val term_rec_type = result();
+
+val [rew,tslist] = goal Term.thy
+    "[| !!t. j(t)==term_rec(t,d);  ts: list(A) |] ==> \
+\    j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
+by (rewtac rew);
+by (rtac (tslist RS term_rec) 1);
+val def_term_rec = result();
+
+val prems = goal Term.thy
+    "[| t: term(A);					     \
+\       !!x zs r. [| x: A;  zs: list(term(A));  r: list(C) |]  \
+\                 ==> d(x, zs, r): C  		     \
+\    |] ==> term_rec(t,d) : C";
+by (REPEAT (ares_tac (term_rec_type::prems) 1));
+by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
+val term_rec_simple_type = result();
+
+
+(** term_map **)
+
+val term_map = standard (term_map_def RS def_term_rec);
+
+val prems = goalw Term.thy [term_map_def]
+    "[| t: term(A);  !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
+by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1));
+val term_map_type = result();
+
+val [major] = goal Term.thy
+    "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
+by (rtac (major RS term_map_type) 1);
+by (etac RepFunI 1);
+val term_map_type2 = result();
+
+
+(** term_size **)
+
+val term_size = standard (term_size_def RS def_term_rec);
+
+goalw Term.thy [term_size_def] "!!t A. t: term(A) ==> term_size(t) : nat";
+by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
+val term_size_type = result();
+
+
+(** reflect **)
+
+val reflect = standard (reflect_def RS def_term_rec);
+
+goalw Term.thy [reflect_def] "!!t A. t: term(A) ==> reflect(t) : term(A)";
+by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
+val reflect_type = result();
+
+(** preorder **)
+
+val preorder = standard (preorder_def RS def_term_rec);
+
+goalw Term.thy [preorder_def]
+    "!!t A. t: term(A) ==> preorder(t) : list(A)";
+by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
+val preorder_type = result();
+
+
+(** Term simplification **)
+
+val term_typechecks =
+    [term.Apply_I, term_map_type, term_map_type2, term_size_type, 
+     reflect_type, preorder_type];
+
+(*map_type2 and term_map_type2 instantiate variables*)
+val term_ss = list_ss 
+      addsimps [term_rec, term_map, term_size, reflect, preorder]
+      setsolver type_auto_tac (list_typechecks@term_typechecks);
+
+
+(** theorems about term_map **)
+
+goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
+val term_map_ident = result();
+
+goal Term.thy
+  "!!t A. 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 (term_ss addsimps [map_compose]) 1);
+val term_map_compose = result();
+
+goal Term.thy
+    "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
+val term_map_reflect = result();
+
+
+(** theorems about term_size **)
+
+goal Term.thy
+    "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
+val term_size_term_map = result();
+
+goal Term.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
+				    list_add_rev]) 1);
+val term_size_reflect = result();
+
+goal Term.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
+val term_size_length = result();
+
+
+(** theorems about reflect **)
+
+goal Term.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
+				    map_ident, rev_rev_ident]) 1);
+val reflect_reflect_ident = result();
+
+
+(** theorems about preorder **)
+
+goal Term.thy
+    "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
+val preorder_term_map = result();
+
+(** preorder(reflect(t)) = rev(postorder(t)) **)
+
+writeln"Reached end of file.";
diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Term.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Term.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,38 @@
+(*  Title: 	ZF/ex/Term.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Terms over an alphabet.
+Illustrates the list functor (essentially the same type as in Trees & Forests)
+*)
+
+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
+  "term(A)" = Apply ("a: A", "l: list(term(A))")
+  monos	      "[list_mono]"
+  type_intrs  "[list_univ RS subsetD]"
+
+rules
+  term_rec_def
+   "term_rec(t,d) == \
+\   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
+
+  term_map_def	"term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
+
+  term_size_def	"term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
+
+  reflect_def	"reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
+
+  preorder_def	"preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
+
+end