1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Oct 23 18:59:24 2009 +0200
1.3 @@ -0,0 +1,389 @@
1.4 +(* Title: HOL/Nitpick_Examples/Manual_Nits.thy
1.5 + Author: Jasmin Blanchette, TU Muenchen
1.6 + Copyright 2009
1.7 +
1.8 +Examples from the Nitpick manual.
1.9 +*)
1.10 +
1.11 +header {* Examples from the Nitpick Manual *}
1.12 +
1.13 +theory Manual_Nits
1.14 +imports Main Coinductive_List RealDef
1.15 +begin
1.16 +
1.17 +chapter {* 3. First Steps *}
1.18 +
1.19 +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
1.20 +
1.21 +subsection {* 3.1. Propositional Logic *}
1.22 +
1.23 +lemma "P \<longleftrightarrow> Q"
1.24 +nitpick
1.25 +apply auto
1.26 +nitpick 1
1.27 +nitpick 2
1.28 +oops
1.29 +
1.30 +subsection {* 3.2. Type Variables *}
1.31 +
1.32 +lemma "P x \<Longrightarrow> P (THE y. P y)"
1.33 +nitpick [verbose]
1.34 +oops
1.35 +
1.36 +subsection {* 3.3. Constants *}
1.37 +
1.38 +lemma "P x \<Longrightarrow> P (THE y. P y)"
1.39 +nitpick [show_consts]
1.40 +nitpick [full_descrs, show_consts]
1.41 +nitpick [dont_specialize, full_descrs, show_consts]
1.42 +oops
1.43 +
1.44 +lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
1.45 +nitpick
1.46 +nitpick [card 'a = 1-50]
1.47 +(* sledgehammer *)
1.48 +apply (metis the_equality)
1.49 +done
1.50 +
1.51 +subsection {* 3.4. Skolemization *}
1.52 +
1.53 +lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
1.54 +nitpick
1.55 +oops
1.56 +
1.57 +lemma "\<exists>x. \<forall>f. f x = x"
1.58 +nitpick
1.59 +oops
1.60 +
1.61 +lemma "refl r \<Longrightarrow> sym r"
1.62 +nitpick
1.63 +oops
1.64 +
1.65 +subsection {* 3.5. Numbers *}
1.66 +
1.67 +lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
1.68 +nitpick
1.69 +oops
1.70 +
1.71 +lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
1.72 +nitpick [card nat = 100, check_potential]
1.73 +oops
1.74 +
1.75 +lemma "P Suc"
1.76 +nitpick [card = 1-6]
1.77 +oops
1.78 +
1.79 +lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
1.80 +nitpick [card nat = 1]
1.81 +nitpick [card nat = 2]
1.82 +oops
1.83 +
1.84 +subsection {* 3.6. Inductive Datatypes *}
1.85 +
1.86 +lemma "hd (xs @ [y, y]) = hd xs"
1.87 +nitpick
1.88 +nitpick [show_consts, show_datatypes]
1.89 +oops
1.90 +
1.91 +lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
1.92 +nitpick [show_datatypes]
1.93 +oops
1.94 +
1.95 +subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
1.96 +
1.97 +typedef three = "{0\<Colon>nat, 1, 2}"
1.98 +by blast
1.99 +
1.100 +definition A :: three where "A \<equiv> Abs_three 0"
1.101 +definition B :: three where "B \<equiv> Abs_three 1"
1.102 +definition C :: three where "C \<equiv> Abs_three 2"
1.103 +
1.104 +lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
1.105 +nitpick [show_datatypes]
1.106 +oops
1.107 +
1.108 +record point =
1.109 + Xcoord :: int
1.110 + Ycoord :: int
1.111 +
1.112 +lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
1.113 +nitpick [show_datatypes]
1.114 +oops
1.115 +
1.116 +lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
1.117 +nitpick [show_datatypes]
1.118 +oops
1.119 +
1.120 +subsection {* 3.8. Inductive and Coinductive Predicates *}
1.121 +
1.122 +inductive even where
1.123 +"even 0" |
1.124 +"even n \<Longrightarrow> even (Suc (Suc n))"
1.125 +
1.126 +lemma "\<exists>n. even n \<and> even (Suc n)"
1.127 +nitpick [card nat = 100, verbose]
1.128 +oops
1.129 +
1.130 +lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
1.131 +nitpick [card nat = 100]
1.132 +oops
1.133 +
1.134 +inductive even' where
1.135 +"even' (0\<Colon>nat)" |
1.136 +"even' 2" |
1.137 +"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
1.138 +
1.139 +lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
1.140 +nitpick [card nat = 10, verbose, show_consts]
1.141 +oops
1.142 +
1.143 +lemma "even' (n - 2) \<Longrightarrow> even' n"
1.144 +nitpick [card nat = 10, show_consts]
1.145 +oops
1.146 +
1.147 +coinductive nats where
1.148 +"nats (x\<Colon>nat) \<Longrightarrow> nats x"
1.149 +
1.150 +lemma "nats = {0, 1, 2, 3, 4}"
1.151 +nitpick [card nat = 10, show_consts]
1.152 +oops
1.153 +
1.154 +inductive odd where
1.155 +"odd 1" |
1.156 +"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
1.157 +
1.158 +lemma "odd n \<Longrightarrow> odd (n - 2)"
1.159 +nitpick [card nat = 10, show_consts]
1.160 +oops
1.161 +
1.162 +subsection {* 3.9. Coinductive Datatypes *}
1.163 +
1.164 +lemma "xs \<noteq> LCons a xs"
1.165 +nitpick
1.166 +oops
1.167 +
1.168 +lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
1.169 +nitpick [verbose]
1.170 +nitpick [bisim_depth = -1, verbose]
1.171 +oops
1.172 +
1.173 +lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
1.174 +nitpick [bisim_depth = -1, show_datatypes]
1.175 +nitpick
1.176 +sorry
1.177 +
1.178 +subsection {* 3.10. Boxing *}
1.179 +
1.180 +datatype tm = Var nat | Lam tm | App tm tm
1.181 +
1.182 +primrec lift where
1.183 +"lift (Var j) k = Var (if j < k then j else j + 1)" |
1.184 +"lift (Lam t) k = Lam (lift t (k + 1))" |
1.185 +"lift (App t u) k = App (lift t k) (lift u k)"
1.186 +
1.187 +primrec loose where
1.188 +"loose (Var j) k = (j \<ge> k)" |
1.189 +"loose (Lam t) k = loose t (Suc k)" |
1.190 +"loose (App t u) k = (loose t k \<or> loose u k)"
1.191 +
1.192 +primrec subst\<^isub>1 where
1.193 +"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
1.194 +"subst\<^isub>1 \<sigma> (Lam t) =
1.195 + Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
1.196 +"subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
1.197 +
1.198 +lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
1.199 +nitpick [verbose]
1.200 +nitpick [eval = "subst\<^isub>1 \<sigma> t"]
1.201 +nitpick [dont_box]
1.202 +oops
1.203 +
1.204 +primrec subst\<^isub>2 where
1.205 +"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
1.206 +"subst\<^isub>2 \<sigma> (Lam t) =
1.207 + Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
1.208 +"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
1.209 +
1.210 +lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
1.211 +nitpick
1.212 +sorry
1.213 +
1.214 +subsection {* 3.11. Scope Monotonicity *}
1.215 +
1.216 +lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
1.217 +nitpick [verbose]
1.218 +nitpick [card = 8, verbose]
1.219 +oops
1.220 +
1.221 +lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
1.222 +nitpick [mono]
1.223 +nitpick
1.224 +oops
1.225 +
1.226 +section {* 4. Case Studies *}
1.227 +
1.228 +nitpick_params [max_potential = 0, max_threads = 2]
1.229 +
1.230 +subsection {* 4.1. A Context-Free Grammar *}
1.231 +
1.232 +datatype alphabet = a | b
1.233 +
1.234 +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
1.235 + "[] \<in> S\<^isub>1"
1.236 +| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
1.237 +| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
1.238 +| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
1.239 +| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
1.240 +| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
1.241 +
1.242 +theorem S\<^isub>1_sound:
1.243 +"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
1.244 +nitpick
1.245 +oops
1.246 +
1.247 +inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
1.248 + "[] \<in> S\<^isub>2"
1.249 +| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
1.250 +| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
1.251 +| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
1.252 +| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
1.253 +| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
1.254 +
1.255 +theorem S\<^isub>2_sound:
1.256 +"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
1.257 +nitpick
1.258 +oops
1.259 +
1.260 +inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
1.261 + "[] \<in> S\<^isub>3"
1.262 +| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
1.263 +| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
1.264 +| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
1.265 +| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
1.266 +| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
1.267 +
1.268 +theorem S\<^isub>3_sound:
1.269 +"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
1.270 +nitpick
1.271 +sorry
1.272 +
1.273 +theorem S\<^isub>3_complete:
1.274 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
1.275 +nitpick
1.276 +oops
1.277 +
1.278 +inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
1.279 + "[] \<in> S\<^isub>4"
1.280 +| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
1.281 +| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
1.282 +| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
1.283 +| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
1.284 +| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
1.285 +| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
1.286 +
1.287 +theorem S\<^isub>4_sound:
1.288 +"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
1.289 +nitpick
1.290 +sorry
1.291 +
1.292 +theorem S\<^isub>4_complete:
1.293 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
1.294 +nitpick
1.295 +sorry
1.296 +
1.297 +theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
1.298 +"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
1.299 +"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
1.300 +"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
1.301 +nitpick
1.302 +sorry
1.303 +
1.304 +subsection {* 4.2. AA Trees *}
1.305 +
1.306 +datatype 'a tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a tree" "'a tree"
1.307 +
1.308 +primrec data where
1.309 +"data \<Lambda> = undefined" |
1.310 +"data (N x _ _ _) = x"
1.311 +
1.312 +primrec dataset where
1.313 +"dataset \<Lambda> = {}" |
1.314 +"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
1.315 +
1.316 +primrec level where
1.317 +"level \<Lambda> = 0" |
1.318 +"level (N _ k _ _) = k"
1.319 +
1.320 +primrec left where
1.321 +"left \<Lambda> = \<Lambda>" |
1.322 +"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
1.323 +
1.324 +primrec right where
1.325 +"right \<Lambda> = \<Lambda>" |
1.326 +"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
1.327 +
1.328 +fun wf where
1.329 +"wf \<Lambda> = True" |
1.330 +"wf (N _ k t u) =
1.331 + (if t = \<Lambda> then
1.332 + k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
1.333 + else
1.334 + wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
1.335 +
1.336 +fun skew where
1.337 +"skew \<Lambda> = \<Lambda>" |
1.338 +"skew (N x k t u) =
1.339 + (if t \<noteq> \<Lambda> \<and> k = level t then
1.340 + N (data t) k (left t) (N x k (right t) u)
1.341 + else
1.342 + N x k t u)"
1.343 +
1.344 +fun split where
1.345 +"split \<Lambda> = \<Lambda>" |
1.346 +"split (N x k t u) =
1.347 + (if u \<noteq> \<Lambda> \<and> k = level (right u) then
1.348 + N (data u) (Suc k) (N x k t (left u)) (right u)
1.349 + else
1.350 + N x k t u)"
1.351 +
1.352 +theorem dataset_skew_split:
1.353 +"dataset (skew t) = dataset t"
1.354 +"dataset (split t) = dataset t"
1.355 +nitpick
1.356 +sorry
1.357 +
1.358 +theorem wf_skew_split:
1.359 +"wf t \<Longrightarrow> skew t = t"
1.360 +"wf t \<Longrightarrow> split t = t"
1.361 +nitpick
1.362 +sorry
1.363 +
1.364 +primrec insort\<^isub>1 where
1.365 +"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
1.366 +"insort\<^isub>1 (N y k t u) x =
1.367 + (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
1.368 + (if x > y then insort\<^isub>1 u x else u))"
1.369 +
1.370 +theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
1.371 +nitpick
1.372 +oops
1.373 +
1.374 +theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
1.375 +nitpick [eval = "insort\<^isub>1 t x"]
1.376 +oops
1.377 +
1.378 +primrec insort\<^isub>2 where
1.379 +"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
1.380 +"insort\<^isub>2 (N y k t u) x =
1.381 + (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
1.382 + (if x > y then insort\<^isub>2 u x else u))"
1.383 +
1.384 +theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
1.385 +nitpick
1.386 +sorry
1.387 +
1.388 +theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
1.389 +nitpick
1.390 +sorry
1.391 +
1.392 +end