prove: proper assumption context, more tactic arguments;
authorwenzelm
Sat Jul 29 00:51:32 2006 +0200 (2006-07-29)
changeset 20250c3f209752749
parent 20249 a13adb4f94dc
child 20251 6379135f21c2
prove: proper assumption context, more tactic arguments;
tuned;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Sat Jul 29 00:51:31 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Sat Jul 29 00:51:32 2006 +0200
     1.3 @@ -20,11 +20,12 @@
     1.4    val compose_hhf: thm -> int -> thm -> thm Seq.seq
     1.5    val compose_hhf_tac: thm -> int -> tactic
     1.6    val comp_hhf: thm -> thm -> thm
     1.7 +  val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
     1.8    val prove_multi: Context.proof -> string list -> term list -> term list ->
     1.9 -    (thm list -> tactic) -> thm list
    1.10 -  val prove: Context.proof -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.11 +    ({prems: thm list, context: Context.proof} -> tactic) -> thm list
    1.12 +  val prove: Context.proof -> string list -> term list -> term ->
    1.13 +    ({prems: thm list, context: Context.proof} -> tactic) -> thm
    1.14    val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.15 -  val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.16    val extract: int -> int -> thm -> thm Seq.seq
    1.17    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    1.18  end;
    1.19 @@ -91,6 +92,14 @@
    1.20  
    1.21  (** tactical theorem proving **)
    1.22  
    1.23 +(* prove_raw -- no checks, no normalization of result! *)
    1.24 +
    1.25 +fun prove_raw casms cprop tac =
    1.26 +  (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
    1.27 +    SOME th => Drule.implies_intr_list casms (finish th)
    1.28 +  | NONE => error "Tactic failed.");
    1.29 +
    1.30 +
    1.31  (* prove_multi *)
    1.32  
    1.33  fun prove_multi ctxt xs asms props tac =
    1.34 @@ -98,37 +107,34 @@
    1.35      val thy = Context.theory_of_proof ctxt;
    1.36      val string_of_term = Sign.string_of_term thy;
    1.37  
    1.38 -    val prop = Logic.mk_conjunction_list props;
    1.39 -    val statement = Logic.list_implies (asms, prop);
    1.40 +    fun err msg = cat_error msg
    1.41 +      ("The error(s) above occurred for the goal statement:\n" ^
    1.42 +        string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
    1.43  
    1.44 -    fun err msg = cat_error msg
    1.45 -      ("The error(s) above occurred for the goal statement:\n" ^ string_of_term statement);
    1.46 -    fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
    1.47 +    fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
    1.48        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.49 +    val casms = map cert_safe asms;
    1.50 +    val cprops = map cert_safe props;
    1.51  
    1.52 -    val _ = cert_safe statement;
    1.53 -    val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
    1.54 -    val casms = map cert_safe asms;
    1.55 -    val prems = map (norm_hhf o Thm.assume) casms;
    1.56 +    val (prems, ctxt') = ctxt
    1.57 +      |> Variable.add_fixes_direct xs
    1.58 +      |> fold Variable.declare_internal (asms @ props)
    1.59 +      |> Assumption.add_assumes casms;
    1.60  
    1.61 -    val ctxt' = ctxt
    1.62 -      |> Variable.set_body false
    1.63 -      |> (snd o Variable.add_fixes xs)
    1.64 -      |> fold Variable.declare_internal (asms @ props);
    1.65 -
    1.66 +    val goal = init (Conjunction.mk_conjunction_list cprops);
    1.67      val res =
    1.68 -      (case SINGLE (tac prems) (init (cert_safe prop)) of
    1.69 +      (case SINGLE (tac {prems = prems, context = ctxt'}) goal of
    1.70          NONE => err "Tactic failed."
    1.71        | SOME res => res);
    1.72 -    val [results] =
    1.73 -      Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg;
    1.74 -    val _ = Unify.matches_list thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    1.75 +    val [results] = Conjunction.elim_precise [length props] (finish res)
    1.76 +      handle THM (msg, _, _) => err msg;
    1.77 +    val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results)
    1.78        orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
    1.79    in
    1.80      results
    1.81 -    |> map (Drule.implies_intr_list casms)
    1.82 +    |> (Seq.hd o Assumption.exports false ctxt' ctxt)
    1.83      |> Variable.export ctxt' ctxt
    1.84 -    |> map (norm_hhf #> Drule.zero_var_indexes)
    1.85 +    |> map Drule.zero_var_indexes
    1.86    end;
    1.87  
    1.88  
    1.89 @@ -137,15 +143,7 @@
    1.90  fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
    1.91  
    1.92  fun prove_global thy xs asms prop tac =
    1.93 -  Drule.standard (prove (Context.init_proof thy) xs asms prop tac);
    1.94 -
    1.95 -
    1.96 -(* prove_raw -- no checks, no normalization of result! *)
    1.97 -
    1.98 -fun prove_raw casms cprop tac =
    1.99 -  (case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of
   1.100 -    SOME th => Drule.implies_intr_list casms (finish th)
   1.101 -  | NONE => error "Tactic failed.");
   1.102 +  Drule.standard (prove (Context.init_proof thy) xs asms prop (fn {prems, ...} => tac prems));
   1.103  
   1.104  
   1.105