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