# HG changeset patch
# User wenzelm
# Date 1435833548 -7200
# Node ID fc7625ec742748b95adc13796a631b97baf53734
# Parent  d4e97fcdf83ef3a864c28e8deabf56e467e62177
clarified module;

diff -r d4e97fcdf83e -r fc7625ec7427 src/Pure/Isar/subgoal.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/subgoal.ML	Thu Jul 02 12:39:08 2015 +0200
@@ -0,0 +1,256 @@
+(*  Title:      Pure/Isar/subgoal.ML
+    Author:     Makarius
+    Author:     Daniel Matichuk, NICTA/UNSW
+
+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.
+
+Isar subgoal command for proof structure within unstructured proof
+scripts.
+*)
+
+signature SUBGOAL =
+sig
+  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+  val focus_params: Proof.context -> int -> thm -> focus * thm
+  val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
+  val focus_prems: Proof.context -> int -> thm -> focus * thm
+  val focus: 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_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
+  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
+  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
+  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
+  val subgoal: Attrib.binding -> Attrib.binding option ->
+    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
+  val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
+    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
+end;
+
+structure Subgoal: SUBGOAL =
+struct
+
+(* focus *)
+
+type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
+
+fun gen_focus (do_prems, do_concl) ctxt i raw_st =
+  let
+    val st = raw_st
+      |> Thm.transfer (Proof_Context.theory_of ctxt)
+      |> Raw_Simplifier.norm_hhf_protect ctxt;
+    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
+    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
+
+    val (asms, concl) =
+      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 (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
+
+    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')
+  end;
+
+val focus_params = gen_focus (false, false);
+val focus_params_fixed = gen_focus (false, true);
+val focus_prems = gen_focus (true, false);
+val focus = gen_focus (true, true);
+
+
+(* lift and retrofit *)
+
+(*
+     B [?'b, ?y]
+  ----------------
+  B ['b, y params]
+*)
+fun lift_import idx params th ctxt =
+  let
+    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
+
+    val Ts = map Thm.typ_of_cterm params;
+    val ts = map Thm.term_of params;
+
+    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 y =
+      let
+        val ((x, i), T) = v;
+        val (U, args) =
+          if member (op =) concl_vars v then (T, [])
+          else (Ts ---> T, ts);
+        val u = Free (y, U);
+        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
+    val (inst1, inst2) =
+      split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
+
+    val th'' = Thm.instantiate ([], inst1) th';
+  in ((inst2, th''), ctxt'') end;
+
+(*
+       [x, A x]
+          :
+       B x ==> C
+  ------------------
+  [!!x. A x ==> B x]
+          :
+          C
+*)
+fun lift_subgoals params asms th =
+  let
+    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
+    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 ctxt1 ctxt0 params asms i st1 st0 =
+  let
+    val idx = Thm.maxidx_of st0 + 1;
+    val ps = map #2 params;
+    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
+    val (subgoals, st3) = lift_subgoals params asms st2;
+    val result = st3
+      |> Goal.conclude
+      |> Drule.implies_intr_list asms
+      |> Drule.forall_intr_list ps
+      |> Drule.implies_intr_list subgoals
+      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
+      |> fold (Thm.forall_elim o #2) subgoal_inst
+      |> Thm.adjust_maxidx_thm idx
+      |> singleton (Variable.export ctxt2 ctxt0);
+  in
+    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
+      (false, result, Thm.nprems_of st1) i st0
+  end;
+
+
+(* tacticals *)
+
+fun GEN_FOCUS flags tac ctxt i st =
+  if Thm.nprems_of st < i then Seq.empty
+  else
+    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
+    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
+
+val FOCUS_PARAMS = GEN_FOCUS (false, false);
+val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
+val FOCUS_PREMS = GEN_FOCUS (true, false);
+val FOCUS = GEN_FOCUS (true, true);
+
+fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
+
+
+(* Isar subgoal command *)
+
+local
+
+fun rename_params ctxt (param_suffix, raw_param_specs) st =
+  let
+    val _ = if Thm.no_prems st then error "No subgoals!" else ();
+    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
+    val subgoal_params =
+      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
+      |> Term.variant_frees subgoal |> map #1;
+
+    val n = length subgoal_params;
+    val m = length raw_param_specs;
+    val _ =
+      m <= n orelse
+        error ("Excessive subgoal parameter specification" ^
+          Position.here_list (map snd (drop n raw_param_specs)));
+
+    val param_specs =
+      raw_param_specs |> map
+        (fn (NONE, _) => NONE
+          | (SOME x, pos) =>
+              let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
+              in SOME (Variable.check_name b) end)
+      |> param_suffix ? append (replicate (n - m) NONE);
+
+    fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
+      | rename_list _ ys = ys;
+
+    fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
+          (c $ Abs (x, T, rename_prop xs t))
+      | rename_prop [] t = t;
+
+    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
+  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
+
+fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
+  let
+    val _ = Proof.assert_backward state;
+
+    val state1 = state |> Proof.refine_insert [];
+    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
+
+    val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
+    val (prems_binding, do_prems) =
+      (case raw_prems_binding of
+        SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
+      | NONE => ((Binding.empty, []), false));
+
+    val (subgoal_focus, _) =
+      rename_params ctxt param_specs st
+      |> (if do_prems then focus else focus_params_fixed) ctxt 1;
+
+    fun after_qed (ctxt'', [[result]]) =
+      Proof.end_block #> (fn state' =>
+        let
+          val ctxt' = Proof.context_of state';
+          val results' =
+            Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
+        in
+          state'
+          |> Proof.refine_primitive (fn _ => fn _ =>
+            retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
+              (Goal.protect 0 result) st
+            |> Seq.hd)
+          |> Proof.map_context
+            (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
+        end)
+      #> Proof.reset_facts
+      #> Proof.enter_backward;
+  in
+    state1
+    |> Proof.enter_forward
+    |> Proof.using_facts []
+    |> Proof.begin_block
+    |> Proof.map_context (fn _ =>
+      #context subgoal_focus
+      |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
+    |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
+        NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
+    |> Proof.using_facts facts
+    |> pair subgoal_focus
+  end;
+
+in
+
+val subgoal = gen_subgoal Attrib.attribute;
+val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
+
+end;
+
+end;
+
+val SUBPROOF = Subgoal.SUBPROOF;
diff -r d4e97fcdf83e -r fc7625ec7427 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Jul 02 12:33:04 2015 +0200
+++ b/src/Pure/ROOT	Thu Jul 02 12:39:08 2015 +0200
@@ -145,6 +145,7 @@
     "Isar/runtime.ML"
     "Isar/spec_rules.ML"
     "Isar/specification.ML"
+    "Isar/subgoal.ML"
     "Isar/token.ML"
     "Isar/toplevel.ML"
     "Isar/typedecl.ML"
@@ -253,7 +254,6 @@
     "simplifier.ML"
     "skip_proof.ML"
     "sorts.ML"
-    "subgoal.ML"
     "tactic.ML"
     "tactical.ML"
     "term.ML"
diff -r d4e97fcdf83e -r fc7625ec7427 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jul 02 12:33:04 2015 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 02 12:39:08 2015 +0200
@@ -262,6 +262,7 @@
 use "Isar/proof.ML";
 use "Isar/element.ML";
 use "Isar/obtain.ML";
+use "Isar/subgoal.ML";
 
 (*local theories and targets*)
 use "Isar/locale.ML";
@@ -317,8 +318,6 @@
 (*theory and proof operations*)
 use "Isar/isar_cmd.ML";
 
-use "subgoal.ML";
-
 
 (* Isabelle/Isar system *)
 
diff -r d4e97fcdf83e -r fc7625ec7427 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Thu Jul 02 12:33:04 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-(*  Title:      Pure/subgoal.ML
-    Author:     Makarius
-    Author:     Daniel Matichuk, NICTA/UNSW
-
-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.
-
-Isar subgoal command for proof structure within unstructured proof
-scripts.
-*)
-
-signature SUBGOAL =
-sig
-  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
-  val focus_params: Proof.context -> int -> thm -> focus * thm
-  val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
-  val focus_prems: Proof.context -> int -> thm -> focus * thm
-  val focus: 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_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
-  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
-  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
-  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
-  val subgoal: Attrib.binding -> Attrib.binding option ->
-    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
-  val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
-    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
-end;
-
-structure Subgoal: SUBGOAL =
-struct
-
-(* focus *)
-
-type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
-  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
-
-fun gen_focus (do_prems, do_concl) ctxt i raw_st =
-  let
-    val st = raw_st
-      |> Thm.transfer (Proof_Context.theory_of ctxt)
-      |> Simplifier.norm_hhf_protect ctxt;
-    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
-    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
-
-    val (asms, concl) =
-      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 (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
-    val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
-
-    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')
-  end;
-
-val focus_params = gen_focus (false, false);
-val focus_params_fixed = gen_focus (false, true);
-val focus_prems = gen_focus (true, false);
-val focus = gen_focus (true, true);
-
-
-(* lift and retrofit *)
-
-(*
-     B [?'b, ?y]
-  ----------------
-  B ['b, y params]
-*)
-fun lift_import idx params th ctxt =
-  let
-    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
-
-    val Ts = map Thm.typ_of_cterm params;
-    val ts = map Thm.term_of params;
-
-    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 y =
-      let
-        val ((x, i), T) = v;
-        val (U, args) =
-          if member (op =) concl_vars v then (T, [])
-          else (Ts ---> T, ts);
-        val u = Free (y, U);
-        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
-    val (inst1, inst2) =
-      split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
-
-    val th'' = Thm.instantiate ([], inst1) th';
-  in ((inst2, th''), ctxt'') end;
-
-(*
-       [x, A x]
-          :
-       B x ==> C
-  ------------------
-  [!!x. A x ==> B x]
-          :
-          C
-*)
-fun lift_subgoals params asms th =
-  let
-    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
-    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 ctxt1 ctxt0 params asms i st1 st0 =
-  let
-    val idx = Thm.maxidx_of st0 + 1;
-    val ps = map #2 params;
-    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
-    val (subgoals, st3) = lift_subgoals params asms st2;
-    val result = st3
-      |> Goal.conclude
-      |> Drule.implies_intr_list asms
-      |> Drule.forall_intr_list ps
-      |> Drule.implies_intr_list subgoals
-      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
-      |> fold (Thm.forall_elim o #2) subgoal_inst
-      |> Thm.adjust_maxidx_thm idx
-      |> singleton (Variable.export ctxt2 ctxt0);
-  in
-    Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
-      (false, result, Thm.nprems_of st1) i st0
-  end;
-
-
-(* tacticals *)
-
-fun GEN_FOCUS flags tac ctxt i st =
-  if Thm.nprems_of st < i then Seq.empty
-  else
-    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
-    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
-
-val FOCUS_PARAMS = GEN_FOCUS (false, false);
-val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
-val FOCUS_PREMS = GEN_FOCUS (true, false);
-val FOCUS = GEN_FOCUS (true, true);
-
-fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
-
-
-(* Isar subgoal command *)
-
-local
-
-fun rename_params ctxt (param_suffix, raw_param_specs) st =
-  let
-    val _ = if Thm.no_prems st then error "No subgoals!" else ();
-    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
-    val subgoal_params =
-      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
-      |> Term.variant_frees subgoal |> map #1;
-
-    val n = length subgoal_params;
-    val m = length raw_param_specs;
-    val _ =
-      m <= n orelse
-        error ("Excessive subgoal parameter specification" ^
-          Position.here_list (map snd (drop n raw_param_specs)));
-
-    val param_specs =
-      raw_param_specs |> map
-        (fn (NONE, _) => NONE
-          | (SOME x, pos) =>
-              let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
-              in SOME (Variable.check_name b) end)
-      |> param_suffix ? append (replicate (n - m) NONE);
-
-    fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
-      | rename_list _ ys = ys;
-
-    fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
-          (c $ Abs (x, T, rename_prop xs t))
-      | rename_prop [] t = t;
-
-    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
-  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
-
-fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
-  let
-    val _ = Proof.assert_backward state;
-
-    val state1 = state |> Proof.refine_insert [];
-    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
-
-    val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
-    val (prems_binding, do_prems) =
-      (case raw_prems_binding of
-        SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
-      | NONE => ((Binding.empty, []), false));
-
-    val (subgoal_focus, _) =
-      rename_params ctxt param_specs st
-      |> (if do_prems then focus else focus_params_fixed) ctxt 1;
-
-    fun after_qed (ctxt'', [[result]]) =
-      Proof.end_block #> (fn state' =>
-        let
-          val ctxt' = Proof.context_of state';
-          val results' =
-            Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
-        in
-          state'
-          |> Proof.refine_primitive (fn _ => fn _ =>
-            retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
-              (Goal.protect 0 result) st
-            |> Seq.hd)
-          |> Proof.map_context
-            (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
-        end)
-      #> Proof.reset_facts
-      #> Proof.enter_backward;
-  in
-    state1
-    |> Proof.enter_forward
-    |> Proof.using_facts []
-    |> Proof.begin_block
-    |> Proof.map_context (fn _ =>
-      #context subgoal_focus
-      |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
-    |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
-        NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
-    |> Proof.using_facts facts
-    |> pair subgoal_focus
-  end;
-
-in
-
-val subgoal = gen_subgoal Attrib.attribute;
-val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
-
-end;
-
-end;
-
-val SUBPROOF = Subgoal.SUBPROOF;