393 |
393 |
394 |
394 |
395 |
395 |
396 (* rewriting *) |
396 (* rewriting *) |
397 |
397 |
398 fun abstract_eq f1 f2 (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = |
398 local |
399 f1 t1 ##>> f2 t2 #>> HOLogic.mk_eq |
399 |
400 | abstract_eq _ _ t = abstract_term t |
400 fun dest_all (Const (@{const_name HOL.All}, _) $ Abs (_, T, t)) nctxt = |
|
401 let |
|
402 val (n, nctxt') = Name.variant "" nctxt |
|
403 val f = Free (n, T) |
|
404 val t' = Term.subst_bound (f, t) |
|
405 in dest_all t' nctxt' |>> cons f end |
|
406 | dest_all t _ = ([], t) |
|
407 |
|
408 fun dest_alls t = |
|
409 let |
|
410 val nctxt = Name.make_context (Term.add_free_names t []) |
|
411 val (lhs, rhs) = HOLogic.dest_eq (dest_prop t) |
|
412 val (ls, lhs') = dest_all lhs nctxt |
|
413 val (rs, rhs') = dest_all rhs nctxt |
|
414 in |
|
415 if eq_list (op aconv) (ls, rs) then SOME (ls, (HOLogic.mk_eq (lhs', rhs'))) |
|
416 else NONE |
|
417 end |
|
418 |
|
419 fun forall_intr ctxt t thm = |
|
420 let val ct = Thm.cterm_of (Proof_Context.theory_of ctxt) t |
|
421 in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end |
|
422 |
|
423 in |
|
424 |
|
425 fun focus_eq f ctxt t = |
|
426 (case dest_alls t of |
|
427 NONE => f ctxt t |
|
428 | SOME (vs, t') => fold (forall_intr ctxt) vs (f ctxt t')) |
|
429 |
|
430 end |
|
431 |
|
432 fun abstract_eq f (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = |
|
433 f t1 ##>> f t2 #>> HOLogic.mk_eq |
|
434 | abstract_eq _ t = abstract_term t |
401 |
435 |
402 fun prove_prop_rewrite ctxt t = |
436 fun prove_prop_rewrite ctxt t = |
403 prove_abstract' ctxt t prop_tac ( |
437 prove_abstract' ctxt t prop_tac ( |
404 abstract_eq abstract_prop abstract_prop (dest_prop t)) |
438 abstract_eq (abstract_eq abstract_prop) (dest_prop t)) |
405 |
439 |
406 fun arith_rewrite_tac ctxt _ = |
440 fun arith_rewrite_tac ctxt _ = |
407 TRY o Simplifier.simp_tac ctxt |
441 TRY o Simplifier.simp_tac ctxt |
408 THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt) |
442 THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt) |
409 |
443 |
410 fun prove_arith_rewrite ctxt t = |
444 fun prove_arith_rewrite ctxt t = |
411 prove_abstract' ctxt t arith_rewrite_tac ( |
445 prove_abstract' ctxt t arith_rewrite_tac ( |
412 abstract_eq (abstract_arith ctxt) (abstract_arith ctxt) (dest_prop t)) |
446 abstract_eq (abstract_arith ctxt) (dest_prop t)) |
413 |
447 |
414 fun rewrite ctxt _ = try_provers ctxt Z3_New_Proof.Rewrite [ |
448 fun rewrite ctxt _ = try_provers ctxt Z3_New_Proof.Rewrite [ |
415 ("rules", apply_rule ctxt), |
449 ("rules", apply_rule ctxt), |
416 ("prop_rewrite", prove_prop_rewrite ctxt), |
450 ("prop_rewrite", prove_prop_rewrite ctxt), |
417 ("arith_rewrite", prove_arith_rewrite ctxt)] [] |
451 ("arith_rewrite", focus_eq prove_arith_rewrite ctxt)] [] |
418 |
452 |
419 fun rewrite_star ctxt = rewrite ctxt |
453 fun rewrite_star ctxt = rewrite ctxt |
420 |
454 |
421 |
455 |
422 |
456 |