# HG changeset patch
# User wenzelm
# Date 1433504466 -7200
# Node ID 8a5cfdda1b980a82e5a5df9c4f2a53c88f84d1fd
# Parent  9ec1d3d2068ebd27a44ae161dc640131facaa40e
added Isar command 'supply';

diff -r 9ec1d3d2068e -r 8a5cfdda1b98 NEWS
--- a/NEWS	Fri Jun 05 13:26:12 2015 +0200
+++ b/NEWS	Fri Jun 05 13:41:06 2015 +0200
@@ -9,6 +9,9 @@
 
 *** Pure ***
 
+* New Isar command 'supply' supports fact definitions during goal
+refinement ('apply' scripts).
+
 * Configuration option rule_insts_schematic has been discontinued
 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
 
diff -r 9ec1d3d2068e -r 8a5cfdda1b98 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Fri Jun 05 13:26:12 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Fri Jun 05 13:41:06 2015 +0200
@@ -860,6 +860,7 @@
   be used in scripts, too.
 
   \begin{matharray}{rcl}
+    @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
     @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
     @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
@@ -869,6 +870,8 @@
   \end{matharray}
 
   @{rail \<open>
+    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+    ;
     ( @@{command apply} | @@{command apply_end} ) @{syntax method}
     ;
     @@{command defer} @{syntax nat}?
@@ -878,6 +881,10 @@
 
   \begin{description}
 
+  \item @{command "supply"} supports fact definitions during goal
+  refinement: it is similar to @{command "note"}, but it operates in
+  backwards mode and does not have any impact on chained facts.
+
   \item @{command "apply"}~@{text m} applies proof method @{text m} in
   initial position, but unlike @{command "proof"} it retains ``@{text
   "proof(prove)"}'' mode.  Thus consecutive method applications may be
diff -r 9ec1d3d2068e -r 8a5cfdda1b98 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jun 05 13:26:12 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 05 13:41:06 2015 +0200
@@ -527,6 +527,10 @@
     (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
 
 val _ =
+  Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)"
+    (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
+
+val _ =
   Outer_Syntax.command @{command_keyword using} "augment goal facts"
     (facts >> (Toplevel.proof o Proof.using_cmd));
 
@@ -647,11 +651,11 @@
     (Parse.nat >> (Toplevel.proof o Proof.prefer));
 
 val _ =
-  Outer_Syntax.command @{command_keyword apply} "initial refinement step (unstructured)"
+  Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
 
 val _ =
-  Outer_Syntax.command @{command_keyword apply_end} "terminal refinement step (unstructured)"
+  Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
 
 val _ =
diff -r 9ec1d3d2068e -r 8a5cfdda1b98 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Jun 05 13:26:12 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Jun 05 13:41:06 2015 +0200
@@ -67,6 +67,8 @@
   val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   val with_thmss: ((thm list * attribute list) list) list -> state -> state
   val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
+  val supply: (Thm.binding * (thm list * attribute list) list) list -> state -> state
+  val supply_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
   val using: ((thm list * attribute list) list) list -> state -> state
   val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
   val unfolding: ((thm list * attribute list) list) list -> state -> state
@@ -706,6 +708,24 @@
 end;
 
 
+(* facts during goal refinement *)
+
+local
+
+fun gen_supply prep_att prep_fact args state =
+  state
+  |> assert_backward
+  |> map_context (fn ctxt => ctxt |> Proof_Context.note_thmss ""
+       (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) args) |> snd);
+
+in
+
+val supply = gen_supply (K I) (K I);
+val supply_cmd = gen_supply Attrib.attribute_cmd Proof_Context.get_fact;
+
+end;
+
+
 (* using/unfolding *)
 
 local
diff -r 9ec1d3d2068e -r 8a5cfdda1b98 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Jun 05 13:26:12 2015 +0200
+++ b/src/Pure/Pure.thy	Fri Jun 05 13:41:06 2015 +0200
@@ -51,7 +51,9 @@
   and "show" :: prf_asm_goal % "proof"
   and "thus" :: prf_asm_goal % "proof" == "then show"
   and "then" "from" "with" :: prf_chain % "proof"
-  and "note" "using" "unfolding" :: prf_decl % "proof"
+  and "note" :: prf_decl % "proof"
+  and "supply" :: prf_script % "proof"
+  and "using" "unfolding" :: prf_decl % "proof"
   and "fix" "assume" "presume" "def" :: prf_asm % "proof"
   and "obtain" :: prf_asm_goal % "proof"
   and "guess" :: prf_asm_goal_script % "proof"