--- a/src/Pure/Isar/element.ML Sat Jun 13 22:44:22 2015 +0200
+++ b/src/Pure/Isar/element.ML Sat Jun 13 23:36:21 2015 +0200
@@ -292,7 +292,7 @@
in
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) #> snd
end;
in
--- a/src/Pure/Isar/isar_syn.ML Sat Jun 13 22:44:22 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sat Jun 13 23:36:21 2015 +0200
@@ -496,23 +496,23 @@
val _ =
Outer_Syntax.command @{command_keyword have} "state local goal"
- (structured_statement >> (fn (fixes, assumes, shows) =>
- Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes assumes shows int)));
+ (structured_statement >> (fn (a, b, c) =>
+ Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) a b c int #> #2)));
val _ =
Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
- (structured_statement >> (fn (fixes, assumes, shows) =>
- Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) fixes assumes shows int)));
+ (structured_statement >> (fn (a, b, c) =>
+ Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) a b c int #> #2)));
val _ =
Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
- (structured_statement >> (fn (fixes, assumes, shows) =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes assumes shows int)));
+ (structured_statement >> (fn (a, b, c) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) a b c int #> #2)));
val _ =
Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\""
- (structured_statement >> (fn (fixes, assumes, shows) =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes assumes shows int)));
+ (structured_statement >> (fn (a, b, c) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) a b c int #> #2)));
(* facts *)
--- a/src/Pure/Isar/obtain.ML Sat Jun 13 22:44:22 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Sat Jun 13 23:36:21 2015 +0200
@@ -158,8 +158,7 @@
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
(map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
[((Binding.empty, atts), [(thesis, [])])] int
- |> (fn state' => state'
- |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
+ |-> Proof.refine_insert
end;
in
@@ -233,8 +232,7 @@
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
[((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
[(Thm.empty_binding, [(thesis, [])])] int
- |> (fn state' => state'
- |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
+ |-> Proof.refine_insert
|> Proof.map_context (fold Variable.bind_term binds')
end;
@@ -407,9 +405,12 @@
|> 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, [])])]
+ |> snd
|> Proof.refine (Method.primitive_text (fn _ => fn _ =>
- Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
+ Goal.init (Thm.cterm_of ctxt thesis)))
+ |> Seq.hd
end;
in
--- a/src/Pure/Isar/proof.ML Sat Jun 13 22:44:22 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sat Jun 13 23:36:21 2015 +0200
@@ -109,23 +109,23 @@
(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 -> state
+ (Thm.binding * (term * term list) list) list -> state -> thm list * state
val have: 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 -> state
+ (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
val have_cmd: 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 -> state
+ (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
val show: 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 -> state
+ (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
val show_cmd: 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 -> state
+ (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
val schematic_goal: state -> bool
val is_relevant: state -> bool
val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
@@ -986,7 +986,7 @@
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);
- val (goal_ctxt, goal_propss, result_binds) =
+ val (goal_ctxt, goal_propss, result_binds, that_fact) =
let
(*fixed variables*)
val ((xs', vars), fix_ctxt) = ctxt
@@ -1006,16 +1006,20 @@
val params = xs ~~ map Free ps;
(*prems*)
- val goal_ctxt = params_ctxt
+ 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)
- |> (fn (premss, ctxt') => ctxt'
- |> not (null assumes_propss) ?
- (snd o Proof_Context.note_thmss ""
- [((Binding.name Auto_Bind.thatN, []),
- [(Assumption.local_prems_of ctxt' ctxt, [])])])
- |> (snd o Proof_Context.note_thmss ""
- (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
+ |> (fn (premss, ctxt') =>
+ let
+ val prems = Assumption.local_prems_of ctxt' ctxt;
+ val ctxt'' =
+ ctxt'
+ |> not (null assumes_propss) ?
+ (snd o Proof_Context.note_thmss ""
+ [((Binding.name Auto_Bind.thatN, []), [(prems, [])])])
+ |> (snd o Proof_Context.note_thmss ""
+ (assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
+ in (prems, ctxt'') end);
val _ = Variable.warn_extra_tfrees fix_ctxt goal_ctxt;
@@ -1029,13 +1033,17 @@
(Auto_Bind.facts goal_ctxt shows_props @ binds')
|> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
|> export_binds goal_ctxt ctxt;
- in (goal_ctxt, shows_propss, result_binds) end;
+ in (goal_ctxt, shows_propss, result_binds, that_fact) end;
fun after_qed' (result_ctxt, results) state' = state'
|> local_results (shows_bindings ~~ burrow (Proof_Context.export result_ctxt ctxt) results)
|-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
|> after_qed (result_ctxt, results);
- in generic_goal kind before_qed (after_qed', K I) goal_ctxt goal_propss result_binds state end;
+ in
+ state
+ |> generic_goal kind before_qed (after_qed', K I) goal_ctxt goal_propss result_binds
+ |> pair that_fact
+ end;
end;
@@ -1157,7 +1165,7 @@
state
|> local_goal print_results prep_att prep_propp prep_var
"show" before_qed after_qed' fixes assumes shows
- |> int ? (fn goal_state =>
+ ||> int ? (fn goal_state =>
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of
Exn.Res _ => goal_state
| Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))