--- 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).
--- 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
;
--- 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;
--- 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
--- 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 *)
--- 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;
--- 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) [] --
--- 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