--
-- We prove several lemmas on queues.
--

mod* EQTRIV {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm}
}

mod! QUEUE (D :: EQTRIV) {
  [Queue]
-- constructors
  op empty :            -> Queue
  op __   : Elt.D Queue -> Queue
-- operators
  op put : Queue Elt.D -> Queue
  op get : Queue -> Queue
  op top : Queue -> Elt.D
  op empty? : Queue -> Bool
  op _\in_ : Elt.D Queue -> Bool
-- CafeOBJ variables
  var Q : Queue
  vars X Y : Elt.D
-- equations
  eq put(empty,X) = X empty .
  eq put((Y Q),X) = Y put(Q,X) .
  eq get(empty) = empty .
  eq get((X Q)) = Q .
  eq top((X Q)) = X .
  eq empty?(empty) = true .
  eq empty?((X Q)) = false .
  eq X \in empty = false .
  eq X \in (X Q) = true .
  ceq X \in (Y Q) = X \in Q if not(X = Y) .
}

--
-- 1. ceq (top(put(Q,Y)) = X) = true if not empty?(Q) and top(Q) = X .
--
-- 2. eq empty?(put(Q,X)) = false .
--
-- 3. ceq X \in Q = false if empty?(Q) .
--
-- 4. eq X \in put(Q,X) = true .
--
-- 5. ceq X \in put(Q,Y) = true if X \in Q .
--

mod LEMMA {
  pr(QUEUE)
-- arbitrary objects
  op q : -> Queue
  ops x y : -> Elt.D
-- declare lemma candidates for Queue
  op lemma1 : Queue Elt.D Elt.D -> Bool
  op lemma2 : Queue Elt.D -> Bool
  op lemma3 : Queue Elt.D -> Bool
  op lemma4 : Queue Elt.D -> Bool
  op lemma5 : Queue Elt.D Elt.D -> Bool
-- CafeOBJ variables
  var Q : Queue
  vars X Y : Elt.D
-- define lemma candidates for Queue
  eq lemma1(Q,X,Y) = (not empty?(Q) and top(Q) = X implies top(put(Q,Y)) = X) .
  eq lemma2(Q,X)   = (not empty?(put(Q,X))) .
  eq lemma3(Q,X)   = (empty?(Q) implies not X \in Q) .
  eq lemma4(Q,X)   = (X \in put(Q,X)) . 
  eq lemma5(Q,X,Y) = (X \in Q implies X \in put(Q,Y)) .
}

-- Proof of lemma1 (by case analysis only)
open LEMMA
-- arbitrary objects
-- assumptions
  eq q = empty .
-- check if lemmae predicate is true .
  red lemma1(q,x,y) .  
close
--
open LEMMA
-- arbitrary objects
  op z : -> Elt.D .
  op qq : -> Queue .
-- assumptions
  eq q = z qq .
-- check if lemmae predicate is true .
  red lemma1(q,x,y) .  
close
-- Q.E.D. of lemma1

-- Proof of lemma2 (by case analysis only)
open LEMMA
-- arbitrary objects
-- assumptions
  eq q = empty .
-- check if lemmae predicate is true .
  red lemma2(q,x) .  
close
--
open LEMMA
-- arbitrary objects
  op z : -> Elt.D .
  op qq : -> Queue .
-- assumptions
  eq q = z qq .
-- check if lemmae predicate is true .
  red lemma2(q,x) .  
close
-- Q.E.D. of lemma2

-- Proof of lemma3 (by case analysis only)
open LEMMA
-- arbitrary objects
-- assumptions
  eq q = empty .
-- check if lemmae predicate is true .
  red lemma3(q,x) .  
close
--
open LEMMA
-- arbitrary objects
  op z : -> Elt.D .
  op qq : -> Queue .
-- assumptions
  eq q = z qq .
-- check if lemmae predicate is true .
  red lemma3(q,x) .  
close
-- Q.E.D. of lemma3

-- Proof of lemma4 (by induction + case analysis)
open LEMMA
-- arbitrary objects
-- assumptions
  eq q = empty .
-- check if lemmae predicate is true .
  red lemma4(q,x) .  
close
--
open LEMMA
-- arbitrary objects
  op z : -> Elt.D .
  op qq : -> Queue .
-- assumptions
  eq q = z qq .
  eq z = x .
-- check if lemmae predicate is true .
  red lemma4(q,x) .  
close
--
open LEMMA
-- arbitrary objects
  op z : -> Elt.D .
  op qq : -> Queue .
-- assumptions
  eq q = z qq .
  eq (z = x) = false .
-- check if lemmae predicate is true .
  red lemma4(qq,x) implies lemma4(q,x) .  
close
-- Q.E.D. of lemma4

-- Proof of lemma5 (by induction + case analysis)
open LEMMA
-- arbitrary objects
-- assumptions
  eq q = empty .
-- check if lemmae predicate is true .
  red lemma5(q,x,y) .  
close
--
open LEMMA
-- arbitrary objects
  op z : -> Elt.D .
  op qq : -> Queue .
-- assumptions
  eq q = z qq .
  eq z = x .
-- check if lemmae predicate is true .
  red lemma5(q,x,y) .  
close
--
open LEMMA
-- arbitrary objects
  op z : -> Elt.D .
  op qq : -> Queue .
-- assumptions
  eq q = z qq .
  eq (z = x) = false .
-- check if lemmae predicate is true .
  red lemma5(qq,x,y) implies lemma5(q,x,y) .  
close
-- Q.E.D. of lemma5