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