src/HOL/Nitpick_Examples/Manual_Nits.thy
author blanchet
Fri Oct 23 18:59:24 2009 +0200 (2009-10-23)
changeset 33197 de6285ebcc05
child 34126 8a2c5d7aff51
permissions -rw-r--r--
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
     1 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009
     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 = MiniSatJNI, 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. Numbers *}
    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, verbose]
   125 oops
   126 
   127 lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
   128 nitpick [card nat = 100]
   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, verbose, show_consts]
   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 section {* 4. Case Studies *}
   224 
   225 nitpick_params [max_potential = 0, max_threads = 2]
   226 
   227 subsection {* 4.1. A Context-Free Grammar *}
   228 
   229 datatype alphabet = a | b
   230 
   231 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
   232   "[] \<in> S\<^isub>1"
   233 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   234 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
   235 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
   236 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   237 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
   238 
   239 theorem S\<^isub>1_sound:
   240 "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   241 nitpick
   242 oops
   243 
   244 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   245   "[] \<in> S\<^isub>2"
   246 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
   247 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
   248 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
   249 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
   250 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
   251 
   252 theorem S\<^isub>2_sound:
   253 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   254 nitpick
   255 oops
   256 
   257 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   258   "[] \<in> S\<^isub>3"
   259 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
   260 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
   261 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
   262 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   263 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   264 
   265 theorem S\<^isub>3_sound:
   266 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   267 nitpick
   268 sorry
   269 
   270 theorem S\<^isub>3_complete:
   271 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   272 nitpick
   273 oops
   274 
   275 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   276   "[] \<in> S\<^isub>4"
   277 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   278 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   279 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   280 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   281 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   282 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   283 
   284 theorem S\<^isub>4_sound:
   285 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   286 nitpick
   287 sorry
   288 
   289 theorem S\<^isub>4_complete:
   290 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   291 nitpick
   292 sorry
   293 
   294 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
   295 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   296 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
   297 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
   298 nitpick
   299 sorry
   300 
   301 subsection {* 4.2. AA Trees *}
   302 
   303 datatype 'a tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a tree" "'a tree"
   304 
   305 primrec data where
   306 "data \<Lambda> = undefined" |
   307 "data (N x _ _ _) = x"
   308 
   309 primrec dataset where
   310 "dataset \<Lambda> = {}" |
   311 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
   312 
   313 primrec level where
   314 "level \<Lambda> = 0" |
   315 "level (N _ k _ _) = k"
   316 
   317 primrec left where
   318 "left \<Lambda> = \<Lambda>" |
   319 "left (N _ _ t\<^isub>1 _) = t\<^isub>1"
   320 
   321 primrec right where
   322 "right \<Lambda> = \<Lambda>" |
   323 "right (N _ _ _ t\<^isub>2) = t\<^isub>2"
   324 
   325 fun wf where
   326 "wf \<Lambda> = True" |
   327 "wf (N _ k t u) =
   328  (if t = \<Lambda> then
   329     k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
   330   else
   331     wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
   332 
   333 fun skew where
   334 "skew \<Lambda> = \<Lambda>" |
   335 "skew (N x k t u) =
   336  (if t \<noteq> \<Lambda> \<and> k = level t then
   337     N (data t) k (left t) (N x k (right t) u)
   338   else
   339     N x k t u)"
   340 
   341 fun split where
   342 "split \<Lambda> = \<Lambda>" |
   343 "split (N x k t u) =
   344  (if u \<noteq> \<Lambda> \<and> k = level (right u) then
   345     N (data u) (Suc k) (N x k t (left u)) (right u)
   346   else
   347     N x k t u)"
   348 
   349 theorem dataset_skew_split:
   350 "dataset (skew t) = dataset t"
   351 "dataset (split t) = dataset t"
   352 nitpick
   353 sorry
   354 
   355 theorem wf_skew_split:
   356 "wf t \<Longrightarrow> skew t = t"
   357 "wf t \<Longrightarrow> split t = t"
   358 nitpick
   359 sorry
   360 
   361 primrec insort\<^isub>1 where
   362 "insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   363 "insort\<^isub>1 (N y k t u) x =
   364  (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
   365                              (if x > y then insort\<^isub>1 u x else u))"
   366 
   367 theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
   368 nitpick
   369 oops
   370 
   371 theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
   372 nitpick [eval = "insort\<^isub>1 t x"]
   373 oops
   374 
   375 primrec insort\<^isub>2 where
   376 "insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   377 "insort\<^isub>2 (N y k t u) x =
   378  (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
   379                        (if x > y then insort\<^isub>2 u x else u))"
   380 
   381 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
   382 nitpick
   383 sorry
   384 
   385 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
   386 nitpick
   387 sorry
   388 
   389 end