products/Sources/formale Sprachen/COBOL/Test-Suite/SQL P/dml100-186/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: gui_Graphics.vdmpp   Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.3 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff