src/HOL/Induct/LList.thy
author paulson
Wed, 07 May 1997 12:50:26 +0200
changeset 3120 c58423c20740
child 3842 b55686a7b22c
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/LList.thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
Definition of type 'a llist by a greatest fixed point
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
Shares NIL, CONS, List_case with List.thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
Still needs filter and flatten functions -- hard because they need
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
bounds on the amount of lookahead required.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
Could try (but would it work for the gfp analogue of term?)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
  LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
A nice but complex example would be [ML for the Working Programmer, page 176]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
  from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
Previous definition of llistD_Fun was explicit:
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
  llistD_Fun_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
   "llistD_Fun(r) ==    
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
       {(LNil,LNil)}  Un        
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
*)
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
LList = Gfp + SList +
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
types
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
  'a llist
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
arities
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
   llist :: (term)term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
consts
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
  list_Fun   :: ['a item set, 'a item set] => 'a item set
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
  LListD_Fun :: 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
      "[('a item * 'a item)set, ('a item * 'a item)set] => 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
      ('a item * 'a item)set"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
  llist      :: 'a item set => 'a item set
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
  LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
  Rep_llist  :: 'a llist => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
  Abs_llist  :: 'a item => 'a llist
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
  LNil       :: 'a llist
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
  LCons      :: ['a, 'a llist] => 'a llist
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
  
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
  LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
  LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
  llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
  lmap       :: ('a=>'b) => ('a llist => 'b llist)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    58
  iterates   :: ['a => 'a, 'a] => 'a llist
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
  Lconst     :: 'a item => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
  Lappend    :: ['a item, 'a item] => 'a item
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
  lappend    :: ['a llist, 'a llist] => 'a llist
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    64
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    65
coinductive "llist(A)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
  intrs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
    NIL_I  "NIL: llist(A)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    68
    CONS_I "[| a: A;  M: llist(A) |] ==> CONS a M : llist(A)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    70
coinductive "LListD(r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    71
  intrs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    72
    NIL_I  "(NIL, NIL) : LListD(r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    73
    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    74
            |] ==> (CONS a M, CONS b N) : LListD(r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    75
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    76
translations
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    77
  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    79
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    80
defs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    81
  (*Now used exclusively for abbreviating the coinduction rule*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    82
  list_Fun_def   "list_Fun A X ==   
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    83
                  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    84
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    85
  LListD_Fun_def "LListD_Fun r X ==   
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    86
                  {z. z = (NIL, NIL) |   
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    87
                      (? M N a b. z = (CONS a M, CONS b N) &   
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    88
                                  (a, b) : r & (M, N) : X)}"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    89
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    90
  (*defining the abstract constructors*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    91
  LNil_def      "LNil == Abs_llist(NIL)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    92
  LCons_def     "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    93
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    94
  llist_case_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    95
   "llist_case c d l == 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    96
       List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    97
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    98
  LList_corec_fun_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    99
    "LList_corec_fun k f == 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   100
     nat_rec (%x. {})                         
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   101
             (%j r x. case f x of Inl u    => NIL
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   102
                                | Inr(z,w) => CONS z (r w)) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   103
             k"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   104
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   105
  LList_corec_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   106
    "LList_corec a f == UN k. LList_corec_fun k f a"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   107
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   108
  llist_corec_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   109
   "llist_corec a f == 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   110
       Abs_llist(LList_corec a 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   111
                 (%z.case f z of Inl x    => Inl(x)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   112
                               | Inr(v,w) => Inr(Leaf(v), w)))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   113
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   114
  llistD_Fun_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   115
   "llistD_Fun(r) ==    
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   116
        prod_fun Abs_llist Abs_llist ``         
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   117
                LListD_Fun (diag(range Leaf))   
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   118
                            (prod_fun Rep_llist Rep_llist `` r)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   119
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   120
  Lconst_def    "Lconst(M) == lfp(%N. CONS M N)"     
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   121
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   122
  Lmap_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   123
   "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   124
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   125
  lmap_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   126
   "lmap f l == llist_corec l (%z. case z of LNil => (Inl ()) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   127
                                           | LCons y z => Inr(f(y), z))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   128
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   129
  iterates_def  "iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   130
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   131
(*Append generates its result by applying f, where
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   132
    f((NIL,NIL))          = Inl(())
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   133
    f((NIL, CONS N1 N2))  = Inr((N1, (NIL,N2))
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   134
    f((CONS M1 M2, N))    = Inr((M1, (M2,N))
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   135
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   136
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   137
  Lappend_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   138
   "Lappend M N == LList_corec (M,N)                                         
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   139
     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   140
                      (%M1 M2 N. Inr((M1, (M2,N))))))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   141
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   142
  lappend_def
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   143
   "lappend l n == llist_corec (l,n)                                         
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   144
   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   145
                     (%l1 l2 n. Inr((l1, (l2,n))))))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   146
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   147
rules
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   148
    (*faking a type definition...*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   149
  Rep_llist         "Rep_llist(xs): llist(range(Leaf))"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   150
  Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   151
  Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   152
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   153
end