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