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