module types.

accumulate typesSig.
accumulate basiclem.
accumulate lemma.

def_definition validtype (T\  
     (forall M\ forall V\ forall Alloc\ forall X\ forall Y\ 
       (T Alloc M V and neg (Alloc X)) imp T Alloc (upd M X Y) V)
     and (forall M\ forall V\ forall Alloc\ forall Alloc'\ 
        (T Alloc M V and (forall Z\ Alloc Z imp Alloc' Z)) imp T Alloc' M V)).

type cutfold_validtype   lprf -> form -> lprf -> lprf.
cutfold_lemma validtype cutfold_validtype.

def_definition  hastype (A\M\V\T\ T A M V  and  validtype T).
type cutfold_hastype   lprf -> form -> lprf -> lprf.
cutfold_lemma hastype cutfold_hastype.

def_lemma hastype_congr 
  (Proof\ pi P1\ pi P2\ pi V\ pi M\ pi X\ pi T\ pi Alloc\
      (Proof P1 P2 V proves hastype Alloc M X T :-
         P1 proves hastype Alloc M V T, P2 proves eq X V))
  (P1\ P2\ V\ just_because).


def_lemma increase_alloc_hastype
  (Proof\ pi P\ pi A\ pi A'\ pi M\ pi V\ pi T\
    Proof P A proves hastype A' M V T :-
      P proves hastype A M V T,
      assume (forall Z\ A Z imp A' Z))
  (P\A\ just_because).

def_definition tag   (Alloc\M\V\I\ 
    readable M V and Alloc V and eq (sel M V) (const I)).

type cutfold_tag   lprf -> form -> lprf -> lprf.
cutfold_lemma tag cutfold_tag.

def_lemma tag_allocated
  (Proof\ pi M\ pi I\ pi V\ pi P\ pi Alloc\
     Proof P Alloc M I proves Alloc V :- P proves tag Alloc M V I)
  (P\Alloc\M\I\ just_because).

def_lemma tag_readable
  (Proof\ pi M\ pi I\ pi V\ pi P\ pi Alloc\
     Proof P Alloc I proves readable M V :- P proves tag Alloc M V I)
  (P\Alloc\I\ just_because).

def_lemma tag_eq
  (Proof\ pi M\ pi I\ pi V\ pi P\ pi Alloc\
     Proof P Alloc proves eq (sel M V) (const I) :- P proves tag Alloc M V I)
  (P\Alloc\ just_because).

def_lemma increase_alloc_tag
  (Proof\ pi Alloc\ pi Alloc'\ pi M\ pi V\ pi I\ pi P\
    Proof P Alloc proves tag Alloc' M V I :- 
        P proves tag Alloc M V I,
        assume (forall Z\ Alloc Z imp Alloc' Z))
  (P\Alloc\ just_because).

def_definition field (Alloc\M\V\J\T\ 
   (readable M (plus V (const J)) 
    and (Alloc (plus V (const J)) 
    and hastype Alloc M (sel M (plus V (const J))) T))).

type cutfold_field   lprf -> form -> lprf -> lprf.
cutfold_lemma field cutfold_field.

def_lemma field_allocated
  (Proof\ pi P\ pi M\ pi V\ pi J\ pi T\ pi Alloc\
     Proof P Alloc M T proves Alloc (plus V (const J)) :-
        P proves field Alloc M V J T)
  (P\Alloc\M\T\ just_because).

def_lemma field_readable
  (Proof\ pi P\ pi M\ pi V\ pi J\ pi T\ pi Alloc\
     Proof P Alloc T proves readable M (plus V (const J)) :-
        P proves field Alloc M V J T)
  (P\Alloc\T\ just_because).

def_lemma field_hastype
  (Proof\ pi P\ pi M\ pi V\ pi J\ pi T\ pi Alloc\
     Proof P proves hastype Alloc M (sel M (plus V (const J))) T :-
        P proves field Alloc M V J T)
  (P\ just_because).

def_lemma increase_alloc_field
  (Proof\ pi Alloc'\ pi M\ pi V\ pi J\ pi T\ pi Alloc\ pi P\
    Proof P Alloc proves field Alloc' M V J T :-
      P proves field Alloc M V J T,
      assume (forall Z\ Alloc Z imp Alloc' Z))
  (P\Alloc\ just_because).

def_lemma upd_inv_tag
  (Proof\ pi P\ pi Q\ pi M\ pi X\ pi Y\ pi V\ pi T\ pi Alloc\
    Proof P Q proves tag Alloc (upd M X Y) V T :- 
            P proves tag Alloc M V T, Q proves neg(Alloc X))
  (P\Q\ just_because).


def_lemma upd_inv_field
  (Proof\ pi P\ pi Q\ pi M\ pi X\ pi Y\ pi V\ pi J\ pi T\ pi Alloc\
    Proof P Q proves field Alloc (upd M X Y) V J T :- 
            P proves field Alloc M V J T, Q proves neg(Alloc X))
  (P\Q\ just_because).

def_definition is_tagged_datatype T\ N\
        validtype T  
   and  forall A\ forall M\ forall V\ 
          hastype A M V T imp 
            (exists I\ readable M V 
             and (eq (sel M V) (const I))
             and neg(greater (const 0) (const I)) 
                            and greater (const N) (const I)).

type cutfold_is_tagged_datatype   lprf -> form -> lprf -> lprf.
cutfold_lemma is_tagged_datatype cutfold_is_tagged_datatype.

def_definition dt_sel A\M\V\D\I\J\T\
         (hastype A M V D and eq (sel M V) (const I))
     imp (readable M (plus V (const J)) 
          and hastype A M (sel M (plus V (const J))) T).

type cutfold_dt_sel   lprf -> form -> lprf -> lprf.
cutfold_lemma dt_sel cutfold_dt_sel.