# HG changeset patch
# User wenzelm
# Date 1248945797 -7200
# Node ID 750101435f60248873c03dd48721bddaa57bc6af
# Parent  4fb3f426052a94c9779a71ca6098ed69e988fb36
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
added FOCUS_PREMS, which may serve as full replacement for OldGoals.METAHYPS;

diff -r 4fb3f426052a -r 750101435f60 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Thu Jul 30 01:14:40 2009 +0200
+++ b/src/Pure/subgoal.ML	Thu Jul 30 11:23:17 2009 +0200
@@ -1,20 +1,23 @@
 (*  Title:      Pure/subgoal.ML
     Author:     Makarius
 
-Tactical operations with explicit subgoal focus, based on
-canonical proof decomposition (similar to fix/assume/show).
+Tactical operations with explicit subgoal focus, based on canonical
+proof decomposition.  The "visible" part of the text within the
+context is fixed, the remaining goal may be schematic.
 *)
 
 signature SUBGOAL =
 sig
   type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-    asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
+    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+  val focus_params: Proof.context -> int -> thm -> focus * thm
+  val focus_prems: Proof.context -> int -> thm -> focus * thm
   val focus: Proof.context -> int -> thm -> focus * thm
-  val focus_params: Proof.context -> int -> thm -> focus * thm
   val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
     int -> thm -> thm -> thm Seq.seq
+  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
+  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
-  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
 end;
 
@@ -24,24 +27,35 @@
 (* focus *)
 
 type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-  asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
+  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
 
-fun gen_focus params_only ctxt i st =
+fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   let
-    val ((schematics, [st']), ctxt') =
-      Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
-    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
+    val st = Simplifier.norm_hhf_protect raw_st;
+    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
+    val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
+
     val (asms, concl) =
-      if params_only then ([], goal)
-      else (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal);
-    val (prems, context) = Assumption.add_assumes asms ctxt'';
+      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
+      else ([], goal);
+    val text = asms @ (if do_concl then [concl] else []);
+
+    val ((_, schematic_terms), ctxt3) =
+      Variable.import_inst true (map Thm.term_of text) ctxt2
+      |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
+
+    val schematics = (schematic_types, schematic_terms);
+    val asms' = map (Thm.instantiate_cterm schematics) asms;
+    val concl' = Thm.instantiate_cterm schematics concl;
+    val (prems, context) = Assumption.add_assumes asms' ctxt3;
   in
     ({context = context, params = params, prems = prems,
-      asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
+      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
   end;
 
-val focus = gen_focus false;
-val focus_params = gen_focus true;
+val focus_params = gen_focus (false, false);
+val focus_prems = gen_focus (true, false);
+val focus = gen_focus (true, true);
 
 
 (* lift and retrofit *)
@@ -53,27 +67,29 @@
 *)
 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 prop = Thm.full_prop_of th';
+    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
+    val vars = rev (Term.add_vars prop []);
     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';
+      if member (op =) concl_vars v then (v, Free (y, T))
+      else (v, list_comb (Free (y, Ts ---> T), ts));
+    val th'' = Thm.certify_instantiate ([], map2 var_inst vars ys) th';
   in (th'', ctxt'') end;
 
 (*
-      [x, A x]
+       [x, A x]
           :
-      B x ==> C
+       B x ==> C
   ------------------
   [!!x. A x ==> B x]
-         :
-         C
+          :
+          C
 *)
 fun lift_subgoals params asms th =
   let
@@ -103,20 +119,22 @@
 
 (* tacticals *)
 
-fun GEN_FOCUS params_only tac ctxt i st =
+fun GEN_FOCUS flags tac ctxt i st =
   if Thm.nprems_of st < i then Seq.empty
   else
-    let val (args as {context, params, asms, ...}, st') = gen_focus params_only ctxt i st;
+    let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st;
     in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
 
-val FOCUS = GEN_FOCUS false;
-val FOCUS_PARAMS = GEN_FOCUS true;
+val FOCUS_PARAMS = GEN_FOCUS (false, false);
+val FOCUS_PREMS = GEN_FOCUS (true, false);
+val FOCUS = GEN_FOCUS (true, true);
 
 fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
 
 end;
 
+val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
+val FOCUS_PREMS = Subgoal.FOCUS_PREMS;
 val FOCUS = Subgoal.FOCUS;
-val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
 val SUBPROOF = Subgoal.SUBPROOF;