ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
ZF/intr-elim/elim_rls: applied make_elim to succ_inject!
ZF/fin: changed type_intrs in inductive def
ZF/datatype/datatype_intrs, datatype_elims: renamed from data_typechecks,
data_elims
ZF/list: now uses datatype_intrs
--- a/src/ZF/Datatype.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/Datatype.ML Fri Oct 22 11:34:41 1993 +0100
@@ -52,19 +52,19 @@
(*For most datatypes involving univ*)
-val data_typechecks =
+val datatype_intrs =
[SigmaI, InlI, InrI,
Pair_in_univ, Inl_in_univ, Inr_in_univ,
zero_in_univ, A_into_univ, nat_into_univ, UnCI];
(*Needed for mutual recursion*)
-val data_elims = [make_elim InlD, make_elim InrD];
+val datatype_elims = [make_elim InlD, make_elim InrD];
(*For most co-datatypes involving quniv*)
-val co_data_typechecks =
+val co_datatype_intrs =
[QSigmaI, QInlI, QInrI,
QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
-val co_data_elims = [make_elim QInlD, make_elim QInrD];
+val co_datatype_elims = [make_elim QInlD, make_elim QInrD];
--- a/src/ZF/List.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/List.ML Fri Oct 22 11:34:41 1993 +0100
@@ -18,7 +18,7 @@
["Nil : list(A)",
"[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"];
val monos = [];
- val type_intrs = data_typechecks
+ val type_intrs = datatype_intrs
val type_elims = []);
val [NilI, ConsI] = List.intrs;
--- a/src/ZF/datatype.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/datatype.ML Fri Oct 22 11:34:41 1993 +0100
@@ -52,19 +52,19 @@
(*For most datatypes involving univ*)
-val data_typechecks =
+val datatype_intrs =
[SigmaI, InlI, InrI,
Pair_in_univ, Inl_in_univ, Inr_in_univ,
zero_in_univ, A_into_univ, nat_into_univ, UnCI];
(*Needed for mutual recursion*)
-val data_elims = [make_elim InlD, make_elim InrD];
+val datatype_elims = [make_elim InlD, make_elim InrD];
(*For most co-datatypes involving quniv*)
-val co_data_typechecks =
+val co_datatype_intrs =
[QSigmaI, QInlI, QInrI,
QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
-val co_data_elims = [make_elim QInlD, make_elim QInrD];
+val co_datatype_elims = [make_elim QInlD, make_elim QInrD];
--- a/src/ZF/fin.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/fin.ML Fri Oct 22 11:34:41 1993 +0100
@@ -25,7 +25,7 @@
"[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
val monos = [];
val con_defs = [];
- val type_intrs = [Pow_bottom, cons_subsetI, PowI]
+ val type_intrs = [empty_subsetI, cons_subsetI, PowI]
val type_elims = [make_elim PowD]);
val [Fin_0I, Fin_consI] = Fin.intrs;
--- a/src/ZF/ind-syntax.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/ind-syntax.ML Fri Oct 22 11:34:41 1993 +0100
@@ -91,22 +91,6 @@
fun mk_tprop P = Trueprop $ P;
fun dest_tprop (Const("Trueprop",_) $ P) = P;
-(*** Tactic for folding constructor definitions ***)
-
-(*The depth of injections in a constructor function*)
-fun inject_depth (Const _ $ t) = 1 + inject_depth t
- | inject_depth t = 0;
-
-val rhs_of_thm = #2 o Logic.dest_equals o #prop o rep_thm;
-
-(*There are critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
- Folds longest definitions first to avoid folding subexpressions of an rhs.*)
-fun fold_con_tac defs =
- let val keylist = make_keylist (inject_depth o rhs_of_thm) defs;
- val keys = distinct (sort op> (map #2 keylist));
- val deflists = map (keyfilter keylist) keys
- in EVERY (map fold_tac deflists) end;
-
(*Prove a goal stated as a term, with exception handling*)
fun prove_term sign defs (P,tacsf) =
let val ct = Sign.cterm_of sign P
--- a/src/ZF/ind_syntax.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/ind_syntax.ML Fri Oct 22 11:34:41 1993 +0100
@@ -91,22 +91,6 @@
fun mk_tprop P = Trueprop $ P;
fun dest_tprop (Const("Trueprop",_) $ P) = P;
-(*** Tactic for folding constructor definitions ***)
-
-(*The depth of injections in a constructor function*)
-fun inject_depth (Const _ $ t) = 1 + inject_depth t
- | inject_depth t = 0;
-
-val rhs_of_thm = #2 o Logic.dest_equals o #prop o rep_thm;
-
-(*There are critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
- Folds longest definitions first to avoid folding subexpressions of an rhs.*)
-fun fold_con_tac defs =
- let val keylist = make_keylist (inject_depth o rhs_of_thm) defs;
- val keys = distinct (sort op> (map #2 keylist));
- val deflists = map (keyfilter keylist) keys
- in EVERY (map fold_tac deflists) end;
-
(*Prove a goal stated as a term, with exception handling*)
fun prove_term sign defs (P,tacsf) =
let val ct = Sign.cterm_of sign P
--- a/src/ZF/intr-elim.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/intr-elim.ML Fri Oct 22 11:34:41 1993 +0100
@@ -263,8 +263,8 @@
(*Includes rules for succ and Pair since they are common constructions*)
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
- Pair_neq_0, sym RS Pair_neq_0, succ_inject, refl_thin,
- conjE, exE, disjE];
+ Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject,
+ refl_thin, conjE, exE, disjE];
val sumprod_free_SEs =
map (gen_make_elim [conjE,FalseE])
@@ -283,7 +283,7 @@
the given defs. Cannot simply use the local con_defs because con_defs=[]
for inference systems. *)
fun con_elim_tac defs =
- rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
+ rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
(*String s should have the form t:Si where Si is an inductive set*)
fun mk_cases defs s =
--- a/src/ZF/intr_elim.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/intr_elim.ML Fri Oct 22 11:34:41 1993 +0100
@@ -263,8 +263,8 @@
(*Includes rules for succ and Pair since they are common constructions*)
val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0,
- Pair_neq_0, sym RS Pair_neq_0, succ_inject, refl_thin,
- conjE, exE, disjE];
+ Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject,
+ refl_thin, conjE, exE, disjE];
val sumprod_free_SEs =
map (gen_make_elim [conjE,FalseE])
@@ -283,7 +283,7 @@
the given defs. Cannot simply use the local con_defs because con_defs=[]
for inference systems. *)
fun con_elim_tac defs =
- rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
+ rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
(*String s should have the form t:Si where Si is an inductive set*)
fun mk_cases defs s =
--- a/src/ZF/list.ML Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/list.ML Fri Oct 22 11:34:41 1993 +0100
@@ -18,7 +18,7 @@
["Nil : list(A)",
"[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"];
val monos = [];
- val type_intrs = data_typechecks
+ val type_intrs = datatype_intrs
val type_elims = []);
val [NilI, ConsI] = List.intrs;