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