(* Title: HOL/Metis_Examples/Clausification.thy
Author: Jasmin Blanchette, TU Muenchen
Example that exercises Metis's Clausifier.
*)
section \<open>Example that Exercises Metis's Clausifier\<close>
theory Clausification
imports Complex_Main
begin
text \<open>Definitional CNF for facts\<close>
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 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> 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 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
by (metis rax)
lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \
(r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
by (metis (full_types) rax)
text \<open>Definitional CNF for goal\<close>
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 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
by (metis pax)
lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> 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 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
by (metis pax)
lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
by (metis (full_types) pax)
text \<open>New Skolemizer\<close>
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) \
(\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> 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
¤ Dauer der Verarbeitung: 0.30 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
