# HG changeset patch # User wenzelm # Date 1433785088 -7200 # Node ID 76359ff1090f4f2070c168d9d71a04748d7b326a # Parent 16b5b1b9dd02ecd235580fce4efa3e67dc69c261 more careful treatment of term bindings in 'obtain' proof body; tuned signature; diff -r 16b5b1b9dd02 -r 76359ff1090f NEWS --- 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). diff -r 16b5b1b9dd02 -r 76359ff1090f src/Pure/Isar/obtain.ML --- 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; diff -r 16b5b1b9dd02 -r 76359ff1090f src/Pure/Isar/proof_context.ML --- 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;