--- a/NEWS Mon Jun 08 14:45:31 2015 +0200
+++ b/NEWS Mon Jun 08 19:38:08 2015 +0200
@@ -9,6 +9,9 @@
*** Pure ***
+* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
+the proof body as well, abstracted over hypothetical parameters.
+
* New Isar command 'supply' supports fact definitions during goal
refinement ('apply' scripts).
--- a/src/Pure/Isar/obtain.ML Mon Jun 08 14:45:31 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Mon Jun 08 19:38:08 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 =
@@ -118,16 +118,26 @@
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 ((propss, binds), props_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
+ val props = flat propss;
+ val asms =
+ map (fn ((b, raw_atts), _) => (b, map (prep_att ctxt) raw_atts)) raw_asms ~~
+ unflat propss (map (rpair []) props);
- (*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' props_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*)
+ fun abs_params t =
+ let
+ val ps =
+ (xs ~~ params) |> map_filter (fn (x, p) =>
+ if exists_subterm (fn u => u aconv p) t then SOME (x, p) else NONE);
+ in fold_rev Term.lambda_name ps t end;
+ val binds' = map (apsnd (Term.close_schematic_term o abs_params)) binds;
(*obtain statements*)
val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
@@ -136,7 +146,7 @@
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 (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 +155,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 (Proof_Context.bind_terms binds)
+ #> 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
@@ -163,8 +174,8 @@
in
-val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.cert_propp;
-val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.read_propp;
+val obtain = gen_obtain (K I) Proof_Context.cert_var Proof_Context.bind_propp;
+val obtain_cmd = gen_obtain Attrib.attribute_cmd Proof_Context.read_var Proof_Context.bind_propp_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Mon Jun 08 14:45:31 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Jun 08 19:38:08 2015 +0200
@@ -114,10 +114,6 @@
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 ->
@@ -888,26 +884,20 @@
local
-fun prep_propp prep_props raw_args ctxt =
+fun gen_bind_propp prep_props raw_args ctxt =
let
val props = prep_props 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;
-fun gen_bind_propp parse_prop raw_args ctxt =
- let
- val (args, ctxt') = prep_propp parse_prop raw_args ctxt;
- val propss = map (map fst) args;
- val binds = (maps o maps) (simult_matches ctxt') args;
+ val patss = maps (map (prep_props (set_mode mode_pattern ctxt') o snd)) raw_args;
+ val propps = unflat raw_args (props ~~ patss);
+ val binds = (maps o maps) (simult_matches ctxt') propps;
+
+ val propss = map (map fst) propps;
in ((propss, binds), bind_terms binds ctxt') end;
in
-val read_propp = prep_propp Syntax.read_props;
-val cert_propp = prep_propp (map o cert_prop);
-
val bind_propp = gen_bind_propp (map o cert_prop);
val bind_propp_cmd = gen_bind_propp Syntax.read_props;