module intlist.

accumulate intlistSig.
accumulate types.
accumulate lemma.

def_definition  intty    (Alloc\M\V\ neg false).
type cutfold_intty   lprf -> form -> lprf -> lprf.
cutfold_lemma intty cutfold_intty.

def_lemma  valid_intty
  (Proof\  Proof proves validtype intty)
  (just_because).



def_definition  intlist  (Alloc\M\V\
  tag Alloc M V 0 
  or tag Alloc M V 1 and field Alloc M V 1 intty and field Alloc M V 2 intlist).     

type cutfold_intlist   lprf -> form -> lprf -> lprf.
cutfold_lemma intlist cutfold_intlist.


def_lemma  valid_intlist
  (Proof\  Proof proves validtype intlist)
  (just_because).


def_lemma  itd_intlist
  (Proof\ Proof proves is_tagged_datatype intlist 2)
  (just_because).

def_lemma intlist_1_1
  (Proof\ pi A\ pi M\ pi V\ 
     Proof proves dt_sel A M V intlist 1 1 intty)
  (just_because).

def_lemma intlist_1_2
  (Proof\ pi A\ pi M\ pi V\ 
     Proof proves dt_sel A M V intlist 1 2 intlist)
  (just_because).

def_lemma intlist_alloc
  (Proof\ pi P\ pi A\ pi M\ pi V\
    Proof P proves hastype A M V intlist :-
      P proves 
       (readable M V and A V) and 
       (eq (sel M V) (const 0) or
        eq (sel M V) (const 1) and
          (readable M (plus V (const 1))
           and (A (plus V (const 1))
           and hastype A M (sel M (plus V (const 1))) intty)) and
          (readable M (plus V (const 2))
           and (A (plus V (const 2))
           and hastype A M (sel M (plus V (const 2))) intlist))))
  (P\ just_because).