support 'when' statement, which corresponds to 'presume';
authorwenzelm
Mon Jun 22 20:36:33 2015 +0200 (2015-06-22)
changeset 6055551a6997b1384
parent 60554 c0e1c121c7c0
child 60556 e7003c8041e2
support 'when' statement, which corresponds to 'presume';
NEWS
src/CCL/Term.thy
src/CTT/CTT.thy
src/Doc/Isar_Ref/Proof.thy
src/FOLP/IFOLP.thy
src/HOL/Isar_Examples/Structured_Statements.thy
src/Pure/Isar/element.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/proof.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Mon Jun 22 19:22:48 2015 +0200
     1.2 +++ b/NEWS	Mon Jun 22 20:36:33 2015 +0200
     1.3 @@ -20,7 +20,8 @@
     1.4  
     1.5  * Local goals ('have', 'show', 'hence', 'thus') allow structured
     1.6  statements like fixes/assumes/shows in theorem specifications, but the
     1.7 -notation is postfix with keywords 'if' and 'for'. For example:
     1.8 +notation is postfix with keywords 'if' (or 'when') and 'for'. For
     1.9 +example:
    1.10  
    1.11    have result: "C x y"
    1.12      if "A x" and "B y"
    1.13 @@ -38,6 +39,9 @@
    1.14    }
    1.15    note result = this
    1.16  
    1.17 +The keyword 'when' may be used instead of 'if', to indicate 'presume'
    1.18 +instead of 'assume' above.
    1.19 +
    1.20  * New command 'supply' supports fact definitions during goal refinement
    1.21  ('apply' scripts).
    1.22  
     2.1 --- a/src/CCL/Term.thy	Mon Jun 22 19:22:48 2015 +0200
     2.2 +++ b/src/CCL/Term.thy	Mon Jun 22 20:36:33 2015 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  
     2.5    inl        :: "i\<Rightarrow>i"
     2.6    inr        :: "i\<Rightarrow>i"
     2.7 -  when       :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
     2.8 +  "when"     :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
     2.9  
    2.10    split      :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
    2.11    fst        :: "i\<Rightarrow>i"
     3.1 --- a/src/CTT/CTT.thy	Mon Jun 22 19:22:48 2015 +0200
     3.2 +++ b/src/CTT/CTT.thy	Mon Jun 22 20:36:33 2015 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4    (*Unions*)
     3.5    inl       :: "i\<Rightarrow>i"
     3.6    inr       :: "i\<Rightarrow>i"
     3.7 -  when      :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
     3.8 +  "when"    :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
     3.9    (*General Sum and Binary Product*)
    3.10    Sum       :: "[t, i\<Rightarrow>t]\<Rightarrow>t"
    3.11    fst       :: "i\<Rightarrow>i"
     4.1 --- a/src/Doc/Isar_Ref/Proof.thy	Mon Jun 22 19:22:48 2015 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Mon Jun 22 20:36:33 2015 +0200
     4.3 @@ -427,13 +427,15 @@
     4.4       @@{command schematic_corollary}) (stmt | statement)
     4.5      ;
     4.6      (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
     4.7 -      stmt (@'if' stmt)? @{syntax for_fixes}
     4.8 +      stmt cond_stmt @{syntax for_fixes}
     4.9      ;
    4.10      @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
    4.11      ;
    4.12  
    4.13      stmt: (@{syntax props} + @'and')
    4.14      ;
    4.15 +    cond_stmt: ((@'if' | @'when') stmt)?
    4.16 +    ;
    4.17      statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
    4.18        conclusion
    4.19      ;
    4.20 @@ -516,10 +518,10 @@
    4.21    @{variable_ref "?thesis"}) to be bound automatically, see also
    4.22    \secref{sec:term-abbrev}.
    4.23  
    4.24 -  Structured goal statements involving @{keyword_ref "if"} define the
    4.25 -  special fact @{fact_ref that} to refer to these assumptions in the proof
    4.26 -  body. The user may provide separate names according to the syntax of the
    4.27 -  statement.
    4.28 +  Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref
    4.29 +  "when"} define the special fact @{fact_ref that} to refer to these
    4.30 +  assumptions in the proof body. The user may provide separate names
    4.31 +  according to the syntax of the statement.
    4.32  \<close>
    4.33  
    4.34  
     5.1 --- a/src/FOLP/IFOLP.thy	Mon Jun 22 19:22:48 2015 +0200
     5.2 +++ b/src/FOLP/IFOLP.thy	Mon Jun 22 20:36:33 2015 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4   split          :: "[p, [p,p]=>p] =>p"
     5.5   inl            :: "p=>p"
     5.6   inr            :: "p=>p"
     5.7 - when           :: "[p, p=>p, p=>p]=>p"
     5.8 + "when"         :: "[p, p=>p, p=>p]=>p"
     5.9   lambda         :: "(p => p) => p"      (binder "lam " 55)
    5.10   App            :: "[p,p]=>p"           (infixl "`" 60)
    5.11   alll           :: "['a=>p]=>p"         (binder "all " 55)
     6.1 --- a/src/HOL/Isar_Examples/Structured_Statements.thy	Mon Jun 22 19:22:48 2015 +0200
     6.2 +++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Mon Jun 22 20:36:33 2015 +0200
     6.3 @@ -130,4 +130,33 @@
     6.4    qed
     6.5  end
     6.6  
     6.7 -end
     6.8 \ No newline at end of file
     6.9 +
    6.10 +subsection \<open>Suffices-to-show\<close>
    6.11 +
    6.12 +notepad
    6.13 +begin
    6.14 +  fix A B C
    6.15 +  assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
    6.16 +
    6.17 +  have C
    6.18 +  proof -
    6.19 +    show ?thesis when A (is ?A) and B (is ?B)
    6.20 +      using that by (rule r)
    6.21 +    show ?A sorry
    6.22 +    show ?B sorry
    6.23 +  qed
    6.24 +next
    6.25 +  fix a :: 'a
    6.26 +  fix A :: "'a \<Rightarrow> bool"
    6.27 +  fix C
    6.28 +
    6.29 +  have C
    6.30 +  proof -
    6.31 +    show ?thesis when "A x" (is ?A) for x :: 'a  -- \<open>abstract @{term x}\<close>
    6.32 +      using that sorry
    6.33 +    show "?A a"  -- \<open>concrete @{term a}\<close>
    6.34 +      sorry
    6.35 +  qed
    6.36 +end
    6.37 +
    6.38 +end
     7.1 --- a/src/Pure/Isar/element.ML	Mon Jun 22 19:22:48 2015 +0200
     7.2 +++ b/src/Pure/Isar/element.ML	Mon Jun 22 20:36:33 2015 +0200
     7.3 @@ -291,7 +291,7 @@
     7.4        after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state';
     7.5    in
     7.6      Proof.map_context (K goal_ctxt) #>
     7.7 -    Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
     7.8 +    Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) true cmd
     7.9        NONE after_qed' [] [] (map (pair Thm.empty_binding) propp) #> snd
    7.10    end;
    7.11  
     8.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Jun 22 19:22:48 2015 +0200
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 22 20:36:33 2015 +0200
     8.3 @@ -491,28 +491,28 @@
     8.4  
     8.5  
     8.6  val structured_statement =
     8.7 -  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
     8.8 -    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
     8.9 +  Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
    8.10 +    >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
    8.11  
    8.12  val _ =
    8.13    Outer_Syntax.command @{command_keyword have} "state local goal"
    8.14 -    (structured_statement >> (fn (a, b, c) =>
    8.15 -      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) a b c int #> #2)));
    8.16 +    (structured_statement >> (fn (a, b, c, d) =>
    8.17 +      Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
    8.18  
    8.19  val _ =
    8.20    Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
    8.21 -    (structured_statement >> (fn (a, b, c) =>
    8.22 -      Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) a b c int #> #2)));
    8.23 +    (structured_statement >> (fn (a, b, c, d) =>
    8.24 +      Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
    8.25  
    8.26  val _ =
    8.27    Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
    8.28 -    (structured_statement >> (fn (a, b, c) =>
    8.29 -      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) a b c int #> #2)));
    8.30 +    (structured_statement >> (fn (a, b, c, d) =>
    8.31 +      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
    8.32  
    8.33  val _ =
    8.34    Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
    8.35 -    (structured_statement >> (fn (a, b, c) =>
    8.36 -      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) a b c int #> #2)));
    8.37 +    (structured_statement >> (fn (a, b, c, d) =>
    8.38 +      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
    8.39  
    8.40  
    8.41  (* facts *)
     9.1 --- a/src/Pure/Isar/obtain.ML	Mon Jun 22 19:22:48 2015 +0200
     9.2 +++ b/src/Pure/Isar/obtain.ML	Mon Jun 22 20:36:33 2015 +0200
     9.3 @@ -159,7 +159,7 @@
     9.4      val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains;
     9.5    in
     9.6      state
     9.7 -    |> Proof.have NONE (K I)
     9.8 +    |> Proof.have true NONE (K I)
     9.9        [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
    9.10        (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
    9.11        [((Binding.empty, atts), [(thesis, [])])] int
    9.12 @@ -233,7 +233,7 @@
    9.13        end;
    9.14    in
    9.15      state
    9.16 -    |> Proof.have NONE after_qed
    9.17 +    |> Proof.have true NONE after_qed
    9.18        [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
    9.19        [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
    9.20        [(Thm.empty_binding, [(thesis, [])])] int
    9.21 @@ -409,7 +409,7 @@
    9.22      |> Proof.begin_block
    9.23      |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
    9.24      |> Proof.chain_facts chain_facts
    9.25 -    |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
    9.26 +    |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess"
    9.27        (SOME before_qed) after_qed
    9.28        [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
    9.29      |> snd
    10.1 --- a/src/Pure/Isar/parse_spec.ML	Mon Jun 22 19:22:48 2015 +0200
    10.2 +++ b/src/Pure/Isar/parse_spec.ML	Mon Jun 22 20:36:33 2015 +0200
    10.3 @@ -25,6 +25,7 @@
    10.4    val context_element: Element.context parser
    10.5    val statement: (Attrib.binding * (string * string list) list) list parser
    10.6    val if_statement: (Attrib.binding * (string * string list) list) list parser
    10.7 +  val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser
    10.8    val obtains: Element.obtains parser
    10.9    val general_statement: (Element.context list * Element.statement) parser
   10.10    val statement_keyword: string parser
   10.11 @@ -134,6 +135,11 @@
   10.12  val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   10.13  val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
   10.14  
   10.15 +val cond_statement =
   10.16 +  Parse.$$$ "if" |-- Parse.!!! statement >> pair true ||
   10.17 +  Parse.$$$ "when" |-- Parse.!!! statement >> pair false ||
   10.18 +  Scan.succeed (true, []);
   10.19 +
   10.20  val obtain_case =
   10.21    Parse.parbinding --
   10.22      (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
    11.1 --- a/src/Pure/Isar/proof.ML	Mon Jun 22 19:22:48 2015 +0200
    11.2 +++ b/src/Pure/Isar/proof.ML	Mon Jun 22 20:36:33 2015 +0200
    11.3 @@ -105,24 +105,24 @@
    11.4    val global_skip_proof: bool -> state -> context
    11.5    val global_done_proof: state -> context
    11.6    val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
    11.7 -    Proof_Context.mode -> string -> Method.text option ->
    11.8 +    Proof_Context.mode -> bool -> string -> Method.text option ->
    11.9      (context * thm list list -> state -> state) ->
   11.10      (binding * typ option * mixfix) list ->
   11.11      (Thm.binding * (term * term list) list) list ->
   11.12      (Thm.binding * (term * term list) list) list -> state -> thm list * state
   11.13 -  val have: Method.text option -> (context * thm list list -> state -> state) ->
   11.14 +  val have: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   11.15      (binding * typ option * mixfix) list ->
   11.16      (Thm.binding * (term * term list) list) list ->
   11.17      (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
   11.18 -  val have_cmd: Method.text option -> (context * thm list list -> state -> state) ->
   11.19 +  val have_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   11.20      (binding * string option * mixfix) list ->
   11.21      (Attrib.binding * (string * string list) list) list ->
   11.22      (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
   11.23 -  val show: Method.text option -> (context * thm list list -> state -> state) ->
   11.24 +  val show: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   11.25      (binding * typ option * mixfix) list ->
   11.26      (Thm.binding * (term * term list) list) list ->
   11.27      (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
   11.28 -  val show_cmd: Method.text option -> (context * thm list list -> state -> state) ->
   11.29 +  val show_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
   11.30      (binding * string option * mixfix) list ->
   11.31      (Attrib.binding * (string * string list) list) list ->
   11.32      (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
   11.33 @@ -982,11 +982,14 @@
   11.34  
   11.35  in
   11.36  
   11.37 -fun local_goal print_results prep_att prep_propp prep_var
   11.38 +fun local_goal print_results prep_att prep_propp prep_var strict_asm
   11.39      kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   11.40    let
   11.41      val ctxt = context_of state;
   11.42  
   11.43 +    val add_assumes =
   11.44 +      Assumption.add_assms
   11.45 +        (if strict_asm then Assumption.assume_export else Assumption.presume_export);
   11.46      val (assumes_bindings, shows_bindings) =
   11.47        apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
   11.48      val (assumes_propp, shows_propp) = apply2 (map snd) (raw_assumes, raw_shows);
   11.49 @@ -1012,8 +1015,7 @@
   11.50  
   11.51          (*prems*)
   11.52          val (that_fact, goal_ctxt) = params_ctxt
   11.53 -          |> fold_burrow (Assumption.add_assms Assumption.assume_export)
   11.54 -              ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
   11.55 +          |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
   11.56            |> (fn (premss, ctxt') =>
   11.57                let
   11.58                  val prems = Assumption.local_prems_of ctxt' ctxt;
   11.59 @@ -1132,12 +1134,12 @@
   11.60  local
   11.61  
   11.62  fun gen_have prep_att prep_propp prep_var
   11.63 -    before_qed after_qed fixes assumes shows int =
   11.64 +    strict_asm before_qed after_qed fixes assumes shows int =
   11.65    local_goal (Proof_Display.print_results int (Position.thread_data ()))
   11.66 -    prep_att prep_propp prep_var "have" before_qed after_qed fixes assumes shows;
   11.67 +    prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
   11.68  
   11.69  fun gen_show prep_att prep_propp prep_var
   11.70 -    before_qed after_qed fixes assumes shows int state =
   11.71 +    strict_asm before_qed after_qed fixes assumes shows int state =
   11.72    let
   11.73      val testing = Unsynchronized.ref false;
   11.74      val rule = Unsynchronized.ref (NONE: thm option);
   11.75 @@ -1168,7 +1170,7 @@
   11.76        |> after_qed (result_ctxt, results);
   11.77    in
   11.78      state
   11.79 -    |> local_goal print_results prep_att prep_propp prep_var
   11.80 +    |> local_goal print_results prep_att prep_propp prep_var strict_asm
   11.81        "show" before_qed after_qed' fixes assumes shows
   11.82      ||> int ? (fn goal_state =>
   11.83        (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
    12.1 --- a/src/Pure/Pure.thy	Mon Jun 22 19:22:48 2015 +0200
    12.2 +++ b/src/Pure/Pure.thy	Mon Jun 22 20:36:33 2015 +0200
    12.3 @@ -12,7 +12,7 @@
    12.4      "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    12.5      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
    12.6      "overloaded" "pervasive" "private" "qualified" "shows"
    12.7 -    "structure" "unchecked" "where" "|"
    12.8 +    "structure" "unchecked" "where" "when" "|"
    12.9    and "text" "txt" :: document_body
   12.10    and "text_raw" :: document_raw
   12.11    and "default_sort" :: thy_decl == ""