--- a/NEWS Tue Jun 09 15:28:06 2015 +0200
+++ b/NEWS Tue Jun 09 16:07:11 2015 +0200
@@ -7,14 +7,20 @@
New in this Isabelle version
----------------------------
+*** Isar ***
+
+* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
+proof body as well, abstracted over relevant parameters.
+
+* Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
+an optional context of local variables ('for' declaration).
+
+* New command 'supply' supports fact definitions during goal refinement
+('apply' scripts).
+
+
*** Pure ***
-* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
-the proof body as well, abstracted over relevant parameters.
-
-* New Isar command 'supply' supports fact definitions during goal
-refinement ('apply' scripts).
-
* Configuration option rule_insts_schematic has been discontinued
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
--- a/src/Doc/Isar_Ref/Proof.thy Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Tue Jun 09 16:07:11 2015 +0200
@@ -432,19 +432,20 @@
@{rail \<open>
(@@{command lemma} | @@{command theorem} | @@{command corollary} |
@@{command schematic_lemma} | @@{command schematic_theorem} |
- @@{command schematic_corollary}) (goal | statement)
+ @@{command schematic_corollary}) (stmt | statement)
;
- (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
+ (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
+ stmt @{syntax for_fixes}
;
@@{command print_statement} @{syntax modes}? @{syntax thmrefs}
;
- goal: (@{syntax props} + @'and')
+ stmt: (@{syntax props} + @'and')
;
statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
conclusion
;
- conclusion: @'shows' goal | @'obtains' (@{syntax par_name}? obtain_case + '|')
+ conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')
;
obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
\<close>}
--- a/src/Pure/Isar/element.ML Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/element.ML Tue Jun 09 16:07:11 2015 +0200
@@ -280,8 +280,8 @@
fun proof_local cmd goal_ctxt int after_qed' propp =
Proof.map_context (K goal_ctxt) #>
- Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE
- after_qed' (map (pair Thm.empty_binding) propp);
+ Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
+ NONE after_qed' [] (map (pair Thm.empty_binding) propp);
in
--- a/src/Pure/Isar/isar_syn.ML Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jun 09 16:07:11 2015 +0200
@@ -490,22 +490,23 @@
val _ =
Outer_Syntax.command @{command_keyword have} "state local goal"
- (Parse_Spec.statement >> (Toplevel.proof' o Proof.have_cmd NONE (K I)));
+ (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
+ Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes stmt 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)));
val _ =
Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
- (Parse_Spec.statement >> (fn stmt =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) stmt int)));
-
-val _ =
- Outer_Syntax.command @{command_keyword show}
- "state local goal, solving current obligation"
- (Parse_Spec.statement >> (Toplevel.proof' o Proof.show_cmd NONE (K I)));
+ (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes stmt int)));
val _ =
Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\""
- (Parse_Spec.statement >> (fn stmt =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) stmt int)));
+ (Parse_Spec.statement -- Parse.for_fixes >> (fn (stmt, fixes) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes stmt int)));
(* facts *)
--- a/src/Pure/Isar/obtain.ML Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Tue Jun 09 16:07:11 2015 +0200
@@ -155,7 +155,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)]
@@ -163,7 +163,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;
@@ -314,8 +314,8 @@
|> Proof.begin_block
|> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
- |> Proof.local_goal print_result (K I) (K (rpair []))
- "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
+ |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+ (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/proof.ML Tue Jun 09 15:28:06 2015 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jun 09 16:07:11 2015 +0200
@@ -89,11 +89,6 @@
val apply_end: Method.text -> state -> state Seq.seq
val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
- val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
- (context -> 'a -> attribute) ->
- (context -> 'b list -> (term list list * (indexname * term) list)) ->
- string -> Method.text option -> (thm list list -> state -> state) ->
- ((binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text_range option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
(term * term list) list list -> context -> state
@@ -110,13 +105,21 @@
val global_immediate_proof: state -> context
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 -> (thm list list -> state -> state) ->
+ (binding * typ option * mixfix) 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 -> 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 -> 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 -> 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 -> bool -> state -> state
val schematic_goal: state -> bool
val is_relevant: state -> bool
@@ -888,6 +891,10 @@
local
+fun export_binds ctxt' ctxt params binds =
+ let val ts = map (fold_rev Term.dependent_lambda_name params o snd) binds;
+ in map fst binds ~~ Variable.export_terms ctxt' ctxt ts end;
+
val is_var =
can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
can (dest_Var o Logic.dest_term);
@@ -907,33 +914,33 @@
in
-fun generic_goal kind before_qed after_qed make_propp state =
+fun generic_goal kind before_qed after_qed make_statement state =
let
val ctxt = context_of state;
val chaining = can assert_chain state;
val pos = Position.thread_data ();
- val ((propss, binds), goal_state) =
+ val ((propss, params, binds), goal_state) =
state
|> assert_forward_or_chain
|> enter_forward
|> open_block
- |> map_context_result make_propp;
+ |> map_context_result make_statement;
val props = flat propss;
val goal_ctxt = context_of goal_state;
+ val result_binds = export_binds goal_ctxt ctxt params binds;
val vars = implicit_vars props;
val propss' = vars :: propss;
val goal_propss = filter_out null propss';
val goal =
Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
- |> Thm.cterm_of ctxt
+ |> Thm.cterm_of goal_ctxt
|> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
val statement = ((kind, pos), propss', Thm.term_of goal);
- val binds' = map #1 binds ~~ Variable.export_terms goal_ctxt ctxt (map #2 binds);
val after_qed' = after_qed |>> (fn after_local => fn results =>
- map_context (fold Variable.bind_term binds') #> after_local results);
+ map_context (fold Variable.bind_term result_binds) #> after_local results);
in
goal_state
|> map_context (init_context #> Variable.set_body true)
@@ -971,28 +978,35 @@
(* local goals *)
-fun local_goal print_results prep_att prep_propp kind before_qed after_qed stmt state =
+fun local_goal print_results prep_att prep_propp prep_var
+ kind before_qed after_qed fixes stmt state =
let
val ((names, attss), propp) =
Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
- fun make_propp ctxt' =
+ fun make_statement ctxt =
let
- val (propss, binds) = prep_propp ctxt' propp;
- val ctxt'' = ctxt'
+ val ((xs', vars), fix_ctxt) = ctxt
+ |> fold_map prep_var fixes
+ |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
+
+ val (propss, binds) = prep_propp fix_ctxt propp;
+ val (Ts, params_ctxt) = fix_ctxt
|> (fold o fold) Variable.declare_term propss
- |> Proof_Context.bind_terms binds;
- in ((propss, binds), ctxt'') end;
+ |> Proof_Context.bind_terms binds
+ |> fold_map Proof_Context.inferred_param xs';
+
+ val xs = map (Variable.check_name o #1) vars;
+ val params = xs ~~ map Free (xs' ~~ Ts);
+
+ val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
+ in ((propss, params, binds), params_ctxt) end;
fun after_qed' results =
local_results ((names ~~ attss) ~~ results)
#-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
#> after_qed results;
- in
- state
- |> generic_goal kind before_qed (after_qed', K I) make_propp
- |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
- end;
+ in generic_goal kind before_qed (after_qed', K I) make_statement state end;
fun local_qeds arg =
end_proof false arg
@@ -1007,15 +1021,15 @@
fun global_goal prep_propp before_qed after_qed propp =
let
- fun make_propp ctxt' =
+ fun make_statement ctxt =
let
val (propss, binds) =
- prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') propp;
- val ctxt'' = ctxt'
+ prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
+ val ctxt' = ctxt
|> (fold o fold) Variable.auto_fixes propss
|> Proof_Context.bind_terms binds;
- in ((propss, binds), ctxt'') end;
- in init #> generic_goal "" before_qed (K I, after_qed) make_propp end;
+ in ((propss, [], []), ctxt') end;
+ in init #> generic_goal "" before_qed (K I, after_qed) make_statement end;
val theorem = global_goal Proof_Context.cert_propp;
val theorem_cmd = global_goal Proof_Context.read_propp;
@@ -1065,13 +1079,19 @@
(* common goal statements *)
+fun internal_goal print_results mode =
+ local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
+ Proof_Context.cert_var;
+
local
-fun gen_have prep_att prep_propp before_qed after_qed stmt int =
+fun gen_have prep_att prep_propp prep_var
+ before_qed after_qed fixes stmt int =
local_goal (Proof_Display.print_results int (Position.thread_data ()))
- prep_att prep_propp "have" before_qed after_qed stmt;
+ prep_att prep_propp prep_var "have" before_qed after_qed fixes stmt;
-fun gen_show prep_att prep_propp before_qed after_qed stmt int state =
+fun gen_show prep_att prep_propp prep_var
+ before_qed after_qed fixes stmt int state =
let
val testing = Unsynchronized.ref false;
val rule = Unsynchronized.ref (NONE: thm option);
@@ -1102,7 +1122,8 @@
#> after_qed results;
in
state
- |> local_goal print_results prep_att prep_propp "show" before_qed after_qed' stmt
+ |> local_goal print_results prep_att prep_propp prep_var
+ "show" before_qed after_qed' fixes stmt
|> int ? (fn goal_state =>
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of
Exn.Res _ => goal_state
@@ -1111,10 +1132,10 @@
in
-val have = gen_have (K I) Proof_Context.cert_propp;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp;
-val show = gen_show (K I) Proof_Context.cert_propp;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp;
+val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
+val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
end;