--- 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