special_list [EVENT_TYPE: TYPE, null_event: EVENT_TYPE]: THEORY

 % A special ssimplementation of a list which is used for the queue in TM ref.  
 
 BEGIN

  list: TYPE = [# size: nat, entry: [posnat -> EVENT_TYPE]#]

  l1,l2,l3: VAR list

  event: VAR EVENT_TYPE

  empty(l1): bool =
    l1`size = 0

  %null?: [list -> boolean] = 
  %  LAMBDA (l1: list): l1`size=0

  %null: (null?)

  null(l1): bool =
    l1`size=0

  %null_event: EVENT_TYPE

  %null1: list = (#size:=0,entry:=LAMBDA (i: posnat): EVENT1#)
  null1: list = (#size:=0,entry:=LAMBDA (i: posnat): null_event#)

  % null iff empty (WHY do we need both null and empty?)
  null_is_empty: LEMMA
    FORALL (l1: list): null(l1) IFF empty(l1) 

  eql(l1,l2): bool =
    l1`size  = l2`size AND
    FORALL (i: posnat): i<= l1`size IMPLIES l1`entry(i) = l2`entry(i) 

  eql_sym: AXIOM
    FORALL(l1,l2: list):
      eql(l1,l2) IMPLIES eql(l2,l1) 

  eql_trans: AXIOM
    FORALL(l1,l2,l3: list):
      (eql(l1,l2) AND
       eql(l2,l3))   IMPLIES
         eql(l1,l3) 

  % this shouldn't real be;
  % better change empty()/null() to talk about entry as well
  empty_eql_null1: AXIOM
    FORALL (l1: list): empty(l1) IMPLIES
                         eql(l1,null1)

  add(event, l1): list =
    l1 WITH [size  := l1`size + 1,
             entry := l1`entry WITH [(l1`size+1) := event]]

  add_size: LEMMA
    FORALL l1,event:
      add(event,l1)`size = l1`size+1   

  add_maintains_eql: AXIOM
    FORALL (l1,l2: list, event): 
      eql(l1,l2) IMPLIES
        eql(add(event,l1),add(event,l2)) 

  cons(event,l1): list =
    l1 WITH [size  := l1`size + 1,
             entry := LAMBDA (i: posnat): 
                        IF i = 1 
                          THEN event
                          ELSE l1`entry(i-1)
                        ENDIF]
 
  car: [list -> EVENT_TYPE]

  % car of cons of event to list is the same event
  car_cons: AXIOM
    car(cons(event,l1)) = event

  % if list is not empty car is the first event
  car_of_list: AXIOM
    NOT empty(l1) IMPLIES 
      car(l1) = l1`entry(1)

  % cons of car of list equals list
  list_car_cons: AXIOM
    FORALL (e1: EVENT_TYPE, l1: list):
      eql(cons(car(l1),l1),l1);


  cdr(l1): list =
    IF empty(l1)
      THEN l1
      ELSE l1 WITH [size  := l1`size - 1,
                    entry := LAMBDA (i: posnat): 
                               l1`entry(i+1)]
    ENDIF

  % appends l2 at the end of l1
  append(l1,l2): RECURSIVE list =
    IF empty(l1)
      THEN l2
      ELSE cons(car(l1),append(cdr(l1),l2))
    ENDIF 
    MEASURE l1`size

  % projecting the list on the elements that satsfy the condition
  projection(condition: [EVENT_TYPE -> bool], l1): RECURSIVE list =
    IF empty(l1)
      THEN l1
      ELSE IF condition(car(l1))
             THEN cons(car(l1),projection(condition,cdr(l1)))
             ELSE projection(condition,cdr(l1))
           ENDIF
    ENDIF 
    MEASURE l1`size 

  % exchanges i with i + 1
  exchange(l1: list,i: posnat): RECURSIVE list =
    IF empty(cdr(l1))
      THEN l1
      ELSE IF i = 1
             THEN cons(car(cdr(l1)),cons(car(l1),cdr(cdr(l1))))
             ELSE cons(car(l1),exchange(cdr(l1),i-1))
           ENDIF
    ENDIF
    MEASURE i

  % reverse the order of l1
  reverse(l1): RECURSIVE list =
    IF empty(l1)
      THEN l1
      ELSE add(car(l1),reverse(cdr(l1)))
    ENDIF
    MEASURE l1`size

  % true if exists at least one event that satisfies p
  some(p: PRED[EVENT_TYPE],l1): RECURSIVE bool =
    IF empty(l1)
      THEN FALSE
      ELSE p(car(l1)) OR some(p,cdr(l1))
    ENDIF
    MEASURE l1`size

  exist(p: PRED[EVENT_TYPE],l1): bool =
    EXISTS (i: posnat):
      p(l1`entry(i))
    


  some_imp_exsits: AXIOM
    FORALL l1,(p: PRED[EVENT_TYPE]):
      some(p,l1) IMPLIES 
        EXISTS (i: posnat): i <= l1`size AND p(l1`entry(i))

%%% need to prove the following
  some_imp_pos_proj: AXIOM
    FORALL l1,(p: PRED[EVENT_TYPE]):
      some(p,l1) IFF
        projection(p,l1)`size > 0
        


  % true iff all events satisfy p
  every(p: PRED[EVENT_TYPE],l1): RECURSIVE bool =
    IF empty(l1)
      THEN TRUE
      ELSE p(car(l1)) AND every(p,cdr(l1))
    ENDIF
    MEASURE l1`size

  % get the last event that satisfies p
  get_last_p: [[PRED[EVENT_TYPE], list] -> EVENT_TYPE] 

End special_list