src/HOL/Nitpick_Examples/Mini_Nits.thy
 author hoelzl Tue Jan 18 21:37:23 2011 +0100 (2011-01-18) changeset 41654 32fe42892983 parent 37495 650fae5eea93 permissions -rw-r--r--
Gauge measure removed
 blanchet@33197 ` 1` ```(* Title: HOL/Nitpick_Examples/Mini_Nits.thy ``` blanchet@33197 ` 2` ``` Author: Jasmin Blanchette, TU Muenchen ``` blanchet@35076 ` 3` ``` Copyright 2009, 2010 ``` blanchet@33197 ` 4` blanchet@33197 ` 5` ```Examples featuring Minipick, the minimalistic version of Nitpick. ``` blanchet@33197 ` 6` ```*) ``` blanchet@33197 ` 7` blanchet@33197 ` 8` ```header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *} ``` blanchet@33197 ` 9` blanchet@33197 ` 10` ```theory Mini_Nits ``` blanchet@33197 ` 11` ```imports Main ``` blanchet@33197 ` 12` ```begin ``` blanchet@33197 ` 13` blanchet@33197 ` 14` ```ML {* ``` blanchet@33197 ` 15` ```exception FAIL ``` blanchet@33197 ` 16` blanchet@37495 ` 17` ```val has_kodkodi = (getenv "KODKODI" <> "") ``` blanchet@37495 ` 18` blanchet@35284 ` 19` ```fun minipick n t = ``` blanchet@35284 ` 20` ``` map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n) ``` blanchet@35284 ` 21` ``` |> Minipick.solve_any_kodkod_problem @{theory} ``` blanchet@37495 ` 22` ```fun minipick_expect expect n t = ``` blanchet@37495 ` 23` ``` if has_kodkodi then ``` blanchet@37495 ` 24` ``` if minipick n t = expect then () else raise FAIL ``` blanchet@37495 ` 25` ``` else ``` blanchet@37495 ` 26` ``` () ``` blanchet@37495 ` 27` ```val none = minipick_expect "none" ``` blanchet@37495 ` 28` ```val genuine = minipick_expect "genuine" ``` blanchet@37495 ` 29` ```val unknown = minipick_expect "unknown" ``` blanchet@33197 ` 30` ```*} ``` blanchet@33197 ` 31` blanchet@33197 ` 32` ```ML {* genuine 1 @{prop "x = Not"} *} ``` blanchet@33197 ` 33` ```ML {* none 1 @{prop "\x. x = Not"} *} ``` blanchet@33197 ` 34` ```ML {* none 1 @{prop "\ False"} *} ``` blanchet@33197 ` 35` ```ML {* genuine 1 @{prop "\ True"} *} ``` blanchet@33197 ` 36` ```ML {* none 1 @{prop "\ \ b \ b"} *} ``` blanchet@33197 ` 37` ```ML {* none 1 @{prop True} *} ``` blanchet@33197 ` 38` ```ML {* genuine 1 @{prop False} *} ``` blanchet@33197 ` 39` ```ML {* genuine 1 @{prop "True \ False"} *} ``` blanchet@33197 ` 40` ```ML {* none 1 @{prop "True \ \ False"} *} ``` blanchet@33197 ` 41` ```ML {* none 5 @{prop "\x. x = x"} *} ``` blanchet@33197 ` 42` ```ML {* none 5 @{prop "\x. x = x"} *} ``` blanchet@33197 ` 43` ```ML {* none 1 @{prop "\x. x = y"} *} ``` blanchet@33197 ` 44` ```ML {* genuine 2 @{prop "\x. x = y"} *} ``` blanchet@33197 ` 45` ```ML {* none 1 @{prop "\x. x = y"} *} ``` blanchet@33197 ` 46` ```ML {* none 2 @{prop "\x. x = y"} *} ``` blanchet@33197 ` 47` ```ML {* none 2 @{prop "\x\'a \ 'a. x = x"} *} ``` blanchet@33197 ` 48` ```ML {* none 2 @{prop "\x\'a \ 'a. x = y"} *} ``` blanchet@33197 ` 49` ```ML {* genuine 2 @{prop "\x\'a \ 'a. x = y"} *} ``` blanchet@33197 ` 50` ```ML {* none 2 @{prop "\x\'a \ 'a. x = y"} *} ``` blanchet@33197 ` 51` ```ML {* none 1 @{prop "All = Ex"} *} ``` blanchet@33197 ` 52` ```ML {* genuine 2 @{prop "All = Ex"} *} ``` blanchet@33197 ` 53` ```ML {* none 1 @{prop "All P = Ex P"} *} ``` blanchet@33197 ` 54` ```ML {* genuine 2 @{prop "All P = Ex P"} *} ``` blanchet@33197 ` 55` ```ML {* none 5 @{prop "x = y \ P x = P y"} *} ``` blanchet@33197 ` 56` ```ML {* none 5 @{prop "(x\'a \ 'a) = y \ P x = P y"} *} ``` blanchet@33197 ` 57` ```ML {* none 2 @{prop "(x\'a \ 'a) = y \ P x y = P y x"} *} ``` blanchet@33197 ` 58` ```ML {* none 5 @{prop "\x\'a \ 'a. x = y \ P x = P y"} *} ``` blanchet@33197 ` 59` ```ML {* none 2 @{prop "(x\'a \ 'a) = y \ P x = P y"} *} ``` blanchet@33197 ` 60` ```ML {* none 2 @{prop "\x\'a \ 'a. x = y \ P x = P y"} *} ``` blanchet@33197 ` 61` ```ML {* genuine 1 @{prop "(op =) X = Ex"} *} ``` blanchet@33197 ` 62` ```ML {* none 2 @{prop "\x::'a \ 'a. x = x"} *} ``` blanchet@33197 ` 63` ```ML {* none 1 @{prop "x = y"} *} ``` blanchet@33197 ` 64` ```ML {* genuine 1 @{prop "x \ y"} *} ``` blanchet@33197 ` 65` ```ML {* genuine 2 @{prop "x = y"} *} ``` blanchet@33197 ` 66` ```ML {* genuine 1 @{prop "X \ Y"} *} ``` blanchet@33197 ` 67` ```ML {* none 1 @{prop "P \ Q \ Q \ P"} *} ``` blanchet@33197 ` 68` ```ML {* none 1 @{prop "P \ Q \ P"} *} ``` blanchet@33197 ` 69` ```ML {* none 1 @{prop "P \ Q \ Q \ P"} *} ``` blanchet@33197 ` 70` ```ML {* genuine 1 @{prop "P \ Q \ P"} *} ``` blanchet@33197 ` 71` ```ML {* none 1 @{prop "(P \ Q) \ (\ P \ Q)"} *} ``` blanchet@33197 ` 72` ```ML {* none 5 @{prop "{a} = {a, a}"} *} ``` blanchet@33197 ` 73` ```ML {* genuine 2 @{prop "{a} = {a, b}"} *} ``` blanchet@33197 ` 74` ```ML {* genuine 1 @{prop "{a} \ {a, b}"} *} ``` blanchet@33197 ` 75` ```ML {* none 5 @{prop "{}\<^sup>+ = {}"} *} ``` blanchet@33197 ` 76` ```ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *} ``` blanchet@33197 ` 77` ```ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *} ``` blanchet@33197 ` 78` ```ML {* none 5 @{prop "a \ c \ {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *} ``` blanchet@33197 ` 79` ```ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} ``` blanchet@33197 ` 80` ```ML {* none 5 @{prop "A \ B = (\x. A x \ B x)"} *} ``` blanchet@33197 ` 81` ```ML {* none 5 @{prop "A - B = (\x. A x \ \ B x)"} *} ``` blanchet@33197 ` 82` ```ML {* none 5 @{prop "\a b. (a, b) = (b, a)"} *} ``` blanchet@33197 ` 83` ```ML {* genuine 2 @{prop "(a, b) = (b, a)"} *} ``` blanchet@33197 ` 84` ```ML {* genuine 2 @{prop "(a, b) \ (b, a)"} *} ``` blanchet@33197 ` 85` ```ML {* none 5 @{prop "\a b\'a \ 'a. (a, b) = (b, a)"} *} ``` blanchet@33197 ` 86` ```ML {* genuine 2 @{prop "(a\'a \ 'a, b) = (b, a)"} *} ``` blanchet@33197 ` 87` ```ML {* none 5 @{prop "\a b\'a \ 'a \ 'a. (a, b) = (b, a)"} *} ``` blanchet@33197 ` 88` ```ML {* genuine 2 @{prop "(a\'a \ 'a \ 'a, b) \ (b, a)"} *} ``` blanchet@33197 ` 89` ```ML {* none 5 @{prop "\a b\'a \ 'a. (a, b) = (b, a)"} *} ``` blanchet@33197 ` 90` ```ML {* genuine 1 @{prop "(a\'a \ 'a, b) \ (b, a)"} *} ``` blanchet@35284 ` 91` ```ML {* none 5 @{prop "fst (a, b) = a"} *} ``` blanchet@33197 ` 92` ```ML {* none 1 @{prop "fst (a, b) = b"} *} ``` blanchet@33197 ` 93` ```ML {* genuine 2 @{prop "fst (a, b) = b"} *} ``` blanchet@33197 ` 94` ```ML {* genuine 2 @{prop "fst (a, b) \ b"} *} ``` blanchet@35284 ` 95` ```ML {* none 5 @{prop "snd (a, b) = b"} *} ``` blanchet@33197 ` 96` ```ML {* none 1 @{prop "snd (a, b) = a"} *} ``` blanchet@33197 ` 97` ```ML {* genuine 2 @{prop "snd (a, b) = a"} *} ``` blanchet@33197 ` 98` ```ML {* genuine 2 @{prop "snd (a, b) \ a"} *} ``` blanchet@33197 ` 99` ```ML {* genuine 1 @{prop P} *} ``` blanchet@33197 ` 100` ```ML {* genuine 1 @{prop "(\x. P) a"} *} ``` blanchet@33197 ` 101` ```ML {* genuine 1 @{prop "(\x y z. P y x z) a b c"} *} ``` blanchet@33197 ` 102` ```ML {* none 5 @{prop "\f. f = (\x. x) \ f y = y"} *} ``` blanchet@33197 ` 103` ```ML {* genuine 1 @{prop "\f. f p \ p \ (\a b. f (a, b) = (a, b))"} *} ``` blanchet@33197 ` 104` ```ML {* none 2 @{prop "\f. \a b. f (a, b) = (a, b)"} *} ``` blanchet@33197 ` 105` ```ML {* none 3 @{prop "f = (\a b. (b, a)) \ f x y = (y, x)"} *} ``` blanchet@33197 ` 106` ```ML {* genuine 2 @{prop "f = (\a b. (b, a)) \ f x y = (x, y)"} *} ``` blanchet@33197 ` 107` blanchet@33197 ` 108` ```end ```