# HG changeset patch # User wenzelm # Date 1433235782 -7200 # Node ID befdc10ebb4299d388dfae0f79a86f4a36338025 # Parent 88505460fde7a89e9fecb71812ae2f660d82bb9e clarified context; diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Tue Jun 02 11:03:02 2015 +0200 @@ -591,7 +591,7 @@ val monos = Inductive.get_monos ctxt; val intrs' = Inductive.unpartition_rules intrs (map (fn (((s, ths), (_, k)), th) => - (s, ths ~~ Inductive.infer_intro_vars th k ths)) + (s, ths ~~ Inductive.infer_intro_vars thy th k ths)) (Inductive.partition_rules raw_induct intrs ~~ Inductive.arities_of raw_induct ~~ elims)); val k = length (Inductive.params_of raw_induct); diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Jun 02 11:03:02 2015 +0200 @@ -1449,7 +1449,7 @@ (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss) |> K |> Goal.prove_sorry lthy [] [] goal |> Thm.close_derivation - |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule))) + |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule))) @{thms eqTrueE eq_False[THEN iffD1] notnotD} |> pair eqn_pos |> single diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Tue Jun 02 11:03:02 2015 +0200 @@ -11,7 +11,7 @@ val trace : bool Config.T val max_clauses : int Config.T val term_pair_of: indexname * (typ * 'a) -> term * 'a - val first_order_resolve : thm -> thm -> thm + val first_order_resolve : Proof.context -> thm -> thm -> thm val size_of_subgoals: thm -> int val has_too_many_clauses: Proof.context -> term -> bool val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context @@ -98,16 +98,16 @@ fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); (*FIXME: currently does not "rename variables apart"*) -fun first_order_resolve thA thB = +fun first_order_resolve ctxt thA thB = (case try (fn () => - let val thy = Thm.theory_of_thm thA + let val thy = Proof_Context.theory_of ctxt val tmA = Thm.concl_of thA val Const(@{const_name Pure.imp},_) $ tmB $ _ = Thm.prop_of thB val tenv = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) |> snd - val ct_pairs = map (apply2 (Thm.global_cterm_of thy) o term_pair_of) (Vartab.dest tenv) + val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv) in thA RS (cterm_instantiate ct_pairs thB) end) () of SOME th => th | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) @@ -359,11 +359,10 @@ in (th RS spec', ctxt') end end; -fun apply_skolem_theorem (th, rls) = +fun apply_skolem_theorem ctxt (th, rls) = let fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) - | tryall (rl :: rls) = - first_order_resolve th rl handle THM _ => tryall rls + | tryall (rl :: rls) = first_order_resolve ctxt th rl handle THM _ => tryall rls in tryall rls end (* Conjunctive normal form, adding clauses from th in front of ths (for foldr). @@ -383,7 +382,7 @@ in ctxt_ref := ctxt'; cnf_aux (th', ths) end | Const (@{const_name Ex}, _) => (*existential quantifier: Insert Skolem functions*) - cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) + cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths) | Const (@{const_name HOL.disj}, _) => (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using all combinations of converting P, Q to CNF.*) diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Jun 02 11:03:02 2015 +0200 @@ -85,7 +85,7 @@ (case add_vars_and_frees u [] of [] => Conv.abs_conv (conv false o snd) ctxt ct - |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) + |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI}) | v :: _ => Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v |> Thm.cterm_of ctxt diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Tools/choice_specification.ML Tue Jun 02 11:03:02 2015 +0200 @@ -140,7 +140,7 @@ val cT = Thm.ctyp_of_cterm cv val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec in thm RS spec' end - fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm + fun remove_alls frees (thm, thy) = (fold (inst_all thy) frees thm, thy) fun process_single ((name, atts), rew_imp, frees) args = let fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm @@ -152,7 +152,7 @@ Global_Theory.store_thm (Binding.name name, thm) thy) in swap args - |> apfst (remove_alls frees) + |> remove_alls frees |> apfst undo_imps |> apfst Drule.export_without_context |-> Thm.theory_attributes diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Tools/inductive.ML Tue Jun 02 11:03:02 2015 +0200 @@ -65,7 +65,7 @@ val partition_rules: thm -> thm list -> (string * thm list) list val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list val unpartition_rules: thm list -> (string * 'a list) list -> 'a list - val infer_intro_vars: thm -> int -> thm list -> term list list + val infer_intro_vars: theory -> thm -> int -> thm list -> term list list end; signature INDUCTIVE = @@ -1132,9 +1132,8 @@ (fn x :: xs => (x, xs)) #>> the) intros xs |> fst; (* infer order of variables in intro rules from order of quantifiers in elim rule *) -fun infer_intro_vars elim arity intros = +fun infer_intro_vars thy elim arity intros = let - val thy = Thm.theory_of_thm elim; val _ :: cases = Thm.prems_of elim; val used = map (fst o fst) (Term.add_vars (Thm.prop_of elim) []); fun mtch (t, u) = diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 02 11:03:02 2015 +0200 @@ -19,9 +19,9 @@ [name] => name | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm])); -fun prf_of thm = +fun prf_of thy thm = Reconstruct.proof_of thm - |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *) + |> Reconstruct.expand_proof thy [("", NONE)]; (* FIXME *) fun subsets [] = [[]] | subsets (x::xs) = @@ -268,7 +268,7 @@ if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt, Extraction.abs_corr_shyps thy rule vs vs2 (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz) - (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule))))) + (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule))))) end; fun rename tab = map (fn x => the_default x (AList.lookup op = tab x)); @@ -285,7 +285,7 @@ val params' = map dest_Var params; val rss = Inductive.partition_rules raw_induct intrs; val rss' = map (fn (((s, rs), (_, arity)), elim) => - (s, (Inductive.infer_intro_vars elim arity rs ~~ rs))) + (s, (Inductive.infer_intro_vars thy elim arity rs ~~ rs))) (rss ~~ arities ~~ elims); val (prfx, _) = split_last (Long_Name.explode (fst (hd rss))); val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets; diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/HOL/Tools/split_rule.ML Tue Jun 02 11:03:02 2015 +0200 @@ -39,12 +39,11 @@ | ap_split _ T3 u = u; (*Curries any Var of function type in the rule*) -fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl = +fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl = let val T' = HOLogic.flatten_tupleT T1 ---> T2; val newt = ap_split T1 T2 (Var (v, T')); - val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl); - in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end - | split_rule_var' _ rl = rl; + in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end + | split_rule_var' _ _ rl = rl; (* complete splitting of partially split rules *) @@ -85,11 +84,11 @@ fun split_rule_var ctxt = - (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var'; + (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var' ctxt; (*curries ALL function variables occurring in a rule's conclusion*) fun split_rule ctxt rl = - fold_rev split_rule_var' (Misc_Legacy.term_vars (Thm.concl_of rl)) rl + fold_rev (split_rule_var' ctxt) (Misc_Legacy.term_vars (Thm.concl_of rl)) rl |> remove_internal_split ctxt |> Drule.export_without_context; diff -r 88505460fde7 -r befdc10ebb42 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Tue Jun 02 10:12:46 2015 +0200 +++ b/src/Provers/splitter.ML Tue Jun 02 11:03:02 2015 +0200 @@ -285,9 +285,8 @@ call split_posns with appropriate parameters *************************************************************) -fun select cmap state i = +fun select thy cmap state i = let - val thy = Thm.theory_of_thm state val goal = Thm.term_of (Thm.cprem_of state i); val Ts = rev (map #2 (Logic.strip_params goal)); val _ $ t $ _ = Logic.strip_assums_concl goal; @@ -313,16 +312,14 @@ i : no. of subgoal **************************************************************) -fun inst_lift Ts t (T, U, pos) state i = +fun inst_lift ctxt Ts t (T, U, pos) state i = let - val cert = Thm.global_cterm_of (Thm.theory_of_thm state); val (cntxt, u) = mk_cntxt t pos (T --> U); val trlift' = Thm.lift_rule (Thm.cprem_of state i) (Thm.rename_boundvars abs_lift u trlift); val (P, _) = strip_comb (fst (Logic.dest_equals (Logic.strip_assums_concl (Thm.prop_of trlift')))); - in cterm_instantiate [(cert P, cert (abss Ts cntxt))] trlift' - end; + in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] trlift' end; (************************************************************* @@ -338,15 +335,13 @@ i : number of subgoal **************************************************************) -fun inst_split Ts t tt thm TB state i = +fun inst_split ctxt Ts t tt thm TB state i = let val thm' = Thm.lift_rule (Thm.cprem_of state i) thm; val (P, _) = strip_comb (fst (Logic.dest_equals (Logic.strip_assums_concl (Thm.prop_of thm')))); - val cert = Thm.global_cterm_of (Thm.theory_of_thm state); val cntxt = mk_cntxt_splitthm t tt TB; - in cterm_instantiate [(cert P, cert (abss Ts cntxt))] thm' - end; + in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] thm' end; (***************************************************************************** @@ -359,14 +354,15 @@ fun split_tac _ [] i = no_tac | split_tac ctxt splits i = let val cmap = cmap_of_split_thms splits - fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift Ts t p st i, 2) i st + fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift ctxt Ts t p st i, 2) i st fun lift_split_tac state = - let val (Ts, t, splits) = select cmap state i + let val (Ts, t, splits) = select (Proof_Context.theory_of ctxt) cmap state i in case splits of [] => no_tac state | (thm, apsns, pos, TB, tt)::_ => (case apsns of - [] => compose_tac ctxt (false, inst_split Ts t tt thm TB state i, 0) i state + [] => + compose_tac ctxt (false, inst_split ctxt Ts t tt thm TB state i, 0) i state | p::_ => EVERY [lift_tac Ts t p, resolve_tac ctxt [reflexive_thm] (i+1), lift_split_tac] state)