-- File: bag2

-- This file treats implementation 2 of the example of bags. It follows the 
-- structure of Section 6.5.2, and is hence divided in the following parts.
-- 1.  Interface
-- 2.  Specification
-- 3.  Implementation
-- 4c. Using a weaker specification
-- 4d. Subset algebras

Path "../lol"
Path "../lolExtra"
Load "lambdaLplus"
Load "list2"
Load "prelims"

----------------------------
--                        --
--  1. I N T E R F A C E  --
--                        --
----------------------------

Def BagI := \X:*s. {| empty : X,
                      add : Nat -> X -> X,
                      card : Nat -> X -> Nat,
                      bound : X -> Nat |}

Def BagImp := Sig X:*s. BagI X

-- We introduce Sim, Bisim, and the parametricity axiom just for BagI;
-- the general scheme cannot be formalized in Yarrow (see the discussion
-- at the end of Section 6.7.6, on pages 190,191).

Def SimBagI := \Rep1,Rep2:*s. \(~):Rep1 ->Rep2->*p.
            \ops1:BagI Rep1. \ops2:BagI Rep2. 
                ops1`empty ~ ops2`empty /\
                (@x:Rep1.@y:Rep2. @m:Nat. x ~ y -> 
                                          ops1`add m x ~ ops2`add m y) /\
                (@x:Rep1.@y:Rep2. @m:Nat.  x ~ y -> 
                                          ops1`card m x = ops2`card m y) /\ 
                (@x:Rep1.@y:Rep2. x ~ y -> ops1`bound x = ops2`bound y) :
            @Rep1,Rep2:*s. (Rep1->Rep2->*p) -> BagI Rep1 -> BagI Rep2 -> *p

Def BisimBagI := \Bag:*s.\(~): Bag->Bag->*p.\ops:BagI Bag. 
                    SimBagI Bag Bag (~) ops ops : 
             @Bag:*s. (Bag->Bag->*p) -> BagI Bag -> *p

Var parSigmaBagI : @X1:*s.@X2:*s.@x1:BagI X1. @x2:BagI X2.
                       @(~) : X1->X2->*p.
                       SimBagI X1 X2 (~) x1 x2 ->
                       pack BagI X1 x1 = pack BagI X2 x2


------------------------------------
--                                --
--  2. S P E C I F I C A T I O N  --
--                                --
------------------------------------

Def NaiveSpec := \Bag:*s. \ops:BagI Bag.
                 @m,n:Nat. @b:Bag. 
                   ops`card m ops`empty = O /\
                   ops`card m (ops`add m b) = S (ops`card m b) /\
                   (Not (m=n) -> ops`card m (ops`add n b) = 
                                                ops`card m b) /\
                   ops`add m (ops`add n b) =
                                   ops`add n (ops`add m b) /\
                   (S O <= ops`card m b -> m <= ops`bound b) :
              @Bag:*s. BagI Bag -> *p

Def UserSpec := \imp:BagImp. ExK Rep:*s. Ex ops:BagI Rep.
                      imp = pack BagI Rep ops /\ NaiveSpec Rep ops

--------------------------------------
--                                  --
--  3. I M P L E M E N T A T I O N  --
--                                  --
--------------------------------------

Def Rep2 := List Nat

Def ops2 := {empty = nil Nat,
             add = insert,
             card = count,
             bound = last O} : BagI Rep2
Def imp2 := pack BagI Rep2 ops2 : BagImp

-------------------------------------------------------------------
--                                                               --
--  4c. U S I N G   A   W E A K E R   S P E C I F I C A T I O N  --
--                                                               --
-------------------------------------------------------------------

Def IsInvarBagI := \Rep:*s.\Inv:Rep->*p.\ops:BagI Rep.
                       Inv (ops`empty) /\
                       @m:Nat. @r:Rep. Inv r -> Inv (ops`add m r)

Prove IsInvar_Ordered_ops2 : IsInvarBagI Rep2 Ordered ops2

Def Spec := \Rep:*s. \Inv : Rep->*p. \ops:BagI Rep.
      @m,n:Nat. @r:Rep. Inv r ->
           ops`card m ops`empty = O /\
           ops`card m (ops`add m r) = S (ops`card m r) /\
           (Not (m=n) -> ops`card m (ops`add n r) = 
                                               ops`card m r) /\
           ops`add m (ops`add n r) =
                                  ops`add n (ops`add m r) /\
           (S O <= ops`card m r -> m <= ops`bound r) :
            @Rep:*s. (Rep->*p) -> BagI Rep -> *p


Def ImplemSpec := \Rep:*s. \ops:BagI Rep.
                  ExQ Inv : Rep->*p. Spec Rep Inv ops /\ 
                    IsInvarBagI Rep Inv ops

Prove Spec_True__NaiveSpec : @R:*s.@opsR:BagI R. Spec R (\r:R. True) opsR ->
                                                 NaiveSpec R opsR

Prove NaiveSpec__Spec_True : @Rep:*s. @ops:BagI Rep. NaiveSpec Rep ops ->
                                                    Spec Rep (\r:Rep. True) ops

Def WeakUserSpec := \bagImp : BagImp. 
                    ExK Rep:*s. Ex ops:BagI Rep. ExQ Inv : Rep->*p.
                    bagImp = pack BagI Rep ops /\ Spec Rep Inv ops /\ 
                    IsInvarBagI Rep Inv ops


Prove Spec_Ordered_ops2 : Spec Rep2 Ordered ops2

Prove ImplemSpec_ops2 : ImplemSpec Rep2 ops2

Prove Implem__WeakUserSpec : @Rep:*s. @ops:BagI Rep.
                                 ImplemSpec Rep ops -> 
                                 WeakUserSpec (pack BagI Rep ops)

Prove WeakUserSpec_imp2 : WeakUserSpec imp2


-----------------------------------------
--                                     --
--  4d. S U B S E T   A L G E B R A S  --
--                                     --
-----------------------------------------

Def IsSubsetAlg :=\R:*s. \opsR : BagI R. \Inv:R->*p. \S:*s. \opsS : BagI S.
               Ex inj:S->R.
                IsInjection inj /\
                (Inv <==> Image inj) /\
                SimBagI R S (\r:R.\s:S. r = inj s) opsR opsS  :
              @R:*s. BagI R -> (R->*p) -> @S:*s. BagI S -> *p

Var exis_SubsetAlg : @R:*s. @opsR:BagI R. @Inv:R->*p.
                     IsInvarBagI R Inv opsR ->
                     ExK S:*s. Ex opsS: BagI S. 
                     IsSubsetAlg R opsR Inv S opsS

-- (i)
prove pack_Subset : @R:*s. @opsR:BagI R. @Inv:R->*p.
                    @S:*s. @opsS: BagI S. IsSubsetAlg R opsR Inv S opsS ->
                    (=) BagImp (pack BagI R opsR) (pack BagI S opsS)

-- (ii)
Prove Spec_Sens :
                @R:*s. @opsR:BagI R. @Inv:R->*p. @S:*s. @opsS: BagI S. 
                IsSubsetAlg R opsR Inv S opsS -> Spec R Inv opsR ->
                Spec S (\s:S. True) opsS

Prove Implem__UserSpec : @Rep:*s. @ops:BagI Rep.
                             ImplemSpec Rep ops -> 
                             UserSpec (pack BagI Rep ops)

Prove UserSpec_imp2 : UserSpec imp2



Prove principle : @imp:BagImp. UserSpec imp ->
              @A:*s.@Q:A->*p.@body:@X:*s. BagI X -> A.
              (@X:*s.@ops:BagI X. Spec X (\r:X.True) ops -> Q (body X ops)) -> 
              Q (unpack imp (\X:*s.\ops:BagI X. body X ops))