src/HOL/SMT.thy
 changeset 44488 587bf61a00a1 parent 44087 8e491cb8841c child 45392 828e08541cee
```     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
```