author  haftmann 
Mon, 16 Apr 2007 16:11:03 +0200  
changeset 22717  74dbc7696083 
parent 22709  9ab51bac6287 
child 22770  615e19792c92 
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 

16014  58 
val rewrite: simpset > cterm > thm 
59 
val asm_rewrite: simpset > cterm > thm 

60 
val full_rewrite: simpset > cterm > thm 

61 
val asm_lr_rewrite: simpset > cterm > thm 

62 
val asm_full_rewrite: simpset > cterm > thm 

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 

22204  74 
val get_simproc: Proof.context > 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 
100 
(struct 

16014  101 
val name = "Pure/simpset"; 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

102 
type T = simpset ref; 
16014  103 

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

104 
val empty = ref empty_ss; 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

105 
fun copy (ref ss) = ref ss: T; (*create new reference!*) 
17898  106 
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

107 
fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

108 
fun print _ (ref ss) = print_ss ss; 
16458  109 
end); 
16014  110 

18708  111 
val _ = Context.add_setup GlobalSimpset.init; 
16014  112 
val print_simpset = GlobalSimpset.print; 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

113 
val get_simpset = ! o GlobalSimpset.get; 
16014  114 

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

115 
val change_simpset_of = change o GlobalSimpset.get; 
22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21708
diff
changeset

116 
fun change_simpset f = change_simpset_of (ML_Context.the_context ()) f; 
16014  117 

17898  118 
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

119 
val simpset = simpset_of o ML_Context.the_context; 
16014  120 

121 

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

122 
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

123 
fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st; 
16014  124 

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

125 
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

126 
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

127 
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

128 
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

129 
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

130 
fun Delcongs args = change_simpset (fn ss => ss delcongs args); 
16014  131 

132 

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

133 
(* local simpsets *) 
16014  134 

16458  135 
structure LocalSimpset = ProofDataFun 
136 
(struct 

16014  137 
val name = "Pure/simpset"; 
138 
type T = simpset; 

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

139 
val init = get_simpset; 
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

140 
fun print _ ss = print_ss ss; 
16458  141 
end); 
16014  142 

18708  143 
val _ = Context.add_setup LocalSimpset.init; 
16014  144 
val print_local_simpset = LocalSimpset.print; 
145 
val get_local_simpset = LocalSimpset.get; 

146 
val put_local_simpset = LocalSimpset.put; 

147 

17898  148 
fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt); 
16014  149 

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

152 

16014  153 

22201  154 
(* generic simpsets *) 
155 

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

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

158 

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

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

161 

162 

16014  163 
(* attributes *) 
164 

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

18688  167 
val simp_add = attrib (op addsimps); 
168 
val simp_del = attrib (op delsimps); 

169 
val cong_add = attrib (op addcongs); 

170 
val cong_del = attrib (op delcongs); 

16014  171 

172 

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

173 

22201  174 
(** named simprocs **) 
175 

176 
fun err_dup_simprocs ds = 

177 
error ("Duplicate simproc(s): " ^ commas_quote ds); 

178 

22236  179 

22204  180 
(* data *) 
181 

22201  182 
structure Simprocs = GenericDataFun 
183 
( 

184 
val name = "Pure/simprocs"; 

22236  185 
type T = simproc NameSpace.table; 
22201  186 
val empty = NameSpace.empty_table; 
187 
val extend = I; 

22236  188 
fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs 
22201  189 
handle Symtab.DUPS ds => err_dup_simprocs ds; 
190 
fun print _ _ = (); 

191 
); 

22204  192 
val _ = Context.add_setup Simprocs.init; 
22201  193 

22204  194 

195 
(* get simprocs *) 

196 

197 
fun get_simproc ctxt xname = 

198 
let 

199 
val (space, tab) = Simprocs.get (Context.Proof ctxt); 

200 
val name = NameSpace.intern space xname; 

201 
in 

202 
(case Symtab.lookup tab name of 

22236  203 
SOME proc => proc 
22204  204 
 NONE => error ("Undefined simplification procedure: " ^ quote name)) 
205 
end; 

206 

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

208 
("simproc", 

209 
"Simplifier.get_simproc (ML_Context.the_local_context ()) " ^ ML_Syntax.print_string name))); 

210 

211 

212 
(* define simprocs *) 

22201  213 

214 
local 

215 

216 
(* FIXME *) 

217 
fun read_terms ctxt ts = 

218 
#1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] 

22709  219 
(map (rpair dummyT) ts)); 
22201  220 

221 
(* FIXME *) 

222 
fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts; 

223 

22236  224 
fun gen_simproc prep {name, lhss, proc, identifier} lthy = 
22201  225 
let 
22236  226 
val naming = LocalTheory.full_naming lthy; 
227 
val simproc = make_simproc 

228 
{name = LocalTheory.full_name lthy name, 

229 
lhss = 

230 
let 

231 
val lhss' = prep lthy lhss; 

232 
val ctxt' = lthy 

233 
> fold Variable.declare_term lhss' 

234 
> fold Variable.auto_fixes lhss'; 

235 
in Variable.export_terms ctxt' lthy lhss' end 

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

237 
proc = proc, 

238 
identifier = identifier} 

239 
> morph_simproc (LocalTheory.target_morphism lthy); 

22201  240 
in 
241 
lthy > LocalTheory.declaration (fn phi => fn context => 

242 
let 

243 
val name' = Morphism.name phi name; 

22236  244 
val simproc' = morph_simproc phi simproc; 
22201  245 
in 
246 
context 

247 
> Simprocs.map (fn simprocs => 

22236  248 
NameSpace.extend_table naming (simprocs, [(name', simproc')]) 
22201  249 
handle Symtab.DUPS ds => err_dup_simprocs ds) 
22236  250 
> map_ss (fn ss => ss addsimprocs [simproc']) 
22201  251 
end) 
252 
end; 

253 

254 
in 

255 

256 
val def_simproc = gen_simproc read_terms; 

257 
val def_simproc_i = gen_simproc cert_terms; 

258 

259 
end; 

260 

261 

262 

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

263 
(** simplification tactics and rules **) 
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 
fun solve_all_tac solvers ss = 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

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

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

268 
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

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

270 

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

271 
(*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

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

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

274 
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

275 
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

276 
val solve_tac = FIRST' (map (MetaSimplifier.solver ss) 
22717  277 
(rev (if safe then solvers else unsafe_solvers))); 
17967
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 
fun simp_loop_tac i = 
21687  280 
Goal.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

281 
(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

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

283 

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

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

285 

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

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

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

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

290 
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

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

292 

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

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

294 

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

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

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

297 

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

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

299 

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

300 

16806  301 
(* tactics *) 
302 

16014  303 
val simp_tac = generic_simp_tac false (false, false, false); 
304 
val asm_simp_tac = generic_simp_tac false (false, true, false); 

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

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

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

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

309 

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

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

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

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

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

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

316 

16806  317 

318 
(* conversions *) 

319 

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

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

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

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

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

324 
val asm_full_simplify = simp_thm (true, true, true); 
16014  325 

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

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

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

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

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

330 
val asm_full_rewrite = simp_cterm (true, true, true); 
16014  331 

332 

333 

334 
(** concrete syntax of attributes **) 

335 

336 
(* add / del *) 

337 

338 
val simpN = "simp"; 

339 
val congN = "cong"; 

340 
val addN = "add"; 

341 
val delN = "del"; 

342 
val onlyN = "only"; 

343 
val no_asmN = "no_asm"; 

344 
val no_asm_useN = "no_asm_use"; 

345 
val no_asm_simpN = "no_asm_simp"; 

346 
val asm_lrN = "asm_lr"; 

347 

348 

349 
(* conversions *) 

350 

351 
local 

352 

353 
fun conv_mode x = 

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

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

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

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

358 

359 
in 

360 

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

365 
end; 

366 

367 

368 
(* setup attributes *) 

369 

370 
val _ = Context.add_setup 

18708  371 
(Attrib.add_attributes 
18728  372 
[(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rule"), 
373 
(congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"), 

374 
("simplified", simplified, "simplified rule")]); 

16014  375 

376 

377 

378 
(** proof methods **) 

379 

380 
(* simplification *) 

381 

382 
val simp_options = 

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

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

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

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

387 
Scan.succeed asm_full_simp_tac); 

388 

16685  389 
fun simp_flags x = (Scan.repeat 
16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

390 
(Args.parens (Args.$$$ "depth_limit"  Args.colon  Args.nat) 
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

391 
>> setmp MetaSimplifier.simp_depth_limit) 
16709  392 
>> (curry (Library.foldl op o) I o rev)) x; 
16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

393 

16014  394 
val cong_modifiers = 
18728  395 
[Args.$$$ congN  Args.colon >> K ((I, cong_add): Method.modifier), 
396 
Args.$$$ congN  Args.add  Args.colon >> K (I, cong_add), 

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

16014  398 

399 
val simp_modifiers = 

18728  400 
[Args.$$$ simpN  Args.colon >> K (I, simp_add), 
401 
Args.$$$ simpN  Args.add  Args.colon >> K (I, simp_add), 

402 
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

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

407 
val simp_modifiers' = 

18728  408 
[Args.add  Args.colon >> K (I, simp_add), 
409 
Args.del  Args.colon >> K (I, simp_del), 

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

414 
fun simp_args more_mods = 

16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

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

416 
(more_mods @ simp_modifiers'); 
16014  417 

16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

418 
fun simp_method ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts => 
16014  419 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN 
16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

420 
(FLAGS o CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)); 
16014  421 

16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

422 
fun simp_method' ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts => 
16014  423 
HEADGOAL (Method.insert_tac (prems @ facts) THEN' 
16684
7b58002668c0
methods: added simp_flags argument, added "depth_limit" flag;
wenzelm
parents:
16458
diff
changeset

424 
((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt))); 
16014  425 

426 

427 

18708  428 
(** setup **) 
429 

430 
fun method_setup more_mods = Method.add_methods 

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

433 

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

437 

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

439 
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac; 

440 

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

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

443 
val safe_solver = mk_solver "easy safe" safe_solver_tac; 

444 

445 
fun mk_eq thm = 

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

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

18708  450 
in 
451 
GlobalSimpset.get thy := 

452 
empty_ss setsubgoaler asm_simp_tac 

453 
setSSolver safe_solver 

454 
setSolver unsafe_solver 

455 
setmksimps mksimps; 

456 
thy 

457 
end); 

16014  458 

459 
end; 

460 

461 
structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier; 

462 
open BasicSimplifier; 