--- a/src/HOL/simpdata.ML Sun Jan 21 16:43:45 2007 +0100
+++ b/src/HOL/simpdata.ML Sun Jan 21 16:43:46 2007 +0100
@@ -20,60 +20,47 @@
val conj = HOLogic.conj
val imp = HOLogic.imp
(*rules*)
- val iff_reflection = thm "eq_reflection"
- val iffI = thm "iffI"
- val iff_trans = thm "trans"
- val conjI= thm "conjI"
- val conjE= thm "conjE"
- val impI = thm "impI"
- val mp = thm "mp"
- val uncurry = thm "uncurry"
- val exI = thm "exI"
- val exE = thm "exE"
- val iff_allI = thm "iff_allI"
- val iff_exI = thm "iff_exI"
- val all_comm = thm "all_comm"
- val ex_comm = thm "ex_comm"
+ val iff_reflection = @{thm eq_reflection}
+ val iffI = @{thm iffI}
+ val iff_trans = @{thm trans}
+ val conjI= @{thm conjI}
+ val conjE= @{thm conjE}
+ val impI = @{thm impI}
+ val mp = @{thm mp}
+ val uncurry = @{thm uncurry}
+ val exI = @{thm exI}
+ val exE = @{thm exE}
+ val iff_allI = @{thm iff_allI}
+ val iff_exI = @{thm iff_exI}
+ val all_comm = @{thm all_comm}
+ val ex_comm = @{thm ex_comm}
end);
structure Simpdata =
struct
-local
- val eq_reflection = thm "eq_reflection"
-in fun mk_meta_eq r = r RS eq_reflection end;
+fun mk_meta_eq r = r RS @{thm eq_reflection};
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
-local
- val Eq_FalseI = thm "Eq_FalseI"
- val Eq_TrueI = thm "Eq_TrueI"
-in fun mk_eq th = case concl_of th
+fun mk_eq th = case concl_of th
(*expects Trueprop if not == *)
of Const ("==",_) $ _ $ _ => th
| _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq th
- | _ $ (Const ("Not", _) $ _) => th RS Eq_FalseI
- | _ => th RS Eq_TrueI
-end;
+ | _ $ (Const ("Not", _) $ _) => th RS @{thm Eq_FalseI}
+ | _ => th RS @{thm Eq_TrueI}
-local
- val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"
- val Eq_TrueI = thm "Eq_TrueI"
-in fun mk_eq_True r =
- SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
-end;
+fun mk_eq_True r =
+ SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
(* Produce theorems of the form
(P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
*)
-local
- val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"
- val simp_implies_def = thm "simp_implies_def"
-in fun lift_meta_eq_to_obj_eq i st =
+fun lift_meta_eq_to_obj_eq i st =
let
fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
| count_imp _ = 0;
val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
- in if j = 0 then meta_eq_to_obj_eq
+ in if j = 0 then @{thm meta_eq_to_obj_eq}
else
let
val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
@@ -86,11 +73,11 @@
[mk_simp_implies (Logic.mk_equals (x, y))]
(mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
(fn prems => EVERY
- [rewrite_goals_tac [simp_implies_def],
- REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
+ [rewrite_goals_tac @{thms simp_implies_def},
+ REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
+ map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
end
end;
-end;
(*Congruence rules for = (instead of ==)*)
fun mk_meta_cong rl = zero_var_indexes
@@ -123,42 +110,33 @@
fun mksimps pairs =
map_filter (try mk_eq) o mk_atomize pairs o gen_all;
-local
- val simp_impliesI = thm "simp_impliesI"
- val TrueI = thm "TrueI"
- val FalseE = thm "FalseE"
- val refl = thm "refl"
-in fun unsafe_solver_tac prems =
- (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
- FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE];
-end;
+fun unsafe_solver_tac prems =
+ (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
+ FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), atac,
+ etac @{thm FalseE}];
+
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
(*No premature instantiation of variables during simplification*)
-local
- val simp_impliesI = thm "simp_impliesI"
- val TrueI = thm "TrueI"
- val FalseE = thm "FalseE"
- val refl = thm "refl"
-in fun safe_solver_tac prems =
- (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
- FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems),
- eq_assume_tac, ematch_tac [FalseE]];
-end;
+fun safe_solver_tac prems =
+ (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
+ FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems),
+ eq_assume_tac, ematch_tac @{thms FalseE}];
+
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
structure SplitterData =
struct
structure Simplifier = Simplifier
val mk_eq = mk_eq
- val meta_eq_to_iff = thm "meta_eq_to_obj_eq"
- val iffD = thm "iffD2"
- val disjE = thm "disjE"
- val conjE = thm "conjE"
- val exE = thm "exE"
- val contrapos = thm "contrapos_nn"
- val contrapos2 = thm "contrapos_pp"
- val notnotD = thm "notnotD"
+ val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
+ val iffD = @{thm iffD2}
+ val disjE = @{thm disjE}
+ val conjE = @{thm conjE}
+ val exE = @{thm exE}
+ val contrapos = @{thm contrapos_nn}
+ val contrapos2 = @{thm contrapos_pp}
+ val notnotD = @{thm notnotD}
end;
structure Splitter = SplitterFun(SplitterData);
@@ -177,19 +155,19 @@
structure Clasimp = ClasimpFun
(structure Simplifier = Simplifier and Splitter = Splitter
and Classical = Classical and Blast = Blast
- val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE");
+ val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
open Clasimp;
val _ = ML_Context.value_antiq "clasimpset"
(Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
val mksimps_pairs =
- [("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]),
- ("All", [thm "spec"]), ("True", []), ("False", []),
- ("HOL.If", [thm "if_bool_eq_conj" RS thm "iffD1"])];
+ [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
+ ("All", [@{thm spec}]), ("True", []), ("False", []),
+ ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
val HOL_basic_ss =
- Simplifier.theory_context (the_context ()) empty_ss
+ Simplifier.theory_context @{theory} empty_ss
setsubgoaler asm_simp_tac
setSSolver safe_solver
setSolver unsafe_solver
@@ -212,8 +190,7 @@
val use_neq_simproc = ref true;
local
- val thy = the_context ();
- val neq_to_EQ_False = thm "not_sym" RS thm "Eq_FalseI";
+ val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
fun neq_prover sg ss (eq $ lhs $ rhs) =
let
fun test thm = (case #prop (rep_thm thm) of
@@ -228,7 +205,7 @@
end
in
-val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover;
+val neq_simproc = Simplifier.simproc @{theory} "neq_simproc" ["x = y"] neq_prover;
end;
@@ -238,22 +215,18 @@
val use_let_simproc = ref true;
local
- val thy = the_context ();
- val Let_folded = thm "Let_folded";
- val Let_unfold = thm "Let_unfold";
- val Let_def = thm "Let_def";
val (f_Let_unfold, x_Let_unfold) =
- let val [(_$(f$x)$_)] = prems_of Let_unfold
- in (cterm_of thy f, cterm_of thy x) end
+ let val [(_$(f$x)$_)] = prems_of @{thm Let_unfold}
+ in (cterm_of @{theory} f, cterm_of @{theory} x) end
val (f_Let_folded, x_Let_folded) =
- let val [(_$(f$x)$_)] = prems_of Let_folded
- in (cterm_of thy f, cterm_of thy x) end;
+ let val [(_$(f$x)$_)] = prems_of @{thm Let_folded}
+ in (cterm_of @{theory} f, cterm_of @{theory} x) end;
val g_Let_folded =
- let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end;
+ let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end;
in
val let_simproc =
- Simplifier.simproc thy "let_simp" ["Let x f"]
+ Simplifier.simproc @{theory} "let_simp" ["Let x f"]
(fn sg => fn ss => fn t =>
let val ctxt = Simplifier.the_context ss;
val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
@@ -261,7 +234,7 @@
(case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
if not (!use_let_simproc) then NONE
else if is_Free x orelse is_Bound x orelse is_Const x
- then SOME Let_def
+ then SOME @{thm Let_def}
else
let
val n = case f of (Abs (x,_,_)) => x | _ => "x";
@@ -274,7 +247,8 @@
in (if (g aconv g')
then
let
- val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
+ val rl =
+ cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] @{thm Let_unfold};
in SOME (rl OF [fx_g]) end
else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
else let
@@ -284,7 +258,7 @@
val rl = cterm_instantiate
[(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
(g_Let_folded,cterm_of sg abs_g')]
- Let_folded;
+ @{thm Let_folded};
in SOME (rl OF [transitive fx_g g_g'x])
end)
end
@@ -314,40 +288,34 @@
*)
local
- val conjE = thm "conjE"
- val exE = thm "exE"
- val disjE = thm "disjE"
- val notE = thm "notE"
- val rev_mp = thm "rev_mp"
- val ccontr = thm "ccontr"
val nnf_simpset =
empty_ss setmkeqTrue mk_eq_True
setmksimps (mksimps mksimps_pairs)
- addsimps [thm "imp_conv_disj", thm "iff_conv_conj_imp", thm "de_Morgan_disj", thm "de_Morgan_conj",
- thm "not_all", thm "not_ex", thm "not_not"];
+ addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
+ @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
fun prem_nnf_tac i st =
full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
in
fun refute_tac test prep_tac ref_tac =
let val refute_prems_tac =
REPEAT_DETERM
- (eresolve_tac [conjE, exE] 1 ORELSE
+ (eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE
filter_prems_tac test 1 ORELSE
- etac disjE 1) THEN
- ((etac notE 1 THEN eq_assume_tac 1) ORELSE
+ etac @{thm disjE} 1) THEN
+ ((etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
ref_tac 1);
in EVERY'[TRY o filter_prems_tac test,
- REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
+ REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac,
SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
end;
end;
val defALL_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
val defEX_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;