--- a/Admin/isatest/isatest-stats Sat May 01 11:46:47 2010 -0700
+++ b/Admin/isatest/isatest-stats Sat May 01 16:13:24 2010 -0700
@@ -6,7 +6,7 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at-poly-test at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
+PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
ISABELLE_SESSIONS="\
HOL-Plain \
--- a/src/FOL/simpdata.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/FOL/simpdata.ML Sat May 01 16:13:24 2010 -0700
@@ -35,10 +35,6 @@
[("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
("All", [@{thm spec}]), ("True", []), ("False", [])];
-(* ###FIXME: move to simplifier.ML
-val mk_atomize: (string * thm list) list -> thm -> thm list
-*)
-(* ###FIXME: move to simplifier.ML *)
fun mk_atomize pairs =
let fun atoms th =
(case concl_of th of
--- a/src/FOLP/simp.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/FOLP/simp.ML Sat May 01 16:13:24 2010 -0700
@@ -222,7 +222,7 @@
fun normed_rews congs =
let val add_norms = add_norm_tags congs in
fn thm => Variable.tradeT
- (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm]
+ (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm]
end;
fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
--- a/src/HOL/Library/Efficient_Nat.thy Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Library/Efficient_Nat.thy Sat May 01 16:13:24 2010 -0700
@@ -152,7 +152,8 @@
in
case map_filter (fn th'' =>
SOME (th'', singleton
- (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
+ (Variable.trade (K (fn [th'''] => [th''' RS th']))
+ (Variable.global_thm_context th'')) th'')
handle THM _ => NONE) thms of
[] => NONE
| thps =>
--- a/src/HOL/Tools/Datatype/datatype_data.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Sat May 01 16:13:24 2010 -0700
@@ -342,8 +342,8 @@
((Binding.empty, map (fn th => th RS notE) (flat distinct)),
[Classical.safe_elim NONE]),
((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
- ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])]
- @ named_rules @ unnamed_rules)
+ ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
+ named_rules @ unnamed_rules)
|> snd
|> add_case_tr' case_names
|> register dt_infos
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat May 01 16:13:24 2010 -0700
@@ -355,7 +355,7 @@
if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
else
let
- val ctxt0 = Variable.thm_context th
+ val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt1) = to_nnf th ctxt0
val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end
@@ -408,7 +408,7 @@
local
fun skolem_def (name, th) thy =
- let val ctxt0 = Variable.thm_context th in
+ let val ctxt0 = Variable.global_thm_context th in
(case try (to_nnf th) ctxt0 of
NONE => (NONE, thy)
| SOME (nnfth, ctxt1) =>
--- a/src/HOL/Tools/meson.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/meson.ML Sat May 01 16:13:24 2010 -0700
@@ -555,7 +555,7 @@
skolemize_nnf_list ctxt ths);
fun add_clauses th cls =
- let val ctxt0 = Variable.thm_context th
+ let val ctxt0 = Variable.global_thm_context th
val (cnfs, ctxt) = make_cnf [] th ctxt0
in Variable.export ctxt ctxt0 cnfs @ cls end;
--- a/src/HOL/Tools/simpdata.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/HOL/Tools/simpdata.ML Sat May 01 16:13:24 2010 -0700
@@ -95,7 +95,7 @@
fun res th = map (fn rl => th RS rl); (*exception THM*)
fun res_fixed rls =
if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls
- else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm];
+ else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm];
in
case concl_of thm
of Const (@{const_name Trueprop}, _) $ p => (case head_of p
--- a/src/Provers/clasimp.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/Provers/clasimp.ML Sat May 01 16:13:24 2010 -0700
@@ -70,8 +70,14 @@
fun get_css context = (Classical.get_cs context, Simplifier.get_ss context);
fun map_css f context =
- let val (cs', ss') = f (get_css context)
- in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
+ let
+ val (cs, ss) = get_css context;
+ val (cs', ss') = f (cs, Simplifier.context (Context.proof_of context) ss);
+ in
+ context
+ |> Classical.map_cs (K cs')
+ |> Simplifier.map_ss (K (Simplifier.inherit_context ss ss'))
+ end;
fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
--- a/src/Pure/simplifier.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/Pure/simplifier.ML Sat May 01 16:13:24 2010 -0700
@@ -37,6 +37,7 @@
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
val global_context: theory -> simpset -> simpset
+ val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
val simproc_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
val simproc: theory -> string -> string list
--- a/src/Pure/variable.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/Pure/variable.ML Sat May 01 16:13:24 2010 -0700
@@ -28,7 +28,7 @@
val declare_typ: typ -> Proof.context -> Proof.context
val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
val declare_thm: thm -> Proof.context -> Proof.context
- val thm_context: thm -> Proof.context
+ val global_thm_context: thm -> Proof.context
val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
val bind_term: indexname * term option -> Proof.context -> Proof.context
val expand_binds: Proof.context -> term -> term
@@ -235,7 +235,7 @@
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
val declare_thm = Thm.fold_terms declare_internal;
-fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
+fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
(* renaming term/type frees *)
--- a/src/Tools/induct.ML Sat May 01 11:46:47 2010 -0700
+++ b/src/Tools/induct.ML Sat May 01 16:13:24 2010 -0700
@@ -46,7 +46,8 @@
val coinduct_pred: string -> attribute
val coinduct_del: attribute
val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic
- val add_simp_rule: attribute
+ val induct_simp_add: attribute
+ val induct_simp_del: attribute
val no_simpN: string
val casesN: string
val inductN: string
@@ -320,8 +321,14 @@
val coinduct_del = del_att map3;
fun map_simpset f = InductData.map (map4 f);
-fun add_simp_rule (ctxt, thm) =
- (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm);
+
+fun induct_simp f =
+ Thm.declaration_attribute (fn thm => fn context =>
+ (map_simpset
+ (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context));
+
+val induct_simp_add = induct_simp (op addsimps);
+val induct_simp_del = induct_simp (op delsimps);
end;
@@ -359,7 +366,7 @@
"declaration of induction rule" #>
Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
"declaration of coinduction rule" #>
- Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule)
+ Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
"declaration of rules for simplifying induction or cases rules";
end;