CKmultiple.pvs

CKmultiple: THEORY
BEGIN
  IMPORTING AssetMapping

  AssetIfdef: TYPE = [AssetName,bool]

  AssetNames: TYPE = finite_sets[AssetName].finite_set

  ans: VAR AssetNames
  n,an: VAR AssetName
  a,b,a1,a2: VAR Asset
  tag: VAR bool
  am,amt,am2,amt2,pairs: VAR AM
  t: VAR AssetIfdef
  assets: VAR finite_sets[Asset].finite_set 

  selectAssets(ans,am,amt):AM = 
    overw(filter(ans,am),amt)

  preprocessfile(a,tag):Asset

  preprocessRefinement(a,b):bool =
   FORALL(tag):|-(preprocessfile(a,tag),preprocessfile(b,tag))
 
  ifdefrefinement: AXIOM
    |-(a,b) <=> FORALL(tag):|-(preprocessfile(a,tag),preprocessfile(b,tag))

  preprocess(t,am,amt):AM = 
    IF (dom(amt)(t`1)) THEN ow((t`1,preprocessfile(map(amt,singleton(t`1)),t`2)),amt)
    ELSE amt
    ENDIF

  keepdom: LEMMA
    dom(amt) = dom(preprocess(t,am,amt))
  
  Transformations: DATATYPE
   BEGIN
    IFDEF(an:AssetName,tag:boolean): IFDEF?
    SELECT(ans:AssetNames): SELECT?
   END Transformations

  ckevaluation(ts:Transformations,am,amt:AM):AM =
    CASES ts OF
      IFDEF(an,tag): preprocess((an,tag),am,amt),
      SELECT(ans): selectAssets(ans,am,amt)
    ENDCASES

  ckPreserves: THEOREM
   FORALL (am1: AM, am2: AM, t: Transformations, amt1: AM, amt2: AM):
    (am1 |> am2) AND (amt1 |> amt2) =>
     (ckevaluation(t, am1, amt1) |> ckevaluation(t, am2, amt2));


  IMPORTING CKtrans{{
  	    Transformation:=Transformations,
	    transform:=ckevaluation
  }}
  
  fm: VAR WFM
  ck,ck2: VAR CK
  it,it2: VAR Item
  its: VAR list[Item]
  exp: VAR Formula_
  c: VAR Configuration
  anSet: VAR finite_sets[AssetName].finite_set
  s: VAR set[Configuration]


  domainPreserved: LEMMA FORALL ck,am,c,amt: subset?(dom(semanticCK(ck,am,c,amt)),union(dom(am),dom(amt)))  


  domSubset: LEMMA FORALL ck,am,c,amt: subset?(dom(amt),dom(semanticCK(ck,am,c,amt)))

  
  unusedAssets: LEMMA FORALL ck,am,c,amt,anSet: subset?(domain(semanticCK(ck,am,c,amt)),anSet)
                                                =>
                                                (semanticCK(ck,am,c,amt) = semanticCK(ck,filter(anSet,am),c,amt))


  sameAmtSameDom: LEMMA FORALL ck,am,c,amt,amt2: domain(amt) = domain(amt2) 
                                                  => 
                                                  domain(semanticCK(ck,am,c,amt)) = domain(semanticCK(ck,am,c,amt2))  



  sameAmSameDom: LEMMA FORALL ck,am,am2,amt,c: 
                                   domain(am) = domain(am2)  
                                    =>
                                   (domain(semanticCK(ck,am,c,amt)) = domain(semanticCK(ck,am2,c,amt)))


  removeIfDefFromCode: THEOREM
         FORALL (am,s,am2,pairs,ck,an,a,a2):
                (
		  am = ow((an,a),pairs) AND
		  am2 = ow((an,a2),pairs) AND
		  NOT preprocessfile(a,true) = preprocessfile(a2,true) AND
		  preprocessfile(a,false) = preprocessfile(a2,false) AND
		  %getRS(it) = IFDEF(an,true) AND
		  (FORALL it: member(it,ck) =>
		  	  (tasks(it) = IFDEF(an,true) OR
			  tasks(it) = SELECT(an))
			  =>
			  FORALL c: s(c) => NOT satisfies(exp(it),c))
		)  
	       =>
	       (FORALL amt: (FORALL c: s(c) => semanticsCK(ck,am,c,amt) = semanticsCK(ck,am2,c,amt)))
            

  

END CKmultiple