1(* Title: Pure/raw_simplifier.ML 2 Author: Tobias Nipkow and Stefan Berghofer, TU Muenchen 3 4Higher-order Simplification. 5*) 6 7infix 4 8 addsimps delsimps addsimprocs delsimprocs 9 setloop addloop delloop 10 setSSolver addSSolver setSolver addSolver; 11 12signature BASIC_RAW_SIMPLIFIER = 13sig 14 val simp_depth_limit: int Config.T 15 val simp_trace_depth_limit: int Config.T 16 val simp_debug: bool Config.T 17 val simp_trace: bool Config.T 18 type cong_name = bool * string 19 type rrule 20 val mk_rrules: Proof.context -> thm list -> rrule list 21 val eq_rrule: rrule * rrule -> bool 22 type proc 23 type solver 24 val mk_solver: string -> (Proof.context -> int -> tactic) -> solver 25 type simpset 26 val empty_ss: simpset 27 val merge_ss: simpset * simpset -> simpset 28 val dest_ss: simpset -> 29 {simps: (string * thm) list, 30 procs: (string * term list) list, 31 congs: (cong_name * thm) list, 32 weak_congs: cong_name list, 33 loopers: string list, 34 unsafe_solvers: string list, 35 safe_solvers: string list} 36 type simproc 37 val eq_simproc: simproc * simproc -> bool 38 val cert_simproc: theory -> string -> 39 {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc 40 val transform_simproc: morphism -> simproc -> simproc 41 val simpset_of: Proof.context -> simpset 42 val put_simpset: simpset -> Proof.context -> Proof.context 43 val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset 44 val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory 45 val empty_simpset: Proof.context -> Proof.context 46 val clear_simpset: Proof.context -> Proof.context 47 val addsimps: Proof.context * thm list -> Proof.context 48 val delsimps: Proof.context * thm list -> Proof.context 49 val addsimprocs: Proof.context * simproc list -> Proof.context 50 val delsimprocs: Proof.context * simproc list -> Proof.context 51 val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context 52 val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context 53 val delloop: Proof.context * string -> Proof.context 54 val setSSolver: Proof.context * solver -> Proof.context 55 val addSSolver: Proof.context * solver -> Proof.context 56 val setSolver: Proof.context * solver -> Proof.context 57 val addSolver: Proof.context * solver -> Proof.context 58 59 val rewrite_rule: Proof.context -> thm list -> thm -> thm 60 val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm 61 val rewrite_goals_tac: Proof.context -> thm list -> tactic 62 val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic 63 val prune_params_tac: Proof.context -> tactic 64 val fold_rule: Proof.context -> thm list -> thm -> thm 65 val fold_goals_tac: Proof.context -> thm list -> tactic 66 val norm_hhf: Proof.context -> thm -> thm 67 val norm_hhf_protect: Proof.context -> thm -> thm 68end; 69 70signature RAW_SIMPLIFIER = 71sig 72 include BASIC_RAW_SIMPLIFIER 73 exception SIMPLIFIER of string * thm list 74 type trace_ops 75 val set_trace_ops: trace_ops -> theory -> theory 76 val subgoal_tac: Proof.context -> int -> tactic 77 val loop_tac: Proof.context -> int -> tactic 78 val solvers: Proof.context -> solver list * solver list 79 val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic 80 val prems_of: Proof.context -> thm list 81 val add_simp: thm -> Proof.context -> Proof.context 82 val del_simp: thm -> Proof.context -> Proof.context 83 val flip_simp: thm -> Proof.context -> Proof.context 84 val init_simpset: thm list -> Proof.context -> Proof.context 85 val add_eqcong: thm -> Proof.context -> Proof.context 86 val del_eqcong: thm -> Proof.context -> Proof.context 87 val add_cong: thm -> Proof.context -> Proof.context 88 val del_cong: thm -> Proof.context -> Proof.context 89 val mksimps: Proof.context -> thm -> thm list 90 val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context 91 val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context 92 val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context 93 val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context 94 val set_term_ord: term ord -> Proof.context -> Proof.context 95 val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context 96 val solver: Proof.context -> solver -> int -> tactic 97 val default_mk_sym: Proof.context -> thm -> thm option 98 val add_prems: thm list -> Proof.context -> Proof.context 99 val set_reorient: (Proof.context -> term list -> term -> term -> bool) -> 100 Proof.context -> Proof.context 101 val set_solvers: solver list -> Proof.context -> Proof.context 102 val rewrite_cterm: bool * bool * bool -> 103 (Proof.context -> thm -> thm option) -> Proof.context -> conv 104 val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term 105 val rewrite_thm: bool * bool * bool -> 106 (Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm 107 val generic_rewrite_goal_tac: bool * bool * bool -> 108 (Proof.context -> tactic) -> Proof.context -> int -> tactic 109 val rewrite: Proof.context -> bool -> thm list -> conv 110end; 111 112structure Raw_Simplifier: RAW_SIMPLIFIER = 113struct 114 115(** datatype simpset **) 116 117(* congruence rules *) 118 119type cong_name = bool * string; 120 121fun cong_name (Const (a, _)) = SOME (true, a) 122 | cong_name (Free (a, _)) = SOME (false, a) 123 | cong_name _ = NONE; 124 125structure Congtab = Table(type key = cong_name val ord = prod_ord bool_ord fast_string_ord); 126 127 128(* rewrite rules *) 129 130type rrule = 131 {thm: thm, (*the rewrite rule*) 132 name: string, (*name of theorem from which rewrite rule was extracted*) 133 lhs: term, (*the left-hand side*) 134 elhs: cterm, (*the eta-contracted lhs*) 135 extra: bool, (*extra variables outside of elhs*) 136 fo: bool, (*use first-order matching*) 137 perm: bool}; (*the rewrite rule is permutative*) 138 139fun trim_context_rrule ({thm, name, lhs, elhs, extra, fo, perm}: rrule) = 140 {thm = Thm.trim_context thm, name = name, lhs = lhs, elhs = Thm.trim_context_cterm elhs, 141 extra = extra, fo = fo, perm = perm}; 142 143(* 144Remarks: 145 - elhs is used for matching, 146 lhs only for preservation of bound variable names; 147 - fo is set iff 148 either elhs is first-order (no Var is applied), 149 in which case fo-matching is complete, 150 or elhs is not a pattern, 151 in which case there is nothing better to do; 152*) 153 154fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) = 155 Thm.eq_thm_prop (thm1, thm2); 156 157(* FIXME: it seems that the conditions on extra variables are too liberal if 158prems are nonempty: does solving the prems really guarantee instantiation of 159all its Vars? Better: a dynamic check each time a rule is applied. 160*) 161fun rewrite_rule_extra_vars prems elhs erhs = 162 let 163 val elhss = elhs :: prems; 164 val tvars = fold Term.add_tvars elhss []; 165 val vars = fold Term.add_vars elhss []; 166 in 167 erhs |> Term.exists_type (Term.exists_subtype 168 (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse 169 erhs |> Term.exists_subterm 170 (fn Var v => not (member (op =) vars v) | _ => false) 171 end; 172 173fun rrule_extra_vars elhs thm = 174 rewrite_rule_extra_vars [] (Thm.term_of elhs) (Thm.full_prop_of thm); 175 176fun mk_rrule2 {thm, name, lhs, elhs, perm} = 177 let 178 val t = Thm.term_of elhs; 179 val fo = Pattern.first_order t orelse not (Pattern.pattern t); 180 val extra = rrule_extra_vars elhs thm; 181 in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end; 182 183(*simple test for looping rewrite rules and stupid orientations*) 184fun default_reorient ctxt prems lhs rhs = 185 rewrite_rule_extra_vars prems lhs rhs 186 orelse 187 is_Var (head_of lhs) 188 orelse 189(* turns t = x around, which causes a headache if x is a local variable - 190 usually it is very useful :-( 191 is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs)) 192 andalso not(exists_subterm is_Var lhs) 193 orelse 194*) 195 exists (fn t => Logic.occs (lhs, t)) (rhs :: prems) 196 orelse 197 null prems andalso Pattern.matches (Proof_Context.theory_of ctxt) (lhs, rhs) 198 (*the condition "null prems" is necessary because conditional rewrites 199 with extra variables in the conditions may terminate although 200 the rhs is an instance of the lhs; example: ?m < ?n \<Longrightarrow> f ?n \<equiv> f ?m *) 201 orelse 202 is_Const lhs andalso not (is_Const rhs); 203 204 205(* simplification procedures *) 206 207datatype proc = 208 Proc of 209 {name: string, 210 lhs: term, 211 proc: Proof.context -> cterm -> thm option, 212 stamp: stamp}; 213 214fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2; 215 216 217(* solvers *) 218 219datatype solver = 220 Solver of 221 {name: string, 222 solver: Proof.context -> int -> tactic, 223 id: stamp}; 224 225fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()}; 226 227fun solver_name (Solver {name, ...}) = name; 228fun solver ctxt (Solver {solver = tac, ...}) = tac ctxt; 229fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2); 230 231 232(* simplification sets *) 233 234(*A simpset contains data required during conversion: 235 rules: discrimination net of rewrite rules; 236 prems: current premises; 237 depth: simp_depth and exceeded flag; 238 congs: association list of congruence rules and 239 a list of `weak' congruence constants. 240 A congruence is `weak' if it avoids normalization of some argument. 241 procs: discrimination net of simplification procedures 242 (functions that prove rewrite rules on the fly); 243 mk_rews: 244 mk: turn simplification thms into rewrite rules; 245 mk_cong: prepare congruence rules; 246 mk_sym: turn \<equiv> around; 247 mk_eq_True: turn P into P \<equiv> True; 248 term_ord: for ordered rewriting;*) 249 250datatype simpset = 251 Simpset of 252 {rules: rrule Net.net, 253 prems: thm list, 254 depth: int * bool Unsynchronized.ref} * 255 {congs: thm Congtab.table * cong_name list, 256 procs: proc Net.net, 257 mk_rews: 258 {mk: Proof.context -> thm -> thm list, 259 mk_cong: Proof.context -> thm -> thm, 260 mk_sym: Proof.context -> thm -> thm option, 261 mk_eq_True: Proof.context -> thm -> thm option, 262 reorient: Proof.context -> term list -> term -> term -> bool}, 263 term_ord: term ord, 264 subgoal_tac: Proof.context -> int -> tactic, 265 loop_tacs: (string * (Proof.context -> int -> tactic)) list, 266 solvers: solver list * solver list}; 267 268fun internal_ss (Simpset (_, ss2)) = ss2; 269 270fun make_ss1 (rules, prems, depth) = {rules = rules, prems = prems, depth = depth}; 271 272fun map_ss1 f {rules, prems, depth} = make_ss1 (f (rules, prems, depth)); 273 274fun make_ss2 (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) = 275 {congs = congs, procs = procs, mk_rews = mk_rews, term_ord = term_ord, 276 subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers}; 277 278fun map_ss2 f {congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers} = 279 make_ss2 (f (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers)); 280 281fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); 282 283fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = 284 {simps = Net.entries rules 285 |> map (fn {name, thm, ...} => (name, thm)), 286 procs = Net.entries procs 287 |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp)) 288 |> partition_eq (eq_snd op =) 289 |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), 290 congs = congs |> fst |> Congtab.dest, 291 weak_congs = congs |> snd, 292 loopers = map fst loop_tacs, 293 unsafe_solvers = map solver_name (#1 solvers), 294 safe_solvers = map solver_name (#2 solvers)}; 295 296 297(* empty *) 298 299fun init_ss depth mk_rews term_ord subgoal_tac solvers = 300 make_simpset ((Net.empty, [], depth), 301 ((Congtab.empty, []), Net.empty, mk_rews, term_ord, subgoal_tac, [], solvers)); 302 303fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm); 304 305val empty_ss = 306 init_ss (0, Unsynchronized.ref false) 307 {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], 308 mk_cong = K I, 309 mk_sym = default_mk_sym, 310 mk_eq_True = K (K NONE), 311 reorient = default_reorient} 312 Term_Ord.term_ord (K (K no_tac)) ([], []); 313 314 315(* merge *) (*NOTE: ignores some fields of 2nd simpset*) 316 317fun merge_ss (ss1, ss2) = 318 if pointer_eq (ss1, ss2) then ss1 319 else 320 let 321 val Simpset ({rules = rules1, prems = prems1, depth = depth1}, 322 {congs = (congs1, weak1), procs = procs1, mk_rews, term_ord, subgoal_tac, 323 loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; 324 val Simpset ({rules = rules2, prems = prems2, depth = depth2}, 325 {congs = (congs2, weak2), procs = procs2, mk_rews = _, term_ord = _, subgoal_tac = _, 326 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; 327 328 val rules' = Net.merge eq_rrule (rules1, rules2); 329 val prems' = Thm.merge_thms (prems1, prems2); 330 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; 331 val congs' = Congtab.merge (K true) (congs1, congs2); 332 val weak' = merge (op =) (weak1, weak2); 333 val procs' = Net.merge eq_proc (procs1, procs2); 334 val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); 335 val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2); 336 val solvers' = merge eq_solver (solvers1, solvers2); 337 in 338 make_simpset ((rules', prems', depth'), ((congs', weak'), procs', 339 mk_rews, term_ord, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) 340 end; 341 342 343 344(** context data **) 345 346structure Simpset = Generic_Data 347( 348 type T = simpset; 349 val empty = empty_ss; 350 val extend = I; 351 val merge = merge_ss; 352); 353 354val simpset_of = Simpset.get o Context.Proof; 355 356fun map_simpset f = Context.proof_map (Simpset.map f); 357fun map_simpset1 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (map_ss1 f ss1, ss2)); 358fun map_simpset2 f = map_simpset (fn Simpset (ss1, ss2) => Simpset (ss1, map_ss2 f ss2)); 359 360fun put_simpset ss = map_simpset (K ss); 361 362fun simpset_map ctxt f ss = ctxt |> put_simpset ss |> f |> simpset_of; 363 364val empty_simpset = put_simpset empty_ss; 365 366fun map_theory_simpset f thy = 367 let 368 val ctxt' = f (Proof_Context.init_global thy); 369 val thy' = Proof_Context.theory_of ctxt'; 370 in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end; 371 372fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f; 373 374val clear_simpset = 375 map_simpset (fn Simpset ({depth, ...}, {mk_rews, term_ord, subgoal_tac, solvers, ...}) => 376 init_ss depth mk_rews term_ord subgoal_tac solvers); 377 378 379(* accessors for tactis *) 380 381fun subgoal_tac ctxt = (#subgoal_tac o internal_ss o simpset_of) ctxt ctxt; 382 383fun loop_tac ctxt = 384 FIRST' (map (fn (_, tac) => tac ctxt) (rev ((#loop_tacs o internal_ss o simpset_of) ctxt))); 385 386val solvers = #solvers o internal_ss o simpset_of 387 388 389(* simp depth *) 390 391(* 392The simp_depth_limit is meant to abort infinite recursion of the simplifier 393early but should not terminate "normal" executions. 394As of 2017, 25 would suffice; 40 builds in a safety margin. 395*) 396 397val simp_depth_limit = Config.declare_int ("simp_depth_limit", \<^here>) (K 40); 398val simp_trace_depth_limit = Config.declare_int ("simp_trace_depth_limit", \<^here>) (K 1); 399 400fun inc_simp_depth ctxt = 401 ctxt |> map_simpset1 (fn (rules, prems, (depth, exceeded)) => 402 (rules, prems, 403 (depth + 1, 404 if depth = Config.get ctxt simp_trace_depth_limit 405 then Unsynchronized.ref false else exceeded))); 406 407fun simp_depth ctxt = 408 let val Simpset ({depth = (depth, _), ...}, _) = simpset_of ctxt 409 in depth end; 410 411 412(* diagnostics *) 413 414exception SIMPLIFIER of string * thm list; 415 416val simp_debug = Config.declare_bool ("simp_debug", \<^here>) (K false); 417val simp_trace = Config.declare_bool ("simp_trace", \<^here>) (K false); 418 419fun cond_warning ctxt msg = 420 if Context_Position.is_really_visible ctxt then warning (msg ()) else (); 421 422fun cond_tracing' ctxt flag msg = 423 if Config.get ctxt flag then 424 let 425 val Simpset ({depth = (depth, exceeded), ...}, _) = simpset_of ctxt; 426 val depth_limit = Config.get ctxt simp_trace_depth_limit; 427 in 428 if depth > depth_limit then 429 if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true) 430 else (tracing (enclose "[" "]" (string_of_int depth) ^ msg ()); exceeded := false) 431 end 432 else (); 433 434fun cond_tracing ctxt = cond_tracing' ctxt simp_trace; 435 436fun print_term ctxt s t = 437 s ^ "\n" ^ Syntax.string_of_term ctxt t; 438 439fun print_thm ctxt s (name, th) = 440 print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th); 441 442 443 444(** simpset operations **) 445 446(* prems *) 447 448fun prems_of ctxt = 449 let val Simpset ({prems, ...}, _) = simpset_of ctxt in prems end; 450 451fun add_prems ths = 452 map_simpset1 (fn (rules, prems, depth) => (rules, ths @ prems, depth)); 453 454 455(* maintain simp rules *) 456 457fun del_rrule loud (rrule as {thm, elhs, ...}) ctxt = 458 ctxt |> map_simpset1 (fn (rules, prems, depth) => 459 (Net.delete_term eq_rrule (Thm.term_of elhs, rrule) rules, prems, depth)) 460 handle Net.DELETE => 461 (if not loud then () 462 else cond_warning ctxt 463 (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); 464 ctxt); 465 466fun insert_rrule (rrule as {thm, name, ...}) ctxt = 467 (cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm)); 468 ctxt |> map_simpset1 (fn (rules, prems, depth) => 469 let 470 val rrule2 as {elhs, ...} = mk_rrule2 rrule; 471 val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule2) rules; 472 in (rules', prems, depth) end) 473 handle Net.INSERT => 474 (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm)); 475 ctxt)); 476 477local 478 479fun vperm (Var _, Var _) = true 480 | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) 481 | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) 482 | vperm (t, u) = (t = u); 483 484fun var_perm (t, u) = 485 vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []); 486 487in 488 489fun decomp_simp thm = 490 let 491 val prop = Thm.prop_of thm; 492 val prems = Logic.strip_imp_prems prop; 493 val concl = Drule.strip_imp_concl (Thm.cprop_of thm); 494 val (lhs, rhs) = Thm.dest_equals concl handle TERM _ => 495 raise SIMPLIFIER ("Rewrite rule not a meta-equality", [thm]); 496 val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs)); 497 val erhs = Envir.eta_contract (Thm.term_of rhs); 498 val perm = 499 var_perm (Thm.term_of elhs, erhs) andalso 500 not (Thm.term_of elhs aconv erhs) andalso 501 not (is_Var (Thm.term_of elhs)); 502 in (prems, Thm.term_of lhs, elhs, Thm.term_of rhs, perm) end; 503 504end; 505 506fun decomp_simp' thm = 507 let val (_, lhs, _, rhs, _) = decomp_simp thm in 508 if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", [thm]) 509 else (lhs, rhs) 510 end; 511 512fun mk_eq_True ctxt (thm, name) = 513 let val Simpset (_, {mk_rews = {mk_eq_True, ...}, ...}) = simpset_of ctxt in 514 (case mk_eq_True ctxt thm of 515 NONE => [] 516 | SOME eq_True => 517 let val (_, lhs, elhs, _, _) = decomp_simp eq_True; 518 in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end) 519 end; 520 521(*create the rewrite rule and possibly also the eq_True variant, 522 in case there are extra vars on the rhs*) 523fun rrule_eq_True ctxt thm name lhs elhs rhs thm2 = 524 let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in 525 if rewrite_rule_extra_vars [] lhs rhs then 526 mk_eq_True ctxt (thm2, name) @ [rrule] 527 else [rrule] 528 end; 529 530fun mk_rrule ctxt (thm, name) = 531 let val (prems, lhs, elhs, rhs, perm) = decomp_simp thm in 532 if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] 533 else 534 (*weak test for loops*) 535 if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (Thm.term_of elhs) 536 then mk_eq_True ctxt (thm, name) 537 else rrule_eq_True ctxt thm name lhs elhs rhs thm 538 end |> map (fn {thm, name, lhs, elhs, perm} => 539 {thm = Thm.trim_context thm, name = name, lhs = lhs, 540 elhs = Thm.trim_context_cterm elhs, perm = perm}); 541 542fun orient_rrule ctxt (thm, name) = 543 let 544 val (prems, lhs, elhs, rhs, perm) = decomp_simp thm; 545 val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = simpset_of ctxt; 546 in 547 if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] 548 else if reorient ctxt prems lhs rhs then 549 if reorient ctxt prems rhs lhs 550 then mk_eq_True ctxt (thm, name) 551 else 552 (case mk_sym ctxt thm of 553 NONE => [] 554 | SOME thm' => 555 let val (_, lhs', elhs', rhs', _) = decomp_simp thm' 556 in rrule_eq_True ctxt thm' name lhs' elhs' rhs' thm end) 557 else rrule_eq_True ctxt thm name lhs elhs rhs thm 558 end; 559 560fun extract_rews ctxt sym thms = 561 let 562 val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt; 563 val mk = 564 if sym then fn ctxt => fn th => (mk ctxt th) RL [Drule.symmetric_thm] 565 else mk 566 in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms 567 end; 568 569fun extract_safe_rrules ctxt thm = 570 maps (orient_rrule ctxt) (extract_rews ctxt false [thm]); 571 572fun mk_rrules ctxt thms = 573 let 574 val rews = extract_rews ctxt false thms 575 val raw_rrules = flat (map (mk_rrule ctxt) rews) 576 in map mk_rrule2 raw_rrules end 577 578 579(* add/del rules explicitly *) 580 581local 582 583fun comb_simps ctxt comb mk_rrule sym thms = 584 let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms); 585 in fold (fold comb o mk_rrule) rews ctxt end; 586 587(* 588This code checks if the symetric version of a rule is already in the simpset. 589However, the variable names in the two versions of the rule may differ. 590Thus the current test modulo eq_rrule is too weak to be useful 591and needs to be refined. 592 593fun present ctxt rules (rrule as {thm, elhs, ...}) = 594 (Net.insert_term eq_rrule (Thm.term_of elhs, trim_context_rrule rrule) rules; 595 false) 596 handle Net.INSERT => 597 (cond_warning ctxt 598 (fn () => print_thm ctxt "Symmetric rewrite rule already in simpset:" ("", thm)); 599 true); 600 601fun sym_present ctxt thms = 602 let 603 val rews = extract_rews ctxt true (map (Thm.transfer' ctxt) thms); 604 val rrules = map mk_rrule2 (flat(map (mk_rrule ctxt) rews)) 605 val Simpset({rules, ...},_) = simpset_of ctxt 606 in exists (present ctxt rules) rrules end 607*) 608in 609 610fun ctxt addsimps thms = 611 comb_simps ctxt insert_rrule (mk_rrule ctxt) false thms; 612 613fun addsymsimps ctxt thms = 614 comb_simps ctxt insert_rrule (mk_rrule ctxt) true thms; 615 616fun ctxt delsimps thms = 617 comb_simps ctxt (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms; 618 619fun delsimps_quiet ctxt thms = 620 comb_simps ctxt (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms; 621 622fun add_simp thm ctxt = ctxt addsimps [thm]; 623(* 624with check for presence of symmetric version: 625 if sym_present ctxt [thm] 626 then (cond_warning ctxt (fn () => print_thm ctxt "Ignoring rewrite rule:" ("", thm)); ctxt) 627 else ctxt addsimps [thm]; 628*) 629fun del_simp thm ctxt = ctxt delsimps [thm]; 630fun flip_simp thm ctxt = addsymsimps (delsimps_quiet ctxt [thm]) [thm]; 631 632end; 633 634fun init_simpset thms ctxt = ctxt 635 |> Context_Position.set_visible false 636 |> empty_simpset 637 |> fold add_simp thms 638 |> Context_Position.restore_visible ctxt; 639 640 641(* congs *) 642 643local 644 645fun is_full_cong_prems [] [] = true 646 | is_full_cong_prems [] _ = false 647 | is_full_cong_prems (p :: prems) varpairs = 648 (case Logic.strip_assums_concl p of 649 Const ("Pure.eq", _) $ lhs $ rhs => 650 let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in 651 is_Var x andalso forall is_Bound xs andalso 652 not (has_duplicates (op =) xs) andalso xs = ys andalso 653 member (op =) varpairs (x, y) andalso 654 is_full_cong_prems prems (remove (op =) (x, y) varpairs) 655 end 656 | _ => false); 657 658fun is_full_cong thm = 659 let 660 val prems = Thm.prems_of thm and concl = Thm.concl_of thm; 661 val (lhs, rhs) = Logic.dest_equals concl; 662 val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs; 663 in 664 f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso 665 is_full_cong_prems prems (xs ~~ ys) 666 end; 667 668fun mk_cong ctxt = 669 let val Simpset (_, {mk_rews = {mk_cong = f, ...}, ...}) = simpset_of ctxt 670 in f ctxt end; 671 672in 673 674fun add_eqcong thm ctxt = ctxt |> map_simpset2 675 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => 676 let 677 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) 678 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]); 679 (*val lhs = Envir.eta_contract lhs;*) 680 val a = the (cong_name (head_of lhs)) handle Option.Option => 681 raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]); 682 val (xs, weak) = congs; 683 val xs' = Congtab.update (a, Thm.trim_context thm) xs; 684 val weak' = if is_full_cong thm then weak else a :: weak; 685 in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end); 686 687fun del_eqcong thm ctxt = ctxt |> map_simpset2 688 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => 689 let 690 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) 691 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]); 692 (*val lhs = Envir.eta_contract lhs;*) 693 val a = the (cong_name (head_of lhs)) handle Option.Option => 694 raise SIMPLIFIER ("Congruence must start with a constant", [thm]); 695 val (xs, _) = congs; 696 val xs' = Congtab.delete_safe a xs; 697 val weak' = Congtab.fold (fn (a, th) => if is_full_cong th then I else insert (op =) a) xs' []; 698 in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end); 699 700fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt; 701fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt; 702 703end; 704 705 706(* simprocs *) 707 708datatype simproc = 709 Simproc of 710 {name: string, 711 lhss: term list, 712 proc: morphism -> Proof.context -> cterm -> thm option, 713 stamp: stamp}; 714 715fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2; 716 717fun cert_simproc thy name {lhss, proc} = 718 Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()}; 719 720fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) = 721 Simproc 722 {name = name, 723 lhss = map (Morphism.term phi) lhss, 724 proc = Morphism.transform phi proc, 725 stamp = stamp}; 726 727local 728 729fun add_proc (proc as Proc {name, lhs, ...}) ctxt = 730 (cond_tracing ctxt (fn () => 731 print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs); 732 ctxt |> map_simpset2 733 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => 734 (congs, Net.insert_term eq_proc (lhs, proc) procs, 735 mk_rews, term_ord, subgoal_tac, loop_tacs, solvers)) 736 handle Net.INSERT => 737 (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name); 738 ctxt)); 739 740fun del_proc (proc as Proc {name, lhs, ...}) ctxt = 741 ctxt |> map_simpset2 742 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => 743 (congs, Net.delete_term eq_proc (lhs, proc) procs, 744 mk_rews, term_ord, subgoal_tac, loop_tacs, solvers)) 745 handle Net.DELETE => 746 (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset"); 747 ctxt); 748 749fun prep_procs (Simproc {name, lhss, proc, stamp}) = 750 lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp}); 751 752in 753 754fun ctxt addsimprocs ps = fold (fold add_proc o prep_procs) ps ctxt; 755fun ctxt delsimprocs ps = fold (fold del_proc o prep_procs) ps ctxt; 756 757end; 758 759 760(* mk_rews *) 761 762local 763 764fun map_mk_rews f = 765 map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => 766 let 767 val {mk, mk_cong, mk_sym, mk_eq_True, reorient} = mk_rews; 768 val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = 769 f (mk, mk_cong, mk_sym, mk_eq_True, reorient); 770 val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', 771 reorient = reorient'}; 772 in (congs, procs, mk_rews', term_ord, subgoal_tac, loop_tacs, solvers) end); 773 774in 775 776fun mksimps ctxt = 777 let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt 778 in mk ctxt end; 779 780fun set_mksimps mk = map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => 781 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); 782 783fun set_mkcong mk_cong = map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => 784 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); 785 786fun set_mksym mk_sym = map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) => 787 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); 788 789fun set_mkeqTrue mk_eq_True = map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) => 790 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); 791 792fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) => 793 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); 794 795end; 796 797 798(* term_ord *) 799 800fun set_term_ord term_ord = 801 map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) => 802 (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers)); 803 804 805(* tactics *) 806 807fun set_subgoaler subgoal_tac = 808 map_simpset2 (fn (congs, procs, mk_rews, term_ord, _, loop_tacs, solvers) => 809 (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers)); 810 811fun ctxt setloop tac = ctxt |> 812 map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) => 813 (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers)); 814 815fun ctxt addloop (name, tac) = ctxt |> 816 map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => 817 (congs, procs, mk_rews, term_ord, subgoal_tac, 818 AList.update (op =) (name, tac) loop_tacs, solvers)); 819 820fun ctxt delloop name = ctxt |> 821 map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => 822 (congs, procs, mk_rews, term_ord, subgoal_tac, 823 (if AList.defined (op =) loop_tacs name then () 824 else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name); 825 AList.delete (op =) name loop_tacs), solvers)); 826 827fun ctxt setSSolver solver = ctxt |> map_simpset2 828 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) => 829 (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); 830 831fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord, 832 subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord, 833 subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers))); 834 835fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord, 836 subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, term_ord, 837 subgoal_tac, loop_tacs, ([solver], solvers))); 838 839fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord, 840 subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord, 841 subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers))); 842 843fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, term_ord, 844 subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, term_ord, 845 subgoal_tac, loop_tacs, (solvers, solvers))); 846 847 848(* trace operations *) 849 850type trace_ops = 851 {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context, 852 trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} -> 853 Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option}; 854 855structure Trace_Ops = Theory_Data 856( 857 type T = trace_ops; 858 val empty: T = 859 {trace_invoke = fn _ => fn ctxt => ctxt, 860 trace_apply = fn _ => fn ctxt => fn cont => cont ctxt}; 861 val extend = I; 862 fun merge (trace_ops, _) = trace_ops; 863); 864 865val set_trace_ops = Trace_Ops.put; 866 867val trace_ops = Trace_Ops.get o Proof_Context.theory_of; 868fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt; 869fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt; 870 871 872 873(** rewriting **) 874 875(* 876 Uses conversions, see: 877 L C Paulson, A higher-order implementation of rewriting, 878 Science of Computer Programming 3 (1983), pages 119-149. 879*) 880 881fun check_conv ctxt msg thm thm' = 882 let 883 val thm'' = Thm.transitive thm thm' handle THM _ => 884 let 885 val nthm' = 886 Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm' 887 in Thm.transitive thm nthm' handle THM _ => 888 let 889 val nthm = 890 Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm)) 891 in Thm.transitive nthm nthm' end 892 end 893 val _ = 894 if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm')) 895 else (); 896 in SOME thm'' end 897 handle THM _ => 898 let 899 val _ $ _ $ prop0 = Thm.prop_of thm; 900 val _ = 901 cond_tracing ctxt (fn () => 902 print_thm ctxt "Proved wrong theorem (bad subgoaler?)" ("", thm') ^ "\n" ^ 903 print_term ctxt "Should have proved:" prop0); 904 in NONE end; 905 906 907(* mk_procrule *) 908 909fun mk_procrule ctxt thm = 910 let 911 val (prems, lhs, elhs, rhs, _) = decomp_simp thm 912 val thm' = Thm.close_derivation \<^here> thm; 913 in 914 if rewrite_rule_extra_vars prems lhs rhs 915 then (cond_warning ctxt (fn () => print_thm ctxt "Extra vars on rhs:" ("", thm)); []) 916 else [mk_rrule2 {thm = thm', name = "", lhs = lhs, elhs = elhs, perm = false}] 917 end; 918 919 920(* rewritec: conversion to apply the meta simpset to a term *) 921 922(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already 923 normalized terms by carrying around the rhs of the rewrite rule just 924 applied. This is called the `skeleton'. It is decomposed in parallel 925 with the term. Once a Var is encountered, the corresponding term is 926 already in normal form. 927 skel0 is a dummy skeleton that is to enforce complete normalization.*) 928 929val skel0 = Bound 0; 930 931(*Use rhs as skeleton only if the lhs does not contain unnormalized bits. 932 The latter may happen iff there are weak congruence rules for constants 933 in the lhs.*) 934 935fun uncond_skel ((_, weak), (lhs, rhs)) = 936 if null weak then rhs (*optimization*) 937 else if exists_subterm 938 (fn Const (a, _) => member (op =) weak (true, a) 939 | Free (a, _) => member (op =) weak (false, a) 940 | _ => false) lhs then skel0 941 else rhs; 942 943(*Behaves like unconditional rule if rhs does not contain vars not in the lhs. 944 Otherwise those vars may become instantiated with unnormalized terms 945 while the premises are solved.*) 946 947fun cond_skel (args as (_, (lhs, rhs))) = 948 if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args 949 else skel0; 950 951(* 952 Rewriting -- we try in order: 953 (1) beta reduction 954 (2) unconditional rewrite rules 955 (3) conditional rewrite rules 956 (4) simplification procedures 957 958 IMPORTANT: rewrite rules must not introduce new Vars or TVars! 959*) 960 961fun rewritec (prover, maxt) ctxt t = 962 let 963 val thy = Proof_Context.theory_of ctxt; 964 val Simpset ({rules, ...}, {congs, procs, term_ord, ...}) = simpset_of ctxt; 965 val eta_thm = Thm.eta_conversion t; 966 val eta_t' = Thm.rhs_of eta_thm; 967 val eta_t = Thm.term_of eta_t'; 968 fun rew rrule = 969 let 970 val {thm = thm0, name, lhs, elhs = elhs0, extra, fo, perm} = rrule; 971 val thm = Thm.transfer thy thm0; 972 val elhs = Thm.transfer_cterm thy elhs0; 973 val prop = Thm.prop_of thm; 974 val (rthm, elhs') = 975 if maxt = ~1 orelse not extra then (thm, elhs) 976 else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); 977 978 val insts = 979 if fo then Thm.first_order_match (elhs', eta_t') 980 else Thm.match (elhs', eta_t'); 981 val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); 982 val prop' = Thm.prop_of thm'; 983 val unconditional = (Logic.count_prems prop' = 0); 984 val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop'); 985 val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule}; 986 in 987 if perm andalso is_greater_equal (term_ord (rhs', lhs')) 988 then 989 (cond_tracing ctxt (fn () => 990 print_thm ctxt "Cannot apply permutative rewrite rule" (name, thm) ^ "\n" ^ 991 print_thm ctxt "Term does not become smaller:" ("", thm')); 992 NONE) 993 else 994 (cond_tracing ctxt (fn () => 995 print_thm ctxt "Applying instance of rewrite rule" (name, thm)); 996 if unconditional 997 then 998 (cond_tracing ctxt (fn () => print_thm ctxt "Rewriting:" ("", thm')); 999 trace_apply trace_args ctxt (fn ctxt' => 1000 let 1001 val lr = Logic.dest_equals prop; 1002 val SOME thm'' = check_conv ctxt' false eta_thm thm'; 1003 in SOME (thm'', uncond_skel (congs, lr)) end)) 1004 else 1005 (cond_tracing ctxt (fn () => print_thm ctxt "Trying to rewrite:" ("", thm')); 1006 if simp_depth ctxt > Config.get ctxt simp_depth_limit 1007 then (cond_tracing ctxt (fn () => "simp_depth_limit exceeded - giving up"); NONE) 1008 else 1009 trace_apply trace_args ctxt (fn ctxt' => 1010 (case prover ctxt' thm' of 1011 NONE => (cond_tracing ctxt' (fn () => print_thm ctxt' "FAILED" ("", thm')); NONE) 1012 | SOME thm2 => 1013 (case check_conv ctxt' true eta_thm thm2 of 1014 NONE => NONE 1015 | SOME thm2' => 1016 let 1017 val concl = Logic.strip_imp_concl prop; 1018 val lr = Logic.dest_equals concl; 1019 in SOME (thm2', cond_skel (congs, lr)) end))))) 1020 end; 1021 1022 fun rews [] = NONE 1023 | rews (rrule :: rrules) = 1024 let val opt = rew rrule handle Pattern.MATCH => NONE 1025 in (case opt of NONE => rews rrules | some => some) end; 1026 1027 fun sort_rrules rrs = 1028 let 1029 fun is_simple ({thm, ...}: rrule) = 1030 (case Thm.prop_of thm of 1031 Const ("Pure.eq", _) $ _ $ _ => true 1032 | _ => false); 1033 fun sort [] (re1, re2) = re1 @ re2 1034 | sort (rr :: rrs) (re1, re2) = 1035 if is_simple rr 1036 then sort rrs (rr :: re1, re2) 1037 else sort rrs (re1, rr :: re2); 1038 in sort rrs ([], []) end; 1039 1040 fun proc_rews [] = NONE 1041 | proc_rews (Proc {name, proc, lhs, ...} :: ps) = 1042 if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then 1043 (cond_tracing' ctxt simp_debug (fn () => 1044 print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t); 1045 (case proc ctxt eta_t' of 1046 NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps) 1047 | SOME raw_thm => 1048 (cond_tracing ctxt (fn () => 1049 print_thm ctxt ("Procedure " ^ quote name ^ " produced rewrite rule:") 1050 ("", raw_thm)); 1051 (case rews (mk_procrule ctxt raw_thm) of 1052 NONE => 1053 (cond_tracing ctxt (fn () => 1054 print_term ctxt ("IGNORED result of simproc " ^ quote name ^ 1055 " -- does not match") (Thm.term_of t)); 1056 proc_rews ps) 1057 | some => some)))) 1058 else proc_rews ps; 1059 in 1060 (case eta_t of 1061 Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0) 1062 | _ => 1063 (case rews (sort_rrules (Net.match_term rules eta_t)) of 1064 NONE => proc_rews (Net.match_term procs eta_t) 1065 | some => some)) 1066 end; 1067 1068 1069(* conversion to apply a congruence rule to a term *) 1070 1071fun congc prover ctxt maxt cong t = 1072 let 1073 val rthm = Thm.incr_indexes (maxt + 1) cong; 1074 val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of rthm))); 1075 val insts = Thm.match (rlhs, t) 1076 (* Thm.match can raise Pattern.MATCH; 1077 is handled when congc is called *) 1078 val thm' = 1079 Thm.instantiate insts (Thm.rename_boundvars (Thm.term_of rlhs) (Thm.term_of t) rthm); 1080 val _ = 1081 cond_tracing ctxt (fn () => print_thm ctxt "Applying congruence rule:" ("", thm')); 1082 fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm ctxt msg ("", thm)); NONE); 1083 in 1084 (case prover thm' of 1085 NONE => err ("Congruence proof failed. Could not prove", thm') 1086 | SOME thm2 => 1087 (case check_conv ctxt true (Drule.beta_eta_conversion t) thm2 of 1088 NONE => err ("Congruence proof failed. Should not have proved", thm2) 1089 | SOME thm2' => 1090 if op aconv (apply2 Thm.term_of (Thm.dest_equals (Thm.cprop_of thm2'))) 1091 then NONE else SOME thm2')) 1092 end; 1093 1094val vA = (("A", 0), propT); 1095val vB = (("B", 0), propT); 1096val vC = (("C", 0), propT); 1097 1098fun transitive1 NONE NONE = NONE 1099 | transitive1 (SOME thm1) NONE = SOME thm1 1100 | transitive1 NONE (SOME thm2) = SOME thm2 1101 | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2); 1102 1103fun transitive2 thm = transitive1 (SOME thm); 1104fun transitive3 thm = transitive1 thm o SOME; 1105 1106fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) = 1107 let 1108 fun botc skel ctxt t = 1109 if is_Var skel then NONE 1110 else 1111 (case subc skel ctxt t of 1112 some as SOME thm1 => 1113 (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of 1114 SOME (thm2, skel2) => 1115 transitive2 (Thm.transitive thm1 thm2) 1116 (botc skel2 ctxt (Thm.rhs_of thm2)) 1117 | NONE => some) 1118 | NONE => 1119 (case rewritec (prover, maxidx) ctxt t of 1120 SOME (thm2, skel2) => transitive2 thm2 1121 (botc skel2 ctxt (Thm.rhs_of thm2)) 1122 | NONE => NONE)) 1123 1124 and try_botc ctxt t = 1125 (case botc skel0 ctxt t of 1126 SOME trec1 => trec1 1127 | NONE => Thm.reflexive t) 1128 1129 and subc skel ctxt t0 = 1130 let val Simpset (_, {congs, ...}) = simpset_of ctxt in 1131 (case Thm.term_of t0 of 1132 Abs (a, T, _) => 1133 let 1134 val (v, ctxt') = Variable.next_bound (a, T) ctxt; 1135 val b = #1 (Term.dest_Free v); 1136 val (v', t') = Thm.dest_abs (SOME b) t0; 1137 val b' = #1 (Term.dest_Free (Thm.term_of v')); 1138 val _ = 1139 if b <> b' then 1140 warning ("Bad Simplifier context: renamed bound variable " ^ 1141 quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) 1142 else (); 1143 val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0); 1144 in 1145 (case botc skel' ctxt' t' of 1146 SOME thm => SOME (Thm.abstract_rule a v' thm) 1147 | NONE => NONE) 1148 end 1149 | t $ _ => 1150 (case t of 1151 Const ("Pure.imp", _) $ _ => impc t0 ctxt 1152 | Abs _ => 1153 let val thm = Thm.beta_conversion false t0 1154 in 1155 (case subc skel0 ctxt (Thm.rhs_of thm) of 1156 NONE => SOME thm 1157 | SOME thm' => SOME (Thm.transitive thm thm')) 1158 end 1159 | _ => 1160 let 1161 fun appc () = 1162 let 1163 val (tskel, uskel) = 1164 (case skel of 1165 tskel $ uskel => (tskel, uskel) 1166 | _ => (skel0, skel0)); 1167 val (ct, cu) = Thm.dest_comb t0; 1168 in 1169 (case botc tskel ctxt ct of 1170 SOME thm1 => 1171 (case botc uskel ctxt cu of 1172 SOME thm2 => SOME (Thm.combination thm1 thm2) 1173 | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) 1174 | NONE => 1175 (case botc uskel ctxt cu of 1176 SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) 1177 | NONE => NONE)) 1178 end; 1179 val (h, ts) = strip_comb t; 1180 in 1181 (case cong_name h of 1182 SOME a => 1183 (case Congtab.lookup (fst congs) a of 1184 NONE => appc () 1185 | SOME cong => 1186 (*post processing: some partial applications h t1 ... tj, j <= length ts, 1187 may be a redex. Example: map (\<lambda>x. x) = (\<lambda>xs. xs) wrt map_cong*) 1188 (let 1189 val thm = congc (prover ctxt) ctxt maxidx cong t0; 1190 val t = the_default t0 (Option.map Thm.rhs_of thm); 1191 val (cl, cr) = Thm.dest_comb t 1192 val dVar = Var(("", 0), dummyT) 1193 val skel = 1194 list_comb (h, replicate (length ts) dVar) 1195 in 1196 (case botc skel ctxt cl of 1197 NONE => thm 1198 | SOME thm' => 1199 transitive3 thm (Thm.combination thm' (Thm.reflexive cr))) 1200 end handle Pattern.MATCH => appc ())) 1201 | _ => appc ()) 1202 end) 1203 | _ => NONE) 1204 end 1205 and impc ct ctxt = 1206 if mutsimp then mut_impc0 [] ct [] [] ctxt 1207 else nonmut_impc ct ctxt 1208 1209 and rules_of_prem prem ctxt = 1210 if maxidx_of_term (Thm.term_of prem) <> ~1 1211 then 1212 (cond_tracing ctxt (fn () => 1213 print_term ctxt "Cannot add premise as rewrite rule because it contains (type) unknowns:" 1214 (Thm.term_of prem)); 1215 (([], NONE), ctxt)) 1216 else 1217 let val (asm, ctxt') = Thm.assume_hyps prem ctxt 1218 in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end 1219 1220 and add_rrules (rrss, asms) ctxt = 1221 (fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms) 1222 1223 and disch r prem eq = 1224 let 1225 val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); 1226 val eq' = 1227 Thm.implies_elim 1228 (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong) 1229 (Thm.implies_intr prem eq); 1230 in 1231 if not r then eq' 1232 else 1233 let 1234 val (prem', concl) = Thm.dest_implies lhs; 1235 val (prem'', _) = Thm.dest_implies rhs; 1236 in 1237 Thm.transitive 1238 (Thm.transitive 1239 (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq) 1240 eq') 1241 (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq) 1242 end 1243 end 1244 1245 and rebuild [] _ _ _ _ eq = eq 1246 | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ctxt eq = 1247 let 1248 val ctxt' = add_rrules (rev rrss, rev asms) ctxt; 1249 val concl' = 1250 Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq)); 1251 val dprem = Option.map (disch false prem); 1252 in 1253 (case rewritec (prover, maxidx) ctxt' concl' of 1254 NONE => rebuild prems concl' rrss asms ctxt (dprem eq) 1255 | SOME (eq', _) => 1256 transitive2 (fold (disch false) prems (the (transitive3 (dprem eq) eq'))) 1257 (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ctxt)) 1258 end 1259 1260 and mut_impc0 prems concl rrss asms ctxt = 1261 let 1262 val prems' = strip_imp_prems concl; 1263 val ((rrss', asms'), ctxt') = fold_map rules_of_prem prems' ctxt |>> split_list; 1264 in 1265 mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') 1266 (asms @ asms') [] [] [] [] ctxt' ~1 ~1 1267 end 1268 1269 and mut_impc [] concl [] [] prems' rrss' asms' eqns ctxt changed k = 1270 transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1 1271 (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE) 1272 (if changed > 0 then 1273 mut_impc (rev prems') concl (rev rrss') (rev asms') 1274 [] [] [] [] ctxt ~1 changed 1275 else rebuild prems' concl rrss' asms' ctxt 1276 (botc skel0 (add_rrules (rev rrss', rev asms') ctxt) concl)) 1277 1278 | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) 1279 prems' rrss' asms' eqns ctxt changed k = 1280 (case (if k = 0 then NONE else botc skel0 (add_rrules 1281 (rev rrss' @ rrss, rev asms' @ asms) ctxt) prem) of 1282 NONE => mut_impc prems concl rrss asms (prem :: prems') 1283 (rrs :: rrss') (asm :: asms') (NONE :: eqns) ctxt changed 1284 (if k = 0 then 0 else k - 1) 1285 | SOME eqn => 1286 let 1287 val prem' = Thm.rhs_of eqn; 1288 val tprems = map Thm.term_of prems; 1289 val i = 1 + fold Integer.max (map (fn p => 1290 find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1; 1291 val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt; 1292 in 1293 mut_impc prems concl rrss asms (prem' :: prems') 1294 (rrs' :: rrss') (asm' :: asms') 1295 (SOME (fold_rev (disch true) 1296 (take i prems) 1297 (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies 1298 (drop i prems, concl))))) :: eqns) 1299 ctxt' (length prems') ~1 1300 end) 1301 1302 (*legacy code -- only for backwards compatibility*) 1303 and nonmut_impc ct ctxt = 1304 let 1305 val (prem, conc) = Thm.dest_implies ct; 1306 val thm1 = if simprem then botc skel0 ctxt prem else NONE; 1307 val prem1 = the_default prem (Option.map Thm.rhs_of thm1); 1308 val ctxt1 = 1309 if not useprem then ctxt 1310 else 1311 let val ((rrs, asm), ctxt') = rules_of_prem prem1 ctxt 1312 in add_rrules ([rrs], [asm]) ctxt' end; 1313 in 1314 (case botc skel0 ctxt1 conc of 1315 NONE => 1316 (case thm1 of 1317 NONE => NONE 1318 | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc))) 1319 | SOME thm2 => 1320 let val thm2' = disch false prem1 thm2 in 1321 (case thm1 of 1322 NONE => SOME thm2' 1323 | SOME thm1' => 1324 SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2')) 1325 end) 1326 end; 1327 1328 in try_botc end; 1329 1330 1331(* Meta-rewriting: rewrites t to u and returns the theorem t \<equiv> u *) 1332 1333(* 1334 Parameters: 1335 mode = (simplify A, 1336 use A in simplifying B, 1337 use prems of B (if B is again a meta-impl.) to simplify A) 1338 when simplifying A \<Longrightarrow> B 1339 prover: how to solve premises in conditional rewrites and congruences 1340*) 1341 1342fun rewrite_cterm mode prover raw_ctxt raw_ct = 1343 let 1344 val thy = Proof_Context.theory_of raw_ctxt; 1345 1346 val ct = raw_ct 1347 |> Thm.transfer_cterm thy 1348 |> Thm.adjust_maxidx_cterm ~1; 1349 val maxidx = Thm.maxidx_of_cterm ct; 1350 1351 val ctxt = 1352 raw_ctxt 1353 |> Variable.set_body true 1354 |> Context_Position.set_visible false 1355 |> inc_simp_depth 1356 |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt); 1357 1358 val _ = 1359 cond_tracing ctxt (fn () => 1360 print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (Thm.term_of ct)); 1361 in 1362 ct 1363 |> bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt 1364 |> Thm.solve_constraints 1365 end; 1366 1367val simple_prover = 1368 SINGLE o (fn ctxt => ALLGOALS (resolve_tac ctxt (prems_of ctxt))); 1369 1370fun rewrite _ _ [] = Thm.reflexive 1371 | rewrite ctxt full thms = 1372 rewrite_cterm (full, false, false) simple_prover (init_simpset thms ctxt); 1373 1374fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true; 1375 1376(*simple term rewriting -- no proof*) 1377fun rewrite_term thy rules procs = 1378 Pattern.rewrite_term thy (map decomp_simp' rules) procs; 1379 1380fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt); 1381 1382(*Rewrite the subgoals of a proof state (represented by a theorem)*) 1383fun rewrite_goals_rule ctxt thms th = 1384 Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover 1385 (init_simpset thms ctxt))) th; 1386 1387 1388(** meta-rewriting tactics **) 1389 1390(*Rewrite all subgoals*) 1391fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs); 1392 1393(*Rewrite one subgoal*) 1394fun generic_rewrite_goal_tac mode prover_tac ctxt i thm = 1395 if 0 < i andalso i <= Thm.nprems_of thm then 1396 Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm) 1397 else Seq.empty; 1398 1399fun rewrite_goal_tac ctxt thms = 1400 generic_rewrite_goal_tac (true, false, false) (K no_tac) (init_simpset thms ctxt); 1401 1402(*Prunes all redundant parameters from the proof state by rewriting.*) 1403fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality]; 1404 1405 1406(* for folding definitions, handling critical pairs *) 1407 1408(*The depth of nesting in a term*) 1409fun term_depth (Abs (_, _, t)) = 1 + term_depth t 1410 | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t) 1411 | term_depth _ = 0; 1412 1413val lhs_of_thm = #1 o Logic.dest_equals o Thm.prop_of; 1414 1415(*folding should handle critical pairs! E.g. K \<equiv> Inl 0, S \<equiv> Inr (Inl 0) 1416 Returns longest lhs first to avoid folding its subexpressions.*) 1417fun sort_lhs_depths defs = 1418 let val keylist = AList.make (term_depth o lhs_of_thm) defs 1419 val keys = sort_distinct (rev_order o int_ord) (map #2 keylist) 1420 in map (AList.find (op =) keylist) keys end; 1421 1422val rev_defs = sort_lhs_depths o map Thm.symmetric; 1423 1424fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs); 1425fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs)); 1426 1427 1428(* HHF normal form: \<And> before \<Longrightarrow>, outermost \<And> generalized *) 1429 1430local 1431 1432fun gen_norm_hhf ss ctxt0 th0 = 1433 let 1434 val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0); 1435 val th' = 1436 if Drule.is_norm_hhf (Thm.prop_of th) then th 1437 else 1438 Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th; 1439 in th' |> Thm.adjust_maxidx_thm ~1 |> Variable.gen_all ctxt end; 1440 1441val hhf_ss = 1442 Context.the_local_context () 1443 |> init_simpset Drule.norm_hhf_eqs 1444 |> simpset_of; 1445 1446val hhf_protect_ss = 1447 Context.the_local_context () 1448 |> init_simpset Drule.norm_hhf_eqs 1449 |> add_eqcong Drule.protect_cong 1450 |> simpset_of; 1451 1452in 1453 1454val norm_hhf = gen_norm_hhf hhf_ss; 1455val norm_hhf_protect = gen_norm_hhf hhf_protect_ss; 1456 1457end; 1458 1459end; 1460 1461structure Basic_Meta_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier; 1462open Basic_Meta_Simplifier; 1463