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