src/HOL/Induct/SList.thy
 author berghofe Fri, 24 Jul 1998 13:39:47 +0200 changeset 5191 8ceaa19f7717 parent 3842 b55686a7b22c child 5977 9f0c8869cf71 permissions -rw-r--r--
Renamed '\$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
```
(*  Title:      HOL/ex/SList.thy
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1993  University of Cambridge

Definition of type 'a list (strict lists) by a least fixed point

We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
so that list can serve as a "functor" for defining other recursive types
*)

SList = Sexp +

types
'a list

arities
list :: (term) term

consts

list        :: 'a item set => 'a item set
Rep_list    :: 'a list => 'a item
Abs_list    :: 'a item => 'a list
NIL         :: 'a item
CONS        :: ['a item, 'a item] => 'a item
Nil         :: 'a list
"#"         :: ['a, 'a list] => 'a list                         (infixr 65)
List_case   :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
List_rec    :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
Rep_map     :: ('b => 'a item) => ('b list => 'a item)
Abs_map     :: ('a item => 'b) => 'a item => 'b list
null        :: 'a list => bool
hd          :: 'a list => 'a
tl,ttl      :: 'a list => 'a list
set         :: ('a list => 'a set)
mem         :: ['a, 'a list] => bool                            (infixl 55)
map         :: ('a=>'b) => ('a list => 'b list)
"@"         :: ['a list, 'a list] => 'a list                    (infixr 65)
filter      :: ['a => bool, 'a list] => 'a list

(* list Enumeration *)

"[]"        :: 'a list                              ("[]")
"@list"     :: args => 'a list                      ("[(_)]")

(* Special syntax for filter *)
"@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")

translations
"[x, xs]"     == "x#[xs]"
"[x]"         == "x#[]"
"[]"          == "Nil"

"case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"

"[x:xs . P]"  == "filter (%x. P) xs"

defs
(* Defining the Concrete Constructors *)
NIL_def       "NIL == In0 (Numb 0)"
CONS_def      "CONS M N == In1 (Scons M N)"

inductive "list(A)"
intrs
NIL_I  "NIL: list(A)"
CONS_I "[| a: A;  M: list(A) |] ==> CONS a M : list(A)"

rules
(* Faking a Type Definition ... *)
Rep_list          "Rep_list(xs): list(range(Leaf))"
Rep_list_inverse  "Abs_list(Rep_list(xs)) = xs"
Abs_list_inverse  "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"

defs
(* Defining the Abstract Constructors *)
Nil_def       "Nil == Abs_list(NIL)"
Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"

List_case_def "List_case c d == Case (%x. c) (Split d)"

(* list Recursion -- the trancl is Essential; see list.ML *)

List_rec_def
"List_rec M c d == wfrec (trancl pred_sexp)
(%g. List_case c (%x y. d x y (g y))) M"

list_rec_def
"list_rec l c d ==
List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"

(* Generalized Map Functionals *)

Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"

null_def      "null(xs)            == list_rec xs True (%x xs r. False)"
hd_def        "hd(xs)              == list_rec xs arbitrary (%x xs r. x)"
tl_def        "tl(xs)              == list_rec xs arbitrary (%x xs r. xs)"
(* a total version of tl: *)
ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r. xs)"

set_def       "set xs              == list_rec xs {} (%x l r. insert x r)"

mem_def       "x mem xs            ==
list_rec xs False (%y ys r. if y=x then True else r)"
map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
filter_def    "filter P xs         ==
list_rec xs [] (%x xs r. if P(x) then x#r else r)"

list_case_def  "list_case a f xs == list_rec xs a (%x xs r. f x xs)"

end
```