Theory Clausification

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

Example that exercises Metis's Clausifier.
*)


header {* 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: "EX ys. tl ys = xs"
using tl.simps(2) by fast

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

end