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