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