added smart_conjunction_tac, prove_multi, prove_multi_standard;
authorwenzelm
Thu Apr 28 21:35:25 2005 +0200 (2005-04-28)
changeset 158746236cc88d4b8
parent 15873 02d9f110ecc1
child 15875 3e9a54e033b9
added smart_conjunction_tac, prove_multi, prove_multi_standard;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Apr 28 17:57:13 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Apr 28 21:35:25 2005 +0200
     1.3 @@ -110,8 +110,14 @@
     1.4    val rewrite: bool -> thm list -> cterm -> thm
     1.5    val simplify: bool -> thm list -> thm -> thm
     1.6    val conjunction_tac: tactic
     1.7 +  val smart_conjunction_tac: int -> tactic
     1.8 +  val prove_multi: Sign.sg -> string list -> term list -> term list ->
     1.9 +    (thm list -> tactic) -> thm list
    1.10 +  val prove_multi_standard: Sign.sg -> string list -> term list -> term list ->
    1.11 +    (thm list -> tactic) -> thm list
    1.12    val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.13 -  val prove_standard: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.14 +  val prove_standard: Sign.sg -> string list -> term list -> term ->
    1.15 +    (thm list -> tactic) -> thm
    1.16    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    1.17                            int -> tactic
    1.18    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    1.19 @@ -641,12 +647,16 @@
    1.20    
    1.21  val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
    1.22  
    1.23 +fun smart_conjunction_tac 0 = assume_tac 1
    1.24 +  | smart_conjunction_tac _ = TRY conjunction_tac;
    1.25 +
    1.26  
    1.27  
    1.28 -(** minimal goal interface for internal use *)
    1.29 +(** minimal goal interface for programmed proofs *)
    1.30  
    1.31 -fun prove sign xs asms prop tac =
    1.32 +fun prove_multi sign xs asms props tac =
    1.33    let
    1.34 +    val prop = Logic.mk_conjunction_list props;
    1.35      val statement = Logic.list_implies (asms, prop);
    1.36      val frees = map Term.dest_Free (Term.term_frees statement);
    1.37      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    1.38 @@ -671,23 +681,29 @@
    1.39      val goal' =
    1.40        (case Seq.pull (tac prems goal) of SOME (goal', _) => goal' | _ => err "Tactic failed.");
    1.41      val ngoals = Thm.nprems_of goal';
    1.42 +    val _ = conditional (ngoals <> 0) (fn () =>
    1.43 +      err ("Proof failed.\n" ^
    1.44 +        Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal')) ^
    1.45 +        ("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!")));
    1.46 +
    1.47      val raw_result = goal' RS Drule.rev_triv_goal;
    1.48      val prop' = prop_of raw_result;
    1.49 +    val _ = conditional (not (Pattern.matches (Sign.tsig_of sign) (prop, prop'))) (fn () =>
    1.50 +      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop'));
    1.51    in
    1.52 -    if ngoals <> 0 then
    1.53 -      err ("Proof failed.\n" ^ Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal'))
    1.54 -        ^ ("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!"))
    1.55 -    else if not (Pattern.matches (Sign.tsig_of sign) (prop, prop')) then
    1.56 -      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop')
    1.57 -    else
    1.58 -      raw_result
    1.59 +    Drule.conj_elim_precise (length props) raw_result
    1.60 +    |> map (fn res => res
    1.61        |> Drule.implies_intr_list casms
    1.62        |> Drule.forall_intr_list cparams
    1.63        |> norm_hhf_rule
    1.64        |> (#1 o Thm.varifyT' fixed_tfrees)
    1.65 -      |> Drule.zero_var_indexes
    1.66 +      |> Drule.zero_var_indexes)
    1.67    end;
    1.68  
    1.69 +fun prove_multi_standard sign xs asms prop tac =
    1.70 +  map Drule.standard (prove_multi sign xs asms prop tac);
    1.71 +
    1.72 +fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac);
    1.73  fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac);
    1.74  
    1.75  end;