Quelle Clausification.thy Sprache: Isabelle

(*  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

quality98%

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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:

sprechenden Kalenders