--- 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;
--- 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. *)
--- 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;
--- 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 **)
--- 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";
--- 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
--- 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]
**)
--- 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)";
-
--- 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;
--- 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 +
--- 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;
--- 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);
--- 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;
--- 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. *)
--- 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;
--- 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;
--- 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 **)
--- 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";
--- 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)";
-
--- 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
--- 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]
**)
--- 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;
--- 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 +
--- 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;
--- 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;
--- 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);