# HG changeset patch
# User boehmes
# Date 1401568263 -7200
# Node ID 1d12e22e7caf570beb8de4298560b8244c854243
# Parent  7b31461802914980d480ce19cee4b3f683823f12
more complete proof replay for Z3: support universally quantified rewrite steps

diff -r 7b3146180291 -r 1d12e22e7caf src/HOL/Tools/SMT2/z3_new_replay_methods.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Fri May 30 18:48:05 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Sat May 31 22:31:03 2014 +0200
@@ -395,13 +395,47 @@
 
 (* rewriting *)
 
-fun abstract_eq f1 f2 (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
-      f1 t1 ##>> f2 t2 #>> HOLogic.mk_eq
-  | abstract_eq _ _ t = abstract_term t
+local
+
+fun dest_all (Const (@{const_name HOL.All}, _) $ Abs (_, T, t)) nctxt =
+      let
+        val (n, nctxt') = Name.variant "" nctxt
+        val f = Free (n, T)
+        val t' = Term.subst_bound (f, t)
+      in dest_all t' nctxt' |>> cons f end
+  | dest_all t _ = ([], t)
+
+fun dest_alls t =
+  let
+    val nctxt = Name.make_context (Term.add_free_names t [])
+    val (lhs, rhs) = HOLogic.dest_eq (dest_prop t)
+    val (ls, lhs') = dest_all lhs nctxt
+    val (rs, rhs') = dest_all rhs nctxt
+  in
+    if eq_list (op aconv) (ls, rs) then SOME (ls, (HOLogic.mk_eq (lhs', rhs')))
+    else NONE
+  end
+
+fun forall_intr ctxt t thm =
+  let val ct = Thm.cterm_of (Proof_Context.theory_of ctxt) t
+  in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end
+
+in
+
+fun focus_eq f ctxt t =
+  (case dest_alls t of
+    NONE => f ctxt t
+  | SOME (vs, t') => fold (forall_intr ctxt) vs (f ctxt t'))
+
+end
+
+fun abstract_eq f (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
+      f t1 ##>> f t2 #>> HOLogic.mk_eq
+  | abstract_eq _ t = abstract_term t
 
 fun prove_prop_rewrite ctxt t =
   prove_abstract' ctxt t prop_tac (
-    abstract_eq abstract_prop abstract_prop (dest_prop t))
+    abstract_eq (abstract_eq abstract_prop) (dest_prop t))
 
 fun arith_rewrite_tac ctxt _ =
   TRY o Simplifier.simp_tac ctxt
@@ -409,12 +443,12 @@
 
 fun prove_arith_rewrite ctxt t =
   prove_abstract' ctxt t arith_rewrite_tac (
-    abstract_eq (abstract_arith ctxt) (abstract_arith ctxt) (dest_prop t))
+    abstract_eq (abstract_arith ctxt) (dest_prop t))
 
 fun rewrite ctxt _ = try_provers ctxt Z3_New_Proof.Rewrite [
   ("rules", apply_rule ctxt),
   ("prop_rewrite", prove_prop_rewrite ctxt),
-  ("arith_rewrite", prove_arith_rewrite ctxt)] []
+  ("arith_rewrite", focus_eq prove_arith_rewrite ctxt)] []
 
 fun rewrite_star ctxt = rewrite ctxt