now exports distinct_subgoal_tac (needed by MetisAPI)
authorpaulson
Mon Apr 02 11:30:44 2007 +0200 (2007-04-02)
changeset 22560f19ddf96c323
parent 22559 b824487d9b41
child 22561 705d4fb9e628
now exports distinct_subgoal_tac (needed by MetisAPI)
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Mon Apr 02 11:29:44 2007 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Apr 02 11:30:44 2007 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
     1.5    val datac             : thm -> int -> int -> tactic
     1.6    val defer_tac         : int -> tactic
     1.7 +  val distinct_subgoal_tac      : int -> tactic
     1.8    val distinct_subgoals_tac     : tactic
     1.9    val dmatch_tac        : thm list -> int -> tactic
    1.10    val dresolve_tac      : thm list -> int -> tactic
    1.11 @@ -186,26 +187,26 @@
    1.12  val flexflex_tac = PRIMSEQ flexflex_rule;
    1.13  
    1.14  (*Remove duplicate subgoals.*)
    1.15 +val perm_tac = PRIMITIVE oo Thm.permute_prems;
    1.16 +
    1.17 +fun distinct_tac (i, k) =
    1.18 +  perm_tac 0 (i - 1) THEN
    1.19 +  perm_tac 1 (k - 1) THEN
    1.20 +  DETERM (PRIMSEQ (fn st =>
    1.21 +    Thm.compose_no_flatten false (st, 0) 1
    1.22 +      (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
    1.23 +  perm_tac 1 (1 - k) THEN
    1.24 +  perm_tac 0 (1 - i);
    1.25 +
    1.26 +fun distinct_subgoal_tac i st =
    1.27 +  (case Library.drop (i - 1, Thm.prems_of st) of
    1.28 +    [] => no_tac st
    1.29 +  | A :: Bs =>
    1.30 +      st |> EVERY (fold (fn (B, k) =>
    1.31 +	if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
    1.32 +
    1.33  fun distinct_subgoals_tac state =
    1.34    let
    1.35 -    val perm_tac = PRIMITIVE oo Thm.permute_prems;
    1.36 -
    1.37 -    fun distinct_tac (i, k) =
    1.38 -      perm_tac 0 (i - 1) THEN
    1.39 -      perm_tac 1 (k - 1) THEN
    1.40 -      DETERM (PRIMSEQ (fn st =>
    1.41 -        Thm.compose_no_flatten false (st, 0) 1
    1.42 -          (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
    1.43 -      perm_tac 1 (1 - k) THEN
    1.44 -      perm_tac 0 (1 - i);
    1.45 -
    1.46 -    fun distinct_subgoal_tac i st =
    1.47 -      (case Library.drop (i - 1, Thm.prems_of st) of
    1.48 -        [] => no_tac st
    1.49 -      | A :: Bs =>
    1.50 -          st |> EVERY (fold (fn (B, k) =>
    1.51 -            if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
    1.52 -
    1.53      val goals = Thm.prems_of state;
    1.54      val dups = distinct (eq_fst (op aconv)) (goals ~~ (1 upto length goals));
    1.55    in EVERY (rev (map (distinct_subgoal_tac o snd) dups)) state end;