# HG changeset patch # User wenzelm # Date 1434998193 -7200 # Node ID 51a6997b13841c8675c09638de4dfafd8bdb0f60 # Parent c0e1c121c7c081c22d6a43c79cf839c37342258c support 'when' statement, which corresponds to 'presume'; diff -r c0e1c121c7c0 -r 51a6997b1384 NEWS --- 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). diff -r c0e1c121c7c0 -r 51a6997b1384 src/CCL/Term.thy --- 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\i" inr :: "i\i" - when :: "[i,i\i,i\i]\i" + "when" :: "[i,i\i,i\i]\i" split :: "[i,[i,i]\i]\i" fst :: "i\i" diff -r c0e1c121c7c0 -r 51a6997b1384 src/CTT/CTT.thy --- 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\i" inr :: "i\i" - when :: "[i, i\i, i\i]\i" + "when" :: "[i, i\i, i\i]\i" (*General Sum and Binary Product*) Sum :: "[t, i\t]\t" fst :: "i\i" diff -r c0e1c121c7c0 -r 51a6997b1384 src/Doc/Isar_Ref/Proof.thy --- 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} *) \ 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. \ diff -r c0e1c121c7c0 -r 51a6997b1384 src/FOLP/IFOLP.thy --- 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) diff -r c0e1c121c7c0 -r 51a6997b1384 src/HOL/Isar_Examples/Structured_Statements.thy --- 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 \Suffices-to-show\ + +notepad +begin + fix A B C + assume r: "A \ B \ 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 \ bool" + fix C + + have C + proof - + show ?thesis when "A x" (is ?A) for x :: 'a -- \abstract @{term x}\ + using that sorry + show "?A a" -- \concrete @{term a}\ + sorry + qed +end + +end diff -r c0e1c121c7c0 -r 51a6997b1384 src/Pure/Isar/element.ML --- 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; diff -r c0e1c121c7c0 -r 51a6997b1384 src/Pure/Isar/isar_syn.ML --- 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 *) diff -r c0e1c121c7c0 -r 51a6997b1384 src/Pure/Isar/obtain.ML --- 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 diff -r c0e1c121c7c0 -r 51a6997b1384 src/Pure/Isar/parse_spec.ML --- 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) [] -- diff -r c0e1c121c7c0 -r 51a6997b1384 src/Pure/Isar/proof.ML --- 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 diff -r c0e1c121c7c0 -r 51a6997b1384 src/Pure/Pure.thy --- 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 == ""