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