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