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›
declare[[smt_trace=false]]
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 "¦x :: int¦ + ¦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))

declare [[verit_options="--proof-with-sharing --proof-define-skolems --proof-prune --proof-merge 
--disable-print-success --disable-banner"]]

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 [[smt_trace=false]] 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 [[smt_trace=false]]
  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))  (*subproof reconstruction is using blast here because we do not distinguish the ∨ properly*)
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 [[smt_trace=false]] 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)

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]][[smt_trace=false]] 
    by (smt (verit))
  subgoal
    supply [[verit_compress_proofs=false]][[smt_trace=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]][[smt_trace=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)"
    supply [[smt_trace]]
    by (smt (verit) L2_matches_L3.elims(2))
  oops

lemma
  assumes
  "       ∀(a::real) c::real. (a * c ≤ c) = ((0 < c ⟶ a ≤ 1) ∧ (c < 0 ⟶ 1 ≤ a))"
       "∀x::real. 0 ≤ norm x"
       "∀x::complex. 0 ≤ cmod x"
       "∀(x::real) y::real. norm (x * y) = norm x * norm y"
       "∀(x::complex) y::complex. cmod (x * y) = cmod x * cmod y"
       "∀r::real. norm (of_real r) = (if r < 0 then - r else r)"
       "∀r::real. cmod (complex_of_real r) = (if r < 0 then - r else r)"
       "0 < (t::real)"
       "(t::real) < 1"
       "(t::real) < inverse (cmod (w::complex) ^ ((k::nat) + 1) * (m::real))"
       "¬ cmod (complex_of_real (t::real) * (w::complex)) ≤ cmod w"
     shows False
  using assms by (smt (verit))
end

locale comm_monoid_fun = comm_monoid
begin

definition G :: "('b ⇒ 'a) ⇒ 'a"
where
  expand_set: "G g = comm_monoid_set.F f ❙1 g {a. g a ≠ ❙1}"

interpretation F: comm_monoid_set f "❙1"
  ..

lemma
  assumes
       "∀(P::'b ⇒ bool) Q::'b ⇒ bool. (∀x::'b. P x ⟶ Q x) ⟶ Collect P ⊆ Collect Q"
       "∀(P::'c ⇒ bool) Q::'c ⇒ bool. (∀x::'c. P x ⟶ Q x) ⟶ Collect P ⊆ Collect Q"
       "∀(g::'b ⇒ 'a) h::'b ⇒ 'a. (∀a::'b. g a = h a) ⟶ G g = G h"
       "∀(g::'c ⇒ 'a) h::'c ⇒ 'a. (∀a::'c. g a = h a) ⟶ G g = G h"
       "∀g::'b ⇒ 'a. G g ≠ ❙1 ∧ (∀a::'b. g a ≠ ❙1 ⟶ False) ⟶ False"
       "∀g::'c ⇒ 'a. G g ≠ ❙1 ∧ (∀a::'c. g a ≠ ❙1 ⟶ False) ⟶ False"
       "finite {a::'b. ∃b::'c. (g::'b ⇒ 'c ⇒ 'a) a b ≠ ❙1}"
       "finite {b::'c. ∃a::'b. (g::'b ⇒ 'c ⇒ 'a) a b ≠ ❙1}"
       "∀(A::'b set) g::'b ⇒ 'a. finite A ∧ {a::'b. g a ≠ ❙1} ⊆ A ⟶ G g = F.F g A"
       "∀(A::'c set) g::'c ⇒ 'a. finite A ∧ {a::'c. g a ≠ ❙1} ⊆ A ⟶ G g = F.F g A"
       "G (λa::'b. G ((g::'b ⇒ 'c ⇒ 'a) a)) ≠ F.F (λa::'b. F.F (g a) {b::'c. ∃a::'b. g a b ≠ ❙1}) {a::'b. ∃b::'c. g a b ≠ ❙1}" 
     shows False
  using assms by (smt (verit, del_insts))
end

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)

text ‹Regressions›
experiment
begin

lemma 
  fixes eq :: "'qt1 ⇒ 'qt1 ⇒ bool" (infix "#=" 50) and
        card_of :: "'var set ⇒ 'var rel" (‹(‹open_block notation=‹mixfix card_of››|_|)›) and
        ordLess2 :: "'var rel ⇒ 'var rel ⇒ bool" (infix ‹<o› 50) and
        qGood :: "'qt1 ⇒ bool" and
        asTerm :: "'qt1 ⇒ 'qt1 set"
  assumes "∀(qX::'qt1) qY::'qt1.
          qGood qX ∧ asTerm qX = asTerm qY ⟶ qX #= qY"
       "∀x2::'qt1. the (Some x2) = x2"
       "∀x2::'qt1 set. the (Some x2) = x2"
       "∀(f1::'qt1 set option)
          (f2::'qt1 ⇒ 'qt1 set option)
          x2::'qt1.
          (case Some x2 of None ⇒ f1 | Some (x::'qt1) ⇒ f2 x) = f2 x2"
       "∀(f1::'qt1 set option)
          (f2::'qt1 ⇒ 'qt1 set option)
          option::'qt1 option.
          (case option of None ⇒ f1 | Some (x::'qt1) ⇒ f2 x) =
          (if option = None then f1 else f2 (the option))"
       "∀x2::'qt1. None ≠ Some x2"
       "∀x2::'qt1 set. None ≠ Some x2"
       "¬ (((∀(xs::'varSort) (i::'var) v::'qt1.
                (qrho::'varSort ⇒ 'var ⇒ 'qt1 option) xs i = Some v ⟶ qGood v) ∧
            (∀ys::'varSort. |{y::'var. ∃ya::'qt1. qrho ys y = Some ya}| <o (card_of UNIV))) ∧
           (λ(xs::'varSort) i::'var.
               case qrho xs i of None ⇒ None | Some (v::'qt1) ⇒ Some (asTerm v)) =
           (λ(xs::'varSort) i::'var.
               case (qrho'::'varSort ⇒ 'var ⇒ 'qt1 option) xs i of None ⇒ None
               | Some (v::'qt1) ⇒ Some (asTerm v)) ⟶
           (∀xs::'varSort.
               (∀i::'var. (qrho xs i = None) = (qrho' xs i = None)) ∧
               (∀(i::'var) (v1::'qt1) v2::'qt1.
                   qrho xs i = Some v1 ∧ qrho' xs i = Some v2 ⟶ v1 #= v2)))"
  shows "False"
   using assms by (smt (verit)) (*bind From: Binding_Syntax_Theory/Transition_QuasiTerms_Terms.thy*)

datatype ('n, 'e) result =
  Normal (normal: 'n)
| Exception (ex: 'e)
| NT

lemma
  assumes "∀(P::('a ⇒ ('b, 'c) result) ⇒ bool) Q::('a ⇒ ('b, 'c) result) ⇒ bool.
          (∀x::'a ⇒ ('b, 'c) result. P x = Q x) ⟶ Collect P = Collect Q"
       "∀(P::('b, 'c) result ⇒ bool) Q::('b, 'c) result ⇒ bool.
          (∀x::('b, 'c) result. P x = Q x) ⟶ Collect P = Collect Q"
       "∀(a::'a ⇒ ('b, 'c) result) P::('a ⇒ ('b, 'c) result) ⇒ bool. (a ∈ Collect P) = P a"
       "∀(a::('b, 'c) result) P::('b, 'c) result ⇒ bool. (a ∈ Collect P) = P a"
       "∀(f1::'b ⇒ bool) (f2::'c ⇒ bool) (f3::bool) result::('b, 'c) result.
          (case result of Normal (x::'b) ⇒ f1 x | Exception (x::'c) ⇒ f2 x | NT ⇒ f3) =
          (if is_Normal result then f1 (normal result) else if is_Exception result then f2 (ex result) else f3)"
       "∀result::('b, 'c) result. (result = NT) = (case result of NT ⇒ True | _ ⇒ False)"
       "∀(x::'a) a::('b, 'c) result.
          result_lub
           {y::('b, 'c) result. ∃xa::'a ⇒ ('b, 'c) result. xa ∈ (A::('a ⇒ ('b, 'c) result) set) ∧ y = xa x} =
          a ⟶
          a = NT ∨ a ∈ {y::('b, 'c) result. ∃xa::'a ⇒ ('b, 'c) result. xa ∈ A ∧ y = xa x}"
       "is_Normal
        (result_lub
          {y::('b, 'c) result. ∃x::'a ⇒ ('b, 'c) result. x ∈ (A::('a ⇒ ('b, 'c) result) set) ∧ y = x (h::'a)}) ∧
       (r::'b + 'c) = Inl (normal (result_lub {y::('b, 'c) result. ∃x::'a ⇒ ('b, 'c) result. x ∈ A ∧ y = x h}))"
       "is_Normal (fun_lub result_lub (A::('a ⇒ ('b, 'c) result) set) (h::'a)) ∧
       (r::'b + 'c) = Inl (normal (fun_lub result_lub A h))"
       "∀x::'a ⇒ ('b, 'c) result.
          x ∈ (A::('a ⇒ ('b, 'c) result) set) ⟶
          (∀(h::'a) r::'b + 'c.
              is_Normal (x h) ∧ r = Inl (normal (x h)) ∨ is_Exception (x h) ∧ r = Inr (ex (x h)) ⟶
              (P::'a ⇒ 'b + 'c ⇒ bool) h r)"
       "¬ (P::'a ⇒ 'b + 'c ⇒ bool) (h::'a) (r::'b + 'c)"
       shows "False"
  using assms by (smt (verit)) (*onepoint From: Isabelle-Solidity/State_Monad.thy*)

lemma
  fixes Sum :: "['a,'a,'a,'a,'a,'a] ⇒ bool" ("Sum _ _ _ _ _ _" [99,99,99,99,99,99] 50) and
        Opp :: "['a,'a,'a,'a,'a] ⇒ bool" ("Opp _ _ _ _ _" [99,99,99,99,99] 50) and
        Diff :: "['a,'a,'a,'a,'a,'a] ⇒ bool" ("Diff _ _ _ _ _ _" [99,99,99,99,99,99] 50)
  assumes "∀(PO::'a) (E::'a) (E'::'a) (A::'a) (B::'a) C::'a.
          (Ar2 PO E E' A B C) = (¬ Col PO E E' ∧ Col PO E A ∧ Col PO E B ∧ Col PO E C)"
       "∀(PO::'a) (E::'a) (E'::'a) (A::'a) (B::'a) C::'a.
          (Diff PO E E' A B C) = (∃B'::'a. Opp PO E E' B B' ∧ Sum PO E E' A B' C)"
       "Diff (PO::'a) (E::'a) (E'::'a) (B::'a) (A::'a) (dBA::'a)"
       "Diff (PO::'a) (E::'a) (E'::'a) (C::'a) (B::'a) (dCB::'a)"
       "Diff (PO::'a) (E::'a) (E'::'a) (C::'a) (A::'a) (dCA::'a)"
       "∀(PO::'a) (E::'a) (E'::'a) (A::'a) (B::'a) AMB::'a. Diff PO E E' A B AMB ⟶ Ar2 PO E E' A B AMB"
       "∀(PO::'a) (E::'a) (E'::'a) (S::'a) (A::'a) B::'a. Diff PO E E' S A B ⟶ Sum PO E E' A B S"
       "∀(PO::'a) (E::'a) (E'::'a) (A::'a) (MA1::'a) MA2::'a.
          ¬ Col PO E E' ∧ Opp PO E E' A MA1 ∧ Opp PO E E' A MA2 ⟶ MA1 = MA2"
       "∀(PO::'a) (E::'a) (E'::'a) (A::'a) (B::'a) (AB::'a) (C::'a) (BC::'a) ABC::'a.
          Sum PO E E' A B AB ∧ Sum PO E E' B C BC ⟶ (Sum PO E E' A BC ABC) = (Sum PO E E' AB C ABC)"
       "∀(PO::'a) (E::'a) (E'::'a) (A::'a) (B::'a) C::'a. ¬ Col PO E E' ∧ Sum PO E E' A B C ⟶ Sum PO E E' B A C"
       "¬ Sum (PO::'a) (E::'a) (E'::'a) (dCB::'a) (dBA::'a) (dCA::'a)"
       shows "False"
  using assms by (smt (verit)) (*qnt_cnf From: IsaGeoCoq/Tarski_Euclidean_2D.thy*)

lemma 
  fixes  holds_for :: "(_ ⇒ bool) ⇒ _ ⇒ bool" (‹_ holds'_for _› [100, 99] 100)
  assumes "∀(x::'cell list × 'cell list ⇒ bool) xa::nat × 'cell list × 'cell list.
          ¬ x holds_for xa ∧
          (∀(P::'cell list × 'cell list ⇒ bool) (s::nat) (l::'cell list) (r::'cell list).
              x = P ∧ xa = (s, l, r) ∧ ¬ P (l, r) ⟶ False) ⟶ False"
       "∀(n::nat) (s::nat) tap::'cell list × 'cell list.
          inv_tm_skip_first_arg_len_eq_1 n (s, tap) =
          (if s = 0 then inv_tm_skip_first_arg_len_eq_1_s0 n tap
           else if s = 1 then inv_tm_skip_first_arg_len_eq_1_s1 n tap
                else if s = (2::nat) then inv_tm_skip_first_arg_len_eq_1_s2 n tap
                     else if s = (3::nat) then inv_tm_skip_first_arg_len_eq_1_s3 n tap
                          else if s = (4::nat) then inv_tm_skip_first_arg_len_eq_1_s4 n tap
                               else if s = (5::nat) then inv_tm_skip_first_arg_len_eq_1_s5 n tap else False)"
       "∀(s::nat) tap::'cell list × 'cell list. is_final (s, tap) = (s = 0)"
       "is_final (steps0 (1, l::'cell list, r::'cell list) tm_skip_first_arg (stp::nat))"
       "inv_tm_skip_first_arg_len_eq_1 (n::nat) (steps0 (1, l::'cell list, r::'cell list) tm_skip_first_arg (stp::nat))"
       "¬ inv_tm_skip_first_arg_len_eq_1_s0
           (n::nat) holds_for steps0 (1, l::'cell list, r::'cell list) tm_skip_first_arg (stp::nat)" 
  shows "False"
  using assms by (smt (verit)) (*qnt_cnf (From: Universal_Turing_Machine/StrongCopyTM.thy)*)
end

(*From Notes_On_Goedels_Ontological_Argument, but transformed into a locale, to make it easier
to move this test within the file*)
locale test =
  fixes x :: "'i" and y :: "'e" and
  existsAt::"'e⇒'i⇒bool" and
  R::"'i⇒'i⇒bool" and
  Mess :: ‹('e ⇒ 'i ⇒ bool) ⇒ 'e ⇒ 'i ⇒ bool›
begin

notation (input) existsAt  ("_❙@_") 
notation (input) R ("_❙r_")

abbreviation (input) Mexiact::"('e⇒'i⇒bool)⇒'i⇒bool" ("❙∃⇧E") where "❙∃⇧EΦ ≡ λw.∃x. x❙@w ∧ Φ x w"
abbreviation (input)Mexiactb (binder "❙∃⇧E" [8]9) where "❙∃⇧Ex. φ(x) ≡ ❙∃⇧Eφ"

abbreviation (input) Mbot::‹('i⇒bool)› ("❙⊥") where "❙⊥ ≡ λw. False"
abbreviation (input) Mtop::‹('i⇒bool)› ("❙⊤") where "❙⊤ ≡ λw. True"
abbreviation (input) Mneg::"(('i⇒bool))⇒('i⇒bool)" ("❙¬_" [52]53) where "❙¬φ ≡ λw. ¬(φ w)"
abbreviation (input) Mand::"(('i⇒bool))⇒('i⇒bool)⇒('i⇒bool)" (infixl "❙∧" 50) where "φ❙∧ψ ≡ λw. φ w ∧ ψ w" 
abbreviation (input) Mor::"('i⇒bool)⇒('i⇒bool)⇒('i⇒bool)" (infixl "❙∨" 49) where "φ❙∨ψ ≡ λw. φ w ∨ ψ w "
abbreviation (input) Mimp::"('i⇒bool)⇒('i⇒bool)⇒('i⇒bool)" (infixr "❙⊃" 48) where "φ❙⊃ψ ≡ λw. φ w ⟶ ψ w" 
abbreviation (input) Mequiv::"('i⇒bool)⇒('i⇒bool)⇒('i⇒bool)" (infixl "❙↔" 47) where "φ❙↔ψ ≡ λw. φ w ⟷ ψ w"
abbreviation (input) Mbox::"('i⇒bool)⇒('i⇒bool)" ("❙□_" [54]55) where "❙□φ ≡ λw.∀v. w ❙r v ⟶ φ v"
abbreviation (input) Mdia::"('i⇒bool)⇒('i⇒bool)" ("❙◇_" [54]55) where "❙◇φ ≡ λw.∃v. w ❙r v ∧ φ v"
abbreviation (input) Mnegpred::"('e⇒('i⇒bool))⇒('e⇒('i⇒bool))" ("❙~_") where "❙~Φ ≡ λx.λw. ¬Φ x w"
abbreviation (input) Mconpred::"('e⇒('i⇒bool))⇒('e⇒('i⇒bool))⇒('e⇒('i⇒bool))" (infixl "❙." 50) where "Φ❙.Ψ ≡ λx.λw. Φ x w ∧ Ψ x w"
abbreviation (input) Mexclor::"('i⇒bool)⇒('i⇒bool)⇒('i⇒bool)" (infixl "❙∨⇧e" 49) where "φ❙∨⇧eψ ≡ (φ ❙∨ ψ) ❙∧ ❙¬(φ ❙∧ ψ)" 
abbreviation (input) Mvalid::"('i⇒bool)⇒bool" ("⌊_⌋⇩g") where "⌊ψ⌋⇩g ≡ ∀w. ψ w"

notation (input) Mess ("_Ess_") 
lemma
  fixes P :: ‹('e⇒'i⇒bool)⇒'i⇒bool› and
        E :: ‹'e ⇒ 'i ⇒ bool›
  assumes "⌊ P E ⌋⇩g"
         "∀(φ::'e ⇒ 'i ⇒ bool) ψ::'e ⇒ 'i ⇒ bool. ⌊P φ ❙∧ ❙□(λv::'i. ∀x::'e. (φ x ❙⊃ ψ x) v) ❙⊃ P ψ⌋⇩g"
         "∀x::'e. ⌊λxa::'i. E x xa = (∀xb::'e ⇒ 'i ⇒ bool. ((xb Ess x) ❙⊃ ❙□Mexiactb xb) xa)⌋⇩g"
         "¬ ⌊P (λx::'e. ((λy::'e. ❙⊥) Ess x) ❙⊃ (❙□(λv::'i. ∃x::'e. (x❙@v) ∧ False)))⌋⇩g"
  shows "False"
  using assms by (smt (verit)) (*bool_simplify From: Notes_On_Goedels_Ontological_Argument/GoedelVariantHOML1AndersonQuant.thy*)
end

experiment 
begin

abbreviation "nonEmpty S ≡ ∃x. S x"

lemma
  fixes φ :: ‹('a ⇒ bool) ⇒ 'a ⇒ bool›
  assumes "(∀S::('a ⇒ bool) ⇒ bool.
           let U::'a ⇒ bool = λw::'a. nonEmpty (λX::'a ⇒ bool. S X ∧ X w)
           in ∀x::'a.
                 ¬ U x ∧ nonEmpty (λX::'a ⇒ bool. nonEmpty (λx::'a ⇒ bool. S x ∧ (φ::('a ⇒ bool) ⇒ 'a ⇒ bool) x = X) ∧ X x) ⟶
                 φ (λw::'a. nonEmpty (λX::'a ⇒ bool. S X ∧ X w)) x) ≠
       (∀S::('a ⇒ bool) ⇒ bool.
           let U::'a ⇒ bool = λw::'a. nonEmpty (λX::'a ⇒ bool. S X ∧ X w)
           in ∀x::'a.
                 ¬ U x ∧ nonEmpty (λX::'a ⇒ bool. nonEmpty (λx::'a ⇒ bool. S x ∧ (λp::'a. φ x p ≠ x p) = X) ∧ X x) ⟶
                 φ (λw::'a. nonEmpty (λX::'a ⇒ bool. S X ∧ X w)) x ≠ nonEmpty (λX::'a ⇒ bool. S X ∧ X x))"
shows "False"
  using assms supply [[smt_trace]] by (smt (verit)) (*qnt_cnf From: Topological_Semantics/conditions_relativized_infinitary.thy*)
end

locale _ =
  fixes order :: "'energy ⇒ 'energy ⇒ bool"  (infix ‹e≤› 80) and
        energies :: "'energy set"
begin

abbreviation "incomparable P ≡ λx y. ¬ P x y ∧ ¬ P y x"

definition possible_pareto:: "('position ⇒ 'energy set) set" where 
  "possible_pareto ≡ {F. ∀g. F g ⊆ {e. e∈energies} 
                          ∧ (∀e e'. (e ∈ F g ∧ e' ∈ F g ∧ e ≠ e') 
                             ⟶ (¬ e e≤ e' ∧ ¬ e' e≤ e))}"

lemma
  assumes "∀(A::('position ⇒ 'energy set) set) P::('position ⇒ 'energy set) ⇒ bool.
          (∀x::'position ⇒ 'energy set. x ∈ A ⟶ P x) = (A ⊆ Collect P)"
       "∀(A::'energy set) P::'energy ⇒ bool. (∀x::'energy. x ∈ A ⟶ P x) = (A ⊆ Collect P)"
       "(P::('position ⇒ 'energy set) set) ⊆ possible_pareto"
       "∀(a::'position ⇒ 'energy set) P::('position ⇒ 'energy set) ⇒ bool. (a ∈ Collect P) = P a"
       "∀(a::'energy) P::'energy ⇒ bool. (a ∈ Collect P) = P a"
       "possible_pareto =
       {F::'position ⇒ 'energy set.
        ∀g::'position.
           F g ⊆ {e::'energy. e ∈ (energies::'energy set)} ∧
           (∀(e::'energy) e'::'energy. e ∈ F g ∧ e' ∈ F g ∧ e ≠ e' ⟶ incomparable (e≤) e e')}"
       "(λg::'position.
           {e::'energy ∈ {e::'energy. ∃F::'position ⇒ 'energy set. F ∈ (P::('position ⇒ 'energy set) set) ∧ e ∈ F g}.
            ∀x::'energy. x ∈ {e::'energy. ∃F::'position ⇒ 'energy set. F ∈ P ∧ e ∈ F g} ∧ e ≠ x ⟶ ¬ x e≤ e})
       ∉ {F::'position ⇒ 'energy set.
           ∀g::'position.
              F g ⊆ {e::'energy. e ∈ (energies::'energy set)} ∧
              (∀(e::'energy) e'::'energy. e ∈ F g ∧ e' ∈ F g ∧ e ≠ e' ⟶ incomparable (e≤) e e')}"
  shows "False"
  using assms by (smt (verit, ccfv_threshold)) (*qnt_cnf From: Galois_Energy_Games/Decidability.thy*)
end

end