# HG changeset patch # User wenzelm # Date 1433229379 -7200 # Node ID aebfbcab1eb8bb72c49ff45d90ddd9995401cac8 # Parent bc0827281dc1e172979a927b609cd13914795fc3 clarified context; diff -r bc0827281dc1 -r aebfbcab1eb8 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Tue Jun 02 09:10:05 2015 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Tue Jun 02 09:16:19 2015 +0200 @@ -41,8 +41,8 @@ val prolog_step_tac': Proof.context -> thm list -> int -> tactic val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic - val make_meta_clause: thm -> thm - val make_meta_clauses: thm list -> thm list + val make_meta_clause: Proof.context -> thm -> thm + val make_meta_clauses: Proof.context -> thm list -> thm list val meson_tac: Proof.context -> thm list -> int -> tactic end @@ -787,15 +787,15 @@ th RS notEfalse handle THM _ => th RS notEfalse'; (*Converting one theorem from a disjunction to a meta-level clause*) -fun make_meta_clause th = - let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th +fun make_meta_clause ctxt th = + let val (fth, thaw) = Misc_Legacy.freeze_thaw_robust ctxt th in (zero_var_indexes o Thm.varifyT_global o thaw 0 o negated_asm_of_head o make_horn resolution_clause_rules) fth end; -fun make_meta_clauses ths = +fun make_meta_clauses ctxt ths = name_thms "MClause#" - (distinct Thm.eq_thm_prop (map make_meta_clause ths)); + (distinct Thm.eq_thm_prop (map (make_meta_clause ctxt) ths)); end; diff -r bc0827281dc1 -r aebfbcab1eb8 src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 02 09:10:05 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 02 09:16:19 2015 +0200 @@ -133,7 +133,7 @@ val proxy_defs = map (fst o snd o snd) proxy_table fun prepare_helper ctxt = - Meson.make_meta_clause #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs) + Meson.make_meta_clause ctxt #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs) fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) = if is_tptp_variable s then @@ -181,7 +181,7 @@ SOME s => let val s = s |> space_explode "_" |> tl |> space_implode "_" in (case Int.fromString s of - SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some + SOME j => Meson.make_meta_clause ctxt (snd (nth clauses j)) |> Isa_Raw |> some | NONE => if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some else raise Fail ("malformed fact identifier " ^ quote ident)) diff -r bc0827281dc1 -r aebfbcab1eb8 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Jun 02 09:10:05 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Jun 02 09:16:19 2015 +0200 @@ -32,8 +32,9 @@ val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true) (* Designed to work also with monomorphic instances of polymorphic theorems. *) -fun have_common_thm ths1 ths2 = - exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) (map Meson.make_meta_clause ths2) +fun have_common_thm ctxt ths1 ths2 = + exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) + (map (Meson.make_meta_clause ctxt) ths2) (*Determining which axiom clauses are actually used*) fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) @@ -54,14 +55,14 @@ (if can HOLogic.dest_not t1 then t2 else t1) |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial | _ => raise Fail "expected reflexive or trivial clause") - |> Meson.make_meta_clause + |> Meson.make_meta_clause ctxt fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth = let val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1 val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) - in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end + in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause ctxt end fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u] | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t @@ -201,7 +202,7 @@ val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used val (used_th_cls_pairs, unused_th_cls_pairs) = - List.partition (have_common_thm used o snd o snd) th_cls_pairs + List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs val unused_ths = maps (snd o snd) unused_th_cls_pairs val unused_names = map fst unused_th_cls_pairs in @@ -210,7 +211,7 @@ verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names) else (); - if not (null cls) andalso not (have_common_thm used cls) then + if not (null cls) andalso not (have_common_thm ctxt used cls) then verbose_warning ctxt "The assumptions are inconsistent" else (); diff -r bc0827281dc1 -r aebfbcab1eb8 src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Tue Jun 02 09:10:05 2015 +0200 +++ b/src/Tools/IsaPlanner/isand.ML Tue Jun 02 09:16:19 2015 +0200 @@ -137,14 +137,12 @@ ["SG0", ..., "SGm"] : thm list -> -- export function "G" : thm) *) -fun subgoal_thms th = +fun subgoal_thms ctxt th = let - val thy = Thm.theory_of_thm th; - val t = Thm.prop_of th; val prems = Logic.strip_imp_prems t; - val aprems = map (Thm.trivial o Thm.global_cterm_of thy) prems; + val aprems = map (Thm.trivial o Thm.cterm_of ctxt) prems; fun explortf premths = Drule.implies_elim_list th premths; in (aprems, explortf) end; @@ -167,7 +165,7 @@ (* requires being given solutions! *) fun fixed_subgoal_thms ctxt th = let - val (subgoals, expf) = subgoal_thms th; + val (subgoals, expf) = subgoal_thms ctxt th; (* fun export_sg (th, exp) = exp th; *) fun export_sgs expfs solthms = expf (map2 (curry (op |>)) solthms expfs); diff -r bc0827281dc1 -r aebfbcab1eb8 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Tue Jun 02 09:10:05 2015 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Tue Jun 02 09:16:19 2015 +0200 @@ -30,15 +30,13 @@ th: A vs ==> B vs Results in: "B vs" [!!x. A x] *) -fun allify_conditions Ts th = +fun allify_conditions ctxt Ts th = let - val thy = Thm.theory_of_thm th; - fun allify (x, T) t = Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t)); - val cTs = map (Thm.global_cterm_of thy o Free) Ts; - val cterm_asms = map (Thm.global_cterm_of thy o fold_rev allify Ts) (Thm.prems_of th); + val cTs = map (Thm.cterm_of ctxt o Free) Ts; + val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th); val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms; in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; @@ -82,7 +80,7 @@ |> Drule.forall_elim_list tonames; (* make unconditional rule and prems *) - val (uncond_rule, cprems) = allify_conditions (rev Ts') rule'; + val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule'; (* using these names create lambda-abstracted version of the rule *) val abstractions = rev (Ts' ~~ tonames); diff -r bc0827281dc1 -r aebfbcab1eb8 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Tue Jun 02 09:10:05 2015 +0200 +++ b/src/Tools/eqsubst.ML Tue Jun 02 09:16:19 2015 +0200 @@ -14,7 +14,7 @@ * term (* outer term *) type searchinfo = - theory + Proof.context * int (* maxidx *) * Zipper.T (* focusterm to search under *) @@ -67,7 +67,7 @@ * term; (* outer term *) type searchinfo = - theory + Proof.context * int (* maxidx *) * Zipper.T; (* focusterm to search under *) @@ -138,8 +138,8 @@ end; (* Unification with exception handled *) -(* given theory, max var index, pat, tgt; returns Seq of instantiations *) -fun clean_unify thy ix (a as (pat, tgt)) = +(* given context, max var index, pat, tgt; returns Seq of instantiations *) +fun clean_unify ctxt ix (a as (pat, tgt)) = let (* type info will be re-derived, maybe this can be cached for efficiency? *) @@ -148,7 +148,7 @@ (* FIXME is it OK to ignore the type instantiation info? or should I be using it? *) val typs_unify = - SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix)) + SOME (Sign.typ_unify (Proof_Context.theory_of ctxt) (pat_ty, tgt_ty) (Vartab.empty, ix)) handle Type.TUNIFY => NONE; in (case typs_unify of @@ -161,7 +161,7 @@ Vartab.dest (Envir.term_env env)); val initenv = Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab}; - val useq = Unify.smash_unifiers (Context.Theory thy) [a] initenv + val useq = Unify.smash_unifiers (Context.Proof ctxt) [a] initenv handle ListPair.UnequalLengths => Seq.empty | Term.TERM _ => Seq.empty; fun clean_unify' useq () = @@ -181,10 +181,10 @@ bound variables. New names have been introduced to make sure they are unique w.r.t all names in the term and each other. usednames' is oldnames + new names. *) -fun clean_unify_z thy maxidx pat z = +fun clean_unify_z ctxt maxidx pat z = let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) - (clean_unify thy maxidx (t, pat)) + (clean_unify ctxt maxidx (t, pat)) end; @@ -230,8 +230,8 @@ end; in Zipper.lzy_search sf_valid_td_lr end; -fun searchf_unify_gen f (thy, maxidx, z) lhs = - Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z); +fun searchf_unify_gen f (ctxt, maxidx, z) lhs = + Seq.map (clean_unify_z ctxt maxidx lhs) (Zipper.limit_apply f z); (* search all unifications *) val searchf_lr_unify_all = searchf_unify_gen search_lr_all; @@ -271,7 +271,7 @@ o Zipper.mktop o Thm.prop_of) conclthm in - ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft)) + ((cfvs, conclthm), (ctxt, maxidx, ft)) end; (* substitute using an object or meta level equality *) @@ -345,23 +345,20 @@ val th = Thm.incr_indexes 1 gth; val tgt_term = Thm.prop_of th; - val thy = Thm.theory_of_thm th; - val cert = Thm.global_cterm_of thy; - val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; - val cfvs = rev (map cert fvs); + val cfvs = rev (map (Thm.cterm_of ctxt) fvs); val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1); val asm_nprems = length (Logic.strip_imp_prems asmt); - val pth = Thm.trivial (cert asmt); + val pth = Thm.trivial ((Thm.cterm_of ctxt) asmt); val maxidx = Thm.maxidx_of th; val ft = (Zipper.move_down_right (* trueprop *) o Zipper.mktop o Thm.prop_of) pth - in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end; + in ((cfvs, j, asm_nprems, pth), (ctxt, maxidx, ft)) end; (* prepare subst in every possible assumption *) fun prep_subst_in_asms ctxt i gth = diff -r bc0827281dc1 -r aebfbcab1eb8 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Tue Jun 02 09:10:05 2015 +0200 +++ b/src/Tools/misc_legacy.ML Tue Jun 02 09:16:19 2015 +0200 @@ -23,8 +23,8 @@ val mk_defpair: term * term -> string * term val get_def: theory -> xstring -> thm val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic - val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) - val freeze_thaw: thm -> thm * (thm -> thm) + val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm) + val freeze_thaw: Proof.context -> thm -> thm * (thm -> thm) end; structure Misc_Legacy: MISC_LEGACY = @@ -161,13 +161,12 @@ fun metahyps_aux_tac ctxt tacf (prem,gno) state = let val (insts,params,hyps,concl) = metahyps_split_prem prem val maxidx = Thm.maxidx_of state - val cterm = Thm.global_cterm_of (Thm.theory_of_thm state) - val chyps = map cterm hyps + val chyps = map (Thm.cterm_of ctxt) hyps val hypths = map Thm.assume chyps val subprems = map (Thm.forall_elim_vars 0) hypths val fparams = map Free params - val cparams = map cterm fparams - fun swap_ctpair (t,u) = (cterm u, cterm t) + val cparams = map (Thm.cterm_of ctxt) fparams + fun swap_ctpair (t, u) = apply2 (Thm.cterm_of ctxt) (u, t) (*Subgoal variables: make Free; lift type over params*) fun mk_subgoal_inst concl_vars (v, T) = if member (op =) concl_vars (v, T) @@ -175,12 +174,12 @@ else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) (*Instantiate subgoal vars by Free applied to params*) fun mk_ctpair (v, in_concl, u) = - if in_concl then (cterm (Var v), cterm u) - else (cterm (Var v), cterm (list_comb (u, fparams))) + if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u) + else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams)) (*Restore Vars with higher type and index*) fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = - if in_concl then (cterm u, cterm (Var ((a, i), T))) - else (cterm u, cterm (Var ((a, i + maxidx), U))) + if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T)) + else apply2 (Thm.cterm_of ctxt) (u, Var ((a, i + maxidx), U)) (*Embed B in the original context of params and hyps*) fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B)) (*Strip the context using elimination rules*) @@ -193,7 +192,7 @@ and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st - val emBs = map (cterm o embed) (Thm.prems_of st') + val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st') val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) in (*restore the unknowns to the hypotheses*) free_instantiate (map swap_ctpair insts @ @@ -206,7 +205,7 @@ fun next st = Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} (false, relift st, Thm.nprems_of st) gno state - in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end; + in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end; fun print_vars_terms ctxt n thm = let @@ -255,9 +254,8 @@ (*Convert all Vars in a theorem to Frees. Also return a function for reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) -fun freeze_thaw_robust th = +fun freeze_thaw_robust ctxt th = let val fth = Thm.legacy_freezeT th - val thy = Thm.theory_of_thm fth in case Thm.fold_terms Term.add_vars fth [] of [] => (fth, fn _ => fn x => x) (*No vars: nothing to do!*) @@ -265,8 +263,8 @@ let fun newName (ix,_) = (ix, gensym (string_of_indexname ix)) val alist = map newName vars fun mk_inst (v,T) = - (Thm.global_cterm_of thy (Var(v,T)), - Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) + apply2 (Thm.cterm_of ctxt) + (Var (v, T), Free (the (AList.lookup (op =) alist v), T)) val insts = map mk_inst vars fun thaw i th' = (*i is non-negative increment for Var indexes*) th' |> forall_intr_list (map #2 insts) @@ -276,9 +274,8 @@ (*Basic version of the function above. No option to rename Vars apart in thaw. The Frees created from Vars have nice names.*) -fun freeze_thaw th = +fun freeze_thaw ctxt th = let val fth = Thm.legacy_freezeT th - val thy = Thm.theory_of_thm fth in case Thm.fold_terms Term.add_vars fth [] of [] => (fth, fn x => x) @@ -289,8 +286,7 @@ val (alist, _) = fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth []) fun mk_inst (v, T) = - (Thm.global_cterm_of thy (Var(v,T)), - Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) + apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T)) val insts = map mk_inst vars fun thaw th' = th' |> forall_intr_list (map #2 insts) @@ -299,4 +295,3 @@ end; end; -