1.1 --- a/src/Pure/goal.ML	Tue Jun 19 23:15:23 2007 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Jun 19 23:15:27 2007 +0200
     1.3 @@ -8,8 +8,8 @@
     1.4  signature BASIC_GOAL =
     1.5  sig
     1.6    val SELECT_GOAL: tactic -> int -> tactic
     1.7 +  val CONJUNCTS: tactic -> int -> tactic
     1.8    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
     1.9 -  val CONJUNCTS: tactic -> int -> tactic
    1.10  end;
    1.11  
    1.12  signature GOAL =
    1.13 @@ -29,8 +29,9 @@
    1.14    val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.15    val extract: int -> int -> thm -> thm Seq.seq
    1.16    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    1.17 +  val conjunction_tac: int -> tactic
    1.18    val precise_conjunction_tac: int -> int -> tactic
    1.19 -  val conjunction_tac: int -> tactic
    1.20 +  val recover_conjunction_tac: tactic
    1.21    val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
    1.22    val rewrite_goal_tac: thm list -> int -> tactic
    1.23    val norm_hhf_tac: int -> tactic
    1.24 @@ -132,12 +133,12 @@
    1.25        |> fold Variable.declare_internal (asms @ props)
    1.26        |> Assumption.add_assumes casms;
    1.27  
    1.28 -    val goal = init (Conjunction.mk_conjunction_list cprops);
    1.29 +    val goal = init (Conjunction.mk_conjunction_balanced cprops);
    1.30      val res =
    1.31        (case SINGLE (tac {prems = prems, context = ctxt'}) goal of
    1.32          NONE => err "Tactic failed."
    1.33        | SOME res => res);
    1.34 -    val [results] = Conjunction.elim_precise [length props] (finish res)
    1.35 +    val results = Conjunction.elim_balanced (length props) (finish res)
    1.36        handle THM (msg, _, _) => err msg;
    1.37      val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results)
    1.38        orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
    1.39 @@ -165,12 +166,13 @@
    1.40  fun extract i n st =
    1.41    (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    1.42     else if n = 1 then Seq.single (Thm.cprem_of st i)
    1.43 -   else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
    1.44 +   else
    1.45 +     Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
    1.46    |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
    1.47  
    1.48  fun retrofit i n st' st =
    1.49    (if n = 1 then st
    1.50 -   else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
    1.51 +   else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
    1.52    |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
    1.53  
    1.54  fun SELECT_GOAL tac i st =
    1.55 @@ -180,48 +182,31 @@
    1.56  
    1.57  (* multiple goals *)
    1.58  
    1.59 -local
    1.60 +fun precise_conjunction_tac 0 i = eq_assume_tac i
    1.61 +  | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
    1.62 +  | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n));
    1.63  
    1.64 -fun conj_intrs n =
    1.65 -  let
    1.66 -    val cert = Thm.cterm_of ProtoPure.thy;
    1.67 -    val names = Name.invents Name.context "A" n;
    1.68 -    val As = map (fn name => cert (Free (name, propT))) names;
    1.69 -  in
    1.70 -    Thm.generalize ([], names) 0
    1.71 -      (Drule.implies_intr_list As (Conjunction.intr_list (map Thm.assume As)))
    1.72 -  end;
    1.73 +val adhoc_conjunction_tac = REPEAT_ALL_NEW
    1.74 +  (SUBGOAL (fn (goal, i) =>
    1.75 +    if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
    1.76 +    else no_tac));
    1.77  
    1.78 -fun count_conjs A =
    1.79 -  (case try Logic.dest_conjunction A of
    1.80 -    NONE => 1
    1.81 -  | SOME (_, B) => count_conjs B + 1);
    1.82 +val conjunction_tac = SUBGOAL (fn (goal, i) =>
    1.83 +  precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
    1.84 +  TRY (adhoc_conjunction_tac i));
    1.85  
    1.86 -in
    1.87 -
    1.88 -val precise_conjunction_tac =
    1.89 -  let
    1.90 -    fun tac 0 i = eq_assume_tac i
    1.91 -      | tac 1 i = SUBGOAL (K all_tac) i
    1.92 -      | tac 2 i = rtac Conjunction.conjunctionI i
    1.93 -      | tac n i = rtac (conj_intrs n) i;
    1.94 -  in TRY oo tac end;
    1.95 -
    1.96 -val conjunction_tac = TRY o REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) =>
    1.97 -  let val n = count_conjs goal
    1.98 -  in if n < 2 then no_tac else precise_conjunction_tac n i end));
    1.99 +val recover_conjunction_tac = PRIMITIVE (fn th =>
   1.100 +  Conjunction.uncurry_balanced (Thm.nprems_of th) th);
   1.101  
   1.102  fun PRECISE_CONJUNCTS n tac =
   1.103    SELECT_GOAL (precise_conjunction_tac n 1
   1.104      THEN tac
   1.105 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
   1.106 +    THEN recover_conjunction_tac);
   1.107  
   1.108  fun CONJUNCTS tac =
   1.109    SELECT_GOAL (conjunction_tac 1
   1.110      THEN tac
   1.111 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
   1.112 -
   1.113 -end;
   1.114 +    THEN recover_conjunction_tac);
   1.115  
   1.116  
   1.117  (* rewriting *)