src/HOL/Nitpick_Examples/Mini_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35076 cc19e2aef17e
child 35284 9edc2bd6d2bd
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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 (* int -> term -> string *)
    18 fun minipick 0 _ = "none"
    19   | minipick n t =
    20     case minipick (n - 1) t of
    21       "none" => Minipick.pick_nits_in_term @{context} (K n) t
    22     | outcome_code => outcome_code
    23 (* int -> term -> bool *)
    24 fun none n t = (minipick n t = "none" orelse raise FAIL)
    25 fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
    26 fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
    27 *}
    28 
    29 ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
    30 
    31 ML {* genuine 1 @{prop "x = Not"} *}
    32 ML {* none 1 @{prop "\<exists>x. x = Not"} *}
    33 ML {* none 1 @{prop "\<not> False"} *}
    34 ML {* genuine 1 @{prop "\<not> True"} *}
    35 ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
    36 ML {* none 1 @{prop True} *}
    37 ML {* genuine 1 @{prop False} *}
    38 ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
    39 ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
    40 ML {* none 5 @{prop "\<forall>x. x = x"} *}
    41 ML {* none 5 @{prop "\<exists>x. x = x"} *}
    42 ML {* none 1 @{prop "\<forall>x. x = y"} *}
    43 ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
    44 ML {* none 1 @{prop "\<exists>x. x = y"} *}
    45 ML {* none 2 @{prop "\<exists>x. x = y"} *}
    46 ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
    47 ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    48 ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
    49 ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    50 ML {* none 1 @{prop "All = Ex"} *}
    51 ML {* genuine 2 @{prop "All = Ex"} *}
    52 ML {* none 1 @{prop "All P = Ex P"} *}
    53 ML {* genuine 2 @{prop "All P = Ex P"} *}
    54 ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
    55 ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
    56 ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
    57 ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
    58 ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
    59 ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
    60 ML {* genuine 1 @{prop "(op =) X = Ex"} *}
    61 ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
    62 ML {* none 1 @{prop "x = y"} *}
    63 ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
    64 ML {* genuine 2 @{prop "x = y"} *}
    65 ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
    66 ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
    67 ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
    68 ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
    69 ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
    70 ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
    71 ML {* none 5 @{prop "{a} = {a, a}"} *}
    72 ML {* genuine 2 @{prop "{a} = {a, b}"} *}
    73 ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    74 ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
    75 ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    76 ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    77 ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    78 ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
    79 ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
    80 ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
    81 ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
    82 ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
    83 ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
    84 ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
    85 ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
    86 ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
    87 ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    88 ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    89 ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    90 ML {* none 8 @{prop "fst (a, b) = a"} *}
    91 ML {* none 1 @{prop "fst (a, b) = b"} *}
    92 ML {* genuine 2 @{prop "fst (a, b) = b"} *}
    93 ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    94 ML {* none 8 @{prop "snd (a, b) = b"} *}
    95 ML {* none 1 @{prop "snd (a, b) = a"} *}
    96 ML {* genuine 2 @{prop "snd (a, b) = a"} *}
    97 ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
    98 ML {* genuine 1 @{prop P} *}
    99 ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
   100 ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
   101 ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
   102 ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
   103 ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
   104 ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
   105 ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
   106 
   107 end