--- a/src/FOL/simpdata.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/FOL/simpdata.ML Wed Apr 08 19:39:08 2015 +0200
@@ -88,7 +88,7 @@
structure Splitter = Splitter
(
- val thy = @{theory}
+ val context = @{context}
val mk_eq = mk_eq
val meta_eq_to_iff = @{thm meta_eq_to_iff}
val iffD = @{thm iffD2}
--- a/src/HOL/Decision_Procs/approximation.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Wed Apr 08 19:39:08 2015 +0200
@@ -50,7 +50,7 @@
(* Should be in HOL.thy ? *)
fun gen_eval_tac conv ctxt = CONVERSION
- (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
+ (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
THEN' rtac TrueI
val form_equations = @{thms interpret_form_equations};
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Apr 08 19:39:08 2015 +0200
@@ -226,7 +226,7 @@
| SOME instance =>
Object_Logic.full_atomize_tac ctxt i THEN
simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN (* FIXME already part of raw_ferrack_qe_conv? *)
- CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
+ CONVERSION (Object_Logic.judgment_conv ctxt (raw_ferrack_qe_conv ctxt instance)) i THEN
simp_tac ctxt i)); (* FIXME really? *)
end;
--- a/src/HOL/Decision_Procs/langford.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Wed Apr 08 19:39:08 2015 +0200
@@ -261,6 +261,6 @@
THEN (CONVERSION Thm.eta_long_conversion) i
THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
THEN Object_Logic.full_atomize_tac ctxt i
- THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
+ THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
THEN (simp_tac (put_simpset ss ctxt) i)));
end;
\ No newline at end of file
--- a/src/HOL/HOL.thy Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/HOL.thy Wed Apr 08 19:39:08 2015 +0200
@@ -848,7 +848,7 @@
apply (rule prem)
apply assumption
apply (rule allI)+
-apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
+apply (tactic {* eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1 *})
apply iprover
done
--- a/src/HOL/Library/bnf_lfp_countable.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML Wed Apr 08 19:39:08 2015 +0200
@@ -172,7 +172,7 @@
Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
inj_map_strongs')
- |> HOLogic.conj_elims
+ |> HOLogic.conj_elims ctxt
|> Proof_Context.export names_ctxt ctxt
|> map Thm.close_derivation
end;
--- a/src/HOL/Library/rewrite.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Library/rewrite.ML Wed Apr 08 19:39:08 2015 +0200
@@ -143,7 +143,7 @@
| _ => raise TERM ("ft_assm", [t])
fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
- if Object_Logic.is_judgment (Proof_Context.theory_of ctxt) t
+ if Object_Logic.is_judgment ctxt t
then ft_arg ctxt ft
else ft
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 08 19:39:08 2015 +0200
@@ -321,7 +321,7 @@
Config.put Quickcheck.finite_types true #>
Config.put Quickcheck.finite_type_size 1 #>
Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
- (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
+ (false, false) [])) (map (rpair [] o Object_Logic.atomize_term ctxt)
(fst (Variable.import_terms true [t] ctxt)))
end
--- a/src/HOL/Nitpick_Examples/minipick.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML Wed Apr 08 19:39:08 2015 +0200
@@ -409,7 +409,7 @@
| concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
| concrete _ = true
val neg_t =
- @{const Not} $ Object_Logic.atomize_term thy t
+ @{const Not} $ Object_Logic.atomize_term ctxt t
|> map_types unsetify_type
val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
val frees = Term.add_frees neg_t []
--- a/src/HOL/Nominal/nominal_induct.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Wed Apr 08 19:39:08 2015 +0200
@@ -93,7 +93,7 @@
fun rule_cases ctxt r =
let val r' = if simp then Induct.simplified_rule ctxt r else r
- in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
+ in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
in
(fn i => fn st =>
rules
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 08 19:39:08 2015 +0200
@@ -1243,10 +1243,9 @@
fun presimp_prop ctxt type_enc t =
let
- val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
|> transform_elim_prop
- |> Object_Logic.atomize_term thy
+ |> Object_Logic.atomize_term ctxt
val need_trueprop = (fastype_of t = @{typ bool})
val is_ho = is_type_enc_higher_order type_enc
in
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Wed Apr 08 19:39:08 2015 +0200
@@ -445,7 +445,7 @@
let
val thy = Proof_Context.theory_of ctxt
- val preproc = Object_Logic.atomize_term thy
+ val preproc = Object_Logic.atomize_term ctxt
val conditions = map preproc hyps_t0
val consequence = preproc concl_t0
--- a/src/HOL/Tools/Function/induction_schema.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Wed Apr 08 19:39:08 2015 +0200
@@ -188,14 +188,12 @@
fun mk_ind_goal ctxt branches =
let
- val thy = Proof_Context.theory_of ctxt
-
fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
HOLogic.mk_Trueprop (list_comb (P, map Free xs))
|> fold_rev (curry Logic.mk_implies) Cs
|> fold_rev (Logic.all o Free) ws
|> term_conv ctxt (ind_atomize ctxt)
- |> Object_Logic.drop_judgment thy
+ |> Object_Logic.drop_judgment ctxt
|> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
in
Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches)
--- a/src/HOL/Tools/Function/termination.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Function/termination.ML Wed Apr 08 19:39:08 2015 +0200
@@ -32,8 +32,6 @@
val decompose_tac : Proof.context -> ttac
end
-
-
structure Termination : TERMINATION =
struct
@@ -275,14 +273,13 @@
fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
let
- val thy = Proof_Context.theory_of ctxt
val ((_ $ (_ $ rel)) :: ineqs) = Thm.prems_of st
fun mk_compr ineq =
let
val (vars, prems, lhs, rhs) = dest_term ineq
in
- mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
+ mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term ctxt) prems)
end
val relation =
@@ -360,5 +357,4 @@
else solve_trivial_tac D i
end)
-
end
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Apr 08 19:39:08 2015 +0200
@@ -300,7 +300,7 @@
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
val nondefs =
- nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
+ nondefs |> filter_out (is_choice_spec_axiom ctxt choice_spec_table)
val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Apr 08 19:39:08 2015 +0200
@@ -218,7 +218,7 @@
val nondef_props_for_const :
theory -> bool -> const_table -> string * typ -> term list
val is_choice_spec_fun : hol_context -> string * typ -> bool
- val is_choice_spec_axiom : theory -> const_table -> term -> bool
+ val is_choice_spec_axiom : Proof.context -> const_table -> term -> bool
val is_raw_equational_fun : hol_context -> string * typ -> bool
val is_equational_fun : hol_context -> string * typ -> bool
val codatatype_bisim_axioms : hol_context -> typ -> term list
@@ -1548,13 +1548,13 @@
| unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
| unvarify_term t = t
-fun axiom_for_choice_spec thy =
+fun axiom_for_choice_spec ctxt =
unvarify_term
- #> Object_Logic.atomize_term thy
+ #> Object_Logic.atomize_term ctxt
#> Choice_Specification.close_form
#> HOLogic.mk_Trueprop
-fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
+fun is_choice_spec_fun ({thy, ctxt, def_tables, nondef_table, choice_spec_table, ...}
: hol_context) x =
case nondef_props_for_const thy true choice_spec_table x of
[] => false
@@ -1565,7 +1565,7 @@
let val ts' = nondef_props_for_const thy true nondef_table x in
length ts' = length ts andalso
forall (fn t =>
- exists (curry (op aconv) (axiom_for_choice_spec thy t))
+ exists (curry (op aconv) (axiom_for_choice_spec ctxt t))
ts') ts
end
@@ -2074,10 +2074,10 @@
exception NO_TRIPLE of unit
-fun triple_for_intro_rule thy x t =
+fun triple_for_intro_rule ctxt x t =
let
- val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
- val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
+ val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term ctxt)
+ val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term ctxt
val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
val is_good_head = curry (op =) (Const x) o head_of
in
@@ -2122,7 +2122,7 @@
[] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
[Const x])
| intro_ts =>
- (case map (triple_for_intro_rule thy x) intro_ts
+ (case map (triple_for_intro_rule ctxt x) intro_ts
|> filter_out (null o #2) of
[] => true
| triples =>
@@ -2149,7 +2149,7 @@
SOME wf => wf
| NONE =>
let
- val goal = prop |> Thm.global_cterm_of thy |> Goal.init
+ val goal = prop |> Thm.cterm_of ctxt |> Goal.init
val wf = exists (terminates_by ctxt tac_timeout goal)
termination_tacs
in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Apr 08 19:39:08 2015 +0200
@@ -1050,7 +1050,7 @@
fun try_out negate =
let
val concl = (negate ? curry (op $) @{const Not})
- (Object_Logic.atomize_term thy prop)
+ (Object_Logic.atomize_term ctxt prop)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
|> map_types (map_type_tfree
(fn (s, []) => TFree (s, @{sort type})
@@ -1062,7 +1062,7 @@
|> writeln
else
()
- val goal = prop |> Thm.global_cterm_of thy |> Goal.init
+ val goal = prop |> Thm.cterm_of ctxt |> Goal.init
in
(goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
|> the |> Goal.finish ctxt; true)
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Apr 08 19:39:08 2015 +0200
@@ -236,7 +236,7 @@
val rewrs = map (swap o dest) @{thms all_simps} @
(map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
@{thm bot_fun_def}, @{thm less_bool_def}])
- val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
+ val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
val (vs, body) = strip_all t'
val vs' = Variable.variant_frees ctxt [t'] vs
in
--- a/src/HOL/Tools/SMT/smtlib_isar.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML Wed Apr 08 19:39:08 2015 +0200
@@ -44,7 +44,7 @@
fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
let val thy = Proof_Context.theory_of ctxt in
Raw_Simplifier.rewrite_term thy rewrite_rules []
- #> Object_Logic.atomize_term thy
+ #> Object_Logic.atomize_term ctxt
#> not (null ll_defs) ? unlift_term ll_defs
#> simplify_bool
#> unskolemize_names ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Apr 08 19:39:08 2015 +0200
@@ -428,10 +428,9 @@
fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
if Config.get ctxt instantiate_inducts then
let
- val thy = Proof_Context.theory_of ctxt
val ind_stmt =
(hyp_ts |> filter_out (null o external_frees), concl_t)
- |> Logic.list_implies |> Object_Logic.atomize_term thy
+ |> Logic.list_implies |> Object_Logic.atomize_term ctxt
val ind_stmt_xs = external_frees ind_stmt
in
maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
--- a/src/HOL/Tools/coinduction.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/coinduction.ML Wed Apr 08 19:39:08 2015 +0200
@@ -98,9 +98,9 @@
DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
(case prems of
[] => all_tac
- | inv::case_prems =>
+ | inv :: case_prems =>
let
- val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
+ val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
val inv_thms = init @ [last];
val eqs = take e inv_thms;
fun is_local_var t =
@@ -115,7 +115,7 @@
end) ctxt) THEN'
K (prune_params_tac ctxt))
#> Seq.maps (fn st =>
- CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of st) cases) all_tac st)
+ CASES (Rule_Cases.make_common ctxt (Thm.prop_of st) cases) all_tac st)
end));
local
--- a/src/HOL/Tools/groebner.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/groebner.ML Wed Apr 08 19:39:08 2015 +0200
@@ -677,13 +677,13 @@
fun refute ctxt tm =
if tm aconvc false_tm then assume_Trueprop tm else
((let
- val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
+ val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims ctxt (assume_Trueprop tm))
val nths = filter (is_eq o Thm.dest_arg o concl) nths0
val eths = filter (is_eq o concl) eths0
in
if null eths then
let
- val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
+ val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
val th2 =
Conv.fconv_rule
((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
@@ -703,13 +703,13 @@
end
else
let
- val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
+ val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
val (vars,pol::pols) =
grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
val (deg,l,cert) = grobner_strong vars pols pol
val th1 =
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth
- val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr th1) neq_01
+ val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
in (vars,l,cert,th2)
end)
val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c >/ rat_0) p)) cert
@@ -724,7 +724,7 @@
(nth eths i |> mk_meta_eq)) pols)
val th1 = thm_fn herts_pos
val th2 = thm_fn herts_neg
- val th3 = HOLogic.conj_intr(mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
+ val th3 = HOLogic.conj_intr ctxt (mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
val th4 =
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
(neq_rule l th3)
@@ -931,7 +931,7 @@
Object_Logic.full_atomize_tac ctxt
THEN' presimplify ctxt add_ths del_ths
THEN' CSUBGOAL (fn (p, i) =>
- rtac (let val form = Object_Logic.dest_judgment p
+ rtac (let val form = Object_Logic.dest_judgment ctxt p
in case get_ring_ideal_convs ctxt form of
NONE => Thm.reflexive form
| SOME thy => #ring_conv thy ctxt form
--- a/src/HOL/Tools/hologic.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/hologic.ML Wed Apr 08 19:39:08 2015 +0200
@@ -24,9 +24,9 @@
val mk_set: typ -> term list -> term
val dest_set: term -> term list
val mk_UNIV: typ -> term
- val conj_intr: thm -> thm -> thm
- val conj_elim: thm -> thm * thm
- val conj_elims: thm -> thm list
+ val conj_intr: Proof.context -> thm -> thm -> thm
+ val conj_elim: Proof.context -> thm -> thm * thm
+ val conj_elims: Proof.context -> thm -> thm list
val conj: term
val disj: term
val imp: term
@@ -203,25 +203,25 @@
| _ => raise CTERM ("Trueprop_conv", [ct]))
-fun conj_intr thP thQ =
+fun conj_intr ctxt thP thQ =
let
- val (P, Q) = apply2 (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
+ val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
-fun conj_elim thPQ =
+fun conj_elim ctxt thPQ =
let
- val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
+ val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
in (thP, thQ) end;
-fun conj_elims th =
- let val (th1, th2) = conj_elim th
- in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
+fun conj_elims ctxt th =
+ let val (th1, th2) = conj_elim ctxt th
+ in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th];
val conj = @{term HOL.conj}
and disj = @{term HOL.disj}
--- a/src/HOL/Tools/simpdata.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Tools/simpdata.ML Wed Apr 08 19:39:08 2015 +0200
@@ -147,7 +147,7 @@
structure Splitter = Splitter
(
- val thy = @{theory}
+ val context = @{context}
val mk_eq = mk_eq
val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
val iffD = @{thm iffD2}
--- a/src/HOL/Topological_Spaces.thy Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Apr 08 19:39:08 2015 +0200
@@ -445,14 +445,13 @@
ML {*
fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
let
- val thy = Proof_Context.theory_of ctxt
val mp_thms = thms RL [@{thm eventually_rev_mp}]
val raw_elim_thm =
(@{thm allI} RS @{thm always_eventually})
|> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
|> fold (fn _ => fn thm => @{thm impI} RS thm) thms
val cases_prop = Thm.prop_of (raw_elim_thm RS st)
- val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
+ val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
in
CASES cases (rtac raw_elim_thm 1)
end) 1
--- a/src/Provers/classical.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Provers/classical.ML Wed Apr 08 19:39:08 2015 +0200
@@ -72,7 +72,7 @@
val deepen_tac: Proof.context -> int -> int -> tactic
val contr_tac: Proof.context -> int -> tactic
- val dup_elim: Context.generic option -> thm -> thm
+ val dup_elim: Proof.context -> thm -> thm
val dup_intr: thm -> thm
val dup_step_tac: Proof.context -> int -> tactic
val eq_mp_tac: Proof.context -> int -> tactic
@@ -96,7 +96,7 @@
signature CLASSICAL =
sig
include BASIC_CLASSICAL
- val classical_rule: thm -> thm
+ val classical_rule: Proof.context -> thm -> thm
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
val rep_cs: claset ->
{safeIs: thm Item_Net.T,
@@ -144,8 +144,8 @@
[| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
*)
-fun classical_rule rule =
- if is_some (Object_Logic.elim_concl rule) then
+fun classical_rule ctxt rule =
+ if is_some (Object_Logic.elim_concl ctxt rule) then
let
val rule' = rule RS Data.classical;
val concl' = Thm.concl_of rule';
@@ -165,13 +165,8 @@
else rule;
(*flatten nested meta connectives in prems*)
-fun flat_rule opt_context th =
- let
- val ctxt =
- (case opt_context of
- NONE => Proof_Context.init_global (Thm.theory_of_thm th)
- | SOME context => Context.proof_of context);
- in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
+fun flat_rule ctxt =
+ Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt));
(*** Useful tactics for classical reasoning ***)
@@ -206,13 +201,8 @@
(*Duplication of hazardous rules, for complete provers*)
fun dup_intr th = zero_var_indexes (th RS Data.classical);
-fun dup_elim context th =
- let
- val ctxt =
- (case context of
- SOME c => Context.proof_of c
- | NONE => Proof_Context.init_global (Thm.theory_of_thm th));
- val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
+fun dup_elim ctxt th =
+ let val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end;
@@ -259,6 +249,9 @@
In case of overlap, new rules are tried BEFORE old ones!!
***)
+fun default_context (SOME context) _ = Context.proof_of context
+ | default_context NONE th = Proof_Context.init_global (Thm.theory_of_thm th);
+
(*For use with biresolve_tac. Combines intro rules with swap to handle negated
assumptions. Pairs elim rules with true. *)
fun joinrules (intrs, elims) =
@@ -320,7 +313,8 @@
if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
else
let
- val th' = flat_rule context th;
+ val ctxt = default_context context th;
+ val th' = flat_rule ctxt th;
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
List.partition Thm.no_prems [th'];
val nI = Item_Net.length safeIs + 1;
@@ -349,7 +343,8 @@
error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
let
- val th' = classical_rule (flat_rule context th);
+ val ctxt = default_context context th;
+ val th' = classical_rule ctxt (flat_rule ctxt th);
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
List.partition (fn rl => Thm.nprems_of rl=1) [th'];
val nI = Item_Net.length safeIs;
@@ -381,7 +376,8 @@
if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
else
let
- val th' = flat_rule context th;
+ val ctxt = default_context context th;
+ val th' = flat_rule ctxt th;
val nI = Item_Net.length hazIs + 1;
val nE = Item_Net.length hazEs;
val _ = warn_claset context th cs;
@@ -410,7 +406,8 @@
error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
let
- val th' = classical_rule (flat_rule context th);
+ val ctxt = default_context context th;
+ val th' = classical_rule ctxt (flat_rule ctxt th);
val nI = Item_Net.length hazIs;
val nE = Item_Net.length hazEs + 1;
val _ = warn_claset context th cs;
@@ -418,7 +415,7 @@
CS
{hazEs = Item_Net.update th hazEs,
haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
- dup_netpair = insert (nI, nE) ([], [dup_elim context th']) dup_netpair,
+ dup_netpair = insert (nI, nE) ([], [dup_elim ctxt th']) dup_netpair,
safeIs = safeIs,
safeEs = safeEs,
hazIs = hazIs,
@@ -443,7 +440,8 @@
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member safeIs th then
let
- val th' = flat_rule context th;
+ val ctxt = default_context context th;
+ val th' = flat_rule ctxt th;
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
in
CS
@@ -466,7 +464,8 @@
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member safeEs th then
let
- val th' = classical_rule (flat_rule context th);
+ val ctxt = default_context context th;
+ val th' = classical_rule ctxt (flat_rule ctxt th);
val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th'];
in
CS
@@ -488,7 +487,10 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member hazIs th then
- let val th' = flat_rule context th in
+ let
+ val ctxt = default_context context th;
+ val th' = flat_rule ctxt th;
+ in
CS
{haz_netpair = delete ([th'], []) haz_netpair,
dup_netpair = delete ([dup_intr th'], []) dup_netpair,
@@ -510,10 +512,13 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if Item_Net.member hazEs th then
- let val th' = classical_rule (flat_rule context th) in
+ let
+ val ctxt = default_context context th;
+ val th' = classical_rule ctxt (flat_rule ctxt th);
+ in
CS
{haz_netpair = delete ([], [th']) haz_netpair,
- dup_netpair = delete ([], [dup_elim context th']) dup_netpair,
+ dup_netpair = delete ([], [dup_elim ctxt th']) dup_netpair,
safeIs = safeIs,
safeEs = safeEs,
hazIs = hazIs,
--- a/src/Provers/splitter.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Provers/splitter.ML Wed Apr 08 19:39:08 2015 +0200
@@ -9,7 +9,7 @@
signature SPLITTER_DATA =
sig
- val thy : theory
+ val context : Proof.context
val mk_eq : thm -> thm
val meta_eq_to_iff: thm (* "x == y ==> x = y" *)
val iffD : thm (* "[| P = Q; Q |] ==> P" *)
@@ -43,14 +43,14 @@
struct
val Const (const_not, _) $ _ =
- Object_Logic.drop_judgment Data.thy
+ Object_Logic.drop_judgment Data.context
(#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
val Const (const_or , _) $ _ $ _ =
- Object_Logic.drop_judgment Data.thy
+ Object_Logic.drop_judgment Data.context
(#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
-val const_Trueprop = Object_Logic.judgment_name Data.thy;
+val const_Trueprop = Object_Logic.judgment_name Data.context;
fun split_format_err () = error "Wrong format for split rule";
--- a/src/Pure/Isar/auto_bind.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML Wed Apr 08 19:39:08 2015 +0200
@@ -9,8 +9,8 @@
val thesisN: string
val thisN: string
val assmsN: string
- val goal: theory -> term list -> (indexname * term option) list
- val facts: theory -> term list -> (indexname * term option) list
+ val goal: Proof.context -> term list -> (indexname * term option) list
+ val facts: Proof.context -> term list -> (indexname * term option) list
val no_facts: (indexname * term option) list
end;
@@ -23,29 +23,29 @@
val thisN = "this";
val assmsN = "assms";
-fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
+fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
-fun statement_binds thy name prop =
- [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))];
+fun statement_binds ctxt name prop =
+ [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment ctxt prop)))];
(* goal *)
-fun goal thy [prop] = statement_binds thy thesisN prop
+fun goal ctxt [prop] = statement_binds ctxt thesisN prop
| goal _ _ = [((thesisN, 0), NONE)];
(* facts *)
-fun get_arg thy prop =
- (case strip_judgment thy prop of
+fun get_arg ctxt prop =
+ (case strip_judgment ctxt prop of
_ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
| _ => NONE);
fun facts _ [] = []
- | facts thy props =
+ | facts ctxt props =
let val prop = List.last props
- in [(Syntax_Ext.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
+ in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)];
--- a/src/Pure/Isar/element.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/element.ML Wed Apr 08 19:39:08 2015 +0200
@@ -197,13 +197,12 @@
local
-fun standard_elim th =
- (case Object_Logic.elim_concl th of
+fun standard_elim ctxt th =
+ (case Object_Logic.elim_concl ctxt th of
SOME C =>
let
- val thy = Thm.theory_of_thm th;
val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
- val th' = Thm.instantiate ([], [(Thm.global_cterm_of thy C, Thm.global_cterm_of thy thesis)]) th;
+ val th' = Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (C, thesis)]) th;
in (th', true) end
| NONE => (th, false));
@@ -227,13 +226,11 @@
fun pretty_statement ctxt kind raw_th =
let
- val thy = Proof_Context.theory_of ctxt;
-
- val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf ctxt raw_th);
+ val (th, is_elim) = standard_elim ctxt (Raw_Simplifier.norm_hhf ctxt raw_th);
val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
val prop = Thm.prop_of th';
val (prems, concl) = Logic.strip_horn prop;
- val concl_term = Object_Logic.drop_judgment thy concl;
+ val concl_term = Object_Logic.drop_judgment ctxt concl;
val fixes = fold_aterms (fn v as Free (x, T) =>
if Variable.is_newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
--- a/src/Pure/Isar/expression.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/expression.ML Wed Apr 08 19:39:08 2015 +0200
@@ -622,16 +622,15 @@
val introN = "intro";
-fun atomize_spec thy ts =
+fun atomize_spec ctxt ts =
let
val t = Logic.mk_conjunction_balanced ts;
- val body = Object_Logic.atomize_term thy t;
+ val body = Object_Logic.atomize_term ctxt t;
val bodyT = Term.fastype_of body;
in
if bodyT = propT
- then (t, propT, Thm.reflexive (Thm.global_cterm_of thy t))
- else
- (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t))
+ then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t))
+ else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t))
end;
(* achieve plain syntax for locale predicates (without "PROP") *)
@@ -658,7 +657,9 @@
let
val name = Sign.full_name thy binding;
- val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
+ val thy_ctxt = Proof_Context.init_global thy;
+
+ val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts;
val env = Term.add_free_names body [];
val xs = filter (member (op =) env o #1) parms;
val Ts = map #2 xs;
@@ -669,7 +670,7 @@
val args = map Logic.mk_type extraTs @ map Free xs;
val head = Term.list_comb (Const (name, predT), args);
- val statement = Object_Logic.ensure_propT thy head;
+ val statement = Object_Logic.ensure_propT thy_ctxt head;
val ([pred_def], defs_thy) =
thy
--- a/src/Pure/Isar/object_logic.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML Wed Apr 08 19:39:08 2015 +0200
@@ -6,26 +6,26 @@
signature OBJECT_LOGIC =
sig
- val get_base_sort: theory -> sort option
+ val get_base_sort: Proof.context -> sort option
val add_base_sort: sort -> theory -> theory
val add_judgment: binding * typ * mixfix -> theory -> theory
val add_judgment_cmd: binding * string * mixfix -> theory -> theory
- val judgment_name: theory -> string
- val is_judgment: theory -> term -> bool
- val drop_judgment: theory -> term -> term
- val fixed_judgment: theory -> string -> term
- val ensure_propT: theory -> term -> term
- val dest_judgment: cterm -> cterm
- val judgment_conv: conv -> conv
- val elim_concl: thm -> term option
+ val judgment_name: Proof.context -> string
+ val is_judgment: Proof.context -> term -> bool
+ val drop_judgment: Proof.context -> term -> term
+ val fixed_judgment: Proof.context -> string -> term
+ val ensure_propT: Proof.context -> term -> term
+ val dest_judgment: Proof.context -> cterm -> cterm
+ val judgment_conv: Proof.context -> conv -> conv
+ val elim_concl: Proof.context -> thm -> term option
val declare_atomize: attribute
val declare_rulify: attribute
- val atomize_term: theory -> term -> term
+ val atomize_term: Proof.context -> term -> term
val atomize: Proof.context -> conv
val atomize_prems: Proof.context -> conv
val atomize_prems_tac: Proof.context -> int -> tactic
val full_atomize_tac: Proof.context -> int -> tactic
- val rulify_term: theory -> term -> term
+ val rulify_term: Proof.context -> term -> term
val rulify_tac: Proof.context -> int -> tactic
val rulify: Proof.context -> thm -> thm
val rulify_no_asm: Proof.context -> thm -> thm
@@ -36,7 +36,7 @@
structure Object_Logic: OBJECT_LOGIC =
struct
-(** theory data **)
+(** context data **)
datatype data = Data of
{base_sort: sort option,
@@ -46,7 +46,7 @@
fun make_data (base_sort, judgment, atomize_rulify) =
Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
-structure Data = Theory_Data
+structure Data = Generic_Data
(
type T = data;
val empty = make_data (NONE, NONE, ([], []));
@@ -66,7 +66,7 @@
fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
make_data (f (base_sort, judgment, atomize_rulify)));
-fun get_data thy = Data.get thy |> (fn Data args => args);
+fun get_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data args => args);
@@ -76,9 +76,10 @@
val get_base_sort = #base_sort o get_data;
-fun add_base_sort S = map_data (fn (base_sort, judgment, atomize_rulify) =>
- if is_some base_sort then error "Attempt to redeclare object-logic base sort"
- else (SOME S, judgment, atomize_rulify));
+fun add_base_sort S =
+ (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
+ if is_some base_sort then error "Attempt to redeclare object-logic base sort"
+ else (SOME S, judgment, atomize_rulify));
(* add judgment *)
@@ -90,7 +91,7 @@
thy
|> add_consts [(b, T, mx)]
|> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
- |> map_data (fn (base_sort, judgment, atomize_rulify) =>
+ |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
if is_some judgment then error "Attempt to redeclare object-logic judgment"
else (base_sort, SOME c, atomize_rulify))
end;
@@ -105,51 +106,50 @@
(* judgments *)
-fun judgment_name thy =
- (case #judgment (get_data thy) of
+fun judgment_name ctxt =
+ (case #judgment (get_data ctxt) of
SOME name => name
| _ => raise TERM ("Unknown object-logic judgment", []));
-fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
+fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
| is_judgment _ _ = false;
-fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
- | drop_judgment thy (tm as (Const (c, _) $ t)) =
- if (c = judgment_name thy handle TERM _ => false) then t else tm
+fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
+ | drop_judgment ctxt (tm as (Const (c, _) $ t)) =
+ if (c = judgment_name ctxt handle TERM _ => false) then t else tm
| drop_judgment _ tm = tm;
-fun fixed_judgment thy x =
+fun fixed_judgment ctxt x =
let (*be robust wrt. low-level errors*)
- val c = judgment_name thy;
+ val c = judgment_name ctxt;
val aT = TFree (Name.aT, []);
val T =
- the_default (aT --> propT) (Sign.const_type thy c)
+ the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
|> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
val U = Term.domain_type T handle Match => aT;
in Const (c, T) $ Free (x, U) end;
-fun ensure_propT thy t =
+fun ensure_propT ctxt t =
let val T = Term.fastype_of t
- in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
+ in if T = propT then t else Const (judgment_name ctxt, T --> propT) $ t end;
-fun dest_judgment ct =
- if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+fun dest_judgment ctxt ct =
+ if is_judgment ctxt (Thm.term_of ct)
then Thm.dest_arg ct
else raise CTERM ("dest_judgment", [ct]);
-fun judgment_conv cv ct =
- if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+fun judgment_conv ctxt cv ct =
+ if is_judgment ctxt (Thm.term_of ct)
then Conv.arg_conv cv ct
else raise CTERM ("judgment_conv", [ct]);
(* elimination rules *)
-fun elim_concl rule =
+fun elim_concl ctxt rule =
let
- val thy = Thm.theory_of_thm rule;
val concl = Thm.concl_of rule;
- val C = drop_judgment thy concl;
+ val C = drop_judgment ctxt concl;
in
if Term.is_Var C andalso
exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
@@ -171,19 +171,19 @@
fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
(base_sort, judgment, (atomize, Thm.add_thm th rulify)));
-val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
-val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
+val declare_atomize = Thm.declaration_attribute add_atomize;
+val declare_rulify = Thm.declaration_attribute add_rulify;
-val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
+val _ = Theory.setup (fold (Context.theory_map o add_rulify) Drule.norm_hhf_eqs);
(* atomize *)
-fun atomize_term thy =
- drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
+fun atomize_term ctxt =
+ drop_judgment ctxt o
+ Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) [];
-fun atomize ctxt =
- Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
+fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt);
fun atomize_prems ctxt ct =
if Logic.has_meta_prems (Thm.term_of ct) then
@@ -196,11 +196,13 @@
(* rulify *)
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
-fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
+fun rulify_term ctxt =
+ Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_rulify ctxt) [];
+
+fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt);
fun gen_rulify full ctxt =
- Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
+ Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
#> Drule.gen_all (Variable.maxidx_of ctxt)
#> Thm.strip_shyps
#> Drule.zero_var_indexes;
--- a/src/Pure/Isar/obtain.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Apr 08 19:39:08 2015 +0200
@@ -73,10 +73,8 @@
fun eliminate fix_ctxt rule xs As thm =
let
- val thy = Proof_Context.theory_of fix_ctxt;
-
val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
- val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
+ val _ = Object_Logic.is_judgment fix_ctxt (Thm.concl_of thm) orelse
error "Conclusion in obtained context must be object-logic judgment";
val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
@@ -99,9 +97,8 @@
fun bind_judgment ctxt name =
let
- val thy = Proof_Context.theory_of ctxt;
val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
- val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x;
+ val (t as _ $ Free v) = Object_Logic.fixed_judgment ctxt x;
in ((v, t), ctxt') end;
val thatN = "that";
--- a/src/Pure/Isar/proof.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/proof.ML Wed Apr 08 19:39:08 2015 +0200
@@ -406,9 +406,8 @@
fun no_goal_cases st = map (rpair NONE) (goals st);
-fun goal_cases st =
- Rule_Cases.make_common
- (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
+fun goal_cases ctxt st =
+ Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
fun apply_method text ctxt state =
#2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} =>
@@ -416,7 +415,7 @@
|> Seq.map (fn (meth_cases, goal') =>
state
|> map_goal
- (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
+ (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #>
Proof_Context.update_cases true meth_cases)
(K (statement, using, goal', before_qed, after_qed)) I));
--- a/src/Pure/Isar/proof_context.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Apr 08 19:39:08 2015 +0200
@@ -842,7 +842,7 @@
fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
| drop_schematic b = b;
-fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
+fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f ctxt ts));
val auto_bind_goal = auto_bind Auto_Bind.goal;
val auto_bind_facts = auto_bind Auto_Bind.facts;
--- a/src/Pure/Isar/rule_cases.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML Wed Apr 08 19:39:08 2015 +0200
@@ -27,9 +27,9 @@
cases: (string * T) list}
val case_hypsN: string
val strip_params: term -> (string * typ) list
- val make_common: theory * term ->
+ val make_common: Proof.context -> term ->
((string * string list) * string list) list -> cases
- val make_nested: term -> theory * term ->
+ val make_nested: Proof.context -> term -> term ->
((string * string list) * string list) list -> cases
val apply: term list -> T -> T
val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
@@ -107,9 +107,9 @@
fun bindings args = map (apfst Binding.name) args;
-fun extract_case thy (case_outline, raw_prop) name hyp_names concls =
+fun extract_case ctxt (case_outline, raw_prop) name hyp_names concls =
let
- val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
+ val props = Logic.dest_conjunctions (Drule.norm_hhf (Proof_Context.theory_of ctxt) raw_prop);
val len = length props;
val nested = is_some case_outline andalso len > 1;
@@ -126,7 +126,7 @@
extract_assumes name hyp_names case_outline prop
|> apply2 (map (apsnd (maps Logic.dest_conjunctions)));
- val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
+ val concl = Object_Logic.drop_judgment ctxt (Logic.strip_assums_concl prop);
val binds =
(case_conclN, concl) :: dest_binops concls concl
|> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
@@ -152,7 +152,7 @@
else SOME (nested_case (hd cases))
end;
-fun make rule_struct (thy, prop) cases =
+fun make ctxt rule_struct prop cases =
let
val n = length cases;
val nprems = Logic.count_prems prop;
@@ -160,13 +160,13 @@
((case try (fn () =>
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
NONE => (name, NONE)
- | SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1);
+ | SOME p => (name, extract_case ctxt p name hyp_names concls)) :: cs, i - 1);
in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
in
-val make_common = make NONE;
-fun make_nested rule_struct = make (SOME rule_struct);
+fun make_common ctxt = make ctxt NONE;
+fun make_nested ctxt rule_struct = make ctxt (SOME rule_struct);
fun apply args =
let
--- a/src/Pure/Isar/specification.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/specification.ML Wed Apr 08 19:39:08 2015 +0200
@@ -356,7 +356,7 @@
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
- val thesis = Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) Auto_Bind.thesisN;
+ val thesis = Object_Logic.fixed_judgment ctxt Auto_Bind.thesisN;
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
--- a/src/Pure/Isar/typedecl.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML Wed Apr 08 19:39:08 2015 +0200
@@ -26,11 +26,6 @@
(* primitives *)
-fun object_logic_arity name thy =
- (case Object_Logic.get_base_sort thy of
- NONE => thy
- | SOME S => Axclass.arity_axiomatization (name, replicate (Sign.arity_number thy name) S, S) thy);
-
fun basic_decl decl (b, n, mx) lthy =
let val name = Local_Theory.full_name lthy b in
lthy
@@ -41,8 +36,11 @@
end;
fun basic_typedecl (b, n, mx) lthy =
- basic_decl (fn name => Sign.add_type lthy (b, n, NoSyn) #> object_logic_arity name)
- (b, n, mx) lthy;
+ basic_decl (fn name =>
+ Sign.add_type lthy (b, n, NoSyn) #>
+ (case Object_Logic.get_base_sort lthy of
+ SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
+ | NONE => I)) (b, n, mx) lthy;
(* global type -- without dependencies on type parameters of the context *)
--- a/src/Pure/Thy/term_style.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Thy/term_style.ML Wed Apr 08 19:39:08 2015 +0200
@@ -49,8 +49,7 @@
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
let
- val concl =
- Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
+ val concl = Object_Logic.drop_judgment ctxt (Logic.strip_imp_concl t);
in
(case concl of
_ $ l $ r => proj (l, r)
--- a/src/Pure/Tools/find_theorems.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Apr 08 19:39:08 2015 +0200
@@ -89,7 +89,7 @@
(* matching theorems *)
-fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
+fun is_nontrivial ctxt = Term.is_Const o Term.head_of o Object_Logic.drop_judgment ctxt;
(*extract terms from term_src, refine them to the parts that concern us,
if po try match them against obj else vice versa.
@@ -100,7 +100,7 @@
val thy = Proof_Context.theory_of ctxt;
fun matches pat =
- is_nontrivial thy pat andalso
+ is_nontrivial ctxt pat andalso
Pattern.matches thy (if po then (pat, obj) else (obj, pat));
fun subst_size pat =
@@ -171,8 +171,7 @@
in
(*elim rules always have assumptions, so an elim with one
assumption is as good as an intro rule with none*)
- if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm)
- andalso not (null successful) then
+ if is_nontrivial ctxt (Thm.major_prem_of thm) andalso not (null successful) then
SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
else NONE
end
--- a/src/Tools/atomize_elim.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Tools/atomize_elim.ML Wed Apr 08 19:39:08 2015 +0200
@@ -55,7 +55,7 @@
fun atomize_elim_conv ctxt ct =
(forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems)
- then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
+ then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct'
then all_conv ct'
else raise CTERM ("atomize_elim", [ct', ct])))
ct
--- a/src/Tools/induct.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Tools/induct.ML Wed Apr 08 19:39:08 2015 +0200
@@ -59,11 +59,11 @@
val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
(term option list * thm list) * Proof.context
- val atomize_term: theory -> term -> term
+ val atomize_term: Proof.context -> term -> term
val atomize_cterm: Proof.context -> conv
val atomize_tac: Proof.context -> int -> tactic
val inner_atomize_tac: Proof.context -> int -> tactic
- val rulified_term: thm -> theory * term
+ val rulified_term: Proof.context -> thm -> term
val rulify_tac: Proof.context -> int -> tactic
val simplified_rule: Proof.context -> thm -> thm
val simplify_tac: Proof.context -> int -> tactic
@@ -75,7 +75,7 @@
thm list -> int -> cases_tactic
val get_inductT: Proof.context -> term option list list -> thm list list
type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
- val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
+ val gen_induct_tac: (case_data * thm -> case_data * thm) ->
Proof.context -> bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
@@ -137,14 +137,12 @@
Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
Conv.rewr_conv Drule.swap_prems_eq
-fun drop_judgment ctxt = Object_Logic.drop_judgment (Proof_Context.theory_of ctxt);
-
fun find_eq ctxt t =
let
val l = length (Logic.strip_params t);
val Hs = Logic.strip_assums_hyp t;
fun find (i, t) =
- (case Induct_Args.dest_def (drop_judgment ctxt t) of
+ (case Induct_Args.dest_def (Object_Logic.drop_judgment ctxt t) of
SOME (Bound j, _) => SOME (i, j)
| SOME (_, Bound j) => SOME (i, j)
| _ => NONE);
@@ -181,7 +179,7 @@
fun rulify_defs_conv ctxt ct =
if exists_subterm (is_some o Induct_Args.dest_def) (Thm.term_of ct) andalso
- not (is_some (Induct_Args.dest_def (drop_judgment ctxt (Thm.term_of ct))))
+ not (is_some (Induct_Args.dest_def (Object_Logic.drop_judgment ctxt (Thm.term_of ct))))
then
(Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
@@ -502,8 +500,8 @@
val rule' = rule
|> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
in
- CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
- Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
+ CASES (Rule_Cases.make_common ctxt
+ (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
(if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
end)
@@ -520,9 +518,9 @@
(* atomize *)
-fun atomize_term thy =
- Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
- #> Object_Logic.drop_judgment thy;
+fun atomize_term ctxt =
+ Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
+ #> Object_Logic.drop_judgment ctxt;
fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
@@ -538,12 +536,11 @@
Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
-fun rulified_term thm =
+fun rulified_term ctxt thm =
let
- val thy = Thm.theory_of_thm thm;
- val rulify = rulify_term thy;
+ val rulify = rulify_term (Proof_Context.theory_of ctxt);
val (As, B) = Logic.strip_horn (Thm.prop_of thm);
- in (thy, Logic.list_implies (map rulify As, rulify B)) end;
+ in Logic.list_implies (map rulify As, rulify B) end;
fun rulify_tac ctxt =
rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
@@ -736,8 +733,6 @@
fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
SUBGOAL_CASES (fn (_, i, st) =>
let
- val thy = Proof_Context.theory_of ctxt;
-
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
@@ -745,9 +740,9 @@
(if null insts then `Rule_Cases.get r
else (align_left "Rule has fewer conclusions than arguments given"
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
- |> maps (prep_inst ctxt align_right (atomize_term thy))
+ |> maps (prep_inst ctxt align_right (atomize_term ctxt))
|> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
- |> mod_cases thy
+ |> mod_cases
|> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
val ruleq =
@@ -766,7 +761,7 @@
val rule'' = rule' |> simp ? simplified_rule ctxt;
val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
- in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
+ in Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end;
in
fn st =>
ruleq
@@ -800,7 +795,7 @@
((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
THEN_ALL_NEW rulify_tac ctxt);
-val induct_tac = gen_induct_tac (K I);
+val induct_tac = gen_induct_tac I;
@@ -847,8 +842,8 @@
guess_instance ctxt rule i st
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
- CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
- Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
+ CASES (Rule_Cases.make_common ctxt
+ (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
(Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
end);
--- a/src/Tools/induction.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/Tools/induction.ML Wed Apr 08 19:39:08 2015 +0200
@@ -43,7 +43,7 @@
(take n cases ~~ take n hnamess);
in ((cases', consumes), th) end;
-val induction_tac = Induct.gen_induct_tac (K name_hyps);
+val induction_tac = Induct.gen_induct_tac name_hyps;
val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);