src/ZF/List.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
added Tools/lin_arith.ML;
clasohm@1478
     1
(*  Title:      ZF/List
lcp@516
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     4
    Copyright   1994  University of Cambridge
lcp@516
     5
lcp@516
     6
*)
lcp@516
     7
paulson@13327
     8
header{*Lists in Zermelo-Fraenkel Set Theory*}
paulson@13327
     9
haftmann@16417
    10
theory List imports Datatype ArithSimp begin
lcp@516
    11
lcp@516
    12
consts
paulson@12789
    13
  list       :: "i=>i"
paulson@13327
    14
lcp@516
    15
datatype
lcp@581
    16
  "list(A)" = Nil | Cons ("a:A", "l: list(A)")
lcp@516
    17
lcp@516
    18
wenzelm@2539
    19
syntax
wenzelm@2539
    20
 "[]"        :: i                                       ("[]")
paulson@12789
    21
 "@List"     :: "is => i"                                 ("[(_)]")
wenzelm@2539
    22
lcp@516
    23
translations
lcp@516
    24
  "[x, xs]"     == "Cons(x, [xs])"
lcp@516
    25
  "[x]"         == "Cons(x, [])"
lcp@516
    26
  "[]"          == "Nil"
lcp@516
    27
lcp@516
    28
paulson@6053
    29
consts
paulson@12789
    30
  length :: "i=>i"
paulson@13396
    31
  hd     :: "i=>i"
paulson@13396
    32
  tl     :: "i=>i"
paulson@6053
    33
paulson@6053
    34
primrec
paulson@6053
    35
  "length([]) = 0"
paulson@6053
    36
  "length(Cons(a,l)) = succ(length(l))"
paulson@13327
    37
paulson@6053
    38
primrec
paulson@13396
    39
  "hd([]) = 0"
paulson@6053
    40
  "hd(Cons(a,l)) = a"
paulson@6053
    41
paulson@6053
    42
primrec
paulson@6053
    43
  "tl([]) = []"
paulson@6053
    44
  "tl(Cons(a,l)) = l"
paulson@6053
    45
paulson@6070
    46
paulson@6070
    47
consts
paulson@13327
    48
  map         :: "[i=>i, i] => i"
paulson@12789
    49
  set_of_list :: "i=>i"
paulson@13327
    50
  app         :: "[i,i]=>i"                        (infixr "@" 60)
paulson@13327
    51
paulson@13327
    52
(*map is a binding operator -- it applies to meta-level functions, not
paulson@13327
    53
object-level functions.  This simplifies the final form of term_rec_conv,
paulson@13327
    54
although complicating its derivation.*)
paulson@6053
    55
primrec
paulson@6053
    56
  "map(f,[]) = []"
paulson@6053
    57
  "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
paulson@13327
    58
paulson@6053
    59
primrec
paulson@6053
    60
  "set_of_list([]) = 0"
paulson@6053
    61
  "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
paulson@13327
    62
paulson@6053
    63
primrec
paulson@13327
    64
  app_Nil:  "[] @ ys = ys"
paulson@13327
    65
  app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
paulson@13327
    66
paulson@6070
    67
paulson@6070
    68
consts
paulson@12789
    69
  rev :: "i=>i"
paulson@12789
    70
  flat       :: "i=>i"
paulson@12789
    71
  list_add   :: "i=>i"
paulson@6070
    72
paulson@6053
    73
primrec
paulson@6053
    74
  "rev([]) = []"
paulson@6053
    75
  "rev(Cons(a,l)) = rev(l) @ [a]"
paulson@6053
    76
paulson@6053
    77
primrec
paulson@6053
    78
  "flat([]) = []"
paulson@6053
    79
  "flat(Cons(l,ls)) = l @ flat(ls)"
paulson@13327
    80
paulson@6053
    81
primrec
paulson@6053
    82
  "list_add([]) = 0"
paulson@6053
    83
  "list_add(Cons(a,l)) = a #+ list_add(l)"
paulson@13327
    84
paulson@6070
    85
consts
paulson@12789
    86
  drop       :: "[i,i]=>i"
paulson@6070
    87
paulson@6070
    88
primrec
paulson@13327
    89
  drop_0:    "drop(0,l) = l"
paulson@13387
    90
  drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
lcp@516
    91
paulson@12789
    92
paulson@12789
    93
(*** Thanks to Sidi Ehmety for the following ***)
paulson@12789
    94
paulson@12789
    95
constdefs
paulson@12789
    96
(* Function `take' returns the first n elements of a list *)
paulson@12789
    97
  take     :: "[i,i]=>i"
paulson@12789
    98
  "take(n, as) == list_rec(lam n:nat. [],
paulson@12789
    99
		%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
paulson@13327
   100
paulson@12789
   101
  nth :: "[i, i]=>i"
paulson@13387
   102
  --{*returns the (n+1)th element of a list, or 0 if the
paulson@13387
   103
   list is too short.*}
paulson@12789
   104
  "nth(n, as) == list_rec(lam n:nat. 0,
paulson@13387
   105
 		          %a l r. lam n:nat. nat_case(a, %m. r`m, n), as) ` n"
paulson@12789
   106
paulson@12789
   107
  list_update :: "[i, i, i]=>i"
paulson@12789
   108
  "list_update(xs, i, v) == list_rec(lam n:nat. Nil,
paulson@12789
   109
      %u us vs. lam n:nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"
paulson@12789
   110
paulson@12789
   111
consts
paulson@12789
   112
  filter :: "[i=>o, i] => i"
paulson@12789
   113
  upt :: "[i, i] =>i"
paulson@12789
   114
paulson@12789
   115
primrec
paulson@12789
   116
  "filter(P, Nil) = Nil"
paulson@12789
   117
  "filter(P, Cons(x, xs)) =
paulson@12789
   118
     (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"
paulson@12789
   119
paulson@12789
   120
primrec
paulson@12789
   121
  "upt(i, 0) = Nil"
paulson@12789
   122
  "upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)"
paulson@12789
   123
paulson@12789
   124
constdefs
paulson@12789
   125
  min :: "[i,i] =>i"
paulson@12789
   126
    "min(x, y) == (if x le y then x else y)"
paulson@13327
   127
paulson@12789
   128
  max :: "[i, i] =>i"
paulson@12789
   129
    "max(x, y) == (if x le y then y else x)"
paulson@12789
   130
paulson@13327
   131
(*** Aspects of the datatype definition ***)
paulson@13327
   132
paulson@13327
   133
declare list.intros [simp,TC]
paulson@13327
   134
paulson@13327
   135
(*An elimination rule, for type-checking*)
paulson@13327
   136
inductive_cases ConsE: "Cons(a,l) : list(A)"
paulson@13327
   137
paulson@14055
   138
lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
paulson@13509
   139
by (blast elim: ConsE) 
paulson@13509
   140
paulson@13327
   141
(*Proving freeness results*)
paulson@13327
   142
lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
paulson@13327
   143
by auto
paulson@13327
   144
paulson@13327
   145
lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
paulson@13327
   146
by auto
paulson@13327
   147
paulson@13327
   148
lemma list_unfold: "list(A) = {0} + (A * list(A))"
paulson@13327
   149
by (blast intro!: list.intros [unfolded list.con_defs]
paulson@13327
   150
          elim: list.cases [unfolded list.con_defs])
paulson@13327
   151
paulson@13327
   152
paulson@13327
   153
(**  Lemmas to justify using "list" in other recursive type definitions **)
paulson@13327
   154
paulson@13327
   155
lemma list_mono: "A<=B ==> list(A) <= list(B)"
paulson@13327
   156
apply (unfold list.defs )
paulson@13327
   157
apply (rule lfp_mono)
paulson@13327
   158
apply (simp_all add: list.bnd_mono)
paulson@13327
   159
apply (assumption | rule univ_mono basic_monos)+
paulson@13327
   160
done
paulson@13327
   161
paulson@13327
   162
(*There is a similar proof by list induction.*)
paulson@13327
   163
lemma list_univ: "list(univ(A)) <= univ(A)"
paulson@13327
   164
apply (unfold list.defs list.con_defs)
paulson@13327
   165
apply (rule lfp_lowerbound)
paulson@13327
   166
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
paulson@13327
   167
apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
paulson@13327
   168
done
paulson@13327
   169
paulson@13327
   170
(*These two theorems justify datatypes involving list(nat), list(A), ...*)
paulson@13327
   171
lemmas list_subset_univ = subset_trans [OF list_mono list_univ]
paulson@13327
   172
paulson@13327
   173
lemma list_into_univ: "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)"
paulson@13327
   174
by (blast intro: list_subset_univ [THEN subsetD])
paulson@13327
   175
paulson@13327
   176
lemma list_case_type:
paulson@13327
   177
    "[| l: list(A);
paulson@13327
   178
        c: C(Nil);
paulson@13327
   179
        !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))
paulson@13327
   180
     |] ==> list_case(c,h,l) : C(l)"
paulson@13387
   181
by (erule list.induct, auto)
paulson@13387
   182
paulson@13387
   183
lemma list_0_triv: "list(0) = {Nil}"
paulson@13387
   184
apply (rule equalityI, auto) 
paulson@13387
   185
apply (induct_tac x, auto) 
paulson@13327
   186
done
paulson@13327
   187
paulson@13327
   188
paulson@13327
   189
(*** List functions ***)
paulson@13327
   190
paulson@13327
   191
lemma tl_type: "l: list(A) ==> tl(l) : list(A)"
paulson@13327
   192
apply (induct_tac "l")
paulson@13327
   193
apply (simp_all (no_asm_simp) add: list.intros)
paulson@13327
   194
done
paulson@13327
   195
paulson@13327
   196
(** drop **)
paulson@13327
   197
paulson@13327
   198
lemma drop_Nil [simp]: "i:nat ==> drop(i, Nil) = Nil"
paulson@13327
   199
apply (induct_tac "i")
paulson@13327
   200
apply (simp_all (no_asm_simp))
paulson@13327
   201
done
paulson@13327
   202
paulson@13327
   203
lemma drop_succ_Cons [simp]: "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"
paulson@13327
   204
apply (rule sym)
paulson@13327
   205
apply (induct_tac "i")
paulson@13327
   206
apply (simp (no_asm))
paulson@13327
   207
apply (simp (no_asm_simp))
paulson@13327
   208
done
paulson@13327
   209
paulson@13327
   210
lemma drop_type [simp,TC]: "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"
paulson@13327
   211
apply (induct_tac "i")
paulson@13327
   212
apply (simp_all (no_asm_simp) add: tl_type)
paulson@13327
   213
done
paulson@13327
   214
paulson@13387
   215
declare drop_succ [simp del]
paulson@13327
   216
paulson@13327
   217
paulson@13327
   218
(** Type checking -- proved by induction, as usual **)
paulson@13327
   219
paulson@13327
   220
lemma list_rec_type [TC]:
paulson@13327
   221
    "[| l: list(A);
paulson@13327
   222
        c: C(Nil);
paulson@13327
   223
        !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))
paulson@13327
   224
     |] ==> list_rec(c,h,l) : C(l)"
paulson@13327
   225
by (induct_tac "l", auto)
paulson@13327
   226
paulson@13327
   227
(** map **)
paulson@13327
   228
paulson@13327
   229
lemma map_type [TC]:
paulson@13327
   230
    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"
paulson@13327
   231
apply (simp add: map_list_def)
paulson@13327
   232
apply (typecheck add: list.intros list_rec_type, blast)
paulson@13327
   233
done
paulson@13327
   234
paulson@13327
   235
lemma map_type2 [TC]: "l: list(A) ==> map(h,l) : list({h(u). u:A})"
paulson@13327
   236
apply (erule map_type)
paulson@13327
   237
apply (erule RepFunI)
paulson@13327
   238
done
paulson@13327
   239
paulson@13327
   240
(** length **)
paulson@13327
   241
paulson@13327
   242
lemma length_type [TC]: "l: list(A) ==> length(l) : nat"
paulson@13327
   243
by (simp add: length_list_def)
paulson@13327
   244
paulson@13327
   245
lemma lt_length_in_nat:
paulson@14055
   246
   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
paulson@13327
   247
by (frule lt_nat_in_nat, typecheck) 
paulson@13327
   248
paulson@13327
   249
(** app **)
paulson@13327
   250
paulson@13327
   251
lemma app_type [TC]: "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)"
paulson@13327
   252
by (simp add: app_list_def)
paulson@13327
   253
paulson@13327
   254
(** rev **)
paulson@13327
   255
paulson@13327
   256
lemma rev_type [TC]: "xs: list(A) ==> rev(xs) : list(A)"
paulson@13327
   257
by (simp add: rev_list_def)
paulson@13327
   258
paulson@13327
   259
paulson@13327
   260
(** flat **)
paulson@13327
   261
paulson@13327
   262
lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) : list(A)"
paulson@13327
   263
by (simp add: flat_list_def)
paulson@13327
   264
paulson@13327
   265
paulson@13327
   266
(** set_of_list **)
paulson@13327
   267
paulson@13327
   268
lemma set_of_list_type [TC]: "l: list(A) ==> set_of_list(l) : Pow(A)"
paulson@13327
   269
apply (unfold set_of_list_list_def)
paulson@13327
   270
apply (erule list_rec_type, auto)
paulson@13327
   271
done
paulson@13327
   272
paulson@13327
   273
lemma set_of_list_append:
paulson@13327
   274
     "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)"
paulson@13327
   275
apply (erule list.induct)
paulson@13327
   276
apply (simp_all (no_asm_simp) add: Un_cons)
paulson@13327
   277
done
paulson@13327
   278
paulson@13327
   279
paulson@13327
   280
(** list_add **)
paulson@13327
   281
paulson@13327
   282
lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) : nat"
paulson@13327
   283
by (simp add: list_add_list_def)
paulson@13327
   284
paulson@13327
   285
paulson@13327
   286
(*** theorems about map ***)
paulson@13327
   287
paulson@13327
   288
lemma map_ident [simp]: "l: list(A) ==> map(%u. u, l) = l"
paulson@13327
   289
apply (induct_tac "l")
paulson@13327
   290
apply (simp_all (no_asm_simp))
paulson@13327
   291
done
paulson@13327
   292
paulson@13327
   293
lemma map_compose: "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"
paulson@13327
   294
apply (induct_tac "l")
paulson@13327
   295
apply (simp_all (no_asm_simp))
paulson@13327
   296
done
paulson@13327
   297
paulson@13327
   298
lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"
paulson@13327
   299
apply (induct_tac "xs")
paulson@13327
   300
apply (simp_all (no_asm_simp))
paulson@13327
   301
done
paulson@13327
   302
paulson@13327
   303
lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"
paulson@13327
   304
apply (induct_tac "ls")
paulson@13327
   305
apply (simp_all (no_asm_simp) add: map_app_distrib)
paulson@13327
   306
done
paulson@13327
   307
paulson@13327
   308
lemma list_rec_map:
paulson@13327
   309
     "l: list(A) ==>
paulson@13327
   310
      list_rec(c, d, map(h,l)) =
paulson@13327
   311
      list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
paulson@13327
   312
apply (induct_tac "l")
paulson@13327
   313
apply (simp_all (no_asm_simp))
paulson@13327
   314
done
paulson@13327
   315
paulson@13327
   316
(** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
paulson@13327
   317
paulson@13327
   318
(* c : list(Collect(B,P)) ==> c : list(B) *)
paulson@13327
   319
lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard]
paulson@13327
   320
paulson@13327
   321
lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
paulson@13327
   322
apply (induct_tac "l")
paulson@13327
   323
apply (simp_all (no_asm_simp))
paulson@13327
   324
done
paulson@13327
   325
paulson@13327
   326
(*** theorems about length ***)
paulson@13327
   327
paulson@13327
   328
lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
paulson@13387
   329
by (induct_tac "xs", simp_all)
paulson@13327
   330
paulson@13327
   331
lemma length_app [simp]:
paulson@13327
   332
     "[| xs: list(A); ys: list(A) |]
paulson@13327
   333
      ==> length(xs@ys) = length(xs) #+ length(ys)"
paulson@13387
   334
by (induct_tac "xs", simp_all)
paulson@13327
   335
paulson@13327
   336
lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
paulson@13327
   337
apply (induct_tac "xs")
paulson@13327
   338
apply (simp_all (no_asm_simp) add: length_app)
paulson@13327
   339
done
paulson@13327
   340
paulson@13327
   341
lemma length_flat:
paulson@13327
   342
     "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"
paulson@13327
   343
apply (induct_tac "ls")
paulson@13327
   344
apply (simp_all (no_asm_simp) add: length_app)
paulson@13327
   345
done
paulson@13327
   346
paulson@13327
   347
(** Length and drop **)
paulson@13327
   348
paulson@13327
   349
(*Lemma for the inductive step of drop_length*)
paulson@13327
   350
lemma drop_length_Cons [rule_format]:
paulson@13327
   351
     "xs: list(A) ==>
paulson@14055
   352
           \<forall>x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
paulson@13387
   353
by (erule list.induct, simp_all)
paulson@13327
   354
paulson@13327
   355
lemma drop_length [rule_format]:
paulson@14055
   356
     "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
paulson@13784
   357
apply (erule list.induct, simp_all, safe)
paulson@13327
   358
apply (erule drop_length_Cons)
paulson@13327
   359
apply (rule natE)
paulson@13387
   360
apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
paulson@13327
   361
apply (blast intro: succ_in_naturalD length_type)
paulson@13327
   362
done
paulson@13327
   363
paulson@13327
   364
paulson@13327
   365
(*** theorems about app ***)
paulson@13327
   366
paulson@13327
   367
lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
paulson@13387
   368
by (erule list.induct, simp_all)
paulson@13327
   369
paulson@13327
   370
lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
paulson@13387
   371
by (induct_tac "xs", simp_all)
paulson@13327
   372
paulson@13327
   373
lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
paulson@13327
   374
apply (induct_tac "ls")
paulson@13327
   375
apply (simp_all (no_asm_simp) add: app_assoc)
paulson@13327
   376
done
paulson@13327
   377
paulson@13327
   378
(*** theorems about rev ***)
paulson@13327
   379
paulson@13327
   380
lemma rev_map_distrib: "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"
paulson@13327
   381
apply (induct_tac "l")
paulson@13327
   382
apply (simp_all (no_asm_simp) add: map_app_distrib)
paulson@13327
   383
done
paulson@13327
   384
paulson@13327
   385
(*Simplifier needs the premises as assumptions because rewriting will not
paulson@13327
   386
  instantiate the variable ?A in the rules' typing conditions; note that
paulson@13327
   387
  rev_type does not instantiate ?A.  Only the premises do.
paulson@13327
   388
*)
paulson@13327
   389
lemma rev_app_distrib:
paulson@13327
   390
     "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"
paulson@13327
   391
apply (erule list.induct)
paulson@13327
   392
apply (simp_all add: app_assoc)
paulson@13327
   393
done
paulson@13327
   394
paulson@13327
   395
lemma rev_rev_ident [simp]: "l: list(A) ==> rev(rev(l))=l"
paulson@13327
   396
apply (induct_tac "l")
paulson@13327
   397
apply (simp_all (no_asm_simp) add: rev_app_distrib)
paulson@13327
   398
done
paulson@13327
   399
paulson@13327
   400
lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"
paulson@13327
   401
apply (induct_tac "ls")
paulson@13327
   402
apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib)
paulson@13327
   403
done
paulson@13327
   404
paulson@13327
   405
paulson@13327
   406
(*** theorems about list_add ***)
paulson@13327
   407
paulson@13327
   408
lemma list_add_app:
paulson@13327
   409
     "[| xs: list(nat);  ys: list(nat) |]
paulson@13327
   410
      ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
paulson@13387
   411
apply (induct_tac "xs", simp_all)
paulson@13327
   412
done
paulson@13327
   413
paulson@13327
   414
lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)"
paulson@13327
   415
apply (induct_tac "l")
paulson@13327
   416
apply (simp_all (no_asm_simp) add: list_add_app)
paulson@13327
   417
done
paulson@13327
   418
paulson@13327
   419
lemma list_add_flat:
paulson@13327
   420
     "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
paulson@13327
   421
apply (induct_tac "ls")
paulson@13327
   422
apply (simp_all (no_asm_simp) add: list_add_app)
paulson@13327
   423
done
paulson@13327
   424
paulson@13509
   425
(** New induction rules **)
paulson@13327
   426
wenzelm@13524
   427
lemma list_append_induct [case_names Nil snoc, consumes 1]:
paulson@13327
   428
    "[| l: list(A);
paulson@13327
   429
        P(Nil);
paulson@13327
   430
        !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])
paulson@13327
   431
     |] ==> P(l)"
paulson@13327
   432
apply (subgoal_tac "P(rev(rev(l)))", simp)
paulson@13327
   433
apply (erule rev_type [THEN list.induct], simp_all)
paulson@13327
   434
done
paulson@13327
   435
paulson@13509
   436
lemma list_complete_induct_lemma [rule_format]:
paulson@13509
   437
 assumes ih: 
paulson@14055
   438
    "\<And>l. [| l \<in> list(A); 
paulson@14055
   439
             \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|] 
paulson@13509
   440
          ==> P(l)"
paulson@14055
   441
  shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n --> P(l)"
paulson@13509
   442
apply (induct_tac n, simp)
paulson@13509
   443
apply (blast intro: ih elim!: leE) 
paulson@13509
   444
done
paulson@13509
   445
paulson@13509
   446
theorem list_complete_induct:
paulson@14055
   447
      "[| l \<in> list(A); 
paulson@14055
   448
          \<And>l. [| l \<in> list(A); 
paulson@14055
   449
                  \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|] 
paulson@13509
   450
               ==> P(l)
paulson@13509
   451
       |] ==> P(l)"
paulson@13509
   452
apply (rule list_complete_induct_lemma [of A]) 
paulson@13509
   453
   prefer 4 apply (rule le_refl, simp) 
paulson@13509
   454
  apply blast 
paulson@13509
   455
 apply simp 
paulson@13509
   456
apply assumption
paulson@13509
   457
done
paulson@13509
   458
paulson@13327
   459
paulson@13327
   460
(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
paulson@13327
   461
paulson@13327
   462
(** min FIXME: replace by Int! **)
paulson@13327
   463
(* Min theorems are also true for i, j ordinals *)
paulson@13327
   464
lemma min_sym: "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)"
paulson@13327
   465
apply (unfold min_def)
paulson@13327
   466
apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
paulson@13327
   467
done
paulson@13327
   468
paulson@13327
   469
lemma min_type [simp,TC]: "[| i:nat; j:nat |] ==> min(i,j):nat"
paulson@13327
   470
by (unfold min_def, auto)
paulson@13327
   471
paulson@13327
   472
lemma min_0 [simp]: "i:nat ==> min(0,i) = 0"
paulson@13327
   473
apply (unfold min_def)
paulson@13327
   474
apply (auto dest: not_lt_imp_le)
paulson@13327
   475
done
paulson@13327
   476
paulson@13327
   477
lemma min_02 [simp]: "i:nat ==> min(i, 0) = 0"
paulson@13327
   478
apply (unfold min_def)
paulson@13327
   479
apply (auto dest: not_lt_imp_le)
paulson@13327
   480
done
paulson@13327
   481
paulson@13327
   482
lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k"
paulson@13327
   483
apply (unfold min_def)
paulson@13327
   484
apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
paulson@13327
   485
done
paulson@13327
   486
paulson@13327
   487
lemma min_succ_succ [simp]:
paulson@13327
   488
     "[| i:nat; j:nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))"
paulson@13327
   489
apply (unfold min_def, auto)
paulson@13327
   490
done
paulson@13327
   491
paulson@13327
   492
(*** more theorems about lists ***)
paulson@13327
   493
paulson@13327
   494
(** filter **)
paulson@13327
   495
paulson@13327
   496
lemma filter_append [simp]:
paulson@13327
   497
     "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"
paulson@13327
   498
by (induct_tac "xs", auto)
paulson@13327
   499
paulson@13327
   500
lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)"
paulson@13327
   501
by (induct_tac "xs", auto)
paulson@13327
   502
paulson@13327
   503
lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) le length(xs)"
paulson@13327
   504
apply (induct_tac "xs", auto)
paulson@13327
   505
apply (rule_tac j = "length (l) " in le_trans)
paulson@13327
   506
apply (auto simp add: le_iff)
paulson@13327
   507
done
paulson@13327
   508
paulson@13327
   509
lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)"
paulson@13327
   510
by (induct_tac "xs", auto)
paulson@13327
   511
paulson@13327
   512
lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil"
paulson@13327
   513
by (induct_tac "xs", auto)
paulson@13327
   514
paulson@13327
   515
lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs"
paulson@13327
   516
by (induct_tac "xs", auto)
paulson@13327
   517
paulson@13327
   518
(** length **)
paulson@13327
   519
paulson@13327
   520
lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil"
paulson@13327
   521
by (erule list.induct, auto)
paulson@13327
   522
paulson@13327
   523
lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"
paulson@13327
   524
by (erule list.induct, auto)
paulson@13327
   525
paulson@13327
   526
lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
paulson@13327
   527
by (erule list.induct, auto)
paulson@13327
   528
paulson@13327
   529
lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil"
paulson@13327
   530
by (erule list.induct, auto)
paulson@13327
   531
paulson@13327
   532
lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)"
paulson@13327
   533
by (erule list.induct, auto)
paulson@13327
   534
paulson@13327
   535
(** more theorems about append **)
paulson@13327
   536
paulson@13327
   537
lemma append_is_Nil_iff [simp]:
paulson@13327
   538
     "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"
paulson@13327
   539
by (erule list.induct, auto)
paulson@13327
   540
paulson@13327
   541
lemma append_is_Nil_iff2 [simp]:
paulson@13327
   542
     "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"
paulson@13327
   543
by (erule list.induct, auto)
paulson@13327
   544
paulson@13327
   545
lemma append_left_is_self_iff [simp]:
paulson@13327
   546
     "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"
paulson@13327
   547
by (erule list.induct, auto)
paulson@13327
   548
paulson@13327
   549
lemma append_left_is_self_iff2 [simp]:
paulson@13327
   550
     "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"
paulson@13327
   551
by (erule list.induct, auto)
paulson@13327
   552
paulson@13327
   553
(*TOO SLOW as a default simprule!*)
paulson@13327
   554
lemma append_left_is_Nil_iff [rule_format]:
paulson@13327
   555
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
paulson@13327
   556
   length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))"
paulson@13327
   557
apply (erule list.induct)
paulson@13327
   558
apply (auto simp add: length_app)
paulson@13327
   559
done
paulson@13327
   560
paulson@13327
   561
(*TOO SLOW as a default simprule!*)
paulson@13327
   562
lemma append_left_is_Nil_iff2 [rule_format]:
paulson@13327
   563
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
paulson@13327
   564
   length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))"
paulson@13327
   565
apply (erule list.induct)
paulson@13327
   566
apply (auto simp add: length_app)
paulson@13327
   567
done
paulson@13327
   568
paulson@13327
   569
lemma append_eq_append_iff [rule_format,simp]:
paulson@14055
   570
     "xs:list(A) ==> \<forall>ys \<in> list(A).
paulson@13327
   571
      length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
paulson@13327
   572
apply (erule list.induct)
paulson@13327
   573
apply (simp (no_asm_simp))
paulson@13327
   574
apply clarify
paulson@13387
   575
apply (erule_tac a = ys in list.cases, auto)
paulson@13327
   576
done
paulson@13327
   577
paulson@13327
   578
lemma append_eq_append [rule_format]:
paulson@13327
   579
  "xs:list(A) ==>
paulson@14055
   580
   \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
paulson@13327
   581
   length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)"
paulson@13327
   582
apply (induct_tac "xs")
paulson@13327
   583
apply (force simp add: length_app, clarify)
paulson@13387
   584
apply (erule_tac a = ys in list.cases, simp)
paulson@13327
   585
apply (subgoal_tac "Cons (a, l) @ us =vs")
paulson@13387
   586
 apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
paulson@13327
   587
done
paulson@13327
   588
paulson@13327
   589
lemma append_eq_append_iff2 [simp]:
paulson@13327
   590
 "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
paulson@13327
   591
  ==>  xs@us = ys@vs <-> (xs=ys & us=vs)"
paulson@13327
   592
apply (rule iffI)
paulson@13327
   593
apply (rule append_eq_append, auto)
paulson@13327
   594
done
paulson@13327
   595
paulson@13327
   596
lemma append_self_iff [simp]:
paulson@13327
   597
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
paulson@13509
   598
by simp
paulson@13327
   599
paulson@13327
   600
lemma append_self_iff2 [simp]:
paulson@13327
   601
     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
paulson@13509
   602
by simp
paulson@13327
   603
paulson@13327
   604
(* Can also be proved from append_eq_append_iff2,
paulson@13327
   605
but the proof requires two more hypotheses: x:A and y:A *)
paulson@13327
   606
lemma append1_eq_iff [rule_format,simp]:
paulson@14055
   607
     "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
paulson@13327
   608
apply (erule list.induct)  
paulson@13327
   609
 apply clarify 
paulson@13327
   610
 apply (erule list.cases)
paulson@13327
   611
 apply simp_all
paulson@13327
   612
txt{*Inductive step*}  
paulson@13327
   613
apply clarify 
paulson@13339
   614
apply (erule_tac a=ys in list.cases, simp_all)  
paulson@13327
   615
done
paulson@13327
   616
paulson@13327
   617
paulson@13327
   618
lemma append_right_is_self_iff [simp]:
paulson@13327
   619
     "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
paulson@13509
   620
by (simp (no_asm_simp) add: append_left_is_Nil_iff)
paulson@13327
   621
paulson@13327
   622
lemma append_right_is_self_iff2 [simp]:
paulson@13327
   623
     "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
paulson@13327
   624
apply (rule iffI)
paulson@13327
   625
apply (drule sym, auto) 
paulson@13327
   626
done
paulson@13327
   627
paulson@13327
   628
lemma hd_append [rule_format,simp]:
paulson@13327
   629
     "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)"
paulson@13327
   630
by (induct_tac "xs", auto)
paulson@13327
   631
paulson@13327
   632
lemma tl_append [rule_format,simp]:
paulson@13327
   633
     "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys"
paulson@13327
   634
by (induct_tac "xs", auto)
paulson@13327
   635
paulson@13327
   636
(** rev **)
paulson@13327
   637
lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"
paulson@13327
   638
by (erule list.induct, auto)
paulson@13327
   639
paulson@13327
   640
lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"
paulson@13327
   641
by (erule list.induct, auto)
paulson@13327
   642
paulson@13327
   643
lemma rev_is_rev_iff [rule_format,simp]:
paulson@14055
   644
     "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
paulson@13387
   645
apply (erule list.induct, force, clarify)
paulson@13387
   646
apply (erule_tac a = ys in list.cases, auto)
paulson@13327
   647
done
paulson@13327
   648
paulson@13327
   649
lemma rev_list_elim [rule_format]:
paulson@13327
   650
     "xs:list(A) ==>
paulson@14055
   651
      (xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P"
paulson@13509
   652
by (erule list_append_induct, auto)
paulson@13327
   653
paulson@13327
   654
paulson@13327
   655
(** more theorems about drop **)
paulson@13327
   656
paulson@13327
   657
lemma length_drop [rule_format,simp]:
paulson@14055
   658
     "n:nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
paulson@13327
   659
apply (erule nat_induct)
paulson@13327
   660
apply (auto elim: list.cases)
paulson@13327
   661
done
paulson@13327
   662
paulson@13327
   663
lemma drop_all [rule_format,simp]:
paulson@14055
   664
     "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n --> drop(n, xs)=Nil"
paulson@13327
   665
apply (erule nat_induct)
paulson@13327
   666
apply (auto elim: list.cases)
paulson@13327
   667
done
paulson@13327
   668
paulson@13327
   669
lemma drop_append [rule_format]:
paulson@13327
   670
     "n:nat ==> 
paulson@14055
   671
      \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
paulson@13327
   672
apply (induct_tac "n")
paulson@13327
   673
apply (auto elim: list.cases)
paulson@13327
   674
done
paulson@13327
   675
paulson@13327
   676
lemma drop_drop:
paulson@14055
   677
    "m:nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
paulson@13327
   678
apply (induct_tac "m")
paulson@13327
   679
apply (auto elim: list.cases)
paulson@13327
   680
done
paulson@13327
   681
paulson@13327
   682
(** take **)
paulson@13327
   683
paulson@13327
   684
lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) =  Nil"
paulson@13327
   685
apply (unfold take_def)
paulson@13327
   686
apply (erule list.induct, auto)
paulson@13327
   687
done
paulson@13327
   688
paulson@13327
   689
lemma take_succ_Cons [simp]:
paulson@13327
   690
    "n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"
paulson@13327
   691
by (simp add: take_def)
paulson@13327
   692
paulson@13327
   693
(* Needed for proving take_all *)
paulson@13327
   694
lemma take_Nil [simp]: "n:nat ==> take(n, Nil) = Nil"
paulson@13327
   695
by (unfold take_def, auto)
paulson@13327
   696
paulson@13327
   697
lemma take_all [rule_format,simp]:
paulson@14055
   698
     "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n  --> take(n, xs) = xs"
paulson@13327
   699
apply (erule nat_induct)
paulson@13327
   700
apply (auto elim: list.cases) 
paulson@13327
   701
done
paulson@13327
   702
paulson@13327
   703
lemma take_type [rule_format,simp,TC]:
paulson@14055
   704
     "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
paulson@13387
   705
apply (erule list.induct, simp, clarify) 
paulson@13327
   706
apply (erule natE, auto)
paulson@13327
   707
done
paulson@13327
   708
paulson@13327
   709
lemma take_append [rule_format,simp]:
paulson@13327
   710
 "xs:list(A) ==>
paulson@14055
   711
  \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
paulson@13327
   712
                            take(n, xs) @ take(n #- length(xs), ys)"
paulson@13387
   713
apply (erule list.induct, simp, clarify) 
paulson@13327
   714
apply (erule natE, auto)
paulson@13327
   715
done
paulson@13327
   716
paulson@13327
   717
lemma take_take [rule_format]:
paulson@13327
   718
   "m : nat ==>
paulson@14055
   719
    \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
paulson@13327
   720
apply (induct_tac "m", auto)
paulson@13387
   721
apply (erule_tac a = xs in list.cases)
paulson@13327
   722
apply (auto simp add: take_Nil)
paulson@13615
   723
apply (erule_tac n=n in natE)
paulson@13327
   724
apply (auto intro: take_0 take_type)
paulson@13327
   725
done
paulson@13327
   726
paulson@13327
   727
(** nth **)
paulson@13327
   728
paulson@13387
   729
lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
paulson@13387
   730
by (simp add: nth_def) 
paulson@13387
   731
paulson@13387
   732
lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
paulson@13387
   733
by (simp add: nth_def) 
paulson@13327
   734
paulson@13387
   735
lemma nth_empty [simp]: "nth(n, Nil) = 0"
paulson@13387
   736
by (simp add: nth_def) 
paulson@13387
   737
paulson@13387
   738
lemma nth_type [rule_format,simp,TC]:
paulson@14055
   739
     "xs:list(A) ==> \<forall>n. n < length(xs) --> nth(n,xs) : A"
paulson@14046
   740
apply (erule list.induct, simp, clarify)
paulson@14055
   741
apply (subgoal_tac "n \<in> nat")  
paulson@14046
   742
 apply (erule natE, auto dest!: le_in_nat)
paulson@13327
   743
done
paulson@13327
   744
paulson@13387
   745
lemma nth_eq_0 [rule_format]:
paulson@14055
   746
     "xs:list(A) ==> \<forall>n \<in> nat. length(xs) le n --> nth(n,xs) = 0"
paulson@13387
   747
apply (erule list.induct, simp, clarify) 
paulson@13327
   748
apply (erule natE, auto)
paulson@13327
   749
done
paulson@13327
   750
paulson@13327
   751
lemma nth_append [rule_format]:
paulson@13327
   752
  "xs:list(A) ==> 
paulson@14055
   753
   \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
paulson@13387
   754
                                else nth(n #- length(xs), ys))"
paulson@13387
   755
apply (induct_tac "xs", simp, clarify) 
paulson@13327
   756
apply (erule natE, auto)
paulson@13327
   757
done
paulson@13327
   758
paulson@13327
   759
lemma set_of_list_conv_nth:
paulson@13327
   760
    "xs:list(A)
paulson@13387
   761
     ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x = nth(i,xs)}"
paulson@13327
   762
apply (induct_tac "xs", simp_all)
paulson@13327
   763
apply (rule equalityI, auto)
paulson@13387
   764
apply (rule_tac x = 0 in bexI, auto)
paulson@13327
   765
apply (erule natE, auto)
paulson@13327
   766
done
paulson@13327
   767
paulson@13327
   768
(* Other theorems about lists *)
paulson@13327
   769
paulson@13327
   770
lemma nth_take_lemma [rule_format]:
paulson@13327
   771
 "k:nat ==>
paulson@14055
   772
  \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) -->
paulson@14055
   773
      (\<forall>i \<in> nat. i<k --> nth(i,xs) = nth(i,ys))--> take(k,xs) = take(k,ys))"
paulson@13327
   774
apply (induct_tac "k")
paulson@13327
   775
apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
paulson@13327
   776
apply clarify
paulson@13327
   777
(*Both lists are non-empty*)
paulson@13387
   778
apply (erule_tac a=xs in list.cases, simp) 
paulson@13387
   779
apply (erule_tac a=ys in list.cases, clarify) 
paulson@13327
   780
apply (simp (no_asm_use) )
paulson@13327
   781
apply clarify
paulson@13327
   782
apply (simp (no_asm_simp))
paulson@13327
   783
apply (rule conjI, force)
paulson@13327
   784
apply (rename_tac y ys z zs) 
paulson@13387
   785
apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)   
paulson@13327
   786
done
paulson@13327
   787
paulson@13327
   788
lemma nth_equalityI [rule_format]:
paulson@13327
   789
     "[| xs:list(A); ys:list(A); length(xs) = length(ys);
paulson@14055
   790
         \<forall>i \<in> nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]
paulson@13327
   791
      ==> xs = ys"
paulson@13327
   792
apply (subgoal_tac "length (xs) le length (ys) ")
paulson@13327
   793
apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma) 
paulson@13327
   794
apply (simp_all add: take_all)
paulson@13327
   795
done
paulson@13327
   796
paulson@13327
   797
(*The famous take-lemma*)
paulson@13327
   798
paulson@13327
   799
lemma take_equalityI [rule_format]:
paulson@14055
   800
    "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |] 
paulson@13327
   801
     ==> xs = ys"
paulson@13327
   802
apply (case_tac "length (xs) le length (ys) ")
paulson@13327
   803
apply (drule_tac x = "length (ys) " in bspec)
paulson@13327
   804
apply (drule_tac [3] not_lt_imp_le)
paulson@13327
   805
apply (subgoal_tac [5] "length (ys) le length (xs) ")
paulson@13327
   806
apply (rule_tac [6] j = "succ (length (ys))" in le_trans)
paulson@13327
   807
apply (rule_tac [6] leI)
paulson@13327
   808
apply (drule_tac [5] x = "length (xs) " in bspec)
paulson@13327
   809
apply (simp_all add: take_all)
paulson@13327
   810
done
paulson@13327
   811
paulson@13327
   812
lemma nth_drop [rule_format]:
paulson@14055
   813
  "n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
paulson@13387
   814
apply (induct_tac "n", simp_all, clarify)
paulson@13387
   815
apply (erule list.cases, auto)  
paulson@13327
   816
done
paulson@13327
   817
paulson@14055
   818
lemma take_succ [rule_format]:
paulson@14055
   819
  "xs\<in>list(A) 
paulson@14055
   820
   ==> \<forall>i. i < length(xs) --> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]"
paulson@14055
   821
apply (induct_tac "xs", auto)
paulson@14055
   822
apply (subgoal_tac "i\<in>nat") 
paulson@14055
   823
apply (erule natE)
paulson@14055
   824
apply (auto simp add: le_in_nat) 
paulson@14055
   825
done
paulson@14055
   826
paulson@14055
   827
lemma take_add [rule_format]:
paulson@14055
   828
     "[|xs\<in>list(A); j\<in>nat|] 
paulson@14055
   829
      ==> \<forall>i\<in>nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))"
paulson@14055
   830
apply (induct_tac "xs", simp_all, clarify)
paulson@14055
   831
apply (erule_tac n = i in natE, simp_all)
paulson@14055
   832
done
paulson@14055
   833
paulson@14076
   834
lemma length_take:
paulson@14076
   835
     "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
paulson@14076
   836
apply (induct_tac "l", safe, simp_all)
paulson@14076
   837
apply (erule natE, simp_all)
paulson@14076
   838
done
paulson@14076
   839
paulson@13327
   840
subsection{*The function zip*}
paulson@13327
   841
paulson@13327
   842
text{*Crafty definition to eliminate a type argument*}
paulson@13327
   843
paulson@13327
   844
consts
paulson@13327
   845
  zip_aux        :: "[i,i]=>i"
paulson@13327
   846
paulson@13327
   847
primrec (*explicit lambda is required because both arguments of "un" vary*)
paulson@13327
   848
  "zip_aux(B,[]) =
paulson@14055
   849
     (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
paulson@13327
   850
paulson@13327
   851
  "zip_aux(B,Cons(x,l)) =
paulson@14055
   852
     (\<lambda>ys \<in> list(B).
paulson@13327
   853
        list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
paulson@13327
   854
paulson@13327
   855
constdefs
paulson@13327
   856
  zip :: "[i, i]=>i"
paulson@13327
   857
   "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys"
paulson@13327
   858
paulson@13327
   859
paulson@13327
   860
(* zip equations *)
paulson@13327
   861
paulson@14055
   862
lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))"
paulson@13327
   863
apply (induct_tac xs, simp_all) 
paulson@13327
   864
apply (blast intro: list_mono [THEN subsetD]) 
paulson@13327
   865
done
paulson@13327
   866
paulson@13327
   867
lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil"
paulson@13327
   868
apply (simp add: zip_def list_on_set_of_list [of _ A])
paulson@13327
   869
apply (erule list.cases, simp_all) 
paulson@13327
   870
done
paulson@13327
   871
paulson@13327
   872
lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil"
paulson@13327
   873
apply (simp add: zip_def list_on_set_of_list [of _ A])
paulson@13327
   874
apply (erule list.cases, simp_all) 
paulson@13327
   875
done
paulson@13327
   876
paulson@13327
   877
lemma zip_aux_unique [rule_format]:
paulson@14055
   878
     "[|B<=C;  xs \<in> list(A)|] 
paulson@14055
   879
      ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
paulson@13327
   880
apply (induct_tac xs) 
paulson@13327
   881
 apply simp_all 
paulson@13327
   882
 apply (blast intro: list_mono [THEN subsetD], clarify) 
paulson@13387
   883
apply (erule_tac a=ys in list.cases, auto) 
paulson@13327
   884
apply (blast intro: list_mono [THEN subsetD]) 
paulson@13327
   885
done
paulson@13327
   886
paulson@13327
   887
lemma zip_Cons_Cons [simp]:
paulson@13327
   888
     "[| xs:list(A); ys:list(B); x:A; y:B |] ==>
paulson@13327
   889
      zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
paulson@13327
   890
apply (simp add: zip_def, auto) 
paulson@13327
   891
apply (rule zip_aux_unique, auto) 
paulson@13327
   892
apply (simp add: list_on_set_of_list [of _ B])
paulson@13327
   893
apply (blast intro: list_on_set_of_list list_mono [THEN subsetD]) 
paulson@13327
   894
done
paulson@13327
   895
paulson@13327
   896
lemma zip_type [rule_format,simp,TC]:
paulson@14055
   897
     "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
paulson@13327
   898
apply (induct_tac "xs")
paulson@13327
   899
apply (simp (no_asm))
paulson@13327
   900
apply clarify
paulson@13387
   901
apply (erule_tac a = ys in list.cases, auto)
paulson@13327
   902
done
paulson@13327
   903
paulson@13327
   904
(* zip length *)
paulson@13327
   905
lemma length_zip [rule_format,simp]:
paulson@14055
   906
     "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
paulson@13327
   907
                                     min(length(xs), length(ys))"
paulson@13327
   908
apply (unfold min_def)
paulson@13387
   909
apply (induct_tac "xs", simp_all, clarify) 
paulson@13339
   910
apply (erule_tac a = ys in list.cases, auto)
paulson@13327
   911
done
paulson@13327
   912
paulson@13327
   913
lemma zip_append1 [rule_format]:
paulson@13327
   914
 "[| ys:list(A); zs:list(B) |] ==>
paulson@14055
   915
  \<forall>xs \<in> list(A). zip(xs @ ys, zs) = 
paulson@13327
   916
                 zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
paulson@13387
   917
apply (induct_tac "zs", force, clarify) 
paulson@13387
   918
apply (erule_tac a = xs in list.cases, simp_all) 
paulson@13327
   919
done
paulson@13327
   920
paulson@13327
   921
lemma zip_append2 [rule_format]:
paulson@14055
   922
 "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
paulson@13327
   923
       zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
paulson@13387
   924
apply (induct_tac "xs", force, clarify) 
paulson@13387
   925
apply (erule_tac a = ys in list.cases, auto)
paulson@13327
   926
done
paulson@13327
   927
paulson@13327
   928
lemma zip_append [simp]:
paulson@13327
   929
 "[| length(xs) = length(us); length(ys) = length(vs);
paulson@13327
   930
     xs:list(A); us:list(B); ys:list(A); vs:list(B) |] 
paulson@13327
   931
  ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"
paulson@13327
   932
by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
paulson@13327
   933
paulson@13327
   934
paulson@13327
   935
lemma zip_rev [rule_format,simp]:
paulson@14055
   936
 "ys:list(B) ==> \<forall>xs \<in> list(A).
paulson@13327
   937
    length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
paulson@13387
   938
apply (induct_tac "ys", force, clarify) 
paulson@13387
   939
apply (erule_tac a = xs in list.cases)
paulson@13327
   940
apply (auto simp add: length_rev)
paulson@13327
   941
done
paulson@13327
   942
paulson@13327
   943
lemma nth_zip [rule_format,simp]:
paulson@14055
   944
   "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
paulson@13327
   945
                    i < length(xs) --> i < length(ys) -->
paulson@13327
   946
                    nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
paulson@13387
   947
apply (induct_tac "ys", force, clarify) 
paulson@13387
   948
apply (erule_tac a = xs in list.cases, simp) 
paulson@13327
   949
apply (auto elim: natE)
paulson@13327
   950
done
paulson@13327
   951
paulson@13327
   952
lemma set_of_list_zip [rule_format]:
paulson@13327
   953
     "[| xs:list(A); ys:list(B); i:nat |]
paulson@13327
   954
      ==> set_of_list(zip(xs, ys)) =
paulson@13327
   955
          {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))
paulson@13387
   956
          & x = nth(i, xs) & y = nth(i, ys)}"
paulson@13327
   957
by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
paulson@13327
   958
paulson@13327
   959
(** list_update **)
paulson@13327
   960
paulson@13327
   961
lemma list_update_Nil [simp]: "i:nat ==>list_update(Nil, i, v) = Nil"
paulson@13327
   962
by (unfold list_update_def, auto)
paulson@13327
   963
paulson@13327
   964
lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)"
paulson@13327
   965
by (unfold list_update_def, auto)
paulson@13327
   966
paulson@13327
   967
lemma list_update_Cons_succ [simp]:
paulson@13327
   968
  "n:nat ==>
paulson@13327
   969
    list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"
paulson@13327
   970
apply (unfold list_update_def, auto)
paulson@13327
   971
done
paulson@13327
   972
paulson@13327
   973
lemma list_update_type [rule_format,simp,TC]:
paulson@14055
   974
     "[| xs:list(A); v:A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
paulson@13327
   975
apply (induct_tac "xs")
paulson@13327
   976
apply (simp (no_asm))
paulson@13327
   977
apply clarify
paulson@13327
   978
apply (erule natE, auto)
paulson@13327
   979
done
paulson@13327
   980
paulson@13327
   981
lemma length_list_update [rule_format,simp]:
paulson@14055
   982
     "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
paulson@13327
   983
apply (induct_tac "xs")
paulson@13327
   984
apply (simp (no_asm))
paulson@13327
   985
apply clarify
paulson@13327
   986
apply (erule natE, auto)
paulson@13327
   987
done
paulson@13327
   988
paulson@13327
   989
lemma nth_list_update [rule_format]:
paulson@14055
   990
     "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs)  -->
paulson@13327
   991
         nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
paulson@13327
   992
apply (induct_tac "xs")
paulson@13327
   993
 apply simp_all
paulson@13327
   994
apply clarify
paulson@13327
   995
apply (rename_tac i j) 
paulson@13327
   996
apply (erule_tac n=i in natE) 
paulson@13327
   997
apply (erule_tac [2] n=j in natE)
paulson@13327
   998
apply (erule_tac n=j in natE, simp_all, force) 
paulson@13327
   999
done
paulson@13327
  1000
paulson@13327
  1001
lemma nth_list_update_eq [simp]:
paulson@13327
  1002
     "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x"
paulson@13327
  1003
by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
paulson@13327
  1004
paulson@13327
  1005
paulson@13327
  1006
lemma nth_list_update_neq [rule_format,simp]:
paulson@13387
  1007
  "xs:list(A) ==> 
paulson@14055
  1008
     \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)"
paulson@13327
  1009
apply (induct_tac "xs")
paulson@13327
  1010
 apply (simp (no_asm))
paulson@13327
  1011
apply clarify
paulson@13327
  1012
apply (erule natE)
paulson@13327
  1013
apply (erule_tac [2] natE, simp_all) 
paulson@13327
  1014
apply (erule natE, simp_all)
paulson@13327
  1015
done
paulson@13327
  1016
paulson@13327
  1017
lemma list_update_overwrite [rule_format,simp]:
paulson@14055
  1018
     "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
paulson@13327
  1019
   --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
paulson@13327
  1020
apply (induct_tac "xs")
paulson@13327
  1021
 apply (simp (no_asm))
paulson@13327
  1022
apply clarify
paulson@13327
  1023
apply (erule natE, auto)
paulson@13327
  1024
done
paulson@13327
  1025
paulson@13327
  1026
lemma list_update_same_conv [rule_format]:
paulson@13387
  1027
     "xs:list(A) ==> 
paulson@14055
  1028
      \<forall>i \<in> nat. i < length(xs) --> 
paulson@13387
  1029
                 (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
paulson@13327
  1030
apply (induct_tac "xs")
paulson@13327
  1031
 apply (simp (no_asm))
paulson@13327
  1032
apply clarify
paulson@13327
  1033
apply (erule natE, auto)
paulson@13327
  1034
done
paulson@13327
  1035
paulson@13327
  1036
lemma update_zip [rule_format]:
paulson@13387
  1037
     "ys:list(B) ==> 
paulson@14055
  1038
      \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
paulson@13387
  1039
        length(xs) = length(ys) -->
paulson@13387
  1040
        list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
paulson@13387
  1041
                                              list_update(ys, i, snd(xy)))"
paulson@13327
  1042
apply (induct_tac "ys")
paulson@13327
  1043
 apply auto
paulson@13387
  1044
apply (erule_tac a = xs in list.cases)
paulson@13327
  1045
apply (auto elim: natE)
paulson@13327
  1046
done
paulson@13327
  1047
paulson@13327
  1048
lemma set_update_subset_cons [rule_format]:
paulson@13339
  1049
  "xs:list(A) ==> 
paulson@14055
  1050
   \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))"
paulson@13327
  1051
apply (induct_tac "xs")
paulson@13327
  1052
 apply simp
paulson@13327
  1053
apply (rule ballI)
paulson@13387
  1054
apply (erule natE, simp_all, auto)
paulson@13327
  1055
done
paulson@13327
  1056
paulson@13327
  1057
lemma set_of_list_update_subsetI:
paulson@13327
  1058
     "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|]
paulson@13327
  1059
   ==> set_of_list(list_update(xs, i,x)) <= A"
paulson@13327
  1060
apply (rule subset_trans)
paulson@13327
  1061
apply (rule set_update_subset_cons, auto)
paulson@13327
  1062
done
paulson@13327
  1063
paulson@13327
  1064
(** upt **)
paulson@13327
  1065
paulson@13327
  1066
lemma upt_rec:
paulson@13327
  1067
     "j:nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)"
paulson@13327
  1068
apply (induct_tac "j", auto)
paulson@13327
  1069
apply (drule not_lt_imp_le)
paulson@13327
  1070
apply (auto simp: lt_Ord intro: le_anti_sym)
paulson@13327
  1071
done
paulson@13327
  1072
paulson@13327
  1073
lemma upt_conv_Nil [simp]: "[| j le i; j:nat |] ==> upt(i,j) = Nil"
paulson@13327
  1074
apply (subst upt_rec, auto)
paulson@13327
  1075
apply (auto simp add: le_iff)
paulson@13327
  1076
apply (drule lt_asym [THEN notE], auto)
paulson@13327
  1077
done
paulson@13327
  1078
paulson@13327
  1079
(*Only needed if upt_Suc is deleted from the simpset*)
paulson@13327
  1080
lemma upt_succ_append:
paulson@13327
  1081
     "[| i le j; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"
paulson@13327
  1082
by simp
paulson@13327
  1083
paulson@13327
  1084
lemma upt_conv_Cons:
paulson@13327
  1085
     "[| i<j; j:nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))"
paulson@13327
  1086
apply (rule trans)
paulson@13327
  1087
apply (rule upt_rec, auto)
paulson@13327
  1088
done
paulson@13327
  1089
paulson@13327
  1090
lemma upt_type [simp,TC]: "j:nat ==> upt(i,j):list(nat)"
paulson@13327
  1091
by (induct_tac "j", auto)
paulson@13327
  1092
paulson@13327
  1093
(*LOOPS as a simprule, since j<=j*)
paulson@13327
  1094
lemma upt_add_eq_append:
paulson@13327
  1095
     "[| i le j; j:nat; k:nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
paulson@13327
  1096
apply (induct_tac "k")
paulson@13327
  1097
apply (auto simp add: app_assoc app_type)
paulson@13387
  1098
apply (rule_tac j = j in le_trans, auto)
paulson@13327
  1099
done
paulson@13327
  1100
paulson@13327
  1101
lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i"
paulson@13327
  1102
apply (induct_tac "j")
paulson@13327
  1103
apply (rule_tac [2] sym)
paulson@14055
  1104
apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
paulson@13327
  1105
done
paulson@13327
  1106
paulson@13327
  1107
lemma nth_upt [rule_format,simp]:
paulson@13327
  1108
     "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k"
paulson@13387
  1109
apply (induct_tac "j", simp)
paulson@14055
  1110
apply (simp add: nth_append le_iff)
paulson@13387
  1111
apply (auto dest!: not_lt_imp_le 
paulson@14055
  1112
            simp add: nth_append less_diff_conv add_commute)
paulson@13327
  1113
done
paulson@13327
  1114
paulson@13327
  1115
lemma take_upt [rule_format,simp]:
paulson@13327
  1116
     "[| m:nat; n:nat |] ==>
paulson@14055
  1117
         \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
paulson@13327
  1118
apply (induct_tac "m")
paulson@13327
  1119
apply (simp (no_asm_simp) add: take_0)
paulson@13327
  1120
apply clarify
paulson@13327
  1121
apply (subst upt_rec, simp) 
paulson@13327
  1122
apply (rule sym)
paulson@13327
  1123
apply (subst upt_rec, simp) 
paulson@13327
  1124
apply (simp_all del: upt.simps)
paulson@13327
  1125
apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
paulson@13327
  1126
apply auto
paulson@13327
  1127
done
paulson@13327
  1128
paulson@13327
  1129
lemma map_succ_upt:
paulson@13327
  1130
     "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
paulson@13327
  1131
apply (induct_tac "n")
paulson@13327
  1132
apply (auto simp add: map_app_distrib)
paulson@13327
  1133
done
paulson@13327
  1134
paulson@13327
  1135
lemma nth_map [rule_format,simp]:
paulson@13327
  1136
     "xs:list(A) ==>
paulson@14055
  1137
      \<forall>n \<in> nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))"
paulson@13327
  1138
apply (induct_tac "xs", simp)
paulson@13327
  1139
apply (rule ballI)
paulson@13327
  1140
apply (induct_tac "n", auto)
paulson@13327
  1141
done
paulson@13327
  1142
paulson@13327
  1143
lemma nth_map_upt [rule_format]:
paulson@13327
  1144
     "[| m:nat; n:nat |] ==>
paulson@14055
  1145
      \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
paulson@13784
  1146
apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp) 
paulson@13387
  1147
apply (subst map_succ_upt [symmetric], simp_all, clarify) 
paulson@13339
  1148
apply (subgoal_tac "i < length (upt (0, x))")
paulson@13327
  1149
 prefer 2 
paulson@13327
  1150
 apply (simp add: less_diff_conv) 
paulson@13339
  1151
 apply (rule_tac j = "succ (i #+ y) " in lt_trans2)
paulson@13327
  1152
  apply simp 
paulson@13327
  1153
 apply simp 
paulson@13339
  1154
apply (subgoal_tac "i < length (upt (y, x))")
paulson@13327
  1155
 apply (simp_all add: add_commute less_diff_conv)
paulson@13327
  1156
done
paulson@13327
  1157
paulson@13327
  1158
(** sublist (a generalization of nth to sets) **)
paulson@13327
  1159
paulson@13327
  1160
constdefs
paulson@13327
  1161
  sublist :: "[i, i] => i"
paulson@13327
  1162
    "sublist(xs, A)==
paulson@13327
  1163
     map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
paulson@13327
  1164
paulson@13327
  1165
lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil"
paulson@13327
  1166
by (unfold sublist_def, auto)
paulson@13327
  1167
paulson@13327
  1168
lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
paulson@13327
  1169
by (unfold sublist_def, auto)
paulson@13327
  1170
paulson@13327
  1171
lemma sublist_shift_lemma:
paulson@13327
  1172
 "[| xs:list(B); i:nat |] ==>
paulson@13327
  1173
  map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
paulson@13327
  1174
  map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))"
paulson@13327
  1175
apply (erule list_append_induct)
paulson@13327
  1176
apply (simp (no_asm_simp))
paulson@13327
  1177
apply (auto simp add: add_commute length_app filter_append map_app_distrib)
paulson@13327
  1178
done
paulson@13327
  1179
paulson@13327
  1180
lemma sublist_type [simp,TC]:
paulson@13327
  1181
     "xs:list(B) ==> sublist(xs, A):list(B)"
paulson@13327
  1182
apply (unfold sublist_def)
paulson@13327
  1183
apply (induct_tac "xs")
paulson@13327
  1184
apply (auto simp add: filter_append map_app_distrib)
paulson@13327
  1185
done
paulson@13327
  1186
paulson@13327
  1187
lemma upt_add_eq_append2:
paulson@13327
  1188
     "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"
paulson@13327
  1189
by (simp add: upt_add_eq_append [of 0] nat_0_le)
paulson@13327
  1190
paulson@13327
  1191
lemma sublist_append:
paulson@13327
  1192
 "[| xs:list(B); ys:list(B)  |] ==>
paulson@13327
  1193
  sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})"
paulson@13327
  1194
apply (unfold sublist_def)
paulson@13387
  1195
apply (erule_tac l = ys in list_append_induct, simp)
paulson@13327
  1196
apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
paulson@13327
  1197
apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
paulson@13327
  1198
apply (simp_all add: add_commute)
paulson@13327
  1199
done
paulson@13327
  1200
paulson@13327
  1201
paulson@13327
  1202
lemma sublist_Cons:
paulson@13327
  1203
     "[| xs:list(B); x:B |] ==>
paulson@13327
  1204
      sublist(Cons(x, xs), A) = 
paulson@13327
  1205
      (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})"
paulson@13387
  1206
apply (erule_tac l = xs in list_append_induct)
paulson@13327
  1207
apply (simp (no_asm_simp) add: sublist_def)  
paulson@13327
  1208
apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) 
paulson@13327
  1209
done
paulson@13327
  1210
paulson@13327
  1211
lemma sublist_singleton [simp]:
paulson@13327
  1212
     "sublist([x], A) = (if 0 : A then [x] else [])"
paulson@14046
  1213
by (simp add: sublist_Cons)
paulson@13327
  1214
paulson@14046
  1215
lemma sublist_upt_eq_take [rule_format, simp]:
paulson@14046
  1216
    "xs:list(A) ==> ALL n:nat. sublist(xs,n) = take(n,xs)"
paulson@14046
  1217
apply (erule list.induct, simp) 
paulson@14046
  1218
apply (clarify ); 
paulson@14046
  1219
apply (erule natE) 
paulson@14046
  1220
apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
paulson@14046
  1221
done
paulson@14046
  1222
paulson@14046
  1223
lemma sublist_Int_eq:
paulson@14055
  1224
     "xs : list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"
paulson@14046
  1225
apply (erule list.induct)
paulson@14046
  1226
apply (simp_all add: sublist_Cons) 
paulson@13327
  1227
done
paulson@13327
  1228
paulson@13387
  1229
text{*Repetition of a List Element*}
paulson@13387
  1230
paulson@13387
  1231
consts   repeat :: "[i,i]=>i"
paulson@13387
  1232
primrec
paulson@13387
  1233
  "repeat(a,0) = []"
paulson@13387
  1234
paulson@13387
  1235
  "repeat(a,succ(n)) = Cons(a,repeat(a,n))"
paulson@13387
  1236
paulson@14055
  1237
lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n"
paulson@13387
  1238
by (induct_tac n, auto)
paulson@13387
  1239
paulson@14055
  1240
lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
paulson@13387
  1241
apply (induct_tac n)
paulson@13387
  1242
apply (simp_all del: app_Cons add: app_Cons [symmetric])
paulson@13387
  1243
done
paulson@13387
  1244
paulson@14055
  1245
lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)"
paulson@13387
  1246
by (induct_tac n, auto)
paulson@13387
  1247
paulson@13387
  1248
paulson@13327
  1249
ML
paulson@13327
  1250
{*
paulson@13327
  1251
val ConsE = thm "ConsE";
paulson@13327
  1252
val Cons_iff = thm "Cons_iff";
paulson@13327
  1253
val Nil_Cons_iff = thm "Nil_Cons_iff";
paulson@13327
  1254
val list_unfold = thm "list_unfold";
paulson@13327
  1255
val list_mono = thm "list_mono";
paulson@13327
  1256
val list_univ = thm "list_univ";
paulson@13327
  1257
val list_subset_univ = thm "list_subset_univ";
paulson@13327
  1258
val list_into_univ = thm "list_into_univ";
paulson@13327
  1259
val list_case_type = thm "list_case_type";
paulson@13327
  1260
val tl_type = thm "tl_type";
paulson@13327
  1261
val drop_Nil = thm "drop_Nil";
paulson@13327
  1262
val drop_succ_Cons = thm "drop_succ_Cons";
paulson@13327
  1263
val drop_type = thm "drop_type";
paulson@13327
  1264
val list_rec_type = thm "list_rec_type";
paulson@13327
  1265
val map_type = thm "map_type";
paulson@13327
  1266
val map_type2 = thm "map_type2";
paulson@13327
  1267
val length_type = thm "length_type";
paulson@13327
  1268
val lt_length_in_nat = thm "lt_length_in_nat";
paulson@13327
  1269
val app_type = thm "app_type";
paulson@13327
  1270
val rev_type = thm "rev_type";
paulson@13327
  1271
val flat_type = thm "flat_type";
paulson@13327
  1272
val set_of_list_type = thm "set_of_list_type";
paulson@13327
  1273
val set_of_list_append = thm "set_of_list_append";
paulson@13327
  1274
val list_add_type = thm "list_add_type";
paulson@13327
  1275
val map_ident = thm "map_ident";
paulson@13327
  1276
val map_compose = thm "map_compose";
paulson@13327
  1277
val map_app_distrib = thm "map_app_distrib";
paulson@13327
  1278
val map_flat = thm "map_flat";
paulson@13327
  1279
val list_rec_map = thm "list_rec_map";
paulson@13327
  1280
val list_CollectD = thm "list_CollectD";
paulson@13327
  1281
val map_list_Collect = thm "map_list_Collect";
paulson@13327
  1282
val length_map = thm "length_map";
paulson@13327
  1283
val length_app = thm "length_app";
paulson@13327
  1284
val length_rev = thm "length_rev";
paulson@13327
  1285
val length_flat = thm "length_flat";
paulson@13327
  1286
val drop_length_Cons = thm "drop_length_Cons";
paulson@13327
  1287
val drop_length = thm "drop_length";
paulson@13327
  1288
val app_right_Nil = thm "app_right_Nil";
paulson@13327
  1289
val app_assoc = thm "app_assoc";
paulson@13327
  1290
val flat_app_distrib = thm "flat_app_distrib";
paulson@13327
  1291
val rev_map_distrib = thm "rev_map_distrib";
paulson@13327
  1292
val rev_app_distrib = thm "rev_app_distrib";
paulson@13327
  1293
val rev_rev_ident = thm "rev_rev_ident";
paulson@13327
  1294
val rev_flat = thm "rev_flat";
paulson@13327
  1295
val list_add_app = thm "list_add_app";
paulson@13327
  1296
val list_add_rev = thm "list_add_rev";
paulson@13327
  1297
val list_add_flat = thm "list_add_flat";
paulson@13327
  1298
val list_append_induct = thm "list_append_induct";
paulson@13327
  1299
val min_sym = thm "min_sym";
paulson@13327
  1300
val min_type = thm "min_type";
paulson@13327
  1301
val min_0 = thm "min_0";
paulson@13327
  1302
val min_02 = thm "min_02";
paulson@13327
  1303
val lt_min_iff = thm "lt_min_iff";
paulson@13327
  1304
val min_succ_succ = thm "min_succ_succ";
paulson@13327
  1305
val filter_append = thm "filter_append";
paulson@13327
  1306
val filter_type = thm "filter_type";
paulson@13327
  1307
val length_filter = thm "length_filter";
paulson@13327
  1308
val filter_is_subset = thm "filter_is_subset";
paulson@13327
  1309
val filter_False = thm "filter_False";
paulson@13327
  1310
val filter_True = thm "filter_True";
paulson@13327
  1311
val length_is_0_iff = thm "length_is_0_iff";
paulson@13327
  1312
val length_is_0_iff2 = thm "length_is_0_iff2";
paulson@13327
  1313
val length_tl = thm "length_tl";
paulson@13327
  1314
val length_greater_0_iff = thm "length_greater_0_iff";
paulson@13327
  1315
val length_succ_iff = thm "length_succ_iff";
paulson@13327
  1316
val append_is_Nil_iff = thm "append_is_Nil_iff";
paulson@13327
  1317
val append_is_Nil_iff2 = thm "append_is_Nil_iff2";
paulson@13327
  1318
val append_left_is_self_iff = thm "append_left_is_self_iff";
paulson@13327
  1319
val append_left_is_self_iff2 = thm "append_left_is_self_iff2";
paulson@13327
  1320
val append_left_is_Nil_iff = thm "append_left_is_Nil_iff";
paulson@13327
  1321
val append_left_is_Nil_iff2 = thm "append_left_is_Nil_iff2";
paulson@13327
  1322
val append_eq_append_iff = thm "append_eq_append_iff";
paulson@13327
  1323
val append_eq_append = thm "append_eq_append";
paulson@13327
  1324
val append_eq_append_iff2 = thm "append_eq_append_iff2";
paulson@13327
  1325
val append_self_iff = thm "append_self_iff";
paulson@13327
  1326
val append_self_iff2 = thm "append_self_iff2";
paulson@13327
  1327
val append1_eq_iff = thm "append1_eq_iff";
paulson@13327
  1328
val append_right_is_self_iff = thm "append_right_is_self_iff";
paulson@13327
  1329
val append_right_is_self_iff2 = thm "append_right_is_self_iff2";
paulson@13327
  1330
val hd_append = thm "hd_append";
paulson@13327
  1331
val tl_append = thm "tl_append";
paulson@13327
  1332
val rev_is_Nil_iff = thm "rev_is_Nil_iff";
paulson@13327
  1333
val Nil_is_rev_iff = thm "Nil_is_rev_iff";
paulson@13327
  1334
val rev_is_rev_iff = thm "rev_is_rev_iff";
paulson@13327
  1335
val rev_list_elim = thm "rev_list_elim";
paulson@13327
  1336
val length_drop = thm "length_drop";
paulson@13327
  1337
val drop_all = thm "drop_all";
paulson@13327
  1338
val drop_append = thm "drop_append";
paulson@13327
  1339
val drop_drop = thm "drop_drop";
paulson@13327
  1340
val take_0 = thm "take_0";
paulson@13327
  1341
val take_succ_Cons = thm "take_succ_Cons";
paulson@13327
  1342
val take_Nil = thm "take_Nil";
paulson@13327
  1343
val take_all = thm "take_all";
paulson@13327
  1344
val take_type = thm "take_type";
paulson@13327
  1345
val take_append = thm "take_append";
paulson@13327
  1346
val take_take = thm "take_take";
paulson@14055
  1347
val take_add = thm "take_add";
paulson@14055
  1348
val take_succ = thm "take_succ";
paulson@13327
  1349
val nth_0 = thm "nth_0";
paulson@13327
  1350
val nth_Cons = thm "nth_Cons";
paulson@13327
  1351
val nth_type = thm "nth_type";
paulson@13327
  1352
val nth_append = thm "nth_append";
paulson@13327
  1353
val set_of_list_conv_nth = thm "set_of_list_conv_nth";
paulson@13327
  1354
val nth_take_lemma = thm "nth_take_lemma";
paulson@13327
  1355
val nth_equalityI = thm "nth_equalityI";
paulson@13327
  1356
val take_equalityI = thm "take_equalityI";
paulson@13327
  1357
val nth_drop = thm "nth_drop";
paulson@13327
  1358
val list_on_set_of_list = thm "list_on_set_of_list";
paulson@13327
  1359
val zip_Nil = thm "zip_Nil";
paulson@13327
  1360
val zip_Nil2 = thm "zip_Nil2";
paulson@13327
  1361
val zip_Cons_Cons = thm "zip_Cons_Cons";
paulson@13327
  1362
val zip_type = thm "zip_type";
paulson@13327
  1363
val length_zip = thm "length_zip";
paulson@13327
  1364
val zip_append1 = thm "zip_append1";
paulson@13327
  1365
val zip_append2 = thm "zip_append2";
paulson@13327
  1366
val zip_append = thm "zip_append";
paulson@13327
  1367
val zip_rev = thm "zip_rev";
paulson@13327
  1368
val nth_zip = thm "nth_zip";
paulson@13327
  1369
val set_of_list_zip = thm "set_of_list_zip";
paulson@13327
  1370
val list_update_Nil = thm "list_update_Nil";
paulson@13327
  1371
val list_update_Cons_0 = thm "list_update_Cons_0";
paulson@13327
  1372
val list_update_Cons_succ = thm "list_update_Cons_succ";
paulson@13327
  1373
val list_update_type = thm "list_update_type";
paulson@13327
  1374
val length_list_update = thm "length_list_update";
paulson@13327
  1375
val nth_list_update = thm "nth_list_update";
paulson@13327
  1376
val nth_list_update_eq = thm "nth_list_update_eq";
paulson@13327
  1377
val nth_list_update_neq = thm "nth_list_update_neq";
paulson@13327
  1378
val list_update_overwrite = thm "list_update_overwrite";
paulson@13327
  1379
val list_update_same_conv = thm "list_update_same_conv";
paulson@13327
  1380
val update_zip = thm "update_zip";
paulson@13327
  1381
val set_update_subset_cons = thm "set_update_subset_cons";
paulson@13327
  1382
val set_of_list_update_subsetI = thm "set_of_list_update_subsetI";
paulson@13327
  1383
val upt_rec = thm "upt_rec";
paulson@13327
  1384
val upt_conv_Nil = thm "upt_conv_Nil";
paulson@13327
  1385
val upt_succ_append = thm "upt_succ_append";
paulson@13327
  1386
val upt_conv_Cons = thm "upt_conv_Cons";
paulson@13327
  1387
val upt_type = thm "upt_type";
paulson@13327
  1388
val upt_add_eq_append = thm "upt_add_eq_append";
paulson@13327
  1389
val length_upt = thm "length_upt";
paulson@13327
  1390
val nth_upt = thm "nth_upt";
paulson@13327
  1391
val take_upt = thm "take_upt";
paulson@13327
  1392
val map_succ_upt = thm "map_succ_upt";
paulson@13327
  1393
val nth_map = thm "nth_map";
paulson@13327
  1394
val nth_map_upt = thm "nth_map_upt";
paulson@13327
  1395
val sublist_0 = thm "sublist_0";
paulson@13327
  1396
val sublist_Nil = thm "sublist_Nil";
paulson@13327
  1397
val sublist_shift_lemma = thm "sublist_shift_lemma";
paulson@13327
  1398
val sublist_type = thm "sublist_type";
paulson@13327
  1399
val upt_add_eq_append2 = thm "upt_add_eq_append2";
paulson@13327
  1400
val sublist_append = thm "sublist_append";
paulson@13327
  1401
val sublist_Cons = thm "sublist_Cons";
paulson@13327
  1402
val sublist_singleton = thm "sublist_singleton";
paulson@13327
  1403
val sublist_upt_eq_take = thm "sublist_upt_eq_take";
paulson@14046
  1404
val sublist_Int_eq = thm "sublist_Int_eq";
paulson@13327
  1405
paulson@13327
  1406
structure list =
paulson@13327
  1407
struct
paulson@13327
  1408
val induct = thm "list.induct"
paulson@13327
  1409
val elim   = thm "list.cases"
paulson@13327
  1410
val intrs  = thms "list.intros"
paulson@13327
  1411
end;  
paulson@13327
  1412
*}
paulson@13327
  1413
lcp@516
  1414
end