--- a/src/HOL/Eisbach/match_method.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Wed Jun 03 21:48:40 2015 +0200
@@ -181,7 +181,7 @@
val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
fun label_thm thm =
- Thm.cterm_of ctxt' (Free (nm, propT))
+ Thm.cterm_of ctxt'' (Free (nm, propT))
|> Drule.mk_term
|> not (null abs_nms) ? Conjunction.intr thm
@@ -509,19 +509,18 @@
(* Fix schematics in the goal *)
fun focus_concl ctxt i goal =
let
- val ({context, concl, params, prems, asms, schematics}, goal') =
+ val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
Subgoal.focus_params ctxt i goal;
- val ((_, schematic_terms), context') =
- Variable.import_inst true [Thm.term_of concl] context
- |>> Thm.certify_inst (Thm.theory_of_thm goal');
+ val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
+ val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
val goal'' = Thm.instantiate ([], schematic_terms) goal';
val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
val (schematic_types, schematic_terms') = schematics;
val schematics' = (schematic_types, schematic_terms @ schematic_terms');
in
- ({context = context', concl = concl', params = params, prems = prems,
+ ({context = ctxt'', concl = concl', params = params, prems = prems,
schematics = schematics', asms = asms} : Subgoal.focus, goal'')
end;
--- a/src/HOL/GCD.thy Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/GCD.thy Wed Jun 03 21:48:40 2015 +0200
@@ -1355,7 +1355,7 @@
lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
- by (auto intro: dvd_antisym [transferred] lcm_least_int) (* FIXME slow *)
+ using lcm_least_int zdvd_antisym_nonneg by auto
interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
--- a/src/HOL/Import/import_rule.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Wed Jun 03 21:48:40 2015 +0200
@@ -328,13 +328,14 @@
fun store_thm binding thm thy =
let
+ val ctxt = Proof_Context.init_global thy
val thm = Drule.export_without_context_open thm
val tvs = Term.add_tvars (Thm.prop_of thm) []
val tns = map (fn (_, _) => "'") tvs
- val nms = fst (fold_map Name.variant tns (Variable.names_of (Proof_Context.init_global thy)))
+ val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
- val cvs = map (Thm.global_ctyp_of thy) vs
- val ctvs = map (Thm.global_ctyp_of thy) (map TVar tvs)
+ val cvs = map (Thm.ctyp_of ctxt) vs
+ val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs)
val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
in
snd (Global_Theory.add_thm ((binding, thm'), []) thy)
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Jun 03 21:48:40 2015 +0200
@@ -28,7 +28,7 @@
(*utility functions*)
val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
Proof.state -> bool
- val theorems_in_proof_term : thm -> thm list
+ val theorems_in_proof_term : theory -> thm -> thm list
val theorems_of_sucessful_proof : Toplevel.state option -> thm list
val get_setting : (string * string) list -> string * string -> string
val get_int_setting : (string * string) list -> string * int -> int
@@ -178,9 +178,9 @@
in
-fun theorems_in_proof_term thm =
+fun theorems_in_proof_term thy thm =
let
- val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) true
+ val all_thms = Global_Theory.all_thms_of thy true
fun collect (s, _, _) = if s <> "" then insert (op =) s else I
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
fun resolve_thms names = map_filter (member_of names) all_thms
@@ -195,7 +195,8 @@
NONE => []
| SOME st =>
if not (Toplevel.is_proof st) then []
- else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st))))
+ else
+ theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st))))
fun get_setting settings (key, default) =
the_default default (AList.lookup (op =) settings key)
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Jun 03 21:48:40 2015 +0200
@@ -120,8 +120,8 @@
val perm_simproc =
Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
-fun projections rule =
- Project_Rule.projections (Proof_Context.init_global (Thm.theory_of_thm rule)) rule
+fun projections ctxt rule =
+ Project_Rule.projections ctxt rule
|> map (Drule.export_without_context #> Rule_Cases.save rule);
val supp_prod = @{thm supp_prod};
@@ -1114,7 +1114,9 @@
val (_, thy9) = thy8 |>
Sign.add_path big_name |>
Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
- Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
+ Global_Theory.add_thmss
+ [((Binding.name "inducts", projections (Proof_Context.init_global thy8) dt_induct),
+ [case_names_induct])] ||>
Sign.parent_path ||>>
Old_Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
Old_Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
@@ -1412,7 +1414,9 @@
Sign.add_path big_name |>
Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
- Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
+ Global_Theory.add_thmss
+ [((Binding.name "strong_inducts", projections (Proof_Context.init_global thy9) induct),
+ [case_names_induct])];
(**** recursion combinator ****)
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jun 03 21:48:40 2015 +0200
@@ -145,10 +145,11 @@
val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
fun inst_fresh vars params i st =
let val vars' = Misc_Legacy.term_vars (Thm.prop_of st);
- val thy = Thm.theory_of_thm st;
in case subtract (op =) vars vars' of
[x] =>
- Seq.single (Thm.instantiate ([], [(Thm.global_cterm_of thy x, Thm.global_cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
+ Seq.single
+ (Thm.instantiate ([],
+ [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st)
| _ => error "fresh_fun_simp: Too many variables, please report."
end
in
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Jun 03 21:48:40 2015 +0200
@@ -39,8 +39,8 @@
fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
[(perm_boolI_pi, pi)] perm_boolI;
-fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
- (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
+fun mk_perm_bool_simproc names =
+ Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
@@ -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);
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Jun 03 21:48:40 2015 +0200
@@ -43,8 +43,8 @@
fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
[(perm_boolI_pi, pi)] perm_boolI;
-fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
- (Thm.theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
+fun mk_perm_bool_simproc names =
+ Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
--- a/src/HOL/Nominal/nominal_permeq.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Jun 03 21:48:40 2015 +0200
@@ -70,11 +70,6 @@
val perm_aux_fold = @{thm "perm_aux_fold"};
val supports_fresh_rule = @{thm "supports_fresh"};
-(* pulls out dynamically a thm via the proof state *)
-fun dynamic_thms st name = Global_Theory.get_thms (Thm.theory_of_thm st) name;
-fun dynamic_thm st name = Global_Theory.get_thm (Thm.theory_of_thm st) name;
-
-
(* needed in the process of fully simplifying permutations *)
val strong_congs = [@{thm "if_cong"}]
(* needed to avoid warnings about overwritten congs *)
@@ -146,7 +141,7 @@
("general simplification of permutations", fn st => SUBGOAL (fn _ =>
let
val ctxt' = ctxt
- addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
+ addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
addsimprocs [perm_simproc_fun, perm_simproc_app]
|> fold Simplifier.del_cong weak_congs
|> fold Simplifier.add_cong strong_congs
@@ -296,7 +291,6 @@
case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of
_ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
let
- val cert = Thm.global_cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (Thm.term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 x [];
@@ -310,8 +304,8 @@
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (Thm.prems_of supports_rule'));
val supports_rule'' = Drule.cterm_instantiate
- [(cert (head_of S), cert s')] supports_rule'
- val fin_supp = dynamic_thms st ("fin_supp")
+ [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_rule'
+ val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
(tactical ctxt ("guessing of the right supports-set",
@@ -332,15 +326,14 @@
fun fresh_guess_tac_i tactical ctxt i st =
let
val goal = nth (cprems_of st) (i - 1)
- val fin_supp = dynamic_thms st ("fin_supp")
- val fresh_atm = dynamic_thms st ("fresh_atm")
+ val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
+ val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm"
val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
case Logic.strip_assums_concl (Thm.term_of goal) of
_ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) =>
let
- val cert = Thm.global_cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (Thm.term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 t [];
@@ -354,7 +347,7 @@
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (Thm.prems_of supports_fresh_rule'));
val supports_fresh_rule'' = Drule.cterm_instantiate
- [(cert (head_of S), cert s')] supports_fresh_rule'
+ [apply2 (Thm.cterm_of ctxt) (head_of S, s')] supports_fresh_rule'
in
(tactical ctxt ("guessing of the right set that supports the goal",
(EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
--- a/src/HOL/Proofs/ex/XML_Data.thy Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy Wed Jun 03 21:48:40 2015 +0200
@@ -12,9 +12,8 @@
subsection {* Export and re-import of global proof terms *}
ML {*
- fun export_proof thm =
+ fun export_proof thy thm =
let
- val thy = Thm.theory_of_thm thm;
val {prop, hyps, shyps, ...} = Thm.rep_thm thm;
val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop));
val prf =
@@ -40,24 +39,24 @@
lemma ex: "A \<longrightarrow> A" ..
ML_val {*
- val xml = export_proof @{thm ex};
+ val xml = export_proof @{theory} @{thm ex};
val thm = import_proof thy1 xml;
*}
ML_val {*
- val xml = export_proof @{thm de_Morgan};
+ val xml = export_proof @{theory} @{thm de_Morgan};
val thm = import_proof thy1 xml;
*}
ML_val {*
- val xml = export_proof @{thm Drinker's_Principle};
+ val xml = export_proof @{theory} @{thm Drinker's_Principle};
val thm = import_proof thy1 xml;
*}
text {* Some fairly large proof: *}
ML_val {*
- val xml = export_proof @{thm abs_less_iff};
+ val xml = export_proof @{theory} @{thm abs_less_iff};
val thm = import_proof thy1 xml;
@{assert} (size (YXML.string_of_body xml) > 1000000);
*}
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Jun 03 21:48:40 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
--- a/src/HOL/Tools/Meson/meson.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Wed Jun 03 21:48:40 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
@@ -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
@@ -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.*)
@@ -787,15 +786,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 Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Wed Jun 03 21:48:40 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_reconstruct.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 03 21:48:40 2015 +0200
@@ -171,11 +171,10 @@
(* INFERENCE RULE: RESOLVE *)
(*Increment the indexes of only the type variables*)
-fun incr_type_indexes inc th =
+fun incr_type_indexes ctxt inc th =
let
val tvs = Term.add_tvars (Thm.full_prop_of th) []
- val thy = Thm.theory_of_thm th
- fun inc_tvar ((a, i), s) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
+ fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s))
in
Thm.instantiate (map inc_tvar tvs, []) th
end
@@ -185,7 +184,7 @@
Instantiations of those Vars could then fail. *)
fun resolve_inc_tyvars ctxt tha i thb =
let
- val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
fun res (tha, thb) =
(case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
(false, tha, Thm.nprems_of tha) i thb
@@ -393,16 +392,16 @@
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
-fun flexflex_first_order th =
+fun flexflex_first_order ctxt th =
(case Thm.tpairs_of th of
[] => th
| pairs =>
let
- val thy = Thm.theory_of_thm th
+ val thy = Proof_Context.theory_of ctxt
val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
- fun mkT (v, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar (v, S), T)
- fun mk (v, (T, t)) = apply2 (Thm.global_cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+ fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T)
+ fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t)
val instsT = Vartab.fold (cons o mkT) tyenv []
val insts = Vartab.fold (cons o mk) tenv []
@@ -462,7 +461,7 @@
val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
- |> flexflex_first_order
+ |> flexflex_first_order ctxt
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg ctxt (fn () => "=============================================")
--- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Jun 03 21:48:40 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
@@ -84,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
@@ -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/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Jun 03 21:48:40 2015 +0200
@@ -947,7 +947,7 @@
val U = TFree ("'u", @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 $ y)
- val th' = Thm.certify_instantiate
+ val th' = Thm.certify_instantiate ctxt
([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
[((fst (dest_Var f), (U --> T') --> T'), f')]) th
val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
@@ -1086,13 +1086,13 @@
if not (fst (dest_Const pred) = fst (dest_Const pred')) then
raise Fail "Trying to instantiate another predicate"
else ()
- in Thm.certify_instantiate (subst_of (pred', pred), []) th end
+ in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
fun instantiate_ho_args th =
let
val (_, args') =
(strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
val ho_args' = map dest_Var (ho_args_of_typ T args')
- in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
+ in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
val outp_pred =
Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
val ((_, ths'), ctxt1) =
--- a/src/HOL/Tools/TFL/casesplit.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Jun 03 21:48:40 2015 +0200
@@ -32,28 +32,28 @@
(* for use when there are no prems to the subgoal *)
(* does a case split on the given variable *)
-fun mk_casesplit_goal_thm sgn (vstr,ty) gt =
+fun mk_casesplit_goal_thm ctxt (vstr,ty) gt =
let
- val x = Free(vstr,ty)
+ val thy = Proof_Context.theory_of ctxt;
+
+ val x = Free(vstr,ty);
val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
- val ctermify = Thm.global_cterm_of sgn;
- val ctypify = Thm.global_ctyp_of sgn;
- val case_thm = case_thm_of_ty sgn ty;
+ val case_thm = case_thm_of_ty thy ty;
- val abs_ct = ctermify abst;
- val free_ct = ctermify x;
+ val abs_ct = Thm.cterm_of ctxt abst;
+ val free_ct = Thm.cterm_of ctxt x;
val (Pv, Dv, type_insts) =
case (Thm.concl_of case_thm) of
- (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
+ (_ $ (Pv $ (Dv as Var(D, Dty)))) =>
(Pv, Dv,
- Sign.typ_match sgn (Dty, ty) Vartab.empty)
+ Sign.typ_match thy (Dty, ty) Vartab.empty)
| _ => error "not a valid case thm";
- val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
+ val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T))
(Vartab.dest type_insts);
- val cPv = ctermify (Envir.subst_term_types type_insts Pv);
- val cDv = ctermify (Envir.subst_term_types type_insts Dv);
+ val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv);
+ val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv);
in
Conv.fconv_rule Drule.beta_eta_conversion
(case_thm
@@ -117,7 +117,6 @@
fun splitto ctxt splitths genth =
let
val _ = not (null splitths) orelse error "splitto: no given splitths";
- val thy = Thm.theory_of_thm genth;
(* check if we are a member of splitths - FIXME: quicker and
more flexible with discrim net. *)
@@ -134,7 +133,7 @@
| SOME v =>
let
val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
- val split_thm = mk_casesplit_goal_thm thy v gt;
+ val split_thm = mk_casesplit_goal_thm ctxt v gt;
val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
in
expf (map recsplitf subthms)
--- a/src/HOL/Tools/TFL/post.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/post.ML Wed Jun 03 21:48:40 2015 +0200
@@ -7,10 +7,10 @@
signature TFL =
sig
- val define_i: bool -> Proof.context -> thm list -> thm list -> xstring -> term -> term list ->
- theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory
- val define: bool -> Proof.context -> thm list -> thm list -> xstring -> string -> string list ->
- theory -> {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * theory
+ val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context ->
+ {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
+ val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context ->
+ {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
val defer_i: thm list -> xstring -> term list -> theory -> thm * theory
val defer: thm list -> xstring -> string list -> theory -> thm * theory
end;
@@ -34,13 +34,13 @@
* non-proved termination conditions, and finally attempts to prove the
* simplified termination conditions.
*--------------------------------------------------------------------------*)
-fun std_postprocessor strict ctxt wfs =
- Prim.postprocess strict
+fun std_postprocessor ctxt strict wfs =
+ Prim.postprocess ctxt strict
{wf_tac = REPEAT (ares_tac wfs 1),
terminator =
asm_simp_tac ctxt 1
THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
- fast_force_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
+ fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
simplifier = Rules.simpl_conv ctxt []};
@@ -78,19 +78,21 @@
val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *)
val cntxt = union (op aconv) cntxtl cntxtr
in
- Rules.GEN_ALL
+ Rules.GEN_ALL ctxt
(Rules.DISCH_ALL
(rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
end
val gen_all = USyntax.gen_all
in
-fun proof_stage strict ctxt wfs theory {f, R, rules, full_pats_TCs, TCs} =
+fun proof_stage ctxt strict wfs {f, R, rules, full_pats_TCs, TCs} =
let
val _ = writeln "Proving induction theorem ..."
- val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
+ val ind =
+ Prim.mk_induction (Proof_Context.theory_of ctxt)
+ {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
val _ = writeln "Postprocessing ...";
val {rules, induction, nested_tcs} =
- std_postprocessor strict ctxt wfs theory {rules=rules, induction=ind, TCs=TCs}
+ std_postprocessor ctxt strict wfs {rules=rules, induction=ind, TCs=TCs}
in
case nested_tcs
of [] => {induction=induction, rules=rules,tcs=[]}
@@ -134,29 +136,28 @@
fun tracing true _ = ()
| tracing false msg = writeln msg;
-fun simplify_defn strict thy ctxt congs wfs id pats def0 =
- let
- val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
- val {rules,rows,TCs,full_pats_TCs} =
- Prim.post_definition congs thy ctxt (def, pats)
- val {lhs=f,rhs} = USyntax.dest_eq (concl def)
- val (_,[R,_]) = USyntax.strip_comb rhs
- val dummy = Prim.trace_thms ctxt "congs =" congs
- (*the next step has caused simplifier looping in some cases*)
- val {induction, rules, tcs} =
- proof_stage strict ctxt wfs thy
- {f = f, R = R, rules = rules,
- full_pats_TCs = full_pats_TCs,
- TCs = TCs}
- val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
- (Rules.CONJUNCTS rules)
- in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
- rules = ListPair.zip(rules', rows),
- tcs = (termination_goals rules') @ tcs}
- end
+fun simplify_defn ctxt strict congs wfs id pats def0 =
+ let
+ val def = Thm.unvarify_global 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
+ val dummy = Prim.trace_thms ctxt "congs =" congs
+ (*the next step has caused simplifier looping in some cases*)
+ val {induction, rules, tcs} =
+ proof_stage ctxt strict wfs
+ {f = f, R = R, rules = rules,
+ full_pats_TCs = full_pats_TCs,
+ TCs = TCs}
+ val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
+ (Rules.CONJUNCTS rules)
+ in
+ {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
+ rules = ListPair.zip(rules', rows),
+ tcs = (termination_goals rules') @ tcs}
+ end
handle Utils.ERR {mesg,func,module} =>
- error (mesg ^
- "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
+ error (mesg ^ "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
(* Derive the initial equations from the case-split rules to meet the
@@ -184,21 +185,21 @@
(*---------------------------------------------------------------------------
* Defining a function with an associated termination relation.
*---------------------------------------------------------------------------*)
-fun define_i strict ctxt congs wfs fid R eqs thy =
- let val {functional,pats} = Prim.mk_functional thy eqs
- val (thy, def) = Prim.wfrec_definition0 thy fid R functional
- val ctxt = Proof_Context.transfer thy ctxt
- val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
- val {induct, rules, tcs} = simplify_defn strict thy ctxt congs wfs fid pats def
- val rules' =
- if strict then derive_init_eqs ctxt rules eqs
- else rules
- in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, thy) end;
+fun define_i strict congs wfs fid R eqs ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val {functional, pats} = Prim.mk_functional thy eqs
+ val (def, thy') = Prim.wfrec_definition0 fid R functional thy
+ val ctxt' = Proof_Context.transfer thy' ctxt
+ val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
+ val {induct, rules, tcs} = simplify_defn ctxt' strict congs wfs fid pats def
+ val rules' = if strict then derive_init_eqs ctxt' rules eqs else rules
+ in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, ctxt') end;
-fun define strict ctxt congs wfs fid R seqs thy =
- define_i strict ctxt congs wfs fid
- (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) thy
- handle Utils.ERR {mesg,...} => error mesg;
+fun define strict congs wfs fid R seqs ctxt =
+ define_i strict congs wfs fid
+ (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt
+ handle Utils.ERR {mesg,...} => error mesg;
(*---------------------------------------------------------------------------
@@ -211,7 +212,8 @@
#1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm)))))));
fun defer_i congs fid eqs thy =
- let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
+ let
+ val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
val dummy = writeln "Proving induction theorem ...";
val induction = Prim.mk_induction theory
--- a/src/HOL/Tools/TFL/rules.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Wed Jun 03 21:48:40 2015 +0200
@@ -21,22 +21,22 @@
val SPEC: cterm -> thm -> thm
val ISPEC: cterm -> thm -> thm
val ISPECL: cterm list -> thm -> thm
- val GEN: cterm -> thm -> thm
- val GENL: cterm list -> thm -> thm
+ val GEN: Proof.context -> cterm -> thm -> thm
+ val GENL: Proof.context -> cterm list -> thm -> thm
val LIST_CONJ: thm list -> thm
val SYM: thm -> thm
val DISCH_ALL: thm -> thm
val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
val SPEC_ALL: thm -> thm
- val GEN_ALL: thm -> thm
+ val GEN_ALL: Proof.context -> thm -> thm
val IMP_TRANS: thm -> thm -> thm
val PROVE_HYP: thm -> thm -> thm
val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
val EXISTS: cterm * cterm -> thm -> thm
val EXISTL: cterm list -> thm -> thm
- val IT_EXISTS: (cterm*cterm) list -> thm -> thm
+ val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
val EVEN_ORS: thm list -> thm list
val DISJ_CASESL: thm -> thm list -> thm
@@ -47,8 +47,8 @@
val rbeta: thm -> thm
val tracing: bool Unsynchronized.ref
- val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
- -> thm -> thm * term list
+ val CONTEXT_REWRITE_RULE: Proof.context ->
+ term * term list * thm * thm list -> thm -> thm * term list
val RIGHT_ASSOC: Proof.context -> thm -> thm
val prove: Proof.context -> bool -> term * tactic -> thm
@@ -158,19 +158,19 @@
(*----------------------------------------------------------------------------
* Disjunction
*---------------------------------------------------------------------------*)
-local val thy = Thm.theory_of_thm disjI1
- val prop = Thm.prop_of disjI1
- val [P,Q] = Misc_Legacy.term_vars prop
- val disj1 = Thm.forall_intr (Thm.global_cterm_of thy Q) disjI1
+local
+ val prop = Thm.prop_of disjI1
+ val [P,Q] = Misc_Legacy.term_vars prop
+ val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
in
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
end;
-local val thy = Thm.theory_of_thm disjI2
- val prop = Thm.prop_of disjI2
- val [P,Q] = Misc_Legacy.term_vars prop
- val disj2 = Thm.forall_intr (Thm.global_cterm_of thy P) disjI2
+local
+ val prop = Thm.prop_of disjI2
+ val [P,Q] = Misc_Legacy.term_vars prop
+ val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
in
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
@@ -262,11 +262,10 @@
* Universals
*---------------------------------------------------------------------------*)
local (* this is fragile *)
- val thy = Thm.theory_of_thm spec
- val prop = Thm.prop_of spec
- val x = hd (tl (Misc_Legacy.term_vars prop))
- val cTV = Thm.global_ctyp_of thy (type_of x)
- val gspec = Thm.forall_intr (Thm.global_cterm_of thy x) spec
+ val prop = Thm.prop_of spec
+ val x = hd (tl (Misc_Legacy.term_vars prop))
+ val cTV = Thm.ctyp_of @{context} (type_of x)
+ val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
in
fun SPEC tm thm =
let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
@@ -279,41 +278,38 @@
val ISPECL = fold ISPEC;
(* Not optimized! Too complicated. *)
-local val thy = Thm.theory_of_thm allI
- val prop = Thm.prop_of allI
- val [P] = Misc_Legacy.add_term_vars (prop, [])
- fun cty_theta s = map (fn (i, (S, ty)) => (Thm.global_ctyp_of s (TVar (i, S)), Thm.global_ctyp_of s ty))
- fun ctm_theta s = map (fn (i, (_, tm2)) =>
- let val ctm2 = Thm.global_cterm_of s tm2
- in (Thm.global_cterm_of s (Var(i, Thm.typ_of_cterm ctm2)), ctm2)
- end)
- fun certify s (ty_theta,tm_theta) =
- (cty_theta s (Vartab.dest ty_theta),
- ctm_theta s (Vartab.dest tm_theta))
+local
+ val prop = Thm.prop_of allI
+ val [P] = Misc_Legacy.add_term_vars (prop, [])
+ fun cty_theta ctxt = map (fn (i, (S, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (i, S), ty))
+ fun ctm_theta ctxt =
+ map (fn (i, (_, tm2)) =>
+ let val ctm2 = Thm.cterm_of ctxt tm2
+ in (Thm.cterm_of ctxt (Var (i, Thm.typ_of_cterm ctm2)), ctm2) end)
+ fun certify ctxt (ty_theta,tm_theta) =
+ (cty_theta ctxt (Vartab.dest ty_theta),
+ ctm_theta ctxt (Vartab.dest tm_theta))
in
-fun GEN v th =
+fun GEN ctxt v th =
let val gth = Thm.forall_intr v th
- val thy = Thm.theory_of_thm gth
+ val thy = Proof_Context.theory_of ctxt
val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
- val allI2 = Drule.instantiate_normalize (certify thy theta) allI
+ val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
val thm = Thm.implies_elim allI2 gth
val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
val prop' = tp $ (A $ Abs(x,ty,M))
- in ALPHA thm (Thm.global_cterm_of thy prop')
- end
+ in ALPHA thm (Thm.cterm_of ctxt prop') end
end;
-val GENL = fold_rev GEN;
+fun GENL ctxt = fold_rev (GEN ctxt);
-fun GEN_ALL thm =
- let val thy = Thm.theory_of_thm thm
- val prop = Thm.prop_of thm
- val tycheck = Thm.global_cterm_of thy
- val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, []))
- in GENL vlist thm
- end;
+fun GEN_ALL ctxt thm =
+ let
+ val prop = Thm.prop_of thm
+ val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
+ in GENL ctxt vlist thm end;
fun MATCH_MP th1 th2 =
@@ -344,24 +340,19 @@
val t$u = Thm.term_of redex
val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
in
- GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
+ GEN ctxt fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
end;
-local val thy = Thm.theory_of_thm exI
- val prop = Thm.prop_of exI
- val [P,x] = Misc_Legacy.term_vars prop
+local
+ val prop = Thm.prop_of exI
+ val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
in
fun EXISTS (template,witness) thm =
- let val thy = Thm.theory_of_thm thm
- val prop = Thm.prop_of thm
- val P' = Thm.global_cterm_of thy P
- val x' = Thm.global_cterm_of thy x
- val abstr = #2 (Dcterm.dest_comb template)
- in
- thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
- handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
- end
+ let val abstr = #2 (Dcterm.dest_comb template) in
+ thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
+ handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
+ end
end;
(*----------------------------------------------------------------------------
@@ -386,16 +377,14 @@
*---------------------------------------------------------------------------*)
(* Could be improved, but needs "subst_free" for certified terms *)
-fun IT_EXISTS blist th =
- let val thy = Thm.theory_of_thm th
- val tych = Thm.global_cterm_of thy
- val blist' = map (apply2 Thm.term_of) blist
- fun ex v M = Thm.global_cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
-
+fun IT_EXISTS ctxt blist th =
+ let
+ val blist' = map (apply2 Thm.term_of) blist
+ fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
in
- fold_rev (fn (b as (r1,r2)) => fn thm =>
+ fold_rev (fn (b as (r1,r2)) => fn thm =>
EXISTS(ex r2 (subst_free [b]
- (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1)
+ (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
thm)
blist' th
end;
@@ -509,13 +498,10 @@
(* Note: Thm.rename_params_rule counts from 1, not 0 *)
fun rename thm =
- let val thy = Thm.theory_of_thm thm
- val tych = Thm.global_cterm_of thy
- val ants = Logic.strip_imp_prems (Thm.prop_of thm)
- val news = get (ants,1,[])
- in
- fold Thm.rename_params_rule news thm
- end;
+ let
+ val ants = Logic.strip_imp_prems (Thm.prop_of thm)
+ val news = get (ants,1,[])
+ in fold Thm.rename_params_rule news thm end;
(*---------------------------------------------------------------------------
@@ -539,8 +525,8 @@
fun print_thms ctxt s L =
say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
-fun print_cterm ctxt s ct =
- say (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)]);
+fun print_term ctxt s t =
+ say (cat_lines [s, Syntax.string_of_term ctxt t]);
(*---------------------------------------------------------------------------
@@ -647,9 +633,9 @@
(fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
t)
-fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
+fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
let val globals = func::G
- val ctxt0 = empty_simpset (Proof_Context.init_global (Thm.theory_of_thm th))
+ val ctxt0 = empty_simpset main_ctxt
val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
val cut_lemma' = cut_lemma RS eq_reflection
@@ -661,28 +647,28 @@
val dummy = say "cong rule:"
val dummy = say (Display.string_of_thm ctxt thm)
(* Unquantified eliminate *)
- fun uq_eliminate (thm,imp,thy) =
- let val tych = Thm.global_cterm_of thy
- val dummy = print_cterm ctxt "To eliminate:" (tych imp)
+ fun uq_eliminate (thm,imp) =
+ let val tych = Thm.cterm_of ctxt
+ val _ = print_term ctxt "To eliminate:" imp
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
handle Utils.ERR _ => Thm.reflexive lhs
- val dummy = print_thms ctxt' "proven:" [lhs_eq_lhs1]
+ val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
in
lhs_eeq_lhs2 COMP thm
end
- fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) =
+ fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
val dummy = forall (op aconv) (ListPair.zip (vlist, args))
orelse error "assertion failed in CONTEXT_REWRITE_RULE"
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
- val tych = Thm.global_cterm_of thy
+ val tych = Thm.cterm_of ctxt
val ants1 = map tych (Logic.strip_imp_prems imp_body1)
val eq1 = Logic.strip_imp_concl imp_body1
val Q = get_lhs eq1
@@ -705,13 +691,13 @@
val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
in ant_th COMP thm
end
- fun q_eliminate (thm,imp,thy) =
+ fun q_eliminate (thm, imp) =
let val (vlist, imp_body, used') = strip_all used imp
val (ants,Q) = dest_impl imp_body
in if (pbeta_redex Q) (length vlist)
- then pq_eliminate (thm,thy,vlist,imp_body,Q)
+ then pq_eliminate (thm, vlist, imp_body, Q)
else
- let val tych = Thm.global_cterm_of thy
+ let val tych = Thm.cterm_of ctxt
val ants1 = map tych ants
val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
@@ -725,22 +711,21 @@
end end
fun eliminate thm =
- case Thm.prop_of thm
- of Const(@{const_name Pure.imp},_) $ imp $ _ =>
+ case Thm.prop_of thm of
+ Const(@{const_name Pure.imp},_) $ imp $ _ =>
eliminate
(if not(is_all imp)
- then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
- else q_eliminate (thm, imp, Thm.theory_of_thm thm))
+ then uq_eliminate (thm, imp)
+ else q_eliminate (thm, imp))
(* Assume that the leading constant is ==, *)
| _ => thm (* if it is not a ==> *)
in SOME(eliminate (rename thm)) end
handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
fun restrict_prover ctxt thm =
- let val dummy = say "restrict_prover:"
+ let val _ = say "restrict_prover:"
val cntxt = rev (Simplifier.prems_of ctxt)
- val dummy = print_thms ctxt "cntxt:" cntxt
- val thy = Thm.theory_of_thm thm
+ val _ = print_thms ctxt "cntxt:" cntxt
val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
@@ -762,14 +747,13 @@
val antl = case rcontext of [] => []
| _ => [USyntax.list_mk_conj(map cncl rcontext)]
val TC = genl(USyntax.list_mk_imp(antl, A))
- val dummy = print_cterm ctxt "func:" (Thm.global_cterm_of thy func)
- val dummy = print_cterm ctxt "TC:" (Thm.global_cterm_of thy (HOLogic.mk_Trueprop TC))
- val dummy = tc_list := (TC :: !tc_list)
+ val _ = print_term ctxt "func:" func
+ val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC)
+ val _ = tc_list := (TC :: !tc_list)
val nestedp = is_some (USyntax.find_term is_func TC)
- val dummy = if nestedp then say "nested" else say "not_nested"
+ val _ = if nestedp then say "nested" else say "not_nested"
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
- else let val cTC = Thm.global_cterm_of thy
- (HOLogic.mk_Trueprop TC)
+ else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
in case rcontext of
[] => SPEC_ALL(ASSUME cTC)
| _ => MP (SPEC_ALL (ASSUME cTC))
--- a/src/HOL/Tools/TFL/tfl.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Jun 03 21:48:40 2015 +0200
@@ -11,8 +11,8 @@
val trace_cterm: Proof.context -> string -> cterm -> unit
type pattern
val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
- val wfrec_definition0: theory -> string -> term -> term -> theory * thm
- val post_definition: thm list -> theory -> Proof.context -> thm * pattern list ->
+ val wfrec_definition0: string -> term -> term -> theory -> thm * theory
+ val post_definition: Proof.context -> thm list -> thm * pattern list ->
{rules: thm,
rows: int list,
TCs: term list list,
@@ -32,9 +32,10 @@
patterns : pattern list}
val mk_induction: theory ->
{fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
- val postprocess: bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm}
- -> theory -> {rules: thm, induction: thm, TCs: term list list}
- -> {rules: thm, induction: thm, nested_tcs: thm list}
+ val postprocess: Proof.context -> bool ->
+ {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
+ {rules: thm, induction: thm, TCs: term list list} ->
+ {rules: thm, induction: thm, nested_tcs: thm list}
end;
structure Prim: PRIM =
@@ -364,21 +365,23 @@
| poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
| poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
-local val f_eq_wfrec_R_M =
- #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
- val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
- val (fname,_) = dest_Free f
- val (wfrec,_) = USyntax.strip_comb rhs
+local
+ val f_eq_wfrec_R_M =
+ #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
+ val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
+ val (fname,_) = dest_Free f
+ val (wfrec,_) = USyntax.strip_comb rhs
in
-fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
- let val def_name = Thm.def_name (Long_Name.base_name fid)
- val wfrec_R_M = map_types poly_tvars
- (wfrec $ map_types poly_tvars R)
- $ functional
- val def_term = const_def thy (fid, Ty, wfrec_R_M)
- val ([def], thy') =
+
+fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy =
+ let
+ val def_name = Thm.def_name (Long_Name.base_name fid)
+ val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
+ val def_term = const_def thy (fid, Ty, wfrec_R_M)
+ val ([def], thy') =
Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
- in (thy', def) end;
+ in (def, thy') end;
+
end;
@@ -415,8 +418,9 @@
fun givens pats = map pat_of (filter given pats);
-fun post_definition meta_tflCongs theory ctxt (def, pats) =
- let val tych = Thry.typecheck theory
+fun post_definition ctxt meta_tflCongs (def, pats) =
+ let val thy = Proof_Context.theory_of ctxt
+ val tych = Thry.typecheck thy
val f = #lhs(USyntax.dest_eq(concl def))
val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
val pats' = filter given pats
@@ -425,9 +429,8 @@
val WFR = #ant(USyntax.dest_imp(concl corollary))
val R = #Rand(USyntax.dest_comb WFR)
val corollary' = Rules.UNDISCH corollary (* put WF R on assums *)
- val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary')
- given_pats
- val (case_rewrites,context_congs) = extraction_thms theory
+ val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
+ val (case_rewrites,context_congs) = extraction_thms thy
(*case_ss causes minimal simplification: bodies of case expressions are
not simplified. Otherwise large examples (Red-Black trees) are too
slow.*)
@@ -435,10 +438,10 @@
put_simpset HOL_basic_ss ctxt
addsimps case_rewrites
|> fold (Simplifier.add_cong o #case_cong_weak o snd)
- (Symtab.dest (BNF_LFP_Compat.get_all theory [BNF_LFP_Compat.Keep_Nesting]))
+ (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
val corollaries' = map (Simplifier.simplify case_simpset) corollaries
- val extract = Rules.CONTEXT_REWRITE_RULE
- (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
+ val extract =
+ Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
val (rules, TCs) = ListPair.unzip (map extract corollaries')
val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
@@ -495,8 +498,8 @@
val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
val corollaries' = map (rewrite_rule ctxt case_rewrites) corollaries
- fun extract X = Rules.CONTEXT_REWRITE_RULE
- (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
+ val extract =
+ Rules.CONTEXT_REWRITE_RULE ctxt (f, R1::SV, @{thm cut_apply}, tflCongs @ context_congs)
in {proto_def = proto_def,
SV=SV,
WFR=WFR,
@@ -535,30 +538,30 @@
val (c,args) = USyntax.strip_comb lhs
val (name,Ty) = dest_atom c
val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
- val ([def0], theory) =
+ val ([def0], thy') =
thy
|> Global_Theory.add_defs false
[Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
val def = Thm.unvarify_global def0;
+ val ctxt' = Syntax.init_pretty_global thy';
val dummy =
- if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
+ if !trace then writeln ("DEF = " ^ Display.string_of_thm ctxt' def)
else ()
(* val fconst = #lhs(USyntax.dest_eq(concl def)) *)
- val tych = Thry.typecheck theory
+ val tych = Thry.typecheck thy'
val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
(*lcp: a lot of object-logic inference to remove*)
val baz = Rules.DISCH_ALL
(fold_rev Rules.DISCH full_rqt_prop
(Rules.LIST_CONJ extractants))
- val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
- else ()
+ val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm ctxt' baz) else ()
val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
val SV' = map tych SV;
val SVrefls = map Thm.reflexive SV'
val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
SVrefls def)
RS meta_eq_to_obj_eq
- val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0
+ val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN ctxt' (tych R1) baz)) def0
val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
theory Hilbert_Choice*)
@@ -566,7 +569,7 @@
handle ERROR msg => cat_error msg
"defer_recdef requires theory Main or at least Hilbert_Choice as parent"
val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
- in {theory = theory, R=R1, SV=SV,
+ in {theory = thy', R=R1, SV=SV,
rules = fold (fn a => fn b => Rules.MP b a) (Rules.CONJUNCTS bar) def',
full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
patterns = pats}
@@ -633,7 +636,7 @@
fun fail s = raise TFL_ERR "mk_case" s
fun mk{rows=[],...} = fail"no rows"
| mk{path=[], rows = [([], (thm, bindings))]} =
- Rules.IT_EXISTS (map tych_binding bindings) thm
+ Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
| mk{path = u::rstp, rows as (p::_, _)::_} =
let val (pat_rectangle,rights) = ListPair.unzip rows
val col0 = map hd pat_rectangle
@@ -693,7 +696,7 @@
val th0 = Rules.ASSUME (tych a_eq_v)
val rows = map (fn x => ([x], (th0,[]))) pats
in
- Rules.GEN (tych a)
+ Rules.GEN ctxt (tych a)
(Rules.RIGHT_ASSOC ctxt
(Rules.CHOOSE ctxt (tych v, ex_th0)
(mk_case ty_info (vname::aname::names)
@@ -774,14 +777,14 @@
* TCs = TC_1[pat] ... TC_n[pat]
* thm = ih1 /\ ... /\ ih_n |- ih[pat]
*---------------------------------------------------------------------------*)
-fun prove_case f thy (tm,TCs_locals,thm) =
- let val tych = Thry.typecheck thy
+fun prove_case ctxt f (tm,TCs_locals,thm) =
+ let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
val antc = tych(#ant(USyntax.dest_imp tm))
val thm' = Rules.SPEC_ALL thm
fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
fun mk_ih ((TC,locals),th2,nested) =
- Rules.GENL (map tych locals)
+ Rules.GENL ctxt (map tych locals)
(if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
else Rules.MP th2 TC)
@@ -845,7 +848,7 @@
val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
- val proved_cases = map (prove_case fconst thy) tasks
+ val proved_cases = map (prove_case ctxt fconst) tasks
val v =
Free (singleton
(Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
@@ -855,14 +858,14 @@
val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
(substs, proved_cases)
val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
- val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
+ val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
val dc = Rules.MP Sinduct dant
val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
- val dc' = fold_rev (Rules.GEN o tych) vars
+ val dc' = fold_rev (Rules.GEN ctxt o tych) vars
(Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
in
- Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
+ Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
end
handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
@@ -911,14 +914,15 @@
else ();
-fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
-let val ctxt = Proof_Context.init_global theory;
- val tych = Thry.typecheck theory;
+fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val tych = Thry.typecheck thy;
(*---------------------------------------------------------------------
* Attempt to eliminate WF condition. It's the only assumption of rules
*---------------------------------------------------------------------*)
- val (rules1,induction1) =
+ val (rules1,induction1) =
let val thm =
Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
@@ -947,7 +951,7 @@
(r,ind)
handle Utils.ERR _ =>
(Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq),
- simplify_induction theory tc_eq ind))
+ simplify_induction thy tc_eq ind))
end
(*----------------------------------------------------------------------
@@ -966,7 +970,7 @@
fun simplify_nested_tc tc =
let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
in
- Rules.GEN_ALL
+ Rules.GEN_ALL ctxt
(Rules.MATCH_MP Thms.eqT tc_eq
handle Utils.ERR _ =>
(Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
--- a/src/HOL/Tools/Transfer/transfer.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Jun 03 21:48:40 2015 +0200
@@ -697,7 +697,7 @@
val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, TFree (a, S)))
val thm2 = thm1
- |> Thm.certify_instantiate (instT, [])
+ |> Thm.certify_instantiate ctxt (instT, [])
|> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
@@ -733,7 +733,7 @@
val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, TFree (a, S)))
val thm2 = thm1
- |> Thm.certify_instantiate (instT, [])
+ |> Thm.certify_instantiate ctxt (instT, [])
|> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
--- a/src/HOL/Tools/choice_specification.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Wed Jun 03 21:48:40 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
--- a/src/HOL/Tools/inductive.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Jun 03 21:48:40 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) =
--- a/src/HOL/Tools/inductive_realizer.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Jun 03 21:48:40 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;
--- a/src/HOL/Tools/recdef.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/recdef.ML Wed Jun 03 21:48:40 2015 +0200
@@ -85,7 +85,7 @@
type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
-structure GlobalRecdefData = Theory_Data
+structure Data = Generic_Data
(
type T = recdef_info Symtab.table * hints;
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
@@ -99,28 +99,15 @@
Thm.merge_thms (wfs1, wfs2)));
);
-val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
-
-fun put_recdef name info thy =
- let
- val (tab, hints) = GlobalRecdefData.get thy;
- val tab' = Symtab.update_new (name, info) tab
- handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
- in GlobalRecdefData.put (tab', hints) thy end;
-
-val get_global_hints = #2 o GlobalRecdefData.get;
+val get_recdef = Symtab.lookup o #1 o Data.get o Context.Theory;
-
-(* proof data *)
+fun put_recdef name info =
+ (Context.theory_map o Data.map o apfst) (fn tab =>
+ Symtab.update_new (name, info) tab
+ handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name));
-structure LocalRecdefData = Proof_Data
-(
- type T = hints;
- val init = get_global_hints;
-);
-
-val get_hints = LocalRecdefData.get;
-fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
+val get_hints = #2 o Data.get o Context.Proof;
+val map_hints = Data.map o apsnd;
(* attributes *)
@@ -155,25 +142,23 @@
-(** prepare_hints(_i) **)
+(** prepare hints **)
-fun prepare_hints thy opt_src =
+fun prepare_hints opt_src ctxt =
let
- val ctxt0 = Proof_Context.init_global thy;
- val ctxt =
+ val ctxt' =
(case opt_src of
- NONE => ctxt0
- | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt0));
+ NONE => ctxt
+ | SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt));
+ val {simps, congs, wfs} = get_hints ctxt';
+ val ctxt'' = ctxt' addsimps simps |> Simplifier.del_cong @{thm imp_cong};
+ in ((rev (map snd congs), wfs), ctxt'') end;
+
+fun prepare_hints_i () ctxt =
+ let
val {simps, congs, wfs} = get_hints ctxt;
val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
- in (ctxt', rev (map snd congs), wfs) end;
-
-fun prepare_hints_i thy () =
- let
- val ctxt = Proof_Context.init_global thy;
- val {simps, congs, wfs} = get_global_hints thy;
- val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
- in (ctxt', rev (map snd congs), wfs) end;
+ in ((rev (map snd congs), wfs), ctxt') end;
@@ -190,30 +175,30 @@
val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
val eq_atts = map (map (prep_att thy)) raw_eq_atts;
- val (ctxt, congs, wfs) = prep_hints thy hints;
+ val ((congs, wfs), ctxt) = prep_hints hints (Proof_Context.init_global thy);
(*We must remove imp_cong to prevent looping when the induction rule
is simplified. Many induction rules have nested implications that would
give rise to looping conditional rewriting.*)
- val ({lhs, rules = rules_idx, induct, tcs}, thy) =
- tfl_fn not_permissive ctxt congs wfs name R eqs thy;
+ val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) =
+ tfl_fn not_permissive congs wfs name R eqs ctxt;
val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
val simp_att =
if null tcs then [Simplifier.simp_add,
Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
else [];
- val ((simps' :: rules', [induct']), thy) =
- thy
+ val ((simps' :: rules', [induct']), thy2) =
+ Proof_Context.theory_of ctxt1
|> Sign.add_path bname
|> Global_Theory.add_thmss
(((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
- val thy =
- thy
+ val thy3 =
+ thy2
|> put_recdef name result
|> Sign.parent_path;
- in (thy, result) end;
+ in (thy3, result) end;
val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints;
fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
--- a/src/HOL/Tools/split_rule.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/HOL/Tools/split_rule.ML Wed Jun 03 21:48:40 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 *)
@@ -54,9 +53,8 @@
(incr_boundvars 1 u) $ Bound 0))
| ap_split' _ _ u = u;
-fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
+fun complete_split_rule_var ctxt (t as Var (v, T), ts) (rl, vs) =
let
- val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl)
val (Us', U') = strip_type T;
val Us = take (length ts) Us';
val U = drop (length ts) Us' ---> U';
@@ -65,17 +63,19 @@
let
val Ts = HOLogic.flatten_tupleT T;
val ys = Name.variant_list xs (replicate (length Ts) a);
- in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
- (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
+ in
+ (xs @ ys,
+ apply2 (Thm.cterm_of ctxt)
+ (v, HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
+ (map (Var o apfst (rpair 0)) (ys ~~ Ts))) :: insts)
end
| mk_tuple _ x = x;
val newt = ap_split' Us U (Var (v, T'));
- val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
val (vs', insts) = fold mk_tuple ts (vs, []);
in
- (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+ (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs')
end
- | complete_split_rule_var _ x = x;
+ | complete_split_rule_var _ _ x = x;
fun collect_vars (Abs (_, _, t)) = collect_vars t
| collect_vars t =
@@ -85,11 +85,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;
@@ -100,7 +100,7 @@
val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
val vars = collect_vars prop [];
in
- fst (fold_rev complete_split_rule_var vars (rl, xs))
+ fst (fold_rev (complete_split_rule_var ctxt) vars (rl, xs))
|> remove_internal_split ctxt
|> Drule.export_without_context
|> Rule_Cases.save rl
--- a/src/Provers/clasimp.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Provers/clasimp.ML Wed Jun 03 21:48:40 2015 +0200
@@ -63,27 +63,26 @@
Failing other cases, A is added as a Safe Intr rule*)
fun add_iff safe unsafe =
- Thm.declaration_attribute (fn th =>
+ Thm.declaration_attribute (fn th => fn context =>
let
val n = Thm.nprems_of th;
val (elim, intro) = if n = 0 then safe else unsafe;
val zero_rotate = zero_var_indexes o rotate_prems n;
- in
- Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #>
- Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
- handle THM _ =>
- (Thm.attribute_declaration elim (zero_rotate (th RS Data.notE))
- handle THM _ => Thm.attribute_declaration intro th)
- end);
+ val decls =
+ [(intro, zero_rotate (th RS Data.iffD2)),
+ (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))]
+ handle THM _ => [(elim, zero_rotate (th RS Data.notE))]
+ handle THM _ => [(intro, th)];
+ in fold (uncurry Thm.attribute_declaration) decls context end);
-fun del_iff del = Thm.declaration_attribute (fn th =>
- let val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th) in
- Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #>
- Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
- handle THM _ =>
- (Thm.attribute_declaration del (zero_rotate (th RS Data.notE))
- handle THM _ => Thm.attribute_declaration del th)
- end);
+fun del_iff del = Thm.declaration_attribute (fn th => fn context =>
+ let
+ val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th);
+ val rls =
+ [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))]
+ handle THM _ => [zero_rotate (th RS Data.notE)]
+ handle THM _ => [th];
+ in fold (Thm.attribute_declaration del) rls context end);
in
--- a/src/Provers/splitter.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Provers/splitter.ML Wed Jun 03 21:48:40 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)
--- a/src/Pure/Isar/code.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/Isar/code.ML Wed Jun 03 21:48:40 2015 +0200
@@ -635,19 +635,19 @@
else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
end;
-fun desymbolize_tvars thms =
+fun desymbolize_tvars thy thms =
let
val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
- in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
+ in map (Thm.global_certify_instantiate thy (tvar_subst, [])) thms end;
-fun desymbolize_vars thm =
+fun desymbolize_vars thy thm =
let
val vs = Term.add_vars (Thm.prop_of thm) [];
val var_subst = mk_desymbolization I I Var vs;
- in Thm.certify_instantiate ([], var_subst) thm end;
+ in Thm.global_certify_instantiate thy ([], var_subst) thm end;
-fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
+fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
(* abstype certificates *)
@@ -706,7 +706,7 @@
in
thm
|> Thm.varifyT_global
- |> Thm.certify_instantiate (inst, [])
+ |> Thm.global_certify_instantiate thy (inst, [])
|> pair subst
end;
@@ -771,7 +771,7 @@
val sorts = map_transpose inter_sorts vss;
val vts = Name.invent_names Name.context Name.aT sorts;
val thms' =
- map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
+ map2 (fn vs => Thm.certify_instantiate ctxt (vs ~~ map TFree vts, [])) vss thms;
val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
fun head_conv ct = if can Thm.dest_comb ct
then Conv.fun_conv head_conv ct
--- a/src/Pure/Isar/proof_context.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jun 03 21:48:40 2015 +0200
@@ -935,7 +935,7 @@
fun comp_hhf_tac ctxt th i st =
PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
- (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
+ (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
fun comp_incr_tac _ [] _ = no_tac
| comp_incr_tac ctxt (th :: ths) i =
--- a/src/Pure/drule.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/drule.ML Wed Jun 03 21:48:40 2015 +0200
@@ -17,7 +17,7 @@
val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
val gen_all: int -> thm -> thm
- val lift_all: cterm -> 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
val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
@@ -192,9 +192,12 @@
(*lift vars wrt. outermost goal parameters
-- reverses the effect of gen_all modulo higher-order unification*)
-fun lift_all goal th =
+fun lift_all ctxt raw_goal raw_th =
let
- val thy = Theory.merge (Thm.theory_of_cterm goal, Thm.theory_of_thm th);
+ val thy = Proof_Context.theory_of ctxt;
+ val goal = Thm.transfer_cterm thy raw_goal;
+ val th = Thm.transfer thy raw_th;
+
val maxidx = Thm.maxidx_of th;
val ps = outer_params (Thm.term_of goal)
|> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
@@ -204,8 +207,8 @@
|> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps)));
in
th
- |> Thm.instantiate (Thm.certify_inst thy ([], inst))
- |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps
+ |> Thm.certify_instantiate ctxt ([], inst)
+ |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
end;
(*direct generalization*)
@@ -225,10 +228,8 @@
| zero_var_indexes_list ths =
let
val thy = Theory.merge_list (map Thm.theory_of_thm ths);
- val inst =
- Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths)
- |> Thm.certify_inst thy;
- in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end;
+ val insts = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+ in map (Thm.adjust_maxidx_thm ~1 o Thm.global_certify_instantiate thy insts) ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
@@ -359,7 +360,7 @@
Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
fun store_standard_thm name th = store_thm name (export_without_context th);
-fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
+fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th);
val reflexive_thm =
let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
--- a/src/Pure/more_thm.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/more_thm.ML Wed Jun 03 21:48:40 2015 +0200
@@ -60,10 +60,15 @@
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
- val certify_inst: theory ->
+ val global_certify_inst: theory ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
(ctyp * ctyp) list * (cterm * cterm) list
- val certify_instantiate:
+ val global_certify_instantiate: theory ->
+ ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
+ val certify_inst: Proof.context ->
+ ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+ (ctyp * ctyp) list * (cterm * cterm) list
+ val certify_instantiate: Proof.context ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
val forall_intr_frees: thm -> thm
val unvarify_global: thm -> thm
@@ -351,12 +356,19 @@
(* certify_instantiate *)
-fun certify_inst thy (instT, inst) =
+fun global_certify_inst thy (instT, inst) =
(map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
-fun certify_instantiate insts th =
- Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
+fun global_certify_instantiate thy insts th =
+ Thm.instantiate (global_certify_inst thy insts) th;
+
+fun certify_inst ctxt (instT, inst) =
+ (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT,
+ map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst);
+
+fun certify_instantiate ctxt insts th =
+ Thm.instantiate (certify_inst ctxt insts) th;
(* forall_intr_frees: generalization over all suitable Free variables *)
@@ -375,6 +387,8 @@
fun unvarify_global 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]);
@@ -383,7 +397,7 @@
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
let val T' = Term_Subst.instantiateT instT T
in (((a, i), T'), Free ((a, T'))) end);
- in certify_instantiate (instT, inst) th end;
+ in global_certify_instantiate thy (instT, inst) th end;
(* close_derivation *)
@@ -444,7 +458,7 @@
val _ = Sign.no_vars ctxt prop;
val (strip, recover, prop') = stripped_sorts thy prop;
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
- val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.global_ctyp_of thy T, S)) strip;
+ val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip;
val thy' = thy
|> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
@@ -461,7 +475,7 @@
fun add_def ctxt unchecked overloaded (b, prop) thy =
let
val _ = Sign.no_vars ctxt prop;
- val prems = map (Thm.global_cterm_of thy) (Logic.strip_imp_prems prop);
+ val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
--- a/src/Pure/subgoal.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/subgoal.ML Wed Jun 03 21:48:40 2015 +0200
@@ -31,7 +31,9 @@
fun gen_focus (do_prems, do_concl) ctxt i raw_st =
let
- val st = Simplifier.norm_hhf_protect ctxt raw_st;
+ val st = raw_st
+ |> Thm.transfer (Proof_Context.theory_of ctxt)
+ |> Simplifier.norm_hhf_protect ctxt;
val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
@@ -40,9 +42,8 @@
else ([], goal);
val text = asms @ (if do_concl then [concl] else []);
- val ((_, schematic_terms), ctxt3) =
- Variable.import_inst true (map Thm.term_of text) ctxt2
- |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
+ val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+ val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
val schematics = (schematic_types, schematic_terms);
val asms' = map (Thm.instantiate_cterm schematics) asms;
--- a/src/Pure/variable.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Pure/variable.ML Wed Jun 03 21:48:40 2015 +0200
@@ -578,9 +578,8 @@
fun importT ths ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
- val insts' as (instT', _) = Thm.certify_inst thy (instT, []);
+ val insts' as (instT', _) = Thm.certify_inst ctxt' (instT, []);
val ths' = map (Thm.instantiate insts') ths;
in ((instT', ths'), ctxt') end;
@@ -592,9 +591,8 @@
fun import is_open ths ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
- val insts' = Thm.certify_inst thy insts;
+ val insts' = Thm.certify_inst ctxt' insts;
val ths' = map (Thm.instantiate insts') ths;
in ((insts', ths'), ctxt') end;
--- a/src/Tools/Code/code_preproc.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Jun 03 21:48:40 2015 +0200
@@ -178,7 +178,7 @@
if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
then (I, ct)
else
- (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global,
+ (Thm.certify_instantiate ctxt (normalization, []) o Thm.varifyT_global,
Thm.cterm_of ctxt (map_types normalize t))
end;
--- a/src/Tools/IsaPlanner/isand.ML Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Wed Jun 03 21:48:40 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 Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Jun 03 21:48:40 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 Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/eqsubst.ML Wed Jun 03 21:48:40 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 Wed Jun 03 09:32:49 2015 +0200
+++ b/src/Tools/misc_legacy.ML Wed Jun 03 21:48:40 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;
-