sample datatype defs now use datatype_intrs, datatype_elims
authorlcp
Fri Oct 22 11:42:02 1993 +0100 (1993-10-22)
changeset 71729fe026c5f3
parent 70 8a29f8b4aca1
child 72 099d949fe467
sample datatype defs now use datatype_intrs, datatype_elims
src/ZF/ex/BT.ML
src/ZF/ex/Bin.ML
src/ZF/ex/Comb.ML
src/ZF/ex/Data.ML
src/ZF/ex/Enum.ML
src/ZF/ex/LList.ML
src/ZF/ex/LList_Eq.ML
src/ZF/ex/ListN.ML
src/ZF/ex/Primrec0.ML
src/ZF/ex/Primrec0.thy
src/ZF/ex/Prop.ML
src/ZF/ex/TF.ML
src/ZF/ex/Term.ML
src/ZF/ex/bin.ML
src/ZF/ex/bt.ML
src/ZF/ex/comb.ML
src/ZF/ex/data.ML
src/ZF/ex/enum.ML
src/ZF/ex/listn.ML
src/ZF/ex/llist.ML
src/ZF/ex/llist_eq.ML
src/ZF/ex/primrec0.ML
src/ZF/ex/primrec0.thy
src/ZF/ex/prop.ML
src/ZF/ex/term.ML
src/ZF/ex/tf.ML
     1.1 --- a/src/ZF/ex/BT.ML	Fri Oct 22 11:34:41 1993 +0100
     1.2 +++ b/src/ZF/ex/BT.ML	Fri Oct 22 11:42:02 1993 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  	  ["Lf : bt(A)",
     1.5  	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
     1.6    val monos = [];
     1.7 -  val type_intrs = data_typechecks
     1.8 +  val type_intrs = datatype_intrs
     1.9    val type_elims = []);
    1.10  
    1.11  val [LfI, BrI] = BT.intrs;
     2.1 --- a/src/ZF/ex/Bin.ML	Fri Oct 22 11:34:41 1993 +0100
     2.2 +++ b/src/ZF/ex/Bin.ML	Fri Oct 22 11:42:02 1993 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4  	   "Minus : bin",
     2.5  	   "[| w: bin;  b: bool |] ==> w$$b : bin"];
     2.6    val monos = [];
     2.7 -  val type_intrs = data_typechecks @ [bool_into_univ];
     2.8 +  val type_intrs = datatype_intrs @ [bool_into_univ];
     2.9    val type_elims = []);
    2.10  
    2.11  (*Perform induction on l, then prove the major premise using prems. *)
     3.1 --- a/src/ZF/ex/Comb.ML	Fri Oct 22 11:34:41 1993 +0100
     3.2 +++ b/src/ZF/ex/Comb.ML	Fri Oct 22 11:42:02 1993 +0100
     3.3 @@ -25,7 +25,7 @@
     3.4  	   "S : comb",
     3.5  	   "[| p: comb;  q: comb |] ==> p#q : comb"];
     3.6    val monos = [];
     3.7 -  val type_intrs = data_typechecks;
     3.8 +  val type_intrs = datatype_intrs;
     3.9    val type_elims = []);
    3.10  
    3.11  val [K_comb,S_comb,Ap_comb] = Comb.intrs;
     4.1 --- a/src/ZF/ex/Data.ML	Fri Oct 22 11:34:41 1993 +0100
     4.2 +++ b/src/ZF/ex/Data.ML	Fri Oct 22 11:42:02 1993 +0100
     4.3 @@ -23,8 +23,8 @@
     4.4  	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
     4.5  	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
     4.6    val monos = [];
     4.7 -  val type_intrs = data_typechecks
     4.8 -  val type_elims = data_elims);
     4.9 +  val type_intrs = datatype_intrs
    4.10 +  val type_elims = datatype_elims);
    4.11  
    4.12  
    4.13  (**  Lemmas to justify using "data" in other recursive type definitions **)
     5.1 --- a/src/ZF/ex/Enum.ML	Fri Oct 22 11:34:41 1993 +0100
     5.2 +++ b/src/ZF/ex/Enum.ML	Fri Oct 22 11:42:02 1993 +0100
     5.3 @@ -24,7 +24,7 @@
     5.4    val ext = None
     5.5    val sintrs = map (fn const => const ^ " : enum") consts;
     5.6    val monos = [];
     5.7 -  val type_intrs = data_typechecks
     5.8 +  val type_intrs = datatype_intrs
     5.9    val type_elims = []);
    5.10  
    5.11  goal Enum.thy "con59 ~= con60";
     6.1 --- a/src/ZF/ex/LList.ML	Fri Oct 22 11:34:41 1993 +0100
     6.2 +++ b/src/ZF/ex/LList.ML	Fri Oct 22 11:42:02 1993 +0100
     6.3 @@ -21,7 +21,7 @@
     6.4        ["LNil : llist(A)",
     6.5         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
     6.6    val monos = [];
     6.7 -  val type_intrs = co_data_typechecks
     6.8 +  val type_intrs = co_datatype_intrs
     6.9    val type_elims = []);
    6.10    
    6.11  val [LNilI, LConsI] = LList.intrs;
    6.12 @@ -49,7 +49,7 @@
    6.13    QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
    6.14  
    6.15  val quniv_cs = ZF_cs addSIs in_quniv_rls 
    6.16 -                     addIs (Int_quniv_in_quniv::co_data_typechecks);
    6.17 +                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
    6.18  
    6.19  (*Keep unfolding the lazy list until the induction hypothesis applies*)
    6.20  goal LList.thy
     7.1 --- a/src/ZF/ex/LList_Eq.ML	Fri Oct 22 11:34:41 1993 +0100
     7.2 +++ b/src/ZF/ex/LList_Eq.ML	Fri Oct 22 11:42:02 1993 +0100
     7.3 @@ -10,7 +10,7 @@
     7.4  
     7.5  structure LList_Eq = Co_Inductive_Fun
     7.6   (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
     7.7 -  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
     7.8 +  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
     7.9    val sintrs = 
    7.10        ["<LNil; LNil> : lleq(A)",
    7.11         "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
    7.12 @@ -21,7 +21,7 @@
    7.13  
    7.14  (** Alternatives for above:
    7.15    val con_defs = LList.con_defs
    7.16 -  val type_intrs = co_data_typechecks
    7.17 +  val type_intrs = co_datatype_intrs
    7.18    val type_elims = [quniv_QPair_E]
    7.19  **)
    7.20  
     8.1 --- a/src/ZF/ex/ListN.ML	Fri Oct 22 11:34:41 1993 +0100
     8.2 +++ b/src/ZF/ex/ListN.ML	Fri Oct 22 11:42:02 1993 +0100
     8.3 @@ -23,8 +23,8 @@
     8.4  val listn_induct = standard 
     8.5      (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
     8.6  
     8.7 -val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
     8.8 -by (rtac (major RS List.induct) 1);
     8.9 +goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
    8.10 +by (etac List.induct 1);
    8.11  by (ALLGOALS (asm_simp_tac list_ss));
    8.12  by (REPEAT (ares_tac ListN.intrs 1));
    8.13  val list_into_listn = result();
    8.14 @@ -47,6 +47,12 @@
    8.15  by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
    8.16  val listn_mono = result();
    8.17  
    8.18 +goal ListN.thy
    8.19 +    "!!n l. [| <n,l> : listn(A);  <n',l'> : listn(A) |] ==> \
    8.20 +\           <n#+n', l@l'> : listn(A)";
    8.21 +by (etac listn_induct 1);
    8.22 +by (ALLGOALS (asm_simp_tac (list_ss addsimps ListN.intrs)));
    8.23 +val listn_append = result();
    8.24 +
    8.25  val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
    8.26  and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)";
    8.27 -
     9.1 --- a/src/ZF/ex/Primrec0.ML	Fri Oct 22 11:34:41 1993 +0100
     9.2 +++ b/src/ZF/ex/Primrec0.ML	Fri Oct 22 11:42:02 1993 +0100
     9.3 @@ -9,6 +9,9 @@
     9.4  Nora Szasz, 
     9.5  A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
     9.6  In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
     9.7 +
     9.8 +See also E. Mendelson, Introduction to Mathematical Logic.
     9.9 +(Van Nostrand, 1964), page 250, exercise 11.
    9.10  *)
    9.11  
    9.12  open Primrec0;
    10.1 --- a/src/ZF/ex/Primrec0.thy	Fri Oct 22 11:34:41 1993 +0100
    10.2 +++ b/src/ZF/ex/Primrec0.thy	Fri Oct 22 11:42:02 1993 +0100
    10.3 @@ -9,6 +9,9 @@
    10.4  Nora Szasz, 
    10.5  A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
    10.6  In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
    10.7 +
    10.8 +See also E. Mendelson, Introduction to Mathematical Logic.
    10.9 +(Van Nostrand, 1964), page 250, exercise 11.
   10.10  *)
   10.11  
   10.12  Primrec0 = ListFn +
    11.1 --- a/src/ZF/ex/Prop.ML	Fri Oct 22 11:34:41 1993 +0100
    11.2 +++ b/src/ZF/ex/Prop.ML	Fri Oct 22 11:42:02 1993 +0100
    11.3 @@ -24,7 +24,7 @@
    11.4  	   "n: nat ==> #n : prop",
    11.5  	   "[| p: prop;  q: prop |] ==> p=>q : prop"];
    11.6    val monos = [];
    11.7 -  val type_intrs = data_typechecks;
    11.8 +  val type_intrs = datatype_intrs;
    11.9    val type_elims = []);
   11.10  
   11.11  val [FlsI,VarI,ImpI] = Prop.intrs;
    12.1 --- a/src/ZF/ex/TF.ML	Fri Oct 22 11:34:41 1993 +0100
    12.2 +++ b/src/ZF/ex/TF.ML	Fri Oct 22 11:42:02 1993 +0100
    12.3 @@ -21,8 +21,8 @@
    12.4  	   "Fnil : forest(A)",
    12.5  	   "[| t: tree(A);  tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
    12.6    val monos = [];
    12.7 -  val type_intrs = data_typechecks
    12.8 -  val type_elims = data_elims);
    12.9 +  val type_intrs = datatype_intrs
   12.10 +  val type_elims = datatype_elims);
   12.11  
   12.12  val [TconsI, FnilI, FconsI] = TF.intrs;
   12.13  
   12.14 @@ -44,9 +44,9 @@
   12.15  
   12.16  (*The (refl RS conjI RS exI RS exI) avoids considerable search!*)
   12.17  val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI]
   12.18 -                    addIs data_typechecks
   12.19 +                    addIs datatype_intrs
   12.20                      addDs [TF.dom_subset RS subsetD]
   12.21 -	            addSEs ([PartE] @ data_elims @ TF.free_SEs);
   12.22 +	            addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
   12.23  
   12.24  goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
   12.25  by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
    13.1 --- a/src/ZF/ex/Term.ML	Fri Oct 22 11:34:41 1993 +0100
    13.2 +++ b/src/ZF/ex/Term.ML	Fri Oct 22 11:42:02 1993 +0100
    13.3 @@ -16,7 +16,7 @@
    13.4    val ext = None
    13.5    val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
    13.6    val monos = [list_mono];
    13.7 -  val type_intrs = data_typechecks;
    13.8 +  val type_intrs = datatype_intrs;
    13.9    val type_elims = [make_elim (list_univ RS subsetD)]);
   13.10  
   13.11  val [ApplyI] = Term.intrs;
    14.1 --- a/src/ZF/ex/bin.ML	Fri Oct 22 11:34:41 1993 +0100
    14.2 +++ b/src/ZF/ex/bin.ML	Fri Oct 22 11:42:02 1993 +0100
    14.3 @@ -20,7 +20,7 @@
    14.4  	   "Minus : bin",
    14.5  	   "[| w: bin;  b: bool |] ==> w$$b : bin"];
    14.6    val monos = [];
    14.7 -  val type_intrs = data_typechecks @ [bool_into_univ];
    14.8 +  val type_intrs = datatype_intrs @ [bool_into_univ];
    14.9    val type_elims = []);
   14.10  
   14.11  (*Perform induction on l, then prove the major premise using prems. *)
    15.1 --- a/src/ZF/ex/bt.ML	Fri Oct 22 11:34:41 1993 +0100
    15.2 +++ b/src/ZF/ex/bt.ML	Fri Oct 22 11:42:02 1993 +0100
    15.3 @@ -17,7 +17,7 @@
    15.4  	  ["Lf : bt(A)",
    15.5  	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
    15.6    val monos = [];
    15.7 -  val type_intrs = data_typechecks
    15.8 +  val type_intrs = datatype_intrs
    15.9    val type_elims = []);
   15.10  
   15.11  val [LfI, BrI] = BT.intrs;
    16.1 --- a/src/ZF/ex/comb.ML	Fri Oct 22 11:34:41 1993 +0100
    16.2 +++ b/src/ZF/ex/comb.ML	Fri Oct 22 11:42:02 1993 +0100
    16.3 @@ -25,7 +25,7 @@
    16.4  	   "S : comb",
    16.5  	   "[| p: comb;  q: comb |] ==> p#q : comb"];
    16.6    val monos = [];
    16.7 -  val type_intrs = data_typechecks;
    16.8 +  val type_intrs = datatype_intrs;
    16.9    val type_elims = []);
   16.10  
   16.11  val [K_comb,S_comb,Ap_comb] = Comb.intrs;
    17.1 --- a/src/ZF/ex/data.ML	Fri Oct 22 11:34:41 1993 +0100
    17.2 +++ b/src/ZF/ex/data.ML	Fri Oct 22 11:42:02 1993 +0100
    17.3 @@ -23,8 +23,8 @@
    17.4  	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
    17.5  	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
    17.6    val monos = [];
    17.7 -  val type_intrs = data_typechecks
    17.8 -  val type_elims = data_elims);
    17.9 +  val type_intrs = datatype_intrs
   17.10 +  val type_elims = datatype_elims);
   17.11  
   17.12  
   17.13  (**  Lemmas to justify using "data" in other recursive type definitions **)
    18.1 --- a/src/ZF/ex/enum.ML	Fri Oct 22 11:34:41 1993 +0100
    18.2 +++ b/src/ZF/ex/enum.ML	Fri Oct 22 11:42:02 1993 +0100
    18.3 @@ -24,7 +24,7 @@
    18.4    val ext = None
    18.5    val sintrs = map (fn const => const ^ " : enum") consts;
    18.6    val monos = [];
    18.7 -  val type_intrs = data_typechecks
    18.8 +  val type_intrs = datatype_intrs
    18.9    val type_elims = []);
   18.10  
   18.11  goal Enum.thy "con59 ~= con60";
    19.1 --- a/src/ZF/ex/listn.ML	Fri Oct 22 11:34:41 1993 +0100
    19.2 +++ b/src/ZF/ex/listn.ML	Fri Oct 22 11:42:02 1993 +0100
    19.3 @@ -23,8 +23,8 @@
    19.4  val listn_induct = standard 
    19.5      (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
    19.6  
    19.7 -val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
    19.8 -by (rtac (major RS List.induct) 1);
    19.9 +goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
   19.10 +by (etac List.induct 1);
   19.11  by (ALLGOALS (asm_simp_tac list_ss));
   19.12  by (REPEAT (ares_tac ListN.intrs 1));
   19.13  val list_into_listn = result();
   19.14 @@ -47,6 +47,12 @@
   19.15  by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
   19.16  val listn_mono = result();
   19.17  
   19.18 +goal ListN.thy
   19.19 +    "!!n l. [| <n,l> : listn(A);  <n',l'> : listn(A) |] ==> \
   19.20 +\           <n#+n', l@l'> : listn(A)";
   19.21 +by (etac listn_induct 1);
   19.22 +by (ALLGOALS (asm_simp_tac (list_ss addsimps ListN.intrs)));
   19.23 +val listn_append = result();
   19.24 +
   19.25  val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
   19.26  and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)";
   19.27 -
    20.1 --- a/src/ZF/ex/llist.ML	Fri Oct 22 11:34:41 1993 +0100
    20.2 +++ b/src/ZF/ex/llist.ML	Fri Oct 22 11:42:02 1993 +0100
    20.3 @@ -21,7 +21,7 @@
    20.4        ["LNil : llist(A)",
    20.5         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
    20.6    val monos = [];
    20.7 -  val type_intrs = co_data_typechecks
    20.8 +  val type_intrs = co_datatype_intrs
    20.9    val type_elims = []);
   20.10    
   20.11  val [LNilI, LConsI] = LList.intrs;
   20.12 @@ -49,7 +49,7 @@
   20.13    QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
   20.14  
   20.15  val quniv_cs = ZF_cs addSIs in_quniv_rls 
   20.16 -                     addIs (Int_quniv_in_quniv::co_data_typechecks);
   20.17 +                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
   20.18  
   20.19  (*Keep unfolding the lazy list until the induction hypothesis applies*)
   20.20  goal LList.thy
    21.1 --- a/src/ZF/ex/llist_eq.ML	Fri Oct 22 11:34:41 1993 +0100
    21.2 +++ b/src/ZF/ex/llist_eq.ML	Fri Oct 22 11:42:02 1993 +0100
    21.3 @@ -10,7 +10,7 @@
    21.4  
    21.5  structure LList_Eq = Co_Inductive_Fun
    21.6   (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
    21.7 -  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
    21.8 +  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
    21.9    val sintrs = 
   21.10        ["<LNil; LNil> : lleq(A)",
   21.11         "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
   21.12 @@ -21,7 +21,7 @@
   21.13  
   21.14  (** Alternatives for above:
   21.15    val con_defs = LList.con_defs
   21.16 -  val type_intrs = co_data_typechecks
   21.17 +  val type_intrs = co_datatype_intrs
   21.18    val type_elims = [quniv_QPair_E]
   21.19  **)
   21.20  
    22.1 --- a/src/ZF/ex/primrec0.ML	Fri Oct 22 11:34:41 1993 +0100
    22.2 +++ b/src/ZF/ex/primrec0.ML	Fri Oct 22 11:42:02 1993 +0100
    22.3 @@ -9,6 +9,9 @@
    22.4  Nora Szasz, 
    22.5  A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
    22.6  In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
    22.7 +
    22.8 +See also E. Mendelson, Introduction to Mathematical Logic.
    22.9 +(Van Nostrand, 1964), page 250, exercise 11.
   22.10  *)
   22.11  
   22.12  open Primrec0;
    23.1 --- a/src/ZF/ex/primrec0.thy	Fri Oct 22 11:34:41 1993 +0100
    23.2 +++ b/src/ZF/ex/primrec0.thy	Fri Oct 22 11:42:02 1993 +0100
    23.3 @@ -9,6 +9,9 @@
    23.4  Nora Szasz, 
    23.5  A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
    23.6  In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
    23.7 +
    23.8 +See also E. Mendelson, Introduction to Mathematical Logic.
    23.9 +(Van Nostrand, 1964), page 250, exercise 11.
   23.10  *)
   23.11  
   23.12  Primrec0 = ListFn +
    24.1 --- a/src/ZF/ex/prop.ML	Fri Oct 22 11:34:41 1993 +0100
    24.2 +++ b/src/ZF/ex/prop.ML	Fri Oct 22 11:42:02 1993 +0100
    24.3 @@ -24,7 +24,7 @@
    24.4  	   "n: nat ==> #n : prop",
    24.5  	   "[| p: prop;  q: prop |] ==> p=>q : prop"];
    24.6    val monos = [];
    24.7 -  val type_intrs = data_typechecks;
    24.8 +  val type_intrs = datatype_intrs;
    24.9    val type_elims = []);
   24.10  
   24.11  val [FlsI,VarI,ImpI] = Prop.intrs;
    25.1 --- a/src/ZF/ex/term.ML	Fri Oct 22 11:34:41 1993 +0100
    25.2 +++ b/src/ZF/ex/term.ML	Fri Oct 22 11:42:02 1993 +0100
    25.3 @@ -16,7 +16,7 @@
    25.4    val ext = None
    25.5    val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
    25.6    val monos = [list_mono];
    25.7 -  val type_intrs = data_typechecks;
    25.8 +  val type_intrs = datatype_intrs;
    25.9    val type_elims = [make_elim (list_univ RS subsetD)]);
   25.10  
   25.11  val [ApplyI] = Term.intrs;
    26.1 --- a/src/ZF/ex/tf.ML	Fri Oct 22 11:34:41 1993 +0100
    26.2 +++ b/src/ZF/ex/tf.ML	Fri Oct 22 11:42:02 1993 +0100
    26.3 @@ -21,8 +21,8 @@
    26.4  	   "Fnil : forest(A)",
    26.5  	   "[| t: tree(A);  tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
    26.6    val monos = [];
    26.7 -  val type_intrs = data_typechecks
    26.8 -  val type_elims = data_elims);
    26.9 +  val type_intrs = datatype_intrs
   26.10 +  val type_elims = datatype_elims);
   26.11  
   26.12  val [TconsI, FnilI, FconsI] = TF.intrs;
   26.13  
   26.14 @@ -44,9 +44,9 @@
   26.15  
   26.16  (*The (refl RS conjI RS exI RS exI) avoids considerable search!*)
   26.17  val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI]
   26.18 -                    addIs data_typechecks
   26.19 +                    addIs datatype_intrs
   26.20                      addDs [TF.dom_subset RS subsetD]
   26.21 -	            addSEs ([PartE] @ data_elims @ TF.free_SEs);
   26.22 +	            addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
   26.23  
   26.24  goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
   26.25  by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);