improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
authorboehmes
Thu Aug 25 11:15:31 2011 +0200 (2011-08-25)
changeset 44488587bf61a00a1
parent 44487 0989d8deab69
child 44489 6cddca146ca0
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
src/HOL/SMT.thy
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
     1.1 --- a/src/HOL/SMT.thy	Thu Aug 25 00:00:36 2011 +0200
     1.2 +++ b/src/HOL/SMT.thy	Thu Aug 25 11:15:31 2011 +0200
     1.3 @@ -329,9 +329,24 @@
     1.4    if_True if_False not_not
     1.5  
     1.6  lemma [z3_rule]:
     1.7 +  "(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
     1.8 +  "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
     1.9 +  "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
    1.10 +  "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
    1.11 +  "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
    1.12 +  "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
    1.13 +  "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
    1.14 +  "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
    1.15 +  by auto
    1.16 +
    1.17 +lemma [z3_rule]:
    1.18    "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
    1.19    "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
    1.20    "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
    1.21 +  "(True \<longrightarrow> P) = P"
    1.22 +  "(P \<longrightarrow> True) = True"
    1.23 +  "(False \<longrightarrow> P) = True"
    1.24 +  "(P \<longrightarrow> P) = True"
    1.25    by auto
    1.26  
    1.27  lemma [z3_rule]:
    1.28 @@ -339,8 +354,18 @@
    1.29    by auto
    1.30  
    1.31  lemma [z3_rule]:
    1.32 +  "(\<not>True) = False"
    1.33 +  "(\<not>False) = True"
    1.34 +  "(x = x) = True"
    1.35 +  "(P = True) = P"
    1.36 +  "(True = P) = P"
    1.37 +  "(P = False) = (\<not>P)"
    1.38 +  "(False = P) = (\<not>P)"
    1.39    "((\<not>P) = P) = False"
    1.40    "(P = (\<not>P)) = False"
    1.41 +  "((\<not>P) = (\<not>Q)) = (P = Q)"
    1.42 +  "\<not>(P = (\<not>Q)) = (P = Q)"
    1.43 +  "\<not>((\<not>P) = Q) = (P = Q)"
    1.44    "(P \<noteq> Q) = (Q = (\<not>P))"
    1.45    "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
    1.46    "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
    1.47 @@ -351,11 +376,36 @@
    1.48    "(if \<not>P then \<not>P else P) = True"
    1.49    "(if P then True else False) = P"
    1.50    "(if P then False else True) = (\<not>P)"
    1.51 +  "(if P then Q else True) = ((\<not>P) \<or> Q)"
    1.52 +  "(if P then Q else True) = (Q \<or> (\<not>P))"
    1.53 +  "(if P then Q else \<not>Q) = (P = Q)"
    1.54 +  "(if P then Q else \<not>Q) = (Q = P)"
    1.55 +  "(if P then \<not>Q else Q) = (P = (\<not>Q))"
    1.56 +  "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
    1.57    "(if \<not>P then x else y) = (if P then y else x)"
    1.58 +  "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
    1.59 +  "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
    1.60 +  "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
    1.61 +  "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)"
    1.62 +  "(if P then x else if P then y else z) = (if P then x else z)"
    1.63 +  "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
    1.64 +  "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)"
    1.65 +  "(if P then x = y else x = z) = (x = (if P then y else z))"
    1.66 +  "(if P then x = y else y = z) = (y = (if P then x else z))"
    1.67 +  "(if P then x = y else z = y) = (y = (if P then x else z))"
    1.68    "f (if P then x else y) = (if P then f x else f y)"
    1.69    by auto
    1.70  
    1.71  lemma [z3_rule]:
    1.72 +  "0 + (x::int) = x"
    1.73 +  "x + 0 = x"
    1.74 +  "x + x = 2 * x"
    1.75 +  "0 * x = 0"
    1.76 +  "1 * x = x"
    1.77 +  "x + y = y + x"
    1.78 +  by auto
    1.79 +
    1.80 +lemma [z3_rule]:  (* for def-axiom *)
    1.81    "P = Q \<or> P \<or> Q"
    1.82    "P = Q \<or> \<not>P \<or> \<not>Q"
    1.83    "(\<not>P) = Q \<or> \<not>P \<or> Q"
    1.84 @@ -370,14 +420,18 @@
    1.85    "P \<or> Q \<or> (\<not>P) \<noteq> Q"
    1.86    "P \<or> \<not>Q \<or> P \<noteq> Q"
    1.87    "\<not>P \<or> Q \<or> P \<noteq> Q"
    1.88 -  by auto
    1.89 -
    1.90 -lemma [z3_rule]:
    1.91 -  "0 + (x::int) = x"
    1.92 -  "x + 0 = x"
    1.93 -  "0 * x = 0"
    1.94 -  "1 * x = x"
    1.95 -  "x + y = y + x"
    1.96 +  "P \<or> y = (if P then x else y)"
    1.97 +  "P \<or> (if P then x else y) = y"
    1.98 +  "\<not>P \<or> x = (if P then x else y)"
    1.99 +  "\<not>P \<or>  (if P then x else y) = x"
   1.100 +  "P \<or> R \<or> \<not>(if P then Q else R)"
   1.101 +  "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
   1.102 +  "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
   1.103 +  "\<not>(if P then Q else R) \<or> P \<or> R"
   1.104 +  "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
   1.105 +  "(if P then Q else R) \<or> P \<or> \<not>R"
   1.106 +  "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
   1.107 +  "(if P then Q else \<not>R) \<or> P \<or> R"
   1.108    by auto
   1.109  
   1.110  
     2.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Aug 25 00:00:36 2011 +0200
     2.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Aug 25 11:15:31 2011 +0200
     2.3 @@ -147,13 +147,15 @@
     2.4    val remove_weight = mk_meta_eq @{thm SMT.weight_def}
     2.5    val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
     2.6  
     2.7 -  fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
     2.8 -    (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
     2.9 +  fun rewrite_conv _ [] = Conv.all_conv
    2.10 +    | rewrite_conv ctxt eqs = Simplifier.full_rewrite
    2.11 +        (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
    2.12  
    2.13    val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
    2.14      remove_fun_app, Z3_Proof_Literals.rewrite_true]
    2.15  
    2.16 -  fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
    2.17 +  fun rewrite _ [] = I
    2.18 +    | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
    2.19  
    2.20    fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
    2.21  
    2.22 @@ -630,7 +632,8 @@
    2.23      in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
    2.24  
    2.25    val sk_rules = @{lemma
    2.26 -    "(EX x. P x) = P (SOME x. P x)"   "(~(ALL x. P x)) = (~P (SOME x. ~P x))"
    2.27 +    "c = (SOME x. P x) ==> (EX x. P x) = P c"
    2.28 +    "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
    2.29      by (metis someI_ex)+}
    2.30  in
    2.31  
    2.32 @@ -638,9 +641,10 @@
    2.33    apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
    2.34  
    2.35  fun discharge_sk_tac i st = (
    2.36 -  Tactic.rtac @{thm trans}
    2.37 -  THEN' Tactic.resolve_tac sk_rules
    2.38 -  THEN' (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac)) i st
    2.39 +  Tactic.rtac @{thm trans} i
    2.40 +  THEN Tactic.resolve_tac sk_rules i
    2.41 +  THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
    2.42 +  THEN Tactic.rtac @{thm refl} i) st
    2.43  
    2.44  end
    2.45  
    2.46 @@ -654,7 +658,7 @@
    2.47      Z3_Proof_Tools.by_tac (
    2.48        NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
    2.49        ORELSE' NAMED ctxt' "simp+arith" (
    2.50 -        Simplifier.simp_tac simpset
    2.51 +        Simplifier.asm_full_simp_tac simpset
    2.52          THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
    2.53  
    2.54  
    2.55 @@ -717,13 +721,15 @@
    2.56          THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
    2.57      Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
    2.58        Z3_Proof_Tools.by_tac (
    2.59 -        NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
    2.60 +        (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
    2.61 +        THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
    2.62          THEN_ALL_NEW (
    2.63            NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
    2.64            ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
    2.65      Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
    2.66        Z3_Proof_Tools.by_tac (
    2.67 -        NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
    2.68 +        (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
    2.69 +        THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
    2.70          THEN_ALL_NEW (
    2.71            NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
    2.72            ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
    2.73 @@ -731,7 +737,8 @@
    2.74      Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
    2.75        (fn ctxt' =>
    2.76          Z3_Proof_Tools.by_tac (
    2.77 -          NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
    2.78 +          (Tactic.rtac @{thm iff_allI} ORELSE' K Tactical.all_tac)
    2.79 +          THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
    2.80            THEN_ALL_NEW (
    2.81              NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
    2.82              ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac