1.1 --- a/src/Pure/goal.ML	Tue Sep 23 18:31:33 2008 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Sep 23 22:04:30 2008 +0200
     1.3 @@ -20,9 +20,12 @@
     1.4    val conclude: thm -> thm
     1.5    val finish: thm -> thm
     1.6    val norm_result: thm -> thm
     1.7 +  val promise_result: Proof.context -> (unit -> thm) -> term -> thm
     1.8    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
     1.9    val prove_multi: Proof.context -> string list -> term list -> term list ->
    1.10      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    1.11 +  val prove_promise: Proof.context -> string list -> term list -> term ->
    1.12 +    ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.13    val prove: Proof.context -> string list -> term list -> term ->
    1.14      ({prems: thm list, context: Proof.context} -> tactic) -> thm
    1.15    val prove_global: theory -> string list -> term list -> term ->
    1.16 @@ -84,6 +87,8 @@
    1.17  
    1.18  (** results **)
    1.19  
    1.20 +(* normal form *)
    1.21 +
    1.22  val norm_result =
    1.23    Drule.flexflex_unique
    1.24    #> MetaSimplifier.norm_hhf_protect
    1.25 @@ -91,6 +96,39 @@
    1.26    #> Drule.zero_var_indexes;
    1.27  
    1.28  
    1.29 +(* promise *)
    1.30 +
    1.31 +fun promise_result ctxt result prop =
    1.32 +  let
    1.33 +    val thy = ProofContext.theory_of ctxt;
    1.34 +    val _ = Context.reject_draft thy;
    1.35 +    val cert = Thm.cterm_of thy;
    1.36 +    val certT = Thm.ctyp_of thy;
    1.37 +
    1.38 +    val assms = Assumption.assms_of ctxt;
    1.39 +    val As = map Thm.term_of assms;
    1.40 +
    1.41 +    val xs = map Free (fold Term.add_frees (prop :: As) []);
    1.42 +    val fixes = map cert xs;
    1.43 +
    1.44 +    val tfrees = fold Term.add_tfrees (prop :: As) [];
    1.45 +    val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
    1.46 +
    1.47 +    val global_prop =
    1.48 +      Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
    1.49 +    val global_result =
    1.50 +      Thm.generalize (map #1 tfrees, []) 0 o
    1.51 +      Drule.forall_intr_list fixes o
    1.52 +      Drule.implies_intr_list assms o
    1.53 +      Thm.adjust_maxidx_thm ~1 o result;
    1.54 +    val local_result =
    1.55 +      Thm.promise (Future.fork_irrelevant global_result) (cert global_prop)
    1.56 +      |> Thm.instantiate (instT, [])
    1.57 +      |> Drule.forall_elim_list fixes
    1.58 +      |> fold (Thm.elim_implies o Thm.assume) assms;
    1.59 +  in local_result end;
    1.60 +
    1.61 +
    1.62  
    1.63  (** tactical theorem proving **)
    1.64  
    1.65 @@ -102,9 +140,9 @@
    1.66    | NONE => error "Tactic failed.");
    1.67  
    1.68  
    1.69 -(* prove_multi *)
    1.70 +(* prove_common etc. *)
    1.71  
    1.72 -fun prove_multi ctxt xs asms props tac =
    1.73 +fun prove_common immediate ctxt xs asms props tac =
    1.74    let
    1.75      val thy = ProofContext.theory_of ctxt;
    1.76      val string_of_term = Syntax.string_of_term ctxt;
    1.77 @@ -124,26 +162,30 @@
    1.78        |> Assumption.add_assumes casms
    1.79        ||> Variable.set_body true;
    1.80  
    1.81 -    val goal = init (Conjunction.mk_conjunction_balanced cprops);
    1.82 -    val res =
    1.83 -      (case SINGLE (tac {prems = prems, context = ctxt'}) goal of
    1.84 +    val stmt = Conjunction.mk_conjunction_balanced cprops;
    1.85 +
    1.86 +    fun result () =
    1.87 +      (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
    1.88          NONE => err "Tactic failed."
    1.89 -      | SOME res => res);
    1.90 -    val results = Conjunction.elim_balanced (length props) (finish res)
    1.91 -      handle THM (msg, _, _) => err msg;
    1.92 -    val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results)
    1.93 -      orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
    1.94 +      | SOME st =>
    1.95 +          let val res = finish st handle THM (msg, _, _) => err msg in
    1.96 +            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
    1.97 +            else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
    1.98 +          end);
    1.99 +    val res =
   1.100 +      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
   1.101 +      else promise_result ctxt result (Thm.term_of stmt);
   1.102    in
   1.103 -    results
   1.104 +    Conjunction.elim_balanced (length props) res
   1.105      |> map (Assumption.export false ctxt' ctxt)
   1.106      |> Variable.export ctxt' ctxt
   1.107      |> map Drule.zero_var_indexes
   1.108    end;
   1.109  
   1.110 +val prove_multi = prove_common false;
   1.111  
   1.112 -(* prove *)
   1.113 -
   1.114 -fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
   1.115 +fun prove_promise ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
   1.116 +fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
   1.117  
   1.118  fun prove_global thy xs asms prop tac =
   1.119    Drule.standard (prove (ProofContext.init thy) xs asms prop tac);