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--
```     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
```