tuned conjunction tactics: slightly smaller proof terms;
authorwenzelm
Mon Jun 18 23:30:46 2007 +0200 (2007-06-18)
changeset 23414927203ad4b3a
parent 23413 5caa2710dd5b
child 23415 9dad8095bd43
tuned conjunction tactics: slightly smaller proof terms;
src/Pure/Isar/element.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/element.ML	Sun Jun 17 18:47:03 2007 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Mon Jun 18 23:30:46 2007 +0200
     1.3 @@ -305,8 +305,8 @@
     1.4  val refine_witness =
     1.5    Proof.refine (Method.Basic (K (Method.RAW_METHOD
     1.6      (K (ALLGOALS
     1.7 -      (PRECISE_CONJUNCTS ~1 (ALLGOALS
     1.8 -        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
     1.9 +      (CONJUNCTS (ALLGOALS
    1.10 +        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
    1.11  
    1.12  fun pretty_witness ctxt witn =
    1.13    let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in
     2.1 --- a/src/Pure/goal.ML	Sun Jun 17 18:47:03 2007 +0200
     2.2 +++ b/src/Pure/goal.ML	Mon Jun 18 23:30:46 2007 +0200
     2.3 @@ -8,8 +8,8 @@
     2.4  signature BASIC_GOAL =
     2.5  sig
     2.6    val SELECT_GOAL: tactic -> int -> tactic
     2.7 +  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
     2.8    val CONJUNCTS: tactic -> int -> tactic
     2.9 -  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    2.10  end;
    2.11  
    2.12  signature GOAL =
    2.13 @@ -29,8 +29,8 @@
    2.14    val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    2.15    val extract: int -> int -> thm -> thm Seq.seq
    2.16    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    2.17 +  val precise_conjunction_tac: int -> int -> tactic
    2.18    val conjunction_tac: int -> tactic
    2.19 -  val precise_conjunction_tac: int -> int -> tactic
    2.20    val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
    2.21    val rewrite_goal_tac: thm list -> int -> tactic
    2.22    val norm_hhf_tac: int -> tactic
    2.23 @@ -180,28 +180,48 @@
    2.24  
    2.25  (* multiple goals *)
    2.26  
    2.27 -val conj_tac = SUBGOAL (fn (goal, i) =>
    2.28 -  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
    2.29 -  else no_tac);
    2.30 +local
    2.31  
    2.32 -val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
    2.33 +fun conj_intrs n =
    2.34 +  let
    2.35 +    val cert = Thm.cterm_of ProtoPure.thy;
    2.36 +    val names = Name.invents Name.context "A" n;
    2.37 +    val As = map (fn name => cert (Free (name, propT))) names;
    2.38 +  in
    2.39 +    Thm.generalize ([], names) 0
    2.40 +      (Drule.implies_intr_list As (Conjunction.intr_list (map Thm.assume As)))
    2.41 +  end;
    2.42 +
    2.43 +fun count_conjs A =
    2.44 +  (case try Logic.dest_conjunction A of
    2.45 +    NONE => 1
    2.46 +  | SOME (_, B) => count_conjs B + 1);
    2.47 +
    2.48 +in
    2.49  
    2.50  val precise_conjunction_tac =
    2.51    let
    2.52      fun tac 0 i = eq_assume_tac i
    2.53        | tac 1 i = SUBGOAL (K all_tac) i
    2.54 -      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
    2.55 +      | tac 2 i = rtac Conjunction.conjunctionI i
    2.56 +      | tac n i = rtac (conj_intrs n) i;
    2.57    in TRY oo tac end;
    2.58  
    2.59 +val conjunction_tac = TRY o REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) =>
    2.60 +  let val n = count_conjs goal
    2.61 +  in if n < 2 then no_tac else precise_conjunction_tac n i end));
    2.62 +
    2.63 +fun PRECISE_CONJUNCTS n tac =
    2.64 +  SELECT_GOAL (precise_conjunction_tac n 1
    2.65 +    THEN tac
    2.66 +    THEN PRIMITIVE (Conjunction.uncurry ~1));
    2.67 +
    2.68  fun CONJUNCTS tac =
    2.69    SELECT_GOAL (conjunction_tac 1
    2.70      THEN tac
    2.71      THEN PRIMITIVE (Conjunction.uncurry ~1));
    2.72  
    2.73 -fun PRECISE_CONJUNCTS n tac =
    2.74 -  SELECT_GOAL (precise_conjunction_tac n 1
    2.75 -    THEN tac
    2.76 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
    2.77 +end;
    2.78  
    2.79  
    2.80  (* rewriting *)