src/HOL/Metis_Examples/Clausification.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 55417 01fbfb60c33e child 61076 bdc1e2f0a86a permissions -rw-r--r--
 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` wenzelm@58889 ` 7` ```section {* 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@50705 ` 21` ```declare [[metis_new_skolem = 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@50705 ` 35` ```declare [[metis_new_skolem]] ``` 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@50705 ` 57` ```declare [[metis_new_skolem = 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@50705 ` 65` ```declare [[metis_new_skolem]] ``` 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@50705 ` 91` ```declare [[metis_new_skolem = 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@50705 ` 101` ```declare [[metis_new_skolem]] ``` 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@50705 ` 114` ```declare [[metis_new_skolem]] ``` 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@55417 ` 141` ```using list.sel(3) 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 ```