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