Theory CertifSafeToSVM_definitions

(*  Title:      Certificate Safe to SVM
    Author:     Javier de Dios and Ricardo Peña
    Copyright:  June 2008, Universidad Complutense de Madrid
*)



header {* Certification of the translation CoreSafe to SVM. Definitions *}

theory CertifSafeToSVM_definitions
imports Main "../CoreSafe/SafeRASemantics" SVMSemantics CoreSafeToSVM

begin


subsection {* Auxiliary functions *}

fun domRho :: "Env => char list set" where
  "domRho [] = {}"
| "domRho ((delta,m,n)#rest) = (dom delta) ∪ domRho rest"

fun identityEnvironment :: "Environment => Env => Stack => bool" (" _ \<Join> '(_, _') " 120) where
  "(E1,E2) \<Join> (ρ,S) = (((dom E1 ∪ dom E2 - {self}) = domRho ρ) 
                                      ∧ (∀ x ∈ dom E1. Val (the (E1 x)) = S!+(ρ |> x))
                                      ∧ (∀ r ∈ dom E2 - {self}. Reg (the (E2 r)) = S!+(ρ |> r)))"


axioms identityEnvironment_good:
 "(E1,E2) \<Join> (ρ,S)
  ==> (∀x∈ dom E1.  S!+(ρ |> x) = Val v) ∧ (∀x∈ dom E2.  S!+(ρ |> x) = Reg r)"

fun sizeST :: "Stack => int" where
  "sizeST [] = 0"
| "sizeST (Val v # S) = 1 + sizeST S"
| "sizeST (Reg r # S) = 1 + sizeST S"
| "sizeST (Cont c # S) = 2 + sizeST S"


fun sizeH :: "Heap => int" where
  "sizeH (h,k) = int (card (dom h))"

fun sizeSVMStateST :: "SVMState => int" where
  "sizeSVMStateST (h,r,pc,s) = sizeST s"

fun sizeSVMStateH :: "SVMState => int" where
  "sizeSVMStateH (h,r,pc,s) = sizeH h"


fun foldl1 :: "('a => 'a => 'a) => 'a list => 'a" where
"foldl1 f (x#xs)  =  foldl f x xs"

fun maximum :: "int list => int" where
  "maximum xs = foldl1 max xs"


fun maxFreshCells :: "SVMState list => int" where
  "maxFreshCells ((h0,r0,pc0,s0)#sts) = maximum (map (%(h,r,pc,s). sizeH h - (sizeH h0)) ((h0,r0,pc0,s0)#sts))"

fun maxFreshWords :: "SVMState list => int" where
  "maxFreshWords ((h0,r0,pc0,s0)#sts) = maximum (map (%(h,r,pc,s). sizeST s - (sizeST s0)) ((h0,r0,pc0,s0)#sts))"

constdefs region :: "Heap => Location => Region"
  "region h l ≡ (case h of 
                  (hm,k) => 
                    case (hm l) of 
                     Some (r,(c,xs)) => r)"

constdefs numCellsRegion :: "Heap => nat => int"
  "numCellsRegion h i ≡ int (card {w ∈ dom (fst h). region h w = i})"

constdefs diff :: "nat => Heap => Heap => nat \<rightharpoonup> int"
  "diff k h h' ≡ (%i. if i ∈ {0..k} 
                       then Some (numCellsRegion h' i - numCellsRegion h i)
                       else None)"
      
constdefs extends :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> 'b) => bool" 
  "extends f g ≡ ((dom f ⊆ dom g) ∧ (∀x ∈ dom f. f x = g x))"

constdefs extendsL :: "('a ×'b) list => ('a ×'b) list => bool" (infix "\<sqsubseteq>" 110 )
 "xs \<sqsubseteq> ys == extends (map_of xs) (map_of ys)"

axioms A7: 
  "SafeHeap.copy (h,k) j p = ((h',k),p') 
   ==> extends h  h' ∧
       size  h' p' = size h p ∧
       sizeH (h',k) - sizeH (h,k) = size h' p' ∧
       (∀ k. k >= j --> diff k (h,k) (h',k) = empty(j\<mapsto>size h' p'))"

constdefs disjointList :: "('a × 'b) list => ('a × 'b) list => bool"
  "disjointList n m ≡ dom (map_of n) ∩ dom (map_of m) = {}"



fun rho_good' :: "Env => bool"  where
  "rho_good' [] = True"
| "rho_good' ((delta,m,n)#rest) = ((∀ x∈ dom delta. m - n >= the (delta x) ∧ the (delta x) >= 1) ∧ rho_good' rest)"

fun rho_good :: "Env => bool"  where
 "rho_good ((delta,m,n)#rest) = (n = 0 ∧ rho_good' ((delta,m,n)#rest))"

end