src/HOL/Nitpick_Examples/Mini_Nits.thy
changeset 63167 0909deb8059b
parent 61076 bdc1e2f0a86a
child 65907 637d18b325d0
     1.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Examples featuring Minipick, the minimalistic version of Nitpick.
     1.5  *)
     1.6  
     1.7 -section {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
     1.8 +section \<open>Examples Featuring Minipick, the Minimalistic Version of Nitpick\<close>
     1.9  
    1.10  theory Mini_Nits
    1.11  imports Main
    1.12 @@ -16,96 +16,96 @@
    1.13  nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
    1.14    total_consts = smart]
    1.15  
    1.16 -ML {*
    1.17 +ML \<open>
    1.18  val check = Minipick.minipick @{context}
    1.19  val expect = Minipick.minipick_expect @{context}
    1.20  val none = expect "none"
    1.21  val genuine = expect "genuine"
    1.22  val unknown = expect "unknown"
    1.23 -*}
    1.24 +\<close>
    1.25  
    1.26 -ML_val {* genuine 1 @{prop "x = Not"} *}
    1.27 -ML_val {* none 1 @{prop "\<exists>x. x = Not"} *}
    1.28 -ML_val {* none 1 @{prop "\<not> False"} *}
    1.29 -ML_val {* genuine 1 @{prop "\<not> True"} *}
    1.30 -ML_val {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
    1.31 -ML_val {* none 1 @{prop True} *}
    1.32 -ML_val {* genuine 1 @{prop False} *}
    1.33 -ML_val {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
    1.34 -ML_val {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
    1.35 -ML_val {* none 4 @{prop "\<forall>x. x = x"} *}
    1.36 -ML_val {* none 4 @{prop "\<exists>x. x = x"} *}
    1.37 -ML_val {* none 1 @{prop "\<forall>x. x = y"} *}
    1.38 -ML_val {* genuine 2 @{prop "\<forall>x. x = y"} *}
    1.39 -ML_val {* none 2 @{prop "\<exists>x. x = y"} *}
    1.40 -ML_val {* none 2 @{prop "\<forall>x::'a \<times> 'a. x = x"} *}
    1.41 -ML_val {* none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"} *}
    1.42 -ML_val {* genuine 2 @{prop "\<forall>x::'a \<times> 'a. x = y"} *}
    1.43 -ML_val {* none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"} *}
    1.44 -ML_val {* none 1 @{prop "All = Ex"} *}
    1.45 -ML_val {* genuine 2 @{prop "All = Ex"} *}
    1.46 -ML_val {* none 1 @{prop "All P = Ex P"} *}
    1.47 -ML_val {* genuine 2 @{prop "All P = Ex P"} *}
    1.48 -ML_val {* none 4 @{prop "x = y \<longrightarrow> P x = P y"} *}
    1.49 -ML_val {* none 4 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
    1.50 -ML_val {* none 2 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
    1.51 -ML_val {* none 4 @{prop "\<exists>x::'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.52 -ML_val {* none 2 @{prop "(x::'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
    1.53 -ML_val {* none 2 @{prop "\<exists>x::'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.54 -ML_val {* genuine 1 @{prop "(op =) X = Ex"} *}
    1.55 -ML_val {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
    1.56 -ML_val {* none 1 @{prop "x = y"} *}
    1.57 -ML_val {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
    1.58 -ML_val {* genuine 2 @{prop "x = y"} *}
    1.59 -ML_val {* genuine 1 @{prop "X \<subseteq> Y"} *}
    1.60 -ML_val {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
    1.61 -ML_val {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
    1.62 -ML_val {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
    1.63 -ML_val {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
    1.64 -ML_val {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
    1.65 -ML_val {* none 4 @{prop "{a} = {a, a}"} *}
    1.66 -ML_val {* genuine 2 @{prop "{a} = {a, b}"} *}
    1.67 -ML_val {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    1.68 -ML_val {* none 4 @{prop "{}\<^sup>+ = {}"} *}
    1.69 -ML_val {* none 4 @{prop "UNIV\<^sup>+ = UNIV"} *}
    1.70 -ML_val {* none 4 @{prop "(UNIV :: ('a \<times> 'b) set) - {} = UNIV"} *}
    1.71 -ML_val {* none 4 @{prop "{} - (UNIV :: ('a \<times> 'b) set) = {}"} *}
    1.72 -ML_val {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.73 -ML_val {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.74 -ML_val {* none 4 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.75 -ML_val {* none 4 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
    1.76 -ML_val {* none 4 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
    1.77 -ML_val {* none 4 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
    1.78 -ML_val {* none 4 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
    1.79 -ML_val {* genuine 2 @{prop "(a, b) = (b, a)"} *}
    1.80 -ML_val {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
    1.81 -ML_val {* none 4 @{prop "\<exists>a b::'a \<times> 'a. (a, b) = (b, a)"} *}
    1.82 -ML_val {* genuine 2 @{prop "(a::'a \<times> 'a, b) = (b, a)"} *}
    1.83 -ML_val {* none 4 @{prop "\<exists>a b::'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
    1.84 -ML_val {* genuine 2 @{prop "(a::'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    1.85 -ML_val {* none 4 @{prop "\<exists>a b::'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    1.86 -ML_val {* genuine 1 @{prop "(a::'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    1.87 -ML_val {* none 4 @{prop "fst (a, b) = a"} *}
    1.88 -ML_val {* none 1 @{prop "fst (a, b) = b"} *}
    1.89 -ML_val {* genuine 2 @{prop "fst (a, b) = b"} *}
    1.90 -ML_val {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    1.91 -ML_val {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
    1.92 -ML_val {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
    1.93 -ML_val {* none 4 @{prop "snd (a, b) = b"} *}
    1.94 -ML_val {* none 1 @{prop "snd (a, b) = a"} *}
    1.95 -ML_val {* genuine 2 @{prop "snd (a, b) = a"} *}
    1.96 -ML_val {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
    1.97 -ML_val {* genuine 1 @{prop P} *}
    1.98 -ML_val {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
    1.99 -ML_val {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
   1.100 -ML_val {* none 4 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
   1.101 -ML_val {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
   1.102 -ML_val {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
   1.103 -ML_val {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
   1.104 -ML_val {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
   1.105 -ML_val {* none 4 @{prop "f = (\<lambda>x. f x)"} *}
   1.106 -ML_val {* none 4 @{prop "f = (\<lambda>x. f x::'a \<Rightarrow> bool)"} *}
   1.107 -ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y)"} *}
   1.108 -ML_val {* none 4 @{prop "f = (\<lambda>x y. f x y::'a \<Rightarrow> bool)"} *}
   1.109 +ML_val \<open>genuine 1 @{prop "x = Not"}\<close>
   1.110 +ML_val \<open>none 1 @{prop "\<exists>x. x = Not"}\<close>
   1.111 +ML_val \<open>none 1 @{prop "\<not> False"}\<close>
   1.112 +ML_val \<open>genuine 1 @{prop "\<not> True"}\<close>
   1.113 +ML_val \<open>none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"}\<close>
   1.114 +ML_val \<open>none 1 @{prop True}\<close>
   1.115 +ML_val \<open>genuine 1 @{prop False}\<close>
   1.116 +ML_val \<open>genuine 1 @{prop "True \<longleftrightarrow> False"}\<close>
   1.117 +ML_val \<open>none 1 @{prop "True \<longleftrightarrow> \<not> False"}\<close>
   1.118 +ML_val \<open>none 4 @{prop "\<forall>x. x = x"}\<close>
   1.119 +ML_val \<open>none 4 @{prop "\<exists>x. x = x"}\<close>
   1.120 +ML_val \<open>none 1 @{prop "\<forall>x. x = y"}\<close>
   1.121 +ML_val \<open>genuine 2 @{prop "\<forall>x. x = y"}\<close>
   1.122 +ML_val \<open>none 2 @{prop "\<exists>x. x = y"}\<close>
   1.123 +ML_val \<open>none 2 @{prop "\<forall>x::'a \<times> 'a. x = x"}\<close>
   1.124 +ML_val \<open>none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"}\<close>
   1.125 +ML_val \<open>genuine 2 @{prop "\<forall>x::'a \<times> 'a. x = y"}\<close>
   1.126 +ML_val \<open>none 2 @{prop "\<exists>x::'a \<times> 'a. x = y"}\<close>
   1.127 +ML_val \<open>none 1 @{prop "All = Ex"}\<close>
   1.128 +ML_val \<open>genuine 2 @{prop "All = Ex"}\<close>
   1.129 +ML_val \<open>none 1 @{prop "All P = Ex P"}\<close>
   1.130 +ML_val \<open>genuine 2 @{prop "All P = Ex P"}\<close>
   1.131 +ML_val \<open>none 4 @{prop "x = y \<longrightarrow> P x = P y"}\<close>
   1.132 +ML_val \<open>none 4 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x = P y"}\<close>
   1.133 +ML_val \<open>none 2 @{prop "(x::'a \<times> 'a) = y \<longrightarrow> P x y = P y x"}\<close>
   1.134 +ML_val \<open>none 4 @{prop "\<exists>x::'a \<times> 'a. x = y \<longrightarrow> P x = P y"}\<close>
   1.135 +ML_val \<open>none 2 @{prop "(x::'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"}\<close>
   1.136 +ML_val \<open>none 2 @{prop "\<exists>x::'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"}\<close>
   1.137 +ML_val \<open>genuine 1 @{prop "(op =) X = Ex"}\<close>
   1.138 +ML_val \<open>none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"}\<close>
   1.139 +ML_val \<open>none 1 @{prop "x = y"}\<close>
   1.140 +ML_val \<open>genuine 1 @{prop "x \<longleftrightarrow> y"}\<close>
   1.141 +ML_val \<open>genuine 2 @{prop "x = y"}\<close>
   1.142 +ML_val \<open>genuine 1 @{prop "X \<subseteq> Y"}\<close>
   1.143 +ML_val \<open>none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"}\<close>
   1.144 +ML_val \<open>none 1 @{prop "P \<and> Q \<longrightarrow> P"}\<close>
   1.145 +ML_val \<open>none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"}\<close>
   1.146 +ML_val \<open>genuine 1 @{prop "P \<or> Q \<longrightarrow> P"}\<close>
   1.147 +ML_val \<open>none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"}\<close>
   1.148 +ML_val \<open>none 4 @{prop "{a} = {a, a}"}\<close>
   1.149 +ML_val \<open>genuine 2 @{prop "{a} = {a, b}"}\<close>
   1.150 +ML_val \<open>genuine 1 @{prop "{a} \<noteq> {a, b}"}\<close>
   1.151 +ML_val \<open>none 4 @{prop "{}\<^sup>+ = {}"}\<close>
   1.152 +ML_val \<open>none 4 @{prop "UNIV\<^sup>+ = UNIV"}\<close>
   1.153 +ML_val \<open>none 4 @{prop "(UNIV :: ('a \<times> 'b) set) - {} = UNIV"}\<close>
   1.154 +ML_val \<open>none 4 @{prop "{} - (UNIV :: ('a \<times> 'b) set) = {}"}\<close>
   1.155 +ML_val \<open>none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"}\<close>
   1.156 +ML_val \<open>genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"}\<close>
   1.157 +ML_val \<open>none 4 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"}\<close>
   1.158 +ML_val \<open>none 4 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"}\<close>
   1.159 +ML_val \<open>none 4 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"}\<close>
   1.160 +ML_val \<open>none 4 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"}\<close>
   1.161 +ML_val \<open>none 4 @{prop "\<exists>a b. (a, b) = (b, a)"}\<close>
   1.162 +ML_val \<open>genuine 2 @{prop "(a, b) = (b, a)"}\<close>
   1.163 +ML_val \<open>genuine 2 @{prop "(a, b) \<noteq> (b, a)"}\<close>
   1.164 +ML_val \<open>none 4 @{prop "\<exists>a b::'a \<times> 'a. (a, b) = (b, a)"}\<close>
   1.165 +ML_val \<open>genuine 2 @{prop "(a::'a \<times> 'a, b) = (b, a)"}\<close>
   1.166 +ML_val \<open>none 4 @{prop "\<exists>a b::'a \<times> 'a \<times> 'a. (a, b) = (b, a)"}\<close>
   1.167 +ML_val \<open>genuine 2 @{prop "(a::'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"}\<close>
   1.168 +ML_val \<open>none 4 @{prop "\<exists>a b::'a \<Rightarrow> 'a. (a, b) = (b, a)"}\<close>
   1.169 +ML_val \<open>genuine 1 @{prop "(a::'a \<Rightarrow> 'a, b) \<noteq> (b, a)"}\<close>
   1.170 +ML_val \<open>none 4 @{prop "fst (a, b) = a"}\<close>
   1.171 +ML_val \<open>none 1 @{prop "fst (a, b) = b"}\<close>
   1.172 +ML_val \<open>genuine 2 @{prop "fst (a, b) = b"}\<close>
   1.173 +ML_val \<open>genuine 2 @{prop "fst (a, b) \<noteq> b"}\<close>
   1.174 +ML_val \<open>genuine 2 @{prop "f ((x, z), y) = (x, z)"}\<close>
   1.175 +ML_val \<open>none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"}\<close>
   1.176 +ML_val \<open>none 4 @{prop "snd (a, b) = b"}\<close>
   1.177 +ML_val \<open>none 1 @{prop "snd (a, b) = a"}\<close>
   1.178 +ML_val \<open>genuine 2 @{prop "snd (a, b) = a"}\<close>
   1.179 +ML_val \<open>genuine 2 @{prop "snd (a, b) \<noteq> a"}\<close>
   1.180 +ML_val \<open>genuine 1 @{prop P}\<close>
   1.181 +ML_val \<open>genuine 1 @{prop "(\<lambda>x. P) a"}\<close>
   1.182 +ML_val \<open>genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"}\<close>
   1.183 +ML_val \<open>none 4 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"}\<close>
   1.184 +ML_val \<open>genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"}\<close>
   1.185 +ML_val \<open>none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"}\<close>
   1.186 +ML_val \<open>none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"}\<close>
   1.187 +ML_val \<open>genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"}\<close>
   1.188 +ML_val \<open>none 4 @{prop "f = (\<lambda>x. f x)"}\<close>
   1.189 +ML_val \<open>none 4 @{prop "f = (\<lambda>x. f x::'a \<Rightarrow> bool)"}\<close>
   1.190 +ML_val \<open>none 4 @{prop "f = (\<lambda>x y. f x y)"}\<close>
   1.191 +ML_val \<open>none 4 @{prop "f = (\<lambda>x y. f x y::'a \<Rightarrow> bool)"}\<close>
   1.192  
   1.193  end