src/HOL/SMT_Examples/SMT_Tests.thy
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 57232 8cecd655eef4
child 57696 fb71c6f100f8
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     1 (*  Title:      HOL/SMT_Examples/SMT_Tests.thy
     2     Author:     Sascha Boehme, TU Muenchen
     3 *)
     4 
     5 header {* Tests for the SMT binding *}
     6 
     7 theory SMT_Tests
     8 imports Complex_Main
     9 begin
    10 
    11 smt_status
    12 smt2_status
    13 
    14 text {* Most examples are taken from various Isabelle theories and from HOL4. *}
    15 
    16 
    17 section {* Propositional logic *}
    18 
    19 lemma
    20   "True"
    21   "\<not> False"
    22   "\<not> \<not> True"
    23   "True \<and> True"
    24   "True \<or> False"
    25   "False \<longrightarrow> True"
    26   "\<not> (False \<longleftrightarrow> True)"
    27   by smt2+
    28 
    29 lemma
    30   "P \<or> \<not> P"
    31   "\<not> (P \<and> \<not> P)"
    32   "(True \<and> P) \<or> \<not> P \<or> (False \<and> P) \<or> P"
    33   "P \<longrightarrow> P"
    34   "P \<and> \<not> P \<longrightarrow> False"
    35   "P \<and> Q \<longrightarrow> Q \<and> P"
    36   "P \<or> Q \<longrightarrow> Q \<or> P"
    37   "P \<and> Q \<longrightarrow> P \<or> Q"
    38   "\<not> (P \<or> Q) \<longrightarrow> \<not> P"
    39   "\<not> (P \<or> Q) \<longrightarrow> \<not> Q"
    40   "\<not> P \<longrightarrow> \<not> (P \<and> Q)"
    41   "\<not> Q \<longrightarrow> \<not> (P \<and> Q)"
    42   "(P \<and> Q) \<longleftrightarrow> (\<not> (\<not> P \<or> \<not> Q))"
    43   "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
    44   "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
    45   "(P \<and> Q) \<or> R  \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
    46   "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R"
    47   "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)"
    48   "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R"
    49   "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
    50   "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
    51   "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
    52   "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow>  ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
    53   "\<not> (P \<longrightarrow> R) \<longrightarrow>  \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
    54   "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
    55   "P \<longrightarrow> (Q \<longrightarrow> P)"
    56   "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q)\<longrightarrow> (P \<longrightarrow> R)"
    57   "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
    58   "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
    59   "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
    60   "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)"
    61   "(P \<longrightarrow> Q) \<and> (Q  \<longrightarrow> P) \<longrightarrow> (P \<longleftrightarrow> Q)"
    62   "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
    63   "\<not> (P \<longleftrightarrow> \<not> P)"
    64   "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
    65   "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"
    66   by smt2+
    67 
    68 lemma
    69   "(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not> P \<longrightarrow> Q2))"
    70   "if P then (Q \<longrightarrow> P) else (P \<longrightarrow> Q)"
    71   "(if P1 \<or> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then Q1 else if P2 then Q1 else Q2)"
    72   "(if P1 \<and> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then if P2 then Q1 else Q2 else Q2)"
    73   "(P1 \<longrightarrow> (if P2 then Q1 else Q2)) \<longleftrightarrow>
    74    (if P1 \<longrightarrow> P2 then P1 \<longrightarrow> Q1 else P1 \<longrightarrow> Q2)"
    75   by smt2+
    76 
    77 lemma
    78   "case P of True \<Rightarrow> P | False \<Rightarrow> \<not> P"
    79   "case P of False \<Rightarrow> \<not> P | True \<Rightarrow> P"
    80   "case \<not> P of True \<Rightarrow> \<not> P | False \<Rightarrow> P"
    81   "case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)"
    82   by smt2+
    83 
    84 
    85 section {* First-order logic with equality *}
    86 
    87 lemma
    88   "x = x"
    89   "x = y \<longrightarrow> y = x"
    90   "x = y \<and> y = z \<longrightarrow> x = z"
    91   "x = y \<longrightarrow> f x = f y"
    92   "x = y \<longrightarrow> g x y = g y x"
    93   "f (f x) = x \<and> f (f (f (f (f x)))) = x \<longrightarrow> f x = x"
    94   "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
    95   by smt2+
    96 
    97 lemma
    98   "\<forall>x. x = x"
    99   "(\<forall>x. P x) \<longleftrightarrow> (\<forall>y. P y)"
   100   "\<forall>x. P x \<longrightarrow> (\<forall>y. P x \<or> P y)"
   101   "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)"
   102   "(\<forall>x. P x) \<or> R \<longleftrightarrow> (\<forall>x. P x \<or> R)"
   103   "(\<forall>x y z. S x z) \<longleftrightarrow> (\<forall>x z. S x z)"
   104   "(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x"
   105   "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))"
   106   "(\<forall>x y. s x y = s y x) \<longrightarrow> a = a \<and> s a b = s b a"
   107   "(\<forall>s. q s \<longrightarrow> r s) \<and> \<not> r s \<and> (\<forall>s. \<not> r s \<and> \<not> q s \<longrightarrow> p t \<or> q t) \<longrightarrow> p t \<or> r t"
   108   by smt2+
   109 
   110 lemma
   111   "(\<forall>x. P x) \<and> R \<longleftrightarrow> (\<forall>x. P x \<and> R)"
   112   by smt2
   113 
   114 lemma
   115   "\<exists>x. x = x"
   116   "(\<exists>x. P x) \<longleftrightarrow> (\<exists>y. P y)"
   117   "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)"
   118   "(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)"
   119   "(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)"
   120   "\<not> ((\<exists>x. \<not> P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not> (\<exists>x. P x))"
   121   by smt2+
   122 
   123 lemma
   124   "\<exists>x y. x = y"
   125   "\<exists>x. P x \<longrightarrow> (\<exists>y. P x \<and> P y)"
   126   "(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)"
   127   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
   128   "\<exists>x. (\<exists>y. P y) \<longrightarrow> P x"
   129   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
   130   by smt2+
   131 
   132 lemma
   133   "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   134   "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   135   "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"
   136   "(if P x then \<not> (\<exists>y. P y) else (\<forall>y. \<not> P y)) \<longrightarrow> P x \<longrightarrow> P y"
   137   "(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c"
   138   by smt2+
   139 
   140 lemma
   141   "\<forall>x. \<exists>y. f x y = f x (g x)"
   142   "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   143   "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   144   "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   145   "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
   146   "(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))"
   147   "\<exists>z. P z \<longrightarrow> (\<forall>x. P x)"
   148   "(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
   149   by smt2+
   150 
   151 lemma
   152   "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)"
   153   "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not> P y))"
   154   "P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)"
   155   "(\<exists>x. P x) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y) \<longrightarrow> (\<exists>!x. P x)"
   156   "(\<exists>!x. P x) \<and> (\<forall>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> R) \<longrightarrow> R"
   157   by smt2+
   158 
   159 lemma
   160   "(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c"
   161   "(\<exists>x\<in>M. P x) \<or> \<not> (P c \<and> c \<in> M)"
   162   by smt2+
   163 
   164 lemma
   165   "let P = True in P"
   166   "let P = P1 \<or> P2 in P \<or> \<not> P"
   167   "let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1"
   168   "(let x = y in x) = y"
   169   "(let x = y in Q x) \<longleftrightarrow> (let z = y in Q z)"
   170   "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y2; x = y1 in R x z)"
   171   "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)"
   172   "let P = (\<forall>x. Q x) in if P then P else \<not> P"
   173   by smt2+
   174 
   175 lemma
   176   "a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
   177   by smt2
   178 
   179 lemma
   180   "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
   181   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
   182   by smt2+
   183 
   184 
   185 section {* Guidance for quantifier heuristics: patterns *}
   186 
   187 lemma
   188   assumes "\<forall>x.
   189     SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat (f x)) SMT2.Symb_Nil) SMT2.Symb_Nil)
   190     (f x = x)"
   191   shows "f 1 = 1"
   192   using assms using [[smt2_trace]] by smt2
   193 
   194 lemma
   195   assumes "\<forall>x y.
   196     SMT2.trigger (SMT2.Symb_Cons (SMT2.Symb_Cons (SMT2.pat (f x))
   197       (SMT2.Symb_Cons (SMT2.pat (g y)) SMT2.Symb_Nil)) SMT2.Symb_Nil) (f x = g y)"
   198   shows "f a = g b"
   199   using assms by smt2
   200 
   201 
   202 section {* Meta-logical connectives *}
   203 
   204 lemma
   205   "True \<Longrightarrow> True"
   206   "False \<Longrightarrow> True"
   207   "False \<Longrightarrow> False"
   208   "P' x \<Longrightarrow> P' x"
   209   "P \<Longrightarrow> P \<or> Q"
   210   "Q \<Longrightarrow> P \<or> Q"
   211   "\<not> P \<Longrightarrow> P \<longrightarrow> Q"
   212   "Q \<Longrightarrow> P \<longrightarrow> Q"
   213   "\<lbrakk>P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<longrightarrow> Q)"
   214   "P' x \<equiv> P' x"
   215   "P' x \<equiv> Q' x \<Longrightarrow> P' x = Q' x"
   216   "P' x = Q' x \<Longrightarrow> P' x \<equiv> Q' x"
   217   "x \<equiv> y \<Longrightarrow> y \<equiv> z \<Longrightarrow> x \<equiv> (z::'a::type)"
   218   "x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y"
   219   "(\<And>x. g x) \<Longrightarrow> g a \<or> a"
   220   "(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x"
   221   "(p \<or> q) \<and> \<not> p \<Longrightarrow> q"
   222   "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   223   by smt2+
   224 
   225 
   226 section {* Natural numbers *}
   227 
   228 lemma
   229   "(0::nat) = 0"
   230   "(1::nat) = 1"
   231   "(0::nat) < 1"
   232   "(0::nat) \<le> 1"
   233   "(123456789::nat) < 2345678901"
   234   by smt2+
   235 
   236 lemma
   237   "Suc 0 = 1"
   238   "Suc x = x + 1"
   239   "x < Suc x"
   240   "(Suc x = Suc y) = (x = y)"
   241   "Suc (x + y) < Suc x + Suc y"
   242   by smt2+
   243 
   244 lemma
   245   "(x::nat) + 0 = x"
   246   "0 + x = x"
   247   "x + y = y + x"
   248   "x + (y + z) = (x + y) + z"
   249   "(x + y = 0) = (x = 0 \<and> y = 0)"
   250   by smt2+
   251 
   252 lemma
   253   "(x::nat) - 0 = x"
   254   "x < y \<longrightarrow> x - y = 0"
   255   "x - y = 0 \<or> y - x = 0"
   256   "(x - y) + y = (if x < y then y else x)"
   257   "x - y - z = x - (y + z)"
   258   by smt2+
   259 
   260 lemma
   261   "(x::nat) * 0 = 0"
   262   "0 * x = 0"
   263   "x * 1 = x"
   264   "1 * x = x"
   265   "3 * x = x * 3"
   266   by smt2+
   267 
   268 lemma
   269   "(0::nat) div 0 = 0"
   270   "(x::nat) div 0 = 0"
   271   "(0::nat) div 1 = 0"
   272   "(1::nat) div 1 = 1"
   273   "(3::nat) div 1 = 3"
   274   "(x::nat) div 1 = x"
   275   "(0::nat) div 3 = 0"
   276   "(1::nat) div 3 = 0"
   277   "(3::nat) div 3 = 1"
   278   "(x::nat) div 3 \<le> x"
   279   "(x div 3 = x) = (x = 0)"
   280   using [[z3_new_extensions]]
   281   by smt2+
   282 
   283 lemma
   284   "(0::nat) mod 0 = 0"
   285   "(x::nat) mod 0 = x"
   286   "(0::nat) mod 1 = 0"
   287   "(1::nat) mod 1 = 0"
   288   "(3::nat) mod 1 = 0"
   289   "(x::nat) mod 1 = 0"
   290   "(0::nat) mod 3 = 0"
   291   "(1::nat) mod 3 = 1"
   292   "(3::nat) mod 3 = 0"
   293   "x mod 3 < 3"
   294   "(x mod 3 = x) = (x < 3)"
   295   using [[z3_new_extensions]]
   296   by smt2+
   297 
   298 lemma
   299   "(x::nat) = x div 1 * 1 + x mod 1"
   300   "x = x div 3 * 3 + x mod 3"
   301   using [[z3_new_extensions]]
   302   by smt2+
   303 
   304 lemma
   305   "min (x::nat) y \<le> x"
   306   "min x y \<le> y"
   307   "min x y \<le> x + y"
   308   "z < x \<and> z < y \<longrightarrow> z < min x y"
   309   "min x y = min y x"
   310   "min x 0 = 0"
   311   by smt2+
   312 
   313 lemma
   314   "max (x::nat) y \<ge> x"
   315   "max x y \<ge> y"
   316   "max x y \<ge> (x - y) + (y - x)"
   317   "z > x \<and> z > y \<longrightarrow> z > max x y"
   318   "max x y = max y x"
   319   "max x 0 = x"
   320   by smt2+
   321 
   322 lemma
   323   "0 \<le> (x::nat)"
   324   "0 < x \<and> x \<le> 1 \<longrightarrow> x = 1"
   325   "x \<le> x"
   326   "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   327   "x < y \<longrightarrow> 3 * x < 3 * y"
   328   "x < y \<longrightarrow> x \<le> y"
   329   "(x < y) = (x + 1 \<le> y)"
   330   "\<not> (x < x)"
   331   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   332   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   333   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   334   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   335   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   336   by smt2+
   337 
   338 
   339 section {* Integers *}
   340 
   341 lemma
   342   "(0::int) = 0"
   343   "(0::int) = (- 0)"
   344   "(1::int) = 1"
   345   "\<not> (-1 = (1::int))"
   346   "(0::int) < 1"
   347   "(0::int) \<le> 1"
   348   "-123 + 345 < (567::int)"
   349   "(123456789::int) < 2345678901"
   350   "(-123456789::int) < 2345678901"
   351   by smt2+
   352 
   353 lemma
   354   "(x::int) + 0 = x"
   355   "0 + x = x"
   356   "x + y = y + x"
   357   "x + (y + z) = (x + y) + z"
   358   "(x + y = 0) = (x = -y)"
   359   by smt2+
   360 
   361 lemma
   362   "(-1::int) = - 1"
   363   "(-3::int) = - 3"
   364   "-(x::int) < 0 \<longleftrightarrow> x > 0"
   365   "x > 0 \<longrightarrow> -x < 0"
   366   "x < 0 \<longrightarrow> -x > 0"
   367   by smt2+
   368 
   369 lemma
   370   "(x::int) - 0 = x"
   371   "0 - x = -x"
   372   "x < y \<longrightarrow> x - y < 0"
   373   "x - y = -(y - x)"
   374   "x - y = -y + x"
   375   "x - y - z = x - (y + z)"
   376   by smt2+
   377 
   378 lemma
   379   "(x::int) * 0 = 0"
   380   "0 * x = 0"
   381   "x * 1 = x"
   382   "1 * x = x"
   383   "x * -1 = -x"
   384   "-1 * x = -x"
   385   "3 * x = x * 3"
   386   by smt2+
   387 
   388 lemma
   389   "(0::int) div 0 = 0"
   390   "(x::int) div 0 = 0"
   391   "(0::int) div 1 = 0"
   392   "(1::int) div 1 = 1"
   393   "(3::int) div 1 = 3"
   394   "(x::int) div 1 = x"
   395   "(0::int) div -1 = 0"
   396   "(1::int) div -1 = -1"
   397   "(3::int) div -1 = -3"
   398   "(x::int) div -1 = -x"
   399   "(0::int) div 3 = 0"
   400   "(0::int) div -3 = 0"
   401   "(1::int) div 3 = 0"
   402   "(3::int) div 3 = 1"
   403   "(5::int) div 3 = 1"
   404   "(1::int) div -3 = -1"
   405   "(3::int) div -3 = -1"
   406   "(5::int) div -3 = -2"
   407   "(-1::int) div 3 = -1"
   408   "(-3::int) div 3 = -1"
   409   "(-5::int) div 3 = -2"
   410   "(-1::int) div -3 = 0"
   411   "(-3::int) div -3 = 1"
   412   "(-5::int) div -3 = 1"
   413   using [[z3_new_extensions]]
   414   by smt2+
   415 
   416 lemma
   417   "(0::int) mod 0 = 0"
   418   "(x::int) mod 0 = x"
   419   "(0::int) mod 1 = 0"
   420   "(1::int) mod 1 = 0"
   421   "(3::int) mod 1 = 0"
   422   "(x::int) mod 1 = 0"
   423   "(0::int) mod -1 = 0"
   424   "(1::int) mod -1 = 0"
   425   "(3::int) mod -1 = 0"
   426   "(x::int) mod -1 = 0"
   427   "(0::int) mod 3 = 0"
   428   "(0::int) mod -3 = 0"
   429   "(1::int) mod 3 = 1"
   430   "(3::int) mod 3 = 0"
   431   "(5::int) mod 3 = 2"
   432   "(1::int) mod -3 = -2"
   433   "(3::int) mod -3 = 0"
   434   "(5::int) mod -3 = -1"
   435   "(-1::int) mod 3 = 2"
   436   "(-3::int) mod 3 = 0"
   437   "(-5::int) mod 3 = 1"
   438   "(-1::int) mod -3 = -1"
   439   "(-3::int) mod -3 = 0"
   440   "(-5::int) mod -3 = -2"
   441   "x mod 3 < 3"
   442   "(x mod 3 = x) \<longrightarrow> (x < 3)"
   443   using [[z3_new_extensions]]
   444   by smt2+
   445 
   446 lemma
   447   "(x::int) = x div 1 * 1 + x mod 1"
   448   "x = x div 3 * 3 + x mod 3"
   449   using [[z3_new_extensions]]
   450   by smt2+
   451 
   452 lemma
   453   "abs (x::int) \<ge> 0"
   454   "(abs x = 0) = (x = 0)"
   455   "(x \<ge> 0) = (abs x = x)"
   456   "(x \<le> 0) = (abs x = -x)"
   457   "abs (abs x) = abs x"
   458   by smt2+
   459 
   460 lemma
   461   "min (x::int) y \<le> x"
   462   "min x y \<le> y"
   463   "z < x \<and> z < y \<longrightarrow> z < min x y"
   464   "min x y = min y x"
   465   "x \<ge> 0 \<longrightarrow> min x 0 = 0"
   466   "min x y \<le> abs (x + y)"
   467   by smt2+
   468 
   469 lemma
   470   "max (x::int) y \<ge> x"
   471   "max x y \<ge> y"
   472   "z > x \<and> z > y \<longrightarrow> z > max x y"
   473   "max x y = max y x"
   474   "x \<ge> 0 \<longrightarrow> max x 0 = x"
   475   "max x y \<ge> - abs x - abs y"
   476   by smt2+
   477 
   478 lemma
   479   "0 < (x::int) \<and> x \<le> 1 \<longrightarrow> x = 1"
   480   "x \<le> x"
   481   "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   482   "x < y \<longrightarrow> 3 * x < 3 * y"
   483   "x < y \<longrightarrow> x \<le> y"
   484   "(x < y) = (x + 1 \<le> y)"
   485   "\<not> (x < x)"
   486   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   487   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   488   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   489   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   490   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   491   by smt2+
   492 
   493 
   494 section {* Reals *}
   495 
   496 lemma
   497   "(0::real) = 0"
   498   "(0::real) = -0"
   499   "(0::real) = (- 0)"
   500   "(1::real) = 1"
   501   "\<not> (-1 = (1::real))"
   502   "(0::real) < 1"
   503   "(0::real) \<le> 1"
   504   "-123 + 345 < (567::real)"
   505   "(123456789::real) < 2345678901"
   506   "(-123456789::real) < 2345678901"
   507   by smt2+
   508 
   509 lemma
   510   "(x::real) + 0 = x"
   511   "0 + x = x"
   512   "x + y = y + x"
   513   "x + (y + z) = (x + y) + z"
   514   "(x + y = 0) = (x = -y)"
   515   by smt2+
   516 
   517 lemma
   518   "(-1::real) = - 1"
   519   "(-3::real) = - 3"
   520   "-(x::real) < 0 \<longleftrightarrow> x > 0"
   521   "x > 0 \<longrightarrow> -x < 0"
   522   "x < 0 \<longrightarrow> -x > 0"
   523   by smt2+
   524 
   525 lemma
   526   "(x::real) - 0 = x"
   527   "0 - x = -x"
   528   "x < y \<longrightarrow> x - y < 0"
   529   "x - y = -(y - x)"
   530   "x - y = -y + x"
   531   "x - y - z = x - (y + z)"
   532   by smt2+
   533 
   534 lemma
   535   "(x::real) * 0 = 0"
   536   "0 * x = 0"
   537   "x * 1 = x"
   538   "1 * x = x"
   539   "x * -1 = -x"
   540   "-1 * x = -x"
   541   "3 * x = x * 3"
   542   by smt2+
   543 
   544 lemma
   545   "(1/2 :: real) < 1"
   546   "(1::real) / 3 = 1 / 3"
   547   "(1::real) / -3 = - 1 / 3"
   548   "(-1::real) / 3 = - 1 / 3"
   549   "(-1::real) / -3 = 1 / 3"
   550   "(x::real) / 1 = x"
   551   "x > 0 \<longrightarrow> x / 3 < x"
   552   "x < 0 \<longrightarrow> x / 3 > x"
   553   using [[z3_new_extensions]]
   554   by smt2+
   555 
   556 lemma
   557   "(3::real) * (x / 3) = x"
   558   "(x * 3) / 3 = x"
   559   "x > 0 \<longrightarrow> 2 * x / 3 < x"
   560   "x < 0 \<longrightarrow> 2 * x / 3 > x"
   561   using [[z3_new_extensions]]
   562   by smt2+
   563 
   564 lemma
   565   "abs (x::real) \<ge> 0"
   566   "(abs x = 0) = (x = 0)"
   567   "(x \<ge> 0) = (abs x = x)"
   568   "(x \<le> 0) = (abs x = -x)"
   569   "abs (abs x) = abs x"
   570   by smt2+
   571 
   572 lemma
   573   "min (x::real) y \<le> x"
   574   "min x y \<le> y"
   575   "z < x \<and> z < y \<longrightarrow> z < min x y"
   576   "min x y = min y x"
   577   "x \<ge> 0 \<longrightarrow> min x 0 = 0"
   578   "min x y \<le> abs (x + y)"
   579   by smt2+
   580 
   581 lemma
   582   "max (x::real) y \<ge> x"
   583   "max x y \<ge> y"
   584   "z > x \<and> z > y \<longrightarrow> z > max x y"
   585   "max x y = max y x"
   586   "x \<ge> 0 \<longrightarrow> max x 0 = x"
   587   "max x y \<ge> - abs x - abs y"
   588   by smt2+
   589 
   590 lemma
   591   "x \<le> (x::real)"
   592   "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   593   "x < y \<longrightarrow> 3 * x < 3 * y"
   594   "x < y \<longrightarrow> x \<le> y"
   595   "\<not> (x < x)"
   596   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   597   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   598   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   599   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   600   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   601   by smt2+
   602 
   603 
   604 section {* Datatypes, Records, and Typedefs *}
   605 
   606 subsection {* Without support by the SMT solver *}
   607 
   608 subsubsection {* Algebraic datatypes *}
   609 
   610 lemma
   611   "x = fst (x, y)"
   612   "y = snd (x, y)"
   613   "((x, y) = (y, x)) = (x = y)"
   614   "((x, y) = (u, v)) = (x = u \<and> y = v)"
   615   "(fst (x, y, z) = fst (u, v, w)) = (x = u)"
   616   "(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)"
   617   "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)"
   618   "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)"
   619   "(fst (x, y) = snd (x, y)) = (x = y)"
   620   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   621   "(fst (x, y) = snd (x, y)) = (x = y)"
   622   "(fst p = snd p) = (p = (snd p, fst p))"
   623   using fst_conv snd_conv pair_collapse
   624   by smt2+
   625 
   626 lemma
   627   "[x] \<noteq> Nil"
   628   "[x, y] \<noteq> Nil"
   629   "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]"
   630   "hd (x # xs) = x"
   631   "tl (x # xs) = xs"
   632   "hd [x, y, z] = x"
   633   "tl [x, y, z] = [y, z]"
   634   "hd (tl [x, y, z]) = y"
   635   "tl (tl [x, y, z]) = [z]"
   636   using list.sel(1,3) list.simps
   637   by smt2+
   638 
   639 lemma
   640   "fst (hd [(a, b)]) = a"
   641   "snd (hd [(a, b)]) = b"
   642   using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps
   643   by smt2+
   644 
   645 
   646 subsubsection {* Records *}
   647 
   648 record point =
   649   cx :: int
   650   cy :: int
   651 
   652 record bw_point = point +
   653   black :: bool
   654 
   655 lemma
   656   "p1 = p2 \<longrightarrow> cx p1 = cx p2"
   657   "p1 = p2 \<longrightarrow> cy p1 = cy p2"
   658   "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
   659   "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
   660   using point.simps
   661   by smt2+
   662 
   663 lemma
   664   "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3"
   665   "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4"
   666   "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>"
   667   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>"
   668   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>"
   669   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   670   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p"
   671   using point.simps
   672   by smt2+
   673 
   674 lemma
   675   "cy (p \<lparr> cx := a \<rparr>) = cy p"
   676   "cx (p \<lparr> cy := a \<rparr>) = cx p"
   677   "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
   678   sorry
   679 
   680 lemma
   681   "p1 = p2 \<longrightarrow> cx p1 = cx p2"
   682   "p1 = p2 \<longrightarrow> cy p1 = cy p2"
   683   "p1 = p2 \<longrightarrow> black p1 = black p2"
   684   "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
   685   "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
   686   "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2"
   687   using point.simps bw_point.simps
   688   by smt2+
   689 
   690 lemma
   691   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3"
   692   "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4"
   693   "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b"
   694   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>"
   695   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>"
   696   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>"
   697   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   698      p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p"
   699   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   700      p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
   701   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   702      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   703   using point.simps bw_point.simps
   704   by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *)
   705 
   706 lemma
   707   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
   708   "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
   709      \<lparr> cx = 3, cy = 4, black = False \<rparr>"
   710   "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> =
   711      p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
   712   sorry
   713 
   714 
   715 subsubsection {* Type definitions *}
   716 
   717 typedef int' = "UNIV::int set" by (rule UNIV_witness)
   718 
   719 definition n0 where "n0 = Abs_int' 0"
   720 definition n1 where "n1 = Abs_int' 1"
   721 definition n2 where "n2 = Abs_int' 2"
   722 definition plus' where "plus' n m = Abs_int' (Rep_int' n + Rep_int' m)"
   723 
   724 lemma
   725   "n0 \<noteq> n1"
   726   "plus' n1 n1 = n2"
   727   "plus' n0 n2 = n2"
   728   by (smt2 n0_def n1_def n2_def plus'_def Abs_int'_inverse Rep_int'_inverse UNIV_I)+
   729 
   730 
   731 subsection {* With support by the SMT solver (but without proofs) *}
   732 
   733 subsubsection {* Algebraic datatypes *}
   734 
   735 lemma
   736   "x = fst (x, y)"
   737   "y = snd (x, y)"
   738   "((x, y) = (y, x)) = (x = y)"
   739   "((x, y) = (u, v)) = (x = u \<and> y = v)"
   740   "(fst (x, y, z) = fst (u, v, w)) = (x = u)"
   741   "(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)"
   742   "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)"
   743   "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)"
   744   "(fst (x, y) = snd (x, y)) = (x = y)"
   745   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   746   "(fst (x, y) = snd (x, y)) = (x = y)"
   747   "(fst p = snd p) = (p = (snd p, fst p))"
   748   using fst_conv snd_conv pair_collapse
   749   using [[smt2_oracle, z3_new_extensions]]
   750   by smt2+
   751 
   752 lemma
   753   "[x] \<noteq> Nil"
   754   "[x, y] \<noteq> Nil"
   755   "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]"
   756   "hd (x # xs) = x"
   757   "tl (x # xs) = xs"
   758   "hd [x, y, z] = x"
   759   "tl [x, y, z] = [y, z]"
   760   "hd (tl [x, y, z]) = y"
   761   "tl (tl [x, y, z]) = [z]"
   762   using list.sel(1,3)
   763   using [[smt2_oracle, z3_new_extensions]]
   764   by smt2+
   765 
   766 lemma
   767   "fst (hd [(a, b)]) = a"
   768   "snd (hd [(a, b)]) = b"
   769   using fst_conv snd_conv pair_collapse list.sel(1,3)
   770   using [[smt2_oracle, z3_new_extensions]]
   771   by smt2+
   772 
   773 
   774 subsubsection {* Records *}
   775 
   776 lemma
   777   "p1 = p2 \<longrightarrow> cx p1 = cx p2"
   778   "p1 = p2 \<longrightarrow> cy p1 = cy p2"
   779   "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
   780   "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
   781   using point.simps
   782   using [[smt2_oracle, z3_new_extensions]]
   783   by smt2+
   784 
   785 lemma
   786   "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3"
   787   "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4"
   788   "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>"
   789   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>"
   790   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>"
   791   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   792   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p"
   793   using point.simps
   794   using [[smt2_oracle, z3_new_extensions]]
   795   by smt2+
   796 
   797 lemma
   798   "cy (p \<lparr> cx := a \<rparr>) = cy p"
   799   "cx (p \<lparr> cy := a \<rparr>) = cx p"
   800   "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
   801   using point.simps
   802   using [[smt2_oracle, z3_new_extensions]]
   803   by smt2+
   804 
   805 lemma
   806   "p1 = p2 \<longrightarrow> cx p1 = cx p2"
   807   "p1 = p2 \<longrightarrow> cy p1 = cy p2"
   808   "p1 = p2 \<longrightarrow> black p1 = black p2"
   809   "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
   810   "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
   811   "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2"
   812   using point.simps bw_point.simps
   813   using [[smt2_oracle, z3_new_extensions]]
   814   by smt2+
   815 
   816 lemma
   817   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3"
   818   "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4"
   819   "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b"
   820   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>"
   821   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>"
   822   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>"
   823   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   824      p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p"
   825   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   826      p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
   827   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
   828      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   829   using point.simps bw_point.simps
   830   using [[smt2_oracle, z3_new_extensions]]
   831   by smt2+
   832 
   833 lemma
   834   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
   835   "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
   836      \<lparr> cx = 3, cy = 4, black = False \<rparr>"
   837   sorry
   838 
   839 lemma
   840   "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> =
   841      p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
   842   using point.simps bw_point.simps
   843   using [[smt2_oracle, z3_new_extensions]]
   844   by smt2
   845 
   846 
   847 subsubsection {* Type definitions *}
   848 
   849 lemma
   850   "n0 \<noteq> n1"
   851   "plus' n1 n1 = n2"
   852   "plus' n0 n2 = n2"
   853   using [[smt2_oracle, z3_new_extensions]]
   854   by (smt2 n0_def n1_def n2_def plus'_def)+
   855 
   856 
   857 section {* Function updates *}
   858 
   859 lemma
   860   "(f (i := v)) i = v"
   861   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2"
   862   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1"
   863   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2"
   864   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   865   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   866   "i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and>  i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
   867   using fun_upd_same fun_upd_apply
   868   by smt2+
   869 
   870 
   871 section {* Sets *}
   872 
   873 lemma Empty: "x \<notin> {}" by simp
   874 
   875 lemmas smt2_sets = Empty UNIV_I Un_iff Int_iff
   876 
   877 lemma
   878   "x \<notin> {}"
   879   "x \<in> UNIV"
   880   "x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B"
   881   "x \<in> P \<union> {} \<longleftrightarrow> x \<in> P"
   882   "x \<in> P \<union> UNIV"
   883   "x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P"
   884   "x \<in> P \<union> P \<longleftrightarrow> x \<in> P"
   885   "x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R"
   886   "x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B"
   887   "x \<notin> P \<inter> {}"
   888   "x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P"
   889   "x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P"
   890   "x \<in> P \<inter> P \<longleftrightarrow> x \<in> P"
   891   "x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R"
   892   "{x. x \<in> P} = {y. y \<in> P}"
   893   by (smt2 smt2_sets)+
   894 
   895 end