--- a/src/FOL/simpdata.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/FOL/simpdata.ML Tue Jul 28 23:29:13 2015 +0200
@@ -50,8 +50,7 @@
| _ => [th])
in atoms end;
-fun mksimps pairs ctxt =
- map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt);
+fun mksimps pairs ctxt = map mk_eq o mk_atomize pairs o Variable.gen_all ctxt;
(** make simplification procedures for quantifier elimination **)
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Jul 28 23:29:13 2015 +0200
@@ -206,7 +206,7 @@
val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
val postcv = Simplifier.rewrite (put_simpset ss ctxt);
val nnf = K (nnf_conv ctxt then_conv postcv)
- val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Thm.add_cterm_frees tm [])
+ val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Drule.cterm_add_frees tm [])
(isolate_conv ctxt) nnf
(fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
whatis = whatis, simpset = ss}) vs
--- a/src/HOL/Decision_Procs/langford.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Tue Jul 28 23:29:13 2015 +0200
@@ -191,7 +191,7 @@
in
fn p =>
Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
- (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+ (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
(K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
end;
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue Jul 28 23:29:13 2015 +0200
@@ -900,9 +900,9 @@
then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
else raise Failure "substitutable_monomial"
| @{term "op + :: real => _"}$_$_ =>
- (substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
+ (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
handle Failure _ =>
- substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
+ substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
| _ => raise Failure "substitutable_monomial")
fun isolate_variable v th =
--- a/src/HOL/Library/old_recdef.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Tue Jul 28 23:29:13 2015 +0200
@@ -2625,7 +2625,8 @@
fun simplify_defn ctxt strict congs wfs pats def0 =
let
- val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
+ val thy = Proof_Context.theory_of ctxt;
+ val def = Thm.unvarify_global thy def0 RS meta_eq_to_obj_eq
val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
val {lhs=f,rhs} = USyntax.dest_eq (concl def)
val (_,[R,_]) = USyntax.strip_comb rhs
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Jul 28 23:29:13 2015 +0200
@@ -800,7 +800,7 @@
fun make_sel_thm xs' case_thm sel_def =
zero_var_indexes
- (Drule.gen_all (Variable.maxidx_of lthy)
+ (Variable.gen_all lthy
(Drule.rename_bvars'
(map (SOME o fst) xs')
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Tue Jul 28 23:29:13 2015 +0200
@@ -27,7 +27,7 @@
let
val thms as thm1 :: _ = raw_thms
|> Conjunction.intr_balanced
- |> Thm.unvarify_global
+ |> Thm.unvarify_global thy
|> Conjunction.elim_balanced (length raw_thms)
|> map Simpdata.mk_meta_eq
|> map Drule.zero_var_indexes;
@@ -53,7 +53,7 @@
fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
- val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
+ val monomorphic_prop_of = Thm.prop_of o Thm.unvarify_global thy o Drule.zero_var_indexes;
fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
--- a/src/HOL/Tools/Qelim/qelim.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Tue Jul 28 23:29:13 2015 +0200
@@ -65,7 +65,7 @@
fun standard_qelim_conv ctxt atcv ncv qcv p =
let val pcv = pcv ctxt
- in gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p end
+ in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
end;
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Tue Jul 28 23:29:13 2015 +0200
@@ -35,12 +35,13 @@
fun find_unused_assms ctxt thy_name =
let
+ val thy = Proof_Context.theory_of ctxt
val ctxt' = ctxt
|> Config.put Quickcheck.abort_potential true
|> Config.put Quickcheck.quiet true
val all_thms =
filter (fn (s, _) => length (Long_Name.explode s) = 2) (* FIXME !? *)
- (thms_of (Proof_Context.theory_of ctxt) thy_name)
+ (thms_of thy thy_name)
fun check_single conjecture =
(case try (Quickcheck.test_terms ctxt' (true, true) []) [(conjecture, [])] of
SOME (SOME _) => false
@@ -53,7 +54,7 @@
if member (op =) S x then I
else insert (eq_set (op =)) (insert (op =) x S)) X) Ss []
fun check (s, th) =
- (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global th)) of
+ (case Logic.strip_horn (Thm.prop_of (Thm.unvarify_global thy th)) of
([], _) => (s, NONE)
| (ts, t) =>
let
--- a/src/HOL/Tools/choice_specification.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Tue Jul 28 23:29:13 2015 +0200
@@ -178,7 +178,7 @@
else ()
in
arg
- |> apsnd Thm.unvarify_global
+ |> apsnd (Thm.unvarify_global thy)
|> process_all (zip3 alt_names rew_imps frees)
end
--- a/src/HOL/Tools/datatype_realizer.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Jul 28 23:29:13 2015 +0200
@@ -147,7 +147,7 @@
| _ => AbsP ("H", SOME p, prf)))
(rec_fns ~~ Thm.prems_of thm)
(Proofterm.proof_combP
- (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+ (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
@@ -212,10 +212,10 @@
(AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
(Proofterm.proof_combP
- (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
+ (Reconstruct.proof_of thy' thm', map PBound (length prems - 1 downto 0))));
val prf' =
Extraction.abs_corr_shyps thy' exhaust []
- (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
+ (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of thy' exhaust);
val r' =
Logic.varify_global (Abs ("y", T,
(fold_rev (Term.abs o dest_Free) rs
--- a/src/HOL/Tools/groebner.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/groebner.ML Tue Jul 28 23:29:13 2015 +0200
@@ -532,7 +532,7 @@
fun simp_ex_conv ctxt =
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
-fun frees t = Thm.add_cterm_frees t [];
+fun frees t = Drule.cterm_add_frees t [];
fun free_in v t = member op aconvc (frees t) v;
val vsubst = let
@@ -741,7 +741,7 @@
Thm.apply
(Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
@{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
- val avs = Thm.add_cterm_frees tm []
+ val avs = Drule.cterm_add_frees tm []
val P' = fold mk_forall avs tm
val th1 = initial_conv ctxt (mk_neg P')
val (evs,bod) = strip_exists(concl th1) in
@@ -797,7 +797,7 @@
val mons = striplist(dest_binary ring_add_tm) t
in member (op aconvc) mons v andalso
forall (fn m => v aconvc m
- orelse not(member (op aconvc) (Thm.add_cterm_frees m []) v)) mons
+ orelse not(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons
end
fun isolate_variable vars tm =
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 28 23:29:13 2015 +0200
@@ -20,7 +20,7 @@
| _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
fun prf_of thy thm =
- Reconstruct.proof_of thm
+ Reconstruct.proof_of thy thm
|> Reconstruct.expand_proof thy [("", NONE)]; (* FIXME *)
fun subsets [] = [[]]
--- a/src/HOL/Tools/simpdata.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/HOL/Tools/simpdata.ML Tue Jul 28 23:29:13 2015 +0200
@@ -112,8 +112,7 @@
end;
in atoms end;
-fun mksimps pairs ctxt =
- map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt);
+fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Variable.gen_all ctxt;
fun unsafe_solver_tac ctxt =
let
--- a/src/Provers/classical.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Provers/classical.ML Tue Jul 28 23:29:13 2015 +0200
@@ -147,6 +147,7 @@
fun classical_rule ctxt rule =
if is_some (Object_Logic.elim_concl ctxt rule) then
let
+ val thy = Proof_Context.theory_of ctxt;
val rule' = rule RS Data.classical;
val concl' = Thm.concl_of rule';
fun redundant_hyp goal =
@@ -161,7 +162,7 @@
else all_tac))
|> Seq.hd
|> Drule.zero_var_indexes;
- in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
+ in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end
else rule;
(*flatten nested meta connectives in prems*)
--- a/src/Pure/Isar/class.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/class.ML Tue Jul 28 23:29:13 2015 +0200
@@ -748,7 +748,7 @@
fun intro_classes_tac ctxt facts st =
let
- val thy = Thm.theory_of_thm st;
+ val thy = Proof_Context.theory_of ctxt;
val classes = Sign.all_classes thy;
val class_trivs = map (Thm.class_triv thy) classes;
val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes;
--- a/src/Pure/Isar/local_defs.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML Tue Jul 28 23:29:13 2015 +0200
@@ -129,30 +129,23 @@
--------------
B as
*)
-fun export inner outer = (*beware of closure sizes*)
+fun export inner outer th =
let
- val exp = Assumption.export false inner outer;
- val exp_term = Assumption.export_term inner outer;
- val asms = Assumption.local_assms_of inner outer;
- in
- fn th =>
- let
- val th' = exp th;
- val defs_asms = asms
- |> filter_out (Drule.is_sort_constraint o Thm.term_of)
- |> map (Thm.assume #> (fn asm =>
- (case try (head_of_def o Thm.prop_of) asm of
- NONE => (asm, false)
- | SOME x =>
- let val t = Free x in
- (case try exp_term t of
- NONE => (asm, false)
- | SOME u =>
- if t aconv u then (asm, false)
- else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
- end)));
- in (apply2 (map #1) (List.partition #2 defs_asms), th') end
- end;
+ val defs_asms =
+ Assumption.local_assms_of inner outer
+ |> filter_out (Drule.is_sort_constraint o Thm.term_of)
+ |> map (Thm.assume #> (fn asm =>
+ (case try (head_of_def o Thm.prop_of) asm of
+ NONE => (asm, false)
+ | SOME x =>
+ let val t = Free x in
+ (case try (Assumption.export_term inner outer) t of
+ NONE => (asm, false)
+ | SOME u =>
+ if t aconv u then (asm, false)
+ else (Drule.abs_def (Variable.gen_all outer asm), true))
+ end)));
+ in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
(*
[xs, xs == as]
--- a/src/Pure/Isar/object_logic.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML Tue Jul 28 23:29:13 2015 +0200
@@ -203,7 +203,7 @@
fun gen_rulify full ctxt =
Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
- #> Drule.gen_all (Variable.maxidx_of ctxt)
+ #> Variable.gen_all ctxt
#> Thm.strip_shyps
#> Drule.zero_var_indexes;
--- a/src/Pure/Isar/proof.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jul 28 23:29:13 2015 +0200
@@ -501,7 +501,7 @@
(Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
handle THM _ => err_lost ())
|> Drule.flexflex_unique (SOME ctxt)
- |> Thm.check_shyps (Variable.sorts_of ctxt)
+ |> Thm.check_shyps ctxt (Variable.sorts_of ctxt)
|> Thm.check_hyps (Context.Proof ctxt);
val goal_propss = filter_out null propss;
--- a/src/Pure/Proof/extraction.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Jul 28 23:29:13 2015 +0200
@@ -769,9 +769,9 @@
| extr d vs ts Ts hs _ defs = error "extr: bad proof";
- fun prep_thm vs thm =
+ fun prep_thm vs raw_thm =
let
- val thy = Thm.theory_of_thm thm;
+ val thm = Thm.transfer thy raw_thm;
val prop = Thm.prop_of thm;
val prf = Thm.proof_of thm;
val name = Thm.derivation_name thm;
--- a/src/Pure/Proof/proof_syntax.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 28 23:29:13 2015 +0200
@@ -14,7 +14,7 @@
val read_term: theory -> bool -> typ -> string -> term
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
val proof_syntax: Proofterm.proof -> theory -> theory
- val proof_of: bool -> thm -> Proofterm.proof
+ val proof_of: theory -> bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
@@ -235,9 +235,9 @@
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
end;
-fun proof_of full thm =
+fun proof_of thy full raw_thm =
let
- val thy = Thm.theory_of_thm thm;
+ val thm = Thm.transfer thy raw_thm;
val prop = Thm.full_prop_of thm;
val prf = Thm.proof_of thm;
val prf' =
@@ -253,6 +253,6 @@
(term_of_proof prf);
fun pretty_proof_of ctxt full th =
- pretty_proof ctxt (proof_of full th);
+ pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th);
end;
--- a/src/Pure/Proof/reconstruct.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Jul 28 23:29:13 2015 +0200
@@ -10,7 +10,7 @@
val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
- val proof_of : thm -> Proofterm.proof
+ val proof_of : theory -> thm -> Proofterm.proof
val expand_proof : theory -> (string * term option) list ->
Proofterm.proof -> Proofterm.proof
end;
@@ -324,8 +324,9 @@
val prop_of' = Envir.beta_eta_contract oo prop_of0;
val prop_of = prop_of' [];
-fun proof_of thm =
- reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+fun proof_of thy raw_thm =
+ let val thm = Thm.transfer thy raw_thm
+ in reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm) end;
--- a/src/Pure/conjunction.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/conjunction.ML Tue Jul 28 23:29:13 2015 +0200
@@ -76,8 +76,7 @@
val A_B = read_prop "A &&& B";
val conjunction_def =
- Thm.unvarify_global
- (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
+ Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def";
fun conjunctionD which =
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
@@ -138,8 +137,13 @@
local
-fun conjs thy n =
- let val As = map (fn A => Thm.global_cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
+val bootstrap_thy = Context.theory_of (Context.the_thread_data ());
+
+fun conjs n =
+ let
+ val As =
+ map (fn A => Thm.global_cterm_of bootstrap_thy (Free (A, propT)))
+ (Name.invent Name.context "A" n);
in (As, mk_conjunction_balanced As) end;
val B = read_prop "B";
@@ -159,8 +163,7 @@
if n < 2 then th
else
let
- val thy = Thm.theory_of_thm th;
- val (As, C) = conjs thy n;
+ val (As, C) = conjs n;
val D = Drule.mk_implies (C, B);
in
comp_rule th
@@ -177,8 +180,7 @@
if n < 2 then th
else
let
- val thy = Thm.theory_of_thm th;
- val (As, C) = conjs thy n;
+ val (As, C) = conjs n;
val D = Drule.list_implies (As, B);
in
comp_rule th
--- a/src/Pure/drule.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/drule.ML Tue Jul 28 23:29:13 2015 +0200
@@ -16,7 +16,6 @@
val forall_intr_list: cterm list -> thm -> thm
val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
- val gen_all: int -> thm -> thm
val lift_all: Proof.context -> cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
@@ -53,6 +52,7 @@
signature DRULE =
sig
include BASIC_DRULE
+ val outer_params: term -> (string * typ) list
val generalize: string list * string list -> thm -> thm
val list_comb: cterm * cterm list -> cterm
val strip_comb: cterm -> cterm * cterm list
@@ -91,6 +91,8 @@
val mk_term: cterm -> thm
val dest_term: thm -> cterm
val cterm_rule: (thm -> thm) -> cterm -> cterm
+ val cterm_add_frees: cterm -> cterm list -> cterm list
+ val cterm_add_vars: cterm -> cterm list -> cterm list
val dummy_thm: thm
val is_sort_constraint: term -> bool
val sort_constraintI: thm
@@ -174,24 +176,12 @@
val forall_intr_list = fold_rev Thm.forall_intr;
(*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th =
- fold Thm.forall_intr
- (map (Thm.global_cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
+fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th;
fun outer_params t =
let val vs = Term.strip_all_vars t
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
-(*generalize outermost parameters*)
-fun gen_all maxidx0 th =
- let
- val thy = Thm.theory_of_thm th;
- val maxidx = Thm.maxidx_thm th maxidx0;
- val prop = Thm.prop_of th;
- fun elim (x, T) =
- Thm.forall_elim (Thm.global_cterm_of thy (Var ((x, maxidx + 1), T)));
- in fold elim (outer_params prop) th end;
-
(*lift vars wrt. outermost goal parameters
-- reverses the effect of gen_all modulo higher-order unification*)
fun lift_all ctxt raw_goal raw_th =
@@ -576,7 +566,7 @@
local
val A = certify (Free ("A", propT));
- val axiom = Thm.unvarify_global o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
+ val axiom = Thm.unvarify_axiom (Context.the_theory (Context.the_thread_data ()));
val prop_def = axiom "Pure.prop_def";
val term_def = axiom "Pure.term_def";
val sort_constraint_def = axiom "Pure.sort_constraint_def";
@@ -631,6 +621,9 @@
fun cterm_rule f = dest_term o f o mk_term;
+val cterm_add_frees = Thm.add_frees o mk_term;
+val cterm_add_vars = Thm.add_vars o mk_term;
+
val dummy_thm = mk_term (certify Term.dummy_prop);
@@ -647,7 +640,7 @@
store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
- (Thm.unvarify_global sort_constraintI)))
+ (Thm.unvarify_global (Context.the_theory (Context.the_thread_data ())) sort_constraintI)))
(implies_intr_list [A, C] (Thm.assume A)));
end;
--- a/src/Pure/goal.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/goal.ML Tue Jul 28 23:29:13 2015 +0200
@@ -214,7 +214,7 @@
val res =
(finish ctxt' st
|> Drule.flexflex_unique (SOME ctxt')
- |> Thm.check_shyps sorts
+ |> Thm.check_shyps ctxt' sorts
|> Thm.check_hyps (Context.Proof ctxt'))
handle THM (msg, _, _) => err msg | ERROR msg => err msg;
in
--- a/src/Pure/more_thm.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/more_thm.ML Tue Jul 28 23:29:13 2015 +0200
@@ -21,7 +21,8 @@
structure Ctermtab: TABLE
structure Thmtab: TABLE
val aconvc: cterm * cterm -> bool
- val add_cterm_frees: cterm -> cterm list -> cterm list
+ val add_frees: thm -> cterm list -> cterm list
+ val add_vars: thm -> cterm list -> cterm list
val all_name: string * cterm -> cterm -> cterm
val all: cterm -> cterm -> cterm
val mk_binop: cterm -> cterm -> cterm -> cterm
@@ -39,10 +40,10 @@
val eq_thm: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
val eq_thm_strict: thm * thm -> bool
- val equiv_thm: thm * thm -> bool
+ val equiv_thm: theory -> thm * thm -> bool
val class_triv: theory -> class -> thm
val of_sort: ctyp * sort -> thm list
- val check_shyps: sort list -> thm -> thm
+ val check_shyps: Proof.context -> sort list -> thm -> thm
val is_dummy: thm -> bool
val plain_prop_of: thm -> term
val add_thm: thm -> thm list -> thm list
@@ -62,7 +63,8 @@
val forall_elim_vars: int -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
val forall_intr_frees: thm -> thm
- val unvarify_global: thm -> thm
+ val unvarify_global: theory -> thm -> thm
+ val unvarify_axiom: theory -> string -> thm
val close_derivation: thm -> thm
val rename_params_rule: string list * int -> thm -> thm
val rename_boundvars: term -> term -> thm -> thm
@@ -112,13 +114,8 @@
val op aconvc = op aconv o apply2 Thm.term_of;
-fun add_cterm_frees ct =
- let
- val thy = Thm.theory_of_cterm ct;
- val t = Thm.term_of ct;
- in
- Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t
- end;
+val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
+val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
(* cterm constructors and destructors *)
@@ -209,8 +206,8 @@
(* pattern equivalence *)
-fun equiv_thm ths =
- Pattern.equiv (Theory.merge (apply2 Thm.theory_of_thm ths)) (apply2 Thm.full_prop_of ths);
+fun equiv_thm thy ths =
+ Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths);
(* type classes and sorts *)
@@ -220,15 +217,14 @@
fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
-fun check_shyps sorts raw_th =
+fun check_shyps ctxt sorts raw_th =
let
val th = Thm.strip_shyps raw_th;
- val prt_sort = Syntax.pretty_sort_global (Thm.theory_of_thm th);
val pending = Sorts.subtract sorts (Thm.extra_shyps th);
in
if null pending then th
else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
- Pretty.brk 1 :: Pretty.commas (map prt_sort pending))))
+ Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) pending))))
end;
@@ -369,20 +365,20 @@
fun forall_intr_frees th =
let
- val thy = Thm.theory_of_thm th;
val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
- val frees = Term.fold_aterms (fn Free v =>
- if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
- in fold (Thm.forall_intr o Thm.global_cterm_of thy o Free) frees th end;
+ val frees =
+ Thm.fold_atomic_cterms (fn a =>
+ (case Thm.term_of a of
+ Free v => not (member (op =) fixed v) ? insert (op aconvc) a
+ | _ => I)) th [];
+ in fold Thm.forall_intr frees th end;
(* unvarify_global: global schematic variables *)
-fun unvarify_global th =
+fun unvarify_global thy th =
let
- val thy = Thm.theory_of_thm th;
-
val prop = Thm.full_prop_of th;
val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
handle TERM (msg, _) => raise THM (msg, 0, [th]);
@@ -393,6 +389,8 @@
in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
+fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
+
(* close_derivation *)
@@ -462,7 +460,7 @@
val axm' = Thm.axiom thy' axm_name;
val thm =
Thm.instantiate (recover, []) axm'
- |> unvarify_global
+ |> unvarify_global thy'
|> fold elim_implies of_sorts;
in ((axm_name, thm), thy') end;
@@ -479,7 +477,7 @@
val axm' = Thm.axiom thy' axm_name;
val thm =
Thm.instantiate (recover, []) axm'
- |> unvarify_global
+ |> unvarify_global thy'
|> fold_rev Thm.implies_intr prems;
in ((axm_name, thm), thy') end;
--- a/src/Pure/raw_simplifier.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/raw_simplifier.ML Tue Jul 28 23:29:13 2015 +0200
@@ -1385,7 +1385,7 @@
Conv.fconv_rule
(rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
|> Thm.adjust_maxidx_thm ~1
- |> Drule.gen_all (Variable.maxidx_of ctxt);
+ |> Variable.gen_all ctxt;
val hhf_ss =
simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
--- a/src/Pure/skip_proof.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/skip_proof.ML Tue Jul 28 23:29:13 2015 +0200
@@ -38,6 +38,6 @@
(* cheat_tac *)
fun cheat_tac ctxt i st =
- resolve_tac ctxt [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
+ resolve_tac ctxt [make_thm (Proof_Context.theory_of ctxt) (Var (("A", 0), propT))] i st;
end;
--- a/src/Pure/thm.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/thm.ML Tue Jul 28 23:29:13 2015 +0200
@@ -69,6 +69,7 @@
tpairs: (cterm * cterm) list,
prop: cterm}
val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
+ val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
val terms_of_tpairs: (term * term) list -> term list
val full_prop_of: thm -> term
val theory_of_thm: thm -> theory
@@ -366,6 +367,15 @@
fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
+fun fold_atomic_cterms f (th as Thm (_, {thy, maxidx, shyps, ...})) =
+ let fun cterm t T = Cterm {thy = thy, t = t, T = T, maxidx = maxidx, sorts = shyps} in
+ (fold_terms o fold_aterms)
+ (fn t as Const (_, T) => f (cterm t T)
+ | t as Free (_, T) => f (cterm t T)
+ | t as Var (_, T) => f (cterm t T)
+ | _ => I) th
+ end;
+
fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
--- a/src/Pure/variable.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Pure/variable.ML Tue Jul 28 23:29:13 2015 +0200
@@ -59,6 +59,7 @@
val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
val variant_fixes: string list -> Proof.context -> string list * Proof.context
val dest_fixes: Proof.context -> (string * string) list
+ val gen_all: Proof.context -> thm -> thm
val export_terms: Proof.context -> Proof.context -> term list -> term list
val exportT_terms: Proof.context -> Proof.context -> term list -> term list
val exportT: Proof.context -> Proof.context -> thm list -> thm list
@@ -497,6 +498,12 @@
(** export -- generalize type/term variables (beware of closure sizes) **)
+fun gen_all ctxt th =
+ let
+ val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1;
+ fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T)));
+ in fold gen (Drule.outer_params (Thm.prop_of th)) th end;
+
fun export_inst inner outer =
let
val declared_outer = is_declared outer;
--- a/src/Sequents/simpdata.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/Sequents/simpdata.ML Tue Jul 28 23:29:13 2015 +0200
@@ -71,8 +71,7 @@
setSSolver (mk_solver "safe" safe_solver)
setSolver (mk_solver "unsafe" unsafe_solver)
|> Simplifier.set_subgoaler asm_simp_tac
- |> Simplifier.set_mksimps (fn ctxt =>
- map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt))
+ |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt)
|> Simplifier.set_mkcong mk_meta_cong
|> simpset_of;
--- a/src/ZF/Main_ZF.thy Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/Main_ZF.thy Tue Jul 28 23:29:13 2015 +0200
@@ -72,7 +72,7 @@
declaration \<open>fn _ =>
Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
- map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
+ map mk_eq o Ord_atomize o Variable.gen_all ctxt))
\<close>
end
--- a/src/ZF/OrdQuant.thy Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/OrdQuant.thy Tue Jul 28 23:29:13 2015 +0200
@@ -362,7 +362,7 @@
\<close>
declaration \<open>fn _ =>
Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
- map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
+ map mk_eq o Ord_atomize o Variable.gen_all ctxt))
\<close>
text \<open>Setting up the one-point-rule simproc\<close>
--- a/src/ZF/Tools/inductive_package.ML Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Jul 28 23:29:13 2015 +0200
@@ -327,8 +327,7 @@
If the premises get simplified, then the proofs could fail.*)
val min_ss =
(empty_simpset (Proof_Context.init_global thy)
- |> Simplifier.set_mksimps (fn ctxt =>
- map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
+ |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt))
setSolver (mk_solver "minimal"
(fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
ORELSE' assume_tac ctxt
--- a/src/ZF/pair.thy Tue Jul 28 18:45:32 2015 +0200
+++ b/src/ZF/pair.thy Tue Jul 28 23:29:13 2015 +0200
@@ -12,8 +12,7 @@
setup \<open>
map_theory_simpset
- (Simplifier.set_mksimps (fn ctxt =>
- map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt))
+ (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
#> Simplifier.add_cong @{thm if_weak_cong})
\<close>