ZF/ex/tf/tree,forest_unfold: streamlined the proofs
Updated other inductive def examples as per changes in the package.
--- a/src/ZF/ex/BT.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/BT.ML Fri Oct 15 10:25:23 1993 +0100
@@ -44,6 +44,5 @@
Pair_in_univ]) 1);
val bt_univ = result();
-val bt_subset_univ = standard (bt_mono RS (bt_univ RSN (2,subset_trans)));
+val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
-
--- a/src/ZF/ex/Bin.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/Bin.ML Fri Oct 15 10:25:23 1993 +0100
@@ -20,7 +20,7 @@
"Minus : bin",
"[| w: bin; b: bool |] ==> w$$b : bin"];
val monos = [];
- val type_intrs = bool_into_univ::data_typechecks;
+ val type_intrs = data_typechecks @ [bool_into_univ];
val type_elims = []);
(*Perform induction on l, then prove the major premise using prems. *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Data.ML Fri Oct 15 10:25:23 1993 +0100
@@ -0,0 +1,47 @@
+(* Title: ZF/ex/data.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Sample datatype definition.
+It has four contructors, of arities 0-3, and two parameters A and B.
+*)
+
+structure Data = Datatype_Fun
+ (val thy = Univ.thy;
+ val rec_specs =
+ [("data", "univ(A Un B)",
+ [(["Zero"], "i"),
+ (["One"], "i=>i"),
+ (["Two"], "[i,i]=>i"),
+ (["Three"], "[i,i,i]=>i")])];
+ val rec_styp = "[i,i]=>i";
+ val ext = None
+ val sintrs =
+ ["Zero : data(A,B)",
+ "[| a: A |] ==> One(a) : data(A,B)",
+ "[| 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);
+
+
+(** 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)";
+by (rtac lfp_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)";
+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,
+ Pair_in_univ]) 1);
+val data_univ = result();
+
+val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
+
+
--- a/src/ZF/ex/Enum.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/Enum.ML Fri Oct 15 10:25:23 1993 +0100
@@ -5,11 +5,11 @@
Example of a BIG enumeration type
-Can go up to at least 100 constructors, but it takes over 10 minutes...
+Can go up to at least 100 constructors, but it takes nearly 7 minutes...
*)
-(*An enumeration type with 60 contructors! -- takes about 214 seconds!*)
+(*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);
@@ -28,6 +28,6 @@
val type_elims = []);
goal Enum.thy "con59 ~= con60";
-by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1); (*2.3 secs*)
+by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
result();
--- a/src/ZF/ex/ListN.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/ListN.ML Fri Oct 15 10:25:23 1993 +0100
@@ -47,3 +47,6 @@
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
val listn_mono = 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 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/Primrec0.ML Fri Oct 15 10:25:23 1993 +0100
@@ -154,7 +154,7 @@
by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr0_typechecks) 1));
val ack_lt_mono2 = result();
-(*PROPERTY A 5', monotonicity for <= *)
+(*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);
--- a/src/ZF/ex/ROOT.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/ROOT.ML Fri Oct 15 10:25:23 1993 +0100
@@ -32,7 +32,8 @@
(*trees/forests: mutual recursion*)
time_use "ex/tf.ML";
time_use_thy "ex/tf_fn";
-(*Enormous enumeration type -- could be even bigger?*)
+(*Sample datatype; enormous enumeration type*)
+time_use "ex/data.ML";
time_use "ex/enum.ML";
(** Inductive definitions **)
--- a/src/ZF/ex/TF.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/TF.ML Fri Oct 15 10:25:23 1993 +0100
@@ -22,7 +22,7 @@
"[| t: tree(A); tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
val monos = [];
val type_intrs = data_typechecks
- val type_elims = []);
+ val type_elims = data_elims);
val [TconsI, FnilI, FconsI] = TF.intrs;
@@ -42,24 +42,25 @@
(** NOT useful, but interesting... **)
+(*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
+ addDs [TF.dom_subset RS subsetD]
+ addSEs ([PartE] @ data_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);
by (rewrite_goals_tac TF.con_defs);
by (rtac equalityI 1);
-by (fast_tac (ZF_cs addIs [PartI] addSEs (PartE::TF.free_SEs)) 1);
-by (fast_tac (ZF_cs addIs ([PartI,InlI,InrI] @ [TF.dom_subset RS subsetD]
- @ data_typechecks)
- addSEs (PartE::TF.free_SEs)) 1);
+by (fast_tac unfold_cs 1);
+by (fast_tac unfold_cs 1);
val tree_unfold = result();
goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
by (rewrite_goals_tac TF.con_defs);
by (rtac equalityI 1);
-by (fast_tac (ZF_cs addIs [PartI,InlI,InrI]
- addSEs (PartE::TF.free_SEs)) 1);
-by (fast_tac (ZF_cs addIs ([PartI,InlI,InrI] @ [TF.dom_subset RS subsetD]
- @ data_typechecks)
- addSEs ([PartE, sumE] @ TF.free_SEs)) 1);
+by (fast_tac unfold_cs 1);
+by (fast_tac unfold_cs 1);
val forest_unfold = result();
--- a/src/ZF/ex/Term.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/Term.ML Fri Oct 15 10:25:23 1993 +0100
@@ -16,8 +16,8 @@
val ext = None
val sintrs = ["[| a: A; l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
val monos = [list_mono];
- val type_intrs = [list_univ RS subsetD] @ data_typechecks;
- val type_elims = []);
+ val type_intrs = data_typechecks;
+ val type_elims = [make_elim (list_univ RS subsetD)]);
val [ApplyI] = Term.intrs;
--- a/src/ZF/ex/bin.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/bin.ML Fri Oct 15 10:25:23 1993 +0100
@@ -20,7 +20,7 @@
"Minus : bin",
"[| w: bin; b: bool |] ==> w$$b : bin"];
val monos = [];
- val type_intrs = bool_into_univ::data_typechecks;
+ val type_intrs = data_typechecks @ [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 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/bt.ML Fri Oct 15 10:25:23 1993 +0100
@@ -44,6 +44,5 @@
Pair_in_univ]) 1);
val bt_univ = result();
-val bt_subset_univ = standard (bt_mono RS (bt_univ RSN (2,subset_trans)));
+val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/data.ML Fri Oct 15 10:25:23 1993 +0100
@@ -0,0 +1,47 @@
+(* Title: ZF/ex/data.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Sample datatype definition.
+It has four contructors, of arities 0-3, and two parameters A and B.
+*)
+
+structure Data = Datatype_Fun
+ (val thy = Univ.thy;
+ val rec_specs =
+ [("data", "univ(A Un B)",
+ [(["Zero"], "i"),
+ (["One"], "i=>i"),
+ (["Two"], "[i,i]=>i"),
+ (["Three"], "[i,i,i]=>i")])];
+ val rec_styp = "[i,i]=>i";
+ val ext = None
+ val sintrs =
+ ["Zero : data(A,B)",
+ "[| a: A |] ==> One(a) : data(A,B)",
+ "[| 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);
+
+
+(** 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)";
+by (rtac lfp_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)";
+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,
+ Pair_in_univ]) 1);
+val data_univ = result();
+
+val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
+
+
--- a/src/ZF/ex/enum.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/enum.ML Fri Oct 15 10:25:23 1993 +0100
@@ -5,11 +5,11 @@
Example of a BIG enumeration type
-Can go up to at least 100 constructors, but it takes over 10 minutes...
+Can go up to at least 100 constructors, but it takes nearly 7 minutes...
*)
-(*An enumeration type with 60 contructors! -- takes about 214 seconds!*)
+(*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);
@@ -28,6 +28,6 @@
val type_elims = []);
goal Enum.thy "con59 ~= con60";
-by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1); (*2.3 secs*)
+by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
result();
--- a/src/ZF/ex/listn.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/listn.ML Fri Oct 15 10:25:23 1993 +0100
@@ -47,3 +47,6 @@
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
val listn_mono = 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 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/primrec0.ML Fri Oct 15 10:25:23 1993 +0100
@@ -154,7 +154,7 @@
by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr0_typechecks) 1));
val ack_lt_mono2 = result();
-(*PROPERTY A 5', monotonicity for <= *)
+(*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);
--- a/src/ZF/ex/term.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/term.ML Fri Oct 15 10:25:23 1993 +0100
@@ -16,8 +16,8 @@
val ext = None
val sintrs = ["[| a: A; l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
val monos = [list_mono];
- val type_intrs = [list_univ RS subsetD] @ data_typechecks;
- val type_elims = []);
+ val type_intrs = data_typechecks;
+ val type_elims = [make_elim (list_univ RS subsetD)]);
val [ApplyI] = Term.intrs;
--- a/src/ZF/ex/tf.ML Fri Oct 15 10:21:01 1993 +0100
+++ b/src/ZF/ex/tf.ML Fri Oct 15 10:25:23 1993 +0100
@@ -22,7 +22,7 @@
"[| t: tree(A); tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
val monos = [];
val type_intrs = data_typechecks
- val type_elims = []);
+ val type_elims = data_elims);
val [TconsI, FnilI, FconsI] = TF.intrs;
@@ -42,24 +42,25 @@
(** NOT useful, but interesting... **)
+(*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
+ addDs [TF.dom_subset RS subsetD]
+ addSEs ([PartE] @ data_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);
by (rewrite_goals_tac TF.con_defs);
by (rtac equalityI 1);
-by (fast_tac (ZF_cs addIs [PartI] addSEs (PartE::TF.free_SEs)) 1);
-by (fast_tac (ZF_cs addIs ([PartI,InlI,InrI] @ [TF.dom_subset RS subsetD]
- @ data_typechecks)
- addSEs (PartE::TF.free_SEs)) 1);
+by (fast_tac unfold_cs 1);
+by (fast_tac unfold_cs 1);
val tree_unfold = result();
goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
by (rewrite_goals_tac TF.con_defs);
by (rtac equalityI 1);
-by (fast_tac (ZF_cs addIs [PartI,InlI,InrI]
- addSEs (PartE::TF.free_SEs)) 1);
-by (fast_tac (ZF_cs addIs ([PartI,InlI,InrI] @ [TF.dom_subset RS subsetD]
- @ data_typechecks)
- addSEs ([PartE, sumE] @ TF.free_SEs)) 1);
+by (fast_tac unfold_cs 1);
+by (fast_tac unfold_cs 1);
val forest_unfold = result();