# HG changeset patch # User lcp # Date 751286081 -3600 # Node ID 8a29f8b4aca1681ffe4043907b527015807ffd3f # Parent e7588b53d6b0c48b6babeaad057f8e160735f24d 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 diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/Datatype.ML --- 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]; diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/List.ML --- 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; diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/datatype.ML --- 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]; diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/fin.ML --- 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; diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/ind-syntax.ML --- 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 diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/ind_syntax.ML --- 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 diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/intr-elim.ML --- 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 = diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/intr_elim.ML --- 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 = diff -r e7588b53d6b0 -r 8a29f8b4aca1 src/ZF/list.ML --- 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;