# HG changeset patch # User blanchet # Date 1302773045 -7200 # Node ID 5ecd559936067b7f85816851c8236eaa50fba2f4 # Parent 4a58173ffb99568f54ad37e28173e474cc604c3d added examples of definitional CNF facts diff -r 4a58173ffb99 -r 5ecd55993606 src/HOL/Metis_Examples/Clausify.thy --- a/src/HOL/Metis_Examples/Clausify.thy Thu Apr 14 11:24:05 2011 +0200 +++ b/src/HOL/Metis_Examples/Clausify.thy Thu Apr 14 11:24:05 2011 +0200 @@ -8,14 +8,73 @@ imports Complex_Main begin -text {* Definitional CNF for goal *} - (* FIXME: shouldn't need this *) declare [[unify_search_bound = 100]] declare [[unify_trace_bound = 100]] +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_skolemizer = false]] + +lemma "\b. \a. (q b a \ q a b)" +by (metis qax) + +lemma "\b. \a. (q b a \ q a b)" +by (metisFT 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 (metisFT qax) + +declare [[metis_new_skolemizer]] + +lemma "\b. \a. (q b a \ q a b)" +by (metis qax) + +lemma "\b. \a. (q b a \ q a b)" +by (metisFT 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 (metisFT 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_skolemizer = 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 (metisFT rax) + +declare [[metis_new_skolemizer]] + +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 (metisFT 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))" +pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" declare [[metis_new_skolemizer = false]]