src/HOL/Nitpick_Examples/Integer_Nits.thy
 author wenzelm Tue Sep 03 01:12:40 2013 +0200 (2013-09-03) changeset 53374 a14d2a854c02 parent 48812 9509fc5485b2 child 54633 86e0b402994c permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
 blanchet@34126 ` 1` ```(* Title: HOL/Nitpick_Examples/Integer_Nits.thy ``` blanchet@34126 ` 2` ``` Author: Jasmin Blanchette, TU Muenchen ``` blanchet@48812 ` 3` ``` Copyright 2009-2012 ``` blanchet@34126 ` 4` blanchet@34126 ` 5` ```Examples featuring Nitpick applied to natural numbers and integers. ``` blanchet@34126 ` 6` ```*) ``` blanchet@34126 ` 7` blanchet@46090 ` 8` ```header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} ``` blanchet@34126 ` 9` blanchet@34126 ` 10` ```theory Integer_Nits ``` blanchet@46090 ` 11` ```imports Main ``` blanchet@34126 ` 12` ```begin ``` blanchet@34126 ` 13` blanchet@42959 ` 14` ```nitpick_params [verbose, card = 1\5, bits = 1,2,3,4,6, ``` krauss@42208 ` 15` ``` sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] ``` blanchet@34126 ` 16` blanchet@34126 ` 17` ```lemma "Suc x = x + 1" ``` blanchet@34126 ` 18` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 19` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 20` ```sorry ``` blanchet@34126 ` 21` blanchet@34126 ` 22` ```lemma "x < Suc x" ``` blanchet@34126 ` 23` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 24` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 25` ```sorry ``` blanchet@34126 ` 26` blanchet@34126 ` 27` ```lemma "x + y \ (x::nat)" ``` blanchet@34126 ` 28` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 29` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 30` ```sorry ``` blanchet@34126 ` 31` blanchet@34126 ` 32` ```lemma "y \ 0 \ x + y > (x::nat)" ``` blanchet@34126 ` 33` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 34` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 35` ```sorry ``` blanchet@34126 ` 36` blanchet@34126 ` 37` ```lemma "x + y = y + (x::nat)" ``` blanchet@34126 ` 38` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 39` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 40` ```sorry ``` blanchet@34126 ` 41` blanchet@34126 ` 42` ```lemma "x > y \ x - y \ (0::nat)" ``` blanchet@34126 ` 43` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 44` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 45` ```sorry ``` blanchet@34126 ` 46` blanchet@34126 ` 47` ```lemma "x \ y \ x - y = (0::nat)" ``` blanchet@34126 ` 48` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 49` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 50` ```sorry ``` blanchet@34126 ` 51` blanchet@34126 ` 52` ```lemma "x - (0::nat) = x" ``` blanchet@34126 ` 53` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 54` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 55` ```sorry ``` blanchet@34126 ` 56` blanchet@34126 ` 57` ```lemma "\x \ 0; y \ 0\ \ x * y \ (0::nat)" ``` blanchet@34126 ` 58` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 59` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 60` ```sorry ``` blanchet@34126 ` 61` blanchet@34126 ` 62` ```lemma "0 * y = (0::nat)" ``` blanchet@34126 ` 63` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 64` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 65` ```sorry ``` blanchet@34126 ` 66` blanchet@34126 ` 67` ```lemma "y * 0 = (0::nat)" ``` blanchet@34126 ` 68` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 69` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 70` ```sorry ``` blanchet@34126 ` 71` blanchet@34126 ` 72` ```lemma "\x \ 0; y \ 0\ \ x * y \ (x::nat)" ``` blanchet@34126 ` 73` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 74` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 75` ```sorry ``` blanchet@34126 ` 76` blanchet@34126 ` 77` ```lemma "\x \ 0; y \ 0\ \ x * y \ (y::nat)" ``` blanchet@34126 ` 78` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 79` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 80` ```sorry ``` blanchet@34126 ` 81` blanchet@34126 ` 82` ```lemma "x * y div y = (x::nat)" ``` blanchet@34126 ` 83` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 84` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 85` ```oops ``` blanchet@34126 ` 86` blanchet@34126 ` 87` ```lemma "y \ 0 \ x * y div y = (x::nat)" ``` blanchet@34126 ` 88` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 89` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 90` ```sorry ``` blanchet@34126 ` 91` blanchet@34126 ` 92` ```lemma "5 * 55 < (260::nat)" ``` blanchet@34126 ` 93` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 94` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 95` ```nitpick [binary_ints, bits = 9, expect = genuine] ``` blanchet@34126 ` 96` ```oops ``` blanchet@34126 ` 97` blanchet@34126 ` 98` ```lemma "nat (of_nat n) = n" ``` blanchet@34126 ` 99` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 100` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 101` ```sorry ``` blanchet@34126 ` 102` blanchet@34126 ` 103` ```lemma "x + y \ (x::int)" ``` blanchet@34126 ` 104` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 105` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 106` ```oops ``` blanchet@34126 ` 107` blanchet@34126 ` 108` ```lemma "\x \ 0; y \ 0\ \ x + y \ (0::int)" ``` blanchet@34126 ` 109` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 110` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 111` ```sorry ``` blanchet@34126 ` 112` blanchet@34126 ` 113` ```lemma "y \ 0 \ x + y \ (x::int)" ``` blanchet@34126 ` 114` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 115` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 116` ```sorry ``` blanchet@34126 ` 117` blanchet@34126 ` 118` ```lemma "x \ 0 \ x + y \ (y::int)" ``` blanchet@34126 ` 119` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 120` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 121` ```sorry ``` blanchet@34126 ` 122` blanchet@34126 ` 123` ```lemma "x \ 0 \ x + y \ (x::int)" ``` blanchet@34126 ` 124` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 125` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 126` ```oops ``` blanchet@34126 ` 127` blanchet@34126 ` 128` ```lemma "\x \ 0; y \ 0\ \ x + y \ (0::int)" ``` blanchet@34126 ` 129` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 130` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 131` ```sorry ``` blanchet@34126 ` 132` blanchet@34126 ` 133` ```lemma "y \ 0 \ x + y > (x::int)" ``` blanchet@34126 ` 134` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 135` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 136` ```oops ``` blanchet@34126 ` 137` blanchet@34126 ` 138` ```lemma "x + y = y + (x::int)" ``` blanchet@34126 ` 139` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 140` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 141` ```sorry ``` blanchet@34126 ` 142` blanchet@34126 ` 143` ```lemma "x > y \ x - y \ (0::int)" ``` blanchet@34126 ` 144` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 145` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 146` ```sorry ``` blanchet@34126 ` 147` blanchet@34126 ` 148` ```lemma "x \ y \ x - y = (0::int)" ``` blanchet@34126 ` 149` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 150` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 151` ```oops ``` blanchet@34126 ` 152` blanchet@34126 ` 153` ```lemma "x - (0::int) = x" ``` blanchet@34126 ` 154` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 155` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 156` ```sorry ``` blanchet@34126 ` 157` blanchet@34126 ` 158` ```lemma "\x \ 0; y \ 0\ \ x * y \ (0::int)" ``` blanchet@34126 ` 159` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 160` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 161` ```sorry ``` blanchet@34126 ` 162` blanchet@34126 ` 163` ```lemma "0 * y = (0::int)" ``` blanchet@34126 ` 164` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 165` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 166` ```sorry ``` blanchet@34126 ` 167` blanchet@34126 ` 168` ```lemma "y * 0 = (0::int)" ``` blanchet@34126 ` 169` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 170` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 171` ```sorry ``` blanchet@34126 ` 172` blanchet@34126 ` 173` ```lemma "\x \ 0; y \ 0\ \ x * y \ (x::int)" ``` blanchet@34126 ` 174` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 175` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 176` ```oops ``` blanchet@34126 ` 177` blanchet@34126 ` 178` ```lemma "\x \ 0; y \ 0\ \ x * y \ (y::int)" ``` blanchet@34126 ` 179` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 180` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 181` ```oops ``` blanchet@34126 ` 182` blanchet@34126 ` 183` ```lemma "x * y div y = (x::int)" ``` blanchet@34126 ` 184` ```nitpick [unary_ints, expect = genuine] ``` blanchet@34126 ` 185` ```nitpick [binary_ints, expect = genuine] ``` blanchet@34126 ` 186` ```oops ``` blanchet@34126 ` 187` blanchet@34126 ` 188` ```lemma "y \ 0 \ x * y div y = (x::int)" ``` blanchet@34126 ` 189` ```nitpick [unary_ints, expect = none] ``` blanchet@42959 ` 190` ```nitpick [binary_ints, card = 1\4, bits = 1\4, expect = none] ``` blanchet@34126 ` 191` ```sorry ``` blanchet@34126 ` 192` blanchet@34126 ` 193` ```lemma "(x * y < 0) \ (x > 0 \ y < 0) \ (x < 0 \ y > (0::int))" ``` blanchet@34126 ` 194` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 195` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 196` ```sorry ``` blanchet@34126 ` 197` blanchet@34126 ` 198` ```lemma "-5 * 55 > (-260::int)" ``` blanchet@34126 ` 199` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 200` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 201` ```nitpick [binary_ints, bits = 9, expect = genuine] ``` blanchet@34126 ` 202` ```oops ``` blanchet@34126 ` 203` blanchet@34126 ` 204` ```lemma "nat (of_nat n) = n" ``` blanchet@34126 ` 205` ```nitpick [unary_ints, expect = none] ``` blanchet@34126 ` 206` ```nitpick [binary_ints, expect = none] ``` blanchet@34126 ` 207` ```sorry ``` blanchet@34126 ` 208` blanchet@35695 ` 209` ```datatype tree = Null | Node nat tree tree ``` blanchet@35695 ` 210` blanchet@35695 ` 211` ```primrec labels where ``` blanchet@35695 ` 212` ```"labels Null = {}" | ``` blanchet@35695 ` 213` ```"labels (Node x t u) = {x} \ labels t \ labels u" ``` blanchet@35695 ` 214` blanchet@35695 ` 215` ```lemma "labels (Node x t u) \ labels (Node y v w)" ``` blanchet@37477 ` 216` ```nitpick [expect = potential] (* unfortunate *) ``` blanchet@35695 ` 217` ```oops ``` blanchet@35695 ` 218` blanchet@35695 ` 219` ```lemma "labels (Node x t u) \ {}" ``` blanchet@35695 ` 220` ```nitpick [expect = none] ``` blanchet@35695 ` 221` ```oops ``` blanchet@35695 ` 222` blanchet@35695 ` 223` ```lemma "card (labels t) > 0" ``` blanchet@37477 ` 224` ```nitpick [expect = potential] (* unfortunate *) ``` blanchet@35695 ` 225` ```oops ``` blanchet@35695 ` 226` blanchet@35695 ` 227` ```lemma "(\n \ labels t. n + 2) \ 2" ``` blanchet@37477 ` 228` ```nitpick [expect = potential] (* unfortunate *) ``` blanchet@35695 ` 229` ```oops ``` blanchet@35695 ` 230` blanchet@35695 ` 231` ```lemma "t \ Null \ (\n \ labels t. n + 2) \ 2" ``` blanchet@39362 ` 232` ```nitpick [expect = potential] (* unfortunate *) ``` blanchet@35695 ` 233` ```sorry ``` blanchet@35695 ` 234` blanchet@35695 ` 235` ```lemma "(\i \ labels (Node x t u). f i\nat) = f x + (\i \ labels t. f i) + (\i \ labels u. f i)" ``` blanchet@39362 ` 236` ```nitpick [expect = potential] (* unfortunate *) ``` blanchet@35695 ` 237` ```oops ``` blanchet@35695 ` 238` blanchet@34126 ` 239` ```end ```