author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24509  23ee6b7788c2 
child 26425  6561665c5cb1 
permissions  rwrr 
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 
signature BASIC_SIMPLIFIER = 

10 
sig 

11 
include BASIC_META_SIMPLIFIER 

12 
val print_simpset: theory > unit 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

13 
val change_simpset_of: theory > (simpset > simpset) > unit 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

14 
val change_simpset: (simpset > simpset) > unit 
16014  15 
val simpset_of: theory > simpset 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

16 
val simpset: unit > simpset 
16014  17 
val SIMPSET: (simpset > tactic) > tactic 
18 
val SIMPSET': (simpset > 'a > tactic) > 'a > tactic 

19 
val Addsimps: thm list > unit 

20 
val Delsimps: thm list > unit 

21 
val Addsimprocs: simproc list > unit 

22 
val Delsimprocs: simproc list > unit 

23 
val Addcongs: thm list > unit 

24 
val Delcongs: thm list > unit 

25 
val local_simpset_of: Proof.context > simpset 

17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

26 
val generic_simp_tac: bool > bool * bool * bool > simpset > int > tactic 
16014  27 
val safe_asm_full_simp_tac: simpset > int > tactic 
28 
val simp_tac: simpset > int > tactic 

29 
val asm_simp_tac: simpset > int > tactic 

30 
val full_simp_tac: simpset > int > tactic 

31 
val asm_lr_simp_tac: simpset > int > tactic 

32 
val asm_full_simp_tac: simpset > int > tactic 

33 
val Simp_tac: int > tactic 

34 
val Asm_simp_tac: int > tactic 

35 
val Full_simp_tac: int > tactic 

36 
val Asm_lr_simp_tac: int > tactic 

37 
val Asm_full_simp_tac: int > tactic 

38 
val simplify: simpset > thm > thm 

39 
val asm_simplify: simpset > thm > thm 

40 
val full_simplify: simpset > thm > thm 

41 
val asm_lr_simplify: simpset > thm > thm 

42 
val asm_full_simplify: simpset > thm > thm 

43 
end; 

44 

45 
signature SIMPLIFIER = 

46 
sig 

47 
include BASIC_SIMPLIFIER 

17004  48 
val clear_ss: simpset > simpset 
17723  49 
val debug_bounds: bool ref 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

50 
val inherit_context: simpset > simpset > simpset 
17898  51 
val the_context: simpset > Proof.context 
52 
val context: Proof.context > simpset > simpset 

53 
val theory_context: theory > simpset > simpset 

16458  54 
val simproc_i: theory > string > term list 
55 
> (theory > simpset > term > thm option) > simproc 

56 
val simproc: theory > string > string list 

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

23598  58 
val rewrite: simpset > conv 
59 
val asm_rewrite: simpset > conv 

60 
val full_rewrite: simpset > conv 

61 
val asm_lr_rewrite: simpset > conv 

62 
val asm_full_rewrite: simpset > conv 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

63 
val get_simpset: theory > simpset 
16014  64 
val print_local_simpset: Proof.context > unit 
65 
val get_local_simpset: Proof.context > simpset 

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

22379  67 
val get_ss: Context.generic > simpset 
68 
val map_ss: (simpset > simpset) > Context.generic > Context.generic 

18728  69 
val attrib: (simpset * thm list > simpset) > attribute 
70 
val simp_add: attribute 

71 
val simp_del: attribute 

72 
val cong_add: attribute 

73 
val cong_del: attribute 

24024  74 
val get_simproc: Context.generic > xstring > simproc 
22236  75 
val def_simproc: {name: string, lhss: string list, 
76 
proc: morphism > simpset > cterm > thm option, identifier: thm list} > 

22201  77 
local_theory > local_theory 
22236  78 
val def_simproc_i: {name: string, lhss: term list, 
79 
proc: morphism > simpset > cterm > thm option, identifier: thm list} > 

22201  80 
local_theory > local_theory 
18033  81 
val cong_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
82 
val simp_modifiers': (Args.T list > (Method.modifier * Args.T list)) list 

16014  83 
val simp_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
84 
val method_setup: (Args.T list > (Method.modifier * Args.T list)) list 

18708  85 
> theory > theory 
86 
val easy_setup: thm > thm list > theory > theory 

16014  87 
end; 
88 

89 
structure Simplifier: SIMPLIFIER = 

90 
struct 

91 

21708  92 
open MetaSimplifier; 
93 

94 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

95 
(** simpset data **) 
16014  96 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

97 
(* global simpsets *) 
16014  98 

16458  99 
structure GlobalSimpset = TheoryDataFun 
22846  100 
( 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

101 
type T = simpset ref; 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

102 
val empty = ref empty_ss; 
22846  103 
fun copy (ref ss) = ref ss: T; 
17898  104 
fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss); 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

105 
fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); 
22846  106 
); 
16014  107 

18708  108 
val _ = Context.add_setup GlobalSimpset.init; 
22846  109 
fun print_simpset thy = print_ss (! (GlobalSimpset.get thy)); 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

110 
val get_simpset = ! o GlobalSimpset.get; 
16014  111 

24024  112 
fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f); 
113 
fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_context ()) f); 

16014  114 

17898  115 
fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy); 
22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21708
diff
changeset

116 
val simpset = simpset_of o ML_Context.the_context; 
16014  117 

118 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

119 
fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st; 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

120 
fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st; 
16014  121 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

122 
fun Addsimps args = change_simpset (fn ss => ss addsimps args); 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

123 
fun Delsimps args = change_simpset (fn ss => ss delsimps args); 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

124 
fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args); 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

125 
fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args); 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

126 
fun Addcongs args = change_simpset (fn ss => ss addcongs args); 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

127 
fun Delcongs args = change_simpset (fn ss => ss delcongs args); 
16014  128 

129 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

130 
(* local simpsets *) 
16014  131 

16458  132 
structure LocalSimpset = ProofDataFun 
22846  133 
( 
16014  134 
type T = simpset; 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

135 
val init = get_simpset; 
22846  136 
); 
16014  137 

22846  138 
val print_local_simpset = print_ss o LocalSimpset.get; 
16014  139 
val get_local_simpset = LocalSimpset.get; 
140 
val put_local_simpset = LocalSimpset.put; 

141 

17898  142 
fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt); 
16014  143 

22132  144 
val _ = ML_Context.value_antiq "simpset" 
145 
(Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())")); 

146 

16014  147 

22201  148 
(* generic simpsets *) 
149 

150 
fun get_ss (Context.Theory thy) = simpset_of thy 

151 
 get_ss (Context.Proof ctxt) = local_simpset_of ctxt; 

152 

153 
fun map_ss f (Context.Theory thy) = (change_simpset_of thy f; Context.Theory thy) 

154 
 map_ss f (Context.Proof ctxt) = Context.Proof (LocalSimpset.map f ctxt); 

155 

156 

16014  157 
(* attributes *) 
158 

22201  159 
fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th]))); 
16014  160 

18688  161 
val simp_add = attrib (op addsimps); 
162 
val simp_del = attrib (op delsimps); 

163 
val cong_add = attrib (op addcongs); 

164 
val cong_del = attrib (op delcongs); 

16014  165 

166 

17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

167 

22201  168 
(** named simprocs **) 
169 

23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23598
diff
changeset

170 
fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name); 
22201  171 

22236  172 

22204  173 
(* data *) 
174 

22201  175 
structure Simprocs = GenericDataFun 
176 
( 

22236  177 
type T = simproc NameSpace.table; 
22201  178 
val empty = NameSpace.empty_table; 
179 
val extend = I; 

22236  180 
fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23598
diff
changeset

181 
handle Symtab.DUP dup => err_dup_simproc dup; 
22201  182 
); 
183 

22204  184 

185 
(* get simprocs *) 

186 

24024  187 
fun get_simproc context xname = 
22204  188 
let 
24024  189 
val (space, tab) = Simprocs.get context; 
22204  190 
val name = NameSpace.intern space xname; 
191 
in 

192 
(case Symtab.lookup tab name of 

22236  193 
SOME proc => proc 
22204  194 
 NONE => error ("Undefined simplification procedure: " ^ quote name)) 
195 
end; 

196 

197 
val _ = ML_Context.value_antiq "simproc" (Scan.lift Args.name >> (fn name => 

198 
("simproc", 

24024  199 
"Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name))); 
22204  200 

201 

202 
(* define simprocs *) 

22201  203 

204 
local 

205 

22236  206 
fun gen_simproc prep {name, lhss, proc, identifier} lthy = 
22201  207 
let 
22236  208 
val naming = LocalTheory.full_naming lthy; 
209 
val simproc = make_simproc 

210 
{name = LocalTheory.full_name lthy name, 

211 
lhss = 

212 
let 

213 
val lhss' = prep lthy lhss; 

214 
val ctxt' = lthy 

215 
> fold Variable.declare_term lhss' 

216 
> fold Variable.auto_fixes lhss'; 

217 
in Variable.export_terms ctxt' lthy lhss' end 

218 
> map (Thm.cterm_of (ProofContext.theory_of lthy)), 

219 
proc = proc, 

220 
identifier = identifier} 

221 
> morph_simproc (LocalTheory.target_morphism lthy); 

22201  222 
in 
24024  223 
lthy > LocalTheory.declaration (fn phi => 
22201  224 
let 
225 
val name' = Morphism.name phi name; 

22236  226 
val simproc' = morph_simproc phi simproc; 
22201  227 
in 
24024  228 
Simprocs.map (fn simprocs => 
23086  229 
NameSpace.extend_table naming [(name', simproc')] simprocs 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23598
diff
changeset

230 
handle Symtab.DUP dup => err_dup_simproc dup) 
24024  231 
#> map_ss (fn ss => ss addsimprocs [simproc']) 
22201  232 
end) 
233 
end; 

234 

235 
in 

236 

24509
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24124
diff
changeset

237 
val def_simproc = gen_simproc Syntax.read_terms; 
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24124
diff
changeset

238 
val def_simproc_i = gen_simproc Syntax.check_terms; 
22201  239 

240 
end; 

241 

242 

243 

17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

244 
(** simplification tactics and rules **) 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

245 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

246 
fun solve_all_tac solvers ss = 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

247 
let 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

248 
val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

249 
val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

250 
in DEPTH_SOLVE (solve_tac 1) end; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

251 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

252 
(*NOTE: may instantiate unknowns that appear also in other subgoals*) 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

253 
fun generic_simp_tac safe mode ss = 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

254 
let 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

255 
val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss; 
21286
b5e7b80caa6a
introduces canonical AList functions for loop_tacs
haftmann
parents:
20872
diff
changeset

256 
val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); 
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

257 
val solve_tac = FIRST' (map (MetaSimplifier.solver ss) 
22717  258 
(rev (if safe then solvers else unsafe_solvers))); 
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

259 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

260 
fun simp_loop_tac i = 
23536
60a1672e298e
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
wenzelm
parents:
23086
diff
changeset

261 
asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN 
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

262 
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

263 
in simp_loop_tac end; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

264 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

265 
local 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

266 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

267 
fun simp rew mode ss thm = 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

268 
let 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

269 
val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss; 
22717  270 
val tacf = solve_all_tac (rev unsafe_solvers); 
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

271 
fun prover s th = Option.map #1 (Seq.pull (tacf s th)); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

272 
in rew mode prover ss thm end; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

273 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

274 
in 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

275 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

276 
val simp_thm = simp MetaSimplifier.rewrite_thm; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

277 
val simp_cterm = simp MetaSimplifier.rewrite_cterm; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

278 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

279 
end; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

280 

7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

281 

16806  282 
(* tactics *) 
283 

16014  284 
val simp_tac = generic_simp_tac false (false, false, false); 
285 
val asm_simp_tac = generic_simp_tac false (false, true, false); 

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

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

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

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

290 

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

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

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

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

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

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

297 

16806  298 

299 
(* conversions *) 

300 

17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

301 
val simplify = simp_thm (false, false, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

302 
val asm_simplify = simp_thm (false, true, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

303 
val full_simplify = simp_thm (true, false, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

304 
val asm_lr_simplify = simp_thm (true, true, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

305 
val asm_full_simplify = simp_thm (true, true, true); 
16014  306 

17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

307 
val rewrite = simp_cterm (false, false, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

308 
val asm_rewrite = simp_cterm (false, true, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

309 
val full_rewrite = simp_cterm (true, false, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

310 
val asm_lr_rewrite = simp_cterm (true, true, false); 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

311 
val asm_full_rewrite = simp_cterm (true, true, true); 
16014  312 

313 

314 

315 
(** concrete syntax of attributes **) 

316 

317 
(* add / del *) 

318 

319 
val simpN = "simp"; 

320 
val congN = "cong"; 

321 
val addN = "add"; 

322 
val delN = "del"; 

323 
val onlyN = "only"; 

324 
val no_asmN = "no_asm"; 

325 
val no_asm_useN = "no_asm_use"; 

326 
val no_asm_simpN = "no_asm_simp"; 

327 
val asm_lrN = "asm_lr"; 

328 

329 

24024  330 
(* simprocs *) 
331 

332 
local 

333 

334 
val add_del = 

335 
(Args.del  Args.colon >> K (op delsimprocs)  

336 
Scan.option (Args.add  Args.colon) >> K (op addsimprocs)) 

337 
>> (fn f => fn simproc => fn phi => Thm.declaration_attribute 

338 
(K (map_ss (fn ss => f (ss, [morph_simproc phi simproc]))))); 

339 

340 
in 

341 

342 
val simproc_att = Attrib.syntax 

343 
(Scan.peek (fn context => 

344 
add_del : (fn decl => 

345 
Scan.repeat1 (Args.named_attribute (decl o get_simproc context)) 

346 
>> (Library.apply o map Morphism.form)))); 

347 

348 
end; 

24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset

349 

24024  350 

16014  351 
(* conversions *) 
352 

353 
local 

354 

355 
fun conv_mode x = 

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

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

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

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

360 

361 
in 

362 

18688  363 
val simplified = 
18988  364 
Attrib.syntax (conv_mode  Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn x => 
18688  365 
f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths)))); 
16014  366 

367 
end; 

368 

369 

370 
(* setup attributes *) 

371 

372 
val _ = Context.add_setup 

18708  373 
(Attrib.add_attributes 
24024  374 
[(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"), 
18728  375 
(congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"), 
24024  376 
("simproc", simproc_att, "declaration of simplification procedures"), 
18728  377 
("simplified", simplified, "simplified rule")]); 
16014  378 

379 

380 

381 
(** proof methods **) 

382 

383 
(* simplification *) 

384 

385 
val simp_options = 

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

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

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

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

390 
Scan.succeed asm_full_simp_tac); 

391 

392 
val cong_modifiers = 

18728  393 
[Args.$$$ congN  Args.colon >> K ((I, cong_add): Method.modifier), 
394 
Args.$$$ congN  Args.add  Args.colon >> K (I, cong_add), 

395 
Args.$$$ congN  Args.del  Args.colon >> K (I, cong_del)]; 

16014  396 

397 
val simp_modifiers = 

18728  398 
[Args.$$$ simpN  Args.colon >> K (I, simp_add), 
399 
Args.$$$ simpN  Args.add  Args.colon >> K (I, simp_add), 

400 
Args.$$$ simpN  Args.del  Args.colon >> K (I, simp_del), 

17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

401 
Args.$$$ simpN  Args.$$$ onlyN  Args.colon 
18728  402 
>> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)] 
16014  403 
@ cong_modifiers; 
404 

405 
val simp_modifiers' = 

18728  406 
[Args.add  Args.colon >> K (I, simp_add), 
407 
Args.del  Args.colon >> K (I, simp_del), 

18688  408 
Args.$$$ onlyN  Args.colon 
18728  409 
>> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)] 
16014  410 
@ cong_modifiers; 
411 

412 
fun simp_args more_mods = 

24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset

413 
Method.sectioned_args (Args.bang_facts  Scan.lift simp_options) 
16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

414 
(more_mods @ simp_modifiers'); 
16014  415 

24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset

416 
fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts => 
16014  417 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN 
24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset

418 
(CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)); 
16014  419 

24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset

420 
fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts => 
16014  421 
HEADGOAL (Method.insert_tac (prems @ facts) THEN' 
24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset

422 
((CHANGED_PROP) oo tac) (local_simpset_of ctxt))); 
16014  423 

424 

425 

18708  426 
(** setup **) 
427 

428 
fun method_setup more_mods = Method.add_methods 

16014  429 
[(simpN, simp_args more_mods simp_method', "simplification"), 
430 
("simp_all", simp_args more_mods simp_method, "simplification (all goals)")]; 

431 

18708  432 
fun easy_setup reflect trivs = method_setup [] #> (fn thy => 
16014  433 
let 
434 
val trivialities = Drule.reflexive_thm :: trivs; 

435 

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

437 
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac; 

438 

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

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

441 
val safe_solver = mk_solver "easy safe" safe_solver_tac; 

442 

443 
fun mk_eq thm = 

20872  444 
if can Logic.dest_equals (Thm.concl_of thm) then [thm] 
16014  445 
else [thm RS reflect] handle THM _ => []; 
446 

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

24024  448 
val _ = CRITICAL (fn () => 
449 
GlobalSimpset.get thy := 

450 
empty_ss setsubgoaler asm_simp_tac 

451 
setSSolver safe_solver 

452 
setSolver unsafe_solver 

453 
setmksimps mksimps); 

454 
in thy end); 

16014  455 

456 
end; 

457 

458 
structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier; 

459 
open BasicSimplifier; 