# HG changeset patch
# User wenzelm
# Date 1461703157 -7200
# Node ID 3f577308551e4210ae54090d8094fe17084d1f65
# Parent  8804faa80bc9745bb77847000c80d9ac786f6746
'obtain' supports structured statements (similar to 'define');

diff -r 8804faa80bc9 -r 3f577308551e NEWS
--- a/NEWS	Tue Apr 26 21:46:12 2016 +0200
+++ b/NEWS	Tue Apr 26 22:39:17 2016 +0200
@@ -64,6 +64,9 @@
 'definition' and 'obtain'. It fits better into the Isar language than
 old 'def', which is now a legacy feature.
 
+* Command 'obtain' supports structured statements with 'if' / 'for'
+context.
+
 * Command '\<proof>' is an alias for 'sorry', with different
 typesetting. E.g. to produce proof holes in examples and documentation.
 
diff -r 8804faa80bc9 -r 3f577308551e src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Tue Apr 26 21:46:12 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Tue Apr 26 22:39:17 2016 +0200
@@ -1322,8 +1322,12 @@
   @{rail \<open>
     @@{command consider} @{syntax obtain_clauses}
     ;
-    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
-      @'where' (@{syntax props} + @'and')
+    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>
+      @'where' concl prems @{syntax for_fixes}
+    ;
+    concl: (@{syntax props} + @'and')
+    ;
+    prems: (@'if' (@{syntax props'} + @'and'))?
     ;
     @@{command guess} (@{syntax "fixes"} + @'and')
   \<close>}
diff -r 8804faa80bc9 -r 3f577308551e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Apr 26 21:46:12 2016 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Apr 26 22:39:17 2016 +0200
@@ -15,8 +15,10 @@
   val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
   val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
   val obtain: binding -> (binding * typ option * mixfix) list ->
+    (binding * typ option * mixfix) list -> (term * term list) list list ->
     (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val obtain_cmd: binding -> (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list -> (string * string list) list list ->
     (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     ((string * cterm) list * thm list) * Proof.context
@@ -193,28 +195,32 @@
 
 local
 
-fun gen_obtain prep_stmt prep_att that_binding raw_vars raw_asms int state =
+fun gen_obtain prep_stmt prep_att that_binding raw_decls raw_fixes raw_prems raw_concls int state =
   let
     val _ = Proof.assert_forward_or_chain state;
 
     val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
+
     val ((vars, propss, binds, binds'), params_ctxt) =
-      prep_stmt raw_vars (map #2 raw_asms) thesis_ctxt;
-    val params = map #2 vars;
+      prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt;
+    val (decls, fixes) = chop (length raw_decls) vars ||> map #2;
+    val (premss, conclss) = chop (length raw_prems) propss;
+    val propss' = (map o map) (Logic.close_prop fixes (flat premss)) conclss;
+
     val that_prop =
-      Logic.list_rename_params (map #1 params)
-        (fold_rev Logic.all (map #2 params) (Logic.list_implies (flat propss, thesis)));
+      Logic.list_rename_params (map (#1 o #2) decls)
+        (fold_rev (Logic.all o #2 o #2) decls (Logic.list_implies (flat propss', thesis)));
 
-    val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) vars;
+    val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) decls;
     val asms =
-      map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~
-      map (map (rpair [])) propss;
+      map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_concls ~~
+      map (map (rpair [])) propss';
 
     fun after_qed (result_ctxt, results) state' =
       let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
         state'
-        |> Proof.fix (map #1 vars)
-        |> Proof.map_context (fold Variable.bind_term binds)
+        |> Proof.fix (map #1 decls)
+        |> Proof.map_context (fold (Variable.bind_term o apsnd (Logic.close_term fixes)) binds)
         |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
       end;
   in
diff -r 8804faa80bc9 -r 3f577308551e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Apr 26 21:46:12 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Apr 26 22:39:17 2016 +0200
@@ -758,8 +758,8 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
-    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
-      >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
+    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
+      >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
 
 val _ =
   Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"