src/HOL/Metis_Examples/Clausification.thy
 author blanchet Mon Jun 06 20:36:35 2011 +0200 (2011-06-06) changeset 43197 c71657bbdbc0 parent 42756 src/HOL/Metis_Examples/Clausify.thy@6b7ef9b724fd child 43228 2ed2f092e990 permissions -rw-r--r--
tuned Metis examples
 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@42338 ` 13` ```(* FIXME: shouldn't need this *) ``` blanchet@42338 ` 14` ```declare [[unify_search_bound = 100]] ``` blanchet@42338 ` 15` ```declare [[unify_trace_bound = 100]] ``` blanchet@42338 ` 16` blanchet@42747 ` 17` blanchet@42345 ` 18` ```text {* Definitional CNF for facts *} ``` blanchet@42345 ` 19` blanchet@42345 ` 20` ```declare [[meson_max_clauses = 10]] ``` blanchet@42345 ` 21` blanchet@42345 ` 22` ```axiomatization q :: "nat \ nat \ bool" where ``` blanchet@42345 ` 23` ```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 ` 24` blanchet@42345 ` 25` ```declare [[metis_new_skolemizer = false]] ``` blanchet@42345 ` 26` blanchet@42345 ` 27` ```lemma "\b. \a. (q b a \ q a b)" ``` blanchet@42345 ` 28` ```by (metis qax) ``` blanchet@42345 ` 29` blanchet@42345 ` 30` ```lemma "\b. \a. (q b a \ q a b)" ``` blanchet@42345 ` 31` ```by (metisFT 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 (metis qax) ``` blanchet@42345 ` 35` blanchet@42345 ` 36` ```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 ` 37` ```by (metisFT qax) ``` blanchet@42345 ` 38` blanchet@42345 ` 39` ```declare [[metis_new_skolemizer]] ``` blanchet@42345 ` 40` blanchet@42345 ` 41` ```lemma "\b. \a. (q b a \ q a b)" ``` blanchet@42345 ` 42` ```by (metis qax) ``` blanchet@42345 ` 43` blanchet@42345 ` 44` ```lemma "\b. \a. (q b a \ q a b)" ``` blanchet@42345 ` 45` ```by (metisFT 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 (metis qax) ``` blanchet@42345 ` 49` blanchet@42345 ` 50` ```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 ` 51` ```by (metisFT qax) ``` blanchet@42345 ` 52` blanchet@42345 ` 53` ```declare [[meson_max_clauses = 60]] ``` blanchet@42345 ` 54` blanchet@42345 ` 55` ```axiomatization r :: "nat \ nat \ bool" where ``` blanchet@42345 ` 56` ```rax: "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ ``` blanchet@42345 ` 57` ``` (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ ``` blanchet@42345 ` 58` ``` (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ ``` blanchet@42345 ` 59` ``` (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" ``` blanchet@42345 ` 60` blanchet@42345 ` 61` ```declare [[metis_new_skolemizer = false]] ``` blanchet@42345 ` 62` blanchet@42345 ` 63` ```lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" ``` blanchet@42345 ` 64` ```by (metis rax) ``` blanchet@42345 ` 65` blanchet@42345 ` 66` ```lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" ``` blanchet@42345 ` 67` ```by (metisFT rax) ``` blanchet@42345 ` 68` blanchet@42345 ` 69` ```declare [[metis_new_skolemizer]] ``` blanchet@42345 ` 70` blanchet@42345 ` 71` ```lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" ``` blanchet@42345 ` 72` ```by (metis rax) ``` blanchet@42345 ` 73` blanchet@42345 ` 74` ```lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" ``` blanchet@42345 ` 75` ```by (metisFT rax) ``` blanchet@42345 ` 76` blanchet@42350 ` 77` ```lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ ``` blanchet@42350 ` 78` ``` (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ ``` blanchet@42350 ` 79` ``` (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ ``` blanchet@42350 ` 80` ``` (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" ``` blanchet@42350 ` 81` ```by (metis rax) ``` blanchet@42350 ` 82` blanchet@42350 ` 83` ```lemma "(r 0 0 \ r 0 1 \ r 0 2 \ r 0 3) \ ``` blanchet@42350 ` 84` ``` (r 1 0 \ r 1 1 \ r 1 2 \ r 1 3) \ ``` blanchet@42350 ` 85` ``` (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ ``` blanchet@42350 ` 86` ``` (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" ``` blanchet@42350 ` 87` ```by (metisFT rax) ``` blanchet@42350 ` 88` blanchet@42747 ` 89` blanchet@42345 ` 90` ```text {* Definitional CNF for goal *} ``` blanchet@42345 ` 91` blanchet@42338 ` 92` ```axiomatization p :: "nat \ nat \ bool" where ``` blanchet@42345 ` 93` ```pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" ``` blanchet@42338 ` 94` blanchet@42338 ` 95` ```declare [[metis_new_skolemizer = false]] ``` 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@42338 ` 99` ```by (metis pax) ``` blanchet@42338 ` 100` blanchet@42338 ` 101` ```lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ ``` blanchet@42338 ` 102` ``` (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" ``` blanchet@42338 ` 103` ```by (metisFT pax) ``` blanchet@42338 ` 104` blanchet@42338 ` 105` ```declare [[metis_new_skolemizer]] ``` 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@42338 ` 109` ```by (metis pax) ``` blanchet@42338 ` 110` blanchet@42338 ` 111` ```lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ ``` blanchet@42338 ` 112` ``` (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" ``` blanchet@42338 ` 113` ```by (metisFT pax) ``` blanchet@42338 ` 114` blanchet@42747 ` 115` blanchet@42338 ` 116` ```text {* New Skolemizer *} ``` blanchet@42338 ` 117` blanchet@42338 ` 118` ```declare [[metis_new_skolemizer]] ``` blanchet@42338 ` 119` blanchet@42338 ` 120` ```lemma ``` blanchet@42338 ` 121` ``` fixes x :: real ``` blanchet@42342 ` 122` ``` assumes fn_le: "!!n. f n \ x" and 1: "f ----> lim f" ``` blanchet@42338 ` 123` ``` shows "lim f \ x" ``` blanchet@42338 ` 124` ```by (metis 1 LIMSEQ_le_const2 fn_le) ``` blanchet@42338 ` 125` blanchet@42338 ` 126` ```definition ``` blanchet@42338 ` 127` ``` bounded :: "'a::metric_space set \ bool" where ``` blanchet@42338 ` 128` ``` "bounded S \ (\x eee. \y\S. dist x y \ eee)" ``` blanchet@42338 ` 129` blanchet@42338 ` 130` ```lemma "bounded T \ S \ T ==> bounded S" ``` blanchet@42338 ` 131` ```by (metis bounded_def subset_eq) ``` blanchet@42338 ` 132` blanchet@42338 ` 133` ```lemma ``` blanchet@42338 ` 134` ``` assumes a: "Quotient R Abs Rep" ``` blanchet@42338 ` 135` ``` shows "symp R" ``` blanchet@42338 ` 136` ```using a unfolding Quotient_def using sympI ``` blanchet@42338 ` 137` ```by metisFT ``` blanchet@42338 ` 138` blanchet@42338 ` 139` ```lemma ``` blanchet@42338 ` 140` ``` "(\x \ set xs. P x) \ ``` blanchet@42342 ` 141` ``` (\ys x zs. xs = ys @ x # zs \ P x \ (\z \ set zs. \ P z))" ``` blanchet@42338 ` 142` ```by (metis split_list_last_prop [where P = P] in_set_conv_decomp) ``` blanchet@42338 ` 143` blanchet@42342 ` 144` ```lemma ex_tl: "EX ys. tl ys = xs" ``` blanchet@42342 ` 145` ```using tl.simps(2) by fast ``` blanchet@42342 ` 146` blanchet@42342 ` 147` ```lemma "(\ys\nat list. tl ys = xs) \ (\bs\int list. tl bs = as)" ``` blanchet@42342 ` 148` ```by (metis ex_tl) ``` blanchet@42342 ` 149` blanchet@42338 ` 150` ```end ```