Theory SMT_Examples_Verit

(*  Title:      HOL/SMT_Examples/SMT_Examples_Verit.thy
    Author:     Sascha Boehme, TU Muenchen
    Author:     Mathias Fleury, JKU

Half of the examples come from the corresponding file for z3,
the others come from the Isabelle distribution or the AFP.
*)

section ‹Examples for the (smt (verit)) binding›

theory SMT_Examples_Verit
imports Complex_Main
begin

external_file ‹SMT_Examples_Verit.certs›

declare [[smt_certificates = "SMT_Examples_Verit.certs"]]
declare [[smt_read_only_certificates = true]]


section ‹Propositional and first-order logic›

lemma "True" by (smt (verit))
lemma "p  ¬p" by (smt (verit))
lemma "(p  True) = p" by (smt (verit))
lemma "(p  q)  ¬p  q" by (smt (verit))
lemma "(a  b)  (c  d)  (a  b)  (c  d)" by (smt (verit))
lemma "(p1  p2)  p3  (p1  (p3  p2)  (p1  p3))  p1" by (smt (verit))
lemma "P = P = P = P = P = P = P = P = P = P" by (smt (verit))

lemma
  assumes "a  b  c  d"
      and "e  f  (a  d)"
      and "¬ (a  (c  ~c))  b"
      and "¬ (b  (x  ¬ x))  c"
      and "¬ (d  False)  c"
      and "¬ (c  (¬ p  (p  (q  ¬ q))))"
  shows False
  using assms by (smt (verit))

axiomatization symm_f :: "'a  'a  'a" where
  symm_f: "symm_f x y = symm_f y x"

lemma "a = a  symm_f a b = symm_f b a"
  by (smt (verit) symm_f)

(*
Taken from ~~/src/HOL/ex/SAT_Examples.thy.
Translated from TPTP problem library: PUZ015-2.006.dimacs
*)
lemma
  assumes "~x0"
  and "~x30"
  and "~x29"
  and "~x59"
  and "x1  x31  x0"
  and "x2  x32  x1"
  and "x3  x33  x2"
  and "x4  x34  x3"
  and "x35  x4"
  and "x5  x36  x30"
  and "x6  x37  x5  x31"
  and "x7  x38  x6  x32"
  and "x8  x39  x7  x33"
  and "x9  x40  x8  x34"
  and "x41  x9  x35"
  and "x10  x42  x36"
  and "x11  x43  x10  x37"
  and "x12  x44  x11  x38"
  and "x13  x45  x12  x39"
  and "x14  x46  x13  x40"
  and "x47  x14  x41"
  and "x15  x48  x42"
  and "x16  x49  x15  x43"
  and "x17  x50  x16  x44"
  and "x18  x51  x17  x45"
  and "x19  x52  x18  x46"
  and "x53  x19  x47"
  and "x20  x54  x48"
  and "x21  x55  x20  x49"
  and "x22  x56  x21  x50"
  and "x23  x57  x22  x51"
  and "x24  x58  x23  x52"
  and "x59  x24  x53"
  and "x25  x54"
  and "x26  x25  x55"
  and "x27  x26  x56"
  and "x28  x27  x57"
  and "x29  x28  x58"
  and "~x1  ~x31"
  and "~x1  ~x0"
  and "~x31  ~x0"
  and "~x2  ~x32"
  and "~x2  ~x1"
  and "~x32  ~x1"
  and "~x3  ~x33"
  and "~x3  ~x2"
  and "~x33  ~x2"
  and "~x4  ~x34"
  and "~x4  ~x3"
  and "~x34  ~x3"
  and "~x35  ~x4"
  and "~x5  ~x36"
  and "~x5  ~x30"
  and "~x36  ~x30"
  and "~x6  ~x37"
  and "~x6  ~x5"
  and "~x6  ~x31"
  and "~x37  ~x5"
  and "~x37  ~x31"
  and "~x5  ~x31"
  and "~x7  ~x38"
  and "~x7  ~x6"
  and "~x7  ~x32"
  and "~x38  ~x6"
  and "~x38  ~x32"
  and "~x6  ~x32"
  and "~x8  ~x39"
  and "~x8  ~x7"
  and "~x8  ~x33"
  and "~x39  ~x7"
  and "~x39  ~x33"
  and "~x7  ~x33"
  and "~x9  ~x40"
  and "~x9  ~x8"
  and "~x9  ~x34"
  and "~x40  ~x8"
  and "~x40  ~x34"
  and "~x8  ~x34"
  and "~x41  ~x9"
  and "~x41  ~x35"
  and "~x9  ~x35"
  and "~x10  ~x42"
  and "~x10  ~x36"
  and "~x42  ~x36"
  and "~x11  ~x43"
  and "~x11  ~x10"
  and "~x11  ~x37"
  and "~x43  ~x10"
  and "~x43  ~x37"
  and "~x10  ~x37"
  and "~x12  ~x44"
  and "~x12  ~x11"
  and "~x12  ~x38"
  and "~x44  ~x11"
  and "~x44  ~x38"
  and "~x11  ~x38"
  and "~x13  ~x45"
  and "~x13  ~x12"
  and "~x13  ~x39"
  and "~x45  ~x12"
  and "~x45  ~x39"
  and "~x12  ~x39"
  and "~x14  ~x46"
  and "~x14  ~x13"
  and "~x14  ~x40"
  and "~x46  ~x13"
  and "~x46  ~x40"
  and "~x13  ~x40"
  and "~x47  ~x14"
  and "~x47  ~x41"
  and "~x14  ~x41"
  and "~x15  ~x48"
  and "~x15  ~x42"
  and "~x48  ~x42"
  and "~x16  ~x49"
  and "~x16  ~x15"
  and "~x16  ~x43"
  and "~x49  ~x15"
  and "~x49  ~x43"
  and "~x15  ~x43"
  and "~x17  ~x50"
  and "~x17  ~x16"
  and "~x17  ~x44"
  and "~x50  ~x16"
  and "~x50  ~x44"
  and "~x16  ~x44"
  and "~x18  ~x51"
  and "~x18  ~x17"
  and "~x18  ~x45"
  and "~x51  ~x17"
  and "~x51  ~x45"
  and "~x17  ~x45"
  and "~x19  ~x52"
  and "~x19  ~x18"
  and "~x19  ~x46"
  and "~x52  ~x18"
  and "~x52  ~x46"
  and "~x18  ~x46"
  and "~x53  ~x19"
  and "~x53  ~x47"
  and "~x19  ~x47"
  and "~x20  ~x54"
  and "~x20  ~x48"
  and "~x54  ~x48"
  and "~x21  ~x55"
  and "~x21  ~x20"
  and "~x21  ~x49"
  and "~x55  ~x20"
  and "~x55  ~x49"
  and "~x20  ~x49"
  and "~x22  ~x56"
  and "~x22  ~x21"
  and "~x22  ~x50"
  and "~x56  ~x21"
  and "~x56  ~x50"
  and "~x21  ~x50"
  and "~x23  ~x57"
  and "~x23  ~x22"
  and "~x23  ~x51"
  and "~x57  ~x22"
  and "~x57  ~x51"
  and "~x22  ~x51"
  and "~x24  ~x58"
  and "~x24  ~x23"
  and "~x24  ~x52"
  and "~x58  ~x23"
  and "~x58  ~x52"
  and "~x23  ~x52"
  and "~x59  ~x24"
  and "~x59  ~x53"
  and "~x24  ~x53"
  and "~x25  ~x54"
  and "~x26  ~x25"
  and "~x26  ~x55"
  and "~x25  ~x55"
  and "~x27  ~x26"
  and "~x27  ~x56"
  and "~x26  ~x56"
  and "~x28  ~x27"
  and "~x28  ~x57"
  and "~x27  ~x57"
  and "~x29  ~x28"
  and "~x29  ~x58"
  and "~x28  ~x58"
shows False
  using assms by (smt (verit))

lemma "x::int. P x  (y::int. P x  P y)"
  by (smt (verit))

lemma
  assumes "(x y. P x y = x)"
  shows "(y. P x y) = P x c"
  using assms by (smt (verit))

lemma
  assumes "(x y. P x y = x)"
  and "(x. y. P x y) = (x. P x c)"
  shows "(y. P x y) = P x c"
  using assms by (smt (verit))

lemma
  assumes "if P x then ¬(y. P y) else (y. ¬P y)"
  shows "P x  P y"
  using assms by (smt (verit))


section ‹Arithmetic›

subsection ‹Linear arithmetic over integers and reals›

lemma "(3::int) = 3" by (smt (verit))
lemma "(3::real) = 3" by (smt (verit))
lemma "(3 :: int) + 1 = 4" by (smt (verit))
lemma "x + (y + z) = y + (z + (x::int))" by (smt (verit))
lemma "max (3::int) 8 > 5" by (smt (verit))
lemma "¦x :: real¦ + ¦y¦  ¦x + y¦" by (smt (verit))
lemma "P ((2::int) < 3) = P True" supply[[smt_trace]] by (smt (verit))
lemma "x + 3  4  x < (1::int)" by (smt (verit))

lemma
  assumes "x  (3::int)" and "y = x + 4"
  shows "y - x > 0"
  using assms by (smt (verit))

lemma "let x = (2 :: int) in x + x  5" by (smt (verit))

lemma
  fixes x :: int
  assumes "3 * x + 7 * a < 4" and "3 < 2 * x"
  shows "a < 0"
  using assms by (smt (verit))

lemma "(0  y + -1 * x  ¬ 0  x  0  (x::int)) = (¬ False)" by (smt (verit))

lemma "
  (n < m  m < n')  (n < m  m = n')  (n < n'  n' < m) 
  (n = n'  n' < m)  (n = m  m < n') 
  (n' < m  m < n)  (n' < m  m = n) 
  (n' < n  n < m)  (n' = n  n < m)  (n' = m  m < n) 
  (m < n  n < n')  (m < n  n' = n)  (m < n'  n' < n) 
  (m = n  n < n')  (m = n'  n' < n) 
  (n' = m  m = (n::int))"
  by (smt (verit))

text‹
The following example was taken from HOL/ex/PresburgerEx.thy, where it says:

  This following theorem proves that all solutions to the
  recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
  period 9.  The example was brought to our attention by John
  Harrison. It does does not require Presburger arithmetic but merely
  quantifier-free linear arithmetic and holds for the rationals as well.

  Warning: it takes (in 2006) over 4.2 minutes!

There, it is proved by "arith". (smt (verit)) is able to prove this within a fraction
of one second. With proof reconstruction, it takes about 13 seconds on a Core2
processor.
›

lemma " x3 = ¦x2¦ - x1; x4 = ¦x3¦ - x2; x5 = ¦x4¦ - x3;
         x6 = ¦x5¦ - x4; x7 = ¦x6¦ - x5; x8 = ¦x7¦ - x6;
         x9 = ¦x8¦ - x7; x10 = ¦x9¦ - x8; x11 = ¦x10¦ - x9 
  x1 = x10  x2 = (x11::int)"
  by (smt (verit))


lemma "let P = 2 * x + 1 > x + (x::real) in P  False  P" by (smt (verit))


subsection ‹Linear arithmetic with quantifiers›

lemma "~ (x::int. False)" by (smt (verit))
lemma "~ (x::real. False)" by (smt (verit))


lemma "x y::int. (x = 0  y = 1)  x  y" by (smt (verit))
lemma "x y::int. x < y  (2 * x + 1) < (2 * y)" by (smt (verit))
lemma "x y::int. x + y > 2  x + y = 2  x + y < 2" by (smt (verit))
lemma "x::int. if x > 0 then x + 1 > 0 else 1 > x" by (smt (verit))
lemma "(if (x::int. x < 0  x > 0) then -1 else 3) > (0::int)" by (smt (verit))
lemma "x::int. x y. 0 < x  0 < y  (0::int) < x + y" by (smt (verit))
lemma "u::int. (x::int) y::real. 0 < x  0 < y  -1 < x" by (smt (verit))
lemma "(a::int) b::int. 0 < b  b < 1" by (smt (verit))

subsection ‹Linear arithmetic for natural numbers›

declare [[smt_nat_as_int]]

lemma "2 * (x::nat)  1" by (smt (verit))

lemma "a < 3  (7::nat) > 2 * a" by (smt (verit))

lemma "let x = (1::nat) + y in x - y > 0 * x" by (smt (verit))

lemma
  "let x = (1::nat) + y in
   let P = (if x > 0 then True else False) in
   False  P = (x - 1 = y)  (¬P  False)"
  by (smt (verit))

lemma "int (nat ¦x::int¦) = ¦x¦" by (smt (verit) int_nat_eq)

definition prime_nat :: "nat  bool" where
  "prime_nat p = (1 < p  (m. m dvd p --> m = 1  m = p))"

lemma "prime_nat (4*m + 1)  m  (1::nat)" by (smt (verit) prime_nat_def)

lemma "2 * (x::nat)  1" 
  by (smt (verit))

lemma 2*(x :: int)  1
  by (smt (verit))

declare [[smt_nat_as_int = false]]


section ‹Pairs›

lemma "fst (x, y) = a  x = a"
  using fst_conv by (smt (verit))

lemma "p1 = (x, y)  p2 = (y, x)  fst p1 = snd p2"
  using fst_conv snd_conv by (smt (verit))


section ‹Higher-order problems and recursion›

lemma "i  i1  i  i2  (f (i1 := v1, i2 := v2)) i = f i"
  using fun_upd_same fun_upd_apply by (smt (verit))

lemma "(f g (x::'a::type) = (g x  True))  (f g x = True)  (g x = True)"
  by (smt (verit))

lemma "id x = x  id True = True"
  by (smt (verit) id_def)

lemma "i  i1  i  i2  ((f (i1 := v1)) (i2 := v2)) i = f i"
  using fun_upd_same fun_upd_apply by (smt (verit))

lemma
  "f (x. g x)  True"
  "f (x. g x)  True"
  by (smt (verit))+

lemma True using let_rsp by (smt (verit))
lemma "le = (≤)  le (3::int) 42" by (smt (verit))
lemma "map (λi::int. i + 1) [0, 1] = [1, 2]" by (smt (verit) list.map)
lemma "(x. P x)  ¬ All P" by (smt (verit))

fun dec_10 :: "int  int" where
  "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"

lemma "dec_10 (4 * dec_10 4) = 6" by (smt (verit) dec_10.simps)

context complete_lattice
begin

lemma
  assumes "Sup {a | i::bool. True}  Sup {b | i::bool. True}"
  and "Sup {b | i::bool. True}  Sup {a | i::bool. True}"
  shows "Sup {a | i::bool. True}  Sup {a | i::bool. True}"
  using assms by (smt (verit) order_trans)

end

lemma
 "eq_set (List.coset xs) (set ys) = rhs"
    if "ys. subset' (List.coset xs) (set ys) = (let n = card (UNIV::'a set) in 0 < n  card (set (xs @ ys)) = n)"
      and "uu A. (uu::'a)  - A  uu  A"
      and "uu. card (set (uu::'a list)) = length (remdups uu)"
      and "uu. finite (set (uu::'a list))"
      and "uu. (uu::'a)  UNIV"
      and "(UNIV::'a set)  {}"
      and "c A B P. (c::'a)  A  B; c  A  P; c  B  P  P"
      and "a b. (a::nat) + b = b + a"
      and "a b. ((a::nat) = a + b) = (b = 0)"
      and "card' (set xs) = length (remdups xs)"
      and "card' = (card :: 'a set  nat)"
      and "A B. finite (A::'a set); finite B  card A + card B = card (A  B) + card (A  B)"
      and "A. (card (A::'a set) = 0) = (A = {}  infinite A)"
      and "A. finite (UNIV::'a set); card (A::'a set) = card (UNIV::'a set)  A = UNIV"
      and "xs. - List.coset (xs::'a list) = set xs"
      and "xs. - set (xs::'a list) = List.coset xs"
      and "A B. (A  B = {}) = (x. (x::'a)  A  x  B)"
      and "eq_set = (=)"
      and "A. finite (A::'a set)  finite (- A) = finite (UNIV::'a set)"
      and "rhs  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  (xset xs'. x  set ys')  (yset ys'. y  set xs')"
      and "xs ys. set ((xs::'a list) @ ys) = set xs  set ys"
      and "A B. ((A::'a set) = B) = (A  B  B  A)"
      and "xs. set (remdups (xs::'a list)) = set xs"
      and "subset' = (⊆)"
      and "A B. (x. (x::'a)  A  x  B)  A  B"
      and "A B. (A::'a set)  B; B  A  A = B"
      and "A ys. (A  List.coset ys) = (yset ys. (y::'a)  A)"
  using that by (smt (verit, default))

notepad
begin
  have "line_integral F {i, j} g = line_integral F {i} g + line_integral F {j} g"
    if (k, g)  one_chain_typeI
      A b B. ({} = (A::(real × real) set)  insert (b::real × real) (B::(real × real) set)) = (b  A  {} = A  B)
      finite ({} :: (real × real) set)
      a A. finite (A::(real × real) set)  finite (insert (a::real × real) A)
      (i::real × real) = (1::real, 0::real)
      a A. (a::real × real)  (A::(real × real) set)  insert a A = A j = (0, 1)
      x. (x::(real × real) set)  {} = {}
      y x A. insert (x::real × real) (insert (y::real × real) (A::(real × real) set)) =  insert y (insert x A)
      a A. insert (a::real × real) (A::(real × real) set) = {a}  A
      F u basis2 basis1 γ. finite (u :: (real × real) set) 
    line_integral_exists F basis1 γ 
    line_integral_exists F basis2 γ 
    basis1  basis2 = u 
    basis1  basis2 = {} 
    line_integral F u γ = line_integral F basis1 γ + line_integral F basis2 γ
      one_chain_line_integral F {i} one_chain_typeI =
    one_chain_line_integral F {i} one_chain_typeII 
    ((k, γ)one_chain_typeI. line_integral_exists F {i} γ) 
    ((k, γ)one_chain_typeII. line_integral_exists F {i} γ)
      one_chain_line_integral (F::real × real  real × real) {j::real × real}
     (one_chain_typeII::(int × (real  real × real)) set) =
    one_chain_line_integral F {j} (one_chain_typeI::(int × (real  real × real)) set) 
    ((k::int, γ::real  real × real)one_chain_typeII. line_integral_exists F {j} γ) 
    ((k::int, γ::real  real × real)one_chain_typeI. line_integral_exists F {j} γ)
    for F i j g one_chain_typeI one_chain_typeII and
      line_integral :: (real × real  real × real)  (real × real) set  (real  real × real)  real and
      line_integral_exists :: (real × real  real × real)  (real × real) set  (real  real × real)  bool and
      one_chain_line_integral :: (real × real  real × real)  (real × real) set  (int × (real  real × real)) set  real and
      k
    using prod.case_eq_if singleton_inject snd_conv
      that
    by (smt (verit))
end


lemma
  fixes x y z :: real
  assumes x + 2 * y > 0 and
    x - 2 * y > 0 and
    x < 0
  shows False
  using assms by (smt (verit))

(*test for arith reconstruction*)
lemma
  fixes d :: real
  assumes 0 < d
   diamond_y  λt. d / 2 - ¦t¦
   a b c :: real. (a / c < b / c) =
    ((0 < c  a < b)  (c < 0  b < a)  c  0)
   a b c :: real. (a / c < b / c) =
    ((0 < c  a < b)  (c < 0  b < a)  c  0)
   a b :: real. - a / b = - (a / b)
   a b :: real. - a * b = - (a * b)
   (x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1  x2 = y2)
 shows (λy. (d / 2, (2 * y - 1) * diamond_y (d / 2))) 
    (λx. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) 
    (λy. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
    (λx. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) 
    False
  using assms
  by (smt (verit,del_insts))

lemma
  fixes d :: real
  assumes 0 < d
   diamond_y  λt. d / 2 - ¦t¦
   a b c :: real. (a / c < b / c) =
    ((0 < c  a < b)  (c < 0  b < a)  c  0)
   a b c :: real. (a / c < b / c) =
    ((0 < c  a < b)  (c < 0  b < a)  c  0)
   a b :: real. - a / b = - (a / b)
   a b :: real. - a * b = - (a * b)
   (x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1  x2 = y2)
 shows (λy. (d / 2, (2 * y - 1) * diamond_y (d / 2))) 
    (λx. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) 
    (λy. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
    (λx. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) 
    False
  using assms
  by (smt (verit,ccfv_threshold))

(*qnt_rm_unused example*)
lemma 
  assumes z y x. P z y
    P z y  False
  shows False
  using assms
  by (smt (verit))


lemma
  "max (x::int) y  y"
  supply [[smt_trace]]
  by (smt (verit))+

context
begin
abbreviation finite' :: "'a set  bool"
  where "finite' A  finite A  A  {}"

lemma
  fixes f :: "'b  'c :: linorder"
  assumes
    (S::'b::type set) f::'b::type  'c::linorder. finite' S  arg_min_on f S  S
    (S::'a::type set) f::'a::type  'c::linorder. finite' S  arg_min_on f S  S
    (S::'b::type set) (y::'b::type) f::'b::type  'c::linorder.
       finite S  S  {}  y  S  f (arg_min_on f S)  f y
    (S::'a::type set) (y::'a::type) f::'a::type  'c::linorder.
       finite S  S  {}  y  S  f (arg_min_on f S)  f y
    (f::'b::type  'c::linorder) (g::'a::type  'b::type) x::'a::type. (f  g) x = f (g x)
    (F::'b::type set) h::'b::type  'a::type. finite F  finite (h ` F)
    (F::'b::type set) h::'b::type  'b::type. finite F  finite (h ` F)
    (F::'a::type set) h::'a::type  'b::type. finite F  finite (h ` F)
    (F::'a::type set) h::'a::type  'a::type. finite F  finite (h ` F)
    (b::'a::type) (f::'b::type  'a::type) A::'b::type set.
       b  f ` A  (x::'b::type. b = f x  x  A  False)  False
    (b::'b::type) (f::'b::type  'b::type) A::'b::type set.
       b  f ` A  (x::'b::type. b = f x  x  A  False)  False
    (b::'b::type) (f::'a::type  'b::type) A::'a::type set.
       b  f ` A  (x::'a::type. b = f x  x  A  False)  False
    (b::'a::type) (f::'a::type  'a::type) A::'a::type set.
       b  f ` A  (x::'a::type. b = f x  x  A  False)  False
    (b::'a::type) (f::'b::type  'a::type) (x::'b::type) A::'b::type set. b = f x  x  A  b  f ` A
    (b::'b::type) (f::'b::type  'b::type) (x::'b::type) A::'b::type set. b = f x  x  A  b  f ` A
    (b::'b::type) (f::'a::type  'b::type) (x::'a::type) A::'a::type set. b = f x  x  A  b  f ` A
    (b::'a::type) (f::'a::type  'a::type) (x::'a::type) A::'a::type set. b = f x  x  A  b  f ` A
    (f::'b::type  'a::type) A::'b::type set. (f ` A = {}) = (A = {})
    (f::'b::type  'b::type) A::'b::type set. (f ` A = {}) = (A = {})
    (f::'a::type  'b::type) A::'a::type set. (f ` A = {}) = (A = {})
    (f::'a::type  'a::type) A::'a::type set. (f ` A = {}) = (A = {})
    (f::'b::type  'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
       inj_on f A  f x = f y  x  A  y  A  x = y
    (x::'c::linorder) y::'c::linorder. (x < y) = (x  y  x  y)
    inj_on (f::'b::type  'c::linorder) ((g::'a::type  'b::type) ` (B::'a::type set))
    finite (B::'a::type set)
    (B::'a::type set)  {}
    arg_min_on ((f::'b::type  'c::linorder)  (g::'a::type  'b::type)) (B::'a::type set)  B
    x::'a::type.
       x  (B::'a::type set) 
       ((f::'b::type  'c::linorder)  (g::'a::type  'b::type)) x < (f  g) (arg_min_on (f  g) B)
    (f::'b::type  'c::linorder) (P::'b::type  bool) a::'b::type.
       inj_on f (Collect P)  P a  (y::'b::type. P y  f a  f y)  arg_min f P = a
    (S::'b::type set) f::'b::type  'c::linorder. finite' S  arg_min_on f S  S
    (S::'a::type set) f::'a::type  'c::linorder. finite' S  arg_min_on f S  S
    (S::'b::type set) (y::'b::type) f::'b::type  'c::linorder.
       finite S  S  {}  y  S  f (arg_min_on f S)  f y
    (S::'a::type set) (y::'a::type) f::'a::type  'c::linorder.
       finite S  S  {}  y  S  f (arg_min_on f S)  f y
    (f::'b::type  'c::linorder) (g::'a::type  'b::type) x::'a::type. (f  g) x = f (g x)
    (F::'b::type set) h::'b::type  'a::type. finite F  finite (h ` F)
    (F::'b::type set) h::'b::type  'b::type. finite F  finite (h ` F)
    (F::'a::type set) h::'a::type  'b::type. finite F  finite (h ` F)
    (F::'a::type set) h::'a::type  'a::type. finite F  finite (h ` F)
    (b::'a::type) (f::'b::type  'a::type) A::'b::type set.
       b  f ` A  (x::'b::type. b = f x  x  A  False)  False
    (b::'b::type) (f::'b::type  'b::type) A::'b::type set.
       b  f ` A  (x::'b::type. b = f x  x  A  False)  False
    (b::'b::type) (f::'a::type  'b::type) A::'a::type set.
       b  f ` A  (x::'a::type. b = f x  x  A  False)  False
    (b::'a::type) (f::'a::type  'a::type) A::'a::type set.
       b  f ` A  (x::'a::type. b = f x  x  A  False)  False
    (b::'a::type) (f::'b::type  'a::type) (x::'b::type) A::'b::type set. b = f x  x  A  b  f ` A
    (b::'b::type) (f::'b::type  'b::type) (x::'b::type) A::'b::type set. b = f x  x  A  b  f ` A
    (b::'b::type) (f::'a::type  'b::type) (x::'a::type) A::'a::type set. b = f x  x  A  b  f ` A
    (b::'a::type) (f::'a::type  'a::type) (x::'a::type) A::'a::type set. b = f x  x  A  b  f ` A
    (f::'b::type  'a::type) A::'b::type set. (f ` A = {}) = (A = {})
    (f::'b::type  'b::type) A::'b::type set. (f ` A = {}) = (A = {})
    (f::'a::type  'b::type) A::'a::type set. (f ` A = {}) = (A = {})
    (f::'a::type  'a::type) A::'a::type set. (f ` A = {}) = (A = {})
    (f::'b::type  'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
       inj_on f A  f x = f y  x  A  y  A  x = y
    (x::'c::linorder) y::'c::linorder. (x < y) = (x  y  x  y)
    arg_min_on (f::'b::type  'c::linorder) ((g::'a::type  'b::type) ` (B::'a::type set)) 
       g (arg_min_on (f  g) B)
   shows False
  using assms
  by (smt (verit))
end


experiment
begin
private datatype abort =
    Rtype_error
  | Rtimeout_error
private datatype ('a) error_result =
  Rraise " 'a " ― ‹ Should only be a value of type exn ›
  | Rabort " abort "

private datatype( 'a, 'b) result =
    Rval " 'a "
    | Rerr " ('b) error_result "

lemma
  fixes clock :: 'astate  nat and
    fun_evaluate_match :: 'astate  'vsemv_env  _  ('pat × 'exp0) list  _ 
      'astate*((('v)list),('v))result
  assumes
    "fix_clock (st::'astate) (fun_evaluate st (env::'vsemv_env) [e::'exp0]) =
    (st'::'astate, r::('v list, 'v) result)"
    "clock (fst (fun_evaluate (st::'astate) (env::'vsemv_env) [e::'exp0]))  clock st"
    "(b::nat) (a::nat) c::nat. b  a  c  b  c  a"
    "(a::'astate) p::'astate × ('v list, 'v) result. (a = fst p) = (b::('v list, 'v) result. p = (a, b))"
    "y::'v error_result. (x1::'v. y = Rraise x1  False)  (x2::abort. y = Rabort x2  False)  False"
    "(f1::'v  'astate × ('v list, 'v) result) (f2::abort  'astate × ('v list, 'v) result) x1::'v.
       (case Rraise x1 of Rraise (x::'v)  f1 x | Rabort (x::abort)  f2 x) = f1 x1"
    "(f1::'v  'astate × ('v list, 'v) result) (f2::abort  'astate × ('v list, 'v) result) x2::abort.
       (case Rabort x2 of Rraise (x::'v)  f1 x | Rabort (x::abort)  f2 x) = f2 x2"
    "(s1::'astate) (s2::'astate) (x::('v list, 'v) result) s::'astate.
       fix_clock s1 (s2, x) = (s, x)  clock s  clock s2"
    "(s::'astate) (s'::'astate) res::('v list, 'v) result.
       fix_clock s (s', res) =
       (update_clock (λ_::nat. if clock s'  clock s then clock s' else clock s) s', res)"
    "(x2::'v error_result) x1::'v.
       (r::('v list, 'v) result) = Rerr x2  x2 = Rraise x1 
       clock (fst (fun_evaluate_match (st'::'astate) (env::'vsemv_env) x1 (pes::('pat × 'exp0) list) x1))
        clock st'"
  shows "((r::('v list, 'v) result) = Rerr (x2::'v error_result) 
           clock
            (fst (case x2 of
                  Rraise (v2::'v) 
                    fun_evaluate_match (st'::'astate) (env::'vsemv_env) v2 (pes::('pat × 'exp0) list) v2
                  | Rabort (abort::abort)  (st', Rerr (Rabort abort))))
            clock (st::'astate))"
  using assms by (smt (verit))
end


context
  fixes piecewise_C1 :: "('real :: {one,zero,ord}  'a :: {one,zero,ord})  'real set  bool"  and
     joinpaths :: "('real  'a)  ('real  'a)  'real  'a"
begin
notation piecewise_C1 (infixr "piecewise'_C1'_differentiable'_on" 50)
notation joinpaths (infixr "+++" 75)

lemma
   (v1. v0. (rec_join v0 = v1 
               (v0 = []  (λuu. 0) = v1  False) 
               (v2. v0 = [v2]  v1 = coeff_cube_to_path v2  False) 
               (v2 v3 v4.
                   v0 = v2 # v3 # v4  v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4)  False) 
               False) =
              (rec_join v0 = rec_join v0 
               (v0 = []  (λuu. 0) = rec_join v0  False) 
               (v2. v0 = [v2]  rec_join v0 = coeff_cube_to_path v2  False) 
               (v2 v3 v4.
                   v0 = v2 # v3 # v4  rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) 
                   False) 
               False)) 
         (v0 v1.
             rec_join v0 = v1 
             (v0 = []  (λuu. 0) = v1  False) 
             (v2. v0 = [v2]  v1 = coeff_cube_to_path v2  False) 
             (v2 v3 v4. v0 = v2 # v3 # v4  v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4)  False) 
             False) =
         (v0. rec_join v0 = rec_join v0 
               (v0 = []  (λuu. 0) = rec_join v0  False) 
               (v2. v0 = [v2]  rec_join v0 = coeff_cube_to_path v2  False) 
               (v2 v3 v4.
                   v0 = v2 # v3 # v4  rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) 
                   False) 
               False)
  by (smt (verit))

end


section ‹Monomorphization examples›

definition Pred :: "'a  bool" where
  "Pred x = True"

lemma poly_Pred: "Pred x  (Pred [x]  ¬ Pred [x])"
  by (simp add: Pred_def)

lemma "Pred (1::int)"
  by (smt (verit) poly_Pred)

axiomatization g :: "'a  nat"
axiomatization where
  g1: "g (Some x) = g [x]" and
  g2: "g None = g []" and
  g3: "g xs = length xs"

lemma "g (Some (3::int)) = g (Some True)" by (smt (verit) g1 g2 g3 list.size)

experiment
begin

lemma duplicate_goal: A  A  A
  by auto

datatype 'a M_nres = is_fail: FAIL | SPEC "'a  bool"

definition "is_res m x  case m of FAIL  True | SPEC P  P x"

datatype ('a,'s) M_state = M_STATE (run: "'s  ('a×'s) M_nres")

(*Courtesy of Peter Lammich
https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20smt.20.28verit.29.3A.20exception.20THM.200.20raised.20.28line.20312.20.2E.2E.2E/near/290088165
*)
lemma "x y. (xa s. is_fail (run (x xa) s) 
                   is_fail (run (y xa) s) = is_fail (run (x xa) s) 
                   (a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))

           (s. is_fail (run (B x) s) 
                is_fail (run (B y) s) = is_fail (run (B x) s) 
                (a b. is_res (run (B y) s) (a, b) = is_res (run (B x) s) (a, b)));
     y. x ya. (xa s. is_fail (run (x xa) s) 
                         is_fail (run (ya xa) s) = is_fail (run (x xa) s) 
                         (a b. is_res (run (ya xa) s) (a, b) = is_res (run (x xa) s) (a, b)))

                 (s. is_fail (run (C y x) s) 
                      is_fail (run (C y ya) s) = is_fail (run (C y x) s) 
                      (a b. is_res (run (C y ya) s) (a, b) = is_res (run (C y x) s) (a,
b)))
     x y. (xa s.
                  is_fail (run (x xa) s) 
                  is_fail (run (y xa) s) = is_fail (run (x xa) s) 
                  (a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))

              (s. is_fail (run (B x) s) 
                   (a b. is_res (run (B x) s) (a, b)  is_fail (run (C a x) b)) 
                   (is_fail (run (B y) s)  (a b. is_res (run (B y) s) (a, b) 
is_fail (run (C a y) b))) =
                   (is_fail (run (B x) s)  (a b. is_res (run (B x) s) (a, b) 
is_fail (run (C a x) b))) 
                   (a b. (is_fail (run (B y) s) 
                           (aa ba. is_res (run (B y) s) (aa, ba)  is_res (run (C aa y)
ba) (a, b))) =
                          (is_fail (run (B x) s) 
                           (aa ba. is_res (run (B x) s) (aa, ba)  is_res (run (C aa x)
ba) (a, b)))))"  
  apply (rule duplicate_goal)
  subgoal
    supply [[verit_compress_proofs=true]]
    by (smt (verit))
  subgoal
    supply [[verit_compress_proofs=false]]
    by (smt (verit))
  done

(*Example of Reordering in skolemization*)
lemma
  fixes Abs_ExpList :: "'freeExp_list  'exp_list" and
    Abs_Exp:: "'freeExp_set  'exp" and
    exprel:: "('freeExp × 'freeExp) set" and
    map2 :: "('freeExp  'exp)  'freeExp_list  'exp_list"
  assumes "Xs. Abs_ExpList Xs   map2 (λU. Abs_Exp (myImage exprel {U})) Xs"
    "P z. (U. z = Abs_Exp (myImage exprel {U})  P)  P"
    "(ys::'exp_list) (f::'freeExp  _). (xs. ys = map2 f xs) = (ymyset ys. x. y = f x)"
  shows "Us. z = Abs_ExpList Us"
  apply (rule duplicate_goal)
  subgoal
    supply [[verit_compress_proofs=true]]
    using assms
    by (smt (verit,del_insts))
  subgoal
    using assms
    supply [[verit_compress_proofs=false]]
    by (smt (verit,del_insts))
  done

end

context
  fixes
    L2_final :: "'afset  'afset × 'afset  bool" and
    L3_final :: "'afset  'afset × 'afset  bool" and
    ground_resolution :: "'a  'a  'a  bool" and
    is_least_false_clause :: "'afset  'a  bool" and
    fset :: "'afset  'a set" and
    union_fset :: "'afset  'afset  'afset" (infixr "|∪|" 50)
begin
term "a |∪| b"

fun L2_matches_L3 where
  "L2_matches_L3 N2 (Ur2, Uff2) N3 (Urr3, Uff3) 
    N2 = N3  Uff2 = Uff3 
    (Cr  fset Ur2. C  fset (N3 |∪| Urr3 |∪| Uff3). D  fset (N3 |∪| Urr3 |∪| Uff3).
      (ground_resolution D)++ C Cr 
      (Crr  fset Urr3. (ground_resolution D)** Cr Crr)  (is_least_false_clause (N2 |∪| Ur2 |∪| Uff2) Cr))"

lemma
  assumes match: "L2_matches_L3 Const2 S2 Const3 S3"
  shows "L2_final Const2 S2  L2_final Const3 S3"
proof -
  from match obtain N Ur Uff Urr where
    state_simps:
      "Const2 = N"
      "Const3 = N"
      "S2 = (Ur, Uff)"
      "S3 = (Urr, Uff)" and
    Ur_spec: "
      Cr  fset Ur.
      C  fset (N |∪| Urr |∪| Uff).
      D  fset (N |∪| Urr |∪| Uff).
      (ground_resolution D)++ C Cr 
      (Crr  fset Urr. (ground_resolution D)** Cr Crr) 
        (is_least_false_clause (N |∪| Ur |∪| Uff) Cr)"
    by (smt (verit) L2_matches_L3.elims(2))
  oops
end

end