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