--- a/NEWS Sat Jan 11 21:03:11 2014 +0100
+++ b/NEWS Sun Jan 12 18:42:06 2014 +0100
@@ -31,6 +31,14 @@
"isabelle jedit -m MODE".
+*** Pure ***
+
+* More thorough check of proof context for goal statements and
+attributed fact expressions: background theory, declared hyps,
+declared variable names. Potential INCOMPATIBILITY, tools need to
+observe standard context discipline.
+
+
*** HOL ***
* "declare [[code abort: ...]]" replaces "code_abort ...".
--- a/src/FOL/simpdata.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/FOL/simpdata.ML Sun Jan 12 18:42:06 2014 +0100
@@ -123,7 +123,7 @@
|> Simplifier.set_mkcong mk_meta_cong
|> simpset_of;
-fun unfold_tac ths ctxt =
+fun unfold_tac ctxt ths =
ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths));
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Sun Jan 12 18:42:06 2014 +0100
@@ -186,10 +186,10 @@
fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
if null set_maps then atac 1
else
- unfold_tac [in_rel] ctxt THEN
+ unfold_tac ctxt [in_rel] THEN
REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
hyp_subst_tac ctxt 1 THEN
- unfold_tac set_maps ctxt THEN
+ unfold_tac ctxt set_maps THEN
EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Jan 12 18:42:06 2014 +0100
@@ -782,7 +782,7 @@
fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
let val n = length ks;
in
- unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
+ unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Jan 12 18:42:06 2014 +0100
@@ -580,7 +580,7 @@
(map (map (rulify_term thy #> rpair [])) vc_compat)
end;
-fun prove_eqvt s xatoms ctxt =
+fun prove_eqvt s xatoms ctxt = (* FIXME ctxt should be called lthy *)
let
val thy = Proof_Context.theory_of ctxt;
val ({names, ...}, {raw_induct, intrs, elims, ...}) =
@@ -609,21 +609,21 @@
atoms)
end;
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
- val eqvt_simpset = put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps
- (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
- [mk_perm_bool_simproc names,
- NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
val (([t], [pi]), ctxt') = ctxt |>
Variable.import_terms false [concl_of raw_induct] ||>>
Variable.variant_fixes ["pi"];
+ val eqvt_simpset = put_simpset HOL_basic_ss ctxt' addsimps
+ (NominalThmDecls.get_eqvt_thms ctxt' @ perm_pi_simp) addsimprocs
+ [mk_perm_bool_simproc names,
+ NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
val ps = map (fst o HOLogic.dest_imp)
(HOLogic.dest_conj (HOLogic.dest_Trueprop t));
- fun eqvt_tac ctxt'' pi (intr, vs) st =
+ fun eqvt_tac pi (intr, vs) st =
let
fun eqvt_err s =
- let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
+ let val ([t], ctxt'') = Variable.import_terms true [prop_of intr] ctxt'
in error ("Could not prove equivariance for introduction rule\n" ^
- Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
+ Syntax.string_of_term ctxt'' t ^ "\n" ^ s)
end;
val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
let
@@ -639,7 +639,7 @@
in
case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
NONE => eqvt_err ("Rule does not match goal\n" ^
- Syntax.string_of_term ctxt'' (hd (prems_of st)))
+ Syntax.string_of_term ctxt' (hd (prems_of st)))
| SOME (th, _) => Seq.single th
end;
val thss = map (fn atom =>
@@ -654,9 +654,9 @@
HOLogic.mk_imp (p, list_comb (h, ts1 @
map (NominalDatatype.mk_perm [] pi') ts2))
end) ps)))
- (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
+ (fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
full_simp_tac eqvt_simpset 1 THEN
- eqvt_tac context pi' intr_vs) intrs')) |>
+ eqvt_tac pi' intr_vs) intrs')) |>
singleton (Proof_Context.export ctxt' ctxt)))
end) atoms
in
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Jan 12 18:42:06 2014 +0100
@@ -12,6 +12,7 @@
signature NOMINAL_THMDECLS =
sig
+ val nominal_eqvt_debug: bool Config.T
val eqvt_add: attribute
val eqvt_del: attribute
val eqvt_force_add: attribute
@@ -69,7 +70,6 @@
fun get_derived_thm ctxt hyp concl orig_thm pi typi =
let
- val thy = Proof_Context.theory_of ctxt;
val pi' = Var (pi, typi);
val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
val ([goal_term, pi''], ctxt') = Variable.import_terms false
--- a/src/HOL/Set.thy Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Set.thy Sun Jan 12 18:42:06 2014 +0100
@@ -69,9 +69,9 @@
*}
simproc_setup defined_Collect ("{x. P x & Q x}") = {*
- fn _ =>
- Quantifier1.rearrange_Collect
- (rtac @{thm Collect_cong} 1 THEN
+ fn _ => Quantifier1.rearrange_Collect
+ (fn _ =>
+ rtac @{thm Collect_cong} 1 THEN
rtac @{thm iffI} 1 THEN
ALLGOALS
(EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
@@ -355,17 +355,17 @@
*}
simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
- let
- val unfold_bex_tac = unfold_tac @{thms Bex_def};
- fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
- in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
+ fn _ => Quantifier1.rearrange_bex
+ (fn ctxt =>
+ unfold_tac ctxt @{thms Bex_def} THEN
+ Quantifier1.prove_one_point_ex_tac)
*}
simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
- let
- val unfold_ball_tac = unfold_tac @{thms Ball_def};
- fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
- in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
+ fn _ => Quantifier1.rearrange_ball
+ (fn ctxt =>
+ unfold_tac ctxt @{thms Ball_def} THEN
+ Quantifier1.prove_one_point_all_tac)
*}
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Jan 12 18:42:06 2014 +0100
@@ -122,19 +122,14 @@
(* General reduction pair application *)
fun rem_inv_img ctxt =
- let
- val unfold_tac = Local_Defs.unfold_tac ctxt
- in
- rtac @{thm subsetI} 1
- THEN etac @{thm CollectE} 1
- THEN REPEAT (etac @{thm exE} 1)
- THEN unfold_tac @{thms inv_image_def}
- THEN rtac @{thm CollectI} 1
- THEN etac @{thm conjE} 1
- THEN etac @{thm ssubst} 1
- THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
- @ @{thms sum.cases})
- end
+ rtac @{thm subsetI} 1
+ THEN etac @{thm CollectE} 1
+ THEN REPEAT (etac @{thm exE} 1)
+ THEN Local_Defs.unfold_tac ctxt @{thms inv_image_def}
+ THEN rtac @{thm CollectI} 1
+ THEN etac @{thm conjE} 1
+ THEN etac @{thm ssubst} 1
+ THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
(* Sets *)
@@ -289,9 +284,8 @@
THEN (rtac @{thm rp_inv_image_rp} 1)
THEN (rtac (order_rpair ms_rp label) 1)
THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
- THEN unfold_tac @{thms rp_inv_image_def} ctxt
- THEN Local_Defs.unfold_tac ctxt
- (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
+ THEN unfold_tac ctxt @{thms rp_inv_image_def}
+ THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
THEN EVERY (map (prove_lev true) sl)
THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
--- a/src/HOL/Tools/Lifting/lifting_def.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Sun Jan 12 18:42:06 2014 +0100
@@ -103,7 +103,8 @@
Drule.cterm_instantiate subst relcomppI
end
- fun zip_transfer_rules ctxt thm = let
+ fun zip_transfer_rules ctxt thm =
+ let
val thy = Proof_Context.theory_of ctxt
fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
@@ -122,7 +123,8 @@
val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
val assms = cprems_of fixed_thm
val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
- val ctxt = Context.proof_map(fold (add_transfer_rule o Thm.assume) assms) ctxt
+ val (prems, ctxt) = fold_map Thm.assume_hyps assms ctxt
+ val ctxt = Context.proof_map (fold add_transfer_rule prems) ctxt
val zipped_thm =
fixed_thm
|> undisch_all
--- a/src/HOL/Tools/TFL/post.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML Sun Jan 12 18:42:06 2014 +0100
@@ -70,9 +70,8 @@
(*Is this the best way to invoke the simplifier??*)
fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
-fun join_assums th =
+fun join_assums ctxt th =
let val thy = Thm.theory_of_thm th
- val ctxt = Proof_Context.init_global thy
val tych = cterm_of thy
val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *)
@@ -101,7 +100,7 @@
if (id_thm th) then (So, Si, th::St) else
if (solved th) then (th::So, Si, St)
else (So, th::Si, St)) nested_tcs ([],[],[])
- val simplified' = map join_assums simplified
+ val simplified' = map (join_assums ctxt) simplified
val dummy = (Prim.trace_thms "solved =" solved;
Prim.trace_thms "simplified' =" simplified')
val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
@@ -189,9 +188,9 @@
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 ctxt = Proof_Context.transfer thy ctxt
val (lhs, _) = Logic.dest_equals (prop_of def)
- val {induct, rules, tcs} = simplify_defn strict thy ctxt' congs wfs fid pats 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
--- a/src/HOL/Tools/TFL/tfl.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Sun Jan 12 18:42:06 2014 +0100
@@ -432,7 +432,7 @@
not simplified. Otherwise large examples (Red-Black trees) are too
slow.*)
val case_simpset =
- put_simpset HOL_basic_ss (Proof_Context.init_global theory)
+ put_simpset HOL_basic_ss ctxt
addsimps case_rewrites
|> fold (Simplifier.add_cong o #weak_case_cong o snd)
(Symtab.dest (Datatype.get_all theory))
--- a/src/HOL/Tools/simpdata.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML Sun Jan 12 18:42:06 2014 +0100
@@ -178,7 +178,7 @@
fun hol_simplify ctxt rews =
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews);
-fun unfold_tac ths ctxt =
+fun unfold_tac ctxt ths =
ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths));
end;
--- a/src/Provers/quantifier1.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Provers/quantifier1.ML Sun Jan 12 18:42:06 2014 +0100
@@ -68,9 +68,9 @@
val prove_one_point_ex_tac: tactic
val rearrange_all: Proof.context -> cterm -> thm option
val rearrange_ex: Proof.context -> cterm -> thm option
- val rearrange_ball: tactic -> Proof.context -> cterm -> thm option
- val rearrange_bex: tactic -> Proof.context -> cterm -> thm option
- val rearrange_Collect: tactic -> Proof.context -> cterm -> thm option
+ val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+ val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+ val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
end;
functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -120,12 +120,13 @@
| exqu xs P = extract (null xs) xs P
in exqu [] end;
-fun prove_conv tac ctxt tu =
+fun prove_conv ctxt tu tac =
let
val (goal, ctxt') =
yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
val thm =
- Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
+ Goal.prove ctxt' [] [] goal
+ (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
in singleton (Variable.export ctxt' ctxt) thm end;
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
@@ -178,7 +179,7 @@
NONE => NONE
| SOME (xs, eq, Q) =>
let val R = quantify all x T xs (Data.imp $ eq $ Q)
- in SOME (prove_conv prove_one_point_all_tac ctxt (F, R)) end)
+ in SOME (prove_conv ctxt (F, R) (K prove_one_point_all_tac)) end)
| _ => NONE);
fun rearrange_ball tac ctxt ct =
@@ -190,7 +191,7 @@
if not (null xs) then NONE
else
let val R = Data.imp $ eq $ Q
- in SOME (prove_conv tac ctxt (F, Ball $ A $ Abs (x, T, R))) end)
+ in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
| _ => NONE);
fun rearrange_ex ctxt ct =
@@ -200,7 +201,7 @@
NONE => NONE
| SOME (xs, eq, Q) =>
let val R = quantify ex x T xs (Data.conj $ eq $ Q)
- in SOME (prove_conv prove_one_point_ex_tac ctxt (F, R)) end)
+ in SOME (prove_conv ctxt (F, R) (K prove_one_point_ex_tac)) end)
| _ => NONE);
fun rearrange_bex tac ctxt ct =
@@ -210,7 +211,7 @@
NONE => NONE
| SOME (xs, eq, Q) =>
if not (null xs) then NONE
- else SOME (prove_conv tac ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
+ else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
| _ => NONE);
fun rearrange_Collect tac ctxt ct =
@@ -220,7 +221,7 @@
NONE => NONE
| SOME (_, eq, Q) =>
let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
- in SOME (prove_conv tac ctxt (F, R)) end)
+ in SOME (prove_conv ctxt (F, R) tac) end)
| _ => NONE);
end;
--- a/src/Pure/Isar/element.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/Isar/element.ML Sun Jan 12 18:42:06 2014 +0100
@@ -473,16 +473,18 @@
(* init *)
-fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
- | init (Constrains _) = I
- | init (Assumes asms) = Context.map_proof (fn ctxt =>
+local
+
+fun init0 (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
+ | init0 (Constrains _) = I
+ | init0 (Assumes asms) = Context.map_proof (fn ctxt =>
let
val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (maps (map #1 o #2) asms')
|> Proof_Context.add_assms_i Assumption.assume_export asms';
in ctxt' end)
- | init (Defines defs) = Context.map_proof (fn ctxt =>
+ | init0 (Defines defs) = Context.map_proof (fn ctxt =>
let
val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
val asms = defs' |> map (fn (b, (t, ps)) =>
@@ -492,7 +494,17 @@
|> fold Variable.auto_fixes (map #1 asms)
|> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
- | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
+ | init0 (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
+
+in
+
+fun init elem context =
+ context
+ |> Context.mapping I Thm.unchecked_hyps
+ |> init0 elem
+ |> Context.mapping I (fn ctxt => Thm.restore_hyps (Context.proof_of context) ctxt);
+
+end;
(* activate *)
--- a/src/Pure/Isar/proof.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/Isar/proof.ML Sun Jan 12 18:42:06 2014 +0100
@@ -492,7 +492,7 @@
handle THM _ => lost_structure ())
|> Drule.flexflex_unique
|> Thm.check_shyps (Variable.sorts_of ctxt)
- |> Thm.check_hyps ctxt;
+ |> Thm.check_hyps (Context.Proof ctxt);
val goal_propss = filter_out null propss;
val results =
--- a/src/Pure/goal.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/goal.ML Sun Jan 12 18:42:06 2014 +0100
@@ -168,8 +168,7 @@
fun prove_internal ctxt casms cprop tac =
(case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
- SOME th => Drule.implies_intr_list casms
- (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
+ SOME th => Drule.implies_intr_list casms (finish ctxt th)
| NONE => error "Tactic failed");
@@ -221,7 +220,7 @@
(finish ctxt' st
|> Drule.flexflex_unique
|> Thm.check_shyps sorts
- (* |> Thm.check_hyps ctxt' *) (* FIXME *))
+ |> Thm.check_hyps (Context.Proof ctxt'))
handle THM (msg, _, _) => err msg | ERROR msg => err msg;
in
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
--- a/src/Pure/more_thm.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/more_thm.ML Sun Jan 12 18:42:06 2014 +0100
@@ -54,7 +54,9 @@
val elim_rules: thm Item_Net.T
val declare_hyps: cterm -> Proof.context -> Proof.context
val assume_hyps: cterm -> Proof.context -> thm * Proof.context
- val check_hyps: Proof.context -> thm -> thm
+ val unchecked_hyps: Proof.context -> Proof.context
+ val restore_hyps: Proof.context -> Proof.context -> Proof.context
+ val check_hyps: Context.generic -> thm -> thm
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
@@ -266,23 +268,40 @@
structure Hyps = Proof_Data
(
- type T = Termtab.set;
- fun init _ : T = Termtab.empty;
+ type T = Termtab.set * bool;
+ fun init _ : T = (Termtab.empty, true);
);
fun declare_hyps ct ctxt =
if Theory.subthy (theory_of_cterm ct, Proof_Context.theory_of ctxt) then
- Hyps.map (Termtab.update (term_of ct, ())) ctxt
+ (Hyps.map o apfst) (Termtab.update (term_of ct, ())) ctxt
else raise CTERM ("assume_hyps: bad background theory", [ct]);
fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
-fun check_hyps ctxt th =
+val unchecked_hyps = (Hyps.map o apsnd) (K false);
+fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
+
+fun check_hyps context th =
let
- val undeclared = filter_out (Termtab.defined (Hyps.get ctxt)) (Thm.hyps_of th);
- val _ = null undeclared orelse
- error ("Undeclared hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) undeclared));
- in th end;
+ val declared_hyps =
+ (case context of
+ Context.Theory _ => K false
+ | Context.Proof ctxt =>
+ (case Hyps.get ctxt of
+ (_, false) => K true
+ | (hyps, _) => Termtab.defined hyps));
+ val undeclared = filter_out declared_hyps (Thm.hyps_of th);
+ in
+ if null undeclared then th
+ else
+ let
+ val ctxt = Context.cases Syntax.init_pretty_global I context;
+ in
+ error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
+ (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared)))
+ end
+ end;
@@ -434,7 +453,7 @@
fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
fun apply_attribute (att: attribute) th x =
- let val (x', th') = att (x, Thm.transfer (Context.theory_of x) th)
+ let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
in (the_default th th', the_default x x') end;
fun attribute_declaration att th x = #2 (apply_attribute att th x);
--- a/src/Pure/raw_simplifier.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Sun Jan 12 18:42:06 2014 +0100
@@ -70,7 +70,7 @@
signature RAW_SIMPLIFIER =
sig
include BASIC_RAW_SIMPLIFIER
- exception SIMPLIFIER of string * thm
+ exception SIMPLIFIER of string * thm list
type trace_ops
val set_trace_ops: trace_ops -> theory -> theory
val internal_ss: simpset ->
@@ -114,7 +114,6 @@
val simp_trace_raw: Config.raw
val simp_debug_raw: Config.raw
val add_prems: thm list -> Proof.context -> Proof.context
- val debug_bounds: bool Unsynchronized.ref
val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
Proof.context -> Proof.context
val set_solvers: solver list -> Proof.context -> Proof.context
@@ -317,14 +316,16 @@
(* empty *)
-fun init_ss mk_rews termless subgoal_tac solvers =
- make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false)),
+fun init_ss bounds depth mk_rews termless subgoal_tac solvers =
+ make_simpset ((Net.empty, [], bounds, depth),
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
val empty_ss =
init_ss
+ (0, [])
+ (0, Unsynchronized.ref false)
{mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
mk_cong = K I,
mk_sym = default_mk_sym,
@@ -398,8 +399,8 @@
fun map_ss f = Context.mapping (map_theory_simpset f) f;
val clear_simpset =
- map_simpset (fn Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
- init_ss mk_rews termless subgoal_tac solvers);
+ map_simpset (fn Simpset ({bounds, depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
+ init_ss bounds depth mk_rews termless subgoal_tac solvers);
(* simp depth *)
@@ -436,7 +437,7 @@
(* diagnostics *)
-exception SIMPLIFIER of string * thm;
+exception SIMPLIFIER of string * thm list;
val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
val simp_debug = Config.bool simp_debug_raw;
@@ -541,7 +542,7 @@
val prems = Logic.strip_imp_prems prop;
val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
- raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
+ raise SIMPLIFIER ("Rewrite rule not a meta-equality", [thm]);
val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
val erhs = Envir.eta_contract (term_of rhs);
val perm =
@@ -554,7 +555,7 @@
fun decomp_simp' thm =
let val (_, lhs, _, rhs, _) = decomp_simp thm in
- if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
+ if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", [thm])
else (lhs, rhs)
end;
@@ -666,10 +667,10 @@
(fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
let
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
- handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+ handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
(*val lhs = Envir.eta_contract lhs;*)
val a = the (cong_name (head_of lhs)) handle Option.Option =>
- raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
+ raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
val (xs, weak) = congs;
val _ =
if AList.defined (op =) xs a then
@@ -684,10 +685,10 @@
(fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
let
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
- handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+ handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
(*val lhs = Envir.eta_contract lhs;*)
val a = the (cong_name (head_of lhs)) handle Option.Option =>
- raise SIMPLIFIER ("Congruence must start with a constant", thm);
+ raise SIMPLIFIER ("Congruence must start with a constant", [thm]);
val (xs, _) = congs;
val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
val weak' = xs' |> map_filter (fn (a, thm) =>
@@ -1321,27 +1322,6 @@
prover: how to solve premises in conditional rewrites and congruences
*)
-val debug_bounds = Unsynchronized.ref false;
-
-fun check_bounds ctxt ct =
- if ! debug_bounds then
- let
- val Simpset ({bounds = (_, bounds), ...}, _) = simpset_of ctxt;
- val bs =
- fold_aterms
- (fn Free (x, _) =>
- if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
- then insert (op =) x else I
- | _ => I) (term_of ct) [];
- in
- if null bs then ()
- else
- print_term ctxt true
- (fn () => "Simplifier: term contains loose bounds: " ^ commas_quote bs)
- (Thm.term_of ct)
- end
- else ();
-
fun rewrite_cterm mode prover raw_ctxt raw_ct =
let
val thy = Proof_Context.theory_of raw_ctxt;
@@ -1359,7 +1339,6 @@
|> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
- val _ = check_bounds ctxt ct;
in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
val simple_prover =
--- a/src/Pure/simplifier.ML Sat Jan 11 21:03:11 2014 +0100
+++ b/src/Pure/simplifier.ML Sun Jan 12 18:42:06 2014 +0100
@@ -31,7 +31,6 @@
val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
val pretty_simpset: Proof.context -> Pretty.T
val default_mk_sym: Proof.context -> thm -> thm option
- val debug_bounds: bool Unsynchronized.ref
val prems_of: Proof.context -> thm list
val add_simp: thm -> Proof.context -> Proof.context
val del_simp: thm -> Proof.context -> Proof.context
--- a/src/ZF/OrdQuant.thy Sat Jan 11 21:03:11 2014 +0100
+++ b/src/ZF/OrdQuant.thy Sun Jan 12 18:42:06 2014 +0100
@@ -368,17 +368,17 @@
text {* Setting up the one-point-rule simproc *}
simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {*
- let
- val unfold_rex_tac = unfold_tac @{thms rex_def};
- fun prove_rex_tac ctxt = unfold_rex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
- in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_rex_tac ctxt) ctxt end
+ fn _ => Quantifier1.rearrange_bex
+ (fn ctxt =>
+ unfold_tac ctxt @{thms rex_def} THEN
+ Quantifier1.prove_one_point_ex_tac)
*}
simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {*
- let
- val unfold_rall_tac = unfold_tac @{thms rall_def};
- fun prove_rall_tac ctxt = unfold_rall_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
- in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_rall_tac ctxt) ctxt end
+ fn _ => Quantifier1.rearrange_ball
+ (fn ctxt =>
+ unfold_tac ctxt @{thms rall_def} THEN
+ Quantifier1.prove_one_point_all_tac)
*}
end
--- a/src/ZF/pair.thy Sat Jan 11 21:03:11 2014 +0100
+++ b/src/ZF/pair.thy Sun Jan 12 18:42:06 2014 +0100
@@ -19,17 +19,17 @@
ML {* val ZF_ss = simpset_of @{context} *}
simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
- let
- val unfold_bex_tac = unfold_tac @{thms Bex_def};
- fun prove_bex_tac ctxt = unfold_bex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
- in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_bex_tac ctxt) ctxt end
+ fn _ => Quantifier1.rearrange_bex
+ (fn ctxt =>
+ unfold_tac ctxt @{thms Bex_def} THEN
+ Quantifier1.prove_one_point_ex_tac)
*}
simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
- let
- val unfold_ball_tac = unfold_tac @{thms Ball_def};
- fun prove_ball_tac ctxt = unfold_ball_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
- in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_ball_tac ctxt) ctxt end
+ fn _ => Quantifier1.rearrange_ball
+ (fn ctxt =>
+ unfold_tac ctxt @{thms Ball_def} THEN
+ Quantifier1.prove_one_point_all_tac)
*}