'obtain' supports structured statements (similar to 'define');
authorwenzelm
Tue Apr 26 22:39:17 2016 +0200 (2016-04-26 ago)
changeset 630593f577308551e
parent 63058 8804faa80bc9
child 63060 293ede07b775
'obtain' supports structured statements (similar to 'define');
NEWS
src/Doc/Isar_Ref/Proof.thy
src/Pure/Isar/obtain.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Tue Apr 26 21:46:12 2016 +0200
     1.2 +++ b/NEWS	Tue Apr 26 22:39:17 2016 +0200
     1.3 @@ -64,6 +64,9 @@
     1.4  'definition' and 'obtain'. It fits better into the Isar language than
     1.5  old 'def', which is now a legacy feature.
     1.6  
     1.7 +* Command 'obtain' supports structured statements with 'if' / 'for'
     1.8 +context.
     1.9 +
    1.10  * Command '\<proof>' is an alias for 'sorry', with different
    1.11  typesetting. E.g. to produce proof holes in examples and documentation.
    1.12  
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Tue Apr 26 21:46:12 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Tue Apr 26 22:39:17 2016 +0200
     2.3 @@ -1322,8 +1322,12 @@
     2.4    @{rail \<open>
     2.5      @@{command consider} @{syntax obtain_clauses}
     2.6      ;
     2.7 -    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
     2.8 -      @'where' (@{syntax props} + @'and')
     2.9 +    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>
    2.10 +      @'where' concl prems @{syntax for_fixes}
    2.11 +    ;
    2.12 +    concl: (@{syntax props} + @'and')
    2.13 +    ;
    2.14 +    prems: (@'if' (@{syntax props'} + @'and'))?
    2.15      ;
    2.16      @@{command guess} (@{syntax "fixes"} + @'and')
    2.17    \<close>}
     3.1 --- a/src/Pure/Isar/obtain.ML	Tue Apr 26 21:46:12 2016 +0200
     3.2 +++ b/src/Pure/Isar/obtain.ML	Tue Apr 26 22:39:17 2016 +0200
     3.3 @@ -15,8 +15,10 @@
     3.4    val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
     3.5    val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
     3.6    val obtain: binding -> (binding * typ option * mixfix) list ->
     3.7 +    (binding * typ option * mixfix) list -> (term * term list) list list ->
     3.8      (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
     3.9    val obtain_cmd: binding -> (binding * string option * mixfix) list ->
    3.10 +    (binding * string option * mixfix) list -> (string * string list) list list ->
    3.11      (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    3.12    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
    3.13      ((string * cterm) list * thm list) * Proof.context
    3.14 @@ -193,28 +195,32 @@
    3.15  
    3.16  local
    3.17  
    3.18 -fun gen_obtain prep_stmt prep_att that_binding raw_vars raw_asms int state =
    3.19 +fun gen_obtain prep_stmt prep_att that_binding raw_decls raw_fixes raw_prems raw_concls int state =
    3.20    let
    3.21      val _ = Proof.assert_forward_or_chain state;
    3.22  
    3.23      val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
    3.24 +
    3.25      val ((vars, propss, binds, binds'), params_ctxt) =
    3.26 -      prep_stmt raw_vars (map #2 raw_asms) thesis_ctxt;
    3.27 -    val params = map #2 vars;
    3.28 +      prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt;
    3.29 +    val (decls, fixes) = chop (length raw_decls) vars ||> map #2;
    3.30 +    val (premss, conclss) = chop (length raw_prems) propss;
    3.31 +    val propss' = (map o map) (Logic.close_prop fixes (flat premss)) conclss;
    3.32 +
    3.33      val that_prop =
    3.34 -      Logic.list_rename_params (map #1 params)
    3.35 -        (fold_rev Logic.all (map #2 params) (Logic.list_implies (flat propss, thesis)));
    3.36 +      Logic.list_rename_params (map (#1 o #2) decls)
    3.37 +        (fold_rev (Logic.all o #2 o #2) decls (Logic.list_implies (flat propss', thesis)));
    3.38  
    3.39 -    val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) vars;
    3.40 +    val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) decls;
    3.41      val asms =
    3.42 -      map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~
    3.43 -      map (map (rpair [])) propss;
    3.44 +      map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_concls ~~
    3.45 +      map (map (rpair [])) propss';
    3.46  
    3.47      fun after_qed (result_ctxt, results) state' =
    3.48        let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
    3.49          state'
    3.50 -        |> Proof.fix (map #1 vars)
    3.51 -        |> Proof.map_context (fold Variable.bind_term binds)
    3.52 +        |> Proof.fix (map #1 decls)
    3.53 +        |> Proof.map_context (fold (Variable.bind_term o apsnd (Logic.close_term fixes)) binds)
    3.54          |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
    3.55        end;
    3.56    in
     4.1 --- a/src/Pure/Pure.thy	Tue Apr 26 21:46:12 2016 +0200
     4.2 +++ b/src/Pure/Pure.thy	Tue Apr 26 22:39:17 2016 +0200
     4.3 @@ -758,8 +758,8 @@
     4.4  
     4.5  val _ =
     4.6    Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
     4.7 -    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
     4.8 -      >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
     4.9 +    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
    4.10 +      >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
    4.11  
    4.12  val _ =
    4.13    Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"