--- 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;
--- 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))
--- 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
();
--- 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);
--- 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);
--- 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 =
--- 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;
-