INSTALLATION OF INDUCTIVE DEFINITIONS
authorlcp
Thu, 25 Aug 1994 10:47:33 +0200
changeset 127 d9527f97246e
parent 126 872f866e630f
child 128 89669c58e506
INSTALLATION OF INDUCTIVE DEFINITIONS HOL/ex/MT.thy: now mentions dependence upon Sum.thy HOL/ex/Acc: new example, borrowed & adapted from ZF HOL/ex/Simult, ex/Term: updated refs to Sexp intr rules HOL/Sexp,List,LList,ex/Term: converted as follows node *set -> item Sexp -> sexp LList_corec -> <self> LList_ -> llist_ LList\> -> llist List_case -> <self> List_rec -> <self> List_ -> list_ List\> -> list Term_rec -> <self> Term_ -> term_ Term\> -> term
ex/Acc.ML
ex/Acc.thy
ex/PL.ML
ex/ROOT.ML
ex/Simult.ML
ex/Simult.thy
ex/Term.ML
ex/Term.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Acc.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -0,0 +1,63 @@
+(*  Title: 	HOL/ex/Acc
+    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.
+*)
+
+open Acc;
+
+(*The intended introduction rule*)
+val prems = goal Acc.thy
+    "[| !!b. <b,a>:r ==> b: acc(r) |] ==> a: acc(r)";
+by (fast_tac (set_cs addIs (prems @ 
+			    map (rewrite_rule [pred_def]) 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 (rewtac pred_def);
+by (fast_tac set_cs 1);
+val acc_downward = result();
+
+val [major,indhyp] = goal Acc.thy
+    "[| 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 indhyp 1);
+by (resolve_tac acc.intrs 1);
+by (rewtac pred_def);
+by (fast_tac set_cs 2);
+be (Int_lower1 RS Pow_mono RS subsetD) 1;
+val acc_induct = result();
+
+
+val [major] = goal Acc.thy "r <= Sigma(acc(r), %u. acc(r)) ==> wf(r)";
+by (rtac (major RS wfI) 1);
+by (etac acc.induct 1);
+by (rewtac pred_def);
+by (fast_tac set_cs 1);
+val acc_wfI = result();
+
+val [major] = goal Acc.thy "wf(r) ==> ALL x. <x,y>: r | <y,x>:r --> y: acc(r)";
+by (rtac (major RS wf_induct) 1);
+br (impI RS allI) 1;
+br accI 1;
+by (fast_tac set_cs 1);
+val acc_wfD_lemma = result();
+
+val [major] = goal Acc.thy "wf(r) ==> r <= Sigma(acc(r), %u. acc(r))";
+by (rtac subsetI 1);
+by (res_inst_tac [("p", "x")] PairE 1);
+by (fast_tac (set_cs addSIs [SigmaI,
+			     major RS acc_wfD_lemma RS spec RS mp]) 1);
+val acc_wfD = result();
+
+goal Acc.thy "wf(r)  =  (r <= Sigma(acc(r), %u. acc(r)))";
+by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
+val wf_acc_iff = result();
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Acc.thy	Thu Aug 25 10:47:33 1994 +0200
@@ -0,0 +1,26 @@
+(*  Title: 	HOL/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 + 
+
+consts
+  pred :: "['b, ('a * 'b)set] => 'a set"	(*Set of predecessors*)
+  acc  :: "('a * 'a)set => 'a set"		(*Accessible part*)
+
+defs
+  pred_def     "pred(x,r) == {y. <y,x>:r}"
+
+inductive "acc(r)"
+  intrs
+    pred    "pred(a,r): Pow(acc(r)) ==> a: acc(r)"
+  monos     "[Pow_mono]"
+
+end
--- a/ex/PL.ML	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/PL.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -101,8 +101,7 @@
 \     !!x. P(((x->false)->false)->x);			\
 \     !!x y. [| H |- x->y;  H |- x;  P(x->y);  P(x) |] ==> P(y) \
 \  |] ==> P(a)";
-by (rtac (major RS (thms_def RS def_induct)) 1);
-by (rtac thms_bnd_mono 1);
+by (rtac ([thms_def, thms_bnd_mono, major] MRS def_induct) 1);
 by (rewrite_tac rule_defs);
 by (fast_tac (set_cs addIs prems) 1);
 val conseq_induct = result();
@@ -267,7 +266,7 @@
 goal PL.thy "hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})";
 by (PL.pl.induct_tac "p" 1);
 by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN'
-              fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI])));
+              fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI])));
 val hyps_finite = result();
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
--- a/ex/ROOT.ML	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/ROOT.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -20,6 +20,7 @@
 time_use_thy "Puzzle";
 time_use_thy "NatSum";
 time_use     "ex/set.ML";
+time_use_thy "Acc";
 time_use_thy "PL";
 time_use_thy "Term";
 time_use_thy "Simult";
--- a/ex/Simult.ML	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Simult.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -3,13 +3,11 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For Simult.thy.
-
 Primitives for simultaneous recursive type definitions
   includes worked example of trees & forests
 
 This is essentially the same data structure that on ex/term.ML, which is
-simpler because it uses List as a new type former.  The approach in this
+simpler because it uses list as a new type former.  The approach in this
 file may be superior for other simultaneous recursions.
 *)
 
@@ -29,15 +27,15 @@
 by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
 val TF_mono = result();
 
-goalw Simult.thy [TF_def] "TF(Sexp) <= Sexp";
+goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [Sexp_NumbI,Sexp_In0I,Sexp_In1I,Sexp_SconsI]
+by (fast_tac (univ_cs addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
                       addSEs [PartE]) 1);
-val TF_Sexp = result();
+val TF_sexp = result();
 
-(* A <= Sexp ==> TF(A) <= Sexp *)
-val TF_subset_Sexp = standard
-    (TF_mono RS (TF_Sexp RSN (2,subset_trans)));
+(* A <= sexp ==> TF(A) <= sexp *)
+val TF_subset_sexp = standard
+    (TF_mono RS (TF_sexp RSN (2,subset_trans)));
 
 
 (** Elimination -- structural induction on the set TF **)
@@ -51,8 +49,7 @@
 \    !!M N. [| M:  Part(TF(A),In0);  N: Part(TF(A),In1);  R(M);  R(N) \
 \            |] ==> R(FCONS(M,N))    \
 \    |] ==> R(i)";
-by (rtac (major RS (TF_def RS def_induct)) 1);
-by (rtac TF_fun_mono 1);
+by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
 by (fast_tac (set_cs addIs (prems@[PartI])
 		       addEs [usumE, uprodE, PartE]) 1);
 val TF_induct = result();
@@ -228,19 +225,19 @@
 val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
 
 
-(*** TF_rec -- by wf recursion on pred_Sexp ***)
+(*** TF_rec -- by wf recursion on pred_sexp ***)
 
 val TF_rec_unfold =
-    wf_pred_Sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+    wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
 
 (** conversion rules for TF_rec **)
 
 goalw Simult.thy [TCONS_def]
-    "!!M N. [| M: Sexp;  N: Sexp |] ==> 	\
+    "!!M N. [| M: sexp;  N: sexp |] ==> 	\
 \           TF_rec(TCONS(M,N),b,c,d) = b(M, N, TF_rec(N,b,c,d))";
 by (rtac (TF_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Case_In0, Split]) 1);
-by (asm_simp_tac (pred_Sexp_ss addsimps [In0_def]) 1);
+by (asm_simp_tac (pred_sexp_ss addsimps [In0_def]) 1);
 val TF_rec_TCONS = result();
 
 goalw Simult.thy [FNIL_def] "TF_rec(FNIL,b,c,d) = c";
@@ -249,29 +246,29 @@
 val TF_rec_FNIL = result();
 
 goalw Simult.thy [FCONS_def]
- "!!M N. [| M: Sexp;  N: Sexp |] ==> 	\
+ "!!M N. [| M: sexp;  N: sexp |] ==> 	\
 \        TF_rec(FCONS(M,N),b,c,d) = d(M, N, TF_rec(M,b,c,d), TF_rec(N,b,c,d))";
 by (rtac (TF_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
-by (asm_simp_tac (pred_Sexp_ss addsimps [CONS_def,In1_def]) 1);
+by (asm_simp_tac (pred_sexp_ss addsimps [CONS_def,In1_def]) 1);
 val TF_rec_FCONS = result();
 
 
 (*** tree_rec, forest_rec -- by TF_rec ***)
 
-val Rep_Tree_in_Sexp =
-    [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+val Rep_Tree_in_sexp =
+    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
      Rep_Tree] MRS subsetD;
-val Rep_Forest_in_Sexp =
-    [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+val Rep_Forest_in_sexp =
+    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
      Rep_Forest] MRS subsetD;
 
 val tf_rec_simps = [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
 		    TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
 		    Rep_Tree_inverse, Rep_Forest_inverse,
 		    Abs_Tree_inverse, Abs_Forest_inverse,
-		    inj_Leaf, Inv_f_f, Sexp_LeafI, range_eqI,
-		    Rep_Tree_in_Sexp, Rep_Forest_in_Sexp];
+		    inj_Leaf, Inv_f_f, sexp.LeafI, range_eqI,
+		    Rep_Tree_in_sexp, Rep_Forest_in_sexp];
 val tf_rec_ss = HOL_ss addsimps tf_rec_simps;
 
 goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
--- a/ex/Simult.thy	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Simult.thy	Thu Aug 25 10:47:33 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	HOL/ex/simult
+(*  Title: 	HOL/ex/Simult
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -6,8 +6,11 @@
 A simultaneous recursive type definition: trees & forests
 
 This is essentially the same data structure that on ex/term.ML, which is
-simpler because it uses List as a new type former.  The approach in this
+simpler because it uses list as a new type former.  The approach in this
 file may be superior for other simultaneous recursions.
+
+The inductive definition package does not help defining this sort of mutually
+recursive data structure because it uses Inl, Inr instead of In0, In1.
 *)
 
 Simult = List +
@@ -18,27 +21,38 @@
 arities  tree,forest :: (term)term
 
 consts
-  TF          :: "'a node set set => 'a node set set"
-  FNIL        :: "'a node set"
-  TCONS,FCONS :: "['a node set, 'a node set] => 'a node set"
-  Rep_Tree    :: "'a tree => 'a node set"
-  Abs_Tree    :: "'a node set => 'a tree"
-  Rep_Forest  :: "'a forest => 'a node set"
-  Abs_Forest  :: "'a node set => 'a forest"
+  TF          :: "'a item set => 'a item set"
+  FNIL        :: "'a item"
+  TCONS,FCONS :: "['a item, 'a item] => 'a item"
+  Rep_Tree    :: "'a tree => 'a item"
+  Abs_Tree    :: "'a item => 'a tree"
+  Rep_Forest  :: "'a forest => 'a item"
+  Abs_Forest  :: "'a item => 'a forest"
   Tcons       :: "['a, 'a forest] => 'a tree"
   Fcons       :: "['a tree, 'a forest] => 'a forest"
   Fnil        :: "'a forest"
-  TF_rec      :: "['a node set, ['a node set , 'a node set, 'b]=>'b,     \
-\                 'b, ['a node set , 'a node set, 'b, 'b]=>'b] => 'b"
+  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     \
+\                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
   tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          \
 \                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
   forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        \
 \                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
 
-rules
+defs
+     (*the concrete constants*)
+  TCONS_def 	"TCONS(M,N) == In0(M $ N)"
+  FNIL_def	"FNIL       == In1(NIL)"
+  FCONS_def	"FCONS(M,N) == In1(CONS(M,N))"
+     (*the abstract constants*)
+  Tcons_def 	"Tcons(a,ts) == Abs_Tree(TCONS(Leaf(a), Rep_Forest(ts)))"
+  Fnil_def  	"Fnil        == Abs_Forest(FNIL)"
+  Fcons_def 	"Fcons(t,ts) == Abs_Forest(FCONS(Rep_Tree(t), Rep_Forest(ts)))"
+
   TF_def	"TF(A) == lfp(%Z. A <*> Part(Z,In1) \
 \                           <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
-    (*faking a type definition for tree...*)
+
+rules
+  (*faking a type definition for tree...*)
   Rep_Tree 	   "Rep_Tree(n): Part(TF(range(Leaf)),In0)"
   Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
   Abs_Tree_inverse "z: Part(TF(range(Leaf)),In0) ==> Rep_Tree(Abs_Tree(z)) = z"
@@ -48,18 +62,11 @@
   Abs_Forest_inverse 
 	"z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z"
 
-     (*the concrete constants*)
-  TCONS_def 	"TCONS(M,N) == In0(M $ N)"
-  FNIL_def	"FNIL       == In1(NIL)"
-  FCONS_def	"FCONS(M,N) == In1(CONS(M,N))"
-     (*the abstract constants*)
-  Tcons_def 	"Tcons(a,ts) == Abs_Tree(TCONS(Leaf(a), Rep_Forest(ts)))"
-  Fnil_def  	"Fnil        == Abs_Forest(FNIL)"
-  Fcons_def 	"Fcons(t,ts) == Abs_Forest(FCONS(Rep_Tree(t), Rep_Forest(ts)))"
 
+defs
      (*recursion*)
   TF_rec_def	
-   "TF_rec(M,b,c,d) == wfrec(trancl(pred_Sexp), M, 			\
+   "TF_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, 			\
 \               Case(Split(%x y g. b(x,y,g(y))),		\
 \	              List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
 
--- a/ex/Term.ML	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Term.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -1,9 +1,9 @@
-(*  Title: 	HOL/ex/term
+(*  Title: 	HOL/ex/Term
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-For term.thy.  illustrates List functor
+Terms over a given alphabet -- function applications; illustrates list functor
   (essentially the same type as in Trees & Forests)
 *)
 
@@ -11,85 +11,83 @@
 
 (*** Monotonicity and unfolding of the function ***)
 
-goal Term.thy "mono(%Z.  A <*> List(Z))";
-by (REPEAT (ares_tac [monoI, subset_refl, List_mono, uprod_mono] 1));
-val Term_fun_mono = result();
+goal Term.thy "term(A) = A <*> list(term(A))";
+by (fast_tac (univ_cs addSIs (equalityI :: term.intrs)
+                      addEs [term.elim]) 1);
+val term_unfold = result();
 
-val Term_unfold = Term_fun_mono RS (Term_def RS def_lfp_Tarski);
-
-(*This justifies using Term in other recursive type definitions*)
-goalw Term.thy [Term_def] "!!A B. A<=B ==> Term(A) <= Term(B)";
-by (REPEAT (ares_tac [lfp_mono, subset_refl, List_mono, uprod_mono] 1));
-val Term_mono = result();
+(*This justifies using term in other recursive type definitions*)
+goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
+by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
+val term_mono = result();
 
-(** Type checking rules -- Term creates well-founded sets **)
+(** Type checking -- term creates well-founded sets **)
 
-val prems = goalw Term.thy [Term_def] "Term(Sexp) <= Sexp";
+goalw Term.thy term.defs "term(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [Sexp_SconsI, List_Sexp RS subsetD]) 1);
-val Term_Sexp = result();
+by (fast_tac (univ_cs addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
+val term_sexp = result();
 
-(* A <= Sexp ==> Term(A) <= Sexp *)
-val Term_subset_Sexp = standard
-    (Term_mono RS (Term_Sexp RSN (2,subset_trans)));
+(* A <= sexp ==> term(A) <= sexp *)
+val term_subset_sexp = standard ([term_mono, term_sexp] MRS subset_trans);
 
 
-(** Elimination -- structural induction on the set Term(A) **)
+(** Elimination -- structural induction on the set term(A) **)
 
-(*Induction for the set Term(A) *)
+(*Induction for the set term(A) *)
 val [major,minor] = goal Term.thy 
-    "[| M: Term(A);  \
-\       !!x zs. [| x: A;  zs: List(Term(A));  zs: List({x.R(x)}) \
+    "[| M: term(A);  \
+\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x.R(x)}) \
 \               |] ==> R(x$zs)  \
 \    |] ==> R(M)";
-by (rtac (major RS (Term_def RS def_induct)) 1);
-by (rtac Term_fun_mono 1);
-by (REPEAT (eresolve_tac ([uprodE, ssubst, minor] @
- 		([Int_lower1,Int_lower2] RL [List_mono RS subsetD])) 1));
-val Term_induct = result();
+by (rtac (major RS term.induct) 1);
+by (REPEAT (eresolve_tac ([minor] @
+ 		([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
+(*Proof could also use  mono_Int RS subsetD RS IntE *)
+val term_induct = result();
 
-(*Induction on Term(A) followed by induction on List *)
+(*Induction on term(A) followed by induction on list *)
 val major::prems = goal Term.thy
-    "[| M: Term(A);  \
+    "[| M: term(A);  \
 \       !!x.      [| x: A |] ==> R(x$NIL);  \
-\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x$zs)  \
+\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R(x$zs)  \
 \                 |] ==> R(x $ CONS(z,zs))  \
 \    |] ==> R(M)";
-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 (REPEAT (ares_tac prems 1));
-val Term_induct2 = result();
+val term_induct2 = result();
 
 (*** Structural Induction on the abstract type 'a term ***)
 
 val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons];
 
-val Rep_Term_in_Sexp =
-    Rep_Term RS (range_Leaf_subset_Sexp RS Term_subset_Sexp RS subsetD);
+val Rep_term_in_sexp =
+    Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
 
 (*Induction for the abstract type 'a term*)
-val prems = goalw Term.thy [App_def,Rep_TList_def,Abs_TList_def]
+val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
     "[| !!x ts. list_all(R,ts) ==> R(App(x,ts))  \
 \    |] ==> R(t)";
-by (rtac (Rep_Term_inverse RS subst) 1);   (*types force good instantiation*)
-by (res_inst_tac [("P","Rep_Term(t) : Sexp")] conjunct2 1);
-by (rtac (Rep_Term RS Term_induct) 1);
-by (REPEAT (ares_tac [conjI, Sexp_SconsI, Term_subset_Sexp RS 
-    List_subset_Sexp,range_Leaf_subset_Sexp] 1
+by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
+by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
+by (rtac (Rep_term RS term_induct) 1);
+by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
+    list_subset_sexp, range_Leaf_subset_sexp] 1
      ORELSE etac rev_subsetD 1));
-by (eres_inst_tac [("A1","Term(?u)"), ("f1","Rep_Term"), ("g1","Abs_Term")]
+by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")]
     	(Abs_map_inverse RS subst) 1);
-by (rtac (range_Leaf_subset_Sexp RS Term_subset_Sexp) 1);
-by (etac Abs_Term_inverse 1);
+by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1);
+by (etac Abs_term_inverse 1);
 by (etac rangeE 1);
 by (hyp_subst_tac 1);
 by (resolve_tac prems 1);
-by (etac List_induct 1);
+by (etac list.induct 1);
 by (etac CollectE 2);
 by (stac Abs_map_CONS 2);
 by (etac conjunct1 2);
 by (etac rev_subsetD 2);
-by (rtac List_subset_Sexp 2);
+by (rtac list_subset_sexp 2);
 by (fast_tac set_cs 2);
 by (ALLGOALS (asm_simp_tac list_all_ss));
 val term_induct = result();
@@ -111,66 +109,56 @@
 	   rename_last_tac a ["1","s"] (i+1)];
 
 
-(** Introduction rule for Term **)
 
-(* c : A <*> List(Term(A)) ==> c : Term(A) *)
-val TermI = standard (Term_unfold RS equalityD2 RS subsetD);
-
-(*The constant APP is not declared; it is simply . *)
-val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M$N : Term(A)";
-by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1));
-val APP_I = result();
-
-
-(*** Term_rec -- by wf recursion on pred_Sexp ***)
+(*** Term_rec -- by wf recursion on pred_sexp ***)
 
 val Term_rec_unfold =
-    wf_pred_Sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
+    wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
 
 (** conversion rules **)
 
 val [prem] = goal Term.thy
-    "N: List(Term(A)) ==>  \
-\    !M. <N,M>: pred_Sexp^+ --> \
-\        Abs_map(cut(h, pred_Sexp^+, M), N) = \
+    "N: list(term(A)) ==>  \
+\    !M. <N,M>: pred_sexp^+ --> \
+\        Abs_map(cut(h, pred_sexp^+, M), N) = \
 \        Abs_map(h,N)";
-by (rtac (prem RS List_induct) 1);
+by (rtac (prem RS list.induct) 1);
 by (simp_tac list_all_ss 1);
 by (strip_tac 1);
-by (etac (pred_Sexp_CONS_D RS conjE) 1);
-by (asm_simp_tac (list_all_ss addsimps [trancl_pred_SexpD1, cut_apply]) 1);
+by (etac (pred_sexp_CONS_D RS conjE) 1);
+by (asm_simp_tac (list_all_ss addsimps [trancl_pred_sexpD1, cut_apply]) 1);
 val Abs_map_lemma = result();
 
-val [prem1,prem2,A_subset_Sexp] = goal Term.thy
-    "[| M: Sexp;  N: List(Term(A));  A<=Sexp |] ==> \
+val [prem1,prem2,A_subset_sexp] = goal Term.thy
+    "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
 \    Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
 by (rtac (Term_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps
       [Split,
-       prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl,
-       prem1, prem2 RS rev_subsetD, List_subset_Sexp,
-       Term_subset_Sexp, A_subset_Sexp])1);
+       prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
+       prem1, prem2 RS rev_subsetD, list_subset_sexp,
+       term_subset_sexp, A_subset_sexp])1);
 val Term_rec = result();
 
 (*** term_rec -- by Term_rec ***)
 
 local
   val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy)
-                        [("f","Rep_Term")] Rep_map_type;
-  val Rep_TList = Rep_Term RS Rep_map_type1;
-  val Rep_Term_rec = range_Leaf_subset_Sexp RSN (2,Rep_TList RSN(2,Term_rec));
+                        [("f","Rep_term")] Rep_map_type;
+  val Rep_Tlist = Rep_term RS Rep_map_type1;
+  val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
 
-  (*Now avoids conditional rewriting with the premise N: List(Term(A)),
+  (*Now avoids conditional rewriting with the premise N: list(term(A)),
     since A will be uninstantiated and will cause rewriting to fail. *)
   val term_rec_ss = HOL_ss 
-      addsimps [Rep_TList RS (rangeI RS APP_I RS Abs_Term_inverse),  
-	       Rep_Term_in_Sexp, Rep_Term_rec, Rep_Term_inverse,
+      addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
+	       Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse,
 	       inj_Leaf, Inv_f_f,
-	       Abs_Rep_map, map_ident, Sexp_LeafI]
+	       Abs_Rep_map, map_ident, sexp.LeafI]
 in
 
 val term_rec = prove_goalw Term.thy
-	 [term_rec_def, App_def, Rep_TList_def, Abs_TList_def]
+	 [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
     "term_rec(App(f,ts), d) = d(f, ts, map (%t. term_rec(t,d), ts))"
  (fn _ => [simp_tac term_rec_ss 1])
 
--- a/ex/Term.thy	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Term.thy	Thu Aug 25 10:47:33 1994 +0200
@@ -1,12 +1,12 @@
-(*  Title: 	HOL/ex/term
+(*  Title: 	HOL/ex/Term
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Terms over a given alphabet -- function applications; illustrates List functor
+Terms over a given alphabet -- function applications; illustrates list functor
   (essentially the same type as in Trees & Forests)
 
-There is no constructor APP because it is simply cons (.) 
+There is no constructor APP because it is simply cons ($) 
 *)
 
 Term = List +
@@ -16,33 +16,40 @@
 arities term :: (term)term
 
 consts
-  Term		:: "'a node set set => 'a node set set"
-  Rep_Term	:: "'a term => 'a node set"
-  Abs_Term	:: "'a node set => 'a term"
-  Rep_TList	:: "'a term list => 'a node set"
-  Abs_TList	:: "'a node set => 'a term list"
+  term		:: "'a item set => 'a item set"
+  Rep_term	:: "'a term => 'a item"
+  Abs_term	:: "'a item => 'a term"
+  Rep_Tlist	:: "'a term list => 'a item"
+  Abs_Tlist	:: "'a item => 'a term list"
   App		:: "['a, ('a term)list] => 'a term"
-  Term_rec	::
-    "['a node set, ['a node set , 'a node set, 'b list]=>'b] => 'b"
+  Term_rec	:: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
   term_rec	:: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
 
-rules
-  Term_def		"Term(A) == lfp(%Z.  A <*> List(Z))"
-    (*faking a type definition for term...*)
-  Rep_Term 		"Rep_Term(n): Term(range(Leaf))"
-  Rep_Term_inverse 	"Abs_Term(Rep_Term(t)) = t"
-  Abs_Term_inverse 	"M: Term(range(Leaf)) ==> Rep_Term(Abs_Term(M)) = M"
-    (*defining abstraction/representation functions for term list...*)
-  Rep_TList_def	"Rep_TList == Rep_map(Rep_Term)"
-  Abs_TList_def	"Abs_TList == Abs_map(Abs_Term)"
-    (*defining the abstract constants*)
-  App_def 	"App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))"
-     (*list recursion*)
+inductive "term(A)"
+  intrs
+    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
+  monos   "[list_mono]"
+
+defs
+  (*defining abstraction/representation functions for term list...*)
+  Rep_Tlist_def	"Rep_Tlist == Rep_map(Rep_term)"
+  Abs_Tlist_def	"Abs_Tlist == Abs_map(Abs_term)"
+
+  (*defining the abstract constants*)
+  App_def 	"App(a,ts) == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
+
+  (*list recursion*)
   Term_rec_def	
-   "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
+   "Term_rec(M,d) == wfrec(trancl(pred_sexp),  M, \
 \            Split(%x y g. d(x,y, Abs_map(g,y))))"
 
   term_rec_def
    "term_rec(t,d) == \
-\   Term_rec(Rep_Term(t), %x y r. d(Inv(Leaf,x), Abs_TList(y), r))"
+\   Term_rec(Rep_term(t), %x y r. d(Inv(Leaf,x), Abs_Tlist(y), r))"
+
+rules
+    (*faking a type definition for term...*)
+  Rep_term 		"Rep_term(n): term(range(Leaf))"
+  Rep_term_inverse 	"Abs_term(Rep_term(t)) = t"
+  Abs_term_inverse 	"M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
 end