src/Pure/tactic.ML
changeset 18471 ca9a864018d6
parent 18209 6bcd9b2ca49b
child 18500 8b1a4e8ed199
     1.1 --- a/src/Pure/tactic.ML	Thu Dec 22 00:29:00 2005 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Dec 22 00:29:01 2005 +0100
     1.3 @@ -98,7 +98,8 @@
     1.4    val instantiate_tac   : (string * string) list -> tactic
     1.5    val thin_tac          : string -> int -> tactic
     1.6    val trace_goalno_tac  : (int -> tactic) -> int -> tactic
     1.7 -  val CONJUNCTS: tactic -> int -> tactic
     1.8 +  val CONJUNCTS: int -> tactic -> int -> tactic
     1.9 +  val CONJUNCTS2: int -> tactic -> int -> tactic
    1.10  end;
    1.11  
    1.12  signature TACTIC =
    1.13 @@ -110,8 +111,8 @@
    1.14    val orderlist: (int * 'a) list -> 'a list
    1.15    val rewrite: bool -> thm list -> cterm -> thm
    1.16    val simplify: bool -> thm list -> thm -> thm
    1.17 -  val conjunction_tac: tactic
    1.18 -  val smart_conjunction_tac: int -> tactic
    1.19 +  val conjunction_tac: int -> tactic
    1.20 +  val precise_conjunction_tac: int -> int -> tactic
    1.21    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    1.22                            int -> tactic
    1.23    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    1.24 @@ -633,24 +634,31 @@
    1.25    end;
    1.26  
    1.27  
    1.28 -(*meta-level conjunction*)
    1.29 -val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $
    1.30 -      (Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) =>
    1.31 -    (fn st =>
    1.32 -      compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
    1.33 -  | _ => no_tac);
    1.34 +(* meta-level conjunction *)
    1.35 +
    1.36 +val conj_tac = SUBGOAL (fn (goal, i) =>
    1.37 +  if can Logic.dest_conjunction goal then
    1.38 +    (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
    1.39 +  else no_tac);
    1.40 +
    1.41 +val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
    1.42  
    1.43 -val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
    1.44 +val precise_conjunction_tac =
    1.45 +  let
    1.46 +    fun tac 0 i = eq_assume_tac i
    1.47 +      | tac 1 i = SUBGOAL (K all_tac) i
    1.48 +      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
    1.49 +  in TRY oo tac end;
    1.50  
    1.51 -fun smart_conjunction_tac 0 = assume_tac 1
    1.52 -  | smart_conjunction_tac _ = TRY conjunction_tac;
    1.53 -
    1.54 -(*treat conjunction as separate sub-goals*)
    1.55 -fun CONJUNCTS tac =
    1.56 -  SELECT_GOAL (TRY conjunction_tac
    1.57 +(*treat conjuncts as separate sub-goals*)
    1.58 +fun CONJUNCTS n tac =
    1.59 +  SELECT_GOAL (precise_conjunction_tac n 1
    1.60      THEN tac
    1.61      THEN PRIMITIVE Drule.conj_curry);
    1.62  
    1.63 +(*treat two levels of conjunctions*)
    1.64 +fun CONJUNCTS2 n tac = CONJUNCTS n (ALLGOALS (CONJUNCTS ~1 tac));
    1.65 +
    1.66  end;
    1.67  
    1.68  structure BasicTactic: BASIC_TACTIC = Tactic;