16014

1 
(* Title: Pure/simplifier.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen


4 


5 
Generic simplifier, suitable for most logics (see also


6 
meta_simplifier.ML for the actual metalevel rewriting engine).


7 
*)


8 


9 
(* added: put_delta_simpset, get_delta_simpset


10 
changed: simp_add_local


11 
07/01/05


12 
*)


13 


14 


15 
signature BASIC_SIMPLIFIER =


16 
sig


17 
include BASIC_META_SIMPLIFIER


18 
type context_solver


19 
val mk_context_solver: string > (Proof.context > thm list > int > tactic)


20 
> context_solver


21 
type context_simproc


22 
val mk_context_simproc: string > cterm list >


23 
(Proof.context > simpset > term > thm option) > context_simproc


24 
val print_simpset: theory > unit

16458

25 
val simpset_ref_of_sg: theory > simpset ref (*obsolete*)

16014

26 
val simpset_ref_of: theory > simpset ref

16458

27 
val simpset_of_sg: theory > simpset (*obsolete*)

16014

28 
val simpset_of: theory > simpset


29 
val SIMPSET: (simpset > tactic) > tactic


30 
val SIMPSET': (simpset > 'a > tactic) > 'a > tactic


31 
val simpset: unit > simpset


32 
val simpset_ref: unit > simpset ref


33 
val Addsimps: thm list > unit


34 
val Delsimps: thm list > unit


35 
val Addsimprocs: simproc list > unit


36 
val Delsimprocs: simproc list > unit


37 
val Addcongs: thm list > unit


38 
val Delcongs: thm list > unit


39 
val local_simpset_of: Proof.context > simpset


40 
val safe_asm_full_simp_tac: simpset > int > tactic


41 
val simp_tac: simpset > int > tactic


42 
val asm_simp_tac: simpset > int > tactic


43 
val full_simp_tac: simpset > int > tactic


44 
val asm_lr_simp_tac: simpset > int > tactic


45 
val asm_full_simp_tac: simpset > int > tactic


46 
val Simp_tac: int > tactic


47 
val Asm_simp_tac: int > tactic


48 
val Full_simp_tac: int > tactic


49 
val Asm_lr_simp_tac: int > tactic


50 
val Asm_full_simp_tac: int > tactic


51 
val simplify: simpset > thm > thm


52 
val asm_simplify: simpset > thm > thm


53 
val full_simplify: simpset > thm > thm


54 
val asm_lr_simplify: simpset > thm > thm


55 
val asm_full_simplify: simpset > thm > thm


56 
end;


57 


58 
signature SIMPLIFIER =


59 
sig


60 
include BASIC_SIMPLIFIER

16458

61 
val simproc_i: theory > string > term list


62 
> (theory > simpset > term > thm option) > simproc


63 
val simproc: theory > string > string list


64 
> (theory > simpset > term > thm option) > simproc


65 
val context_simproc_i: theory > string > term list

16014

66 
> (Proof.context > simpset > term > thm option) > context_simproc

16458

67 
val context_simproc: theory > string > string list

16014

68 
> (Proof.context > simpset > term > thm option) > context_simproc


69 
val rewrite: simpset > cterm > thm


70 
val asm_rewrite: simpset > cterm > thm


71 
val full_rewrite: simpset > cterm > thm


72 
val asm_lr_rewrite: simpset > cterm > thm


73 
val asm_full_rewrite: simpset > cterm > thm


74 
val add_context_simprocs: context_simproc list > theory > theory


75 
val del_context_simprocs: context_simproc list > theory > theory


76 
val set_context_subgoaler: (Proof.context > simpset > int > tactic) > theory > theory


77 
val reset_context_subgoaler: theory > theory


78 
val add_context_looper: string * (Proof.context > int > Tactical.tactic) >


79 
theory > theory


80 
val del_context_looper: string > theory > theory


81 
val add_context_unsafe_solver: context_solver > theory > theory


82 
val add_context_safe_solver: context_solver > theory > theory


83 
val print_local_simpset: Proof.context > unit


84 
val get_local_simpset: Proof.context > simpset


85 
val put_local_simpset: simpset > Proof.context > Proof.context


86 
val change_global_ss: (simpset * thm list > simpset) > theory attribute


87 
val change_local_ss: (simpset * thm list > simpset) > Proof.context attribute


88 
val simp_add_global: theory attribute


89 
val simp_del_global: theory attribute


90 
val simp_add_local: Proof.context attribute


91 
val simp_del_local: Proof.context attribute


92 
val cong_add_global: theory attribute


93 
val cong_del_global: theory attribute


94 
val cong_add_local: Proof.context attribute


95 
val cong_del_local: Proof.context attribute


96 
val change_simpset_of: (simpset * 'a > simpset) > 'a > theory > theory


97 
val simp_modifiers: (Args.T list > (Method.modifier * Args.T list)) list


98 
val method_setup: (Args.T list > (Method.modifier * Args.T list)) list


99 
> (theory > theory) list


100 
val easy_setup: thm > thm list > (theory > theory) list


101 


102 
val get_delta_simpset: ProofContext.context > Thm.thm list


103 
val put_delta_simpset: Thm.thm list > ProofContext.context > ProofContext.context


104 
end;


105 


106 
structure Simplifier: SIMPLIFIER =


107 
struct


108 


109 
open MetaSimplifier;


110 


111 


112 
(** context dependent simpset components **)


113 


114 
(* datatype context_solver *)


115 


116 
datatype context_solver =


117 
ContextSolver of (string * (Proof.context > thm list > int > tactic)) * stamp;


118 


119 
fun mk_context_solver name f = ContextSolver ((name, f), stamp ());


120 
fun eq_context_solver (ContextSolver (_, id1), ContextSolver (_, id2)) = (id1 = id2);


121 
val merge_context_solvers = gen_merge_lists eq_context_solver;


122 


123 


124 
(* datatype context_simproc *)


125 


126 
datatype context_simproc = ContextSimproc of


127 
(string * cterm list * (Proof.context > simpset > term > thm option)) * stamp;


128 


129 
fun mk_context_simproc name lhss f = ContextSimproc ((name, lhss, f), stamp ());


130 
fun eq_context_simproc (ContextSimproc (_, id1), ContextSimproc (_, id2)) = (id1 = id2);


131 
val merge_context_simprocs = gen_merge_lists eq_context_simproc;


132 

16458

133 
fun context_simproc_i thy name =


134 
mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify);

16014

135 

16458

136 
fun context_simproc thy name =


137 
context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);

16014

138 


139 


140 
(* datatype context_ss *)


141 


142 
datatype context_ss = ContextSS of


143 
{simprocs: context_simproc list,


144 
subgoal_tac: (Proof.context > simpset > int > tactic) option,


145 
loop_tacs: (string * (Proof.context > int > tactic)) list,


146 
unsafe_solvers: context_solver list,


147 
solvers: context_solver list};


148 


149 
fun context_ss ctxt ss ctxt_ss =


150 
let


151 
val ContextSS {simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers} = ctxt_ss;


152 
fun prep_simproc (ContextSimproc ((name, lhss, f), _)) =


153 
mk_simproc name lhss (K (f ctxt));


154 
fun add_loop (name, f) simpset = simpset addloop (name, f ctxt);


155 
fun add_solver add (ContextSolver ((name, f), _)) simpset =


156 
add (simpset, mk_solver name (f ctxt));


157 
in


158 
((case subgoal_tac of NONE => ss  SOME tac => ss setsubgoaler tac ctxt)


159 
addsimprocs map prep_simproc simprocs)


160 
> fold_rev add_loop loop_tacs


161 
> fold_rev (add_solver (op addSolver)) unsafe_solvers


162 
> fold_rev (add_solver (op addSSolver)) solvers


163 
end;


164 


165 
fun make_context_ss (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =


166 
ContextSS {simprocs = simprocs, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,


167 
unsafe_solvers = unsafe_solvers, solvers = solvers};


168 


169 
val empty_context_ss = make_context_ss ([], NONE, [], [], []);


170 


171 
fun merge_context_ss (ctxt_ss1, ctxt_ss2) =


172 
let


173 
val ContextSS {simprocs = simprocs1, subgoal_tac = subgoal_tac1, loop_tacs = loop_tacs1,


174 
unsafe_solvers = unsafe_solvers1, solvers = solvers1} = ctxt_ss1;


175 
val ContextSS {simprocs = simprocs2, subgoal_tac = subgoal_tac2, loop_tacs = loop_tacs2,


176 
unsafe_solvers = unsafe_solvers2, solvers = solvers2} = ctxt_ss2;


177 


178 
val simprocs' = merge_context_simprocs simprocs1 simprocs2;


179 
val subgoal_tac' = (case subgoal_tac1 of NONE => subgoal_tac2  some => some);


180 
val loop_tacs' = merge_alists loop_tacs1 loop_tacs2;


181 
val unsafe_solvers' = merge_context_solvers unsafe_solvers1 unsafe_solvers2;


182 
val solvers' = merge_context_solvers solvers1 solvers2;


183 
in make_context_ss (simprocs', subgoal_tac', loop_tacs', unsafe_solvers', solvers') end;


184 


185 


186 


187 
(** global and local simpset data **)


188 


189 
(* theory data kind 'Pure/simpset' *)


190 

16458

191 
structure GlobalSimpset = TheoryDataFun


192 
(struct

16014

193 
val name = "Pure/simpset";


194 
type T = simpset ref * context_ss;


195 


196 
val empty = (ref empty_ss, empty_context_ss);


197 
fun copy (ref ss, ctxt_ss) = (ref ss, ctxt_ss): T; (*create new reference!*)

16458

198 
val extend = copy;


199 
fun merge _ ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =

16014

200 
(ref (merge_ss (ss1, ss2)), merge_context_ss (ctxt_ss1, ctxt_ss2));


201 
fun print _ (ref ss, _) = print_ss ss;

16458

202 
end);

16014

203 


204 
val _ = Context.add_setup [GlobalSimpset.init];


205 
val print_simpset = GlobalSimpset.print;


206 


207 
val simpset_ref_of = #1 o GlobalSimpset.get;

16458

208 
val simpset_ref_of_sg = simpset_ref_of;

16014

209 
val get_context_ss = #2 o GlobalSimpset.get o ProofContext.theory_of;


210 


211 
fun map_context_ss f = GlobalSimpset.map (apsnd


212 
(fn ContextSS {simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers} =>


213 
make_context_ss (f (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers))));


214 


215 


216 
(* access global simpset *)


217 

16458

218 
val simpset_of = ! o simpset_ref_of;


219 
val simpset_of_sg = simpset_of;

16014

220 

16458

221 
fun SIMPSET tacf state = tacf (simpset_of (Thm.theory_of_thm state)) state;


222 
fun SIMPSET' tacf i state = tacf (simpset_of (Thm.theory_of_thm state)) i state;

16014

223 


224 
val simpset = simpset_of o Context.the_context;

16458

225 
val simpset_ref = simpset_ref_of o Context.the_context;

16014

226 


227 


228 
(* change global simpset *)


229 


230 
fun change_simpset_of f x thy =


231 
let val r = simpset_ref_of thy


232 
in r := f (! r, x); thy end;


233 


234 
fun change_simpset f x = (change_simpset_of f x (Context.the_context ()); ());


235 


236 
val Addsimps = change_simpset (op addsimps);


237 
val Delsimps = change_simpset (op delsimps);


238 
val Addsimprocs = change_simpset (op addsimprocs);


239 
val Delsimprocs = change_simpset (op delsimprocs);


240 
val Addcongs = change_simpset (op addcongs);


241 
val Delcongs = change_simpset (op delcongs);


242 


243 


244 
(* change context dependent components *)


245 


246 
fun add_context_simprocs procs =


247 
map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>


248 
(merge_context_simprocs procs simprocs, subgoal_tac, loop_tacs,


249 
unsafe_solvers, solvers));


250 


251 
fun del_context_simprocs procs =


252 
map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>


253 
(gen_rems eq_context_simproc (simprocs, procs), subgoal_tac, loop_tacs,


254 
unsafe_solvers, solvers));


255 


256 
fun set_context_subgoaler tac =


257 
map_context_ss (fn (simprocs, _, loop_tacs, unsafe_solvers, solvers) =>


258 
(simprocs, SOME tac, loop_tacs, unsafe_solvers, solvers));


259 


260 
val reset_context_subgoaler =


261 
map_context_ss (fn (simprocs, _, loop_tacs, unsafe_solvers, solvers) =>


262 
(simprocs, NONE, loop_tacs, unsafe_solvers, solvers));


263 


264 
fun add_context_looper (name, tac) =


265 
map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>


266 
(simprocs, subgoal_tac, merge_alists [(name, tac)] loop_tacs,


267 
unsafe_solvers, solvers));


268 


269 
fun del_context_looper name =


270 
map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>


271 
(simprocs, subgoal_tac, filter_out (equal name o #1) loop_tacs,


272 
unsafe_solvers, solvers));


273 


274 
fun add_context_unsafe_solver solver =


275 
map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>


276 
(simprocs, subgoal_tac, loop_tacs,


277 
merge_context_solvers [solver] unsafe_solvers, solvers));


278 


279 
fun add_context_safe_solver solver =


280 
map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>


281 
(simprocs, subgoal_tac, loop_tacs, unsafe_solvers,


282 
merge_context_solvers [solver] solvers));


283 


284 


285 
(* proof data kind 'Pure/simpset' *)


286 

16458

287 
structure LocalSimpset = ProofDataFun


288 
(struct

16014

289 
val name = "Pure/simpset";


290 
type T = simpset;


291 
val init = simpset_of;


292 
fun print ctxt ss = print_ss (context_ss ctxt ss (get_context_ss ctxt));

16458

293 
end);

16014

294 


295 
val _ = Context.add_setup [LocalSimpset.init];


296 
val print_local_simpset = LocalSimpset.print;


297 


298 
val get_local_simpset = LocalSimpset.get;


299 
val put_local_simpset = LocalSimpset.put;


300 
fun map_local_simpset f ctxt = put_local_simpset (f (get_local_simpset ctxt)) ctxt;


301 


302 
fun local_simpset_of ctxt =


303 
context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);


304 


305 


306 
(* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset


307 
also added methods to retrieve them. *)


308 
(* CB: changed "delta simpsets" to context data,


309 
moved counter to here, it is no longer a ref *)


310 


311 
structure DeltaSimpsetArgs =


312 
struct


313 
val name = "Pure/delta_simpset";


314 
type T = Thm.thm list * int; (*the type is thm list * int*)


315 
fun init _ = ([], 0);


316 
fun print ctxt thms = ();


317 
end;


318 


319 
structure DeltaSimpsetData = ProofDataFun(DeltaSimpsetArgs);


320 
val _ = Context.add_setup [DeltaSimpsetData.init];


321 


322 
val get_delta_simpset = #1 o DeltaSimpsetData.get;


323 
fun put_delta_simpset ss = DeltaSimpsetData.map (fn (_, i) => (ss, i));


324 
fun delta_increment ctxt =


325 
let val ctxt' = DeltaSimpsetData.map (fn (ss, i) => (ss, i+1)) ctxt


326 
in (ctxt', #2 (DeltaSimpsetData.get ctxt'))


327 
end;


328 


329 
(* Jia: added to rename a local thm if necessary *)


330 
local


331 
fun rename_thm' (ctxt,thm) =


332 
let val (new_ctxt, new_id) = delta_increment ctxt


333 
val new_name = "anon_simp_" ^ (string_of_int new_id)


334 
in


335 
(new_ctxt, Thm.name_thm(new_name,thm))


336 
end;


337 


338 
in


339 


340 
fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);


341 


342 
end


343 


344 
(* attributes *)


345 


346 
fun change_global_ss f (thy, th) =


347 
let val r = simpset_ref_of thy


348 
in r := f (! r, [th]); (thy, th) end;


349 


350 
fun change_local_ss f (ctxt, th) =


351 
let val ss = f (get_local_simpset ctxt, [th])


352 
in (put_local_simpset ss ctxt, th) end;


353 


354 
val simp_add_global = change_global_ss (op addsimps);


355 
val simp_del_global = change_global_ss (op delsimps);


356 


357 


358 


359 


360 


361 
(* Jia: note: when simplifier rules are added to local_simpset, they are also added to delta_simpset in ProofContext.context, but not removed if simp_del_local is called *)


362 
fun simp_add_local (ctxt,th) =


363 
let val delta_ss = get_delta_simpset ctxt


364 
val thm_name = Thm.name_of_thm th


365 
val (ctxt', th') =


366 
if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)


367 
val new_dss = th'::delta_ss


368 
val ctxt'' = put_delta_simpset new_dss ctxt'


369 
in


370 
change_local_ss (op addsimps) (ctxt'',th)


371 
end;


372 


373 
val simp_del_local = change_local_ss (op delsimps);


374 


375 
val cong_add_global = change_global_ss (op addcongs);


376 
val cong_del_global = change_global_ss (op delcongs);


377 
val cong_add_local = change_local_ss (op addcongs);


378 
val cong_del_local = change_local_ss (op delcongs);


379 


380 


381 
val simp_tac = generic_simp_tac false (false, false, false);


382 
val asm_simp_tac = generic_simp_tac false (false, true, false);


383 
val full_simp_tac = generic_simp_tac false (true, false, false);


384 
val asm_lr_simp_tac = generic_simp_tac false (true, true, false);


385 
val asm_full_simp_tac = generic_simp_tac false (true, true, true);


386 
val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);


387 


388 


389 


390 
(*the abstraction over the proof state delays the dereferencing*)


391 
fun Simp_tac i st = simp_tac (simpset ()) i st;


392 
fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st;


393 
fun Full_simp_tac i st = full_simp_tac (simpset ()) i st;


394 
fun Asm_lr_simp_tac i st = asm_lr_simp_tac (simpset ()) i st;


395 
fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;


396 


397 
val simplify = simp_thm (false, false, false);


398 
val asm_simplify = simp_thm (false, true, false);


399 
val full_simplify = simp_thm (true, false, false);


400 
val asm_lr_simplify = simp_thm (true, true, false);


401 
val asm_full_simplify = simp_thm (true, true, true);


402 


403 
val rewrite = simp_cterm (false, false, false);


404 
val asm_rewrite = simp_cterm (false, true, false);


405 
val full_rewrite = simp_cterm (true, false, false);


406 
val asm_lr_rewrite = simp_cterm (true, true, false);


407 
val asm_full_rewrite = simp_cterm (true, true, true);


408 


409 


410 


411 
(** concrete syntax of attributes **)


412 


413 
(* add / del *)


414 


415 
val simpN = "simp";


416 
val congN = "cong";


417 
val addN = "add";


418 
val delN = "del";


419 
val onlyN = "only";


420 
val no_asmN = "no_asm";


421 
val no_asm_useN = "no_asm_use";


422 
val no_asm_simpN = "no_asm_simp";


423 
val asm_lrN = "asm_lr";


424 


425 
val simp_attr =


426 
(Attrib.add_del_args simp_add_global simp_del_global,


427 
Attrib.add_del_args simp_add_local simp_del_local);


428 


429 
val cong_attr =


430 
(Attrib.add_del_args cong_add_global cong_del_global,


431 
Attrib.add_del_args cong_add_local cong_del_local);


432 


433 


434 
(* conversions *)


435 


436 
local


437 


438 
fun conv_mode x =


439 
((Args.parens (Args.$$$ no_asmN) >> K simplify 


440 
Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify 


441 
Args.parens (Args.$$$ no_asm_useN) >> K full_simplify 


442 
Scan.succeed asm_full_simplify) > Scan.lift) x;


443 


444 
fun simplified_att get args =


445 
Attrib.syntax (conv_mode  args >> (fn (f, ths) =>


446 
Drule.rule_attribute (fn x => f ((if null ths then I else clear_ss) (get x) addsimps ths))));


447 


448 
in


449 


450 
val simplified_attr =


451 
(simplified_att simpset_of Attrib.global_thmss,


452 
simplified_att local_simpset_of Attrib.local_thmss);


453 


454 
end;


455 


456 


457 
(* setup attributes *)


458 


459 
val _ = Context.add_setup


460 
[Attrib.add_attributes


461 
[(simpN, simp_attr, "declaration of simplification rule"),


462 
(congN, cong_attr, "declaration of Simplifier congruence rule"),


463 
("simplified", simplified_attr, "simplified rule")]];


464 


465 


466 


467 
(** proof methods **)


468 


469 
(* simplification *)


470 


471 
val simp_options =


472 
(Args.parens (Args.$$$ no_asmN) >> K simp_tac 


473 
Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac 


474 
Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac 


475 
Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac 


476 
Scan.succeed asm_full_simp_tac);


477 


478 
val cong_modifiers =


479 
[Args.$$$ congN  Args.colon >> K ((I, cong_add_local):Method.modifier),


480 
Args.$$$ congN  Args.add  Args.colon >> K (I, cong_add_local),


481 
Args.$$$ congN  Args.del  Args.colon >> K (I, cong_del_local)];


482 


483 
val simp_modifiers =


484 
[Args.$$$ simpN  Args.colon >> K (I, simp_add_local),


485 
Args.$$$ simpN  Args.add  Args.colon >> K (I, simp_add_local),


486 
Args.$$$ simpN  Args.del  Args.colon >> K (I, simp_del_local),


487 
Args.$$$ simpN  Args.$$$ onlyN  Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]


488 
@ cong_modifiers;


489 


490 
val simp_modifiers' =


491 
[Args.add  Args.colon >> K (I, simp_add_local),


492 
Args.del  Args.colon >> K (I, simp_del_local),


493 
Args.$$$ onlyN  Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]


494 
@ cong_modifiers;


495 


496 
fun simp_args more_mods =


497 
Method.sectioned_args (Args.bang_facts  Scan.lift simp_options) (more_mods @ simp_modifiers');


498 


499 


500 
fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>


501 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN


502 
(CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));


503 


504 
fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>


505 
HEADGOAL (Method.insert_tac (prems @ facts) THEN'


506 
(CHANGED_PROP oo tac) (local_simpset_of ctxt)));


507 


508 


509 
(* setup methods *)


510 


511 
fun setup_methods more_mods = Method.add_methods


512 
[(simpN, simp_args more_mods simp_method', "simplification"),


513 
("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];


514 


515 
fun method_setup mods = [setup_methods mods];


516 


517 


518 
(** easy_setup **)


519 


520 
fun easy_setup reflect trivs =


521 
let


522 
val trivialities = Drule.reflexive_thm :: trivs;


523 


524 
fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];


525 
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;


526 


527 
(*no premature instantiation of variables during simplification*)


528 
fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];


529 
val safe_solver = mk_solver "easy safe" safe_solver_tac;


530 


531 
fun mk_eq thm =


532 
if Logic.is_equals (Thm.concl_of thm) then [thm]


533 
else [thm RS reflect] handle THM _ => [];


534 


535 
fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);


536 


537 
fun init_ss thy =


538 
(simpset_ref_of thy :=


539 
empty_ss setsubgoaler asm_simp_tac


540 
setSSolver safe_solver


541 
setSolver unsafe_solver


542 
setmksimps mksimps; thy);


543 
in method_setup [] @ [init_ss] end;


544 


545 
end;


546 


547 
structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;


548 
open BasicSimplifier;
