src/HOL/Induct/SList.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 23235 eb365b39b36d
child 23281 e26ec695c9b3
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
paulson@12169
     1
(* *********************************************************************** *)
paulson@12169
     2
(*                                                                         *)
paulson@12169
     3
(* Title:      SList.thy (Extended List Theory)                            *)
paulson@13079
     4
(* Based on:   $Id$      *)
paulson@12169
     5
(* Author:     Lawrence C Paulson, Cambridge University Computer Laboratory*)
paulson@12169
     6
(* Author:     B. Wolff, University of Bremen                              *)
paulson@12169
     7
(* Purpose:    Enriched theory of lists                                    *)
paulson@12169
     8
(*	       mutual indirect recursive data-types                        *)
paulson@12169
     9
(*                                                                         *)
paulson@12169
    10
(* *********************************************************************** *)
paulson@3120
    11
paulson@12169
    12
(* Definition of type 'a list (strict lists) by a least fixed point
paulson@3120
    13
paulson@3120
    14
We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
paulson@3120
    15
and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
paulson@12169
    16
paulson@12169
    17
so that list can serve as a "functor" for defining other recursive types.
paulson@12169
    18
paulson@12169
    19
This enables the conservative construction of mutual recursive data-types
paulson@12169
    20
such as
paulson@12169
    21
paulson@12169
    22
datatype 'a m = Node 'a * ('a m) list
paulson@12169
    23
paulson@12169
    24
Tidied by lcp.  Still needs removal of nat_rec.
paulson@3120
    25
*)
paulson@3120
    26
haftmann@23235
    27
theory SList
haftmann@23235
    28
imports Sexp
haftmann@23235
    29
begin
paulson@13079
    30
paulson@13079
    31
(*Hilbert_Choice is needed for the function "inv"*)
paulson@13079
    32
paulson@12169
    33
(* *********************************************************************** *)
paulson@12169
    34
(*                                                                         *)
paulson@12169
    35
(* Building up data type                                                   *)
paulson@12169
    36
(*                                                                         *)
paulson@12169
    37
(* *********************************************************************** *)
paulson@3120
    38
paulson@3120
    39
paulson@13079
    40
(* Defining the Concrete Constructors *)
wenzelm@19736
    41
definition
wenzelm@21404
    42
  NIL  :: "'a item" where
wenzelm@20801
    43
  "NIL = In0(Numb(0))"
paulson@3120
    44
wenzelm@21404
    45
definition
wenzelm@21404
    46
  CONS :: "['a item, 'a item] => 'a item" where
wenzelm@20801
    47
  "CONS M N = In1(Scons M N)"
paulson@3120
    48
paulson@13079
    49
consts
paulson@13079
    50
  list      :: "'a item set => 'a item set"
paulson@3120
    51
inductive "list(A)"
paulson@13079
    52
  intros
paulson@13079
    53
    NIL_I:  "NIL: list A"
paulson@13079
    54
    CONS_I: "[| a: A;  M: list A |] ==> CONS a M : list A"
paulson@3120
    55
paulson@5977
    56
paulson@5977
    57
typedef (List)
wenzelm@20801
    58
    'a list = "list(range Leaf) :: 'a item set" 
paulson@13079
    59
  by (blast intro: list.NIL_I)
paulson@5977
    60
wenzelm@21404
    61
abbreviation "Case == Datatype.Case"
wenzelm@21404
    62
abbreviation "Split == Datatype.Split"
wenzelm@20801
    63
wenzelm@19736
    64
definition
wenzelm@21404
    65
  List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" where
wenzelm@20801
    66
  "List_case c d = Case(%x. c)(Split(d))"
paulson@5977
    67
  
wenzelm@21404
    68
definition
wenzelm@21404
    69
  List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" where
berghofe@22267
    70
  "List_rec M c d = wfrec (pred_sexp^+)
wenzelm@20801
    71
                           (%g. List_case c (%x y. d x y (g y))) M"
paulson@3120
    72
paulson@5977
    73
paulson@12169
    74
(* *********************************************************************** *)
paulson@12169
    75
(*                                                                         *)
paulson@12169
    76
(* Abstracting data type                                                   *)
paulson@12169
    77
(*                                                                         *)
paulson@12169
    78
(* *********************************************************************** *)
paulson@12169
    79
paulson@12169
    80
(*Declaring the abstract list constructors*)
paulson@13079
    81
haftmann@23235
    82
(*<*)no_translations
wenzelm@20801
    83
  "[x, xs]" == "x#[xs]"
wenzelm@20801
    84
  "[x]" == "x#[]"
wenzelm@20801
    85
no_syntax
wenzelm@20801
    86
  Nil :: "'a list"  ("[]")
haftmann@23235
    87
  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "#" 65)(*>*)
wenzelm@20801
    88
wenzelm@19736
    89
definition
wenzelm@21404
    90
  Nil       :: "'a list"                               ("[]") where
wenzelm@19736
    91
   "Nil  = Abs_List(NIL)"
paulson@13079
    92
wenzelm@21404
    93
definition
wenzelm@21404
    94
  "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65) where
wenzelm@19736
    95
   "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
paulson@13079
    96
wenzelm@21404
    97
definition
paulson@13079
    98
  (* list Recursion -- the trancl is Essential; see list.ML *)
wenzelm@21404
    99
  list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" where
wenzelm@19736
   100
   "list_rec l c d =
paulson@13079
   101
      List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
paulson@13079
   102
wenzelm@21404
   103
definition
wenzelm@21404
   104
  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" where
wenzelm@19736
   105
   "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
wenzelm@14653
   106
paulson@12169
   107
(* list Enumeration *)
paulson@12169
   108
translations
paulson@12169
   109
  "[x, xs]" == "x#[xs]"
paulson@12169
   110
  "[x]"     == "x#[]"
paulson@12169
   111
wenzelm@20770
   112
  "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
paulson@12169
   113
wenzelm@20770
   114
paulson@12169
   115
(* *********************************************************************** *)
paulson@12169
   116
(*                                                                         *)
paulson@12169
   117
(* Generalized Map Functionals                                             *)
paulson@12169
   118
(*                                                                         *)
paulson@12169
   119
(* *********************************************************************** *)
paulson@12169
   120
paulson@12169
   121
  
paulson@12169
   122
(* Generalized Map Functionals *)
paulson@12169
   123
wenzelm@19736
   124
definition
wenzelm@21404
   125
  Rep_map   :: "('b => 'a item) => ('b list => 'a item)" where
wenzelm@19736
   126
   "Rep_map f xs = list_rec xs  NIL(%x l r. CONS(f x) r)"
paulson@12169
   127
wenzelm@21404
   128
definition
wenzelm@21404
   129
  Abs_map   :: "('a item => 'b) => 'a item => 'b list" where
wenzelm@19736
   130
   "Abs_map g M  = List_rec M Nil (%N L r. g(N)#r)"
paulson@12169
   131
paulson@12169
   132
paulson@12169
   133
(**** Function definitions ****)
paulson@12169
   134
wenzelm@19736
   135
definition
wenzelm@21404
   136
  null      :: "'a list => bool" where
wenzelm@19736
   137
  "null xs  = list_rec xs True (%x xs r. False)"
paulson@12169
   138
wenzelm@21404
   139
definition
wenzelm@21404
   140
  hd        :: "'a list => 'a" where
wenzelm@19736
   141
  "hd xs    = list_rec xs (@x. True) (%x xs r. x)"
paulson@12169
   142
wenzelm@21404
   143
definition
wenzelm@21404
   144
  tl        :: "'a list => 'a list" where
wenzelm@19736
   145
  "tl xs    = list_rec xs (@xs. True) (%x xs r. xs)"
paulson@12169
   146
wenzelm@21404
   147
definition
paulson@12169
   148
  (* a total version of tl: *)
wenzelm@21404
   149
  ttl       :: "'a list => 'a list" where
wenzelm@19736
   150
  "ttl xs   = list_rec xs [] (%x xs r. xs)"
paulson@12169
   151
wenzelm@21404
   152
definition
wenzelm@21404
   153
  member :: "['a, 'a list] => bool"    (infixl "mem" 55) where
wenzelm@19736
   154
  "x mem xs = list_rec xs False (%y ys r. if y=x then True else r)"
paulson@12169
   155
wenzelm@21404
   156
definition
wenzelm@21404
   157
  list_all  :: "('a => bool) => ('a list => bool)" where
wenzelm@19736
   158
  "list_all P xs = list_rec xs True(%x l r. P(x) & r)"
paulson@12169
   159
wenzelm@21404
   160
definition
wenzelm@21404
   161
  map       :: "('a=>'b) => ('a list => 'b list)" where
wenzelm@19736
   162
  "map f xs = list_rec xs [] (%x l r. f(x)#r)"
paulson@12169
   163
haftmann@23235
   164
(*<*)no_syntax
haftmann@23235
   165
  "\<^const>List.append" :: "'a list => 'a list => 'a list" (infixr "@" 65)(*>*)
wenzelm@21404
   166
definition
wenzelm@21404
   167
  append    :: "['a list, 'a list] => 'a list"   (infixr "@" 65) where
wenzelm@19736
   168
  "xs@ys = list_rec xs ys (%x l r. x#r)"
paulson@5977
   169
wenzelm@21404
   170
definition
wenzelm@21404
   171
  filter    :: "['a => bool, 'a list] => 'a list" where
wenzelm@19736
   172
  "filter P xs = list_rec xs []  (%x xs r. if P(x)then x#r else r)"
paulson@12169
   173
wenzelm@21404
   174
definition
wenzelm@21404
   175
  foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b" where
wenzelm@19736
   176
  "foldl f a xs = list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
paulson@12169
   177
wenzelm@21404
   178
definition
wenzelm@21404
   179
  foldr     :: "[['a,'b] => 'b, 'b, 'a list] => 'b" where
wenzelm@19736
   180
  "foldr f a xs     = list_rec xs a (%x xs r. (f x r))"
paulson@12169
   181
wenzelm@21404
   182
definition
wenzelm@21404
   183
  length    :: "'a list => nat" where
wenzelm@19736
   184
  "length xs = list_rec xs 0 (%x xs r. Suc r)"
paulson@12169
   185
wenzelm@21404
   186
definition
wenzelm@21404
   187
  drop      :: "['a list,nat] => 'a list" where
wenzelm@19736
   188
  "drop t n = (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
paulson@12169
   189
wenzelm@21404
   190
definition
wenzelm@21404
   191
  copy      :: "['a, nat] => 'a list"  where     (* make list of n copies of x *)
wenzelm@19736
   192
  "copy t   = nat_rec [] (%m xs. t # xs)"
paulson@12169
   193
wenzelm@21404
   194
definition
wenzelm@21404
   195
  flat      :: "'a list list => 'a list" where
wenzelm@19736
   196
  "flat     = foldr (op @) []"
paulson@12169
   197
wenzelm@21404
   198
definition
wenzelm@21404
   199
  nth       :: "[nat, 'a list] => 'a" where
wenzelm@19736
   200
  "nth      = nat_rec hd (%m r xs. r(tl xs))"
paulson@12169
   201
wenzelm@21404
   202
definition
wenzelm@21404
   203
  rev       :: "'a list => 'a list" where
wenzelm@19736
   204
  "rev xs   = list_rec xs [] (%x xs xsa. xsa @ [x])"
paulson@5977
   205
paulson@12169
   206
(* miscellaneous definitions *)
wenzelm@21404
   207
definition
wenzelm@21404
   208
  zipWith   :: "['a * 'b => 'c, 'a list * 'b list] => 'c list" where
wenzelm@19736
   209
  "zipWith f S = (list_rec (fst S)  (%T.[])
paulson@12169
   210
                            (%x xs r. %T. if null T then [] 
paulson@12169
   211
                                          else f(x,hd T) # r(tl T)))(snd(S))"
paulson@3120
   212
wenzelm@21404
   213
definition
wenzelm@21404
   214
  zip       :: "'a list * 'b list => ('a*'b) list" where
wenzelm@19736
   215
  "zip      = zipWith  (%s. s)"
wenzelm@14653
   216
wenzelm@21404
   217
definition
wenzelm@21404
   218
  unzip     :: "('a*'b) list => ('a list * 'b list)" where
wenzelm@19736
   219
  "unzip    = foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
paulson@5977
   220
paulson@5977
   221
paulson@12169
   222
consts take      :: "['a list,nat] => 'a list"
paulson@12169
   223
primrec
paulson@13079
   224
  take_0:  "take xs 0 = []"
paulson@13079
   225
  take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
paulson@3120
   226
paulson@12169
   227
consts enum      :: "[nat,nat] => nat list"
paulson@12169
   228
primrec
paulson@13079
   229
  enum_0:   "enum i 0 = []"
paulson@13079
   230
  enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"
paulson@5977
   231
paulson@5977
   232
wenzelm@20801
   233
no_translations
wenzelm@20801
   234
  "[x:xs . P]" == "filter (%x. P) xs"
wenzelm@20801
   235
paulson@12169
   236
syntax
paulson@12169
   237
  (* Special syntax for list_all and filter *)
paulson@12169
   238
  "@Alls"       :: "[idt, 'a list, bool] => bool"        ("(2Alls _:_./ _)" 10)
paulson@12169
   239
paulson@5977
   240
translations
wenzelm@20770
   241
  "[x:xs. P]" == "CONST filter(%x. P) xs"
wenzelm@20770
   242
  "Alls x:xs. P" == "CONST list_all(%x. P)xs"
paulson@5977
   243
paulson@3120
   244
paulson@13079
   245
lemma ListI: "x : list (range Leaf) ==> x : List"
paulson@13079
   246
by (simp add: List_def)
paulson@13079
   247
paulson@13079
   248
lemma ListD: "x : List ==> x : list (range Leaf)"
paulson@13079
   249
by (simp add: List_def)
paulson@13079
   250
paulson@13079
   251
lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))"
paulson@13079
   252
  by (fast intro!: list.intros [unfolded NIL_def CONS_def]
paulson@13079
   253
           elim: list.cases [unfolded NIL_def CONS_def])
paulson@13079
   254
paulson@13079
   255
(*This justifies using list in other recursive type definitions*)
paulson@13079
   256
lemma list_mono: "A<=B ==> list(A) <= list(B)"
paulson@13079
   257
apply (unfold list.defs )
paulson@13079
   258
apply (rule lfp_mono)
paulson@13079
   259
apply (assumption | rule basic_monos)+
paulson@13079
   260
done
paulson@13079
   261
paulson@13079
   262
(*Type checking -- list creates well-founded sets*)
paulson@13079
   263
lemma list_sexp: "list(sexp) <= sexp"
paulson@13079
   264
apply (unfold NIL_def CONS_def list.defs)
paulson@13079
   265
apply (rule lfp_lowerbound)
paulson@13079
   266
apply (fast intro: sexp.intros sexp_In0I sexp_In1I)
paulson@13079
   267
done
paulson@13079
   268
paulson@13079
   269
(* A <= sexp ==> list(A) <= sexp *)
paulson@13079
   270
lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp] 
paulson@13079
   271
paulson@13079
   272
paulson@13079
   273
(*Induction for the type 'a list *)
paulson@13079
   274
lemma list_induct:
paulson@13079
   275
    "[| P(Nil);    
paulson@13079
   276
        !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)"
paulson@13079
   277
apply (unfold Nil_def Cons_def) 
paulson@13079
   278
apply (rule Rep_List_inverse [THEN subst])
paulson@13079
   279
			 (*types force good instantiation*)
paulson@13079
   280
apply (rule Rep_List [unfolded List_def, THEN list.induct], simp)
paulson@13079
   281
apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast) 
paulson@13079
   282
done
paulson@13079
   283
paulson@13079
   284
paulson@13079
   285
(*** Isomorphisms ***)
paulson@13079
   286
paulson@13079
   287
lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))"
paulson@13079
   288
apply (rule inj_on_inverseI)
paulson@13079
   289
apply (erule Abs_List_inverse [unfolded List_def])
paulson@13079
   290
done
paulson@13079
   291
paulson@13079
   292
(** Distinctness of constructors **)
paulson@13079
   293
paulson@13079
   294
lemma CONS_not_NIL [iff]: "CONS M N ~= NIL"
paulson@13079
   295
by (simp add: NIL_def CONS_def)
paulson@13079
   296
paulson@13079
   297
lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
paulson@13079
   298
lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
paulson@13079
   299
lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
paulson@13079
   300
paulson@13079
   301
lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
paulson@13079
   302
apply (unfold Nil_def Cons_def)
paulson@13079
   303
apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]])
paulson@13079
   304
apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
paulson@13079
   305
done
paulson@13079
   306
paulson@13079
   307
lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
paulson@13079
   308
lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
paulson@13079
   309
lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
paulson@13079
   310
paulson@13079
   311
(** Injectiveness of CONS and Cons **)
paulson@13079
   312
paulson@13079
   313
lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)"
paulson@13079
   314
by (simp add: CONS_def)
paulson@13079
   315
paulson@13079
   316
(*For reasoning about abstract list constructors*)
paulson@13079
   317
declare Rep_List [THEN ListD, intro] ListI [intro]
paulson@13079
   318
declare list.intros [intro,simp]
paulson@13079
   319
declare Leaf_inject [dest!]
paulson@13079
   320
paulson@13079
   321
lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)"
paulson@13079
   322
apply (simp add: Cons_def)
paulson@13079
   323
apply (subst Abs_List_inject)
paulson@13079
   324
apply (auto simp add: Rep_List_inject)
paulson@13079
   325
done
paulson@13079
   326
paulson@13079
   327
lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
paulson@13079
   328
paulson@13079
   329
lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
wenzelm@18413
   330
  by (induct L == "CONS M N" set: list) auto
paulson@13079
   331
paulson@13079
   332
lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
paulson@13079
   333
apply (simp add: CONS_def In1_def)
paulson@13079
   334
apply (fast dest!: Scons_D)
paulson@13079
   335
done
paulson@13079
   336
paulson@13079
   337
paulson@13079
   338
(*Reasoning about constructors and their freeness*)
paulson@13079
   339
paulson@13079
   340
paulson@13079
   341
lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N"
paulson@13079
   342
by (erule list.induct, simp_all)
paulson@13079
   343
paulson@13079
   344
lemma not_Cons_self2: "\<forall>x. l ~= x#l"
paulson@13079
   345
by (induct_tac "l" rule: list_induct, simp_all)
paulson@13079
   346
paulson@13079
   347
paulson@13079
   348
lemma neq_Nil_conv2: "(xs ~= []) = (\<exists>y ys. xs = y#ys)"
paulson@13079
   349
by (induct_tac "xs" rule: list_induct, auto)
paulson@13079
   350
paulson@13079
   351
(** Conversion rules for List_case: case analysis operator **)
paulson@13079
   352
paulson@13079
   353
lemma List_case_NIL [simp]: "List_case c h NIL = c"
paulson@13079
   354
by (simp add: List_case_def NIL_def)
paulson@13079
   355
paulson@13079
   356
lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
paulson@13079
   357
by (simp add: List_case_def CONS_def)
paulson@13079
   358
paulson@13079
   359
paulson@13079
   360
(*** List_rec -- by wf recursion on pred_sexp ***)
paulson@13079
   361
paulson@13079
   362
(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
paulson@13079
   363
   hold if pred_sexp^+ were changed to pred_sexp. *)
paulson@13079
   364
paulson@13079
   365
lemma List_rec_unfold_lemma:
paulson@13079
   366
     "(%M. List_rec M c d) == 
berghofe@22267
   367
      wfrec (pred_sexp^+) (%g. List_case c (%x y. d x y (g y)))"
paulson@13079
   368
by (simp add: List_rec_def)
paulson@13079
   369
paulson@13079
   370
lemmas List_rec_unfold = 
paulson@13079
   371
    def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl], 
paulson@13079
   372
               standard]
paulson@13079
   373
paulson@13079
   374
paulson@13079
   375
(** pred_sexp lemmas **)
paulson@13079
   376
paulson@13079
   377
lemma pred_sexp_CONS_I1: 
paulson@13079
   378
    "[| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+"
paulson@13079
   379
by (simp add: CONS_def In1_def)
paulson@13079
   380
paulson@13079
   381
lemma pred_sexp_CONS_I2: 
paulson@13079
   382
    "[| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+"
paulson@13079
   383
by (simp add: CONS_def In1_def)
paulson@13079
   384
paulson@13079
   385
lemma pred_sexp_CONS_D: 
paulson@13079
   386
    "(CONS M1 M2, N) : pred_sexp^+ ==>  
paulson@13079
   387
     (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"
paulson@13079
   388
apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD])
paulson@13079
   389
apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2 
paulson@13079
   390
                    trans_trancl [THEN transD])
paulson@13079
   391
done
paulson@13079
   392
paulson@13079
   393
paulson@13079
   394
(** Conversion rules for List_rec **)
paulson@13079
   395
paulson@13079
   396
lemma List_rec_NIL [simp]: "List_rec NIL c h = c"
paulson@13079
   397
apply (rule List_rec_unfold [THEN trans])
paulson@13079
   398
apply (simp add: List_case_NIL)
paulson@13079
   399
done
paulson@13079
   400
paulson@13079
   401
lemma List_rec_CONS [simp]:
paulson@13079
   402
     "[| M: sexp;  N: sexp |] 
paulson@13079
   403
      ==> List_rec (CONS M N) c h = h M N (List_rec N c h)"
paulson@13079
   404
apply (rule List_rec_unfold [THEN trans])
paulson@13079
   405
apply (simp add: pred_sexp_CONS_I2)
paulson@13079
   406
done
paulson@13079
   407
paulson@13079
   408
paulson@13079
   409
(*** list_rec -- by List_rec ***)
paulson@13079
   410
paulson@13079
   411
lemmas Rep_List_in_sexp =
paulson@13079
   412
    subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp]
paulson@13079
   413
                Rep_List [THEN ListD]] 
paulson@13079
   414
paulson@13079
   415
paulson@13079
   416
lemma list_rec_Nil [simp]: "list_rec Nil c h = c"
paulson@13079
   417
by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def)
paulson@13079
   418
paulson@13079
   419
paulson@13079
   420
lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)"
paulson@13079
   421
by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def
paulson@13079
   422
              Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp)
paulson@13079
   423
paulson@13079
   424
paulson@13079
   425
(*Type checking.  Useful?*)
paulson@13079
   426
lemma List_rec_type:
paulson@13079
   427
     "[| M: list(A);      
paulson@13079
   428
         A<=sexp;         
paulson@13079
   429
         c: C(NIL);       
paulson@13079
   430
         !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y)  
paulson@13079
   431
      |] ==> List_rec M c h : C(M :: 'a item)"
paulson@13079
   432
apply (erule list.induct, simp) 
paulson@13079
   433
apply (insert list_subset_sexp) 
paulson@13079
   434
apply (subst List_rec_CONS, blast+)
paulson@13079
   435
done
paulson@13079
   436
paulson@13079
   437
paulson@13079
   438
paulson@13079
   439
(** Generalized map functionals **)
paulson@13079
   440
paulson@13079
   441
lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL"
paulson@13079
   442
by (simp add: Rep_map_def)
paulson@13079
   443
paulson@13079
   444
lemma Rep_map_Cons [simp]: 
paulson@13079
   445
    "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)"
paulson@13079
   446
by (simp add: Rep_map_def)
paulson@13079
   447
paulson@13079
   448
lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)"
paulson@13079
   449
apply (simp add: Rep_map_def)
paulson@13079
   450
apply (rule list_induct, auto)
paulson@13079
   451
done
paulson@13079
   452
paulson@13079
   453
lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil"
paulson@13079
   454
by (simp add: Abs_map_def)
paulson@13079
   455
paulson@13079
   456
lemma Abs_map_CONS [simp]: 
paulson@13079
   457
    "[| M: sexp;  N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
paulson@13079
   458
by (simp add: Abs_map_def)
paulson@13079
   459
wenzelm@19736
   460
(*Eases the use of primitive recursion.*)
paulson@13079
   461
lemma def_list_rec_NilCons:
wenzelm@19736
   462
    "[| !!xs. f(xs) = list_rec xs c h  |] 
paulson@13079
   463
     ==> f [] = c & f(x#xs) = h x xs (f xs)"
paulson@13079
   464
by simp 
paulson@13079
   465
paulson@13079
   466
paulson@13079
   467
paulson@13079
   468
lemma Abs_map_inverse:
paulson@13079
   469
     "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |]  
paulson@13079
   470
      ==> Rep_map f (Abs_map g M) = M"
paulson@13079
   471
apply (erule list.induct, simp_all)
paulson@13079
   472
apply (insert list_subset_sexp) 
paulson@13079
   473
apply (subst Abs_map_CONS, blast)
paulson@13079
   474
apply blast 
paulson@13079
   475
apply simp 
paulson@13079
   476
done
paulson@13079
   477
paulson@13079
   478
(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
paulson@13079
   479
paulson@13079
   480
(** list_case **)
paulson@13079
   481
paulson@13079
   482
(* setting up rewrite sets *)
paulson@13079
   483
paulson@13079
   484
text{*Better to have a single theorem with a conjunctive conclusion.*}
paulson@13079
   485
declare def_list_rec_NilCons [OF list_case_def, simp]
paulson@13079
   486
paulson@13079
   487
(** list_case **)
paulson@13079
   488
paulson@13079
   489
lemma expand_list_case: 
paulson@13079
   490
 "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))"
paulson@13079
   491
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   492
paulson@13079
   493
paulson@13079
   494
(**** Function definitions ****)
paulson@13079
   495
paulson@13079
   496
declare def_list_rec_NilCons [OF null_def, simp]
paulson@13079
   497
declare def_list_rec_NilCons [OF hd_def, simp]
paulson@13079
   498
declare def_list_rec_NilCons [OF tl_def, simp]
paulson@13079
   499
declare def_list_rec_NilCons [OF ttl_def, simp]
paulson@13079
   500
declare def_list_rec_NilCons [OF append_def, simp]
paulson@13079
   501
declare def_list_rec_NilCons [OF member_def, simp]
paulson@13079
   502
declare def_list_rec_NilCons [OF map_def, simp]
paulson@13079
   503
declare def_list_rec_NilCons [OF filter_def, simp]
paulson@13079
   504
declare def_list_rec_NilCons [OF list_all_def, simp]
paulson@13079
   505
paulson@13079
   506
paulson@13079
   507
(** nth **)
paulson@13079
   508
paulson@13079
   509
lemma def_nat_rec_0_eta:
wenzelm@19736
   510
    "[| !!n. f = nat_rec c h |] ==> f(0) = c"
paulson@13079
   511
by simp
paulson@13079
   512
paulson@13079
   513
lemma def_nat_rec_Suc_eta:
wenzelm@19736
   514
    "[| !!n. f = nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
paulson@13079
   515
by simp
paulson@13079
   516
paulson@13079
   517
declare def_nat_rec_0_eta [OF nth_def, simp]
paulson@13079
   518
declare def_nat_rec_Suc_eta [OF nth_def, simp]
paulson@13079
   519
paulson@13079
   520
paulson@13079
   521
(** length **)
paulson@13079
   522
paulson@13079
   523
lemma length_Nil [simp]: "length([]) = 0"
paulson@13079
   524
by (simp add: length_def)
paulson@13079
   525
paulson@13079
   526
lemma length_Cons [simp]: "length(a#xs) = Suc(length(xs))"
paulson@13079
   527
by (simp add: length_def)
paulson@13079
   528
paulson@13079
   529
paulson@13079
   530
(** @ - append **)
paulson@13079
   531
paulson@13079
   532
lemma append_assoc [simp]: "(xs@ys)@zs = xs@(ys@zs)"
paulson@13079
   533
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   534
paulson@13079
   535
lemma append_Nil2 [simp]: "xs @ [] = xs"
paulson@13079
   536
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   537
paulson@13079
   538
(** mem **)
paulson@13079
   539
paulson@13079
   540
lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)"
paulson@13079
   541
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   542
paulson@13079
   543
lemma mem_filter [simp]: "x mem [x:xs. P x ] = (x mem xs & P(x))"
paulson@13079
   544
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   545
paulson@13079
   546
(** list_all **)
paulson@13079
   547
paulson@13079
   548
lemma list_all_True [simp]: "(Alls x:xs. True) = True"
paulson@13079
   549
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   550
paulson@13079
   551
lemma list_all_conj [simp]:
paulson@13079
   552
     "list_all p (xs@ys) = ((list_all p xs) & (list_all p ys))"
paulson@13079
   553
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   554
paulson@13079
   555
lemma list_all_mem_conv: "(Alls x:xs. P(x)) = (!x. x mem xs --> P(x))"
paulson@13079
   556
apply (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   557
apply blast 
paulson@13079
   558
done
paulson@13079
   559
paulson@13079
   560
lemma nat_case_dist : "(! n. P n) = (P 0 & (! n. P (Suc n)))"
paulson@13079
   561
apply auto
paulson@13079
   562
apply (induct_tac "n", auto)
paulson@13079
   563
done
paulson@13079
   564
paulson@13079
   565
paulson@13079
   566
lemma alls_P_eq_P_nth: "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))"
paulson@13079
   567
apply (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   568
apply (rule trans)
paulson@13079
   569
apply (rule_tac [2] nat_case_dist [symmetric], simp_all)
paulson@13079
   570
done
paulson@13079
   571
paulson@13079
   572
paulson@13079
   573
lemma list_all_imp:
paulson@13079
   574
     "[| !x. P x --> Q x;  (Alls x:xs. P(x)) |] ==> (Alls x:xs. Q(x))"
paulson@13079
   575
by (simp add: list_all_mem_conv)
paulson@13079
   576
paulson@13079
   577
paulson@13079
   578
(** The functional "map" and the generalized functionals **)
paulson@13079
   579
paulson@13079
   580
lemma Abs_Rep_map: 
paulson@13079
   581
     "(!!x. f(x): sexp) ==>  
paulson@13079
   582
        Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"
paulson@13079
   583
apply (induct_tac "xs" rule: list_induct)
paulson@13079
   584
apply (simp_all add: Rep_map_type list_sexp [THEN subsetD])
paulson@13079
   585
done
paulson@13079
   586
paulson@13079
   587
paulson@13079
   588
(** Additional mapping lemmas **)
paulson@13079
   589
paulson@13079
   590
lemma map_ident [simp]: "map(%x. x)(xs) = xs"
paulson@13079
   591
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   592
paulson@13079
   593
lemma map_append [simp]: "map f (xs@ys) = map f xs  @ map f ys"
paulson@13079
   594
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   595
paulson@13079
   596
lemma map_compose: "map(f o g)(xs) = map f (map g xs)"
paulson@13079
   597
apply (simp add: o_def)
paulson@13079
   598
apply (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   599
done
paulson@13079
   600
paulson@13079
   601
paulson@13079
   602
lemma mem_map_aux1 [rule_format]:
paulson@13079
   603
     "x mem (map f q) --> (\<exists>y. y mem q & x = f y)"
paulson@13079
   604
by (induct_tac "q" rule: list_induct, simp_all, blast)
paulson@13079
   605
paulson@13079
   606
lemma mem_map_aux2 [rule_format]: 
paulson@13079
   607
     "(\<exists>y. y mem q & x = f y) --> x mem (map f q)"
paulson@13079
   608
by (induct_tac "q" rule: list_induct, auto)
paulson@13079
   609
paulson@13079
   610
lemma mem_map: "x mem (map f q) = (\<exists>y. y mem q & x = f y)"
paulson@13079
   611
apply (rule iffI)
paulson@13079
   612
apply (erule mem_map_aux1)
paulson@13079
   613
apply (erule mem_map_aux2)
paulson@13079
   614
done
paulson@13079
   615
paulson@13079
   616
lemma hd_append [rule_format]: "A ~= [] --> hd(A @ B) = hd(A)"
paulson@13079
   617
by (induct_tac "A" rule: list_induct, auto)
paulson@13079
   618
paulson@13079
   619
lemma tl_append [rule_format]: "A ~= [] --> tl(A @ B) = tl(A) @ B"
paulson@13079
   620
by (induct_tac "A" rule: list_induct, auto)
paulson@13079
   621
paulson@13079
   622
paulson@13079
   623
(** take **)
paulson@13079
   624
paulson@13079
   625
lemma take_Suc1 [simp]: "take [] (Suc x) = []"
paulson@13079
   626
by simp
paulson@13079
   627
paulson@13079
   628
lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x"
paulson@13079
   629
by simp
paulson@13079
   630
paulson@13079
   631
paulson@13079
   632
(** drop **)
paulson@13079
   633
paulson@13079
   634
lemma drop_0 [simp]: "drop xs 0 = xs"
paulson@13079
   635
by (simp add: drop_def)
paulson@13079
   636
paulson@13079
   637
lemma drop_Suc1 [simp]: "drop [] (Suc x) = []"
paulson@13079
   638
apply (simp add: drop_def)
paulson@13079
   639
apply (induct_tac "x", auto) 
paulson@13079
   640
done
paulson@13079
   641
paulson@13079
   642
lemma drop_Suc2 [simp]: "drop(a#xs)(Suc x) = drop xs x"
paulson@13079
   643
by (simp add: drop_def)
paulson@13079
   644
paulson@13079
   645
paulson@13079
   646
(** copy **)
paulson@13079
   647
paulson@13079
   648
lemma copy_0 [simp]: "copy x 0 = []"
paulson@13079
   649
by (simp add: copy_def)
paulson@13079
   650
paulson@13079
   651
lemma copy_Suc [simp]: "copy x (Suc y) = x # copy x y"
paulson@13079
   652
by (simp add: copy_def)
paulson@13079
   653
paulson@13079
   654
paulson@13079
   655
(** fold **)
paulson@13079
   656
paulson@13079
   657
lemma foldl_Nil [simp]: "foldl f a [] = a"
paulson@13079
   658
by (simp add: foldl_def)
paulson@13079
   659
paulson@13079
   660
lemma foldl_Cons [simp]: "foldl f a(x#xs) = foldl f (f a x) xs"
paulson@13079
   661
by (simp add: foldl_def)
paulson@13079
   662
paulson@13079
   663
lemma foldr_Nil [simp]: "foldr f a [] = a"
paulson@13079
   664
by (simp add: foldr_def)
paulson@13079
   665
paulson@13079
   666
lemma foldr_Cons [simp]: "foldr f z(x#xs)  = f x (foldr f z xs)"
paulson@13079
   667
by (simp add: foldr_def)
paulson@13079
   668
paulson@13079
   669
paulson@13079
   670
(** flat **)
paulson@13079
   671
paulson@13079
   672
lemma flat_Nil [simp]: "flat [] = []"
paulson@13079
   673
by (simp add: flat_def)
paulson@13079
   674
paulson@13079
   675
lemma flat_Cons [simp]: "flat (x # xs) = x @ flat xs"
paulson@13079
   676
by (simp add: flat_def)
paulson@13079
   677
paulson@13079
   678
(** rev **)
paulson@13079
   679
paulson@13079
   680
lemma rev_Nil [simp]: "rev [] = []"
paulson@13079
   681
by (simp add: rev_def)
paulson@13079
   682
paulson@13079
   683
lemma rev_Cons [simp]: "rev (x # xs) = rev xs @ [x]"
paulson@13079
   684
by (simp add: rev_def)
paulson@13079
   685
paulson@13079
   686
paulson@13079
   687
(** zip **)
paulson@13079
   688
paulson@13079
   689
lemma zipWith_Cons_Cons [simp]:
paulson@13079
   690
     "zipWith f (a#as,b#bs)   = f(a,b) # zipWith f (as,bs)"
paulson@13079
   691
by (simp add: zipWith_def)
paulson@13079
   692
paulson@13079
   693
lemma zipWith_Nil_Nil [simp]: "zipWith f ([],[])      = []"
paulson@13079
   694
by (simp add: zipWith_def)
paulson@13079
   695
paulson@13079
   696
paulson@13079
   697
lemma zipWith_Cons_Nil [simp]: "zipWith f (x,[])  = []"
paulson@13079
   698
apply (simp add: zipWith_def)
paulson@13079
   699
apply (induct_tac "x" rule: list_induct, simp_all)
paulson@13079
   700
done
paulson@13079
   701
paulson@13079
   702
paulson@13079
   703
lemma zipWith_Nil_Cons [simp]: "zipWith f ([],x) = []"
paulson@13079
   704
by (simp add: zipWith_def)
paulson@13079
   705
paulson@13079
   706
lemma unzip_Nil [simp]: "unzip [] = ([],[])"
paulson@13079
   707
by (simp add: unzip_def)
paulson@13079
   708
paulson@13079
   709
paulson@13079
   710
paulson@13079
   711
(** SOME LIST THEOREMS **)
paulson@13079
   712
paulson@13079
   713
(* SQUIGGOL LEMMAS *)
paulson@13079
   714
paulson@13079
   715
lemma map_compose_ext: "map(f o g) = ((map f) o (map g))"
paulson@13079
   716
apply (simp add: o_def)
paulson@13079
   717
apply (rule ext)
paulson@13079
   718
apply (simp add: map_compose [symmetric] o_def)
paulson@13079
   719
done
paulson@13079
   720
paulson@13079
   721
lemma map_flat: "map f (flat S) = flat(map (map f) S)"
paulson@13079
   722
by (induct_tac "S" rule: list_induct, simp_all)
paulson@13079
   723
paulson@13079
   724
lemma list_all_map_eq: "(Alls u:xs. f(u) = g(u)) --> map f xs = map g xs"
paulson@13079
   725
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   726
paulson@13079
   727
lemma filter_map_d: "filter p (map f xs) = map f (filter(p o f)(xs))"
paulson@13079
   728
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   729
paulson@13079
   730
lemma filter_compose: "filter p (filter q xs) = filter(%x. p x & q x) xs"
paulson@13079
   731
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   732
paulson@13079
   733
(* "filter(p, filter(q,xs)) = filter(q, filter(p,xs))",
paulson@13079
   734
   "filter(p, filter(p,xs)) = filter(p,xs)" BIRD's thms.*)
paulson@13079
   735
 
paulson@13079
   736
lemma filter_append [rule_format, simp]:
paulson@13079
   737
     "\<forall>B. filter p (A @ B) = (filter p A @ filter p B)"
paulson@13079
   738
by (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   739
paulson@13079
   740
paulson@13079
   741
(* inits(xs) == map(fst,splits(xs)), 
paulson@13079
   742
 
paulson@13079
   743
   splits([]) = []
paulson@13079
   744
   splits(a # xs) = <[],xs> @ map(%x. <a # fst(x),snd(x)>, splits(xs))
paulson@13079
   745
   (x @ y = z) = <x,y> mem splits(z)
paulson@13079
   746
   x mem xs & y mem ys = <x,y> mem diag(xs,ys) *)
paulson@13079
   747
paulson@13079
   748
lemma length_append: "length(xs@ys) = length(xs)+length(ys)"
paulson@13079
   749
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   750
paulson@13079
   751
lemma length_map: "length(map f xs) = length(xs)"
paulson@13079
   752
by (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   753
paulson@13079
   754
paulson@13079
   755
lemma take_Nil [simp]: "take [] n = []"
paulson@13079
   756
by (induct_tac "n", simp_all)
paulson@13079
   757
paulson@13079
   758
lemma take_take_eq [simp]: "\<forall>n. take (take xs n) n = take xs n"
paulson@13079
   759
apply (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   760
apply (rule allI)
paulson@13079
   761
apply (induct_tac "n", auto)
paulson@13079
   762
done
paulson@13079
   763
paulson@13079
   764
lemma take_take_Suc_eq1 [rule_format]:
paulson@13079
   765
     "\<forall>n. take (take xs(Suc(n+m))) n = take xs n"
paulson@13079
   766
apply (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   767
apply (rule allI)
paulson@13079
   768
apply (induct_tac "n", auto)
paulson@13079
   769
done
paulson@13079
   770
paulson@13079
   771
declare take_Suc [simp del]
paulson@13079
   772
paulson@13079
   773
lemma take_take_1: "take (take xs (n+m)) n = take xs n"
paulson@13079
   774
apply (induct_tac "m")
paulson@13079
   775
apply (simp_all add: take_take_Suc_eq1)
paulson@13079
   776
done
paulson@13079
   777
paulson@13079
   778
lemma take_take_Suc_eq2 [rule_format]:
paulson@13079
   779
     "\<forall>n. take (take xs n)(Suc(n+m)) = take xs n"
paulson@13079
   780
apply (induct_tac "xs" rule: list_induct, simp_all)
paulson@13079
   781
apply (rule allI)
paulson@13079
   782
apply (induct_tac "n", auto)
paulson@13079
   783
done
paulson@13079
   784
paulson@13079
   785
lemma take_take_2: "take(take xs n)(n+m) = take xs n"
paulson@13079
   786
apply (induct_tac "m")
paulson@13079
   787
apply (simp_all add: take_take_Suc_eq2)
paulson@13079
   788
done
paulson@13079
   789
paulson@13079
   790
(* length(take(xs,n)) = min(n, length(xs)) *)
paulson@13079
   791
(* length(drop(xs,n)) = length(xs) - n *)
paulson@13079
   792
paulson@13079
   793
lemma drop_Nil [simp]: "drop  [] n  = []"
paulson@13079
   794
by (induct_tac "n", auto)
paulson@13079
   795
paulson@13079
   796
lemma drop_drop [rule_format]: "\<forall>xs. drop (drop xs m) n = drop xs(m+n)"
paulson@13079
   797
apply (induct_tac "m", auto) 
paulson@13079
   798
apply (induct_tac "xs" rule: list_induct, auto) 
paulson@13079
   799
done
paulson@13079
   800
paulson@13079
   801
lemma take_drop [rule_format]: "\<forall>xs. (take xs n) @ (drop xs n) = xs"
paulson@13079
   802
apply (induct_tac "n", auto) 
paulson@13079
   803
apply (induct_tac "xs" rule: list_induct, auto) 
paulson@13079
   804
done
paulson@13079
   805
paulson@13079
   806
lemma copy_copy: "copy x n @ copy x m = copy x (n+m)"
paulson@13079
   807
by (induct_tac "n", auto)
paulson@13079
   808
paulson@13079
   809
lemma length_copy: "length(copy x n)  = n"
paulson@13079
   810
by (induct_tac "n", auto)
paulson@13079
   811
paulson@13079
   812
lemma length_take [rule_format, simp]:
paulson@13079
   813
     "\<forall>xs. length(take xs n) = min (length xs) n"
paulson@13079
   814
apply (induct_tac "n")
paulson@13079
   815
 apply auto
paulson@13079
   816
apply (induct_tac "xs" rule: list_induct)
paulson@13079
   817
 apply auto
paulson@13079
   818
done
paulson@13079
   819
paulson@13079
   820
lemma length_take_drop: "length(take A k) + length(drop A k) = length(A)" 
paulson@13079
   821
by (simp only: length_append [symmetric] take_drop)
paulson@13079
   822
paulson@13079
   823
lemma take_append [rule_format]: "\<forall>A. length(A) = n --> take(A@B) n = A"
paulson@13079
   824
apply (induct_tac "n")
paulson@13079
   825
apply (rule allI)
paulson@13079
   826
apply (rule_tac [2] allI)
paulson@13079
   827
apply (induct_tac "A" rule: list_induct)
paulson@13079
   828
apply (induct_tac [3] "A" rule: list_induct, simp_all)
paulson@13079
   829
done
paulson@13079
   830
paulson@13079
   831
lemma take_append2 [rule_format]:
paulson@13079
   832
     "\<forall>A. length(A) = n --> take(A@B) (n+k) = A @ take B k"
paulson@13079
   833
apply (induct_tac "n")
paulson@13079
   834
apply (rule allI)
paulson@13079
   835
apply (rule_tac [2] allI)
paulson@13079
   836
apply (induct_tac "A" rule: list_induct)
paulson@13079
   837
apply (induct_tac [3] "A" rule: list_induct, simp_all)
paulson@13079
   838
done
paulson@13079
   839
paulson@13079
   840
lemma take_map [rule_format]: "\<forall>n. take (map f A) n = map f (take A n)"
paulson@13079
   841
apply (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   842
apply (rule allI)
paulson@13079
   843
apply (induct_tac "n", simp_all)
paulson@13079
   844
done
paulson@13079
   845
paulson@13079
   846
lemma drop_append [rule_format]: "\<forall>A. length(A) = n --> drop(A@B)n = B"
paulson@13079
   847
apply (induct_tac "n")
paulson@13079
   848
apply (rule allI)
paulson@13079
   849
apply (rule_tac [2] allI)
paulson@13079
   850
apply (induct_tac "A" rule: list_induct)
paulson@13079
   851
apply (induct_tac [3] "A" rule: list_induct, simp_all)
paulson@13079
   852
done
paulson@13079
   853
paulson@13079
   854
lemma drop_append2 [rule_format]:
paulson@13079
   855
     "\<forall>A. length(A) = n --> drop(A@B)(n+k) = drop B k"
paulson@13079
   856
apply (induct_tac "n")
paulson@13079
   857
apply (rule allI)
paulson@13079
   858
apply (rule_tac [2] allI)
paulson@13079
   859
apply (induct_tac "A" rule: list_induct)
paulson@13079
   860
apply (induct_tac [3] "A" rule: list_induct, simp_all)
paulson@13079
   861
done
paulson@13079
   862
paulson@13079
   863
paulson@13079
   864
lemma drop_all [rule_format]: "\<forall>A. length(A) = n --> drop A n = []"
paulson@13079
   865
apply (induct_tac "n")
paulson@13079
   866
apply (rule allI)
paulson@13079
   867
apply (rule_tac [2] allI)
paulson@13079
   868
apply (induct_tac "A" rule: list_induct)
paulson@13079
   869
apply (induct_tac [3] "A" rule: list_induct, auto)
paulson@13079
   870
done
paulson@13079
   871
paulson@13079
   872
lemma drop_map [rule_format]: "\<forall>n. drop (map f A) n = map f (drop A n)"
paulson@13079
   873
apply (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   874
apply (rule allI)
paulson@13079
   875
apply (induct_tac "n", simp_all)
paulson@13079
   876
done
paulson@13079
   877
paulson@13079
   878
lemma take_all [rule_format]: "\<forall>A. length(A) = n --> take A n = A"
paulson@13079
   879
apply (induct_tac "n")
paulson@13079
   880
apply (rule allI)
paulson@13079
   881
apply (rule_tac [2] allI)
paulson@13079
   882
apply (induct_tac "A" rule: list_induct)
paulson@13079
   883
apply (induct_tac [3] "A" rule: list_induct, auto) 
paulson@13079
   884
done
paulson@13079
   885
paulson@13079
   886
lemma foldl_single: "foldl f a [b] = f a b"
paulson@13079
   887
by simp_all
paulson@13079
   888
paulson@13079
   889
lemma foldl_append [rule_format, simp]:
paulson@13079
   890
     "\<forall>a. foldl f a (A @ B) = foldl f (foldl f a A) B"
paulson@13079
   891
by (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   892
paulson@13079
   893
lemma foldl_map [rule_format]:
paulson@13079
   894
     "\<forall>e. foldl f e (map g S) = foldl (%x y. f x (g y)) e S"
paulson@13079
   895
by (induct_tac "S" rule: list_induct, simp_all)
paulson@13079
   896
paulson@13079
   897
lemma foldl_neutr_distr [rule_format]:
paulson@13079
   898
  assumes r_neutr: "\<forall>a. f a e = a" 
paulson@13079
   899
      and r_neutl: "\<forall>a. f e a = a"
paulson@13079
   900
      and assoc:   "\<forall>a b c. f a (f b c) = f(f a b) c"
paulson@13079
   901
  shows "\<forall>y. f y (foldl f e A) = foldl f y A"
paulson@13079
   902
apply (induct_tac "A" rule: list_induct)
paulson@13079
   903
apply (simp_all add: r_neutr r_neutl, clarify) 
paulson@13079
   904
apply (erule all_dupE) 
paulson@13079
   905
apply (rule trans) 
paulson@13079
   906
prefer 2 apply assumption
berghofe@13612
   907
apply (simp (no_asm_use) add: assoc [THEN spec, THEN spec, THEN spec, THEN sym])
berghofe@13612
   908
apply simp
paulson@13079
   909
done
paulson@13079
   910
paulson@13079
   911
lemma foldl_append_sym: 
paulson@13079
   912
"[| !a. f a e = a; !a. f e a = a;           
paulson@13079
   913
    !a b c. f a (f b c) = f(f a b) c |]    
paulson@13079
   914
  ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"
paulson@13079
   915
apply (rule trans)
paulson@13079
   916
apply (rule foldl_append)
paulson@13079
   917
apply (rule sym) 
paulson@13079
   918
apply (rule foldl_neutr_distr, auto)
paulson@13079
   919
done
paulson@13079
   920
paulson@13079
   921
lemma foldr_append [rule_format, simp]:
paulson@13079
   922
     "\<forall>a. foldr f a (A @ B) = foldr f (foldr f a B) A"
paulson@13079
   923
apply (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   924
done
paulson@13079
   925
paulson@13079
   926
paulson@13079
   927
lemma foldr_map [rule_format]: "\<forall>e. foldr f e (map g S) = foldr (f o g) e S"
paulson@13079
   928
apply (simp add: o_def)
paulson@13079
   929
apply (induct_tac "S" rule: list_induct, simp_all)
paulson@13079
   930
done
paulson@13079
   931
paulson@13079
   932
lemma foldr_Un_eq_UN: "foldr op Un {} S = (UN X: {t. t mem S}.X)"
paulson@13079
   933
by (induct_tac "S" rule: list_induct, auto)
paulson@13079
   934
paulson@13079
   935
lemma foldr_neutr_distr:
paulson@13079
   936
     "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]    
paulson@13079
   937
      ==> foldr f y S = f (foldr f e S) y"
paulson@13079
   938
by (induct_tac "S" rule: list_induct, auto)
paulson@13079
   939
paulson@13079
   940
lemma foldr_append2: 
paulson@13079
   941
    "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]
paulson@13079
   942
     ==> foldr f e (A @ B) = f (foldr f e A) (foldr f e B)"
paulson@13079
   943
apply auto
paulson@13079
   944
apply (rule foldr_neutr_distr, auto)
paulson@13079
   945
done
paulson@13079
   946
paulson@13079
   947
lemma foldr_flat: 
paulson@13079
   948
    "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] ==>  
paulson@13079
   949
      foldr f e (flat S) = (foldr f e)(map (foldr f e) S)"
paulson@13079
   950
apply (induct_tac "S" rule: list_induct)
paulson@13079
   951
apply (simp_all del: foldr_append add: foldr_append2)
paulson@13079
   952
done
paulson@13079
   953
paulson@13079
   954
paulson@13079
   955
lemma list_all_map: "(Alls x:map f xs .P(x)) = (Alls x:xs.(P o f)(x))"
paulson@13079
   956
by (induct_tac "xs" rule: list_induct, auto)
paulson@13079
   957
paulson@13079
   958
lemma list_all_and: 
paulson@13079
   959
     "(Alls x:xs. P(x)&Q(x)) = ((Alls x:xs. P(x))&(Alls x:xs. Q(x)))"
paulson@13079
   960
by (induct_tac "xs" rule: list_induct, auto)
paulson@13079
   961
paulson@13079
   962
paulson@13079
   963
lemma nth_map [rule_format]:
paulson@13079
   964
     "\<forall>i. i < length(A)  --> nth i (map f A) = f(nth i A)"
paulson@13079
   965
apply (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   966
apply (rule allI)
paulson@13079
   967
apply (induct_tac "i", auto) 
paulson@13079
   968
done
paulson@13079
   969
paulson@13079
   970
lemma nth_app_cancel_right [rule_format]:
paulson@13079
   971
     "\<forall>i. i < length(A)  --> nth i(A@B) = nth i A"
paulson@13079
   972
apply (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   973
apply (rule allI)
paulson@13079
   974
apply (induct_tac "i", simp_all)
paulson@13079
   975
done
paulson@13079
   976
paulson@13079
   977
lemma nth_app_cancel_left [rule_format]:
paulson@13079
   978
     "\<forall>n. n = length(A) --> nth(n+i)(A@B) = nth i B"
paulson@13079
   979
by (induct_tac "A" rule: list_induct, simp_all)
paulson@13079
   980
paulson@13079
   981
paulson@13079
   982
(** flat **)
paulson@13079
   983
paulson@13079
   984
lemma flat_append [simp]: "flat(xs@ys) = flat(xs) @ flat(ys)"
paulson@13079
   985
by (induct_tac "xs" rule: list_induct, auto)
paulson@13079
   986
paulson@13079
   987
lemma filter_flat: "filter p (flat S) = flat(map (filter p) S)"
paulson@13079
   988
by (induct_tac "S" rule: list_induct, auto)
paulson@13079
   989
paulson@13079
   990
paulson@13079
   991
(** rev **)
paulson@13079
   992
paulson@13079
   993
lemma rev_append [simp]: "rev(xs@ys) = rev(ys) @ rev(xs)"
paulson@13079
   994
by (induct_tac "xs" rule: list_induct, auto)
paulson@13079
   995
paulson@13079
   996
lemma rev_rev_ident [simp]: "rev(rev l) = l"
paulson@13079
   997
by (induct_tac "l" rule: list_induct, auto)
paulson@13079
   998
paulson@13079
   999
lemma rev_flat: "rev(flat ls) = flat (map rev (rev ls))"
paulson@13079
  1000
by (induct_tac "ls" rule: list_induct, auto)
paulson@13079
  1001
paulson@13079
  1002
lemma rev_map_distrib: "rev(map f l) = map f (rev l)"
paulson@13079
  1003
by (induct_tac "l" rule: list_induct, auto)
paulson@13079
  1004
paulson@13079
  1005
lemma foldl_rev: "foldl f b (rev l) = foldr (%x y. f y x) b l"
paulson@13079
  1006
by (induct_tac "l" rule: list_induct, auto)
paulson@13079
  1007
paulson@13079
  1008
lemma foldr_rev: "foldr f b (rev l) = foldl (%x y. f y x) b l"
paulson@13079
  1009
apply (rule sym)
paulson@13079
  1010
apply (rule trans)
paulson@13079
  1011
apply (rule_tac [2] foldl_rev, simp)
paulson@13079
  1012
done
paulson@13079
  1013
paulson@3120
  1014
end