Quelle  SMT_Examples_Verit.thy   Sprache: Isabelle

(*  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 \ (\x\set xs'. x \ set ys') \ (\y\set 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) = (\y\set 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) = (\y\myset 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