--- a/NEWS Mon Jun 08 18:56:04 2015 +0100
+++ b/NEWS Mon Jun 08 22:04:19 2015 +0200
@@ -9,6 +9,9 @@
*** Pure ***
+* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
+the proof body as well, abstracted over the hypothetical parameters.
+
* New Isar command 'supply' supports fact definitions during goal
refinement ('apply' scripts).
--- a/src/Pure/Isar/element.ML Mon Jun 08 18:56:04 2015 +0100
+++ b/src/Pure/Isar/element.ML Mon Jun 08 22:04:19 2015 +0200
@@ -278,10 +278,10 @@
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness #> Seq.hd end;
-fun proof_local cmd goal_ctxt int after_qed' propss =
+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.bind_propp cmd NONE
- after_qed' (map (pair Thm.empty_binding) propss);
+ Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE
+ after_qed' (map (pair Thm.empty_binding) propp);
in
--- a/src/Pure/Isar/obtain.ML Mon Jun 08 18:56:04 2015 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Jun 08 22:04:19 2015 +0200
@@ -71,13 +71,13 @@
space_implode " " (map (Syntax.string_of_term ctxt) bads));
in tm end;
-fun eliminate fix_ctxt rule xs As thm =
+fun eliminate ctxt rule xs As thm =
let
- val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
- val _ = Object_Logic.is_judgment fix_ctxt (Thm.concl_of thm) orelse
+ val _ = eliminate_term ctxt xs (Thm.full_prop_of thm);
+ val _ = Object_Logic.is_judgment ctxt (Thm.concl_of thm) orelse
error "Conclusion in obtained context must be object-logic judgment";
- val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
+ val ((_, [thm']), ctxt') = Variable.import true [thm] ctxt;
val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
in
((Drule.implies_elim_list thm' (map Thm.assume prems)
@@ -85,7 +85,7 @@
|> Drule.forall_intr_list xs)
COMP rule)
|> Drule.implies_intr_list prems
- |> singleton (Variable.export ctxt' fix_ctxt)
+ |> singleton (Variable.export ctxt' ctxt)
end;
fun obtain_export ctxt rule xs _ As =
@@ -113,30 +113,37 @@
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
(*obtain vars*)
- val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
- val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
+ val ((xs', vars), fix_ctxt) = ctxt
+ |> fold_map prep_var raw_vars
+ |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
val xs = map (Variable.check_name o #1) vars;
(*obtain asms*)
- val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
- val ((_, binds), binds_ctxt) = Proof_Context.bind_propp proppss asms_ctxt;
- val asm_props = maps (map fst) proppss;
- val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss;
+ val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
+ val asm_props = flat asm_propss;
+ val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds;
+ val asms =
+ map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
+ map (map (rpair [])) asm_propss;
- (*obtain parms*)
- val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
- val parms = map Free (xs' ~~ Ts);
- val cparms = map (Thm.cterm_of ctxt) parms;
- val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
+ (*obtain params*)
+ val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
+ val params = map Free (xs' ~~ Ts);
+ val cparams = map (Thm.cterm_of params_ctxt) params;
+ val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
+
+ (*abstracted term bindings*)
+ val abs_term = Term.close_schematic_term o fold_rev Term.lambda_name (xs ~~ params);
+ val binds' = map (apsnd abs_term) binds;
(*obtain statements*)
val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
- val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
+ val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN);
val that_name = if name = "" then thatN else name;
val that_prop =
Logic.list_rename_params xs
- (fold_rev Logic.all parms (Logic.list_implies (asm_props, thesis)));
+ (fold_rev Logic.all params (Logic.list_implies (asm_props, thesis)));
val obtain_prop =
Logic.list_rename_params [Auto_Bind.thesisN]
(Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
@@ -145,12 +152,13 @@
Proof.local_qed (NONE, false)
#> `Proof.the_fact #-> (fn rule =>
Proof.fix vars
- #> Proof.assm (obtain_export fix_ctxt rule cparms) asms);
+ #> Proof.map_context declare_asms
+ #> Proof.assm (obtain_export params_ctxt rule cparams) asms);
in
state
|> Proof.enter_forward
|> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
- |> Proof.map_context (Proof_Context.export_bind_terms binds binds_ctxt)
+ |> Proof.map_context (Proof_Context.bind_terms binds')
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume
@@ -308,7 +316,7 @@
|> Proof.begin_block
|> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
- |> Proof.local_goal print_result (K I) (pair o rpair [])
+ |> Proof.local_goal print_result (K I) (K (rpair []))
"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
--- a/src/Pure/Isar/proof.ML Mon Jun 08 18:56:04 2015 +0100
+++ b/src/Pure/Isar/proof.ML Mon Jun 08 22:04:19 2015 +0200
@@ -91,7 +91,7 @@
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) ->
- ('b list -> context -> (term list list * (indexname * term) list) * context) ->
+ (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
@@ -910,19 +910,21 @@
in
-fun generic_goal prepp kind before_qed after_qed raw_propp state =
+fun generic_goal prep_propp kind before_qed after_qed propp 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, binds) = prep_propp ctxt propp;
+ val props = flat propss;
+
+ val goal_state =
state
|> assert_forward_or_chain
|> enter_forward
|> open_block
- |> map_context_result (prepp raw_propp);
- val props = flat propss;
+ |> map_context (fold Variable.auto_fixes props #> Proof_Context.bind_terms binds);
val goal_ctxt = context_of goal_state;
val vars = implicit_vars props;
@@ -972,7 +974,7 @@
(* local goals *)
-fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
+fun local_goal print_results prep_att prep_propp kind before_qed after_qed stmt state =
let
val ((names, attss), propp) =
Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
@@ -983,7 +985,8 @@
#> after_qed results;
in
state
- |> generic_goal prepp kind before_qed (after_qed', K I) propp
+ |> map_context (Variable.set_body true)
+ |> generic_goal prep_propp kind before_qed (after_qed', K I) propp
|> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
end;
@@ -998,16 +1001,13 @@
(* global goals *)
-fun prepp_auto_fixes prepp args =
- prepp args #>
- (fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt));
+fun global_goal prep_propp before_qed after_qed propp =
+ init
+ #> generic_goal (prep_propp o Proof_Context.set_mode Proof_Context.mode_schematic) ""
+ before_qed (K I, after_qed) propp;
-fun global_goal prepp before_qed after_qed propp =
- init #>
- generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp;
-
-val theorem = global_goal Proof_Context.bind_propp_schematic;
-val theorem_cmd = global_goal Proof_Context.bind_propp_schematic_cmd;
+val theorem = global_goal Proof_Context.cert_propp;
+val theorem_cmd = global_goal Proof_Context.read_propp;
fun global_qeds arg =
end_proof true arg
@@ -1056,11 +1056,11 @@
local
-fun gen_have prep_att prepp before_qed after_qed stmt int =
+fun gen_have prep_att prep_propp before_qed after_qed stmt int =
local_goal (Proof_Display.print_results int (Position.thread_data ()))
- prep_att prepp "have" before_qed after_qed stmt;
+ prep_att prep_propp "have" before_qed after_qed stmt;
-fun gen_show prep_att prepp before_qed after_qed stmt int state =
+fun gen_show prep_att prep_propp before_qed after_qed stmt int state =
let
val testing = Unsynchronized.ref false;
val rule = Unsynchronized.ref (NONE: thm option);
@@ -1091,7 +1091,7 @@
#> after_qed results;
in
state
- |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
+ |> local_goal print_results prep_att prep_propp "show" before_qed after_qed' stmt
|> int ? (fn goal_state =>
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of
Exn.Res _ => goal_state
@@ -1100,10 +1100,10 @@
in
-val have = gen_have (K I) Proof_Context.bind_propp;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp_cmd;
-val show = gen_show (K I) Proof_Context.bind_propp;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp_cmd;
+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;
end;
--- a/src/Pure/Isar/proof_context.ML Mon Jun 08 18:56:04 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Jun 08 22:04:19 2015 +0200
@@ -114,18 +114,10 @@
term list * Proof.context
val match_bind_cmd: bool -> (string list * string) list -> Proof.context ->
term list * Proof.context
- val read_propp: (string * string list) list list -> Proof.context ->
- (term * term list) list list * Proof.context
- val cert_propp: (term * term list) list list -> Proof.context ->
- (term * term list) list list * Proof.context
- val bind_propp: (term * term list) list list -> Proof.context ->
- (term list list * (indexname * term) list) * Proof.context
- val bind_propp_cmd: (string * string list) list list -> Proof.context ->
- (term list list * (indexname * term) list) * Proof.context
- val bind_propp_schematic: (term * term list) list list -> Proof.context ->
- (term list list * (indexname * term) list) * Proof.context
- val bind_propp_schematic_cmd: (string * string list) list list -> Proof.context ->
- (term list list * (indexname * term) list) * Proof.context
+ val cert_propp: Proof.context -> (term * term list) list list ->
+ (term list list * (indexname * term) list)
+ val read_propp: Proof.context -> (string * string list) list list ->
+ (term list list * (indexname * term) list)
val fact_tac: Proof.context -> thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
@@ -892,30 +884,20 @@
local
-fun prep_propp mode prep_props raw_args ctxt =
+fun prep_propp prep_props ctxt raw_args =
let
- val props = prep_props (set_mode mode ctxt) (maps (map fst) raw_args);
- val ctxt' = fold Variable.declare_term props ctxt;
- val patss = maps (map (prep_props (set_mode mode_pattern ctxt') o snd)) raw_args;
- val propp = unflat raw_args (props ~~ patss);
- in (propp, ctxt') end;
+ val props = prep_props ctxt (maps (map fst) raw_args);
+ val props_ctxt = fold Variable.declare_term props ctxt;
+ val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args;
-fun gen_bind_propp mode parse_prop raw_args ctxt =
- let
- val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt;
- val propss = map (map fst) args;
- val binds = (maps o maps) (simult_matches ctxt') args;
- in ((propss, binds), bind_terms binds ctxt') end;
+ val propps = unflat raw_args (props ~~ patss);
+ val binds = (maps o maps) (simult_matches props_ctxt) propps;
+ in (map (map fst) propps, binds) end;
in
-val read_propp = prep_propp mode_default Syntax.read_props;
-val cert_propp = prep_propp mode_default (map o cert_prop);
-
-val bind_propp = gen_bind_propp mode_default (map o cert_prop);
-val bind_propp_cmd = gen_bind_propp mode_default Syntax.read_props;
-val bind_propp_schematic = gen_bind_propp mode_schematic (map o cert_prop);
-val bind_propp_schematic_cmd = gen_bind_propp mode_schematic Syntax.read_props;
+val cert_propp = prep_propp (map o cert_prop);
+val read_propp = prep_propp Syntax.read_props;
end;
@@ -1176,22 +1158,25 @@
local
-fun gen_assms prepp exp args ctxt =
+fun gen_assms prep_propp exp args ctxt =
let
- val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
- val _ = Variable.warn_extra_tfrees ctxt ctxt1;
- val (premss, ctxt2) =
- fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss ctxt1;
+ val (propss, binds) = prep_propp ctxt (map snd args);
+ val props = flat propss;
in
- ctxt2
- |> auto_bind_facts (flat propss)
- |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)
+ ctxt
+ |> fold Variable.declare_term props
+ |> tap (Variable.warn_extra_tfrees ctxt)
+ |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
+ |-> (fn premss =>
+ auto_bind_facts props
+ #> bind_terms binds
+ #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
end;
in
-val add_assms = gen_assms bind_propp;
-val add_assms_cmd = gen_assms bind_propp_cmd;
+val add_assms = gen_assms cert_propp;
+val add_assms_cmd = gen_assms read_propp;
end;