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