improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization

--- a/src/HOL/SMT.thy	Thu Aug 25 00:00:36 2011 +0200
+++ b/src/HOL/SMT.thy	Thu Aug 25 11:15:31 2011 +0200
@@ -329,9 +329,24 @@
   if_True if_False not_not
 
 lemma [z3_rule]:
+  "(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
+  "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
+  "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
+  "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
+  "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
+  "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
+  "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
+  "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
+  by auto
+
+lemma [z3_rule]:
   "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
   "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
   "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
+  "(True \<longrightarrow> P) = P"
+  "(P \<longrightarrow> True) = True"
+  "(False \<longrightarrow> P) = True"
+  "(P \<longrightarrow> P) = True"
   by auto
 
 lemma [z3_rule]:
@@ -339,8 +354,18 @@
   by auto
 
 lemma [z3_rule]:
+  "(\<not>True) = False"
+  "(\<not>False) = True"
+  "(x = x) = True"
+  "(P = True) = P"
+  "(True = P) = P"
+  "(P = False) = (\<not>P)"
+  "(False = P) = (\<not>P)"
   "((\<not>P) = P) = False"
   "(P = (\<not>P)) = False"
+  "((\<not>P) = (\<not>Q)) = (P = Q)"
+  "\<not>(P = (\<not>Q)) = (P = Q)"
+  "\<not>((\<not>P) = Q) = (P = Q)"
   "(P \<noteq> Q) = (Q = (\<not>P))"
   "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
   "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
@@ -351,11 +376,36 @@
   "(if \<not>P then \<not>P else P) = True"
   "(if P then True else False) = P"
   "(if P then False else True) = (\<not>P)"
+  "(if P then Q else True) = ((\<not>P) \<or> Q)"
+  "(if P then Q else True) = (Q \<or> (\<not>P))"
+  "(if P then Q else \<not>Q) = (P = Q)"
+  "(if P then Q else \<not>Q) = (Q = P)"
+  "(if P then \<not>Q else Q) = (P = (\<not>Q))"
+  "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
   "(if \<not>P then x else y) = (if P then y else x)"
+  "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
+  "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
+  "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
+  "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)"
+  "(if P then x else if P then y else z) = (if P then x else z)"
+  "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
+  "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)"
+  "(if P then x = y else x = z) = (x = (if P then y else z))"
+  "(if P then x = y else y = z) = (y = (if P then x else z))"
+  "(if P then x = y else z = y) = (y = (if P then x else z))"
   "f (if P then x else y) = (if P then f x else f y)"
   by auto
 
 lemma [z3_rule]:
+  "0 + (x::int) = x"
+  "x + 0 = x"
+  "x + x = 2 * x"
+  "0 * x = 0"
+  "1 * x = x"
+  "x + y = y + x"
+  by auto
+
+lemma [z3_rule]:  (* for def-axiom *)
   "P = Q \<or> P \<or> Q"
   "P = Q \<or> \<not>P \<or> \<not>Q"
   "(\<not>P) = Q \<or> \<not>P \<or> Q"
@@ -370,14 +420,18 @@
   "P \<or> Q \<or> (\<not>P) \<noteq> Q"
   "P \<or> \<not>Q \<or> P \<noteq> Q"
   "\<not>P \<or> Q \<or> P \<noteq> Q"
-  by auto
-
-lemma [z3_rule]:
-  "0 + (x::int) = x"
-  "x + 0 = x"
-  "0 * x = 0"
-  "1 * x = x"
-  "x + y = y + x"
+  "P \<or> y = (if P then x else y)"
+  "P \<or> (if P then x else y) = y"
+  "\<not>P \<or> x = (if P then x else y)"
+  "\<not>P \<or>  (if P then x else y) = x"
+  "P \<or> R \<or> \<not>(if P then Q else R)"
+  "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
+  "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
+  "\<not>(if P then Q else R) \<or> P \<or> R"
+  "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
+  "(if P then Q else R) \<or> P \<or> \<not>R"
+  "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
+  "(if P then Q else \<not>R) \<or> P \<or> R"
   by auto
 
 

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Aug 25 00:00:36 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Aug 25 11:15:31 2011 +0200
@@ -147,13 +147,15 @@
   val remove_weight = mk_meta_eq @{thm SMT.weight_def}
   val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
 
-  fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
-    (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
+  fun rewrite_conv _ [] = Conv.all_conv
+    | rewrite_conv ctxt eqs = Simplifier.full_rewrite
+        (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
 
   val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
     remove_fun_app, Z3_Proof_Literals.rewrite_true]
 
-  fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
+  fun rewrite _ [] = I
+    | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
 
   fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
 
@@ -630,7 +632,8 @@
     in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
 
   val sk_rules = @{lemma
-    "(EX x. P x) = P (SOME x. P x)"   "(~(ALL x. P x)) = (~P (SOME x. ~P x))"
+    "c = (SOME x. P x) ==> (EX x. P x) = P c"
+    "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
     by (metis someI_ex)+}
 in
 
@@ -638,9 +641,10 @@
   apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
 
 fun discharge_sk_tac i st = (
-  Tactic.rtac @{thm trans}
-  THEN' Tactic.resolve_tac sk_rules
-  THEN' (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac)) i st
+  Tactic.rtac @{thm trans} i
+  THEN Tactic.resolve_tac sk_rules i
+  THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+  THEN Tactic.rtac @{thm refl} i) st
 
 end
 
@@ -654,7 +658,7 @@
     Z3_Proof_Tools.by_tac (
       NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
       ORELSE' NAMED ctxt' "simp+arith" (
-        Simplifier.simp_tac simpset
+        Simplifier.asm_full_simp_tac simpset
         THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
 
 
@@ -717,13 +721,15 @@
         THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
     Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
-        NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+        (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+        THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
         THEN_ALL_NEW (
           NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
           ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
     Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
       Z3_Proof_Tools.by_tac (
-        NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+        (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+        THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
         THEN_ALL_NEW (
           NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
           ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
@@ -731,7 +737,8 @@
     Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
       (fn ctxt' =>
         Z3_Proof_Tools.by_tac (
-          NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
+          (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
+          THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
           THEN_ALL_NEW (
             NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
             ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac