# HG changeset patch
# User wenzelm
# Date 1433940391 -7200
# Node ID f25f2f2ba48c8f48946debe1f4c21cc72c35be91
# Parent  0824fd1e9c406c9539c2fb2e867f1b51618fdb88
support for "if prems" in local goal statements;

diff -r 0824fd1e9c40 -r f25f2f2ba48c NEWS
--- a/NEWS	Wed Jun 10 11:52:54 2015 +0200
+++ b/NEWS	Wed Jun 10 14:46:31 2015 +0200
@@ -15,8 +15,25 @@
 * Term abbreviations via 'is' patterns also work for schematic
 statements: result is abstracted over unknowns.
 
-* Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
-an optional context of local variables ('for' declaration).
+* 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:
+
+  have result: "C x y"
+    if "A x" and "B y"
+    for x :: 'a and y :: 'a
+    <proof>
+
+The local assumptions are always bound to the name "prems".  The result
+is exported from context of the statement as usual.  The above roughly
+corresponds to a raw proof block like this:
+
+  {
+    fix x :: 'a and y :: 'a
+    assume prems: "A x" "B y"
+    have "C x y" <proof>
+  }
+  note result = this
 
 * New command 'supply' supports fact definitions during goal refinement
 ('apply' scripts).
diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Jun 10 14:46:31 2015 +0200
@@ -435,13 +435,15 @@
      @@{command schematic_corollary}) (stmt | statement)
     ;
     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
-      stmt @{syntax for_fixes}
+      stmt if_prems @{syntax for_fixes}
     ;
     @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
     ;
   
     stmt: (@{syntax props} + @'and')
     ;
+    if_prems: (@'if' stmt)?
+    ;
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Wed Jun 10 14:46:31 2015 +0200
@@ -8,6 +8,7 @@
 sig
   val thesisN: string
   val thisN: string
+  val premsN: string
   val assmsN: string
   val abs_params: term -> term -> term
   val goal: Proof.context -> term list -> (indexname * term option) list
@@ -23,6 +24,7 @@
 val thesisN = "thesis";
 val thisN = "this";
 val assmsN = "assms";
+val premsN = "prems";
 
 fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
 
diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jun 10 14:46:31 2015 +0200
@@ -281,7 +281,7 @@
 fun proof_local cmd goal_ctxt int after_qed' propp =
   Proof.map_context (K goal_ctxt) #>
   Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
-    NONE after_qed' [] (map (pair Thm.empty_binding) propp);
+    NONE after_qed' [] [] (map (pair Thm.empty_binding) propp);
 
 in
 
diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 10 14:46:31 2015 +0200
@@ -464,6 +464,11 @@
 
 (** proof commands **)
 
+val _ =
+  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
+    (Parse.begin >> K Proof.begin_notepad);
+
+
 (* statements *)
 
 fun theorem spec schematic kind =
@@ -484,29 +489,29 @@
 val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK;
 val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK;
 
-val _ =
-  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
-    (Parse.begin >> K Proof.begin_notepad);
+
+val structured_statement =
+  Parse_Spec.statement -- Parse_Spec.if_prems -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
 
 val _ =
   Outer_Syntax.command @{command_keyword have} "state local goal"
-    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
-      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes stmt int)));
+    (structured_statement >> (fn (fixes, assumes, shows) =>
+      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes assumes shows int)));
 
 val _ =
   Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
-    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
-      Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) fixes stmt int)));
+    (structured_statement >> (fn (fixes, assumes, shows) =>
+      Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) fixes assumes shows int)));
 
 val _ =
   Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
-    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes stmt int)));
+    (structured_statement >> (fn (fixes, assumes, shows) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes assumes shows int)));
 
 val _ =
   Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
-    (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes stmt int)));
+    (structured_statement >> (fn (fixes, assumes, shows) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes assumes shows int)));
 
 
 (* facts *)
diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jun 10 14:46:31 2015 +0200
@@ -157,7 +157,7 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have NONE (K I) [] [(Thm.empty_binding, [(obtain_prop, [])])] int
+    |> Proof.have NONE (K I) [] [] [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.map_context (fold Variable.bind_term binds')
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
@@ -165,7 +165,7 @@
       [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show NONE after_qed [] [(Thm.empty_binding, [(thesis, [])])] false
+    ||> Proof.show NONE after_qed [] [] [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
@@ -317,7 +317,7 @@
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
-      (SOME before_qed) after_qed [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
+      (SOME before_qed) after_qed [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
     |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
         Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
   end;
diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Wed Jun 10 14:46:31 2015 +0200
@@ -24,6 +24,7 @@
   val locale_expression: bool -> Expression.expression parser
   val context_element: Element.context parser
   val statement: (Attrib.binding * (string * string list) list) list parser
+  val if_prems: (Attrib.binding * (string * string list) list) list parser
   val general_statement: (Element.context list * Element.statement) parser
   val statement_keyword: string parser
 end;
@@ -131,6 +132,8 @@
 
 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
 
+val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
+
 val obtain_case =
   Parse.parbinding --
     (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 10 14:46:31 2015 +0200
@@ -108,18 +108,23 @@
   val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
     Proof_Context.mode -> string -> Method.text option -> (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 -> state
   val have: Method.text option -> (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 -> state
   val have_cmd: Method.text option -> (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 -> state
   val show: Method.text option -> (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 -> state
   val show_cmd: Method.text option -> (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 -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
@@ -982,43 +987,56 @@
 in
 
 fun local_goal print_results prep_att prep_propp prep_var
-    kind before_qed after_qed fixes stmt state =
+    kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   let
-    val ((names, attss), propp) =
-      Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
+    val (assumes_bindings, shows_bindings) =
+      apply2 (map (apsnd (map (prep_att (context_of state))) o fst)) (raw_assumes, raw_shows);
+    val (assumes_propp, shows_propp) = apply2 (map snd) (raw_assumes, raw_shows);
 
     fun make_statement ctxt =
       let
+        (*fixed variables*)
         val ((xs', vars), fix_ctxt) = ctxt
-          |> fold_map prep_var fixes
+          |> fold_map prep_var raw_fixes
           |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
 
-        val (propss, binds) = prep_propp fix_ctxt propp;
-        val props = flat propss;
+        (*propositions with term bindings*)
+        val (all_propss, binds) = prep_propp fix_ctxt (assumes_propp @ shows_propp);
+        val (assumes_propss, shows_propss) = chop (length assumes_propp) all_propss;
 
-        val (ps, params_ctxt) = fix_ctxt
-          |> fold Variable.declare_term props
+        (*prems*)
+        val asms = assumes_bindings ~~ (map o map) (rpair []) assumes_propss;
+        fun note_prems ctxt' =
+          ctxt' |> not (null asms) ?
+            (snd o Proof_Context.note_thmss ""
+              [((Binding.name Auto_Bind.premsN, []), [(Assumption.local_prems_of ctxt' ctxt, [])])]);
+
+        (*params*)
+        val (ps, goal_ctxt) = fix_ctxt
+          |> (fold o fold) Variable.declare_term all_propss
+          |> Proof_Context.add_assms Assumption.assume_export asms |> snd
+          |> note_prems
           |> fold Variable.bind_term binds
           |> fold_map Proof_Context.inferred_param xs';
-
         val xs = map (Variable.check_name o #1) vars;
         val params = xs ~~ map Free ps;
 
+        val _ = Variable.warn_extra_tfrees fix_ctxt goal_ctxt;
+
+        (*result term bindings*)
+        val shows_props = flat shows_propss;
         val binds' =
-          (case try List.last props of
+          (case try List.last shows_props of
             NONE => []
           | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
         val result_binds =
-          (Auto_Bind.facts params_ctxt props @ binds')
+          (Auto_Bind.facts goal_ctxt shows_props @ binds')
           |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
-          |> export_binds params_ctxt ctxt;
-
-        val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
-
-      in ((propss, result_binds), params_ctxt) end;
+          |> export_binds goal_ctxt ctxt;
+      in ((shows_propss, result_binds), goal_ctxt) end;
 
     fun after_qed' results =
-      local_results ((names ~~ attss) ~~ results)
+      local_results (shows_bindings ~~ results)
       #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
       #> after_qed results;
   in generic_goal kind before_qed (after_qed', K I) make_statement state end;
@@ -1102,12 +1120,12 @@
 local
 
 fun gen_have prep_att prep_propp prep_var
-    before_qed after_qed fixes stmt int =
+    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 stmt;
+    prep_att prep_propp prep_var "have" before_qed after_qed fixes assumes shows;
 
 fun gen_show prep_att prep_propp prep_var
-    before_qed after_qed fixes stmt int state =
+    before_qed after_qed fixes assumes shows int state =
   let
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
@@ -1139,7 +1157,7 @@
   in
     state
     |> local_goal print_results prep_att prep_propp prep_var
-      "show" before_qed after_qed' fixes stmt
+      "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
         Exn.Res _ => goal_state