--- a/src/HOL/Eisbach/Eisbach.thy Wed Jul 01 10:53:14 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Wed Jul 01 21:29:57 2015 +0200
@@ -9,7 +9,6 @@
keywords
"method" :: thy_decl and
"conclusion"
- "premises"
"declares"
"methods"
"\<bar>" "\<Rightarrow>"
--- a/src/Pure/Isar/isar_syn.ML Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jul 01 21:29:57 2015 +0200
@@ -679,6 +679,32 @@
Toplevel.skip_proof (fn i => i + 1))));
+(* subgoal focus *)
+
+local
+
+val opt_fact_binding =
+ Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
+ Attrib.empty_binding;
+
+val params =
+ Parse.binding -- Parse.mixfix' >> single || Scan.repeat1 Parse.binding >> map (rpair NoSyn);
+
+val for_params =
+ Scan.optional (@{keyword "for"} |-- Parse.!!! (Parse.and_list1 params >> flat)) [];
+
+in
+
+val _ =
+ Outer_Syntax.command @{command_keyword subgoal}
+ "focus on first subgoal within backward refinement"
+ (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
+ for_params >> (fn ((a, b), c) =>
+ Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
+
+end;
+
+
(* proof navigation *)
fun report_back () =
--- a/src/Pure/Isar/proof.ML Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jul 01 21:29:57 2015 +0200
@@ -33,10 +33,12 @@
val enter_chain: state -> state
val enter_backward: state -> state
val has_bottom_goal: state -> bool
+ val using_facts: thm list -> state -> state
val pretty_state: state -> Pretty.T list
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
val refine_insert: thm list -> state -> state
+ val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
val simple_goal: state -> {context: context, goal: thm}
@@ -430,6 +432,9 @@
fun refine_insert ths =
Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_primitive r = (* FIXME Seq.Error!? *)
+ Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt))));
+
end;
--- a/src/Pure/Pure.thy Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/Pure.thy Wed Jul 01 21:29:57 2015 +0200
@@ -11,7 +11,7 @@
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
- "overloaded" "pervasive" "private" "qualified" "shows"
+ "overloaded" "pervasive" "premises" "private" "qualified" "shows"
"structure" "unchecked" "where" "when" "|"
and "text" "txt" :: document_body
and "text_raw" :: document_raw
@@ -69,6 +69,7 @@
and "oops" :: qed_global % "proof"
and "defer" "prefer" "apply" :: prf_script % "proof"
and "apply_end" :: prf_script % "proof" == ""
+ and "subgoal" :: prf_goal % "proof"
and "proof" :: prf_block % "proof"
and "also" "moreover" :: prf_decl % "proof"
and "finally" "ultimately" :: prf_chain % "proof"
--- a/src/Pure/conjunction.ML Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/conjunction.ML Wed Jul 01 21:29:57 2015 +0200
@@ -19,6 +19,7 @@
val intr: thm -> thm -> thm
val intr_balanced: thm list -> thm
val elim: thm -> thm * thm
+ val elim_conjunctions: thm -> thm list
val elim_balanced: int -> thm -> thm list
val curry_balanced: int -> thm -> thm
val uncurry_balanced: int -> thm -> thm
@@ -118,6 +119,11 @@
end;
+fun elim_conjunctions th =
+ (case try elim th of
+ NONE => [th]
+ | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2);
+
(* balanced conjuncts *)
--- a/src/Pure/subgoal.ML Wed Jul 01 10:53:14 2015 +0200
+++ b/src/Pure/subgoal.ML Wed Jul 01 21:29:57 2015 +0200
@@ -1,9 +1,13 @@
(* 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 =
@@ -19,6 +23,10 @@
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 -> (binding * mixfix) list ->
+ Proof.state -> focus * Proof.state
+ val subgoal_cmd: Attrib.binding -> Attrib.binding option -> (binding * mixfix) list ->
+ Proof.state -> focus * Proof.state
end;
structure Subgoal: SUBGOAL =
@@ -146,7 +154,64 @@
fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
+
+(* Isar subgoal command *)
+
+local
+
+fun gen_focus prep_atts raw_result_binding raw_prems_binding params state =
+ let
+ val _ = Proof.assert_backward state;
+ val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state;
+
+ 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));
+
+ fun check_param (b, mx) = ignore (Proof_Context.cert_var (b, NONE, mx) ctxt);
+ val _ = List.app check_param params;
+
+ val _ = if Thm.no_prems st then error "No subgoals!" else ();
+ val subgoal_focus = #1 (focus ctxt 1 st); (* FIXME clarify prems/params *)
+
+ 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);
+ in
+ state
+ |> 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_focus Attrib.attribute;
+val subgoal_cmd = gen_focus Attrib.attribute_cmd;
+
+end;
+
end;
val SUBPROOF = Subgoal.SUBPROOF;
-