support 'when' statement, which corresponds to 'presume';

--- a/NEWS	Mon Jun 22 19:22:48 2015 +0200
+++ b/NEWS	Mon Jun 22 20:36:33 2015 +0200
@@ -20,7 +20,8 @@
 
 * Local goals ('have', 'show', 'hence', 'thus') allow structured
 statements like fixes/assumes/shows in theorem specifications, but the
-notation is postfix with keywords 'if' and 'for'. For example:
+notation is postfix with keywords 'if' (or 'when') and 'for'. For
+example:
 
   have result: "C x y"
     if "A x" and "B y"
@@ -38,6 +39,9 @@
   }
   note result = this
 
+The keyword 'when' may be used instead of 'if', to indicate 'presume'
+instead of 'assume' above.
+
 * New command 'supply' supports fact definitions during goal refinement
 ('apply' scripts).
 

--- a/src/CCL/Term.thy	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/CCL/Term.thy	Mon Jun 22 20:36:33 2015 +0200
@@ -17,7 +17,7 @@
 
   inl        :: "i\<Rightarrow>i"
   inr        :: "i\<Rightarrow>i"
-  when       :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+  "when"     :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
 
   split      :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   fst        :: "i\<Rightarrow>i"

--- a/src/CTT/CTT.thy	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/CTT/CTT.thy	Mon Jun 22 20:36:33 2015 +0200
@@ -29,7 +29,7 @@
   (*Unions*)
   inl       :: "i\<Rightarrow>i"
   inr       :: "i\<Rightarrow>i"
-  when      :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
+  "when"    :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
   (*General Sum and Binary Product*)
   Sum       :: "[t, i\<Rightarrow>t]\<Rightarrow>t"
   fst       :: "i\<Rightarrow>i"

--- a/src/Doc/Isar_Ref/Proof.thy	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Mon Jun 22 20:36:33 2015 +0200
@@ -427,13 +427,15 @@
      @@{command schematic_corollary}) (stmt | statement)
     ;
     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
-      stmt (@'if' stmt)? @{syntax for_fixes}
+      stmt cond_stmt @{syntax for_fixes}
     ;
     @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
     ;
 
     stmt: (@{syntax props} + @'and')
     ;
+    cond_stmt: ((@'if' | @'when') stmt)?
+    ;
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
@@ -516,10 +518,10 @@
   @{variable_ref "?thesis"}) to be bound automatically, see also
   \secref{sec:term-abbrev}.
 
-  Structured goal statements involving @{keyword_ref "if"} define the
-  special fact @{fact_ref that} to refer to these assumptions in the proof
-  body. The user may provide separate names according to the syntax of the
-  statement.
+  Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref
+  "when"} define the special fact @{fact_ref that} to refer to these
+  assumptions in the proof body. The user may provide separate names
+  according to the syntax of the statement.
 \<close>
 
 

--- a/src/FOLP/IFOLP.thy	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/FOLP/IFOLP.thy	Mon Jun 22 20:36:33 2015 +0200
@@ -50,7 +50,7 @@
  split          :: "[p, [p,p]=>p] =>p"
  inl            :: "p=>p"
  inr            :: "p=>p"
- when           :: "[p, p=>p, p=>p]=>p"
+ "when"         :: "[p, p=>p, p=>p]=>p"
  lambda         :: "(p => p) => p"      (binder "lam " 55)
  App            :: "[p,p]=>p"           (infixl "`" 60)
  alll           :: "['a=>p]=>p"         (binder "all " 55)

--- a/src/HOL/Isar_Examples/Structured_Statements.thy	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Mon Jun 22 20:36:33 2015 +0200
@@ -130,4 +130,33 @@
   qed
 end
 
-end
\ No newline at end of file
+
+subsection \<open>Suffices-to-show\<close>
+
+notepad
+begin
+  fix A B C
+  assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
+
+  have C
+  proof -
+    show ?thesis when A (is ?A) and B (is ?B)
+      using that by (rule r)
+    show ?A sorry
+    show ?B sorry
+  qed
+next
+  fix a :: 'a
+  fix A :: "'a \<Rightarrow> bool"
+  fix C
+
+  have C
+  proof -
+    show ?thesis when "A x" (is ?A) for x :: 'a  -- \<open>abstract @{term x}\<close>
+      using that sorry
+    show "?A a"  -- \<open>concrete @{term a}\<close>
+      sorry
+  qed
+end
+
+end

--- a/src/Pure/Isar/element.ML	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Pure/Isar/element.ML	Mon Jun 22 20:36:33 2015 +0200
@@ -291,7 +291,7 @@
       after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state';
   in
     Proof.map_context (K goal_ctxt) #>
-    Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
+    Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) true cmd
       NONE after_qed' [] [] (map (pair Thm.empty_binding) propp) #> snd
   end;
 

--- a/src/Pure/Isar/isar_syn.ML	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 22 20:36:33 2015 +0200
@@ -491,28 +491,28 @@
 
 
 val structured_statement =
-  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
-    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
+  Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
+    >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
 
 val _ =
   Outer_Syntax.command @{command_keyword have} "state local goal"
-    (structured_statement >> (fn (a, b, c) =>
-      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) a b c int #> #2)));
+    (structured_statement >> (fn (a, b, c, d) =>
+      Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
 
 val _ =
   Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
-    (structured_statement >> (fn (a, b, c) =>
-      Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) a b c int #> #2)));
+    (structured_statement >> (fn (a, b, c, d) =>
+      Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
 
 val _ =
   Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
-    (structured_statement >> (fn (a, b, c) =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) a b c int #> #2)));
+    (structured_statement >> (fn (a, b, c, d) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
 
 val _ =
   Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
-    (structured_statement >> (fn (a, b, c) =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) a b c int #> #2)));
+    (structured_statement >> (fn (a, b, c, d) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
 
 
 (* facts *)

--- a/src/Pure/Isar/obtain.ML	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 22 20:36:33 2015 +0200
@@ -159,7 +159,7 @@
     val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains;
   in
     state
-    |> Proof.have NONE (K I)
+    |> Proof.have true NONE (K I)
       [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
       (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
       [((Binding.empty, atts), [(thesis, [])])] int
@@ -233,7 +233,7 @@
       end;
   in
     state
-    |> Proof.have NONE after_qed
+    |> Proof.have true NONE after_qed
       [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
       [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
       [(Thm.empty_binding, [(thesis, [])])] int
@@ -409,7 +409,7 @@
     |> Proof.begin_block
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
-    |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+    |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess"
       (SOME before_qed) after_qed
       [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
     |> snd

--- a/src/Pure/Isar/parse_spec.ML	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Mon Jun 22 20:36:33 2015 +0200
@@ -25,6 +25,7 @@
   val context_element: Element.context parser
   val statement: (Attrib.binding * (string * string list) list) list parser
   val if_statement: (Attrib.binding * (string * string list) list) list parser
+  val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser
   val obtains: Element.obtains parser
   val general_statement: (Element.context list * Element.statement) parser
   val statement_keyword: string parser
@@ -134,6 +135,11 @@
 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
 val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
 
+val cond_statement =
+  Parse.$$$ "if" |-- Parse.!!! statement >> pair true ||
+  Parse.$$$ "when" |-- Parse.!!! statement >> pair false ||
+  Scan.succeed (true, []);
+
 val obtain_case =
   Parse.parbinding --
     (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --

--- a/src/Pure/Isar/proof.ML	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jun 22 20:36:33 2015 +0200
@@ -105,24 +105,24 @@
   val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
   val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
-    Proof_Context.mode -> string -> Method.text option ->
+    Proof_Context.mode -> bool -> string -> Method.text option ->
     (context * thm list list -> state -> state) ->
     (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list ->
     (Thm.binding * (term * term list) list) list -> state -> thm list * state
-  val have: Method.text option -> (context * thm list list -> state -> state) ->
+  val have: bool -> Method.text option -> (context * thm list list -> state -> state) ->
     (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list ->
     (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
-  val have_cmd: Method.text option -> (context * thm list list -> state -> state) ->
+  val have_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
-  val show: Method.text option -> (context * thm list list -> state -> state) ->
+  val show: bool -> Method.text option -> (context * thm list list -> state -> state) ->
     (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list ->
     (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
-  val show_cmd: Method.text option -> (context * thm list list -> state -> state) ->
+  val show_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
@@ -982,11 +982,14 @@
 
 in
 
-fun local_goal print_results prep_att prep_propp prep_var
+fun local_goal print_results prep_att prep_propp prep_var strict_asm
     kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   let
     val ctxt = context_of state;
 
+    val add_assumes =
+      Assumption.add_assms
+        (if strict_asm then Assumption.assume_export else Assumption.presume_export);
     val (assumes_bindings, shows_bindings) =
       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
     val (assumes_propp, shows_propp) = apply2 (map snd) (raw_assumes, raw_shows);
@@ -1012,8 +1015,7 @@
 
         (*prems*)
         val (that_fact, goal_ctxt) = params_ctxt
-          |> fold_burrow (Assumption.add_assms Assumption.assume_export)
-              ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
+          |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
           |> (fn (premss, ctxt') =>
               let
                 val prems = Assumption.local_prems_of ctxt' ctxt;
@@ -1132,12 +1134,12 @@
 local
 
 fun gen_have prep_att prep_propp prep_var
-    before_qed after_qed fixes assumes shows int =
+    strict_asm before_qed after_qed fixes assumes shows int =
   local_goal (Proof_Display.print_results int (Position.thread_data ()))
-    prep_att prep_propp prep_var "have" before_qed after_qed fixes assumes shows;
+    prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
 
 fun gen_show prep_att prep_propp prep_var
-    before_qed after_qed fixes assumes shows int state =
+    strict_asm before_qed after_qed fixes assumes shows int state =
   let
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
@@ -1168,7 +1170,7 @@
       |> after_qed (result_ctxt, results);
   in
     state
-    |> local_goal print_results prep_att prep_propp prep_var
+    |> local_goal print_results prep_att prep_propp prep_var strict_asm
       "show" before_qed after_qed' fixes assumes shows
     ||> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of

--- a/src/Pure/Pure.thy	Mon Jun 22 19:22:48 2015 +0200
+++ b/src/Pure/Pure.thy	Mon Jun 22 20:36:33 2015 +0200
@@ -12,7 +12,7 @@
     "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "private" "qualified" "shows"
-    "structure" "unchecked" "where" "|"
+    "structure" "unchecked" "where" "when" "|"
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""