(*  Title:      HOL/Metis_Examples/Clausification.thy
    Author:     Jasmin Blanchette, TU Muenchen

Example that exercises Metis's Clausifier.
*)

section ‹Example that Exercises Metis's Clausifier›

theory Clausification
imports Complex_Main
begin


text ‹Definitional CNF for facts›

declare [[meson_max_clauses = 10]]

axiomatization q :: "nat → nat → bool" where
qax: "∃b. ∀a. (q b a ∧ q 0 0 ∧ q 1 a ∧ q a 1) ∨ (q 0 1 ∧ q 1 0 ∧ q a b ∧ q 1 1)"

declare [[metis_new_skolem = false]]

lemma "∃b. ∀a. (q b a ∨ q a b)"
by (metis qax)

lemma "∃b. ∀a. (q b a ∨ q a b)"
by (metis (full_types) qax)

lemma "∃b. ∀a. (q b a ∧ q 0 0 ∧ q 1 a ∧ q a 1) ∨ (q 0 1 ∧ q 1 0 ∧ q a b ∧ q 1 1)"
by (metis qax)

lemma "∃b. ∀a. (q b a ∧ q 0 0 ∧ q 1 a ∧ q a 1) ∨ (q 0 1 ∧ q 1 0 ∧ q a b ∧ q 1 1)"
by (metis (full_types) qax)

declare [[metis_new_skolem]]

lemma "∃b. ∀a. (q b a ∨ q a b)"
by (metis qax)

lemma "∃b. ∀a. (q b a ∨ q a b)"
by (metis (full_types) qax)

lemma "∃b. ∀a. (q b a ∧ q 0 0 ∧ q 1 a ∧ q a 1) ∨ (q 0 1 ∧ q 1 0 ∧ q a b ∧ q 1 1)"
by (metis qax)

lemma "∃b. ∀a. (q b a ∧ q 0 0 ∧ q 1 a ∧ q a 1) ∨ (q 0 1 ∧ q 1 0 ∧ q a b ∧ q 1 1)"
by (metis (full_types) qax)

declare [[meson_max_clauses = 60]]

axiomatization r :: "nat → nat → bool" where
rax: "(r 0 0 ∧ r 0 1 ∧ r 0 2 ∧ r 0 3) ∨
      (r 1 0 ∧ r 1 1 ∧ r 1 2 ∧ r 1 3) ∨
      (r 2 0 ∧ r 2 1 ∧ r 2 2 ∧ r 2 3) ∨
      (r 3 0 ∧ r 3 1 ∧ r 3 2 ∧ r 3 3)"

declare [[metis_new_skolem = false]]

lemma "r 0 0 ∨ r 1 1 ∨ r 2 2 ∨ r 3 3"
by (metis rax)

lemma "r 0 0 ∨ r 1 1 ∨ r 2 2 ∨ r 3 3"
by (metis (full_types) rax)

declare [[metis_new_skolem]]

lemma "r 0 0 ∨ r 1 1 ∨ r 2 2 ∨ r 3 3"
by (metis rax)

lemma "r 0 0 ∨ r 1 1 ∨ r 2 2 ∨ r 3 3"
by (metis (full_types) rax)

lemma "(r 0 0 ∧ r 0 1 ∧ r 0 2 ∧ r 0 3) ∨
       (r 1 0 ∧ r 1 1 ∧ r 1 2 ∧ r 1 3) ∨
       (r 2 0 ∧ r 2 1 ∧ r 2 2 ∧ r 2 3) ∨
       (r 3 0 ∧ r 3 1 ∧ r 3 2 ∧ r 3 3)"
by (metis rax)

lemma "(r 0 0 ∧ r 0 1 ∧ r 0 2 ∧ r 0 3) ∨
       (r 1 0 ∧ r 1 1 ∧ r 1 2 ∧ r 1 3) ∨
       (r 2 0 ∧ r 2 1 ∧ r 2 2 ∧ r 2 3) ∨
       (r 3 0 ∧ r 3 1 ∧ r 3 2 ∧ r 3 3)"
by (metis (full_types) rax)


text ‹Definitional CNF for goal›

axiomatization p :: "nat → nat → bool" where
pax: "∃b. ∀a. (p b a ∧ p 0 0 ∧ p 1 a) ∨ (p 0 1 ∧ p 1 0 ∧ p a b)"

declare [[metis_new_skolem = false]]

lemma "∃b. ∀a. ∃x. (p b a ∨ x) ∧ (p 0 0 ∨ x) ∧ (p 1 a ∨ x) ∧
                   (p 0 1 ∨ ¬ x) ∧ (p 1 0 ∨ ¬ x) ∧ (p a b ∨ ¬ x)"
by (metis pax)

lemma "∃b. ∀a. ∃x. (p b a ∨ x) ∧ (p 0 0 ∨ x) ∧ (p 1 a ∨ x) ∧
                   (p 0 1 ∨ ¬ x) ∧ (p 1 0 ∨ ¬ x) ∧ (p a b ∨ ¬ x)"
by (metis (full_types) pax)

declare [[metis_new_skolem]]

lemma "∃b. ∀a. ∃x. (p b a ∨ x) ∧ (p 0 0 ∨ x) ∧ (p 1 a ∨ x) ∧
                   (p 0 1 ∨ ¬ x) ∧ (p 1 0 ∨ ¬ x) ∧ (p a b ∨ ¬ x)"
by (metis pax)

lemma "∃b. ∀a. ∃x. (p b a ∨ x) ∧ (p 0 0 ∨ x) ∧ (p 1 a ∨ x) ∧
                   (p 0 1 ∨ ¬ x) ∧ (p 1 0 ∨ ¬ x) ∧ (p a b ∨ ¬ x)"
by (metis (full_types) pax)


text ‹New Skolemizer›

declare [[metis_new_skolem]]

lemma
  fixes x :: real
  assumes fn_le: "!!n. f n ≤ x" and 1: "f <---- lim f"
  shows "lim f ≤ x"
by (metis 1 LIMSEQ_le_const2 fn_le)

definition
  bounded :: "'a::metric_space set → bool" where
  "bounded S ⟷ (∃x eee. ∀y∈S. dist x y ≤ eee)"

lemma "bounded T ==> S ⊆ T ==> bounded S"
by (metis bounded_def subset_eq)

lemma
  assumes a: "Quotient R Abs Rep T"
  shows "symp R"
using a unfolding Quotient_def using sympI
by (metis (full_types))

lemma
  "(∃x ∈ set xs. P x) ⟷
   (∃ys x zs. xs = ys @ x # zs ∧ P x ∧ (∀z ∈ set zs. ¬ P z))"
by (metis split_list_last_prop[where P = P] in_set_conv_decomp)

lemma ex_tl: "∃ys. tl ys = xs"
using list.sel(3) by fast

lemma "(∃ys::nat list. tl ys = xs) ∧ (∃bs::int list. tl bs = as)"
by (metis ex_tl)

end