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