src/HOL/ex/SList.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1815 cd3ffa5f1e31
child 1908 55d8e38262a8
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/ex/SList.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     6
Definition of type 'a list (strict lists) by a least fixed point
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     7
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     9
and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    10
so that list can serve as a "functor" for defining other recursive types
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    11
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    12
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    13
SList = Sexp +
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    14
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    15
types
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    16
  'a list
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    17
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    18
arities
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    19
  list :: (term) term
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
consts
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    23
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    24
  list      :: 'a item set => 'a item set
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    25
  Rep_list  :: 'a list => 'a item
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    26
  Abs_list  :: 'a item => 'a list
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    27
  NIL       :: 'a item
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    28
  CONS      :: ['a item, 'a item] => 'a item
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    29
  Nil       :: 'a list
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    30
  "#"       :: ['a, 'a list] => 'a list                         (infixr 65)
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    31
  List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    32
  List_rec  :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    33
  list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    34
  list_rec  :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    35
  Rep_map   :: ('b => 'a item) => ('b list => 'a item)
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    36
  Abs_map   :: ('a item => 'b) => 'a item => 'b list
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    37
  null      :: 'a list => bool
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    38
  hd        :: 'a list => 'a
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    39
  tl,ttl    :: 'a list => 'a list
1815
cd3ffa5f1e31 Addition of setOfList
paulson
parents: 1808
diff changeset
    40
  setOfList :: ('a list => 'a set)
cd3ffa5f1e31 Addition of setOfList
paulson
parents: 1808
diff changeset
    41
  mem       :: ['a, 'a list] => bool                            (infixl 55)
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    42
  map       :: ('a=>'b) => ('a list => 'b list)
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    43
  "@"       :: ['a list, 'a list] => 'a list                    (infixr 65)
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    44
  filter    :: ['a => bool, 'a list] => 'a list
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    45
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    46
  (* list Enumeration *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    47
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    48
  "[]"      :: 'a list                            ("[]")
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1266
diff changeset
    49
  "@list"   :: args => 'a list                    ("[(_)]")
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    50
1808
785a7672962e Removed quantification over lists
paulson
parents: 1476
diff changeset
    51
  (* Special syntax for filter *)
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    52
  "@filter"     :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    53
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    54
translations
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    55
  "[x, xs]"     == "x#[xs]"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    56
  "[x]"         == "x#[]"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    57
  "[]"          == "Nil"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    58
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    59
  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    60
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    61
  "[x:xs . P]"  == "filter (%x.P) xs"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    62
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    63
defs
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    64
  (* Defining the Concrete Constructors *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    65
  NIL_def       "NIL == In0(Numb(0))"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    66
  CONS_def      "CONS M N == In1(M $ N)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    67
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    68
inductive "list(A)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    69
  intrs
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    70
    NIL_I  "NIL: list(A)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    71
    CONS_I "[| a: A;  M: list(A) |] ==> CONS a M : list(A)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    72
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    73
rules
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    74
  (* Faking a Type Definition ... *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    75
  Rep_list          "Rep_list(xs): list(range(Leaf))"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    76
  Rep_list_inverse  "Abs_list(Rep_list(xs)) = xs"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    77
  Abs_list_inverse  "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    78
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    79
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    80
defs
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    81
  (* Defining the Abstract Constructors *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    82
  Nil_def       "Nil == Abs_list(NIL)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    83
  Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    84
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    85
  List_case_def "List_case c d == Case (%x.c) (Split d)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    86
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    87
  (* list Recursion -- the trancl is Essential; see list.ML *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    88
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    89
  List_rec_def
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    90
   "List_rec M c d == wfrec (trancl pred_sexp)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    91
                            (%g. List_case c (%x y. d x y (g y))) M"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    92
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    93
  list_rec_def
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    94
   "list_rec l c d == 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    95
   List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    96
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    97
  (* Generalized Map Functionals *)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    98
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    99
  Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   100
  Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   101
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   102
  null_def      "null(xs)            == list_rec xs True (%x xs r.False)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   103
  hd_def        "hd(xs)              == list_rec xs (@x.True) (%x xs r.x)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   104
  tl_def        "tl(xs)              == list_rec xs (@xs.True) (%x xs r.xs)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   105
  (* a total version of tl: *)
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
   106
  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   107
1815
cd3ffa5f1e31 Addition of setOfList
paulson
parents: 1808
diff changeset
   108
  setOfList_def "setOfList xs == list_rec xs {} (%x l r. insert x r)"
cd3ffa5f1e31 Addition of setOfList
paulson
parents: 1808
diff changeset
   109
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
   110
  mem_def       "x mem xs            == 
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
   111
                   list_rec xs False (%y ys r. if y=x then True else r)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   112
  map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
   113
  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
   114
  filter_def    "filter P xs         == 
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
   115
                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   116
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1151
diff changeset
   117
  list_case_def  "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   118
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
   119
end