src/HOL/Metis_Examples/Clausification.thy
 author blanchet Thu Jan 03 13:28:37 2013 +0100 (2013-01-03) changeset 50696 85f944352d55 parent 47308 9caab698dbe4 child 50705 0e943b33d907 permissions -rw-r--r--
get rid of two-year-old hack, now that the "metis" skolemizer no longer gets stuck in HO unification
 blanchet@43197 1 (* Title: HOL/Metis_Examples/Clausification.thy blanchet@42338 2 Author: Jasmin Blanchette, TU Muenchen blanchet@42338 3 blanchet@43197 4 Example that exercises Metis's Clausifier. blanchet@42338 5 *) blanchet@42338 6 blanchet@43197 7 header {* Example that Exercises Metis's Clausifier *} blanchet@43197 8 blanchet@43197 9 theory Clausification blanchet@42338 10 imports Complex_Main blanchet@42338 11 begin blanchet@42338 12 blanchet@42747 13 blanchet@42345 14 text {* Definitional CNF for facts *} blanchet@42345 15 blanchet@42345 16 declare [[meson_max_clauses = 10]] blanchet@42345 17 blanchet@42345 18 axiomatization q :: "nat \ nat \ bool" where blanchet@42345 19 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 20 blanchet@42345 21 declare [[metis_new_skolemizer = false]] blanchet@42345 22 blanchet@42345 23 lemma "\b. \a. (q b a \ q a b)" blanchet@42345 24 by (metis qax) blanchet@42345 25 blanchet@42345 26 lemma "\b. \a. (q b a \ q a b)" blanchet@43228 27 by (metis (full_types) qax) blanchet@42345 28 blanchet@42345 29 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 30 by (metis qax) blanchet@42345 31 blanchet@42345 32 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@43228 33 by (metis (full_types) qax) blanchet@42345 34 blanchet@42345 35 declare [[metis_new_skolemizer]] blanchet@42345 36 blanchet@42345 37 lemma "\b. \a. (q b a \ q a b)" blanchet@42345 38 by (metis qax) blanchet@42345 39 blanchet@42345 40 lemma "\b. \a. (q b a \ q a b)" blanchet@43228 41 by (metis (full_types) qax) blanchet@42345 42 blanchet@42345 43 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 44 by (metis qax) blanchet@42345 45 blanchet@42345 46 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@43228 47 by (metis (full_types) qax) blanchet@42345 48 blanchet@42345 49 declare [[meson_max_clauses = 60]] blanchet@42345 50 blanchet@42345 51 axiomatization r :: "nat \ nat \ bool" where blanchet@42345 52 rax: "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ blanchet@42345 53 (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ blanchet@42345 54 (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ blanchet@42345 55 (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" blanchet@42345 56 blanchet@42345 57 declare [[metis_new_skolemizer = false]] blanchet@42345 58 blanchet@42345 59 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@42345 60 by (metis rax) blanchet@42345 61 blanchet@42345 62 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@43228 63 by (metis (full_types) rax) blanchet@42345 64 blanchet@42345 65 declare [[metis_new_skolemizer]] blanchet@42345 66 blanchet@42345 67 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@42345 68 by (metis rax) blanchet@42345 69 blanchet@42345 70 lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" blanchet@43228 71 by (metis (full_types) rax) blanchet@42345 72 blanchet@42350 73 lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ blanchet@42350 74 (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ blanchet@42350 75 (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ blanchet@42350 76 (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" blanchet@42350 77 by (metis rax) blanchet@42350 78 blanchet@42350 79 lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ blanchet@42350 80 (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ blanchet@42350 81 (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ blanchet@42350 82 (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" blanchet@43228 83 by (metis (full_types) rax) blanchet@42350 84 blanchet@42747 85 blanchet@42345 86 text {* Definitional CNF for goal *} blanchet@42345 87 blanchet@42338 88 axiomatization p :: "nat \ nat \ bool" where blanchet@42345 89 pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" blanchet@42338 90 blanchet@42338 91 declare [[metis_new_skolemizer = false]] blanchet@42338 92 blanchet@42338 93 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 94 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@42338 95 by (metis pax) blanchet@42338 96 blanchet@42338 97 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 98 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@43228 99 by (metis (full_types) pax) blanchet@42338 100 blanchet@42338 101 declare [[metis_new_skolemizer]] blanchet@42338 102 blanchet@42338 103 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 104 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@42338 105 by (metis pax) blanchet@42338 106 blanchet@42338 107 lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ blanchet@42338 108 (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" blanchet@43228 109 by (metis (full_types) pax) blanchet@42338 110 blanchet@42747 111 blanchet@42338 112 text {* New Skolemizer *} blanchet@42338 113 blanchet@42338 114 declare [[metis_new_skolemizer]] blanchet@42338 115 blanchet@42338 116 lemma blanchet@42338 117 fixes x :: real blanchet@42342 118 assumes fn_le: "!!n. f n \ x" and 1: "f ----> lim f" blanchet@42338 119 shows "lim f \ x" blanchet@42338 120 by (metis 1 LIMSEQ_le_const2 fn_le) blanchet@42338 121 blanchet@42338 122 definition blanchet@42338 123 bounded :: "'a::metric_space set \ bool" where blanchet@42338 124 "bounded S \ (\x eee. \y\S. dist x y \ eee)" blanchet@42338 125 blanchet@42338 126 lemma "bounded T \ S \ T ==> bounded S" blanchet@42338 127 by (metis bounded_def subset_eq) blanchet@42338 128 blanchet@42338 129 lemma kuncar@47308 130 assumes a: "Quotient R Abs Rep T" blanchet@42338 131 shows "symp R" blanchet@42338 132 using a unfolding Quotient_def using sympI blanchet@43228 133 by (metis (full_types)) blanchet@42338 134 blanchet@42338 135 lemma blanchet@42338 136 "(\x \ set xs. P x) \ blanchet@42342 137 (\ys x zs. xs = ys @ x # zs \ P x \ (\z \ set zs. \ P z))" blanchet@50696 138 by (metis split_list_last_prop[where P = P] in_set_conv_decomp) blanchet@42338 139 blanchet@42342 140 lemma ex_tl: "EX ys. tl ys = xs" blanchet@42342 141 using tl.simps(2) by fast blanchet@42342 142 blanchet@42342 143 lemma "(\ys\nat list. tl ys = xs) \ (\bs\int list. tl bs = as)" blanchet@42342 144 by (metis ex_tl) blanchet@42342 145 blanchet@42338 146 end