src/HOL/Metis_Examples/Clausify.thy
 author blanchet Thu Apr 14 11:24:05 2011 +0200 (2011-04-14) changeset 42345 5ecd55993606 parent 42343 118cc349de35 child 42350 128dc0fa87fc permissions -rw-r--r--
added examples of definitional CNF facts
 blanchet@42343 1 (* Title: HOL/Metis_Examples/Clausify.thy blanchet@42338 2 Author: Jasmin Blanchette, TU Muenchen blanchet@42338 3 blanchet@42338 4 Testing Metis's clausifier. blanchet@42338 5 *) blanchet@42338 6 blanchet@42343 7 theory Clausify blanchet@42338 8 imports Complex_Main blanchet@42338 9 begin blanchet@42338 10 blanchet@42338 11 (* FIXME: shouldn't need this *) blanchet@42338 12 declare [[unify_search_bound = 100]] blanchet@42338 13 declare [[unify_trace_bound = 100]] blanchet@42338 14 blanchet@42345 15 text {* Definitional CNF for facts *} blanchet@42345 16 blanchet@42345 17 declare [[meson_max_clauses = 10]] blanchet@42345 18 blanchet@42345 19 axiomatization q :: "nat \ nat \ bool" where blanchet@42345 20 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)" blanchet@42345 21 blanchet@42345 22 declare [[metis_new_skolemizer = false]] blanchet@42345 23 blanchet@42345 24 lemma "\b. \a. (q b a \ q a b)" blanchet@42345 25 by (metis qax) blanchet@42345 26 blanchet@42345 27 lemma "\b. \a. (q b a \ q a b)" blanchet@42345 28 by (metisFT qax) blanchet@42345 29 blanchet@42345 30 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)" blanchet@42345 31 by (metis qax) blanchet@42345 32 blanchet@42345 33 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)" blanchet@42345 34 by (metisFT qax) blanchet@42345 35 blanchet@42345 36 declare [[metis_new_skolemizer]] blanchet@42345 37 blanchet@42345 38 lemma "\b. \a. (q b a \ q a b)" blanchet@42345 39 by (metis qax) blanchet@42345 40 blanchet@42345 41 lemma "\b. \a. (q b a \ q a b)" blanchet@42345 42 by (metisFT qax) blanchet@42345 43 blanchet@42345 44 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)" blanchet@42345 45 by (metis qax) blanchet@42345 46 blanchet@42345 47 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)" blanchet@42345 48 by (metisFT qax) blanchet@42345 49 blanchet@42345 50 declare [[meson_max_clauses = 60]] blanchet@42345 51 blanchet@42345 52 axiomatization r :: "nat \ nat \ bool" where blanchet@42345 53 rax: "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ blanchet@42345 54 (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ blanchet@42345 55 (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ blanchet@42345 56 (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" blanchet@42345 57 blanchet@42345 58 declare [[metis_new_skolemizer = false]] blanchet@42345 59 blanchet@42345 60 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@42345 61 by (metis rax) blanchet@42345 62 blanchet@42345 63 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@42345 64 by (metisFT rax) blanchet@42345 65 blanchet@42345 66 declare [[metis_new_skolemizer]] blanchet@42345 67 blanchet@42345 68 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@42345 69 by (metis rax) blanchet@42345 70 blanchet@42345 71 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@42345 72 by (metisFT rax) blanchet@42345 73 blanchet@42345 74 text {* Definitional CNF for goal *} blanchet@42345 75 blanchet@42338 76 axiomatization p :: "nat \ nat \ bool" where blanchet@42345 77 pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" blanchet@42338 78 blanchet@42338 79 declare [[metis_new_skolemizer = false]] blanchet@42338 80 blanchet@42338 81 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 82 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@42338 83 by (metis pax) blanchet@42338 84 blanchet@42338 85 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 86 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@42338 87 by (metisFT pax) blanchet@42338 88 blanchet@42338 89 declare [[metis_new_skolemizer]] blanchet@42338 90 blanchet@42338 91 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 92 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@42338 93 by (metis pax) blanchet@42338 94 blanchet@42338 95 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 96 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@42338 97 by (metisFT pax) blanchet@42338 98 blanchet@42338 99 text {* New Skolemizer *} blanchet@42338 100 blanchet@42338 101 declare [[metis_new_skolemizer]] blanchet@42338 102 blanchet@42338 103 lemma blanchet@42338 104 fixes x :: real blanchet@42342 105 assumes fn_le: "!!n. f n \ x" and 1: "f ----> lim f" blanchet@42338 106 shows "lim f \ x" blanchet@42338 107 by (metis 1 LIMSEQ_le_const2 fn_le) blanchet@42338 108 blanchet@42338 109 definition blanchet@42338 110 bounded :: "'a::metric_space set \ bool" where blanchet@42338 111 "bounded S \ (\x eee. \y\S. dist x y \ eee)" blanchet@42338 112 blanchet@42338 113 lemma "bounded T \ S \ T ==> bounded S" blanchet@42338 114 by (metis bounded_def subset_eq) blanchet@42338 115 blanchet@42338 116 lemma blanchet@42338 117 assumes a: "Quotient R Abs Rep" blanchet@42338 118 shows "symp R" blanchet@42338 119 using a unfolding Quotient_def using sympI blanchet@42338 120 by metisFT blanchet@42338 121 blanchet@42338 122 lemma blanchet@42338 123 "(\x \ set xs. P x) \ blanchet@42342 124 (\ys x zs. xs = ys @ x # zs \ P x \ (\z \ set zs. \ P z))" blanchet@42338 125 by (metis split_list_last_prop [where P = P] in_set_conv_decomp) blanchet@42338 126 blanchet@42342 127 lemma ex_tl: "EX ys. tl ys = xs" blanchet@42342 128 using tl.simps(2) by fast blanchet@42342 129 blanchet@42342 130 lemma "(\ys\nat list. tl ys = xs) \ (\bs\int list. tl bs = as)" blanchet@42342 131 by (metis ex_tl) blanchet@42342 132 blanchet@42338 133 end