src/HOL/SMT_Examples/SMT_Examples_Verit.thy
author wenzelm
Fri, 05 Mar 2021 22:23:57 +0100
changeset 73391 f16f209f996c
parent 72908 6a26a955308e
child 74403 dbd69d287ec6
permissions -rw-r--r--
obsolete (see f3378101f555);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72458
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     1
(*  Title:      HOL/SMT_Examples/SMT_Examples_Verit.thy
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     3
    Author:     Mathias Fleury, JKU
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     4
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     5
Half of the examples come from the corresponding file for z3,
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     6
the others come from the Isabelle distribution or the AFP.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     7
*)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     8
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     9
section \<open>Examples for the (smt (verit)) binding\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    10
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    11
theory SMT_Examples_Verit
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    12
imports Complex_Main
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    13
begin
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    14
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    15
external_file \<open>SMT_Examples_Verit.certs\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    16
 
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    17
declare [[smt_certificates = "SMT_Examples_Verit.certs"]]
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    18
declare [[smt_read_only_certificates = true]]
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    19
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    20
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    21
section \<open>Propositional and first-order logic\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    22
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    23
lemma "True" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    24
lemma "p \<or> \<not>p" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    25
lemma "(p \<and> True) = p" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    26
lemma "(p \<or> q) \<and> \<not>p \<Longrightarrow> q" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    27
lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    28
lemma "(p1 \<and> p2) \<or> p3 \<longrightarrow> (p1 \<longrightarrow> (p3 \<and> p2) \<or> (p1 \<and> p3)) \<or> p1" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    29
lemma "P = P = P = P = P = P = P = P = P = P" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    30
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    31
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    32
  assumes "a \<or> b \<or> c \<or> d"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    33
      and "e \<or> f \<or> (a \<and> d)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    34
      and "\<not> (a \<or> (c \<and> ~c)) \<or> b"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    35
      and "\<not> (b \<and> (x \<or> \<not> x)) \<or> c"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    36
      and "\<not> (d \<or> False) \<or> c"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    37
      and "\<not> (c \<or> (\<not> p \<and> (p \<or> (q \<and> \<not> q))))"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    38
  shows False
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    39
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    40
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    41
axiomatization symm_f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    42
  symm_f: "symm_f x y = symm_f y x"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    43
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    44
lemma "a = a \<and> symm_f a b = symm_f b a"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    45
  by (smt (verit) symm_f)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    46
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    47
(*
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    48
Taken from ~~/src/HOL/ex/SAT_Examples.thy.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    49
Translated from TPTP problem library: PUZ015-2.006.dimacs
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    50
*)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    51
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    52
  assumes "~x0"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    53
  and "~x30"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    54
  and "~x29"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    55
  and "~x59"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    56
  and "x1 \<or> x31 \<or> x0"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    57
  and "x2 \<or> x32 \<or> x1"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    58
  and "x3 \<or> x33 \<or> x2"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    59
  and "x4 \<or> x34 \<or> x3"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    60
  and "x35 \<or> x4"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    61
  and "x5 \<or> x36 \<or> x30"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    62
  and "x6 \<or> x37 \<or> x5 \<or> x31"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    63
  and "x7 \<or> x38 \<or> x6 \<or> x32"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    64
  and "x8 \<or> x39 \<or> x7 \<or> x33"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    65
  and "x9 \<or> x40 \<or> x8 \<or> x34"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    66
  and "x41 \<or> x9 \<or> x35"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    67
  and "x10 \<or> x42 \<or> x36"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    68
  and "x11 \<or> x43 \<or> x10 \<or> x37"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    69
  and "x12 \<or> x44 \<or> x11 \<or> x38"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    70
  and "x13 \<or> x45 \<or> x12 \<or> x39"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    71
  and "x14 \<or> x46 \<or> x13 \<or> x40"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    72
  and "x47 \<or> x14 \<or> x41"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    73
  and "x15 \<or> x48 \<or> x42"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    74
  and "x16 \<or> x49 \<or> x15 \<or> x43"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    75
  and "x17 \<or> x50 \<or> x16 \<or> x44"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    76
  and "x18 \<or> x51 \<or> x17 \<or> x45"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    77
  and "x19 \<or> x52 \<or> x18 \<or> x46"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    78
  and "x53 \<or> x19 \<or> x47"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    79
  and "x20 \<or> x54 \<or> x48"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    80
  and "x21 \<or> x55 \<or> x20 \<or> x49"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    81
  and "x22 \<or> x56 \<or> x21 \<or> x50"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    82
  and "x23 \<or> x57 \<or> x22 \<or> x51"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    83
  and "x24 \<or> x58 \<or> x23 \<or> x52"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    84
  and "x59 \<or> x24 \<or> x53"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    85
  and "x25 \<or> x54"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    86
  and "x26 \<or> x25 \<or> x55"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    87
  and "x27 \<or> x26 \<or> x56"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    88
  and "x28 \<or> x27 \<or> x57"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    89
  and "x29 \<or> x28 \<or> x58"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    90
  and "~x1 \<or> ~x31"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    91
  and "~x1 \<or> ~x0"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    92
  and "~x31 \<or> ~x0"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    93
  and "~x2 \<or> ~x32"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    94
  and "~x2 \<or> ~x1"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    95
  and "~x32 \<or> ~x1"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    96
  and "~x3 \<or> ~x33"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    97
  and "~x3 \<or> ~x2"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    98
  and "~x33 \<or> ~x2"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    99
  and "~x4 \<or> ~x34"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   100
  and "~x4 \<or> ~x3"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   101
  and "~x34 \<or> ~x3"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   102
  and "~x35 \<or> ~x4"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   103
  and "~x5 \<or> ~x36"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   104
  and "~x5 \<or> ~x30"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   105
  and "~x36 \<or> ~x30"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   106
  and "~x6 \<or> ~x37"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   107
  and "~x6 \<or> ~x5"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   108
  and "~x6 \<or> ~x31"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   109
  and "~x37 \<or> ~x5"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   110
  and "~x37 \<or> ~x31"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   111
  and "~x5 \<or> ~x31"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   112
  and "~x7 \<or> ~x38"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   113
  and "~x7 \<or> ~x6"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   114
  and "~x7 \<or> ~x32"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   115
  and "~x38 \<or> ~x6"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   116
  and "~x38 \<or> ~x32"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   117
  and "~x6 \<or> ~x32"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   118
  and "~x8 \<or> ~x39"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   119
  and "~x8 \<or> ~x7"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   120
  and "~x8 \<or> ~x33"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   121
  and "~x39 \<or> ~x7"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   122
  and "~x39 \<or> ~x33"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   123
  and "~x7 \<or> ~x33"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   124
  and "~x9 \<or> ~x40"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   125
  and "~x9 \<or> ~x8"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   126
  and "~x9 \<or> ~x34"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   127
  and "~x40 \<or> ~x8"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   128
  and "~x40 \<or> ~x34"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   129
  and "~x8 \<or> ~x34"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   130
  and "~x41 \<or> ~x9"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   131
  and "~x41 \<or> ~x35"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   132
  and "~x9 \<or> ~x35"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   133
  and "~x10 \<or> ~x42"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   134
  and "~x10 \<or> ~x36"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   135
  and "~x42 \<or> ~x36"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   136
  and "~x11 \<or> ~x43"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   137
  and "~x11 \<or> ~x10"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   138
  and "~x11 \<or> ~x37"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   139
  and "~x43 \<or> ~x10"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   140
  and "~x43 \<or> ~x37"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   141
  and "~x10 \<or> ~x37"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   142
  and "~x12 \<or> ~x44"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   143
  and "~x12 \<or> ~x11"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   144
  and "~x12 \<or> ~x38"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   145
  and "~x44 \<or> ~x11"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   146
  and "~x44 \<or> ~x38"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   147
  and "~x11 \<or> ~x38"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   148
  and "~x13 \<or> ~x45"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   149
  and "~x13 \<or> ~x12"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   150
  and "~x13 \<or> ~x39"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   151
  and "~x45 \<or> ~x12"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   152
  and "~x45 \<or> ~x39"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   153
  and "~x12 \<or> ~x39"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   154
  and "~x14 \<or> ~x46"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   155
  and "~x14 \<or> ~x13"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   156
  and "~x14 \<or> ~x40"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   157
  and "~x46 \<or> ~x13"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   158
  and "~x46 \<or> ~x40"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   159
  and "~x13 \<or> ~x40"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   160
  and "~x47 \<or> ~x14"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   161
  and "~x47 \<or> ~x41"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   162
  and "~x14 \<or> ~x41"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   163
  and "~x15 \<or> ~x48"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   164
  and "~x15 \<or> ~x42"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   165
  and "~x48 \<or> ~x42"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   166
  and "~x16 \<or> ~x49"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   167
  and "~x16 \<or> ~x15"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   168
  and "~x16 \<or> ~x43"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   169
  and "~x49 \<or> ~x15"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   170
  and "~x49 \<or> ~x43"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   171
  and "~x15 \<or> ~x43"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   172
  and "~x17 \<or> ~x50"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   173
  and "~x17 \<or> ~x16"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   174
  and "~x17 \<or> ~x44"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   175
  and "~x50 \<or> ~x16"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   176
  and "~x50 \<or> ~x44"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   177
  and "~x16 \<or> ~x44"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   178
  and "~x18 \<or> ~x51"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   179
  and "~x18 \<or> ~x17"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   180
  and "~x18 \<or> ~x45"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   181
  and "~x51 \<or> ~x17"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   182
  and "~x51 \<or> ~x45"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   183
  and "~x17 \<or> ~x45"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   184
  and "~x19 \<or> ~x52"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   185
  and "~x19 \<or> ~x18"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   186
  and "~x19 \<or> ~x46"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   187
  and "~x52 \<or> ~x18"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   188
  and "~x52 \<or> ~x46"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   189
  and "~x18 \<or> ~x46"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   190
  and "~x53 \<or> ~x19"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   191
  and "~x53 \<or> ~x47"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   192
  and "~x19 \<or> ~x47"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   193
  and "~x20 \<or> ~x54"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   194
  and "~x20 \<or> ~x48"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   195
  and "~x54 \<or> ~x48"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   196
  and "~x21 \<or> ~x55"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   197
  and "~x21 \<or> ~x20"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   198
  and "~x21 \<or> ~x49"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   199
  and "~x55 \<or> ~x20"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   200
  and "~x55 \<or> ~x49"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   201
  and "~x20 \<or> ~x49"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   202
  and "~x22 \<or> ~x56"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   203
  and "~x22 \<or> ~x21"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   204
  and "~x22 \<or> ~x50"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   205
  and "~x56 \<or> ~x21"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   206
  and "~x56 \<or> ~x50"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   207
  and "~x21 \<or> ~x50"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   208
  and "~x23 \<or> ~x57"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   209
  and "~x23 \<or> ~x22"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   210
  and "~x23 \<or> ~x51"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   211
  and "~x57 \<or> ~x22"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   212
  and "~x57 \<or> ~x51"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   213
  and "~x22 \<or> ~x51"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   214
  and "~x24 \<or> ~x58"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   215
  and "~x24 \<or> ~x23"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   216
  and "~x24 \<or> ~x52"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   217
  and "~x58 \<or> ~x23"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   218
  and "~x58 \<or> ~x52"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   219
  and "~x23 \<or> ~x52"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   220
  and "~x59 \<or> ~x24"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   221
  and "~x59 \<or> ~x53"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   222
  and "~x24 \<or> ~x53"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   223
  and "~x25 \<or> ~x54"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   224
  and "~x26 \<or> ~x25"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   225
  and "~x26 \<or> ~x55"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   226
  and "~x25 \<or> ~x55"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   227
  and "~x27 \<or> ~x26"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   228
  and "~x27 \<or> ~x56"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   229
  and "~x26 \<or> ~x56"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   230
  and "~x28 \<or> ~x27"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   231
  and "~x28 \<or> ~x57"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   232
  and "~x27 \<or> ~x57"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   233
  and "~x29 \<or> ~x28"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   234
  and "~x29 \<or> ~x58"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   235
  and "~x28 \<or> ~x58"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   236
shows False
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   237
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   238
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   239
lemma "\<forall>x::int. P x \<longrightarrow> (\<forall>y::int. P x \<or> P y)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   240
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   241
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   242
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   243
  assumes "(\<forall>x y. P x y = x)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   244
  shows "(\<exists>y. P x y) = P x c"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   245
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   246
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   247
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   248
  assumes "(\<forall>x y. P x y = x)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   249
  and "(\<forall>x. \<exists>y. P x y) = (\<forall>x. P x c)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   250
  shows "(\<exists>y. P x y) = P x c"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   251
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   252
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   253
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   254
  assumes "if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   255
  shows "P x \<longrightarrow> P y"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   256
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   257
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   258
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   259
section \<open>Arithmetic\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   260
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   261
subsection \<open>Linear arithmetic over integers and reals\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   262
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   263
lemma "(3::int) = 3" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   264
lemma "(3::real) = 3" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   265
lemma "(3 :: int) + 1 = 4" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   266
lemma "x + (y + z) = y + (z + (x::int))" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   267
lemma "max (3::int) 8 > 5" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   268
lemma "\<bar>x :: real\<bar> + \<bar>y\<bar> \<ge> \<bar>x + y\<bar>" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   269
lemma "P ((2::int) < 3) = P True" supply[[smt_trace]] by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   270
lemma "x + 3 \<ge> 4 \<or> x < (1::int)" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   271
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   272
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   273
  assumes "x \<ge> (3::int)" and "y = x + 4"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   274
  shows "y - x > 0"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   275
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   276
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   277
lemma "let x = (2 :: int) in x + x \<noteq> 5" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   278
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   279
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   280
  fixes x :: int
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   281
  assumes "3 * x + 7 * a < 4" and "3 < 2 * x"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   282
  shows "a < 0"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   283
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   284
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   285
lemma "(0 \<le> y + -1 * x \<or> \<not> 0 \<le> x \<or> 0 \<le> (x::int)) = (\<not> False)" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   286
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   287
lemma "
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   288
  (n < m \<and> m < n') \<or> (n < m \<and> m = n') \<or> (n < n' \<and> n' < m) \<or>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   289
  (n = n' \<and> n' < m) \<or> (n = m \<and> m < n') \<or>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   290
  (n' < m \<and> m < n) \<or> (n' < m \<and> m = n) \<or>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   291
  (n' < n \<and> n < m) \<or> (n' = n \<and> n < m) \<or> (n' = m \<and> m < n) \<or>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   292
  (m < n \<and> n < n') \<or> (m < n \<and> n' = n) \<or> (m < n' \<and> n' < n) \<or>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   293
  (m = n \<and> n < n') \<or> (m = n' \<and> n' < n) \<or>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   294
  (n' = m \<and> m = (n::int))"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   295
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   296
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   297
text\<open>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   298
The following example was taken from HOL/ex/PresburgerEx.thy, where it says:
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   299
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   300
  This following theorem proves that all solutions to the
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   301
  recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   302
  period 9.  The example was brought to our attention by John
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   303
  Harrison. It does does not require Presburger arithmetic but merely
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   304
  quantifier-free linear arithmetic and holds for the rationals as well.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   305
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   306
  Warning: it takes (in 2006) over 4.2 minutes!
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   307
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   308
There, it is proved by "arith". (smt (verit)) is able to prove this within a fraction
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   309
of one second. With proof reconstruction, it takes about 13 seconds on a Core2
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   310
processor.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   311
\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   312
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   313
lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   314
         x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   315
         x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   316
 \<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   317
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   318
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   319
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   320
lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   321
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   322
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   323
subsection \<open>Linear arithmetic with quantifiers\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   324
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   325
lemma "~ (\<exists>x::int. False)" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   326
lemma "~ (\<exists>x::real. False)" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   327
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   328
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   329
lemma "\<forall>x y::int. (x = 0 \<and> y = 1) \<longrightarrow> x \<noteq> y" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   330
lemma "\<forall>x y::int. x < y \<longrightarrow> (2 * x + 1) < (2 * y)" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   331
lemma "\<forall>x y::int. x + y > 2 \<or> x + y = 2 \<or> x + y < 2" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   332
lemma "\<forall>x::int. if x > 0 then x + 1 > 0 else 1 > x" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   333
lemma "(if (\<forall>x::int. x < 0 \<or> x > 0) then -1 else 3) > (0::int)" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   334
lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   335
lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   336
lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   337
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   338
subsection \<open>Linear arithmetic for natural numbers\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   339
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   340
declare [[smt_nat_as_int]]
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   341
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   342
lemma "2 * (x::nat) \<noteq> 1" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   343
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   344
lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   345
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   346
lemma "let x = (1::nat) + y in x - y > 0 * x" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   347
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   348
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   349
  "let x = (1::nat) + y in
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   350
   let P = (if x > 0 then True else False) in
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   351
   False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   352
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   353
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   354
lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by (smt (verit) int_nat_eq)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   355
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   356
definition prime_nat :: "nat \<Rightarrow> bool" where
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   357
  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   358
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   359
lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)" by (smt (verit) prime_nat_def)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   360
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   361
lemma "2 * (x::nat) \<noteq> 1" 
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   362
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   363
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   364
lemma \<open>2*(x :: int) \<noteq> 1\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   365
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   366
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   367
declare [[smt_nat_as_int = false]]
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   368
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   369
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   370
section \<open>Pairs\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   371
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   372
lemma "fst (x, y) = a \<Longrightarrow> x = a"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   373
  using fst_conv by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   374
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   375
lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   376
  using fst_conv snd_conv by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   377
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   378
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   379
section \<open>Higher-order problems and recursion\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   380
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   381
lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> (f (i1 := v1, i2 := v2)) i = f i"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   382
  using fun_upd_same fun_upd_apply by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   383
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   384
lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   385
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   386
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   387
lemma "id x = x \<and> id True = True"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   388
  by (smt (verit) id_def)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   389
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   390
lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   391
  using fun_upd_same fun_upd_apply by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   392
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   393
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   394
  "f (\<exists>x. g x) \<Longrightarrow> True"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   395
  "f (\<forall>x. g x) \<Longrightarrow> True"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   396
  by (smt (verit))+
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   397
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   398
lemma True using let_rsp by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   399
lemma "le = (\<le>) \<Longrightarrow> le (3::int) 42" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   400
lemma "map (\<lambda>i::int. i + 1) [0, 1] = [1, 2]" by (smt (verit) list.map)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   401
lemma "(\<forall>x. P x) \<or> \<not> All P" by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   402
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   403
fun dec_10 :: "int \<Rightarrow> int" where
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   404
  "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   405
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   406
lemma "dec_10 (4 * dec_10 4) = 6" by (smt (verit) dec_10.simps)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   407
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   408
context complete_lattice
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   409
begin
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   410
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   411
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   412
  assumes "Sup {a | i::bool. True} \<le> Sup {b | i::bool. True}"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   413
  and "Sup {b | i::bool. True} \<le> Sup {a | i::bool. True}"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   414
  shows "Sup {a | i::bool. True} \<le> Sup {a | i::bool. True}"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   415
  using assms by (smt (verit) order_trans)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   416
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   417
end
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   418
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   419
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   420
 "eq_set (List.coset xs) (set ys) = rhs"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   421
    if "\<And>ys. subset' (List.coset xs) (set ys) = (let n = card (UNIV::'a set) in 0 < n \<and> card (set (xs @ ys)) = n)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   422
      and "\<And>uu A. (uu::'a) \<in> - A \<Longrightarrow> uu \<notin> A"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   423
      and "\<And>uu. card (set (uu::'a list)) = length (remdups uu)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   424
      and "\<And>uu. finite (set (uu::'a list))"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   425
      and "\<And>uu. (uu::'a) \<in> UNIV"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   426
      and "(UNIV::'a set) \<noteq> {}"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   427
      and "\<And>c A B P. \<lbrakk>(c::'a) \<in> A \<union> B; c \<in> A \<Longrightarrow> P; c \<in> B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   428
      and "\<And>a b. (a::nat) + b = b + a"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   429
      and "\<And>a b. ((a::nat) = a + b) = (b = 0)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   430
      and "card' (set xs) = length (remdups xs)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   431
      and "card' = (card :: 'a set \<Rightarrow> nat)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   432
      and "\<And>A B. \<lbrakk>finite (A::'a set); finite B\<rbrakk> \<Longrightarrow> card A + card B = card (A \<union> B) + card (A \<inter> B)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   433
      and "\<And>A. (card (A::'a set) = 0) = (A = {} \<or> infinite A)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   434
      and "\<And>A. \<lbrakk>finite (UNIV::'a set); card (A::'a set) = card (UNIV::'a set)\<rbrakk> \<Longrightarrow> A = UNIV"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   435
      and "\<And>xs. - List.coset (xs::'a list) = set xs"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   436
      and "\<And>xs. - set (xs::'a list) = List.coset xs"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   437
      and "\<And>A B. (A \<inter> B = {}) = (\<forall>x. (x::'a) \<in> A \<longrightarrow> x \<notin> B)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   438
      and "eq_set = (=)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   439
      and "\<And>A. finite (A::'a set) \<Longrightarrow> finite (- A) = finite (UNIV::'a set)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   440
      and "rhs \<equiv> let n = card (UNIV::'a set) in if n = 0 then False else let xs' = remdups xs; ys' = remdups ys in length xs' + length ys' = n \<and> (\<forall>x\<in>set xs'. x \<notin> set ys') \<and> (\<forall>y\<in>set ys'. y \<notin> set xs')"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   441
      and "\<And>xs ys. set ((xs::'a list) @ ys) = set xs \<union> set ys"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   442
      and "\<And>A B. ((A::'a set) = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   443
      and "\<And>xs. set (remdups (xs::'a list)) = set xs"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   444
      and "subset' = (\<subseteq>)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   445
      and "\<And>A B. (\<And>x. (x::'a) \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   446
      and "\<And>A B. \<lbrakk>(A::'a set) \<subseteq> B; B \<subseteq> A\<rbrakk> \<Longrightarrow> A = B"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   447
      and "\<And>A ys. (A \<subseteq> List.coset ys) = (\<forall>y\<in>set ys. (y::'a) \<notin> A)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   448
  using that by (smt (verit, default))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   449
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   450
notepad
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   451
begin
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   452
  have "line_integral F {i, j} g = line_integral F {i} g + line_integral F {j} g"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   453
    if \<open>(k, g) \<in> one_chain_typeI\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   454
      \<open>\<And>A b B. ({} = (A::(real \<times> real) set) \<inter> insert (b::real \<times> real) (B::(real \<times> real) set)) = (b \<notin> A \<and> {} = A \<inter> B)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   455
      \<open>finite ({} :: (real \<times> real) set)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   456
      \<open>\<And>a A. finite (A::(real \<times> real) set) \<Longrightarrow> finite (insert (a::real \<times> real) A)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   457
      \<open>(i::real \<times> real) = (1::real, 0::real)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   458
      \<open> \<And>a A. (a::real \<times> real) \<in> (A::(real \<times> real) set) \<Longrightarrow> insert a A = A\<close> \<open>j = (0, 1)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   459
      \<open>\<And>x. (x::(real \<times> real) set) \<inter> {} = {}\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   460
      \<open>\<And>y x A. insert (x::real \<times> real) (insert (y::real \<times> real) (A::(real \<times> real) set)) =  insert y (insert x A)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   461
      \<open>\<And>a A. insert (a::real \<times> real) (A::(real \<times> real) set) = {a} \<union> A\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   462
      \<open>\<And>F u basis2 basis1 \<gamma>. finite (u :: (real \<times> real) set) \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   463
    line_integral_exists F basis1 \<gamma> \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   464
    line_integral_exists F basis2 \<gamma> \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   465
    basis1 \<union> basis2 = u \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   466
    basis1 \<inter> basis2 = {} \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   467
    line_integral F u \<gamma> = line_integral F basis1 \<gamma> + line_integral F basis2 \<gamma>\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   468
      \<open>one_chain_line_integral F {i} one_chain_typeI =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   469
    one_chain_line_integral F {i} one_chain_typeII \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   470
    (\<forall>(k, \<gamma>)\<in>one_chain_typeI. line_integral_exists F {i} \<gamma>) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   471
    (\<forall>(k, \<gamma>)\<in>one_chain_typeII. line_integral_exists F {i} \<gamma>)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   472
      \<open> one_chain_line_integral (F::real \<times> real \<Rightarrow> real \<times> real) {j::real \<times> real}
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   473
     (one_chain_typeII::(int \<times> (real \<Rightarrow> real \<times> real)) set) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   474
    one_chain_line_integral F {j} (one_chain_typeI::(int \<times> (real \<Rightarrow> real \<times> real)) set) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   475
    (\<forall>(k::int, \<gamma>::real \<Rightarrow> real \<times> real)\<in>one_chain_typeII. line_integral_exists F {j} \<gamma>) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   476
    (\<forall>(k::int, \<gamma>::real \<Rightarrow> real \<times> real)\<in>one_chain_typeI. line_integral_exists F {j} \<gamma>)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   477
    for F i j g one_chain_typeI one_chain_typeII and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   478
      line_integral :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (real \<Rightarrow> real \<times> real) \<Rightarrow> real\<close> and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   479
      line_integral_exists :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (real \<Rightarrow> real \<times> real) \<Rightarrow> bool\<close> and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   480
      one_chain_line_integral :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (int \<times> (real \<Rightarrow> real \<times> real)) set \<Rightarrow> real\<close> and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   481
      k
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   482
    using prod.case_eq_if singleton_inject snd_conv
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   483
      that
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   484
    by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   485
end
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   486
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   487
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   488
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   489
  fixes x y z :: real
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   490
  assumes \<open>x + 2 * y > 0\<close> and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   491
    \<open>x - 2 * y > 0\<close> and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   492
    \<open>x < 0\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   493
  shows False
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   494
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   495
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   496
(*test for arith reconstruction*)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   497
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   498
  fixes d :: real
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   499
  assumes \<open>0 < d\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   500
   \<open>diamond_y \<equiv> \<lambda>t. d / 2 - \<bar>t\<bar>\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   501
   \<open>\<And>a b c :: real. (a / c < b / c) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   502
    ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   503
   \<open>\<And>a b c :: real. (a / c < b / c) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   504
    ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   505
   \<open>\<And>a b :: real. - a / b = - (a / b)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   506
   \<open>\<And>a b :: real. - a * b = - (a * b)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   507
   \<open>\<And>(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 \<and> x2 = y2)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   508
 shows \<open>(\<lambda>y. (d / 2, (2 * y - 1) * diamond_y (d / 2))) \<noteq>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   509
    (\<lambda>x. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   510
    (\<lambda>y. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   511
    (\<lambda>x. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   512
    False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   513
  using assms
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   514
  by (smt (verit,del_insts))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   515
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   516
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   517
  fixes d :: real
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   518
  assumes \<open>0 < d\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   519
   \<open>diamond_y \<equiv> \<lambda>t. d / 2 - \<bar>t\<bar>\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   520
   \<open>\<And>a b c :: real. (a / c < b / c) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   521
    ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   522
   \<open>\<And>a b c :: real. (a / c < b / c) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   523
    ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   524
   \<open>\<And>a b :: real. - a / b = - (a / b)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   525
   \<open>\<And>a b :: real. - a * b = - (a * b)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   526
   \<open>\<And>(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 \<and> x2 = y2)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   527
 shows \<open>(\<lambda>y. (d / 2, (2 * y - 1) * diamond_y (d / 2))) \<noteq>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   528
    (\<lambda>x. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   529
    (\<lambda>y. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   530
    (\<lambda>x. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   531
    False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   532
  using assms
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   533
  by (smt (verit,ccfv_threshold))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   534
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   535
(*qnt_rm_unused example*)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   536
lemma 
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   537
  assumes \<open>\<forall>z y x. P z y\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   538
    \<open>P z y \<Longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   539
  shows False
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   540
  using assms
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   541
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   542
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   543
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   544
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   545
  "max (x::int) y \<ge> y"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   546
  supply [[smt_trace]]
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   547
  by (smt (verit))+
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   548
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   549
context
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   550
begin
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   551
abbreviation finite' :: "'a set \<Rightarrow> bool"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   552
  where "finite' A \<equiv> finite A \<and> A \<noteq> {}"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   553
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   554
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   555
  fixes f :: "'b \<Rightarrow> 'c :: linorder"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   556
  assumes
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   557
    \<open>\<forall>(S::'b::type set) f::'b::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   558
    \<open>\<forall>(S::'a::type set) f::'a::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   559
    \<open>\<forall>(S::'b::type set) (y::'b::type) f::'b::type \<Rightarrow> 'c::linorder.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   560
       finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   561
    \<open>\<forall>(S::'a::type set) (y::'a::type) f::'a::type \<Rightarrow> 'c::linorder.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   562
       finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   563
    \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (g::'a::type \<Rightarrow> 'b::type) x::'a::type. (f \<circ> g) x = f (g x)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   564
    \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   565
    \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   566
    \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   567
    \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   568
    \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) A::'b::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   569
       b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   570
    \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) A::'b::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   571
       b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   572
    \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) A::'a::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   573
       b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   574
    \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) A::'a::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   575
       b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   576
    \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   577
    \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   578
    \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   579
    \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   580
    \<open>\<forall>(f::'b::type \<Rightarrow> 'a::type) A::'b::type set. (f ` A = {}) = (A = {})  \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   581
    \<open>\<forall>(f::'b::type \<Rightarrow> 'b::type) A::'b::type set. (f ` A = {}) = (A = {})  \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   582
    \<open>\<forall>(f::'a::type \<Rightarrow> 'b::type) A::'a::type set. (f ` A = {}) = (A = {})  \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   583
    \<open>\<forall>(f::'a::type \<Rightarrow> 'a::type) A::'a::type set. (f ` A = {}) = (A = {})  \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   584
    \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   585
       inj_on f A \<and> f x = f y \<and> x \<in> A \<and> y \<in> A \<longrightarrow> x = y\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   586
    \<open>\<forall>(x::'c::linorder) y::'c::linorder. (x < y) = (x \<le> y \<and> x \<noteq> y)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   587
    \<open>inj_on (f::'b::type \<Rightarrow> 'c::linorder) ((g::'a::type \<Rightarrow> 'b::type) ` (B::'a::type set))\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   588
    \<open>finite (B::'a::type set)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   589
    \<open>(B::'a::type set) \<noteq> {}\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   590
    \<open>arg_min_on ((f::'b::type \<Rightarrow> 'c::linorder) \<circ> (g::'a::type \<Rightarrow> 'b::type)) (B::'a::type set) \<in> B\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   591
    \<open>\<nexists>x::'a::type.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   592
       x \<in> (B::'a::type set) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   593
       ((f::'b::type \<Rightarrow> 'c::linorder) \<circ> (g::'a::type \<Rightarrow> 'b::type)) x < (f \<circ> g) (arg_min_on (f \<circ> g) B)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   594
    \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (P::'b::type \<Rightarrow> bool) a::'b::type.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   595
       inj_on f (Collect P) \<and> P a \<and> (\<forall>y::'b::type. P y \<longrightarrow> f a \<le> f y) \<longrightarrow> arg_min f P = a\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   596
    \<open>\<forall>(S::'b::type set) f::'b::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   597
    \<open>\<forall>(S::'a::type set) f::'a::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   598
    \<open>\<forall>(S::'b::type set) (y::'b::type) f::'b::type \<Rightarrow> 'c::linorder.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   599
       finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   600
    \<open>\<forall>(S::'a::type set) (y::'a::type) f::'a::type \<Rightarrow> 'c::linorder.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   601
       finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   602
    \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (g::'a::type \<Rightarrow> 'b::type) x::'a::type. (f \<circ> g) x = f (g x)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   603
    \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   604
    \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   605
    \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   606
    \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   607
    \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) A::'b::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   608
       b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   609
    \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) A::'b::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   610
       b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   611
    \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) A::'a::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   612
       b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   613
    \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) A::'a::type set.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   614
       b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   615
    \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   616
    \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   617
    \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   618
    \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   619
    \<open>\<forall>(f::'b::type \<Rightarrow> 'a::type) A::'b::type set. (f ` A = {}) = (A = {})      \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   620
    \<open>\<forall>(f::'b::type \<Rightarrow> 'b::type) A::'b::type set. (f ` A = {}) = (A = {})      \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   621
    \<open>\<forall>(f::'a::type \<Rightarrow> 'b::type) A::'a::type set. (f ` A = {}) = (A = {})      \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   622
    \<open>\<forall>(f::'a::type \<Rightarrow> 'a::type) A::'a::type set. (f ` A = {}) = (A = {})\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   623
    \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   624
       inj_on f A \<and> f x = f y \<and> x \<in> A \<and> y \<in> A \<longrightarrow> x = y\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   625
    \<open>\<forall>(x::'c::linorder) y::'c::linorder. (x < y) = (x \<le> y \<and> x \<noteq> y)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   626
    \<open>arg_min_on (f::'b::type \<Rightarrow> 'c::linorder) ((g::'a::type \<Rightarrow> 'b::type) ` (B::'a::type set)) \<noteq>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   627
       g (arg_min_on (f \<circ> g) B) \<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   628
   shows False
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   629
  using assms
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   630
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   631
end
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   632
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   633
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   634
experiment
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   635
begin
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   636
private datatype abort =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   637
    Rtype_error
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   638
  | Rtimeout_error
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   639
private datatype ('a) error_result =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   640
  Rraise " 'a " \<comment> \<open>\<open> Should only be a value of type exn \<close>\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   641
  | Rabort " abort "
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   642
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   643
private datatype( 'a, 'b) result =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   644
    Rval " 'a "
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   645
    | Rerr " ('b) error_result "
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   646
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   647
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   648
  fixes clock :: \<open>'astate \<Rightarrow> nat\<close> and
72908
6a26a955308e improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents: 72458
diff changeset
   649
    fun_evaluate_match :: \<open>'astate \<Rightarrow> 'vsemv_env \<Rightarrow> _ \<Rightarrow> ('pat \<times> 'exp0) list \<Rightarrow> _ \<Rightarrow>
72458
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   650
      'astate*((('v)list),('v))result\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   651
  assumes
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   652
         " fix_clock (st::'astate) (fun_evaluate st (env::'vsemv_env) [e::'exp0]) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   653
       (st'::'astate, r::('v list, 'v) result)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   654
      " clock (fst (fun_evaluate (st::'astate) (env::'vsemv_env) [e::'exp0])) \<le> clock st"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   655
       "\<forall>(b::nat) (a::nat) c::nat. b \<le> a \<and> c \<le> b \<longrightarrow> c \<le> a"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   656
       "\<forall>(a::'astate) p::'astate \<times> ('v list, 'v) result. (a = fst p) = (\<exists>b::('v list, 'v) result. p = (a, b))"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   657
       "\<forall>y::'v error_result. (\<forall>x1::'v. y = Rraise x1 \<longrightarrow> False) \<and> (\<forall>x2::abort. y = Rabort x2 \<longrightarrow> False) \<longrightarrow> False"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   658
       "\<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x1::'v.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   659
          (case Rraise x1 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f1 x1"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   660
      " \<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x2::abort.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   661
          (case Rabort x2 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f2 x2"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   662
       "\<forall>(s1::'astate) (s2::'astate) (x::('v list, 'v) result) s::'astate.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   663
          fix_clock s1 (s2, x) = (s, x) \<longrightarrow> clock s \<le> clock s2"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   664
       "\<forall>(s::'astate) (s'::'astate) res::('v list, 'v) result.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   665
          fix_clock s (s', res) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   666
          (update_clock (\<lambda>_::nat. if clock s' \<le> clock s then clock s' else clock s) s', res)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   667
       "\<forall>(x2::'v error_result) x1::'v.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   668
          (r::('v list, 'v) result) = Rerr x2 \<and> x2 = Rraise x1 \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   669
          clock (fst (fun_evaluate_match (st'::'astate) (env::'vsemv_env) x1 (pes::('pat \<times> 'exp0) list) x1))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   670
          \<le> clock st'"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   671
     shows "((r::('v list, 'v) result) = Rerr (x2::'v error_result) \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   672
           clock
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   673
            (fst (case x2 of
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   674
                  Rraise (v2::'v) \<Rightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   675
                    fun_evaluate_match (st'::'astate) (env::'vsemv_env) v2 (pes::('pat \<times> 'exp0) list) v2
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   676
                  | Rabort (abort::abort) \<Rightarrow> (st', Rerr (Rabort abort))))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   677
           \<le> clock (st::'astate)) "
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   678
  using assms by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   679
end
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   680
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   681
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   682
context
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   683
  fixes piecewise_C1 :: "('real :: {one,zero,ord} \<Rightarrow> 'a :: {one,zero,ord}) \<Rightarrow> 'real set \<Rightarrow> bool"  and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   684
     joinpaths :: "('real \<Rightarrow> 'a) \<Rightarrow> ('real \<Rightarrow> 'a) \<Rightarrow> 'real \<Rightarrow> 'a"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   685
begin
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   686
notation piecewise_C1 (infixr "piecewise'_C1'_differentiable'_on" 50)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   687
notation joinpaths (infixr "+++" 75)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   688
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   689
lemma
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   690
   \<open>(\<And>v1. \<forall>v0. (rec_join v0 = v1 \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   691
               (v0 = [] \<and> (\<lambda>uu. 0) = v1 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   692
               (\<forall>v2. v0 = [v2] \<and> v1 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   693
               (\<forall>v2 v3 v4.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   694
                   v0 = v2 # v3 # v4 \<and> v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow> False) \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   695
               False) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   696
              (rec_join v0 = rec_join v0 \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   697
               (v0 = [] \<and> (\<lambda>uu. 0) = rec_join v0 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   698
               (\<forall>v2. v0 = [v2] \<and> rec_join v0 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   699
               (\<forall>v2 v3 v4.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   700
                   v0 = v2 # v3 # v4 \<and> rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   701
                   False) \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   702
               False)) \<Longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   703
         (\<forall>v0 v1.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   704
             rec_join v0 = v1 \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   705
             (v0 = [] \<and> (\<lambda>uu. 0) = v1 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   706
             (\<forall>v2. v0 = [v2] \<and> v1 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   707
             (\<forall>v2 v3 v4. v0 = v2 # v3 # v4 \<and> v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow> False) \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   708
             False) =
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   709
         (\<forall>v0. rec_join v0 = rec_join v0 \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   710
               (v0 = [] \<and> (\<lambda>uu. 0) = rec_join v0 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   711
               (\<forall>v2. v0 = [v2] \<and> rec_join v0 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   712
               (\<forall>v2 v3 v4.
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   713
                   v0 = v2 # v3 # v4 \<and> rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   714
                   False) \<longrightarrow>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   715
               False)\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   716
  by (smt (verit))
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   717
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   718
end
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   719
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   720
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   721
section \<open>Monomorphization examples\<close>
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   722
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   723
definition Pred :: "'a \<Rightarrow> bool" where
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   724
  "Pred x = True"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   725
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   726
lemma poly_Pred: "Pred x \<and> (Pred [x] \<or> \<not> Pred [x])"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   727
  by (simp add: Pred_def)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   728
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   729
lemma "Pred (1::int)"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   730
  by (smt (verit) poly_Pred)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   731
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   732
axiomatization g :: "'a \<Rightarrow> nat"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   733
axiomatization where
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   734
  g1: "g (Some x) = g [x]" and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   735
  g2: "g None = g []" and
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   736
  g3: "g xs = length xs"
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   737
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   738
lemma "g (Some (3::int)) = g (Some True)" by (smt (verit) g1 g2 g3 list.size)
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   739
b44e894796d5 add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   740
end