src/HOL/Nitpick_Examples/Manual_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35078 6fd1052fe463
child 35180 c57dba973391
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     4 
     5 Examples from the Nitpick manual.
     6 *)
     7 
     8 header {* Examples from the Nitpick Manual *}
     9 
    10 theory Manual_Nits
    11 imports Main Coinductive_List RealDef
    12 begin
    13 
    14 chapter {* 3. First Steps *}
    15 
    16 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
    17 
    18 subsection {* 3.1. Propositional Logic *}
    19 
    20 lemma "P \<longleftrightarrow> Q"
    21 nitpick
    22 apply auto
    23 nitpick 1
    24 nitpick 2
    25 oops
    26 
    27 subsection {* 3.2. Type Variables *}
    28 
    29 lemma "P x \<Longrightarrow> P (THE y. P y)"
    30 nitpick [verbose]
    31 oops
    32 
    33 subsection {* 3.3. Constants *}
    34 
    35 lemma "P x \<Longrightarrow> P (THE y. P y)"
    36 nitpick [show_consts]
    37 nitpick [full_descrs, show_consts]
    38 nitpick [dont_specialize, full_descrs, show_consts]
    39 oops
    40 
    41 lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
    42 nitpick
    43 nitpick [card 'a = 1-50]
    44 (* sledgehammer *)
    45 apply (metis the_equality)
    46 done
    47 
    48 subsection {* 3.4. Skolemization *}
    49 
    50 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    51 nitpick
    52 oops
    53 
    54 lemma "\<exists>x. \<forall>f. f x = x"
    55 nitpick
    56 oops
    57 
    58 lemma "refl r \<Longrightarrow> sym r"
    59 nitpick
    60 oops
    61 
    62 subsection {* 3.5. Natural Numbers and Integers *}
    63 
    64 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    65 nitpick
    66 oops
    67 
    68 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
    69 nitpick [card nat = 100, check_potential]
    70 oops
    71 
    72 lemma "P Suc"
    73 nitpick [card = 1-6]
    74 oops
    75 
    76 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
    77 nitpick [card nat = 1]
    78 nitpick [card nat = 2]
    79 oops
    80 
    81 subsection {* 3.6. Inductive Datatypes *}
    82 
    83 lemma "hd (xs @ [y, y]) = hd xs"
    84 nitpick
    85 nitpick [show_consts, show_datatypes]
    86 oops
    87 
    88 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
    89 nitpick [show_datatypes]
    90 oops
    91 
    92 subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
    93 
    94 typedef three = "{0\<Colon>nat, 1, 2}"
    95 by blast
    96 
    97 definition A :: three where "A \<equiv> Abs_three 0"
    98 definition B :: three where "B \<equiv> Abs_three 1"
    99 definition C :: three where "C \<equiv> Abs_three 2"
   100 
   101 lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
   102 nitpick [show_datatypes]
   103 oops
   104 
   105 record point =
   106   Xcoord :: int
   107   Ycoord :: int
   108 
   109 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
   110 nitpick [show_datatypes]
   111 oops
   112 
   113 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
   114 nitpick [show_datatypes]
   115 oops
   116 
   117 subsection {* 3.8. Inductive and Coinductive Predicates *}
   118 
   119 inductive even where
   120 "even 0" |
   121 "even n \<Longrightarrow> even (Suc (Suc n))"
   122 
   123 lemma "\<exists>n. even n \<and> even (Suc n)"
   124 nitpick [card nat = 100, unary_ints, verbose]
   125 oops
   126 
   127 lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
   128 nitpick [card nat = 100, unary_ints, verbose]
   129 oops
   130 
   131 inductive even' where
   132 "even' (0\<Colon>nat)" |
   133 "even' 2" |
   134 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
   135 
   136 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
   137 nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
   138 oops
   139 
   140 lemma "even' (n - 2) \<Longrightarrow> even' n"
   141 nitpick [card nat = 10, show_consts]
   142 oops
   143 
   144 coinductive nats where
   145 "nats (x\<Colon>nat) \<Longrightarrow> nats x"
   146 
   147 lemma "nats = {0, 1, 2, 3, 4}"
   148 nitpick [card nat = 10, show_consts]
   149 oops
   150 
   151 inductive odd where
   152 "odd 1" |
   153 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
   154 
   155 lemma "odd n \<Longrightarrow> odd (n - 2)"
   156 nitpick [card nat = 10, show_consts]
   157 oops
   158 
   159 subsection {* 3.9. Coinductive Datatypes *}
   160 
   161 lemma "xs \<noteq> LCons a xs"
   162 nitpick
   163 oops
   164 
   165 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
   166 nitpick [verbose]
   167 nitpick [bisim_depth = -1, verbose]
   168 oops
   169 
   170 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
   171 nitpick [bisim_depth = -1, show_datatypes]
   172 nitpick
   173 sorry
   174 
   175 subsection {* 3.10. Boxing *}
   176 
   177 datatype tm = Var nat | Lam tm | App tm tm
   178 
   179 primrec lift where
   180 "lift (Var j) k = Var (if j < k then j else j + 1)" |
   181 "lift (Lam t) k = Lam (lift t (k + 1))" |
   182 "lift (App t u) k = App (lift t k) (lift u k)"
   183 
   184 primrec loose where
   185 "loose (Var j) k = (j \<ge> k)" |
   186 "loose (Lam t) k = loose t (Suc k)" |
   187 "loose (App t u) k = (loose t k \<or> loose u k)"
   188 
   189 primrec subst\<^isub>1 where
   190 "subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
   191 "subst\<^isub>1 \<sigma> (Lam t) =
   192  Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
   193 "subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
   194 
   195 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
   196 nitpick [verbose]
   197 nitpick [eval = "subst\<^isub>1 \<sigma> t"]
   198 nitpick [dont_box]
   199 oops
   200 
   201 primrec subst\<^isub>2 where
   202 "subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
   203 "subst\<^isub>2 \<sigma> (Lam t) =
   204  Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
   205 "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
   206 
   207 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
   208 nitpick
   209 sorry
   210 
   211 subsection {* 3.11. Scope Monotonicity *}
   212 
   213 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   214 nitpick [verbose]
   215 nitpick [card = 8, verbose]
   216 oops
   217 
   218 lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
   219 nitpick [mono]
   220 nitpick
   221 oops
   222 
   223 subsection {* 3.12. Inductive Properties *}
   224 
   225 inductive_set reach where
   226 "(4\<Colon>nat) \<in> reach" |
   227 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
   228 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
   229 
   230 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
   231 nitpick
   232 apply (induct set: reach)
   233   apply auto
   234  nitpick
   235  apply (thin_tac "n \<in> reach")
   236  nitpick
   237 oops
   238 
   239 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
   240 nitpick
   241 apply (induct set: reach)
   242   apply auto
   243  nitpick
   244  apply (thin_tac "n \<in> reach")
   245  nitpick
   246 oops
   247 
   248 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
   249 by (induct set: reach) arith+
   250 
   251 datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
   252 
   253 primrec labels where
   254 "labels (Leaf a) = {a}" |
   255 "labels (Branch t u) = labels t \<union> labels u"
   256 
   257 primrec swap where
   258 "swap (Leaf c) a b =
   259  (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
   260 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
   261 
   262 lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
   263 nitpick
   264 proof (induct t)
   265   case Leaf thus ?case by simp
   266 next
   267   case (Branch t u) thus ?case
   268   nitpick
   269   nitpick [non_std "'a bin_tree", show_consts]
   270 oops
   271 
   272 lemma "labels (swap t a b) =
   273        (if a \<in> labels t then
   274           if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
   275         else
   276           if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
   277 nitpick
   278 proof (induct t)
   279   case Leaf thus ?case by simp
   280 next
   281   case (Branch t u) thus ?case
   282   nitpick [non_std "'a bin_tree", show_consts]
   283   by auto
   284 qed
   285 
   286 section {* 4. Case Studies *}
   287 
   288 nitpick_params [max_potential = 0, max_threads = 2]
   289 
   290 subsection {* 4.1. A Context-Free Grammar *}
   291 
   292 datatype alphabet = a | b
   293 
   294 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
   295   "[] \<in> S\<^isub>1"
   296 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   297 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
   298 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
   299 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   300 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
   301 
   302 theorem S\<^isub>1_sound:
   303 "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   304 nitpick
   305 oops
   306 
   307 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   308   "[] \<in> S\<^isub>2"
   309 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
   310 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
   311 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
   312 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
   313 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
   314 
   315 theorem S\<^isub>2_sound:
   316 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   317 nitpick
   318 oops
   319 
   320 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   321   "[] \<in> S\<^isub>3"
   322 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
   323 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
   324 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
   325 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   326 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   327 
   328 theorem S\<^isub>3_sound:
   329 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   330 nitpick
   331 sorry
   332 
   333 theorem S\<^isub>3_complete:
   334 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   335 nitpick
   336 oops
   337 
   338 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   339   "[] \<in> S\<^isub>4"
   340 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   341 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   342 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   343 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   344 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   345 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   346 
   347 theorem S\<^isub>4_sound:
   348 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   349 nitpick
   350 sorry
   351 
   352 theorem S\<^isub>4_complete:
   353 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   354 nitpick
   355 sorry
   356 
   357 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
   358 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   359 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
   360 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
   361 nitpick
   362 sorry
   363 
   364 subsection {* 4.2. AA Trees *}
   365 
   366 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
   367 
   368 primrec data where
   369 "data \<Lambda> = undefined" |
   370 "data (N x _ _ _) = x"
   371 
   372 primrec dataset where
   373 "dataset \<Lambda> = {}" |
   374 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
   375 
   376 primrec level where
   377 "level \<Lambda> = 0" |
   378 "level (N _ k _ _) = k"
   379 
   380 primrec left where
   381 "left \<Lambda> = \<Lambda>" |
   382 "left (N _ _ t\<^isub>1 _) = t\<^isub>1"
   383 
   384 primrec right where
   385 "right \<Lambda> = \<Lambda>" |
   386 "right (N _ _ _ t\<^isub>2) = t\<^isub>2"
   387 
   388 fun wf where
   389 "wf \<Lambda> = True" |
   390 "wf (N _ k t u) =
   391  (if t = \<Lambda> then
   392     k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
   393   else
   394     wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
   395 
   396 fun skew where
   397 "skew \<Lambda> = \<Lambda>" |
   398 "skew (N x k t u) =
   399  (if t \<noteq> \<Lambda> \<and> k = level t then
   400     N (data t) k (left t) (N x k (right t) u)
   401   else
   402     N x k t u)"
   403 
   404 fun split where
   405 "split \<Lambda> = \<Lambda>" |
   406 "split (N x k t u) =
   407  (if u \<noteq> \<Lambda> \<and> k = level (right u) then
   408     N (data u) (Suc k) (N x k t (left u)) (right u)
   409   else
   410     N x k t u)"
   411 
   412 theorem dataset_skew_split:
   413 "dataset (skew t) = dataset t"
   414 "dataset (split t) = dataset t"
   415 nitpick
   416 sorry
   417 
   418 theorem wf_skew_split:
   419 "wf t \<Longrightarrow> skew t = t"
   420 "wf t \<Longrightarrow> split t = t"
   421 nitpick
   422 sorry
   423 
   424 primrec insort\<^isub>1 where
   425 "insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   426 "insort\<^isub>1 (N y k t u) x =
   427  (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
   428                              (if x > y then insort\<^isub>1 u x else u))"
   429 
   430 theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
   431 nitpick
   432 oops
   433 
   434 theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
   435 nitpick [eval = "insort\<^isub>1 t x"]
   436 oops
   437 
   438 primrec insort\<^isub>2 where
   439 "insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   440 "insort\<^isub>2 (N y k t u) x =
   441  (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
   442                        (if x > y then insort\<^isub>2 u x else u))"
   443 
   444 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
   445 nitpick
   446 sorry
   447 
   448 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
   449 nitpick
   450 sorry
   451 
   452 end