# HG changeset patch
# User wenzelm
# Date 1248627482 -7200
# Node ID 9a829b9ef00314068807c164df11610db4b042b1
# Parent  e6a42620e6c122f459b2a53e255ef6a99fe631d5# Parent  443d5cfaba1b7d6e51b2b9a984c976c1736a01ef
merged

diff -r e6a42620e6c1 -r 9a829b9ef003 doc-src/IsarImplementation/Thy/Proof.thy
--- a/doc-src/IsarImplementation/Thy/Proof.thy	Sun Jul 26 08:03:40 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Sun Jul 26 18:58:02 2009 +0200
@@ -95,7 +95,7 @@
   @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
   @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
   ((ctyp list * cterm list) * thm list) * Proof.context"} \\
-  @{index_ML Variable.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
+  @{index_ML Variable.focus: "cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context"} \\
   \end{mldecls}
 
   \begin{description}
@@ -284,10 +284,7 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML SUBPROOF:
-  "({context: Proof.context, schematics: ctyp list * cterm list,
-    params: cterm list, asms: cterm list, concl: cterm,
-    prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
+  @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\
   \end{mldecls}
   \begin{mldecls}
   @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
@@ -297,7 +294,7 @@
   \end{mldecls}
   \begin{mldecls}
   @{index_ML Obtain.result: "(Proof.context -> tactic) ->
-  thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
+  thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
   \end{mldecls}
 
   \begin{description}
diff -r e6a42620e6c1 -r 9a829b9ef003 doc-src/IsarImplementation/Thy/Tactic.thy
--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Sun Jul 26 08:03:40 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Sun Jul 26 18:58:02 2009 +0200
@@ -63,7 +63,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML Goal.init: "cterm -> thm"} \\
-  @{index_ML Goal.finish: "thm -> thm"} \\
+  @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
   @{index_ML Goal.protect: "thm -> thm"} \\
   @{index_ML Goal.conclude: "thm -> thm"} \\
   \end{mldecls}
@@ -73,9 +73,10 @@
   \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
   the well-formed proposition @{text C}.
 
-  \item @{ML "Goal.finish"}~@{text "thm"} checks whether theorem
+  \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
   @{text "thm"} is a solved goal (no subgoals), and concludes the
-  result by removing the goal protection.
+  result by removing the goal protection.  The context is only
+  required for printing error messages.
 
   \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
   of theorem @{text "thm"}.
diff -r e6a42620e6c1 -r 9a829b9ef003 doc-src/IsarImplementation/Thy/document/Proof.tex
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Sun Jul 26 08:03:40 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Sun Jul 26 18:58:02 2009 +0200
@@ -113,7 +113,7 @@
   \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
   \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
 \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
-  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
+  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context| \\
   \end{mldecls}
 
   \begin{description}
@@ -324,9 +324,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
-\verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
-\verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
+  \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
   \end{mldecls}
   \begin{mldecls}
   \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
@@ -336,7 +334,7 @@
   \end{mldecls}
   \begin{mldecls}
   \indexdef{}{ML}{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
-\verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
+\verb|  thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context| \\
   \end{mldecls}
 
   \begin{description}
diff -r e6a42620e6c1 -r 9a829b9ef003 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Sun Jul 26 08:03:40 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Sun Jul 26 18:58:02 2009 +0200
@@ -84,7 +84,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\
-  \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: thm -> thm| \\
+  \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: Proof.context -> thm -> thm| \\
   \indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\
   \indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
   \end{mldecls}
@@ -94,9 +94,10 @@
   \item \verb|Goal.init|~\isa{C} initializes a tactical goal from
   the well-formed proposition \isa{C}.
 
-  \item \verb|Goal.finish|~\isa{thm} checks whether theorem
+  \item \verb|Goal.finish|~\isa{ctxt\ thm} checks whether theorem
   \isa{thm} is a solved goal (no subgoals), and concludes the
-  result by removing the goal protection.
+  result by removing the goal protection.  The context is only
+  required for printing error messages.
 
   \item \verb|Goal.protect|~\isa{thm} protects the full statement
   of theorem \isa{thm}.
diff -r e6a42620e6c1 -r 9a829b9ef003 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -1257,7 +1257,7 @@
             [resolve_tac exists_fresh' 1,
              simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
                fin_set_supp @ ths)) 1]);
-        val (([cx], ths), ctxt') = Obtain.result
+        val (([(_, cx)], ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
@@ -1324,7 +1324,7 @@
                        val _ $ (_ $ _ $ u) = concl';
                        val U = fastype_of u;
                        val (xs, params') =
-                         chop (length cargs) (map term_of params);
+                         chop (length cargs) (map (term_of o #2) params);
                        val Ts = map fastype_of xs;
                        val cnstr = Const (cname, Ts ---> U);
                        val (pis, z) = split_last params';
@@ -1640,7 +1640,7 @@
                     REPEAT_DETERM (resolve_tac [allI, impI] 1),
                     REPEAT_DETERM (etac conjE 1),
                     rtac unique 1,
-                    SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
+                    SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
                       [cut_facts_tac [rec_prem] 1,
                        rtac (Thm.instantiate ([],
                          [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
@@ -1693,7 +1693,7 @@
              REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
              resolve_tac exists_fresh' 1,
              asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
-        val (([cx], ths), ctxt') = Obtain.result
+        val (([(_, cx)], ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
@@ -1763,7 +1763,7 @@
                     val cargsr' = partition_cargs idxs cargsr;
                     val boundsr = List.concat (map fst cargsr');
                     val (params1, _ :: params2) =
-                      chop (length params div 2) (map term_of params);
+                      chop (length params div 2) (map (term_of o #2) params);
                     val params' = params1 @ params2;
                     val rec_prems = filter (fn th => case prop_of th of
                         _ $ p => (case head_of p of
diff -r e6a42620e6c1 -r 9a829b9ef003 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -301,7 +301,7 @@
           (fn _ => EVERY
             [resolve_tac exists_fresh' 1,
              resolve_tac fs_atoms 1]);
-        val (([cx], ths), ctxt') = Obtain.result
+        val (([(_, cx)], ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
@@ -319,7 +319,7 @@
              SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
                let
                  val (params', (pis, z)) =
-                   chop (length params - length atomTs - 1) (map term_of params) ||>
+                   chop (length params - length atomTs - 1) (map (term_of o #2) params) ||>
                    split_last;
                  val bvars' = map
                    (fn (Bound i, T) => (nth params' (length params' - i), T)
@@ -474,7 +474,7 @@
                 rtac (first_order_mrs case_hyps case_hyp) 1
               else
                 let
-                  val params' = map (term_of o nth (rev params)) is;
+                  val params' = map (term_of o #2 o nth (rev params)) is;
                   val tab = params' ~~ map fst qs;
                   val (hyps1, hyps2) = chop (length args) case_hyps;
                   (* turns a = t and [x1 # t, ..., xn # t] *)
@@ -635,7 +635,7 @@
             val prems'' = map (fn th => Simplifier.simplify eqvt_ss
               (mk_perm_bool (cterm_of thy pi) th)) prems';
             val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
-               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of) params)
+               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
                intr
           in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
           end) ctxt' 1 st
diff -r e6a42620e6c1 -r 9a829b9ef003 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -323,7 +323,7 @@
         val avoid_th = Drule.instantiate'
           [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
           ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
-        val (([cx], th1 :: th2 :: ths), ctxt') = Obtain.result
+        val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [rtac avoid_th 1,
              full_simp_tac (HOL_ss addsimps [@{thm fresh_star_prod_set}]) 1,
@@ -359,7 +359,7 @@
              SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
                let
                  val (cparams', (pis, z)) =
-                   chop (length params - length atomTs - 1) params ||>
+                   chop (length params - length atomTs - 1) (map #2 params) ||>
                    (map term_of #> split_last);
                  val params' = map term_of cparams'
                  val sets' = map (apfst (curry subst_bounds (rev params'))) sets;
diff -r e6a42620e6c1 -r 9a829b9ef003 src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -210,7 +210,7 @@
 
     in
       if Thm.no_prems no_step
-      then NoStep (Goal.finish no_step RS no_stepI)
+      then NoStep (Goal.finish ctxt no_step RS no_stepI)
       else
         let
           fun set_m1 i =
@@ -240,10 +240,10 @@
                       val thm1 = decr with_m2
                     in
                       if Thm.no_prems thm1
-                      then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1))
+                      then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish ctxt thm1) 1))
                       else let val thm2 = decreq with_m2 in
                              if Thm.no_prems thm2
-                             then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1))
+                             then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish ctxt thm2) 1))
                              else all_tac end
                     end
               in set_m2 end
@@ -257,7 +257,7 @@
                     |> cterm_of thy
                     |> Goal.init
                     |> tac |> Seq.hd
-                    |> Goal.finish
+                    |> Goal.finish ctxt
 
           val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
         in
diff -r e6a42620e6c1 -r 9a829b9ef003 src/HOL/Tools/Function/fundef_lib.ML
--- a/src/HOL/Tools/Function/fundef_lib.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -126,7 +126,10 @@
 fun try_proof cgoal tac = 
     case SINGLE tac (Goal.init cgoal) of
       NONE => Fail
-    | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
+    | SOME st =>
+        if Thm.no_prems st
+        then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
+        else Stuck st
 
 
 fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
diff -r e6a42620e6c1 -r 9a829b9ef003 src/HOL/Tools/Function/induction_scheme.ML
--- a/src/HOL/Tools/Function/induction_scheme.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -324,7 +324,7 @@
                          THEN CONVERSION ind_rulify 1)
                      |> Seq.hd
                      |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
-                     |> Goal.finish
+                     |> Goal.finish ctxt
                      |> implies_intr (cprop_of branch_hyp)
                      |> fold_rev (forall_intr o cert) fxs
           in
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/Isar/element.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -213,7 +213,7 @@
   let
     val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
     val As = Logic.strip_imp_prems (Thm.term_of prop');
-  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
+  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of o #2) xs, As)), ctxt') end;
 
 in
 
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -44,7 +44,7 @@
   val obtain_i: string -> (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
-    (cterm list * thm list) * Proof.context
+    ((string * cterm) list * thm list) * Proof.context
   val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
 end;
@@ -200,7 +200,7 @@
     val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
     val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
-      Assumption.add_assms (obtain_export fix_ctxt obtain_rule params)
+      Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
         (Drule.strip_imp_prems stmt) fix_ctxt;
   in ((params, prems), ctxt'') end;
 
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/axclass.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -607,8 +607,10 @@
     val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
     val ths =
       sort |> map (fn c =>
-        Goal.finish (the (lookup_type cache' typ c) RS
-          Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
+        Goal.finish
+          (Syntax.init_pretty_global thy)
+          (the (lookup_type cache' typ c) RS
+            Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
         |> Thm.adjust_maxidx_thm ~1);
   in (ths, cache') end;
 
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/goal.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -18,7 +18,8 @@
   val init: cterm -> thm
   val protect: thm -> thm
   val conclude: thm -> thm
-  val finish: thm -> thm
+  val check_finished: Proof.context -> thm -> unit
+  val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
   val future_enabled: unit -> bool
   val local_future_enabled: unit -> bool
@@ -74,12 +75,15 @@
   --- (finish)
    C
 *)
-fun finish th =
+fun check_finished ctxt th =
   (case Thm.nprems_of th of
-    0 => conclude th
+    0 => ()
   | n => raise THM ("Proof failed.\n" ^
-      Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context n th)) ^
-      ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
+      Pretty.string_of (Pretty.chunks
+        (Goal_Display.pretty_goals ctxt {total = true, main = true, maxgoals = n} th)) ^
+      "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
+
+fun finish ctxt th = (check_finished ctxt th; conclude th);
 
 
 
@@ -145,7 +149,8 @@
 
 fun prove_internal casms cprop tac =
   (case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
-    SOME th => Drule.implies_intr_list casms (finish th)
+    SOME th => Drule.implies_intr_list casms
+      (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
   | NONE => error "Tactic failed.");
 
 
@@ -180,7 +185,7 @@
       (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
         NONE => err "Tactic failed."
       | SOME st =>
-          let val res = finish st handle THM (msg, _, _) => err msg in
+          let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
             if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
             then Thm.check_shyps sorts res
             else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/more_thm.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -11,6 +11,8 @@
   include THM
   val aconvc: cterm * cterm -> bool
   val add_cterm_frees: cterm -> cterm list -> cterm list
+  val all_name: string * cterm -> cterm -> cterm
+  val all: cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
   val dest_binop: cterm -> cterm * cterm
   val dest_implies: cterm -> cterm * cterm
@@ -102,6 +104,14 @@
 
 (* cterm constructors and destructors *)
 
+fun all_name (x, t) A =
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_cterm t);
+    val T = #T (Thm.rep_cterm t);
+  in Thm.capply (cert (Const ("all", (T --> propT) --> propT))) (Thm.cabs_name (x, t) A) end;
+
+fun all t A = all_name ("", t) A;
+
 fun mk_binop c a b = Thm.capply (Thm.capply c a) b;
 fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
 
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/subgoal.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -1,30 +1,28 @@
 (*  Title:      Pure/subgoal.ML
     Author:     Makarius
 
-Tactical operations depending on local subgoal structure.
+Tactical operations with explicit subgoal focus, based on
+canonical proof decomposition (similar to fix/assume/show).
 *)
 
-signature BASIC_SUBGOAL =
-sig
-  val SUBPROOF:
-    ({context: Proof.context, schematics: ctyp list * cterm list,
-      params: cterm list, asms: cterm list, concl: cterm,
-      prems: thm list} -> tactic) -> Proof.context -> int -> tactic
-end
-
 signature SUBGOAL =
 sig
-  include BASIC_SUBGOAL
-  val focus: Proof.context -> int -> thm ->
-   {context: Proof.context, schematics: ctyp list * cterm list,
-    params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
-
+  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+    asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
+  val focus: Proof.context -> int -> thm -> focus * thm
+  val retrofit: Proof.context -> (string * cterm) list -> cterm list ->
+    int -> thm -> thm -> thm Seq.seq
+  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
+  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
 end;
 
 structure Subgoal: SUBGOAL =
 struct
 
-(* canonical proof decomposition -- similar to fix/assume/show *)
+(* focus *)
+
+type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+  asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
 
 fun focus ctxt i st =
   let
@@ -35,24 +33,78 @@
     val concl = Drule.strip_imp_concl goal;
     val (prems, context) = Assumption.add_assumes asms ctxt'';
   in
-    ({context = context, schematics = schematics, params = params,
-      asms = asms, concl = concl, prems = prems}, Goal.init concl)
+    ({context = context, params = params, prems = prems,
+      asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
   end;
 
-fun SUBPROOF tac ctxt i st =
+
+(* lift and retrofit *)
+
+(*
+     B [?'b, ?y]
+  ----------------
+  B ['b, y params]
+*)
+fun lift_import params th ctxt =
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_thm th);
+    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
+
+    val Ts = map (#T o Thm.rep_cterm) params;
+    val ts = map Thm.term_of params;
+
+    val vars = rev (Term.add_vars (Thm.full_prop_of th') []);
+    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
+    fun var_inst (v as (_, T)) y =
+      (cert (Var v), cert (list_comb (Free (y, Ts ---> T), ts)));
+    val th'' = Thm.instantiate ([], map2 var_inst vars ys) th';
+  in (th'', ctxt'') end;
+
+(*
+        [A x]
+          :
+      B x ==> C
+  ------------------
+  [!!x. A x ==> B x]
+         :
+         C
+*)
+fun lift_subgoals params asms th =
+  let
+    val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms;
+    val unlift =
+      fold (Thm.elim_implies o Thm.assume) asms o
+      Drule.forall_elim_list (map #2 params) o Thm.assume;
+    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
+    val th' = fold (Thm.elim_implies o unlift) subgoals th;
+  in (subgoals, th') end;
+
+fun retrofit ctxt params asms i th =
+  let
+    val ps = map #2 params;
+    val res0 = Goal.conclude th;
+    val (res1, ctxt1) = lift_import ps res0 ctxt;
+    val (subgoals, res2) = lift_subgoals params asms res1;
+    val result = res2
+      |> Drule.implies_intr_list asms
+      |> Drule.forall_intr_list ps
+      |> Drule.implies_intr_list subgoals
+      |> singleton (Variable.export ctxt1 ctxt);
+  in Thm.compose_no_flatten false (result, Thm.nprems_of res0) i end;
+
+
+(* tacticals *)
+
+fun FOCUS tac ctxt i st =
   if Thm.nprems_of st < i then Seq.empty
   else
-    let
-      val (args as {context, params, ...}, st') = focus ctxt i st;
-      fun export_closed th =
-        let
-          val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
-          val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
-        in Drule.forall_intr_list vs th' end;
-      fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
-    in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
+    let val (args as {context, params, asms, ...}, st') = focus ctxt i st;
+    in Seq.lifts (retrofit context params asms i) (tac args st') st end;
+
+fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
 
 end;
 
-structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
-open BasicSubgoal;
+val FOCUS = Subgoal.FOCUS;
+val SUBPROOF = Subgoal.SUBPROOF;
+
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/term.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -151,6 +151,7 @@
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val map_abs_vars: (string -> string) -> term -> term
   val rename_abs: term -> term -> term -> term option
+  val lambda_name: string * term -> term -> term
   val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
   val maxidx_typs: typ list -> int -> int
@@ -719,14 +720,15 @@
         | _ => raise Same.SAME);
   in abs 0 body handle Same.SAME => body end;
 
-fun lambda v t =
-  let val x =
-    (case v of
-      Const (x, _) => Long_Name.base_name x
-    | Free (x, _) => x
-    | Var ((x, _), _) => x
-    | _ => Name.uu)
-  in Abs (x, fastype_of v, abstract_over (v, t)) end;
+fun term_name (Const (x, _)) = Long_Name.base_name x
+  | term_name (Free (x, _)) = x
+  | term_name (Var ((x, _), _)) = x
+  | term_name _ = Name.uu;
+
+fun lambda_name (x, v) t =
+  Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
+
+fun lambda v t = lambda_name ("", v) t;
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/thm.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -110,6 +110,7 @@
   val dest_arg1: cterm -> cterm
   val dest_abs: string option -> cterm -> cterm * cterm
   val capply: cterm -> cterm -> cterm
+  val cabs_name: string * cterm -> cterm -> cterm
   val cabs: cterm -> cterm -> cterm
   val adjust_maxidx_cterm: int -> cterm -> cterm
   val incr_indexes_cterm: int -> cterm -> cterm
@@ -274,16 +275,18 @@
       else raise CTERM ("capply: types don't agree", [cf, cx])
   | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);
 
-fun cabs
-  (ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
+fun cabs_name
+  (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
   (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
-    let val t = Term.lambda t1 t2 in
+    let val t = Term.lambda_name (x, t1) t2 in
       Cterm {thy_ref = merge_thys0 ct1 ct2,
         t = t, T = T1 --> T2,
         maxidx = Int.max (maxidx1, maxidx2),
         sorts = Sorts.union sorts1 sorts2}
     end;
 
+fun cabs t u = cabs_name ("", t) u;
+
 
 (* indexes *)
 
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Pure/variable.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -57,8 +57,8 @@
     ((ctyp list * cterm list) * thm list) * Proof.context
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
-  val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
-  val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
+  val focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
+  val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
   val polymorphic: Proof.context -> term list -> term list
@@ -477,7 +477,7 @@
     val ps' = ListPair.map (cert o Free) (xs', Ts);
     val goal' = fold forall_elim_prop ps' goal;
     val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
-  in ((ps', goal'), ctxt'') end;
+  in ((xs ~~ ps', goal'), ctxt'') end;
 
 fun focus_subgoal i st =
   let
diff -r e6a42620e6c1 -r 9a829b9ef003 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Sun Jul 26 08:03:40 2009 +0200
+++ b/src/Tools/coherent.ML	Sun Jul 26 18:58:02 2009 +0200
@@ -215,7 +215,7 @@
 fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
   rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
   SUBPROOF (fn {prems = prems', concl, context, ...} =>
-    let val xs = map term_of params @
+    let val xs = map (term_of o #2) params @
       map (fn (_, s) => Free (s, the (Variable.default_type context s)))
         (Variable.fixes_of context)
     in