src/Pure/goal.ML
changeset 20056 0698a403a066
parent 19862 7f29aa958b72
child 20157 28638d2a6bc7
     1.1 --- a/src/Pure/goal.ML	Sat Jul 08 12:54:43 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Sat Jul 08 12:54:44 2006 +0200
     1.3 @@ -22,9 +22,10 @@
     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_multi: theory -> string list -> term list -> term list ->
     1.8 +  val prove_multi: Context.proof -> string list -> term list -> term list ->
     1.9      (thm list -> tactic) -> thm list
    1.10 -  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.11 +  val prove: Context.proof -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.12 +  val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.13    val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.14    val extract: int -> int -> thm -> thm Seq.seq
    1.15    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    1.16 @@ -116,28 +117,29 @@
    1.17  
    1.18  (* prove_multi *)
    1.19  
    1.20 -fun prove_multi thy xs asms props tac =
    1.21 +fun prove_multi ctxt xs asms props tac =
    1.22    let
    1.23 +    val thy = Context.theory_of_proof ctxt;
    1.24 +    val string_of_term = Sign.string_of_term thy;
    1.25 +
    1.26      val prop = Logic.mk_conjunction_list props;
    1.27      val statement = Logic.list_implies (asms, prop);
    1.28 -    val frees = Term.add_frees statement [];
    1.29 -    val fixed_frees = filter_out (member (op =) xs o #1) frees;
    1.30 -    val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
    1.31 -    val params = map_filter (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    1.32  
    1.33      fun err msg = cat_error msg
    1.34 -      ("The error(s) above occurred for the goal statement:\n" ^
    1.35 -        Sign.string_of_term thy (Term.list_all_free (params, statement)));
    1.36 +      ("The error(s) above occurred for the goal statement:\n" ^ string_of_term statement);
    1.37      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
    1.38        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.39  
    1.40      val _ = cert_safe statement;
    1.41      val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
    1.42 -
    1.43 -    val cparams = map (cert_safe o Free) params;
    1.44      val casms = map cert_safe asms;
    1.45      val prems = map (norm_hhf o Thm.assume) casms;
    1.46  
    1.47 +    val ctxt' = ctxt
    1.48 +      |> Variable.set_body false
    1.49 +      |> (snd o Variable.add_fixes xs)
    1.50 +      |> fold Variable.declare_term (asms @ props);
    1.51 +
    1.52      val res =
    1.53        (case SINGLE (tac prems) (init (cert_safe prop)) of
    1.54          NONE => err "Tactic failed."
    1.55 @@ -145,20 +147,21 @@
    1.56      val [results] =
    1.57        Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg;
    1.58      val _ = Unify.matches_list thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    1.59 -      orelse err ("Proved a different theorem: " ^ Sign.string_of_term thy (Thm.prop_of res));
    1.60 +      orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
    1.61    in
    1.62 -    results |> map
    1.63 -      (Drule.implies_intr_list casms
    1.64 -        #> Drule.forall_intr_list cparams
    1.65 -        #> norm_hhf
    1.66 -        #> Thm.varifyT' fixed_tfrees
    1.67 -        #-> K Drule.zero_var_indexes)
    1.68 +    results
    1.69 +    |> map (Drule.implies_intr_list casms)
    1.70 +    |> Variable.export ctxt' ctxt
    1.71 +    |> map (norm_hhf #> Drule.zero_var_indexes)
    1.72    end;
    1.73  
    1.74  
    1.75  (* prove *)
    1.76  
    1.77 -fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
    1.78 +fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
    1.79 +
    1.80 +fun prove_global thy xs asms prop tac =
    1.81 +  Drule.standard (prove (Context.init_proof thy) xs asms prop tac);
    1.82  
    1.83  
    1.84  (* prove_raw -- no checks, no normalization of result! *)