author  wenzelm 
Sat, 30 May 2009 12:53:11 +0200  
changeset 31300  40fa39d9bce7 
parent 30609  983e8b6e4e69 
child 32091  30e2ffbba718 
permissions  rwrr 
16014  1 
(* Title: Pure/simplifier.ML 
2 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 

3 

4 
Generic simplifier, suitable for most logics (see also 

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

6 
*) 

7 

8 
signature BASIC_SIMPLIFIER = 

9 
sig 

10 
include BASIC_META_SIMPLIFIER 

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

11 
val change_simpset: (simpset > simpset) > unit 
16014  12 
val simpset_of: theory > simpset 
13 
val Addsimprocs: simproc list > unit 

14 
val Delsimprocs: simproc list > unit 

15 
val local_simpset_of: Proof.context > simpset 

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

16 
val generic_simp_tac: bool > bool * bool * bool > simpset > int > tactic 
16014  17 
val safe_asm_full_simp_tac: simpset > int > tactic 
18 
val simp_tac: simpset > int > tactic 

19 
val asm_simp_tac: simpset > int > tactic 

20 
val full_simp_tac: simpset > int > tactic 

21 
val asm_lr_simp_tac: simpset > int > tactic 

22 
val asm_full_simp_tac: simpset > int > tactic 

23 
val simplify: simpset > thm > thm 

24 
val asm_simplify: simpset > thm > thm 

25 
val full_simplify: simpset > thm > thm 

26 
val asm_lr_simplify: simpset > thm > thm 

27 
val asm_full_simplify: simpset > thm > thm 

28 
end; 

29 

30 
signature SIMPLIFIER = 

31 
sig 

32 
include BASIC_SIMPLIFIER 

30356  33 
val pretty_ss: Proof.context > simpset > Pretty.T 
17004  34 
val clear_ss: simpset > simpset 
17723  35 
val debug_bounds: bool ref 
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset

36 
val inherit_context: simpset > simpset > simpset 
17898  37 
val the_context: simpset > Proof.context 
38 
val context: Proof.context > simpset > simpset 

39 
val theory_context: theory > simpset > simpset 

16458  40 
val simproc_i: theory > string > term list 
41 
> (theory > simpset > term > thm option) > simproc 

42 
val simproc: theory > string > string list 

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

23598  44 
val rewrite: simpset > conv 
45 
val asm_rewrite: simpset > conv 

46 
val full_rewrite: simpset > conv 

47 
val asm_lr_rewrite: simpset > conv 

48 
val asm_full_rewrite: simpset > conv 

22379  49 
val get_ss: Context.generic > simpset 
50 
val map_ss: (simpset > simpset) > Context.generic > Context.generic 

18728  51 
val attrib: (simpset * thm list > simpset) > attribute 
52 
val simp_add: attribute 

53 
val simp_del: attribute 

54 
val cong_add: attribute 

55 
val cong_del: attribute 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

56 
val map_simpset: (simpset > simpset) > theory > theory 
24024  57 
val get_simproc: Context.generic > xstring > simproc 
22236  58 
val def_simproc: {name: string, lhss: string list, 
59 
proc: morphism > simpset > cterm > thm option, identifier: thm list} > 

22201  60 
local_theory > local_theory 
22236  61 
val def_simproc_i: {name: string, lhss: term list, 
62 
proc: morphism > simpset > cterm > thm option, identifier: thm list} > 

22201  63 
local_theory > local_theory 
30513  64 
val cong_modifiers: Method.modifier parser list 
65 
val simp_modifiers': Method.modifier parser list 

66 
val simp_modifiers: Method.modifier parser list 

67 
val method_setup: Method.modifier parser list > theory > theory 

18708  68 
val easy_setup: thm > thm list > theory > theory 
16014  69 
end; 
70 

71 
structure Simplifier: SIMPLIFIER = 

72 
struct 

73 

21708  74 
open MetaSimplifier; 
75 

76 

30356  77 
(** pretty printing **) 
78 

79 
fun pretty_ss ctxt ss = 

80 
let 

81 
val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of; 

82 
val pretty_thm = ProofContext.pretty_thm ctxt; 

83 
fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss); 

84 
fun pretty_cong (name, thm) = 

85 
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm]; 

86 

87 
val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; 

88 
in 

89 
[Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps), 

90 
Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)), 

91 
Pretty.big_list "congruences:" (map pretty_cong congs), 

92 
Pretty.strs ("loopers:" :: map quote loopers), 

93 
Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers), 

94 
Pretty.strs ("safe solvers:" :: map quote safe_solvers)] 

95 
> Pretty.chunks 

96 
end; 

97 

98 

99 

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

100 
(** simpset data **) 
16014  101 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

102 
structure SimpsetData = GenericDataFun 
22846  103 
( 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

104 
type T = simpset; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

105 
val empty = empty_ss; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

106 
fun extend ss = MetaSimplifier.inherit_context empty_ss ss; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

107 
fun merge _ = merge_ss; 
22846  108 
); 
16014  109 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

110 
val get_ss = SimpsetData.get; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

111 
val map_ss = SimpsetData.map; 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

112 

1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

113 

1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

114 
(* attributes *) 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

115 

1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

116 
fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th]))); 
16014  117 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

118 
val simp_add = attrib (op addsimps); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

119 
val simp_del = attrib (op delsimps); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

120 
val cong_add = attrib (op addcongs); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

121 
val cong_del = attrib (op delcongs); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

122 

16014  123 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

124 
(* global simpset *) 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

125 

1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

126 
fun map_simpset f = Context.theory_map (map_ss f); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

127 
fun change_simpset f = Context.>> (Context.map_theory (map_simpset f)); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

128 
fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy)); 
16014  129 

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

130 
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

131 
fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args); 
16014  132 

133 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

134 
(* local simpset *) 
16014  135 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

136 
fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt)); 
16014  137 

27338  138 
val _ = ML_Antiquote.value "simpset" 
139 
(Scan.succeed "Simplifier.local_simpset_of (ML_Context.the_local_context ())"); 

22132  140 

16014  141 

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

142 

22201  143 
(** named simprocs **) 
144 

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

145 
fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name); 
22201  146 

22236  147 

22204  148 
(* data *) 
149 

22201  150 
structure Simprocs = GenericDataFun 
151 
( 

22236  152 
type T = simproc NameSpace.table; 
22201  153 
val empty = NameSpace.empty_table; 
154 
val extend = I; 

22236  155 
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

156 
handle Symtab.DUP dup => err_dup_simproc dup; 
22201  157 
); 
158 

22204  159 

160 
(* get simprocs *) 

161 

24024  162 
fun get_simproc context xname = 
22204  163 
let 
24024  164 
val (space, tab) = Simprocs.get context; 
22204  165 
val name = NameSpace.intern space xname; 
166 
in 

167 
(case Symtab.lookup tab name of 

22236  168 
SOME proc => proc 
22204  169 
 NONE => error ("Undefined simplification procedure: " ^ quote name)) 
170 
end; 

171 

27338  172 
val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name => 
173 
"Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name)); 

22204  174 

175 

176 
(* define simprocs *) 

22201  177 

178 
local 

179 

22236  180 
fun gen_simproc prep {name, lhss, proc, identifier} lthy = 
22201  181 
let 
28991  182 
val b = Binding.name name; 
22236  183 
val naming = LocalTheory.full_naming lthy; 
184 
val simproc = make_simproc 

28991  185 
{name = LocalTheory.full_name lthy b, 
22236  186 
lhss = 
187 
let 

188 
val lhss' = prep lthy lhss; 

189 
val ctxt' = lthy 

190 
> fold Variable.declare_term lhss' 

191 
> fold Variable.auto_fixes lhss'; 

192 
in Variable.export_terms ctxt' lthy lhss' end 

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

194 
proc = proc, 

195 
identifier = identifier} 

196 
> morph_simproc (LocalTheory.target_morphism lthy); 

22201  197 
in 
24024  198 
lthy > LocalTheory.declaration (fn phi => 
22201  199 
let 
28991  200 
val b' = Morphism.binding phi b; 
22236  201 
val simproc' = morph_simproc phi simproc; 
22201  202 
in 
24024  203 
Simprocs.map (fn simprocs => 
30466  204 
NameSpace.define naming (b', simproc') simprocs > snd 
28863  205 
handle Symtab.DUP dup => err_dup_simproc dup) 
24024  206 
#> map_ss (fn ss => ss addsimprocs [simproc']) 
22201  207 
end) 
208 
end; 

209 

210 
in 

211 

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

212 
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

213 
val def_simproc_i = gen_simproc Syntax.check_terms; 
22201  214 

215 
end; 

216 

217 

218 

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

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

220 

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

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

222 
let 
30336  223 
val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss; 
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

224 
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

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

226 

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

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

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

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

231 
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

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

234 

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

235 
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

236 
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

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

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

239 

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

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

241 

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

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

243 
let 
30336  244 
val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss; 
22717  245 
val tacf = solve_all_tac (rev unsafe_solvers); 
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

246 
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

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

248 

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

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

250 

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

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

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

253 

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

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

255 

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

256 

16806  257 
(* tactics *) 
258 

16014  259 
val simp_tac = generic_simp_tac false (false, false, false); 
260 
val asm_simp_tac = generic_simp_tac false (false, true, false); 

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

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

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

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

265 

16806  266 

267 
(* conversions *) 

268 

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

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

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

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

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

273 
val asm_full_simplify = simp_thm (true, true, true); 
16014  274 

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

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

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

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

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

279 
val asm_full_rewrite = simp_cterm (true, true, true); 
16014  280 

281 

282 

283 
(** concrete syntax of attributes **) 

284 

285 
(* add / del *) 

286 

287 
val simpN = "simp"; 

288 
val congN = "cong"; 

289 
val addN = "add"; 

290 
val delN = "del"; 

291 
val onlyN = "only"; 

292 
val no_asmN = "no_asm"; 

293 
val no_asm_useN = "no_asm_use"; 

294 
val no_asm_simpN = "no_asm_simp"; 

295 
val asm_lrN = "asm_lr"; 

296 

297 

24024  298 
(* simprocs *) 
299 

300 
local 

301 

302 
val add_del = 

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

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

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

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

307 

308 
in 

309 

30528  310 
val simproc_att = 
311 
Scan.peek (fn context => 

24024  312 
add_del : (fn decl => 
313 
Scan.repeat1 (Args.named_attribute (decl o get_simproc context)) 

30528  314 
>> (Library.apply o map Morphism.form))); 
24024  315 

316 
end; 

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

317 

24024  318 

16014  319 
(* conversions *) 
320 

321 
local 

322 

323 
fun conv_mode x = 

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

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

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

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

328 

329 
in 

330 

30528  331 
val simplified = conv_mode  Attrib.thms >> 
332 
(fn (f, ths) => Thm.rule_attribute (fn context => 

27021  333 
f ((if null ths then I else MetaSimplifier.clear_ss) 
30528  334 
(local_simpset_of (Context.proof_of context)) addsimps ths))); 
16014  335 

336 
end; 

337 

338 

339 
(* setup attributes *) 

340 

26463  341 
val _ = Context.>> (Context.map_theory 
30528  342 
(Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del) 
343 
"declaration of Simplifier rewrite rule" #> 

344 
Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del) 

345 
"declaration of Simplifier congruence rule" #> 

346 
Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #> 

347 
Attrib.setup (Binding.name "simplified") simplified "simplified rule")); 

16014  348 

349 

350 

31300  351 
(** method syntax **) 
16014  352 

353 
val cong_modifiers = 

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

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

16014  357 

358 
val simp_modifiers = 

18728  359 
[Args.$$$ simpN  Args.colon >> K (I, simp_add), 
360 
Args.$$$ simpN  Args.add  Args.colon >> K (I, simp_add), 

361 
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

362 
Args.$$$ simpN  Args.$$$ onlyN  Args.colon 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

363 
>> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)] 
16014  364 
@ cong_modifiers; 
365 

366 
val simp_modifiers' = 

18728  367 
[Args.add  Args.colon >> K (I, simp_add), 
368 
Args.del  Args.colon >> K (I, simp_del), 

18688  369 
Args.$$$ onlyN  Args.colon 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

370 
>> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)] 
16014  371 
@ cong_modifiers; 
372 

31300  373 
val simp_options = 
374 
(Args.parens (Args.$$$ no_asmN) >> K simp_tac  

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

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

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

378 
Scan.succeed asm_full_simp_tac); 

16014  379 

31300  380 
fun simp_method more_mods meth = 
381 
Args.bang_facts  Scan.lift simp_options  

382 
Method.sections (more_mods @ simp_modifiers') >> 

383 
(fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts))); 

16014  384 

385 

386 

18708  387 
(** setup **) 
388 

31300  389 
fun method_setup more_mods = 
390 
Method.setup (Binding.name simpN) 

391 
(simp_method more_mods (fn ctxt => fn tac => fn facts => 

392 
HEADGOAL (Method.insert_tac facts THEN' 

393 
(CHANGED_PROP oo tac) (local_simpset_of ctxt)))) 

394 
"simplification" #> 

395 
Method.setup (Binding.name "simp_all") 

396 
(simp_method more_mods (fn ctxt => fn tac => fn facts => 

397 
ALLGOALS (Method.insert_tac facts) THEN 

398 
(CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt))) 

399 
"simplification (all goals)"; 

16014  400 

26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

401 
fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ => 
16014  402 
let 
403 
val trivialities = Drule.reflexive_thm :: trivs; 

404 

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

406 
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac; 

407 

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

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

410 
val safe_solver = mk_solver "easy safe" safe_solver_tac; 

411 

412 
fun mk_eq thm = 

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

26653  416 
fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm); 
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

417 
in 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

418 
empty_ss setsubgoaler asm_simp_tac 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

419 
setSSolver safe_solver 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

420 
setSolver unsafe_solver 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

421 
setmksimps mksimps 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

422 
end)); 
16014  423 

424 
end; 

425 

426 
structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier; 

427 
open BasicSimplifier; 