src/HOL/Nitpick_Examples/Manual_Nits.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 41278 8e1cde88aae6
child 42208 02513eb26eb7
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     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 (* The "expect" arguments to Nitpick in this theory and the other example
    11    theories are there so that the example can also serve as a regression test
    12    suite. *)
    13 
    14 theory Manual_Nits
    15 imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
    16 begin
    17 
    18 chapter {* 3. First Steps *}
    19 
    20 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
    21                 timeout = 60]
    22 
    23 subsection {* 3.1. Propositional Logic *}
    24 
    25 lemma "P \<longleftrightarrow> Q"
    26 nitpick [expect = genuine]
    27 apply auto
    28 nitpick [expect = genuine] 1
    29 nitpick [expect = genuine] 2
    30 oops
    31 
    32 subsection {* 3.2. Type Variables *}
    33 
    34 lemma "P x \<Longrightarrow> P (THE y. P y)"
    35 nitpick [verbose, expect = genuine]
    36 oops
    37 
    38 subsection {* 3.3. Constants *}
    39 
    40 lemma "P x \<Longrightarrow> P (THE y. P y)"
    41 nitpick [show_consts, expect = genuine]
    42 nitpick [dont_specialize, show_consts, expect = genuine]
    43 oops
    44 
    45 lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
    46 nitpick [expect = none]
    47 nitpick [card 'a = 1\<midarrow>50, expect = none]
    48 (* sledgehammer *)
    49 apply (metis the_equality)
    50 done
    51 
    52 subsection {* 3.4. Skolemization *}
    53 
    54 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    55 nitpick [expect = genuine]
    56 oops
    57 
    58 lemma "\<exists>x. \<forall>f. f x = x"
    59 nitpick [expect = genuine]
    60 oops
    61 
    62 lemma "refl r \<Longrightarrow> sym r"
    63 nitpick [expect = genuine]
    64 oops
    65 
    66 subsection {* 3.5. Natural Numbers and Integers *}
    67 
    68 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    69 nitpick [expect = genuine]
    70 oops
    71 
    72 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
    73 nitpick [card nat = 100, check_potential, expect = genuine]
    74 oops
    75 
    76 lemma "P Suc"
    77 nitpick [expect = none]
    78 oops
    79 
    80 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
    81 nitpick [card nat = 1, expect = genuine]
    82 nitpick [card nat = 2, expect = none]
    83 oops
    84 
    85 subsection {* 3.6. Inductive Datatypes *}
    86 
    87 lemma "hd (xs @ [y, y]) = hd xs"
    88 nitpick [expect = genuine]
    89 nitpick [show_consts, show_datatypes, expect = genuine]
    90 oops
    91 
    92 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
    93 nitpick [show_datatypes, expect = genuine]
    94 oops
    95 
    96 subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
    97 
    98 typedef three = "{0\<Colon>nat, 1, 2}"
    99 by blast
   100 
   101 definition A :: three where "A \<equiv> Abs_three 0"
   102 definition B :: three where "B \<equiv> Abs_three 1"
   103 definition C :: three where "C \<equiv> Abs_three 2"
   104 
   105 lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
   106 nitpick [show_datatypes, expect = genuine]
   107 oops
   108 
   109 fun my_int_rel where
   110 "my_int_rel (x, y) (u, v) = (x + v = u + y)"
   111 
   112 quotient_type my_int = "nat \<times> nat" / my_int_rel
   113 by (auto simp add: equivp_def fun_eq_iff)
   114 
   115 definition add_raw where
   116 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
   117 
   118 quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
   119 
   120 lemma "add x y = add x x"
   121 nitpick [show_datatypes, expect = genuine]
   122 oops
   123 
   124 ML {*
   125 fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
   126     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
   127                          - snd (HOLogic.dest_number t2))
   128   | my_int_postproc _ _ _ _ t = t
   129 *}
   130 
   131 declaration {*
   132 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
   133 *}
   134 
   135 lemma "add x y = add x x"
   136 nitpick [show_datatypes]
   137 oops
   138 
   139 record point =
   140   Xcoord :: int
   141   Ycoord :: int
   142 
   143 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
   144 nitpick [show_datatypes, expect = genuine]
   145 oops
   146 
   147 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
   148 nitpick [show_datatypes, expect = genuine]
   149 oops
   150 
   151 subsection {* 3.8. Inductive and Coinductive Predicates *}
   152 
   153 inductive even where
   154 "even 0" |
   155 "even n \<Longrightarrow> even (Suc (Suc n))"
   156 
   157 lemma "\<exists>n. even n \<and> even (Suc n)"
   158 nitpick [card nat = 50, unary_ints, verbose, expect = potential]
   159 oops
   160 
   161 lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
   162 nitpick [card nat = 50, unary_ints, expect = genuine]
   163 oops
   164 
   165 inductive even' where
   166 "even' (0\<Colon>nat)" |
   167 "even' 2" |
   168 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
   169 
   170 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
   171 nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
   172 oops
   173 
   174 lemma "even' (n - 2) \<Longrightarrow> even' n"
   175 nitpick [card nat = 10, show_consts, expect = genuine]
   176 oops
   177 
   178 coinductive nats where
   179 "nats (x\<Colon>nat) \<Longrightarrow> nats x"
   180 
   181 lemma "nats = {0, 1, 2, 3, 4}"
   182 nitpick [card nat = 10, show_consts, expect = genuine]
   183 oops
   184 
   185 inductive odd where
   186 "odd 1" |
   187 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
   188 
   189 lemma "odd n \<Longrightarrow> odd (n - 2)"
   190 nitpick [card nat = 10, show_consts, expect = genuine]
   191 oops
   192 
   193 subsection {* 3.9. Coinductive Datatypes *}
   194 
   195 (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
   196    we cannot rely on its presence, we expediently provide our own
   197    axiomatization. The examples also work unchanged with Lochbihler's
   198    "Coinductive_List" theory. *)
   199 
   200 typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
   201 
   202 definition LNil where
   203 "LNil = Abs_llist (Inl [])"
   204 definition LCons where
   205 "LCons y ys = Abs_llist (case Rep_llist ys of
   206                            Inl ys' \<Rightarrow> Inl (y # ys')
   207                          | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
   208 
   209 axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
   210 
   211 lemma iterates_def [nitpick_simp]:
   212 "iterates f a = LCons a (iterates f (f a))"
   213 sorry
   214 
   215 declaration {*
   216 Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
   217     (map dest_Const [@{term LNil}, @{term LCons}])
   218 *}
   219 
   220 lemma "xs \<noteq> LCons a xs"
   221 nitpick [expect = genuine]
   222 oops
   223 
   224 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
   225 nitpick [verbose, expect = genuine]
   226 oops
   227 
   228 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
   229 nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
   230 nitpick [card = 1\<midarrow>5, expect = none]
   231 sorry
   232 
   233 subsection {* 3.10. Boxing *}
   234 
   235 datatype tm = Var nat | Lam tm | App tm tm
   236 
   237 primrec lift where
   238 "lift (Var j) k = Var (if j < k then j else j + 1)" |
   239 "lift (Lam t) k = Lam (lift t (k + 1))" |
   240 "lift (App t u) k = App (lift t k) (lift u k)"
   241 
   242 primrec loose where
   243 "loose (Var j) k = (j \<ge> k)" |
   244 "loose (Lam t) k = loose t (Suc k)" |
   245 "loose (App t u) k = (loose t k \<or> loose u k)"
   246 
   247 primrec subst\<^isub>1 where
   248 "subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
   249 "subst\<^isub>1 \<sigma> (Lam t) =
   250  Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
   251 "subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
   252 
   253 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
   254 nitpick [verbose, expect = genuine]
   255 nitpick [eval = "subst\<^isub>1 \<sigma> t", expect = genuine]
   256 (* nitpick [dont_box, expect = unknown] *)
   257 oops
   258 
   259 primrec subst\<^isub>2 where
   260 "subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
   261 "subst\<^isub>2 \<sigma> (Lam t) =
   262  Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
   263 "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
   264 
   265 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
   266 nitpick [card = 1\<midarrow>5, expect = none]
   267 sorry
   268 
   269 subsection {* 3.11. Scope Monotonicity *}
   270 
   271 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   272 nitpick [verbose, expect = genuine]
   273 oops
   274 
   275 lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
   276 nitpick [mono, expect = none]
   277 nitpick [expect = genuine]
   278 oops
   279 
   280 subsection {* 3.12. Inductive Properties *}
   281 
   282 inductive_set reach where
   283 "(4\<Colon>nat) \<in> reach" |
   284 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
   285 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
   286 
   287 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
   288 (* nitpick *)
   289 apply (induct set: reach)
   290   apply auto
   291  nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
   292  apply (thin_tac "n \<in> reach")
   293  nitpick [expect = genuine]
   294 oops
   295 
   296 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
   297 (* nitpick *)
   298 apply (induct set: reach)
   299   apply auto
   300  nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
   301  apply (thin_tac "n \<in> reach")
   302  nitpick [expect = genuine]
   303 oops
   304 
   305 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
   306 by (induct set: reach) arith+
   307 
   308 datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
   309 
   310 primrec labels where
   311 "labels (Leaf a) = {a}" |
   312 "labels (Branch t u) = labels t \<union> labels u"
   313 
   314 primrec swap where
   315 "swap (Leaf c) a b =
   316  (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
   317 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
   318 
   319 lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
   320 (* nitpick *)
   321 proof (induct t)
   322   case Leaf thus ?case by simp
   323 next
   324   case (Branch t u) thus ?case
   325   (* nitpick *)
   326   nitpick [non_std, show_all, expect = genuine]
   327 oops
   328 
   329 lemma "labels (swap t a b) =
   330        (if a \<in> labels t then
   331           if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
   332         else
   333           if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
   334 (* nitpick *)
   335 proof (induct t)
   336   case Leaf thus ?case by simp
   337 next
   338   case (Branch t u) thus ?case
   339   nitpick [non_std, card = 1\<midarrow>4, expect = none]
   340   by auto
   341 qed
   342 
   343 section {* 4. Case Studies *}
   344 
   345 nitpick_params [max_potential = 0]
   346 
   347 subsection {* 4.1. A Context-Free Grammar *}
   348 
   349 datatype alphabet = a | b
   350 
   351 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
   352   "[] \<in> S\<^isub>1"
   353 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   354 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
   355 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
   356 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   357 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
   358 
   359 theorem S\<^isub>1_sound:
   360 "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   361 nitpick [expect = genuine]
   362 oops
   363 
   364 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   365   "[] \<in> S\<^isub>2"
   366 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
   367 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
   368 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
   369 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
   370 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
   371 
   372 theorem S\<^isub>2_sound:
   373 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   374 nitpick [expect = genuine]
   375 oops
   376 
   377 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   378   "[] \<in> S\<^isub>3"
   379 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
   380 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
   381 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
   382 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   383 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   384 
   385 theorem S\<^isub>3_sound:
   386 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   387 nitpick [card = 1\<midarrow>5, expect = none]
   388 sorry
   389 
   390 theorem S\<^isub>3_complete:
   391 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   392 nitpick [expect = genuine]
   393 oops
   394 
   395 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   396   "[] \<in> S\<^isub>4"
   397 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   398 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   399 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   400 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   401 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   402 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   403 
   404 theorem S\<^isub>4_sound:
   405 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   406 nitpick [card = 1\<midarrow>5, expect = none]
   407 sorry
   408 
   409 theorem S\<^isub>4_complete:
   410 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   411 nitpick [card = 1\<midarrow>5, expect = none]
   412 sorry
   413 
   414 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
   415 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   416 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
   417 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
   418 nitpick [card = 1\<midarrow>5, expect = none]
   419 sorry
   420 
   421 subsection {* 4.2. AA Trees *}
   422 
   423 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
   424 
   425 primrec data where
   426 "data \<Lambda> = undefined" |
   427 "data (N x _ _ _) = x"
   428 
   429 primrec dataset where
   430 "dataset \<Lambda> = {}" |
   431 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
   432 
   433 primrec level where
   434 "level \<Lambda> = 0" |
   435 "level (N _ k _ _) = k"
   436 
   437 primrec left where
   438 "left \<Lambda> = \<Lambda>" |
   439 "left (N _ _ t\<^isub>1 _) = t\<^isub>1"
   440 
   441 primrec right where
   442 "right \<Lambda> = \<Lambda>" |
   443 "right (N _ _ _ t\<^isub>2) = t\<^isub>2"
   444 
   445 fun wf where
   446 "wf \<Lambda> = True" |
   447 "wf (N _ k t u) =
   448  (if t = \<Lambda> then
   449     k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
   450   else
   451     wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
   452 
   453 fun skew where
   454 "skew \<Lambda> = \<Lambda>" |
   455 "skew (N x k t u) =
   456  (if t \<noteq> \<Lambda> \<and> k = level t then
   457     N (data t) k (left t) (N x k (right t) u)
   458   else
   459     N x k t u)"
   460 
   461 fun split where
   462 "split \<Lambda> = \<Lambda>" |
   463 "split (N x k t u) =
   464  (if u \<noteq> \<Lambda> \<and> k = level (right u) then
   465     N (data u) (Suc k) (N x k t (left u)) (right u)
   466   else
   467     N x k t u)"
   468 
   469 theorem dataset_skew_split:
   470 "dataset (skew t) = dataset t"
   471 "dataset (split t) = dataset t"
   472 nitpick [card = 1\<midarrow>5, expect = none]
   473 sorry
   474 
   475 theorem wf_skew_split:
   476 "wf t \<Longrightarrow> skew t = t"
   477 "wf t \<Longrightarrow> split t = t"
   478 nitpick [card = 1\<midarrow>5, expect = none]
   479 sorry
   480 
   481 primrec insort\<^isub>1 where
   482 "insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   483 "insort\<^isub>1 (N y k t u) x =
   484  (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
   485                              (if x > y then insort\<^isub>1 u x else u))"
   486 
   487 theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
   488 nitpick [expect = genuine]
   489 oops
   490 
   491 theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
   492 nitpick [eval = "insort\<^isub>1 t x", expect = genuine]
   493 oops
   494 
   495 primrec insort\<^isub>2 where
   496 "insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   497 "insort\<^isub>2 (N y k t u) x =
   498  (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
   499                        (if x > y then insort\<^isub>2 u x else u))"
   500 
   501 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
   502 nitpick [card = 1\<midarrow>5, expect = none]
   503 sorry
   504 
   505 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
   506 nitpick [card = 1\<midarrow>5, expect = none]
   507 sorry
   508 
   509 end