author  wenzelm 
Tue, 02 Sep 2008 14:10:19 +0200  
changeset 28074  90adbbf03187 
parent 27338  2cd6c60cc10b 
child 28738  677312de6608 
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 

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

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

14 
val simpset: unit > simpset 
16014  15 
val SIMPSET: (simpset > tactic) > tactic 
16 
val SIMPSET': (simpset > 'a > tactic) > 'a > tactic 

17 
val Addsimps: thm list > unit 

18 
val Delsimps: thm list > unit 

19 
val Addsimprocs: simproc list > unit 

20 
val Delsimprocs: simproc list > unit 

21 
val Addcongs: thm list > unit 

22 
val Delcongs: thm list > unit 

23 
val local_simpset_of: Proof.context > simpset 

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

24 
val generic_simp_tac: bool > bool * bool * bool > simpset > int > tactic 
16014  25 
val safe_asm_full_simp_tac: simpset > int > tactic 
26 
val simp_tac: simpset > int > tactic 

27 
val asm_simp_tac: simpset > int > tactic 

28 
val full_simp_tac: simpset > int > tactic 

29 
val asm_lr_simp_tac: simpset > int > tactic 

30 
val asm_full_simp_tac: simpset > int > tactic 

31 
val Simp_tac: int > tactic 

32 
val Asm_simp_tac: int > tactic 

33 
val Full_simp_tac: int > tactic 

34 
val Asm_lr_simp_tac: int > tactic 

35 
val Asm_full_simp_tac: int > tactic 

36 
val simplify: simpset > thm > thm 

37 
val asm_simplify: simpset > thm > thm 

38 
val full_simplify: simpset > thm > thm 

39 
val asm_lr_simplify: simpset > thm > thm 

40 
val asm_full_simplify: simpset > thm > thm 

41 
end; 

42 

43 
signature SIMPLIFIER = 

44 
sig 

45 
include BASIC_SIMPLIFIER 

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

48 
val inherit_context: simpset > simpset > simpset 
17898  49 
val the_context: simpset > Proof.context 
50 
val context: Proof.context > simpset > simpset 

51 
val theory_context: theory > simpset > simpset 

16458  52 
val simproc_i: theory > string > term list 
53 
> (theory > simpset > term > thm option) > simproc 

54 
val simproc: theory > string > string list 

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

23598  56 
val rewrite: simpset > conv 
57 
val asm_rewrite: simpset > conv 

58 
val full_rewrite: simpset > conv 

59 
val asm_lr_rewrite: simpset > conv 

60 
val asm_full_rewrite: simpset > conv 

22379  61 
val get_ss: Context.generic > simpset 
62 
val map_ss: (simpset > simpset) > Context.generic > Context.generic 

18728  63 
val attrib: (simpset * thm list > simpset) > attribute 
64 
val simp_add: attribute 

65 
val simp_del: attribute 

66 
val cong_add: attribute 

67 
val cong_del: attribute 

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

68 
val map_simpset: (simpset > simpset) > theory > theory 
24024  69 
val get_simproc: Context.generic > xstring > simproc 
22236  70 
val def_simproc: {name: string, lhss: string list, 
71 
proc: morphism > simpset > cterm > thm option, identifier: thm list} > 

22201  72 
local_theory > local_theory 
22236  73 
val def_simproc_i: {name: string, lhss: term list, 
74 
proc: morphism > simpset > cterm > thm option, identifier: thm list} > 

22201  75 
local_theory > local_theory 
18033  76 
val cong_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
77 
val simp_modifiers': (Args.T list > (Method.modifier * Args.T list)) list 

16014  78 
val simp_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
79 
val method_setup: (Args.T list > (Method.modifier * Args.T list)) list 

18708  80 
> theory > theory 
81 
val easy_setup: thm > thm list > theory > theory 

16014  82 
end; 
83 

84 
structure Simplifier: SIMPLIFIER = 

85 
struct 

86 

21708  87 
open MetaSimplifier; 
88 

89 

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

90 
(** simpset data **) 
16014  91 

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

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

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

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

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

97 
fun merge _ = merge_ss; 
22846  98 
); 
16014  99 

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

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

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

102 

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

103 

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

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

105 

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

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

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

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

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

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

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

112 

16014  113 

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

114 
(* global simpset *) 
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 map_simpset f = Context.theory_map (map_ss f); 
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset

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

118 
fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy)); 
26425
6561665c5cb1
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
24509
diff
changeset

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

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

121 
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

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

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

124 
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

125 
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

126 
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

127 
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

128 
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

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

131 

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

132 
(* local simpset *) 
16014  133 

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

134 
fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt)); 
16014  135 

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

22132  138 

16014  139 

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

140 

22201  141 
(** named simprocs **) 
142 

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

143 
fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name); 
22201  144 

22236  145 

22204  146 
(* data *) 
147 

22201  148 
structure Simprocs = GenericDataFun 
149 
( 

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

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

154 
handle Symtab.DUP dup => err_dup_simproc dup; 
22201  155 
); 
156 

22204  157 

158 
(* get simprocs *) 

159 

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

165 
(case Symtab.lookup tab name of 

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

169 

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

22204  172 

173 

174 
(* define simprocs *) 

22201  175 

176 
local 

177 

22236  178 
fun gen_simproc prep {name, lhss, proc, identifier} lthy = 
22201  179 
let 
22236  180 
val naming = LocalTheory.full_naming lthy; 
181 
val simproc = make_simproc 

182 
{name = LocalTheory.full_name lthy name, 

183 
lhss = 

184 
let 

185 
val lhss' = prep lthy lhss; 

186 
val ctxt' = lthy 

187 
> fold Variable.declare_term lhss' 

188 
> fold Variable.auto_fixes lhss'; 

189 
in Variable.export_terms ctxt' lthy lhss' end 

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

191 
proc = proc, 

192 
identifier = identifier} 

193 
> morph_simproc (LocalTheory.target_morphism lthy); 

22201  194 
in 
24024  195 
lthy > LocalTheory.declaration (fn phi => 
22201  196 
let 
28074  197 
val name' = Name.name_of (Morphism.name phi (Name.binding name)); 
22236  198 
val simproc' = morph_simproc phi simproc; 
22201  199 
in 
24024  200 
Simprocs.map (fn simprocs => 
23086  201 
NameSpace.extend_table naming [(name', simproc')] simprocs 
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23598
diff
changeset

202 
handle Symtab.DUP dup => err_dup_simproc dup) 
24024  203 
#> map_ss (fn ss => ss addsimprocs [simproc']) 
22201  204 
end) 
205 
end; 

206 

207 
in 

208 

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

209 
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

210 
val def_simproc_i = gen_simproc Syntax.check_terms; 
22201  211 

212 
end; 

213 

214 

215 

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

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

217 

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

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

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

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

221 
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

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

223 

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

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

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

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

227 
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

228 
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

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

231 

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

232 
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

233 
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

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

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

236 

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

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

238 

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

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

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

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

243 
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

244 
in rew mode prover ss thm end; 
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 
in 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

247 

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

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

249 
val simp_cterm = simp MetaSimplifier.rewrite_cterm; 
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 
end; 
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset

252 

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

253 

16806  254 
(* tactics *) 
255 

16014  256 
val simp_tac = generic_simp_tac false (false, false, false); 
257 
val asm_simp_tac = generic_simp_tac false (false, true, false); 

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

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

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

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

262 

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

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

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

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

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

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

269 

16806  270 

271 
(* conversions *) 

272 

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

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

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

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

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

277 
val asm_full_simplify = simp_thm (true, true, true); 
16014  278 

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

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

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

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

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

283 
val asm_full_rewrite = simp_cterm (true, true, true); 
16014  284 

285 

286 

287 
(** concrete syntax of attributes **) 

288 

289 
(* add / del *) 

290 

291 
val simpN = "simp"; 

292 
val congN = "cong"; 

293 
val addN = "add"; 

294 
val delN = "del"; 

295 
val onlyN = "only"; 

296 
val no_asmN = "no_asm"; 

297 
val no_asm_useN = "no_asm_use"; 

298 
val no_asm_simpN = "no_asm_simp"; 

299 
val asm_lrN = "asm_lr"; 

300 

301 

24024  302 
(* simprocs *) 
303 

304 
local 

305 

306 
val add_del = 

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

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

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

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

311 

312 
in 

313 

314 
val simproc_att = Attrib.syntax 

315 
(Scan.peek (fn context => 

316 
add_del : (fn decl => 

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

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

319 

320 
end; 

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

321 

24024  322 

16014  323 
(* conversions *) 
324 

325 
local 

326 

327 
fun conv_mode x = 

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

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

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

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

332 

333 
in 

334 

18688  335 
val simplified = 
27021  336 
Attrib.syntax (conv_mode  Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context => 
337 
f ((if null ths then I else MetaSimplifier.clear_ss) 

338 
(local_simpset_of (Context.proof_of context)) addsimps ths)))); 

16014  339 

340 
end; 

341 

342 

343 
(* setup attributes *) 

344 

26463  345 
val _ = Context.>> (Context.map_theory 
18708  346 
(Attrib.add_attributes 
24024  347 
[(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"), 
18728  348 
(congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"), 
24024  349 
("simproc", simproc_att, "declaration of simplification procedures"), 
26463  350 
("simplified", simplified, "simplified rule")])); 
16014  351 

352 

353 

354 
(** proof methods **) 

355 

356 
(* simplification *) 

357 

358 
val simp_options = 

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

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

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

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

363 
Scan.succeed asm_full_simp_tac); 

364 

365 
val cong_modifiers = 

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

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

16014  369 

370 
val simp_modifiers = 

18728  371 
[Args.$$$ simpN  Args.colon >> K (I, simp_add), 
372 
Args.$$$ simpN  Args.add  Args.colon >> K (I, simp_add), 

373 
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

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

375 
>> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)] 
16014  376 
@ cong_modifiers; 
377 

378 
val simp_modifiers' = 

18728  379 
[Args.add  Args.colon >> K (I, simp_add), 
380 
Args.del  Args.colon >> K (I, simp_del), 

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

382 
>> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)] 
16014  383 
@ cong_modifiers; 
384 

385 
fun simp_args more_mods = 

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

386 
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

387 
(more_mods @ simp_modifiers'); 
16014  388 

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

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

391 
(CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)); 
16014  392 

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

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

395 
((CHANGED_PROP) oo tac) (local_simpset_of ctxt))); 
16014  396 

397 

398 

18708  399 
(** setup **) 
400 

401 
fun method_setup more_mods = Method.add_methods 

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

404 

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

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

408 

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

410 
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac; 

411 

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

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

414 
val safe_solver = mk_solver "easy safe" safe_solver_tac; 

415 

416 
fun mk_eq thm = 

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

26653  420 
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

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

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

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

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

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

426 
end)); 
16014  427 

428 
end; 

429 

430 
structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier; 

431 
open BasicSimplifier; 