module INT-MULTISET {

  imports {
    using(INT) -- (le module INT importe le module NAT)
  }
  
  signature {
  
    [ IntMultiset ]   ** multi-ensembles d'entiers
 
        op occur : Int IntMultiset -> Nat                  ** nombre d'occurrences d'un entier dans un multi-ensemble d'entiers
        op _in_  : Int IntMultiset -> Bool                 ** appartenance
	op _union_ : IntMultiset IntMultiset -> IntMultiset  ** union
	op _diffe_ : IntMultiset IntMultiset -> IntMultiset  ** différence  
  }
  axioms {

        vars m m1 m2 : IntMultiset                
	var x : Int
	
        eq x in m = occur(x,m) > 0 .
        eq occur(x,m1 union m2) = occur(x,m1) + occur(x,m2) .
	eq occur(x,m1 diffe m2) = if occur(x,m1) > occur(x,m2) then sd(occur(x,m1),occur(x,m2)) else 0 fi . 	
  }
}



module INT-ARRAY {

  imports {
    using(INT)
  }
  
  signature {  
  
    [ IntArray ]    ** tableaux d'entiers  
    
        op new-array : Int -> IntArray              ** crée un tableau dont le nombre d'éléments est donné
        op _[_]      : IntArray Int -> Int          ** élément à l'indice donné (on chosit Int pour sorte des indices)
        op modif     : IntArray Int Int -> IntArray ** modifie un élément de tableau 
        op size      : IntArray -> Int              ** taille d'un tableau
    }
    axioms {

        var  x     : Int        
	vars i j n : Int
        var  t     : IntArray
	 
        eq modif(t,i,x)[j] = if i == j then x else t[j] fi .
	
        eq size(new-array(n)) = n .
        eq size(modif(t,i,x)) = size(t) .
   }
}


module INT-MS-USING-INT-ARRAY {

  imports {
    using(INT-MULTISET)
    using(INT-ARRAY)
  }
   
   signature {
   	[ IntMS ] ** pour représenter les multi-ensembles à au plus n éléments où n est la taille des tableaux
                  ** on suppose les tableaux indicés à partir de 0 (comme en C)
		  
   	op (<_;_>) : IntArray Int -> IntMS	 
 	
        op occur-t   : Int IntMS -> Nat
        op _in-t_    : Int IntMS -> Bool  
        op _union-t_ : IntMS IntMS -> IntMS
	op _diffe-t_ : IntMS IntMS -> IntMS
	
	** fonctions auxiliaires
	op occur-aux : Int IntArray Int -> Nat  
	op in-aux    : Int IntArray Int -> Bool        
	op union-aux : Int IntArray Int IntArray -> IntArray  ** concaténation de 2 tableaux
	op diffe-aux : Int IntArray Int -> IntArray   
	op decal     : IntArray Int -> IntArray   ** décalage d'une position vers la gauche            
   } 

   axioms {
   
        vars  x y         : Int        
	vars  i j n n1 n2 : Int
        vars  t t1 t2     : IntArray
	
	    
       eq  occur-t(x, < t ; n > ) = occur-aux(x,t,n) .
       
       eq  occur-aux(x,t,0) = 0 .
       ceq occur-aux(x,t,i) = s(occur-aux(x, t, i - 1))  if t[i - 1] == x .
       ceq occur-aux(x,t,i) = occur-aux(x, t, i - 1)     if not (t[i - 1] == x) .
                    
       eq  x in-t < t ; n >  = in-aux(x,t,n) .
              
       eq in-aux(x,t,0) = false .
       eq in-aux(x,t,i) = (t[i - 1] == x) or in-aux(x,t,i - 1) .
       
       ceq < t1 ; n1 > union-t < t2 ; n2 > = < union-aux(n1,t1,n2,t2) ; n1 + n2 > if size(t1) == size(t2) and (n1 + n2 <= size(t1)) .
       
       eq union-aux(n1,t1,n2,t2)[i] = if i < n1 then t1[i] else t2[i - n1] fi .

       eq  < t1 ; n1 > diffe-t < t2 ; 0 > = < t1 ; n1 > .  
       ceq < t1 ; n1 > diffe-t < t2 ; n > = < t1 ; n1 > diffe-t < t2 ; n - 1 >                         if not ((t2[n - 1]) in-t < t1 ; n1 >) . 
       ceq < t1 ; n1 > diffe-t < t2 ; n > = < diffe-aux(t2[n - 1],t1,n1) ; n1 - 1 > diffe-t < t2 ; n - 1 > if (t2[n - 1]) in-t < t1 ; n1 > . 
      
       ceq decal(t,i)[j] = t[j + 1] if j >= i .
       ceq decal(t,i)[j] = t[j]     if j <  i .
       
       ceq diffe-aux(x,t,i) = decal(t, i - 1)      if t[i - 1] == x .
       ceq diffe-aux(x,t,i) = diffe-aux(x,t,i - 1) if not (t[i - 1] == x) .
       
   }
}
 
 open INT-MS-USING-INT-ARRAY
 
 op M1 : -> IntMultiset .
 op M2 : -> IntMultiset .
 
 var x : Int . 
 
 eq occur(3, M1) = 2 .
 eq occur(2, M1) = 1 .
 eq occur(1, M1) = 1 .
 ceq occur(x, M1) = 0 if (not ((x == 1) or (x == 2) or (x == 3))) .
 
 -- M1 = { 3, 3, 2, 1 }
 
 eq occur(3, M2) = 1 . 1ère année
 eq occur(2, M2) = 2 .
 eq occur(1, M2) = 1 .
 ceq occur(x, M1) = 0 if (not ((x == 1) or (x == 2) or (x == 3))) .
 
 -- M2 = { 3, 2, 2, 1 }
 
 red occur(3,M1 union M2) . -- donne 3 !
 red occur(3,M1 diffe M2) . -- donne 1 !
 
 op M1-t : -> IntMS .
 op M2-t : -> IntMS .
 
 eq M1-t = < (modif(modif(modif(modif(new-array(10),0,3),1,3),2,2),3,1)) ; 4 >  .   
 eq M2-t = < (modif(modif(modif(modif(new-array(10),0,3),1,2),2,2),3,1)) ; 4 >  .   
 
 -- M1-t et M2-t sont les représentations des multi-ensembles M1 et M2
 -- sous la forme d'un tableau à 10 éléments 
 
 red occur-t(3,(M1-t union-t M2-t)) . -- donne 3 !
 red occur-t(3,(M1-t diffe-t M2-t)) . -- donne 1 !
 
 
 -- Pour vérifier que l'implantation des multi-ensembles par des tableaux est correcte.
 
 -- Il faudrait démontrer les théorèmes obtenus 
 -- en remplacant les opérations occur, in, union et diffe par leurs "équivalents" 
 -- avec les tableaux càd occur-t, in-t, union-t et diffe-t
 -- dans les axiomes du module INT-MULTISET càd :
 
 
 --   x in-t m == occur-t(x,m) > 0 .
 --   occur-t(x,m1 union-t m2) == occur-t(x,m1) + occur-t(x,m2) 
 --   occur-t(x,m1 diffe-t m2) == if occur-t(x,m1) > occur-t(x,m2) then sd(occur-t(x,m1),occur-t(x,m2)) else 0 fi . 	
  
 
 close