sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
authorwenzelm
Wed Feb 15 21:35:06 2006 +0100 (2006-02-15)
changeset 190566ac9dfe98e54
parent 19055 4f408867f9d4
child 19057 9201b2bb36c2
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Wed Feb 15 21:35:06 2006 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Feb 15 21:35:06 2006 +0100
     1.3 @@ -199,25 +199,30 @@
     1.4  (*Smash all flex-flex disagreement pairs in the proof state.*)
     1.5  val flexflex_tac = PRIMSEQ flexflex_rule;
     1.6  
     1.7 -
     1.8 -(*Remove duplicate subgoals.  By Mark Staples*)
     1.9 -local
    1.10 -fun cterm_aconv (a,b) = term_of a aconv term_of b;
    1.11 -in
    1.12 +(*Remove duplicate subgoals.*)
    1.13  fun distinct_subgoals_tac state =
    1.14 -    let val (frozth,thawfn) = freeze_thaw state
    1.15 -        val froz_prems = cprems_of frozth
    1.16 -        val assumed = implies_elim_list frozth (map assume froz_prems)
    1.17 -        val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
    1.18 -                                        assumed;
    1.19 -    in  (*Applying Thm.varifyT to the result of thawfn would (re-)generalize
    1.20 -          all type variables that appear in the subgoals. Unfortunately, it
    1.21 -          would also break the function AxClass.intro_classes_tac, even in the
    1.22 -          trivial case where the type class has no axioms.*)
    1.23 -        Seq.single (thawfn implied)
    1.24 -    end
    1.25 -end;
    1.26 +  let
    1.27 +    val perm_tac = PRIMITIVE oo Thm.permute_prems;
    1.28  
    1.29 +    fun distinct_tac (i, k) =
    1.30 +      perm_tac 0 (i - 1) THEN
    1.31 +      perm_tac 1 (k - 1) THEN
    1.32 +      DETERM (PRIMSEQ (fn st =>
    1.33 +        Thm.compose_no_flatten false (st, 0) 1
    1.34 +          (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
    1.35 +      perm_tac 1 (1 - k) THEN
    1.36 +      perm_tac 0 (1 - i);
    1.37 +
    1.38 +    fun distinct_subgoal_tac i st =
    1.39 +      (case Library.drop (i - 1, Thm.prems_of st) of
    1.40 +        [] => no_tac st
    1.41 +      | A :: Bs =>
    1.42 +          st |> EVERY (fold (fn (B, k) =>
    1.43 +            if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
    1.44 +
    1.45 +    val goals = Thm.prems_of state;
    1.46 +    val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
    1.47 +  in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;
    1.48  
    1.49  (*Determine print names of goal parameters (reversed)*)
    1.50  fun innermost_params i st =
    1.51 @@ -567,7 +572,7 @@
    1.52    Returns longest lhs first to avoid folding its subexpressions.*)
    1.53  fun sort_lhs_depths defs =
    1.54    let val keylist = AList.make (term_depth o lhs_of_thm) defs
    1.55 -      val keys = gen_distinct (op =) (sort (rev_order o int_ord) (map #2 keylist))
    1.56 +      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
    1.57    in map (AList.find (op =) keylist) keys end;
    1.58  
    1.59  val rev_defs = sort_lhs_depths o map symmetric;