added Isar command 'supply';
authorwenzelm
Fri Jun 05 13:41:06 2015 +0200 (2015-06-05)
changeset 603718a5cfdda1b98
parent 60370 9ec1d3d2068e
child 60372 b62eaac5c1af
added Isar command 'supply';
NEWS
src/Doc/Isar_Ref/Proof.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Fri Jun 05 13:26:12 2015 +0200
     1.2 +++ b/NEWS	Fri Jun 05 13:41:06 2015 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* New Isar command 'supply' supports fact definitions during goal
     1.8 +refinement ('apply' scripts).
     1.9 +
    1.10  * Configuration option rule_insts_schematic has been discontinued
    1.11  (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Fri Jun 05 13:26:12 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Fri Jun 05 13:41:06 2015 +0200
     2.3 @@ -860,6 +860,7 @@
     2.4    be used in scripts, too.
     2.5  
     2.6    \begin{matharray}{rcl}
     2.7 +    @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
     2.8      @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
     2.9      @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
    2.10      @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
    2.11 @@ -869,6 +870,8 @@
    2.12    \end{matharray}
    2.13  
    2.14    @{rail \<open>
    2.15 +    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    2.16 +    ;
    2.17      ( @@{command apply} | @@{command apply_end} ) @{syntax method}
    2.18      ;
    2.19      @@{command defer} @{syntax nat}?
    2.20 @@ -878,6 +881,10 @@
    2.21  
    2.22    \begin{description}
    2.23  
    2.24 +  \item @{command "supply"} supports fact definitions during goal
    2.25 +  refinement: it is similar to @{command "note"}, but it operates in
    2.26 +  backwards mode and does not have any impact on chained facts.
    2.27 +
    2.28    \item @{command "apply"}~@{text m} applies proof method @{text m} in
    2.29    initial position, but unlike @{command "proof"} it retains ``@{text
    2.30    "proof(prove)"}'' mode.  Thus consecutive method applications may be
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jun 05 13:26:12 2015 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jun 05 13:41:06 2015 +0200
     3.3 @@ -527,6 +527,10 @@
     3.4      (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
     3.5  
     3.6  val _ =
     3.7 +  Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)"
     3.8 +    (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
     3.9 +
    3.10 +val _ =
    3.11    Outer_Syntax.command @{command_keyword using} "augment goal facts"
    3.12      (facts >> (Toplevel.proof o Proof.using_cmd));
    3.13  
    3.14 @@ -647,11 +651,11 @@
    3.15      (Parse.nat >> (Toplevel.proof o Proof.prefer));
    3.16  
    3.17  val _ =
    3.18 -  Outer_Syntax.command @{command_keyword apply} "initial refinement step (unstructured)"
    3.19 +  Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
    3.20      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
    3.21  
    3.22  val _ =
    3.23 -  Outer_Syntax.command @{command_keyword apply_end} "terminal refinement step (unstructured)"
    3.24 +  Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
    3.25      (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
    3.26  
    3.27  val _ =
     4.1 --- a/src/Pure/Isar/proof.ML	Fri Jun 05 13:26:12 2015 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Fri Jun 05 13:41:06 2015 +0200
     4.3 @@ -67,6 +67,8 @@
     4.4    val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
     4.5    val with_thmss: ((thm list * attribute list) list) list -> state -> state
     4.6    val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
     4.7 +  val supply: (Thm.binding * (thm list * attribute list) list) list -> state -> state
     4.8 +  val supply_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
     4.9    val using: ((thm list * attribute list) list) list -> state -> state
    4.10    val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    4.11    val unfolding: ((thm list * attribute list) list) list -> state -> state
    4.12 @@ -706,6 +708,24 @@
    4.13  end;
    4.14  
    4.15  
    4.16 +(* facts during goal refinement *)
    4.17 +
    4.18 +local
    4.19 +
    4.20 +fun gen_supply prep_att prep_fact args state =
    4.21 +  state
    4.22 +  |> assert_backward
    4.23 +  |> map_context (fn ctxt => ctxt |> Proof_Context.note_thmss ""
    4.24 +       (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) args) |> snd);
    4.25 +
    4.26 +in
    4.27 +
    4.28 +val supply = gen_supply (K I) (K I);
    4.29 +val supply_cmd = gen_supply Attrib.attribute_cmd Proof_Context.get_fact;
    4.30 +
    4.31 +end;
    4.32 +
    4.33 +
    4.34  (* using/unfolding *)
    4.35  
    4.36  local
     5.1 --- a/src/Pure/Pure.thy	Fri Jun 05 13:26:12 2015 +0200
     5.2 +++ b/src/Pure/Pure.thy	Fri Jun 05 13:41:06 2015 +0200
     5.3 @@ -51,7 +51,9 @@
     5.4    and "show" :: prf_asm_goal % "proof"
     5.5    and "thus" :: prf_asm_goal % "proof" == "then show"
     5.6    and "then" "from" "with" :: prf_chain % "proof"
     5.7 -  and "note" "using" "unfolding" :: prf_decl % "proof"
     5.8 +  and "note" :: prf_decl % "proof"
     5.9 +  and "supply" :: prf_script % "proof"
    5.10 +  and "using" "unfolding" :: prf_decl % "proof"
    5.11    and "fix" "assume" "presume" "def" :: prf_asm % "proof"
    5.12    and "obtain" :: prf_asm_goal % "proof"
    5.13    and "guess" :: prf_asm_goal_script % "proof"