# HG changeset patch # User wenzelm # Date 1433843465 -7200 # Node ID 16cf5090d3a6912f8cd8c823dbe9122f28a09014 # Parent b640770117fd727155d73f3b41b9a9bf546594a6 clarified term bindings; diff -r b640770117fd -r 16cf5090d3a6 src/Pure/Isar/auto_bind.ML --- a/src/Pure/Isar/auto_bind.ML Mon Jun 08 22:04:19 2015 +0200 +++ b/src/Pure/Isar/auto_bind.ML Tue Jun 09 11:51:05 2015 +0200 @@ -11,7 +11,7 @@ val assmsN: string val goal: Proof.context -> term list -> (indexname * term option) list val facts: Proof.context -> term list -> (indexname * term option) list - val no_facts: (indexname * term option) list + val no_facts: indexname list end; structure Auto_Bind: AUTO_BIND = @@ -47,6 +47,6 @@ let val prop = List.last props in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end; -val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)]; +val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)]; end; diff -r b640770117fd -r 16cf5090d3a6 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Mon Jun 08 22:04:19 2015 +0200 +++ b/src/Pure/Isar/obtain.ML Tue Jun 09 11:51:05 2015 +0200 @@ -130,11 +130,9 @@ 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; + val binds' = map (apsnd (fold_rev Term.lambda_name (xs ~~ params))) binds; - (*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; + val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt; (*obtain statements*) val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN; @@ -158,7 +156,7 @@ state |> Proof.enter_forward |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int - |> Proof.map_context (Proof_Context.bind_terms binds') + |> Proof.map_context (fold Variable.bind_term binds') |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)] |> Proof.assume @@ -297,7 +295,7 @@ |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts)) [(Thm.empty_binding, asms)]) - |> Proof.map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts) + |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts) end; val goal = Var (("guess", 0), propT); diff -r b640770117fd -r 16cf5090d3a6 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Jun 08 22:04:19 2015 +0200 +++ b/src/Pure/Isar/proof.ML Tue Jun 09 11:51:05 2015 +0200 @@ -769,7 +769,7 @@ in state' |> assume assumptions - |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts) + |> map_context (fold Variable.unbind_term Auto_Bind.no_facts) |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])]) end; @@ -935,8 +935,9 @@ |> Thm.cterm_of ctxt |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt); val statement = ((kind, pos), propss', Thm.term_of goal); + val binds' = map #1 binds ~~ Variable.export_terms goal_ctxt ctxt (map #2 binds); val after_qed' = after_qed |>> (fn after_local => fn results => - map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results); + map_context (fold Variable.bind_term binds') #> after_local results); in goal_state |> map_context (init_context #> Variable.set_body true) diff -r b640770117fd -r 16cf5090d3a6 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Jun 08 22:04:19 2015 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Jun 09 11:51:05 2015 +0200 @@ -107,7 +107,6 @@ val norm_export_morphism: Proof.context -> Proof.context -> morphism val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context val bind_terms: (indexname * term) list -> Proof.context -> Proof.context - val export_bind_terms: (indexname * term) list -> Proof.context -> Proof.context -> Proof.context val auto_bind_goal: term list -> Proof.context -> Proof.context val auto_bind_facts: term list -> Proof.context -> Proof.context val match_bind: bool -> (term list * term) list -> Proof.context -> @@ -823,14 +822,10 @@ val maybe_bind_terms = fold (fn (xi, t) => fn ctxt => ctxt - |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t)); + |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t)); val bind_terms = maybe_bind_terms o map (apsnd SOME); -fun export_bind_terms binds ctxt ctxt0 = - let val ts0 = map Term.close_schematic_term (Variable.export_terms ctxt ctxt0 (map snd binds)) - in bind_terms (map fst binds ~~ ts0) ctxt0 end; - (* auto_bind *) diff -r b640770117fd -r 16cf5090d3a6 src/Pure/variable.ML --- a/src/Pure/variable.ML Mon Jun 08 22:04:19 2015 +0200 +++ b/src/Pure/variable.ML Tue Jun 09 11:51:05 2015 +0200 @@ -24,7 +24,9 @@ val declare_prf: Proofterm.proof -> Proof.context -> Proof.context val declare_thm: thm -> Proof.context -> Proof.context val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list - val bind_term: indexname * term option -> Proof.context -> Proof.context + val bind_term: indexname * term -> Proof.context -> Proof.context + val unbind_term: indexname -> Proof.context -> Proof.context + val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context val expand_binds: Proof.context -> term -> term val lookup_const: Proof.context -> string -> string option val is_const: Proof.context -> string -> bool @@ -274,12 +276,16 @@ (** term bindings **) -fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi) - | bind_term ((x, i), SOME t) = - let - val u = Term.close_schematic_term t; - val U = Term.fastype_of u; - in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end; +fun bind_term ((x, i), t) = + let + val u = Term.close_schematic_term t; + val U = Term.fastype_of u; + in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end; + +val unbind_term = map_binds o Vartab.delete_safe; + +fun maybe_bind_term (xi, SOME t) = bind_term (xi, t) + | maybe_bind_term (xi, NONE) = unbind_term xi; fun expand_binds ctxt = let @@ -638,9 +644,8 @@ fun focus_subgoal i st = let val all_vars = Thm.fold_terms Term.add_vars st []; - val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars; in - fold bind_term no_binds #> + fold (unbind_term o #1) all_vars #> fold (declare_constraints o Var) all_vars #> focus_cterm (Thm.cprem_of st i) end;