clarified context;
authorwenzelm
Tue Jun 02 09:16:19 2015 +0200 (2015-06-02)
changeset 60358aebfbcab1eb8
parent 60357 bc0827281dc1
child 60359 cb8828b859a1
clarified context;
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/eqsubst.ML
src/Tools/misc_legacy.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -41,8 +41,8 @@
     1.4    val prolog_step_tac': Proof.context -> thm list -> int -> tactic
     1.5    val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic
     1.6    val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
     1.7 -  val make_meta_clause: thm -> thm
     1.8 -  val make_meta_clauses: thm list -> thm list
     1.9 +  val make_meta_clause: Proof.context -> thm -> thm
    1.10 +  val make_meta_clauses: Proof.context -> thm list -> thm list
    1.11    val meson_tac: Proof.context -> thm list -> int -> tactic
    1.12  end
    1.13  
    1.14 @@ -787,15 +787,15 @@
    1.15      th RS notEfalse handle THM _ => th RS notEfalse';
    1.16  
    1.17  (*Converting one theorem from a disjunction to a meta-level clause*)
    1.18 -fun make_meta_clause th =
    1.19 -  let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th
    1.20 +fun make_meta_clause ctxt th =
    1.21 +  let val (fth, thaw) = Misc_Legacy.freeze_thaw_robust ctxt th
    1.22    in  
    1.23        (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
    1.24         negated_asm_of_head o make_horn resolution_clause_rules) fth
    1.25    end;
    1.26  
    1.27 -fun make_meta_clauses ths =
    1.28 +fun make_meta_clauses ctxt ths =
    1.29      name_thms "MClause#"
    1.30 -      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
    1.31 +      (distinct Thm.eq_thm_prop (map (make_meta_clause ctxt) ths));
    1.32  
    1.33  end;
     2.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 02 09:10:05 2015 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 02 09:16:19 2015 +0200
     2.3 @@ -133,7 +133,7 @@
     2.4  
     2.5  val proxy_defs = map (fst o snd o snd) proxy_table
     2.6  fun prepare_helper ctxt =
     2.7 -  Meson.make_meta_clause #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
     2.8 +  Meson.make_meta_clause ctxt #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
     2.9  
    2.10  fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
    2.11    if is_tptp_variable s then
    2.12 @@ -181,7 +181,7 @@
    2.13            SOME s =>
    2.14            let val s = s |> space_explode "_" |> tl |> space_implode "_" in
    2.15              (case Int.fromString s of
    2.16 -              SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
    2.17 +              SOME j => Meson.make_meta_clause ctxt (snd (nth clauses j)) |> Isa_Raw |> some
    2.18              | NONE =>
    2.19                if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
    2.20                else raise Fail ("malformed fact identifier " ^ quote ident))
     3.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Jun 02 09:10:05 2015 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Jun 02 09:16:19 2015 +0200
     3.3 @@ -32,8 +32,9 @@
     3.4  val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
     3.5  
     3.6  (* Designed to work also with monomorphic instances of polymorphic theorems. *)
     3.7 -fun have_common_thm ths1 ths2 =
     3.8 -  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1) (map Meson.make_meta_clause ths2)
     3.9 +fun have_common_thm ctxt ths1 ths2 =
    3.10 +  exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
    3.11 +    (map (Meson.make_meta_clause ctxt) ths2)
    3.12  
    3.13  (*Determining which axiom clauses are actually used*)
    3.14  fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
    3.15 @@ -54,14 +55,14 @@
    3.16      (if can HOLogic.dest_not t1 then t2 else t1)
    3.17      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
    3.18    | _ => raise Fail "expected reflexive or trivial clause")
    3.19 -  |> Meson.make_meta_clause
    3.20 +  |> Meson.make_meta_clause ctxt
    3.21  
    3.22  fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
    3.23    let
    3.24      val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac ctxt [refl] 1
    3.25      val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
    3.26      val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t)
    3.27 -  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
    3.28 +  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause ctxt end
    3.29  
    3.30  fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
    3.31    | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
    3.32 @@ -201,7 +202,7 @@
    3.33           val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
    3.34           val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
    3.35           val (used_th_cls_pairs, unused_th_cls_pairs) =
    3.36 -           List.partition (have_common_thm used o snd o snd) th_cls_pairs
    3.37 +           List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
    3.38           val unused_ths = maps (snd o snd) unused_th_cls_pairs
    3.39           val unused_names = map fst unused_th_cls_pairs
    3.40         in
    3.41 @@ -210,7 +211,7 @@
    3.42             verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names)
    3.43           else
    3.44             ();
    3.45 -         if not (null cls) andalso not (have_common_thm used cls) then
    3.46 +         if not (null cls) andalso not (have_common_thm ctxt used cls) then
    3.47             verbose_warning ctxt "The assumptions are inconsistent"
    3.48           else
    3.49             ();
     4.1 --- a/src/Tools/IsaPlanner/isand.ML	Tue Jun 02 09:10:05 2015 +0200
     4.2 +++ b/src/Tools/IsaPlanner/isand.ML	Tue Jun 02 09:16:19 2015 +0200
     4.3 @@ -137,14 +137,12 @@
     4.4   ["SG0", ..., "SGm"] : thm list ->   -- export function
     4.5     "G" : thm)
     4.6  *)
     4.7 -fun subgoal_thms th =
     4.8 +fun subgoal_thms ctxt th =
     4.9    let
    4.10 -    val thy = Thm.theory_of_thm th;
    4.11 -
    4.12      val t = Thm.prop_of th;
    4.13  
    4.14      val prems = Logic.strip_imp_prems t;
    4.15 -    val aprems = map (Thm.trivial o Thm.global_cterm_of thy) prems;
    4.16 +    val aprems = map (Thm.trivial o Thm.cterm_of ctxt) prems;
    4.17  
    4.18      fun explortf premths = Drule.implies_elim_list th premths;
    4.19    in (aprems, explortf) end;
    4.20 @@ -167,7 +165,7 @@
    4.21  (* requires being given solutions! *)
    4.22  fun fixed_subgoal_thms ctxt th =
    4.23    let
    4.24 -    val (subgoals, expf) = subgoal_thms th;
    4.25 +    val (subgoals, expf) = subgoal_thms ctxt th;
    4.26  (*  fun export_sg (th, exp) = exp th; *)
    4.27      fun export_sgs expfs solthms =
    4.28        expf (map2 (curry (op |>)) solthms expfs);
     5.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Tue Jun 02 09:10:05 2015 +0200
     5.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Tue Jun 02 09:16:19 2015 +0200
     5.3 @@ -30,15 +30,13 @@
     5.4  th: A vs ==> B vs
     5.5  Results in: "B vs" [!!x. A x]
     5.6  *)
     5.7 -fun allify_conditions Ts th =
     5.8 +fun allify_conditions ctxt Ts th =
     5.9    let
    5.10 -    val thy = Thm.theory_of_thm th;
    5.11 -
    5.12      fun allify (x, T) t =
    5.13        Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
    5.14  
    5.15 -    val cTs = map (Thm.global_cterm_of thy o Free) Ts;
    5.16 -    val cterm_asms = map (Thm.global_cterm_of thy o fold_rev allify Ts) (Thm.prems_of th);
    5.17 +    val cTs = map (Thm.cterm_of ctxt o Free) Ts;
    5.18 +    val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th);
    5.19      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms;
    5.20    in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    5.21  
    5.22 @@ -82,7 +80,7 @@
    5.23        |> Drule.forall_elim_list tonames;
    5.24  
    5.25      (* make unconditional rule and prems *)
    5.26 -    val (uncond_rule, cprems) = allify_conditions (rev Ts') rule';
    5.27 +    val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule';
    5.28  
    5.29      (* using these names create lambda-abstracted version of the rule *)
    5.30      val abstractions = rev (Ts' ~~ tonames);
     6.1 --- a/src/Tools/eqsubst.ML	Tue Jun 02 09:10:05 2015 +0200
     6.2 +++ b/src/Tools/eqsubst.ML	Tue Jun 02 09:16:19 2015 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4      * term (* outer term *)
     6.5  
     6.6    type searchinfo =
     6.7 -    theory
     6.8 +    Proof.context
     6.9      * int (* maxidx *)
    6.10      * Zipper.T (* focusterm to search under *)
    6.11  
    6.12 @@ -67,7 +67,7 @@
    6.13    * term; (* outer term *)
    6.14  
    6.15  type searchinfo =
    6.16 -  theory
    6.17 +  Proof.context
    6.18    * int (* maxidx *)
    6.19    * Zipper.T; (* focusterm to search under *)
    6.20  
    6.21 @@ -138,8 +138,8 @@
    6.22    end;
    6.23  
    6.24  (* Unification with exception handled *)
    6.25 -(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
    6.26 -fun clean_unify thy ix (a as (pat, tgt)) =
    6.27 +(* given context, max var index, pat, tgt; returns Seq of instantiations *)
    6.28 +fun clean_unify ctxt ix (a as (pat, tgt)) =
    6.29    let
    6.30      (* type info will be re-derived, maybe this can be cached
    6.31         for efficiency? *)
    6.32 @@ -148,7 +148,7 @@
    6.33      (* FIXME is it OK to ignore the type instantiation info?
    6.34         or should I be using it? *)
    6.35      val typs_unify =
    6.36 -      SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix))
    6.37 +      SOME (Sign.typ_unify (Proof_Context.theory_of ctxt) (pat_ty, tgt_ty) (Vartab.empty, ix))
    6.38          handle Type.TUNIFY => NONE;
    6.39    in
    6.40      (case typs_unify of
    6.41 @@ -161,7 +161,7 @@
    6.42               Vartab.dest (Envir.term_env env));
    6.43            val initenv =
    6.44              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
    6.45 -          val useq = Unify.smash_unifiers (Context.Theory thy) [a] initenv
    6.46 +          val useq = Unify.smash_unifiers (Context.Proof ctxt) [a] initenv
    6.47              handle ListPair.UnequalLengths => Seq.empty
    6.48                | Term.TERM _ => Seq.empty;
    6.49            fun clean_unify' useq () =
    6.50 @@ -181,10 +181,10 @@
    6.51     bound variables. New names have been introduced to make sure they are
    6.52     unique w.r.t all names in the term and each other. usednames' is
    6.53     oldnames + new names. *)
    6.54 -fun clean_unify_z thy maxidx pat z =
    6.55 +fun clean_unify_z ctxt maxidx pat z =
    6.56    let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
    6.57      Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
    6.58 -      (clean_unify thy maxidx (t, pat))
    6.59 +      (clean_unify ctxt maxidx (t, pat))
    6.60    end;
    6.61  
    6.62  
    6.63 @@ -230,8 +230,8 @@
    6.64        end;
    6.65    in Zipper.lzy_search sf_valid_td_lr end;
    6.66  
    6.67 -fun searchf_unify_gen f (thy, maxidx, z) lhs =
    6.68 -  Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z);
    6.69 +fun searchf_unify_gen f (ctxt, maxidx, z) lhs =
    6.70 +  Seq.map (clean_unify_z ctxt maxidx lhs) (Zipper.limit_apply f z);
    6.71  
    6.72  (* search all unifications *)
    6.73  val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
    6.74 @@ -271,7 +271,7 @@
    6.75         o Zipper.mktop
    6.76         o Thm.prop_of) conclthm
    6.77    in
    6.78 -    ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
    6.79 +    ((cfvs, conclthm), (ctxt, maxidx, ft))
    6.80    end;
    6.81  
    6.82  (* substitute using an object or meta level equality *)
    6.83 @@ -345,23 +345,20 @@
    6.84      val th = Thm.incr_indexes 1 gth;
    6.85      val tgt_term = Thm.prop_of th;
    6.86  
    6.87 -    val thy = Thm.theory_of_thm th;
    6.88 -    val cert = Thm.global_cterm_of thy;
    6.89 -
    6.90      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
    6.91 -    val cfvs = rev (map cert fvs);
    6.92 +    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
    6.93  
    6.94      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
    6.95      val asm_nprems = length (Logic.strip_imp_prems asmt);
    6.96  
    6.97 -    val pth = Thm.trivial (cert asmt);
    6.98 +    val pth = Thm.trivial ((Thm.cterm_of ctxt) asmt);
    6.99      val maxidx = Thm.maxidx_of th;
   6.100  
   6.101      val ft =
   6.102        (Zipper.move_down_right (* trueprop *)
   6.103           o Zipper.mktop
   6.104           o Thm.prop_of) pth
   6.105 -  in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end;
   6.106 +  in ((cfvs, j, asm_nprems, pth), (ctxt, maxidx, ft)) end;
   6.107  
   6.108  (* prepare subst in every possible assumption *)
   6.109  fun prep_subst_in_asms ctxt i gth =
     7.1 --- a/src/Tools/misc_legacy.ML	Tue Jun 02 09:10:05 2015 +0200
     7.2 +++ b/src/Tools/misc_legacy.ML	Tue Jun 02 09:16:19 2015 +0200
     7.3 @@ -23,8 +23,8 @@
     7.4    val mk_defpair: term * term -> string * term
     7.5    val get_def: theory -> xstring -> thm
     7.6    val METAHYPS: Proof.context -> (thm list -> tactic) -> int -> tactic
     7.7 -  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
     7.8 -  val freeze_thaw: thm -> thm * (thm -> thm)
     7.9 +  val freeze_thaw_robust: Proof.context -> thm -> thm * (int -> thm -> thm)
    7.10 +  val freeze_thaw: Proof.context -> thm -> thm * (thm -> thm)
    7.11  end;
    7.12  
    7.13  structure Misc_Legacy: MISC_LEGACY =
    7.14 @@ -161,13 +161,12 @@
    7.15  fun metahyps_aux_tac ctxt tacf (prem,gno) state =
    7.16    let val (insts,params,hyps,concl) = metahyps_split_prem prem
    7.17        val maxidx = Thm.maxidx_of state
    7.18 -      val cterm = Thm.global_cterm_of (Thm.theory_of_thm state)
    7.19 -      val chyps = map cterm hyps
    7.20 +      val chyps = map (Thm.cterm_of ctxt) hyps
    7.21        val hypths = map Thm.assume chyps
    7.22        val subprems = map (Thm.forall_elim_vars 0) hypths
    7.23        val fparams = map Free params
    7.24 -      val cparams = map cterm fparams
    7.25 -      fun swap_ctpair (t,u) = (cterm u, cterm t)
    7.26 +      val cparams = map (Thm.cterm_of ctxt) fparams
    7.27 +      fun swap_ctpair (t, u) = apply2 (Thm.cterm_of ctxt) (u, t)
    7.28        (*Subgoal variables: make Free; lift type over params*)
    7.29        fun mk_subgoal_inst concl_vars (v, T) =
    7.30            if member (op =) concl_vars (v, T)
    7.31 @@ -175,12 +174,12 @@
    7.32            else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
    7.33        (*Instantiate subgoal vars by Free applied to params*)
    7.34        fun mk_ctpair (v, in_concl, u) =
    7.35 -          if in_concl then (cterm (Var v), cterm u)
    7.36 -          else (cterm (Var v), cterm (list_comb (u, fparams)))
    7.37 +          if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u)
    7.38 +          else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams))
    7.39        (*Restore Vars with higher type and index*)
    7.40        fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
    7.41 -          if in_concl then (cterm u, cterm (Var ((a, i), T)))
    7.42 -          else (cterm u, cterm (Var ((a, i + maxidx), U)))
    7.43 +          if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T))
    7.44 +          else apply2 (Thm.cterm_of ctxt) (u, Var ((a, i + maxidx), U))
    7.45        (*Embed B in the original context of params and hyps*)
    7.46        fun embed B = fold_rev Logic.all fparams (Logic.list_implies (hyps, B))
    7.47        (*Strip the context using elimination rules*)
    7.48 @@ -193,7 +192,7 @@
    7.49              and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
    7.50              val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
    7.51              val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
    7.52 -            val emBs = map (cterm o embed) (Thm.prems_of st')
    7.53 +            val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st')
    7.54              val Cth  = implies_elim_list st' (map (elim o Thm.assume) emBs)
    7.55          in  (*restore the unknowns to the hypotheses*)
    7.56              free_instantiate (map swap_ctpair insts @
    7.57 @@ -206,7 +205,7 @@
    7.58        fun next st =
    7.59          Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
    7.60            (false, relift st, Thm.nprems_of st) gno state
    7.61 -  in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
    7.62 +  in Seq.maps next (tacf subprems (Thm.trivial (Thm.cterm_of ctxt concl))) end;
    7.63  
    7.64  fun print_vars_terms ctxt n thm =
    7.65    let
    7.66 @@ -255,9 +254,8 @@
    7.67  (*Convert all Vars in a theorem to Frees.  Also return a function for
    7.68    reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
    7.69  
    7.70 -fun freeze_thaw_robust th =
    7.71 +fun freeze_thaw_robust ctxt th =
    7.72   let val fth = Thm.legacy_freezeT th
    7.73 -     val thy = Thm.theory_of_thm fth
    7.74   in
    7.75     case Thm.fold_terms Term.add_vars fth [] of
    7.76         [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
    7.77 @@ -265,8 +263,8 @@
    7.78           let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
    7.79               val alist = map newName vars
    7.80               fun mk_inst (v,T) =
    7.81 -                 (Thm.global_cterm_of thy (Var(v,T)),
    7.82 -                  Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
    7.83 +                 apply2 (Thm.cterm_of ctxt)
    7.84 +                  (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
    7.85               val insts = map mk_inst vars
    7.86               fun thaw i th' = (*i is non-negative increment for Var indexes*)
    7.87                   th' |> forall_intr_list (map #2 insts)
    7.88 @@ -276,9 +274,8 @@
    7.89  
    7.90  (*Basic version of the function above. No option to rename Vars apart in thaw.
    7.91    The Frees created from Vars have nice names.*)
    7.92 -fun freeze_thaw th =
    7.93 +fun freeze_thaw ctxt th =
    7.94   let val fth = Thm.legacy_freezeT th
    7.95 -     val thy = Thm.theory_of_thm fth
    7.96   in
    7.97     case Thm.fold_terms Term.add_vars fth [] of
    7.98         [] => (fth, fn x => x)
    7.99 @@ -289,8 +286,7 @@
   7.100               val (alist, _) =
   7.101                   fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
   7.102               fun mk_inst (v, T) =
   7.103 -                 (Thm.global_cterm_of thy (Var(v,T)),
   7.104 -                  Thm.global_cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   7.105 +                apply2 (Thm.cterm_of ctxt) (Var (v, T), Free (the (AList.lookup (op =) alist v), T))
   7.106               val insts = map mk_inst vars
   7.107               fun thaw th' =
   7.108                   th' |> forall_intr_list (map #2 insts)
   7.109 @@ -299,4 +295,3 @@
   7.110   end;
   7.111  
   7.112  end;
   7.113 -