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