1(* Title: Pure/simplifier.ML 2 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 3 4Generic simplifier, suitable for most logics (see also 5raw_simplifier.ML for the actual meta-level rewriting engine). 6*) 7 8signature BASIC_SIMPLIFIER = 9sig 10 include BASIC_RAW_SIMPLIFIER 11 val simp_tac: Proof.context -> int -> tactic 12 val asm_simp_tac: Proof.context -> int -> tactic 13 val full_simp_tac: Proof.context -> int -> tactic 14 val asm_lr_simp_tac: Proof.context -> int -> tactic 15 val asm_full_simp_tac: Proof.context -> int -> tactic 16 val safe_simp_tac: Proof.context -> int -> tactic 17 val safe_asm_simp_tac: Proof.context -> int -> tactic 18 val safe_full_simp_tac: Proof.context -> int -> tactic 19 val safe_asm_lr_simp_tac: Proof.context -> int -> tactic 20 val safe_asm_full_simp_tac: Proof.context -> int -> tactic 21 val simplify: Proof.context -> thm -> thm 22 val asm_simplify: Proof.context -> thm -> thm 23 val full_simplify: Proof.context -> thm -> thm 24 val asm_lr_simplify: Proof.context -> thm -> thm 25 val asm_full_simplify: Proof.context -> thm -> thm 26end; 27 28signature SIMPLIFIER = 29sig 30 include BASIC_SIMPLIFIER 31 val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic 32 val attrib: (thm -> Proof.context -> Proof.context) -> attribute 33 val simp_add: attribute 34 val simp_del: attribute 35 val simp_flip: attribute 36 val cong_add: attribute 37 val cong_del: attribute 38 val check_simproc: Proof.context -> xstring * Position.T -> string 39 val the_simproc: Proof.context -> string -> simproc 40 type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option} 41 val make_simproc: Proof.context -> string -> term simproc_spec -> simproc 42 val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory 43 val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory 44 val pretty_simpset: bool -> Proof.context -> Pretty.T 45 val default_mk_sym: Proof.context -> thm -> thm option 46 val prems_of: Proof.context -> thm list 47 val add_simp: thm -> Proof.context -> Proof.context 48 val del_simp: thm -> Proof.context -> Proof.context 49 val init_simpset: thm list -> Proof.context -> Proof.context 50 val add_eqcong: thm -> Proof.context -> Proof.context 51 val del_eqcong: thm -> Proof.context -> Proof.context 52 val add_cong: thm -> Proof.context -> Proof.context 53 val del_cong: thm -> Proof.context -> Proof.context 54 val add_prems: thm list -> Proof.context -> Proof.context 55 val mksimps: Proof.context -> thm -> thm list 56 val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context 57 val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context 58 val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context 59 val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context 60 val set_term_ord: term ord -> Proof.context -> Proof.context 61 val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context 62 type trace_ops 63 val set_trace_ops: trace_ops -> theory -> theory 64 val rewrite: Proof.context -> conv 65 val asm_rewrite: Proof.context -> conv 66 val full_rewrite: Proof.context -> conv 67 val asm_lr_rewrite: Proof.context -> conv 68 val asm_full_rewrite: Proof.context -> conv 69 val cong_modifiers: Method.modifier parser list 70 val simp_modifiers': Method.modifier parser list 71 val simp_modifiers: Method.modifier parser list 72 val method_setup: Method.modifier parser list -> theory -> theory 73 val unsafe_solver_tac: Proof.context -> int -> tactic 74 val unsafe_solver: solver 75 val safe_solver_tac: Proof.context -> int -> tactic 76 val safe_solver: solver 77end; 78 79structure Simplifier: SIMPLIFIER = 80struct 81 82open Raw_Simplifier; 83 84 85(** declarations **) 86 87(* attributes *) 88 89fun attrib f = Thm.declaration_attribute (map_ss o f); 90 91val simp_add = attrib add_simp; 92val simp_del = attrib del_simp; 93val simp_flip = attrib flip_simp; 94val cong_add = attrib add_cong; 95val cong_del = attrib del_cong; 96 97 98(** named simprocs **) 99 100structure Simprocs = Generic_Data 101( 102 type T = simproc Name_Space.table; 103 val empty : T = Name_Space.empty_table "simproc"; 104 val extend = I; 105 fun merge data : T = Name_Space.merge_tables data; 106); 107 108 109(* get simprocs *) 110 111val get_simprocs = Simprocs.get o Context.Proof; 112 113fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1; 114val the_simproc = Name_Space.get o get_simprocs; 115 116val _ = Theory.setup 117 (ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close> 118 (Args.context -- Scan.lift Args.embedded_position 119 >> (fn (ctxt, name) => 120 "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name)))); 121 122 123(* define simprocs *) 124 125type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}; 126 127fun make_simproc ctxt name {lhss, proc} = 128 let 129 val ctxt' = fold Proof_Context.augment lhss ctxt; 130 val lhss' = Variable.export_terms ctxt' ctxt lhss; 131 in 132 cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc} 133 end; 134 135local 136 137fun def_simproc prep b {lhss, proc} lthy = 138 let 139 val simproc = 140 make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc}; 141 in 142 lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context => 143 let 144 val b' = Morphism.binding phi b; 145 val simproc' = transform_simproc phi simproc; 146 in 147 context 148 |> Simprocs.map (#2 o Name_Space.define context true (b', simproc')) 149 |> map_ss (fn ctxt => ctxt addsimprocs [simproc']) 150 end) 151 end; 152 153in 154 155val define_simproc = def_simproc Syntax.check_terms; 156val define_simproc_cmd = def_simproc Syntax.read_terms; 157 158end; 159 160 161 162(** pretty_simpset **) 163 164fun pretty_simpset verbose ctxt = 165 let 166 val pretty_term = Syntax.pretty_term ctxt; 167 val pretty_thm = Thm.pretty_thm ctxt; 168 val pretty_thm_item = Thm.pretty_thm_item ctxt; 169 170 fun pretty_simproc (name, lhss) = 171 Pretty.block 172 (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk :: 173 Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss)); 174 175 fun pretty_cong_name (const, name) = 176 pretty_term ((if const then Const else Free) (name, dummyT)); 177 fun pretty_cong (name, thm) = 178 Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm]; 179 180 val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = 181 dest_ss (simpset_of ctxt); 182 val simprocs = 183 Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs; 184 in 185 [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps), 186 Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs), 187 Pretty.big_list "congruences:" (map pretty_cong congs), 188 Pretty.strs ("loopers:" :: map quote loopers), 189 Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers), 190 Pretty.strs ("safe solvers:" :: map quote safe_solvers)] 191 |> Pretty.chunks 192 end; 193 194 195 196(** simplification tactics and rules **) 197 198fun solve_all_tac solvers ctxt = 199 let 200 val subgoal_tac = Raw_Simplifier.subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt); 201 val solve_tac = subgoal_tac THEN_ALL_NEW (K no_tac); 202 in DEPTH_SOLVE (solve_tac 1) end; 203 204(*NOTE: may instantiate unknowns that appear also in other subgoals*) 205fun generic_simp_tac safe mode ctxt = 206 let 207 val loop_tac = Raw_Simplifier.loop_tac ctxt; 208 val (unsafe_solvers, solvers) = Raw_Simplifier.solvers ctxt; 209 val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt) 210 (rev (if safe then solvers else unsafe_solvers))); 211 212 fun simp_loop_tac i = 213 Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN 214 (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); 215 in PREFER_GOAL (simp_loop_tac 1) end; 216 217local 218 219fun simp rew mode ctxt thm = 220 let 221 val (unsafe_solvers, _) = Raw_Simplifier.solvers ctxt; 222 val tacf = solve_all_tac (rev unsafe_solvers); 223 fun prover s th = Option.map #1 (Seq.pull (tacf s th)); 224 in rew mode prover ctxt thm end; 225 226in 227 228val simp_thm = simp Raw_Simplifier.rewrite_thm; 229val simp_cterm = simp Raw_Simplifier.rewrite_cterm; 230 231end; 232 233 234(* tactics *) 235 236val simp_tac = generic_simp_tac false (false, false, false); 237val asm_simp_tac = generic_simp_tac false (false, true, false); 238val full_simp_tac = generic_simp_tac false (true, false, false); 239val asm_lr_simp_tac = generic_simp_tac false (true, true, false); 240val asm_full_simp_tac = generic_simp_tac false (true, true, true); 241 242(*not totally safe: may instantiate unknowns that appear also in other subgoals*) 243val safe_simp_tac = generic_simp_tac true (false, false, false); 244val safe_asm_simp_tac = generic_simp_tac true (false, true, false); 245val safe_full_simp_tac = generic_simp_tac true (true, false, false); 246val safe_asm_lr_simp_tac = generic_simp_tac true (true, true, false); 247val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true); 248 249 250(* conversions *) 251 252val simplify = simp_thm (false, false, false); 253val asm_simplify = simp_thm (false, true, false); 254val full_simplify = simp_thm (true, false, false); 255val asm_lr_simplify = simp_thm (true, true, false); 256val asm_full_simplify = simp_thm (true, true, true); 257 258val rewrite = simp_cterm (false, false, false); 259val asm_rewrite = simp_cterm (false, true, false); 260val full_rewrite = simp_cterm (true, false, false); 261val asm_lr_rewrite = simp_cterm (true, true, false); 262val asm_full_rewrite = simp_cterm (true, true, true); 263 264 265 266(** concrete syntax of attributes **) 267 268(* add / del *) 269 270val simpN = "simp"; 271val flipN = "flip" 272val congN = "cong"; 273val onlyN = "only"; 274val no_asmN = "no_asm"; 275val no_asm_useN = "no_asm_use"; 276val no_asm_simpN = "no_asm_simp"; 277val asm_lrN = "asm_lr"; 278 279 280(* simprocs *) 281 282local 283 284val add_del = 285 (Args.del -- Args.colon >> K (op delsimprocs) || 286 Scan.option (Args.add -- Args.colon) >> K (op addsimprocs)) 287 >> (fn f => fn simproc => fn phi => Thm.declaration_attribute 288 (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc]))))); 289 290in 291 292val simproc_att = 293 (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) => 294 Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt)))) 295 >> (fn atts => Thm.declaration_attribute (fn th => 296 fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)); 297 298end; 299 300 301(* conversions *) 302 303local 304 305fun conv_mode x = 306 ((Args.parens (Args.$$$ no_asmN) >> K simplify || 307 Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify || 308 Args.parens (Args.$$$ no_asm_useN) >> K full_simplify || 309 Scan.succeed asm_full_simplify) |> Scan.lift) x; 310 311in 312 313val simplified = conv_mode -- Attrib.thms >> 314 (fn (f, ths) => Thm.rule_attribute ths (fn context => 315 f ((if null ths then I else Raw_Simplifier.clear_simpset) 316 (Context.proof_of context) addsimps ths))); 317 318end; 319 320 321(* setup attributes *) 322 323val _ = Theory.setup 324 (Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del) 325 "declaration of Simplifier rewrite rule" #> 326 Attrib.setup \<^binding>\<open>cong\<close> (Attrib.add_del cong_add cong_del) 327 "declaration of Simplifier congruence rule" #> 328 Attrib.setup \<^binding>\<open>simproc\<close> simproc_att 329 "declaration of simplification procedures" #> 330 Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule"); 331 332 333 334(** method syntax **) 335 336val cong_modifiers = 337 [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add \<^here>), 338 Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add \<^here>), 339 Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del \<^here>)]; 340 341val simp_modifiers = 342 [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>), 343 Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>), 344 Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>), 345 Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>), 346 Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> 347 K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}] 348 @ cong_modifiers; 349 350val simp_modifiers' = 351 [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>), 352 Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>), 353 Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>), 354 Args.$$$ onlyN -- Args.colon >> 355 K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}] 356 @ cong_modifiers; 357 358val 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 365fun simp_method more_mods meth = 366 Scan.lift simp_options --| 367 Method.sections (more_mods @ simp_modifiers') >> 368 (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts)); 369 370 371 372(** setup **) 373 374fun method_setup more_mods = 375 Method.setup \<^binding>\<open>simp\<close> 376 (simp_method more_mods (fn ctxt => fn tac => fn facts => 377 HEADGOAL (Method.insert_tac ctxt facts THEN' 378 (CHANGED_PROP oo tac) ctxt))) 379 "simplification" #> 380 Method.setup \<^binding>\<open>simp_all\<close> 381 (simp_method more_mods (fn ctxt => fn tac => fn facts => 382 ALLGOALS (Method.insert_tac ctxt facts) THEN 383 (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt)) 384 "simplification (all goals)"; 385 386fun unsafe_solver_tac ctxt = 387 FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt]; 388val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac; 389 390(*no premature instantiation of variables during simplification*) 391fun safe_solver_tac ctxt = 392 FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac]; 393val safe_solver = mk_solver "Pure safe" safe_solver_tac; 394 395val _ = 396 Theory.setup 397 (method_setup [] #> Context.theory_map (map_ss (fn ctxt => 398 empty_simpset ctxt 399 setSSolver safe_solver 400 setSolver unsafe_solver 401 |> set_subgoaler asm_simp_tac))); 402 403end; 404 405structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier; 406open Basic_Simplifier; 407