clarified module;
authorwenzelm
Thu Jul 02 12:39:08 2015 +0200 (2015-07-02)
changeset 60630fc7625ec7427
parent 60629 d4e97fcdf83e
child 60631 441fdbfbb2d3
clarified module;
src/Pure/Isar/subgoal.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/subgoal.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/subgoal.ML	Thu Jul 02 12:39:08 2015 +0200
     1.3 @@ -0,0 +1,256 @@
     1.4 +(*  Title:      Pure/Isar/subgoal.ML
     1.5 +    Author:     Makarius
     1.6 +    Author:     Daniel Matichuk, NICTA/UNSW
     1.7 +
     1.8 +Tactical operations with explicit subgoal focus, based on canonical
     1.9 +proof decomposition.  The "visible" part of the text within the
    1.10 +context is fixed, the remaining goal may be schematic.
    1.11 +
    1.12 +Isar subgoal command for proof structure within unstructured proof
    1.13 +scripts.
    1.14 +*)
    1.15 +
    1.16 +signature SUBGOAL =
    1.17 +sig
    1.18 +  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    1.19 +    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
    1.20 +  val focus_params: Proof.context -> int -> thm -> focus * thm
    1.21 +  val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
    1.22 +  val focus_prems: Proof.context -> int -> thm -> focus * thm
    1.23 +  val focus: Proof.context -> int -> thm -> focus * thm
    1.24 +  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
    1.25 +    int -> thm -> thm -> thm Seq.seq
    1.26 +  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.27 +  val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
    1.28 +  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.29 +  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.30 +  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
    1.31 +  val subgoal: Attrib.binding -> Attrib.binding option ->
    1.32 +    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
    1.33 +  val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
    1.34 +    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
    1.35 +end;
    1.36 +
    1.37 +structure Subgoal: SUBGOAL =
    1.38 +struct
    1.39 +
    1.40 +(* focus *)
    1.41 +
    1.42 +type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    1.43 +  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
    1.44 +
    1.45 +fun gen_focus (do_prems, do_concl) ctxt i raw_st =
    1.46 +  let
    1.47 +    val st = raw_st
    1.48 +      |> Thm.transfer (Proof_Context.theory_of ctxt)
    1.49 +      |> Raw_Simplifier.norm_hhf_protect ctxt;
    1.50 +    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
    1.51 +    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
    1.52 +
    1.53 +    val (asms, concl) =
    1.54 +      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
    1.55 +      else ([], goal);
    1.56 +    val text = asms @ (if do_concl then [concl] else []);
    1.57 +
    1.58 +    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
    1.59 +    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
    1.60 +
    1.61 +    val schematics = (schematic_types, schematic_terms);
    1.62 +    val asms' = map (Thm.instantiate_cterm schematics) asms;
    1.63 +    val concl' = Thm.instantiate_cterm schematics concl;
    1.64 +    val (prems, context) = Assumption.add_assumes asms' ctxt3;
    1.65 +  in
    1.66 +    ({context = context, params = params, prems = prems,
    1.67 +      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
    1.68 +  end;
    1.69 +
    1.70 +val focus_params = gen_focus (false, false);
    1.71 +val focus_params_fixed = gen_focus (false, true);
    1.72 +val focus_prems = gen_focus (true, false);
    1.73 +val focus = gen_focus (true, true);
    1.74 +
    1.75 +
    1.76 +(* lift and retrofit *)
    1.77 +
    1.78 +(*
    1.79 +     B [?'b, ?y]
    1.80 +  ----------------
    1.81 +  B ['b, y params]
    1.82 +*)
    1.83 +fun lift_import idx params th ctxt =
    1.84 +  let
    1.85 +    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    1.86 +
    1.87 +    val Ts = map Thm.typ_of_cterm params;
    1.88 +    val ts = map Thm.term_of params;
    1.89 +
    1.90 +    val prop = Thm.full_prop_of th';
    1.91 +    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
    1.92 +    val vars = rev (Term.add_vars prop []);
    1.93 +    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
    1.94 +
    1.95 +    fun var_inst v y =
    1.96 +      let
    1.97 +        val ((x, i), T) = v;
    1.98 +        val (U, args) =
    1.99 +          if member (op =) concl_vars v then (T, [])
   1.100 +          else (Ts ---> T, ts);
   1.101 +        val u = Free (y, U);
   1.102 +        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
   1.103 +    val (inst1, inst2) =
   1.104 +      split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
   1.105 +
   1.106 +    val th'' = Thm.instantiate ([], inst1) th';
   1.107 +  in ((inst2, th''), ctxt'') end;
   1.108 +
   1.109 +(*
   1.110 +       [x, A x]
   1.111 +          :
   1.112 +       B x ==> C
   1.113 +  ------------------
   1.114 +  [!!x. A x ==> B x]
   1.115 +          :
   1.116 +          C
   1.117 +*)
   1.118 +fun lift_subgoals params asms th =
   1.119 +  let
   1.120 +    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
   1.121 +    val unlift =
   1.122 +      fold (Thm.elim_implies o Thm.assume) asms o
   1.123 +      Drule.forall_elim_list (map #2 params) o Thm.assume;
   1.124 +    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
   1.125 +    val th' = fold (Thm.elim_implies o unlift) subgoals th;
   1.126 +  in (subgoals, th') end;
   1.127 +
   1.128 +fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
   1.129 +  let
   1.130 +    val idx = Thm.maxidx_of st0 + 1;
   1.131 +    val ps = map #2 params;
   1.132 +    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
   1.133 +    val (subgoals, st3) = lift_subgoals params asms st2;
   1.134 +    val result = st3
   1.135 +      |> Goal.conclude
   1.136 +      |> Drule.implies_intr_list asms
   1.137 +      |> Drule.forall_intr_list ps
   1.138 +      |> Drule.implies_intr_list subgoals
   1.139 +      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
   1.140 +      |> fold (Thm.forall_elim o #2) subgoal_inst
   1.141 +      |> Thm.adjust_maxidx_thm idx
   1.142 +      |> singleton (Variable.export ctxt2 ctxt0);
   1.143 +  in
   1.144 +    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
   1.145 +      (false, result, Thm.nprems_of st1) i st0
   1.146 +  end;
   1.147 +
   1.148 +
   1.149 +(* tacticals *)
   1.150 +
   1.151 +fun GEN_FOCUS flags tac ctxt i st =
   1.152 +  if Thm.nprems_of st < i then Seq.empty
   1.153 +  else
   1.154 +    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
   1.155 +    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
   1.156 +
   1.157 +val FOCUS_PARAMS = GEN_FOCUS (false, false);
   1.158 +val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
   1.159 +val FOCUS_PREMS = GEN_FOCUS (true, false);
   1.160 +val FOCUS = GEN_FOCUS (true, true);
   1.161 +
   1.162 +fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
   1.163 +
   1.164 +
   1.165 +(* Isar subgoal command *)
   1.166 +
   1.167 +local
   1.168 +
   1.169 +fun rename_params ctxt (param_suffix, raw_param_specs) st =
   1.170 +  let
   1.171 +    val _ = if Thm.no_prems st then error "No subgoals!" else ();
   1.172 +    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
   1.173 +    val subgoal_params =
   1.174 +      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
   1.175 +      |> Term.variant_frees subgoal |> map #1;
   1.176 +
   1.177 +    val n = length subgoal_params;
   1.178 +    val m = length raw_param_specs;
   1.179 +    val _ =
   1.180 +      m <= n orelse
   1.181 +        error ("Excessive subgoal parameter specification" ^
   1.182 +          Position.here_list (map snd (drop n raw_param_specs)));
   1.183 +
   1.184 +    val param_specs =
   1.185 +      raw_param_specs |> map
   1.186 +        (fn (NONE, _) => NONE
   1.187 +          | (SOME x, pos) =>
   1.188 +              let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
   1.189 +              in SOME (Variable.check_name b) end)
   1.190 +      |> param_suffix ? append (replicate (n - m) NONE);
   1.191 +
   1.192 +    fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
   1.193 +      | rename_list _ ys = ys;
   1.194 +
   1.195 +    fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
   1.196 +          (c $ Abs (x, T, rename_prop xs t))
   1.197 +      | rename_prop [] t = t;
   1.198 +
   1.199 +    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
   1.200 +  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
   1.201 +
   1.202 +fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
   1.203 +  let
   1.204 +    val _ = Proof.assert_backward state;
   1.205 +
   1.206 +    val state1 = state |> Proof.refine_insert [];
   1.207 +    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
   1.208 +
   1.209 +    val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
   1.210 +    val (prems_binding, do_prems) =
   1.211 +      (case raw_prems_binding of
   1.212 +        SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
   1.213 +      | NONE => ((Binding.empty, []), false));
   1.214 +
   1.215 +    val (subgoal_focus, _) =
   1.216 +      rename_params ctxt param_specs st
   1.217 +      |> (if do_prems then focus else focus_params_fixed) ctxt 1;
   1.218 +
   1.219 +    fun after_qed (ctxt'', [[result]]) =
   1.220 +      Proof.end_block #> (fn state' =>
   1.221 +        let
   1.222 +          val ctxt' = Proof.context_of state';
   1.223 +          val results' =
   1.224 +            Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
   1.225 +        in
   1.226 +          state'
   1.227 +          |> Proof.refine_primitive (fn _ => fn _ =>
   1.228 +            retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
   1.229 +              (Goal.protect 0 result) st
   1.230 +            |> Seq.hd)
   1.231 +          |> Proof.map_context
   1.232 +            (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
   1.233 +        end)
   1.234 +      #> Proof.reset_facts
   1.235 +      #> Proof.enter_backward;
   1.236 +  in
   1.237 +    state1
   1.238 +    |> Proof.enter_forward
   1.239 +    |> Proof.using_facts []
   1.240 +    |> Proof.begin_block
   1.241 +    |> Proof.map_context (fn _ =>
   1.242 +      #context subgoal_focus
   1.243 +      |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
   1.244 +    |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
   1.245 +        NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
   1.246 +    |> Proof.using_facts facts
   1.247 +    |> pair subgoal_focus
   1.248 +  end;
   1.249 +
   1.250 +in
   1.251 +
   1.252 +val subgoal = gen_subgoal Attrib.attribute;
   1.253 +val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
   1.254 +
   1.255 +end;
   1.256 +
   1.257 +end;
   1.258 +
   1.259 +val SUBPROOF = Subgoal.SUBPROOF;
     2.1 --- a/src/Pure/ROOT	Thu Jul 02 12:33:04 2015 +0200
     2.2 +++ b/src/Pure/ROOT	Thu Jul 02 12:39:08 2015 +0200
     2.3 @@ -145,6 +145,7 @@
     2.4      "Isar/runtime.ML"
     2.5      "Isar/spec_rules.ML"
     2.6      "Isar/specification.ML"
     2.7 +    "Isar/subgoal.ML"
     2.8      "Isar/token.ML"
     2.9      "Isar/toplevel.ML"
    2.10      "Isar/typedecl.ML"
    2.11 @@ -253,7 +254,6 @@
    2.12      "simplifier.ML"
    2.13      "skip_proof.ML"
    2.14      "sorts.ML"
    2.15 -    "subgoal.ML"
    2.16      "tactic.ML"
    2.17      "tactical.ML"
    2.18      "term.ML"
     3.1 --- a/src/Pure/ROOT.ML	Thu Jul 02 12:33:04 2015 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Thu Jul 02 12:39:08 2015 +0200
     3.3 @@ -262,6 +262,7 @@
     3.4  use "Isar/proof.ML";
     3.5  use "Isar/element.ML";
     3.6  use "Isar/obtain.ML";
     3.7 +use "Isar/subgoal.ML";
     3.8  
     3.9  (*local theories and targets*)
    3.10  use "Isar/locale.ML";
    3.11 @@ -317,8 +318,6 @@
    3.12  (*theory and proof operations*)
    3.13  use "Isar/isar_cmd.ML";
    3.14  
    3.15 -use "subgoal.ML";
    3.16 -
    3.17  
    3.18  (* Isabelle/Isar system *)
    3.19  
     4.1 --- a/src/Pure/subgoal.ML	Thu Jul 02 12:33:04 2015 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,256 +0,0 @@
     4.4 -(*  Title:      Pure/subgoal.ML
     4.5 -    Author:     Makarius
     4.6 -    Author:     Daniel Matichuk, NICTA/UNSW
     4.7 -
     4.8 -Tactical operations with explicit subgoal focus, based on canonical
     4.9 -proof decomposition.  The "visible" part of the text within the
    4.10 -context is fixed, the remaining goal may be schematic.
    4.11 -
    4.12 -Isar subgoal command for proof structure within unstructured proof
    4.13 -scripts.
    4.14 -*)
    4.15 -
    4.16 -signature SUBGOAL =
    4.17 -sig
    4.18 -  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    4.19 -    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
    4.20 -  val focus_params: Proof.context -> int -> thm -> focus * thm
    4.21 -  val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
    4.22 -  val focus_prems: Proof.context -> int -> thm -> focus * thm
    4.23 -  val focus: Proof.context -> int -> thm -> focus * thm
    4.24 -  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
    4.25 -    int -> thm -> thm -> thm Seq.seq
    4.26 -  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
    4.27 -  val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
    4.28 -  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
    4.29 -  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
    4.30 -  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
    4.31 -  val subgoal: Attrib.binding -> Attrib.binding option ->
    4.32 -    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
    4.33 -  val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
    4.34 -    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
    4.35 -end;
    4.36 -
    4.37 -structure Subgoal: SUBGOAL =
    4.38 -struct
    4.39 -
    4.40 -(* focus *)
    4.41 -
    4.42 -type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    4.43 -  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
    4.44 -
    4.45 -fun gen_focus (do_prems, do_concl) ctxt i raw_st =
    4.46 -  let
    4.47 -    val st = raw_st
    4.48 -      |> Thm.transfer (Proof_Context.theory_of ctxt)
    4.49 -      |> Simplifier.norm_hhf_protect ctxt;
    4.50 -    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
    4.51 -    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
    4.52 -
    4.53 -    val (asms, concl) =
    4.54 -      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
    4.55 -      else ([], goal);
    4.56 -    val text = asms @ (if do_concl then [concl] else []);
    4.57 -
    4.58 -    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
    4.59 -    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
    4.60 -
    4.61 -    val schematics = (schematic_types, schematic_terms);
    4.62 -    val asms' = map (Thm.instantiate_cterm schematics) asms;
    4.63 -    val concl' = Thm.instantiate_cterm schematics concl;
    4.64 -    val (prems, context) = Assumption.add_assumes asms' ctxt3;
    4.65 -  in
    4.66 -    ({context = context, params = params, prems = prems,
    4.67 -      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
    4.68 -  end;
    4.69 -
    4.70 -val focus_params = gen_focus (false, false);
    4.71 -val focus_params_fixed = gen_focus (false, true);
    4.72 -val focus_prems = gen_focus (true, false);
    4.73 -val focus = gen_focus (true, true);
    4.74 -
    4.75 -
    4.76 -(* lift and retrofit *)
    4.77 -
    4.78 -(*
    4.79 -     B [?'b, ?y]
    4.80 -  ----------------
    4.81 -  B ['b, y params]
    4.82 -*)
    4.83 -fun lift_import idx params th ctxt =
    4.84 -  let
    4.85 -    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    4.86 -
    4.87 -    val Ts = map Thm.typ_of_cterm params;
    4.88 -    val ts = map Thm.term_of params;
    4.89 -
    4.90 -    val prop = Thm.full_prop_of th';
    4.91 -    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
    4.92 -    val vars = rev (Term.add_vars prop []);
    4.93 -    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
    4.94 -
    4.95 -    fun var_inst v y =
    4.96 -      let
    4.97 -        val ((x, i), T) = v;
    4.98 -        val (U, args) =
    4.99 -          if member (op =) concl_vars v then (T, [])
   4.100 -          else (Ts ---> T, ts);
   4.101 -        val u = Free (y, U);
   4.102 -        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
   4.103 -    val (inst1, inst2) =
   4.104 -      split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
   4.105 -
   4.106 -    val th'' = Thm.instantiate ([], inst1) th';
   4.107 -  in ((inst2, th''), ctxt'') end;
   4.108 -
   4.109 -(*
   4.110 -       [x, A x]
   4.111 -          :
   4.112 -       B x ==> C
   4.113 -  ------------------
   4.114 -  [!!x. A x ==> B x]
   4.115 -          :
   4.116 -          C
   4.117 -*)
   4.118 -fun lift_subgoals params asms th =
   4.119 -  let
   4.120 -    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
   4.121 -    val unlift =
   4.122 -      fold (Thm.elim_implies o Thm.assume) asms o
   4.123 -      Drule.forall_elim_list (map #2 params) o Thm.assume;
   4.124 -    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
   4.125 -    val th' = fold (Thm.elim_implies o unlift) subgoals th;
   4.126 -  in (subgoals, th') end;
   4.127 -
   4.128 -fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
   4.129 -  let
   4.130 -    val idx = Thm.maxidx_of st0 + 1;
   4.131 -    val ps = map #2 params;
   4.132 -    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
   4.133 -    val (subgoals, st3) = lift_subgoals params asms st2;
   4.134 -    val result = st3
   4.135 -      |> Goal.conclude
   4.136 -      |> Drule.implies_intr_list asms
   4.137 -      |> Drule.forall_intr_list ps
   4.138 -      |> Drule.implies_intr_list subgoals
   4.139 -      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
   4.140 -      |> fold (Thm.forall_elim o #2) subgoal_inst
   4.141 -      |> Thm.adjust_maxidx_thm idx
   4.142 -      |> singleton (Variable.export ctxt2 ctxt0);
   4.143 -  in
   4.144 -    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
   4.145 -      (false, result, Thm.nprems_of st1) i st0
   4.146 -  end;
   4.147 -
   4.148 -
   4.149 -(* tacticals *)
   4.150 -
   4.151 -fun GEN_FOCUS flags tac ctxt i st =
   4.152 -  if Thm.nprems_of st < i then Seq.empty
   4.153 -  else
   4.154 -    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
   4.155 -    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
   4.156 -
   4.157 -val FOCUS_PARAMS = GEN_FOCUS (false, false);
   4.158 -val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
   4.159 -val FOCUS_PREMS = GEN_FOCUS (true, false);
   4.160 -val FOCUS = GEN_FOCUS (true, true);
   4.161 -
   4.162 -fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
   4.163 -
   4.164 -
   4.165 -(* Isar subgoal command *)
   4.166 -
   4.167 -local
   4.168 -
   4.169 -fun rename_params ctxt (param_suffix, raw_param_specs) st =
   4.170 -  let
   4.171 -    val _ = if Thm.no_prems st then error "No subgoals!" else ();
   4.172 -    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
   4.173 -    val subgoal_params =
   4.174 -      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
   4.175 -      |> Term.variant_frees subgoal |> map #1;
   4.176 -
   4.177 -    val n = length subgoal_params;
   4.178 -    val m = length raw_param_specs;
   4.179 -    val _ =
   4.180 -      m <= n orelse
   4.181 -        error ("Excessive subgoal parameter specification" ^
   4.182 -          Position.here_list (map snd (drop n raw_param_specs)));
   4.183 -
   4.184 -    val param_specs =
   4.185 -      raw_param_specs |> map
   4.186 -        (fn (NONE, _) => NONE
   4.187 -          | (SOME x, pos) =>
   4.188 -              let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
   4.189 -              in SOME (Variable.check_name b) end)
   4.190 -      |> param_suffix ? append (replicate (n - m) NONE);
   4.191 -
   4.192 -    fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
   4.193 -      | rename_list _ ys = ys;
   4.194 -
   4.195 -    fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
   4.196 -          (c $ Abs (x, T, rename_prop xs t))
   4.197 -      | rename_prop [] t = t;
   4.198 -
   4.199 -    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
   4.200 -  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
   4.201 -
   4.202 -fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
   4.203 -  let
   4.204 -    val _ = Proof.assert_backward state;
   4.205 -
   4.206 -    val state1 = state |> Proof.refine_insert [];
   4.207 -    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
   4.208 -
   4.209 -    val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
   4.210 -    val (prems_binding, do_prems) =
   4.211 -      (case raw_prems_binding of
   4.212 -        SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
   4.213 -      | NONE => ((Binding.empty, []), false));
   4.214 -
   4.215 -    val (subgoal_focus, _) =
   4.216 -      rename_params ctxt param_specs st
   4.217 -      |> (if do_prems then focus else focus_params_fixed) ctxt 1;
   4.218 -
   4.219 -    fun after_qed (ctxt'', [[result]]) =
   4.220 -      Proof.end_block #> (fn state' =>
   4.221 -        let
   4.222 -          val ctxt' = Proof.context_of state';
   4.223 -          val results' =
   4.224 -            Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
   4.225 -        in
   4.226 -          state'
   4.227 -          |> Proof.refine_primitive (fn _ => fn _ =>
   4.228 -            retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
   4.229 -              (Goal.protect 0 result) st
   4.230 -            |> Seq.hd)
   4.231 -          |> Proof.map_context
   4.232 -            (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
   4.233 -        end)
   4.234 -      #> Proof.reset_facts
   4.235 -      #> Proof.enter_backward;
   4.236 -  in
   4.237 -    state1
   4.238 -    |> Proof.enter_forward
   4.239 -    |> Proof.using_facts []
   4.240 -    |> Proof.begin_block
   4.241 -    |> Proof.map_context (fn _ =>
   4.242 -      #context subgoal_focus
   4.243 -      |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
   4.244 -    |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
   4.245 -        NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
   4.246 -    |> Proof.using_facts facts
   4.247 -    |> pair subgoal_focus
   4.248 -  end;
   4.249 -
   4.250 -in
   4.251 -
   4.252 -val subgoal = gen_subgoal Attrib.attribute;
   4.253 -val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
   4.254 -
   4.255 -end;
   4.256 -
   4.257 -end;
   4.258 -
   4.259 -val SUBPROOF = Subgoal.SUBPROOF;