src/HOL/Induct/SList.thy

new SList theory from Bu Wolff

(* *********************************************************************** *)
(*                                                                         *)
(* Title:      SList.thy (Extended List Theory)                            *)
(* Based on:   $Id$       *)
(* Author:     Lawrence C Paulson, Cambridge University Computer Laboratory*)
(* Author:     B. Wolff, University of Bremen                              *)
(* Purpose:    Enriched theory of lists                                    *)
(*	       mutual indirect recursive data-types                        *)
(*                                                                         *)
(* *********************************************************************** *)

(* 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.

This enables the conservative construction of mutual recursive data-types
such as

datatype 'a m = Node 'a * ('a m) list

Tidied by lcp.  Still needs removal of nat_rec.
*)

SList = NatArith + Sexp + Hilbert_Choice (*gives us "inv"*) +
(* *********************************************************************** *)
(*                                                                         *)
(* Building up data type                                                   *)
(*                                                                         *)
(* *********************************************************************** *)

consts

  list      :: "'a item set => 'a item set"

  NIL       :: "'a item"
  CONS      :: "['a item, 'a item] => 'a item"
  List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
  List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"

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"


typedef (List)
  'a list = "list(range Leaf) :: 'a item set" (list.NIL_I)

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


(* *********************************************************************** *)
(*                                                                         *)
(* Abstracting data type                                                   *)
(*                                                                         *)
(* *********************************************************************** *)

(*Declaring the abstract list constructors*)
consts
  Nil       :: "'a list"
  "#"       :: "['a, 'a list] => 'a list"           (infixr 65)
  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
  list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"


(* list Enumeration *)

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

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

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



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 a f xs == list_rec xs a (%x xs r. f x xs)"

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

  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                                             *)
(*                                                                         *)
(* *********************************************************************** *)

  
(* Generalized Map Functionals *)

consts
  Rep_map   :: "('b => 'a item) => ('b list => 'a item)"
  Abs_map   :: "('a item => 'b) => 'a item => 'b list"

defs
  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)"


(**** Function definitions ****)

constdefs

  null      :: "'a list => bool"
  "null xs  == list_rec xs True (%x xs r. False)"

  hd        :: "'a list => 'a"
  "hd xs    == list_rec xs (@x. True) (%x xs r. x)"

  tl        :: "'a list => 'a list"
  "tl xs    == list_rec xs (@xs. True) (%x xs r. xs)"

  (* a total version of tl: *)
  ttl       :: "'a list => 'a list"
  "ttl xs   == list_rec xs [] (%x xs r. xs)"

  mem       :: "['a, 'a list] => bool"                              (infixl 55)
  "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"

  list_all  :: "('a => bool) => ('a list => bool)"
  "list_all P xs == list_rec xs True(%x l r. P(x) & r)"

  map       :: "('a=>'b) => ('a list => 'b list)"
  "map f xs == list_rec xs [] (%x l r. f(x)#r)"


consts
  "@"       :: ['a list, 'a list] => 'a list                        (infixr 65)
defs
  append_def"xs@ys == list_rec xs ys (%x l r. x#r)"


constdefs
  filter    :: "['a => bool, 'a list] => 'a list"
  "filter P xs == list_rec xs []  (%x xs r. if P(x)then x#r else r)"

  foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
  "foldl f a xs == list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"

  foldr     :: "[['a,'b] => 'b, 'b, 'a list] => 'b"
  "foldr f a xs     == list_rec xs a (%x xs r. (f x r))"

  length    :: "'a list => nat"
  "length xs== list_rec xs 0 (%x xs r. Suc r)"

  drop      :: "['a list,nat] => 'a list"
  "drop t n == (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"

  copy      :: "['a, nat] => 'a list"      (* make list of n copies of x *)
  "copy t   == nat_rec [] (%m xs. t # xs)"

  flat      :: "'a list list => 'a list"
  "flat     == foldr (op @) []"

  nth       :: "[nat, 'a list] => 'a"
  "nth      == nat_rec hd (%m r xs. r(tl xs))"

  rev       :: "'a list => 'a list"
  "rev xs   == list_rec xs [] (%x xs xsa. xsa @ [x])"


(* miscellaneous definitions *)
  zip       :: "'a list * 'b list => ('a*'b) list"
  "zip      == zipWith  (%s. s)"

  zipWith   :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
  "zipWith f S == (list_rec (fst S)  (%T.[])
                            (%x xs r. %T. if null T then [] 
                                          else f(x,hd T) # r(tl T)))(snd(S))"

  unzip     :: "('a*'b) list => ('a list * 'b list)"
  "unzip    == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"


consts take      :: "['a list,nat] => 'a list"
primrec
  take_0  "take xs 0 = []"
  take_Suc "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"

consts enum      :: "[nat,nat] => nat list"
primrec
  enum_0   "enum i 0 = []"
  enum_Suc "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"


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

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


end