src/HOL/Nitpick_Examples/Manual_Nits.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 41278 8e1cde88aae6
child 42208 02513eb26eb7
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35076
     3
    Copyright   2009, 2010
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
wenzelm@41413
    15
imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
blanchet@33197
    16
begin
blanchet@33197
    17
blanchet@33197
    18
chapter {* 3. First Steps *}
blanchet@33197
    19
blanchet@41278
    20
nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
blanchet@41278
    21
                timeout = 60]
blanchet@33197
    22
blanchet@33197
    23
subsection {* 3.1. Propositional Logic *}
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@33197
    32
subsection {* 3.2. Type Variables *}
blanchet@33197
    33
blanchet@33197
    34
lemma "P x \<Longrightarrow> P (THE y. P y)"
blanchet@35671
    35
nitpick [verbose, expect = genuine]
blanchet@33197
    36
oops
blanchet@33197
    37
blanchet@33197
    38
subsection {* 3.3. Constants *}
blanchet@33197
    39
blanchet@33197
    40
lemma "P x \<Longrightarrow> P (THE y. P y)"
blanchet@35671
    41
nitpick [show_consts, expect = genuine]
blanchet@39362
    42
nitpick [dont_specialize, show_consts, expect = genuine]
blanchet@33197
    43
oops
blanchet@33197
    44
blanchet@33197
    45
lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
blanchet@35671
    46
nitpick [expect = none]
blanchet@35671
    47
nitpick [card 'a = 1\<midarrow>50, expect = none]
blanchet@33197
    48
(* sledgehammer *)
blanchet@33197
    49
apply (metis the_equality)
blanchet@33197
    50
done
blanchet@33197
    51
blanchet@33197
    52
subsection {* 3.4. Skolemization *}
blanchet@33197
    53
blanchet@33197
    54
lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
blanchet@35671
    55
nitpick [expect = genuine]
blanchet@33197
    56
oops
blanchet@33197
    57
blanchet@33197
    58
lemma "\<exists>x. \<forall>f. f x = x"
blanchet@35671
    59
nitpick [expect = genuine]
blanchet@33197
    60
oops
blanchet@33197
    61
blanchet@33197
    62
lemma "refl r \<Longrightarrow> sym r"
blanchet@35671
    63
nitpick [expect = genuine]
blanchet@33197
    64
oops
blanchet@33197
    65
blanchet@34126
    66
subsection {* 3.5. Natural Numbers and Integers *}
blanchet@33197
    67
blanchet@33197
    68
lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
blanchet@35671
    69
nitpick [expect = genuine]
blanchet@33197
    70
oops
blanchet@33197
    71
blanchet@33197
    72
lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
blanchet@35671
    73
nitpick [card nat = 100, check_potential, expect = genuine]
blanchet@33197
    74
oops
blanchet@33197
    75
blanchet@33197
    76
lemma "P Suc"
blanchet@35671
    77
nitpick [expect = none]
blanchet@33197
    78
oops
blanchet@33197
    79
blanchet@33197
    80
lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
blanchet@35671
    81
nitpick [card nat = 1, expect = genuine]
blanchet@35671
    82
nitpick [card nat = 2, expect = none]
blanchet@33197
    83
oops
blanchet@33197
    84
blanchet@33197
    85
subsection {* 3.6. Inductive Datatypes *}
blanchet@33197
    86
blanchet@33197
    87
lemma "hd (xs @ [y, y]) = hd xs"
blanchet@35671
    88
nitpick [expect = genuine]
blanchet@35671
    89
nitpick [show_consts, show_datatypes, expect = genuine]
blanchet@33197
    90
oops
blanchet@33197
    91
blanchet@33197
    92
lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
blanchet@35671
    93
nitpick [show_datatypes, expect = genuine]
blanchet@33197
    94
oops
blanchet@33197
    95
blanchet@33197
    96
subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
blanchet@33197
    97
blanchet@33197
    98
typedef three = "{0\<Colon>nat, 1, 2}"
blanchet@33197
    99
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@33197
   105
lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P 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
blanchet@35284
   119
blanchet@35284
   120
lemma "add x y = add x x"
blanchet@35671
   121
nitpick [show_datatypes, expect = genuine]
blanchet@35284
   122
oops
blanchet@35284
   123
blanchet@35711
   124
ML {*
blanchet@35712
   125
fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
blanchet@35712
   126
    HOLogic.mk_number T (snd (HOLogic.dest_number t1)
blanchet@35712
   127
                         - snd (HOLogic.dest_number t2))
blanchet@35712
   128
  | my_int_postproc _ _ _ _ t = t
blanchet@35711
   129
*}
blanchet@35711
   130
blanchet@38288
   131
declaration {*
blanchet@38284
   132
Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
blanchet@38242
   133
*}
blanchet@35711
   134
blanchet@35711
   135
lemma "add x y = add x x"
blanchet@35711
   136
nitpick [show_datatypes]
blanchet@35711
   137
oops
blanchet@35711
   138
blanchet@33197
   139
record point =
blanchet@33197
   140
  Xcoord :: int
blanchet@33197
   141
  Ycoord :: int
blanchet@33197
   142
blanchet@33197
   143
lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
blanchet@35671
   144
nitpick [show_datatypes, expect = genuine]
blanchet@33197
   145
oops
blanchet@33197
   146
blanchet@33197
   147
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
blanchet@35671
   148
nitpick [show_datatypes, expect = genuine]
blanchet@33197
   149
oops
blanchet@33197
   150
blanchet@33197
   151
subsection {* 3.8. Inductive and Coinductive Predicates *}
blanchet@33197
   152
blanchet@33197
   153
inductive even where
blanchet@33197
   154
"even 0" |
blanchet@33197
   155
"even n \<Longrightarrow> even (Suc (Suc n))"
blanchet@33197
   156
blanchet@33197
   157
lemma "\<exists>n. even n \<and> even (Suc n)"
blanchet@35710
   158
nitpick [card nat = 50, unary_ints, verbose, expect = potential]
blanchet@33197
   159
oops
blanchet@33197
   160
blanchet@35710
   161
lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
blanchet@38184
   162
nitpick [card nat = 50, unary_ints, expect = genuine]
blanchet@33197
   163
oops
blanchet@33197
   164
blanchet@33197
   165
inductive even' where
blanchet@33197
   166
"even' (0\<Colon>nat)" |
blanchet@33197
   167
"even' 2" |
blanchet@33197
   168
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
blanchet@33197
   169
blanchet@33197
   170
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
blanchet@35671
   171
nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
blanchet@33197
   172
oops
blanchet@33197
   173
blanchet@33197
   174
lemma "even' (n - 2) \<Longrightarrow> even' n"
blanchet@35671
   175
nitpick [card nat = 10, show_consts, expect = genuine]
blanchet@33197
   176
oops
blanchet@33197
   177
blanchet@33197
   178
coinductive nats where
blanchet@33197
   179
"nats (x\<Colon>nat) \<Longrightarrow> nats x"
blanchet@33197
   180
blanchet@33197
   181
lemma "nats = {0, 1, 2, 3, 4}"
blanchet@35671
   182
nitpick [card nat = 10, show_consts, expect = genuine]
blanchet@33197
   183
oops
blanchet@33197
   184
blanchet@33197
   185
inductive odd where
blanchet@33197
   186
"odd 1" |
blanchet@33197
   187
"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
blanchet@33197
   188
blanchet@33197
   189
lemma "odd n \<Longrightarrow> odd (n - 2)"
blanchet@35671
   190
nitpick [card nat = 10, show_consts, expect = genuine]
blanchet@33197
   191
oops
blanchet@33197
   192
blanchet@33197
   193
subsection {* 3.9. Coinductive Datatypes *}
blanchet@33197
   194
blanchet@35665
   195
(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
blanchet@38184
   196
   we cannot rely on its presence, we expediently provide our own
blanchet@38184
   197
   axiomatization. The examples also work unchanged with Lochbihler's
blanchet@38184
   198
   "Coinductive_List" theory. *)
blanchet@35665
   199
blanchet@35665
   200
typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
blanchet@35665
   201
blanchet@35671
   202
definition LNil where
blanchet@35671
   203
"LNil = Abs_llist (Inl [])"
blanchet@35665
   204
definition LCons where
blanchet@35665
   205
"LCons y ys = Abs_llist (case Rep_llist ys of
blanchet@35665
   206
                           Inl ys' \<Rightarrow> Inl (y # ys')
blanchet@35665
   207
                         | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
blanchet@35665
   208
blanchet@35665
   209
axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
blanchet@35665
   210
blanchet@35665
   211
lemma iterates_def [nitpick_simp]:
blanchet@35665
   212
"iterates f a = LCons a (iterates f (f a))"
blanchet@35665
   213
sorry
blanchet@35665
   214
blanchet@38288
   215
declaration {*
blanchet@38284
   216
Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
blanchet@35665
   217
    (map dest_Const [@{term LNil}, @{term LCons}])
blanchet@35665
   218
*}
blanchet@35665
   219
blanchet@33197
   220
lemma "xs \<noteq> LCons a xs"
blanchet@35671
   221
nitpick [expect = genuine]
blanchet@33197
   222
oops
blanchet@33197
   223
blanchet@33197
   224
lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
blanchet@35671
   225
nitpick [verbose, expect = genuine]
blanchet@33197
   226
oops
blanchet@33197
   227
blanchet@33197
   228
lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
blanchet@35671
   229
nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
blanchet@38184
   230
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   231
sorry
blanchet@33197
   232
blanchet@33197
   233
subsection {* 3.10. Boxing *}
blanchet@33197
   234
blanchet@33197
   235
datatype tm = Var nat | Lam tm | App tm tm
blanchet@33197
   236
blanchet@33197
   237
primrec lift where
blanchet@33197
   238
"lift (Var j) k = Var (if j < k then j else j + 1)" |
blanchet@33197
   239
"lift (Lam t) k = Lam (lift t (k + 1))" |
blanchet@33197
   240
"lift (App t u) k = App (lift t k) (lift u k)"
blanchet@33197
   241
blanchet@33197
   242
primrec loose where
blanchet@33197
   243
"loose (Var j) k = (j \<ge> k)" |
blanchet@33197
   244
"loose (Lam t) k = loose t (Suc k)" |
blanchet@33197
   245
"loose (App t u) k = (loose t k \<or> loose u k)"
blanchet@33197
   246
blanchet@33197
   247
primrec subst\<^isub>1 where
blanchet@33197
   248
"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
blanchet@33197
   249
"subst\<^isub>1 \<sigma> (Lam t) =
blanchet@33197
   250
 Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
blanchet@33197
   251
"subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
blanchet@33197
   252
blanchet@33197
   253
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
blanchet@35671
   254
nitpick [verbose, expect = genuine]
blanchet@35671
   255
nitpick [eval = "subst\<^isub>1 \<sigma> t", expect = genuine]
blanchet@35671
   256
(* nitpick [dont_box, expect = unknown] *)
blanchet@33197
   257
oops
blanchet@33197
   258
blanchet@33197
   259
primrec subst\<^isub>2 where
blanchet@33197
   260
"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
blanchet@33197
   261
"subst\<^isub>2 \<sigma> (Lam t) =
blanchet@33197
   262
 Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
blanchet@33197
   263
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
blanchet@33197
   264
blanchet@33197
   265
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
blanchet@35710
   266
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   267
sorry
blanchet@33197
   268
blanchet@33197
   269
subsection {* 3.11. Scope Monotonicity *}
blanchet@33197
   270
blanchet@33197
   271
lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
blanchet@35671
   272
nitpick [verbose, expect = genuine]
blanchet@33197
   273
oops
blanchet@33197
   274
blanchet@33197
   275
lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
blanchet@35671
   276
nitpick [mono, expect = none]
blanchet@35671
   277
nitpick [expect = genuine]
blanchet@33197
   278
oops
blanchet@33197
   279
blanchet@34982
   280
subsection {* 3.12. Inductive Properties *}
blanchet@34982
   281
blanchet@34982
   282
inductive_set reach where
blanchet@34982
   283
"(4\<Colon>nat) \<in> reach" |
blanchet@34982
   284
"n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
blanchet@34982
   285
"n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
blanchet@34982
   286
blanchet@34982
   287
lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
blanchet@38184
   288
(* nitpick *)
blanchet@34982
   289
apply (induct set: reach)
blanchet@34982
   290
  apply auto
blanchet@38184
   291
 nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
blanchet@34982
   292
 apply (thin_tac "n \<in> reach")
blanchet@35671
   293
 nitpick [expect = genuine]
blanchet@34982
   294
oops
blanchet@34982
   295
blanchet@34982
   296
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
blanchet@38184
   297
(* nitpick *)
blanchet@34982
   298
apply (induct set: reach)
blanchet@34982
   299
  apply auto
blanchet@38184
   300
 nitpick [card = 1\<midarrow>4, bits = 1\<midarrow>4, expect = none]
blanchet@34982
   301
 apply (thin_tac "n \<in> reach")
blanchet@35671
   302
 nitpick [expect = genuine]
blanchet@34982
   303
oops
blanchet@34982
   304
blanchet@34982
   305
lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
blanchet@34982
   306
by (induct set: reach) arith+
blanchet@34982
   307
blanchet@34982
   308
datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
blanchet@34982
   309
blanchet@34982
   310
primrec labels where
blanchet@34982
   311
"labels (Leaf a) = {a}" |
blanchet@34982
   312
"labels (Branch t u) = labels t \<union> labels u"
blanchet@34982
   313
blanchet@34982
   314
primrec swap where
blanchet@34982
   315
"swap (Leaf c) a b =
blanchet@34982
   316
 (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
blanchet@34982
   317
"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
blanchet@34982
   318
blanchet@35180
   319
lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
blanchet@35671
   320
(* nitpick *)
blanchet@34982
   321
proof (induct t)
blanchet@34982
   322
  case Leaf thus ?case by simp
blanchet@34982
   323
next
blanchet@34982
   324
  case (Branch t u) thus ?case
blanchet@35671
   325
  (* nitpick *)
blanchet@35671
   326
  nitpick [non_std, show_all, expect = genuine]
blanchet@34982
   327
oops
blanchet@34982
   328
blanchet@34982
   329
lemma "labels (swap t a b) =
blanchet@34982
   330
       (if a \<in> labels t then
blanchet@34982
   331
          if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
blanchet@34982
   332
        else
blanchet@34982
   333
          if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
blanchet@35309
   334
(* nitpick *)
blanchet@34982
   335
proof (induct t)
blanchet@34982
   336
  case Leaf thus ?case by simp
blanchet@34982
   337
next
blanchet@34982
   338
  case (Branch t u) thus ?case
blanchet@38184
   339
  nitpick [non_std, card = 1\<midarrow>4, expect = none]
blanchet@34982
   340
  by auto
blanchet@34982
   341
qed
blanchet@34982
   342
blanchet@33197
   343
section {* 4. Case Studies *}
blanchet@33197
   344
blanchet@36268
   345
nitpick_params [max_potential = 0]
blanchet@33197
   346
blanchet@33197
   347
subsection {* 4.1. A Context-Free Grammar *}
blanchet@33197
   348
blanchet@33197
   349
datatype alphabet = a | b
blanchet@33197
   350
blanchet@33197
   351
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
blanchet@33197
   352
  "[] \<in> S\<^isub>1"
blanchet@33197
   353
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
blanchet@33197
   354
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
blanchet@33197
   355
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
blanchet@33197
   356
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
blanchet@33197
   357
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
blanchet@33197
   358
blanchet@33197
   359
theorem S\<^isub>1_sound:
blanchet@33197
   360
"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@35671
   361
nitpick [expect = genuine]
blanchet@33197
   362
oops
blanchet@33197
   363
blanchet@33197
   364
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
blanchet@33197
   365
  "[] \<in> S\<^isub>2"
blanchet@33197
   366
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
blanchet@33197
   367
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
blanchet@33197
   368
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
blanchet@33197
   369
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
blanchet@33197
   370
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
blanchet@33197
   371
blanchet@33197
   372
theorem S\<^isub>2_sound:
blanchet@33197
   373
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@35671
   374
nitpick [expect = genuine]
blanchet@33197
   375
oops
blanchet@33197
   376
blanchet@33197
   377
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
blanchet@33197
   378
  "[] \<in> S\<^isub>3"
blanchet@33197
   379
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
blanchet@33197
   380
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
blanchet@33197
   381
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
blanchet@33197
   382
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
blanchet@33197
   383
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
blanchet@33197
   384
blanchet@33197
   385
theorem S\<^isub>3_sound:
blanchet@33197
   386
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@37477
   387
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   388
sorry
blanchet@33197
   389
blanchet@33197
   390
theorem S\<^isub>3_complete:
blanchet@33197
   391
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
blanchet@35671
   392
nitpick [expect = genuine]
blanchet@33197
   393
oops
blanchet@33197
   394
blanchet@33197
   395
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
blanchet@33197
   396
  "[] \<in> S\<^isub>4"
blanchet@33197
   397
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
blanchet@33197
   398
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
blanchet@33197
   399
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
blanchet@33197
   400
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
blanchet@33197
   401
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
blanchet@33197
   402
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
blanchet@33197
   403
blanchet@33197
   404
theorem S\<^isub>4_sound:
blanchet@33197
   405
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@37477
   406
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   407
sorry
blanchet@33197
   408
blanchet@33197
   409
theorem S\<^isub>4_complete:
blanchet@33197
   410
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
blanchet@37477
   411
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   412
sorry
blanchet@33197
   413
blanchet@33197
   414
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
blanchet@33197
   415
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
blanchet@33197
   416
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
blanchet@33197
   417
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
blanchet@37477
   418
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   419
sorry
blanchet@33197
   420
blanchet@33197
   421
subsection {* 4.2. AA Trees *}
blanchet@33197
   422
blanchet@34982
   423
datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
blanchet@33197
   424
blanchet@33197
   425
primrec data where
blanchet@33197
   426
"data \<Lambda> = undefined" |
blanchet@33197
   427
"data (N x _ _ _) = x"
blanchet@33197
   428
blanchet@33197
   429
primrec dataset where
blanchet@33197
   430
"dataset \<Lambda> = {}" |
blanchet@33197
   431
"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
blanchet@33197
   432
blanchet@33197
   433
primrec level where
blanchet@33197
   434
"level \<Lambda> = 0" |
blanchet@33197
   435
"level (N _ k _ _) = k"
blanchet@33197
   436
blanchet@33197
   437
primrec left where
blanchet@33197
   438
"left \<Lambda> = \<Lambda>" |
blanchet@33197
   439
"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
blanchet@33197
   440
blanchet@33197
   441
primrec right where
blanchet@33197
   442
"right \<Lambda> = \<Lambda>" |
blanchet@33197
   443
"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
blanchet@33197
   444
blanchet@33197
   445
fun wf where
blanchet@33197
   446
"wf \<Lambda> = True" |
blanchet@33197
   447
"wf (N _ k t u) =
blanchet@33197
   448
 (if t = \<Lambda> then
blanchet@33197
   449
    k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
blanchet@33197
   450
  else
blanchet@33197
   451
    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
   452
blanchet@33197
   453
fun skew where
blanchet@33197
   454
"skew \<Lambda> = \<Lambda>" |
blanchet@33197
   455
"skew (N x k t u) =
blanchet@33197
   456
 (if t \<noteq> \<Lambda> \<and> k = level t then
blanchet@33197
   457
    N (data t) k (left t) (N x k (right t) u)
blanchet@33197
   458
  else
blanchet@33197
   459
    N x k t u)"
blanchet@33197
   460
blanchet@33197
   461
fun split where
blanchet@33197
   462
"split \<Lambda> = \<Lambda>" |
blanchet@33197
   463
"split (N x k t u) =
blanchet@33197
   464
 (if u \<noteq> \<Lambda> \<and> k = level (right u) then
blanchet@33197
   465
    N (data u) (Suc k) (N x k t (left u)) (right u)
blanchet@33197
   466
  else
blanchet@33197
   467
    N x k t u)"
blanchet@33197
   468
blanchet@33197
   469
theorem dataset_skew_split:
blanchet@33197
   470
"dataset (skew t) = dataset t"
blanchet@33197
   471
"dataset (split t) = dataset t"
blanchet@35747
   472
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   473
sorry
blanchet@33197
   474
blanchet@33197
   475
theorem wf_skew_split:
blanchet@33197
   476
"wf t \<Longrightarrow> skew t = t"
blanchet@33197
   477
"wf t \<Longrightarrow> split t = t"
blanchet@35747
   478
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   479
sorry
blanchet@33197
   480
blanchet@33197
   481
primrec insort\<^isub>1 where
blanchet@33197
   482
"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
blanchet@33197
   483
"insort\<^isub>1 (N y k t u) x =
blanchet@33197
   484
 (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
blanchet@33197
   485
                             (if x > y then insort\<^isub>1 u x else u))"
blanchet@33197
   486
blanchet@33197
   487
theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
blanchet@35671
   488
nitpick [expect = genuine]
blanchet@33197
   489
oops
blanchet@33197
   490
blanchet@33197
   491
theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
blanchet@35671
   492
nitpick [eval = "insort\<^isub>1 t x", expect = genuine]
blanchet@33197
   493
oops
blanchet@33197
   494
blanchet@33197
   495
primrec insort\<^isub>2 where
blanchet@33197
   496
"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
blanchet@33197
   497
"insort\<^isub>2 (N y k t u) x =
blanchet@33197
   498
 (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
blanchet@33197
   499
                       (if x > y then insort\<^isub>2 u x else u))"
blanchet@33197
   500
blanchet@33197
   501
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
blanchet@35747
   502
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   503
sorry
blanchet@33197
   504
blanchet@33197
   505
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
blanchet@35747
   506
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   507
sorry
blanchet@33197
   508
blanchet@33197
   509
end