src/HOL/Nitpick_Examples/Manual_Nits.thy
changeset 33197 de6285ebcc05
child 34126 8a2c5d7aff51
     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