src/HOL/Nitpick_Examples/Manual_Nits.thy
author blanchet
Fri Oct 23 18:59:24 2009 +0200 (2009-10-23)
changeset 33197 de6285ebcc05
child 34126 8a2c5d7aff51
permissions -rw-r--r--
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33197
     3
    Copyright   2009
blanchet@33197
     4
blanchet@33197
     5
Examples from the Nitpick manual.
blanchet@33197
     6
*)
blanchet@33197
     7
blanchet@33197
     8
header {* Examples from the Nitpick Manual *}
blanchet@33197
     9
blanchet@33197
    10
theory Manual_Nits
blanchet@33197
    11
imports Main Coinductive_List RealDef
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@33197
    14
chapter {* 3. First Steps *}
blanchet@33197
    15
blanchet@33197
    16
nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
blanchet@33197
    17
blanchet@33197
    18
subsection {* 3.1. Propositional Logic *}
blanchet@33197
    19
blanchet@33197
    20
lemma "P \<longleftrightarrow> Q"
blanchet@33197
    21
nitpick
blanchet@33197
    22
apply auto
blanchet@33197
    23
nitpick 1
blanchet@33197
    24
nitpick 2
blanchet@33197
    25
oops
blanchet@33197
    26
blanchet@33197
    27
subsection {* 3.2. Type Variables *}
blanchet@33197
    28
blanchet@33197
    29
lemma "P x \<Longrightarrow> P (THE y. P y)"
blanchet@33197
    30
nitpick [verbose]
blanchet@33197
    31
oops
blanchet@33197
    32
blanchet@33197
    33
subsection {* 3.3. Constants *}
blanchet@33197
    34
blanchet@33197
    35
lemma "P x \<Longrightarrow> P (THE y. P y)"
blanchet@33197
    36
nitpick [show_consts]
blanchet@33197
    37
nitpick [full_descrs, show_consts]
blanchet@33197
    38
nitpick [dont_specialize, full_descrs, show_consts]
blanchet@33197
    39
oops
blanchet@33197
    40
blanchet@33197
    41
lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
blanchet@33197
    42
nitpick
blanchet@33197
    43
nitpick [card 'a = 1-50]
blanchet@33197
    44
(* sledgehammer *)
blanchet@33197
    45
apply (metis the_equality)
blanchet@33197
    46
done
blanchet@33197
    47
blanchet@33197
    48
subsection {* 3.4. Skolemization *}
blanchet@33197
    49
blanchet@33197
    50
lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
blanchet@33197
    51
nitpick
blanchet@33197
    52
oops
blanchet@33197
    53
blanchet@33197
    54
lemma "\<exists>x. \<forall>f. f x = x"
blanchet@33197
    55
nitpick
blanchet@33197
    56
oops
blanchet@33197
    57
blanchet@33197
    58
lemma "refl r \<Longrightarrow> sym r"
blanchet@33197
    59
nitpick
blanchet@33197
    60
oops
blanchet@33197
    61
blanchet@33197
    62
subsection {* 3.5. Numbers *}
blanchet@33197
    63
blanchet@33197
    64
lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
blanchet@33197
    65
nitpick
blanchet@33197
    66
oops
blanchet@33197
    67
blanchet@33197
    68
lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
blanchet@33197
    69
nitpick [card nat = 100, check_potential]
blanchet@33197
    70
oops
blanchet@33197
    71
blanchet@33197
    72
lemma "P Suc"
blanchet@33197
    73
nitpick [card = 1-6]
blanchet@33197
    74
oops
blanchet@33197
    75
blanchet@33197
    76
lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
blanchet@33197
    77
nitpick [card nat = 1]
blanchet@33197
    78
nitpick [card nat = 2]
blanchet@33197
    79
oops
blanchet@33197
    80
blanchet@33197
    81
subsection {* 3.6. Inductive Datatypes *}
blanchet@33197
    82
blanchet@33197
    83
lemma "hd (xs @ [y, y]) = hd xs"
blanchet@33197
    84
nitpick
blanchet@33197
    85
nitpick [show_consts, show_datatypes]
blanchet@33197
    86
oops
blanchet@33197
    87
blanchet@33197
    88
lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
blanchet@33197
    89
nitpick [show_datatypes]
blanchet@33197
    90
oops
blanchet@33197
    91
blanchet@33197
    92
subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
blanchet@33197
    93
blanchet@33197
    94
typedef three = "{0\<Colon>nat, 1, 2}"
blanchet@33197
    95
by blast
blanchet@33197
    96
blanchet@33197
    97
definition A :: three where "A \<equiv> Abs_three 0"
blanchet@33197
    98
definition B :: three where "B \<equiv> Abs_three 1"
blanchet@33197
    99
definition C :: three where "C \<equiv> Abs_three 2"
blanchet@33197
   100
blanchet@33197
   101
lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
blanchet@33197
   102
nitpick [show_datatypes]
blanchet@33197
   103
oops
blanchet@33197
   104
blanchet@33197
   105
record point =
blanchet@33197
   106
  Xcoord :: int
blanchet@33197
   107
  Ycoord :: int
blanchet@33197
   108
blanchet@33197
   109
lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
blanchet@33197
   110
nitpick [show_datatypes]
blanchet@33197
   111
oops
blanchet@33197
   112
blanchet@33197
   113
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
blanchet@33197
   114
nitpick [show_datatypes]
blanchet@33197
   115
oops
blanchet@33197
   116
blanchet@33197
   117
subsection {* 3.8. Inductive and Coinductive Predicates *}
blanchet@33197
   118
blanchet@33197
   119
inductive even where
blanchet@33197
   120
"even 0" |
blanchet@33197
   121
"even n \<Longrightarrow> even (Suc (Suc n))"
blanchet@33197
   122
blanchet@33197
   123
lemma "\<exists>n. even n \<and> even (Suc n)"
blanchet@33197
   124
nitpick [card nat = 100, verbose]
blanchet@33197
   125
oops
blanchet@33197
   126
blanchet@33197
   127
lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
blanchet@33197
   128
nitpick [card nat = 100]
blanchet@33197
   129
oops
blanchet@33197
   130
blanchet@33197
   131
inductive even' where
blanchet@33197
   132
"even' (0\<Colon>nat)" |
blanchet@33197
   133
"even' 2" |
blanchet@33197
   134
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
blanchet@33197
   135
blanchet@33197
   136
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
blanchet@33197
   137
nitpick [card nat = 10, verbose, show_consts]
blanchet@33197
   138
oops
blanchet@33197
   139
blanchet@33197
   140
lemma "even' (n - 2) \<Longrightarrow> even' n"
blanchet@33197
   141
nitpick [card nat = 10, show_consts]
blanchet@33197
   142
oops
blanchet@33197
   143
blanchet@33197
   144
coinductive nats where
blanchet@33197
   145
"nats (x\<Colon>nat) \<Longrightarrow> nats x"
blanchet@33197
   146
blanchet@33197
   147
lemma "nats = {0, 1, 2, 3, 4}"
blanchet@33197
   148
nitpick [card nat = 10, show_consts]
blanchet@33197
   149
oops
blanchet@33197
   150
blanchet@33197
   151
inductive odd where
blanchet@33197
   152
"odd 1" |
blanchet@33197
   153
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
blanchet@33197
   154
blanchet@33197
   155
lemma "odd n \<Longrightarrow> odd (n - 2)"
blanchet@33197
   156
nitpick [card nat = 10, show_consts]
blanchet@33197
   157
oops
blanchet@33197
   158
blanchet@33197
   159
subsection {* 3.9. Coinductive Datatypes *}
blanchet@33197
   160
blanchet@33197
   161
lemma "xs \<noteq> LCons a xs"
blanchet@33197
   162
nitpick
blanchet@33197
   163
oops
blanchet@33197
   164
blanchet@33197
   165
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
blanchet@33197
   166
nitpick [verbose]
blanchet@33197
   167
nitpick [bisim_depth = -1, verbose]
blanchet@33197
   168
oops
blanchet@33197
   169
blanchet@33197
   170
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
blanchet@33197
   171
nitpick [bisim_depth = -1, show_datatypes]
blanchet@33197
   172
nitpick
blanchet@33197
   173
sorry
blanchet@33197
   174
blanchet@33197
   175
subsection {* 3.10. Boxing *}
blanchet@33197
   176
blanchet@33197
   177
datatype tm = Var nat | Lam tm | App tm tm
blanchet@33197
   178
blanchet@33197
   179
primrec lift where
blanchet@33197
   180
"lift (Var j) k = Var (if j < k then j else j + 1)" |
blanchet@33197
   181
"lift (Lam t) k = Lam (lift t (k + 1))" |
blanchet@33197
   182
"lift (App t u) k = App (lift t k) (lift u k)"
blanchet@33197
   183
blanchet@33197
   184
primrec loose where
blanchet@33197
   185
"loose (Var j) k = (j \<ge> k)" |
blanchet@33197
   186
"loose (Lam t) k = loose t (Suc k)" |
blanchet@33197
   187
"loose (App t u) k = (loose t k \<or> loose u k)"
blanchet@33197
   188
blanchet@33197
   189
primrec subst\<^isub>1 where
blanchet@33197
   190
"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
blanchet@33197
   191
"subst\<^isub>1 \<sigma> (Lam t) =
blanchet@33197
   192
 Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
blanchet@33197
   193
"subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
blanchet@33197
   194
blanchet@33197
   195
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
blanchet@33197
   196
nitpick [verbose]
blanchet@33197
   197
nitpick [eval = "subst\<^isub>1 \<sigma> t"]
blanchet@33197
   198
nitpick [dont_box]
blanchet@33197
   199
oops
blanchet@33197
   200
blanchet@33197
   201
primrec subst\<^isub>2 where
blanchet@33197
   202
"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
blanchet@33197
   203
"subst\<^isub>2 \<sigma> (Lam t) =
blanchet@33197
   204
 Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
blanchet@33197
   205
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
blanchet@33197
   206
blanchet@33197
   207
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
blanchet@33197
   208
nitpick
blanchet@33197
   209
sorry
blanchet@33197
   210
blanchet@33197
   211
subsection {* 3.11. Scope Monotonicity *}
blanchet@33197
   212
blanchet@33197
   213
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
blanchet@33197
   214
nitpick [verbose]
blanchet@33197
   215
nitpick [card = 8, verbose]
blanchet@33197
   216
oops
blanchet@33197
   217
blanchet@33197
   218
lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
blanchet@33197
   219
nitpick [mono]
blanchet@33197
   220
nitpick
blanchet@33197
   221
oops
blanchet@33197
   222
blanchet@33197
   223
section {* 4. Case Studies *}
blanchet@33197
   224
blanchet@33197
   225
nitpick_params [max_potential = 0, max_threads = 2]
blanchet@33197
   226
blanchet@33197
   227
subsection {* 4.1. A Context-Free Grammar *}
blanchet@33197
   228
blanchet@33197
   229
datatype alphabet = a | b
blanchet@33197
   230
blanchet@33197
   231
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
blanchet@33197
   232
  "[] \<in> S\<^isub>1"
blanchet@33197
   233
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
blanchet@33197
   234
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
blanchet@33197
   235
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
blanchet@33197
   236
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
blanchet@33197
   237
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
blanchet@33197
   238
blanchet@33197
   239
theorem S\<^isub>1_sound:
blanchet@33197
   240
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@33197
   241
nitpick
blanchet@33197
   242
oops
blanchet@33197
   243
blanchet@33197
   244
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
blanchet@33197
   245
  "[] \<in> S\<^isub>2"
blanchet@33197
   246
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
blanchet@33197
   247
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
blanchet@33197
   248
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
blanchet@33197
   249
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
blanchet@33197
   250
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
blanchet@33197
   251
blanchet@33197
   252
theorem S\<^isub>2_sound:
blanchet@33197
   253
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@33197
   254
nitpick
blanchet@33197
   255
oops
blanchet@33197
   256
blanchet@33197
   257
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
blanchet@33197
   258
  "[] \<in> S\<^isub>3"
blanchet@33197
   259
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
blanchet@33197
   260
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
blanchet@33197
   261
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
blanchet@33197
   262
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
blanchet@33197
   263
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
blanchet@33197
   264
blanchet@33197
   265
theorem S\<^isub>3_sound:
blanchet@33197
   266
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@33197
   267
nitpick
blanchet@33197
   268
sorry
blanchet@33197
   269
blanchet@33197
   270
theorem S\<^isub>3_complete:
blanchet@33197
   271
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
blanchet@33197
   272
nitpick
blanchet@33197
   273
oops
blanchet@33197
   274
blanchet@33197
   275
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
blanchet@33197
   276
  "[] \<in> S\<^isub>4"
blanchet@33197
   277
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
blanchet@33197
   278
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
blanchet@33197
   279
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
blanchet@33197
   280
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
blanchet@33197
   281
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
blanchet@33197
   282
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
blanchet@33197
   283
blanchet@33197
   284
theorem S\<^isub>4_sound:
blanchet@33197
   285
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@33197
   286
nitpick
blanchet@33197
   287
sorry
blanchet@33197
   288
blanchet@33197
   289
theorem S\<^isub>4_complete:
blanchet@33197
   290
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
blanchet@33197
   291
nitpick
blanchet@33197
   292
sorry
blanchet@33197
   293
blanchet@33197
   294
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
blanchet@33197
   295
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@33197
   296
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
blanchet@33197
   297
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
blanchet@33197
   298
nitpick
blanchet@33197
   299
sorry
blanchet@33197
   300
blanchet@33197
   301
subsection {* 4.2. AA Trees *}
blanchet@33197
   302
blanchet@33197
   303
datatype 'a tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a tree" "'a tree"
blanchet@33197
   304
blanchet@33197
   305
primrec data where
blanchet@33197
   306
"data \<Lambda> = undefined" |
blanchet@33197
   307
"data (N x _ _ _) = x"
blanchet@33197
   308
blanchet@33197
   309
primrec dataset where
blanchet@33197
   310
"dataset \<Lambda> = {}" |
blanchet@33197
   311
"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
blanchet@33197
   312
blanchet@33197
   313
primrec level where
blanchet@33197
   314
"level \<Lambda> = 0" |
blanchet@33197
   315
"level (N _ k _ _) = k"
blanchet@33197
   316
blanchet@33197
   317
primrec left where
blanchet@33197
   318
"left \<Lambda> = \<Lambda>" |
blanchet@33197
   319
"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
blanchet@33197
   320
blanchet@33197
   321
primrec right where
blanchet@33197
   322
"right \<Lambda> = \<Lambda>" |
blanchet@33197
   323
"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
blanchet@33197
   324
blanchet@33197
   325
fun wf where
blanchet@33197
   326
"wf \<Lambda> = True" |
blanchet@33197
   327
"wf (N _ k t u) =
blanchet@33197
   328
 (if t = \<Lambda> then
blanchet@33197
   329
    k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
blanchet@33197
   330
  else
blanchet@33197
   331
    wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
blanchet@33197
   332
blanchet@33197
   333
fun skew where
blanchet@33197
   334
"skew \<Lambda> = \<Lambda>" |
blanchet@33197
   335
"skew (N x k t u) =
blanchet@33197
   336
 (if t \<noteq> \<Lambda> \<and> k = level t then
blanchet@33197
   337
    N (data t) k (left t) (N x k (right t) u)
blanchet@33197
   338
  else
blanchet@33197
   339
    N x k t u)"
blanchet@33197
   340
blanchet@33197
   341
fun split where
blanchet@33197
   342
"split \<Lambda> = \<Lambda>" |
blanchet@33197
   343
"split (N x k t u) =
blanchet@33197
   344
 (if u \<noteq> \<Lambda> \<and> k = level (right u) then
blanchet@33197
   345
    N (data u) (Suc k) (N x k t (left u)) (right u)
blanchet@33197
   346
  else
blanchet@33197
   347
    N x k t u)"
blanchet@33197
   348
blanchet@33197
   349
theorem dataset_skew_split:
blanchet@33197
   350
"dataset (skew t) = dataset t"
blanchet@33197
   351
"dataset (split t) = dataset t"
blanchet@33197
   352
nitpick
blanchet@33197
   353
sorry
blanchet@33197
   354
blanchet@33197
   355
theorem wf_skew_split:
blanchet@33197
   356
"wf t \<Longrightarrow> skew t = t"
blanchet@33197
   357
"wf t \<Longrightarrow> split t = t"
blanchet@33197
   358
nitpick
blanchet@33197
   359
sorry
blanchet@33197
   360
blanchet@33197
   361
primrec insort\<^isub>1 where
blanchet@33197
   362
"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
blanchet@33197
   363
"insort\<^isub>1 (N y k t u) x =
blanchet@33197
   364
 (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
blanchet@33197
   365
                             (if x > y then insort\<^isub>1 u x else u))"
blanchet@33197
   366
blanchet@33197
   367
theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
blanchet@33197
   368
nitpick
blanchet@33197
   369
oops
blanchet@33197
   370
blanchet@33197
   371
theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
blanchet@33197
   372
nitpick [eval = "insort\<^isub>1 t x"]
blanchet@33197
   373
oops
blanchet@33197
   374
blanchet@33197
   375
primrec insort\<^isub>2 where
blanchet@33197
   376
"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
blanchet@33197
   377
"insort\<^isub>2 (N y k t u) x =
blanchet@33197
   378
 (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
blanchet@33197
   379
                       (if x > y then insort\<^isub>2 u x else u))"
blanchet@33197
   380
blanchet@33197
   381
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
blanchet@33197
   382
nitpick
blanchet@33197
   383
sorry
blanchet@33197
   384
blanchet@33197
   385
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
blanchet@33197
   386
nitpick
blanchet@33197
   387
sorry
blanchet@33197
   388
blanchet@33197
   389
end