# HG changeset patch
# User lcp
# Date 751286522 -3600
# Node ID 729fe026c5f35576e5cb75a2f036d4cc438c10cd
# Parent  8a29f8b4aca1681ffe4043907b527015807ffd3f
sample datatype defs now use datatype_intrs, datatype_elims

diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/BT.ML
--- a/src/ZF/ex/BT.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/BT.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -17,7 +17,7 @@
 	  ["Lf : bt(A)",
 	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
   val monos = [];
-  val type_intrs = data_typechecks
+  val type_intrs = datatype_intrs
   val type_elims = []);
 
 val [LfI, BrI] = BT.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Bin.ML
--- a/src/ZF/ex/Bin.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Bin.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -20,7 +20,7 @@
 	   "Minus : bin",
 	   "[| w: bin;  b: bool |] ==> w$$b : bin"];
   val monos = [];
-  val type_intrs = data_typechecks @ [bool_into_univ];
+  val type_intrs = datatype_intrs @ [bool_into_univ];
   val type_elims = []);
 
 (*Perform induction on l, then prove the major premise using prems. *)
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Comb.ML
--- a/src/ZF/ex/Comb.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Comb.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -25,7 +25,7 @@
 	   "S : comb",
 	   "[| p: comb;  q: comb |] ==> p#q : comb"];
   val monos = [];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = []);
 
 val [K_comb,S_comb,Ap_comb] = Comb.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Data.ML
--- a/src/ZF/ex/Data.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Data.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -23,8 +23,8 @@
 	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
 	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
   val monos = [];
-  val type_intrs = data_typechecks
-  val type_elims = data_elims);
+  val type_intrs = datatype_intrs
+  val type_elims = datatype_elims);
 
 
 (**  Lemmas to justify using "data" in other recursive type definitions **)
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Enum.ML
--- a/src/ZF/ex/Enum.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Enum.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -24,7 +24,7 @@
   val ext = None
   val sintrs = map (fn const => const ^ " : enum") consts;
   val monos = [];
-  val type_intrs = data_typechecks
+  val type_intrs = datatype_intrs
   val type_elims = []);
 
 goal Enum.thy "con59 ~= con60";
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/LList.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -21,7 +21,7 @@
       ["LNil : llist(A)",
        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   val monos = [];
-  val type_intrs = co_data_typechecks
+  val type_intrs = co_datatype_intrs
   val type_elims = []);
   
 val [LNilI, LConsI] = LList.intrs;
@@ -49,7 +49,7 @@
   QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
 
 val quniv_cs = ZF_cs addSIs in_quniv_rls 
-                     addIs (Int_quniv_in_quniv::co_data_typechecks);
+                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
 
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList.thy
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/LList_Eq.ML
--- a/src/ZF/ex/LList_Eq.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/LList_Eq.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -10,7 +10,7 @@
 
 structure LList_Eq = Co_Inductive_Fun
  (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
+  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
   val sintrs = 
       ["<LNil; LNil> : lleq(A)",
        "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
@@ -21,7 +21,7 @@
 
 (** Alternatives for above:
   val con_defs = LList.con_defs
-  val type_intrs = co_data_typechecks
+  val type_intrs = co_datatype_intrs
   val type_elims = [quniv_QPair_E]
 **)
 
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/ListN.ML
--- a/src/ZF/ex/ListN.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/ListN.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -23,8 +23,8 @@
 val listn_induct = standard 
     (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
 
-val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
-by (rtac (major RS List.induct) 1);
+goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
+by (etac List.induct 1);
 by (ALLGOALS (asm_simp_tac list_ss));
 by (REPEAT (ares_tac ListN.intrs 1));
 val list_into_listn = result();
@@ -47,6 +47,12 @@
 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
 val listn_mono = result();
 
+goal ListN.thy
+    "!!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)));
+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,xs)> : listn(A)";
-
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Primrec0.ML
--- a/src/ZF/ex/Primrec0.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Primrec0.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -9,6 +9,9 @@
 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 Primrec0;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Primrec0.thy
--- a/src/ZF/ex/Primrec0.thy	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Primrec0.thy	Fri Oct 22 11:42:02 1993 +0100
@@ -9,6 +9,9 @@
 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.
 *)
 
 Primrec0 = ListFn +
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Prop.ML
--- a/src/ZF/ex/Prop.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Prop.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -24,7 +24,7 @@
 	   "n: nat ==> #n : prop",
 	   "[| p: prop;  q: prop |] ==> p=>q : prop"];
   val monos = [];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = []);
 
 val [FlsI,VarI,ImpI] = Prop.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/TF.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -21,8 +21,8 @@
 	   "Fnil : forest(A)",
 	   "[| t: tree(A);  tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
   val monos = [];
-  val type_intrs = data_typechecks
-  val type_elims = data_elims);
+  val type_intrs = datatype_intrs
+  val type_elims = datatype_elims);
 
 val [TconsI, FnilI, FconsI] = TF.intrs;
 
@@ -44,9 +44,9 @@
 
 (*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 data_typechecks
+                    addIs datatype_intrs
                     addDs [TF.dom_subset RS subsetD]
-	            addSEs ([PartE] @ data_elims @ TF.free_SEs);
+	            addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
 
 goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Term.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -16,7 +16,7 @@
   val ext = None
   val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
   val monos = [list_mono];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = [make_elim (list_univ RS subsetD)]);
 
 val [ApplyI] = Term.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/bin.ML
--- a/src/ZF/ex/bin.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/bin.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -20,7 +20,7 @@
 	   "Minus : bin",
 	   "[| w: bin;  b: bool |] ==> w$$b : bin"];
   val monos = [];
-  val type_intrs = data_typechecks @ [bool_into_univ];
+  val type_intrs = datatype_intrs @ [bool_into_univ];
   val type_elims = []);
 
 (*Perform induction on l, then prove the major premise using prems. *)
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/bt.ML
--- a/src/ZF/ex/bt.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/bt.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -17,7 +17,7 @@
 	  ["Lf : bt(A)",
 	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
   val monos = [];
-  val type_intrs = data_typechecks
+  val type_intrs = datatype_intrs
   val type_elims = []);
 
 val [LfI, BrI] = BT.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/comb.ML
--- a/src/ZF/ex/comb.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/comb.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -25,7 +25,7 @@
 	   "S : comb",
 	   "[| p: comb;  q: comb |] ==> p#q : comb"];
   val monos = [];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = []);
 
 val [K_comb,S_comb,Ap_comb] = Comb.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/data.ML
--- a/src/ZF/ex/data.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/data.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -23,8 +23,8 @@
 	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
 	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
   val monos = [];
-  val type_intrs = data_typechecks
-  val type_elims = data_elims);
+  val type_intrs = datatype_intrs
+  val type_elims = datatype_elims);
 
 
 (**  Lemmas to justify using "data" in other recursive type definitions **)
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/enum.ML
--- a/src/ZF/ex/enum.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/enum.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -24,7 +24,7 @@
   val ext = None
   val sintrs = map (fn const => const ^ " : enum") consts;
   val monos = [];
-  val type_intrs = data_typechecks
+  val type_intrs = datatype_intrs
   val type_elims = []);
 
 goal Enum.thy "con59 ~= con60";
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/listn.ML
--- a/src/ZF/ex/listn.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/listn.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -23,8 +23,8 @@
 val listn_induct = standard 
     (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
 
-val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
-by (rtac (major RS List.induct) 1);
+goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
+by (etac List.induct 1);
 by (ALLGOALS (asm_simp_tac list_ss));
 by (REPEAT (ares_tac ListN.intrs 1));
 val list_into_listn = result();
@@ -47,6 +47,12 @@
 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
 val listn_mono = result();
 
+goal ListN.thy
+    "!!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)));
+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,xs)> : listn(A)";
-
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/llist.ML
--- a/src/ZF/ex/llist.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/llist.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -21,7 +21,7 @@
       ["LNil : llist(A)",
        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   val monos = [];
-  val type_intrs = co_data_typechecks
+  val type_intrs = co_datatype_intrs
   val type_elims = []);
   
 val [LNilI, LConsI] = LList.intrs;
@@ -49,7 +49,7 @@
   QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
 
 val quniv_cs = ZF_cs addSIs in_quniv_rls 
-                     addIs (Int_quniv_in_quniv::co_data_typechecks);
+                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
 
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList.thy
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/llist_eq.ML
--- a/src/ZF/ex/llist_eq.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/llist_eq.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -10,7 +10,7 @@
 
 structure LList_Eq = Co_Inductive_Fun
  (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq","llist(A) <*> llist(A)")];
+  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
   val sintrs = 
       ["<LNil; LNil> : lleq(A)",
        "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
@@ -21,7 +21,7 @@
 
 (** Alternatives for above:
   val con_defs = LList.con_defs
-  val type_intrs = co_data_typechecks
+  val type_intrs = co_datatype_intrs
   val type_elims = [quniv_QPair_E]
 **)
 
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/primrec0.ML
--- a/src/ZF/ex/primrec0.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/primrec0.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -9,6 +9,9 @@
 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 Primrec0;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/primrec0.thy
--- a/src/ZF/ex/primrec0.thy	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/primrec0.thy	Fri Oct 22 11:42:02 1993 +0100
@@ -9,6 +9,9 @@
 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.
 *)
 
 Primrec0 = ListFn +
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/prop.ML
--- a/src/ZF/ex/prop.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/prop.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -24,7 +24,7 @@
 	   "n: nat ==> #n : prop",
 	   "[| p: prop;  q: prop |] ==> p=>q : prop"];
   val monos = [];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = []);
 
 val [FlsI,VarI,ImpI] = Prop.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/term.ML
--- a/src/ZF/ex/term.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/term.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -16,7 +16,7 @@
   val ext = None
   val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
   val monos = [list_mono];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = [make_elim (list_univ RS subsetD)]);
 
 val [ApplyI] = Term.intrs;
diff -r 8a29f8b4aca1 -r 729fe026c5f3 src/ZF/ex/tf.ML
--- a/src/ZF/ex/tf.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/tf.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -21,8 +21,8 @@
 	   "Fnil : forest(A)",
 	   "[| t: tree(A);  tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
   val monos = [];
-  val type_intrs = data_typechecks
-  val type_elims = data_elims);
+  val type_intrs = datatype_intrs
+  val type_elims = datatype_elims);
 
 val [TconsI, FnilI, FconsI] = TF.intrs;
 
@@ -44,9 +44,9 @@
 
 (*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 data_typechecks
+                    addIs datatype_intrs
                     addDs [TF.dom_subset RS subsetD]
-	            addSEs ([PartE] @ data_elims @ TF.free_SEs);
+	            addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
 
 goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);