# HG changeset patch
# User wenzelm
# Date 1248606774 -7200
# Node ID 2bd8ab91a426776be84c79fb5abe8843b101975c
# Parent  82c4c570310aef8489e2c4cb01e7fea98047106b
advanced retrofit, which allows new subgoals and variables;
added FOCUS -- does not require closed proof;

diff -r 82c4c570310a -r 2bd8ab91a426 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Sun Jul 26 13:12:54 2009 +0200
+++ b/src/Pure/subgoal.ML	Sun Jul 26 13:12:54 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;
+