Theory Value

(*  Title:       Jive Data and Store Model
    Author:      Norbert Schirmer <schirmer at informatik.tu-muenchen.de>  and  
                 Nicole Rauch <rauch at informatik.uni-kl.de>, 2003
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)
 
section ‹Value›

theory Value imports Subtype begin

text ‹This theory contains our model of the values in the store. The store is untyped, therefore all
  types that exist in Java are wrapped into one type ‹Value›.

  In a first approach, the primitive Java types supported in this formalization are 
  mapped to similar Isabelle
  types. Later, we will have
  proper formalizations of the Java types in Isabelle, which will then be used here.
›
  
type_synonym JavaInt = int
type_synonym JavaShort = int
type_synonym JavaByte = int
type_synonym JavaBoolean = bool

text ‹The objects of each class are identified by a unique ID.
We use elements of type @{typ nat} here, but in general it is sufficient to use
an infinite type with a successor function and a comparison predicate.
›

type_synonym ObjectId = nat

text ‹The definition of the datatype ‹Value›. Values can be of the Java types 
boolean, int, short and byte. Additionally, they can be an object reference,
an array reference or the value null.›

datatype Value = boolV  JavaBoolean
               | intgV  JavaInt  
               | shortV JavaShort
               | byteV  JavaByte
               | objV   CTypeId ObjectId   ― ‹typed object reference›
               | arrV   Arraytype ObjectId ― ‹typed array reference›
               | nullV
               

text ‹Arrays are modeled as references just like objects. So they
can be viewed as special kinds of objects, like in Java.›

subsection ‹Discriminator Functions›

text ‹To test values, we define the following discriminator functions.›

definition isBoolV  :: "Value ⇒ bool" where
"isBoolV v = (case v of
               boolV b  ⇒ True 
             | intgV i  ⇒ False
             | shortV s ⇒ False
             | byteV  by ⇒ False
             | objV C a ⇒ False
             | arrV T a ⇒ False
             | nullV    ⇒ False)"

lemma isBoolV_simps [simp]:
"isBoolV (boolV b)       = True" 
"isBoolV (intgV i)       = False"
"isBoolV (shortV s)      = False"
"isBoolV (byteV by)       = False"
"isBoolV (objV C a)      = False"
"isBoolV (arrV T a)      = False"
"isBoolV (nullV)         = False"
  by (simp_all add: isBoolV_def)


definition isIntgV  :: "Value ⇒ bool" where
"isIntgV v = (case v of
               boolV b  ⇒ False 
             | intgV i  ⇒ True
             | shortV s ⇒ False
             | byteV by  ⇒ False
             | objV C a ⇒ False
             | arrV T a ⇒ False
             | nullV    ⇒ False)" 

lemma isIntgV_simps [simp]:
"isIntgV (boolV b)       = False" 
"isIntgV (intgV i)       = True"
"isIntgV (shortV s)       = False"
"isIntgV (byteV by)       = False"
"isIntgV (objV C a)      = False"
"isIntgV (arrV T a)      = False"
"isIntgV (nullV)         = False"
  by (simp_all add: isIntgV_def)


definition isShortV :: "Value ⇒ bool" where
"isShortV v = (case v of
               boolV b  ⇒ False 
             | intgV i  ⇒ False
             | shortV s ⇒ True
             | byteV by  ⇒ False
             | objV C a ⇒ False
             | arrV T a ⇒ False
             | nullV    ⇒ False)" 

lemma isShortV_simps [simp]:
"isShortV (boolV b)     = False" 
"isShortV (intgV i)     = False"
"isShortV (shortV s)    = True"
"isShortV (byteV by)     = False"
"isShortV (objV C a)    = False"
"isShortV (arrV T a)    = False"
"isShortV (nullV)       = False"
  by (simp_all add: isShortV_def)


definition isByteV :: "Value ⇒ bool" where
"isByteV v = (case v of
               boolV b  ⇒ False 
             | intgV i  ⇒ False
             | shortV s ⇒ False
             | byteV by  ⇒ True
             | objV C a ⇒ False
             | arrV T a ⇒ False
             | nullV    ⇒ False)" 

lemma isByteV_simps [simp]:
"isByteV (boolV b)      = False" 
"isByteV (intgV i)      = False"
"isByteV (shortV s)     = False"
"isByteV (byteV by)      = True"
"isByteV (objV C a)     = False"
"isByteV (arrV T a)     = False"
"isByteV (nullV)        = False"
  by (simp_all add: isByteV_def)


definition isRefV :: "Value ⇒ bool" where
"isRefV v = (case v of
               boolV b  ⇒ False 
             | intgV i  ⇒ False
             | shortV s ⇒ False
             | byteV by ⇒ False
             | objV C a  ⇒ True
             | arrV T a  ⇒ True
             | nullV     ⇒ True)"

lemma isRefV_simps [simp]:
"isRefV (boolV b)       = False" 
"isRefV (intgV i)       = False"
"isRefV (shortV s)      = False"
"isRefV (byteV by)      = False"
"isRefV (objV C a)      = True"
"isRefV (arrV T a)      = True"
"isRefV (nullV)         = True"
  by (simp_all add: isRefV_def)


definition isObjV :: "Value ⇒ bool" where
"isObjV v = (case v of
               boolV b  ⇒ False 
             | intgV i  ⇒ False
             | shortV s  ⇒ False
             | byteV by  ⇒ False
             | objV C a ⇒ True
             | arrV T a ⇒ False
             | nullV    ⇒ False)"

lemma isObjV_simps [simp]:
"isObjV (boolV b)  = False" 
"isObjV (intgV i)  = False"
"isObjV (shortV s)  = False"
"isObjV (byteV by)  = False"
"isObjV (objV c a) = True" 
"isObjV (arrV T a) = False"
"isObjV nullV      = False"
  by (simp_all add: isObjV_def)


definition isArrV :: "Value ⇒ bool" where
"isArrV v = (case v of
               boolV b  ⇒ False 
             | intgV i  ⇒ False
             | shortV s  ⇒ False
             | byteV by  ⇒ False
             | objV C a ⇒ False
             | arrV T a ⇒ True
             | nullV    ⇒ False)"

lemma isArrV_simps [simp]:
"isArrV (boolV b)  = False" 
"isArrV (intgV i)  = False"
"isArrV (shortV s)  = False"
"isArrV (byteV by)  = False"
"isArrV (objV c a) = False" 
"isArrV (arrV T a) = True"
"isArrV nullV      = False"
  by (simp_all add: isArrV_def)


definition isNullV  :: "Value ⇒ bool" where
"isNullV v = (case v of
               boolV b  ⇒ False 
             | intgV i  ⇒ False
             | shortV s  ⇒ False
             | byteV by  ⇒ False
             | objV C a ⇒ False
             | arrV T a ⇒ False
             | nullV    ⇒ True)"

lemma isNullV_simps [simp]:
"isNullV (boolV b)   = False" 
"isNullV (intgV i)   = False"
"isNullV (shortV s)   = False"
"isNullV (byteV by)   = False"
"isNullV (objV c a) = False" 
"isNullV (arrV T a) = False"
"isNullV nullV      = True"
  by (simp_all add: isNullV_def)

subsection ‹Selector Functions›

definition aI :: "Value ⇒ JavaInt" where
"aI v = (case v of  
            boolV  b   ⇒ undefined
          | intgV  i   ⇒ i
          | shortV sh  ⇒ undefined
          | byteV  by  ⇒ undefined
          | objV   C a ⇒ undefined
          | arrV  T a  ⇒ undefined
          | nullV      ⇒ undefined)"
lemma aI_simps [simp]:
"aI (intgV i) = i"
by (simp add: aI_def)


definition aB :: "Value ⇒ JavaBoolean" where
"aB v = (case v of  
            boolV  b   ⇒ b
          | intgV  i   ⇒ undefined
          | shortV sh  ⇒ undefined
          | byteV  by  ⇒ undefined
          | objV   C a ⇒ undefined
          | arrV  T a  ⇒ undefined
          | nullV      ⇒ undefined)"
lemma aB_simps [simp]:
"aB (boolV b) = b"
by (simp add: aB_def)


definition aSh :: "Value ⇒ JavaShort" where
"aSh v = (case v of  
            boolV  b   ⇒ undefined
          | intgV  i   ⇒ undefined
          | shortV sh  ⇒ sh
          | byteV  by  ⇒ undefined
          | objV   C a ⇒ undefined
          | arrV  T a  ⇒ undefined
          | nullV      ⇒ undefined)"
lemma aSh_simps [simp]:
"aSh (shortV sh) = sh"
by (simp add: aSh_def)


definition aBy :: "Value ⇒ JavaByte" where
"aBy v = (case v of  
            boolV  b   ⇒ undefined
          | intgV  i   ⇒ undefined
          | shortV s   ⇒ undefined
          | byteV  by  ⇒ by
          | objV   C a ⇒ undefined
          | arrV  T a  ⇒ undefined
          | nullV      ⇒ undefined)"
lemma aBy_simps [simp]:
"aBy (byteV by) = by"
by (simp add: aBy_def)


definition tid :: "Value ⇒ CTypeId" where
"tid v = (case v of
            boolV  b   ⇒ undefined
          | intgV  i   ⇒ undefined
          | shortV s   ⇒ undefined
          | byteV  by  ⇒ undefined
          | objV   C a ⇒ C
          | arrV  T a  ⇒ undefined
          | nullV      ⇒ undefined)"

lemma tid_simps [simp]:
"tid (objV C a) = C"
by (simp add: tid_def)


definition oid :: "Value ⇒ ObjectId" where
"oid v = (case v of
            boolV  b   ⇒ undefined
          | intgV  i   ⇒ undefined
          | shortV s   ⇒ undefined
          | byteV  by  ⇒ undefined
          | objV   C a ⇒ a
          | arrV  T a  ⇒ undefined
          | nullV      ⇒ undefined)"

lemma oid_simps [simp]:
"oid (objV C a) = a"
by (simp add: oid_def)


definition jt :: "Value ⇒ Javatype" where
"jt v = (case v of
            boolV  b   ⇒ undefined
          | intgV  i   ⇒ undefined
          | shortV s   ⇒ undefined
          | byteV  by  ⇒ undefined
          | objV   C a ⇒ undefined
          | arrV  T a  ⇒ at2jt T
          | nullV      ⇒ undefined)"

lemma jt_simps [simp]:
"jt (arrV T a) = at2jt T"
by (simp add: jt_def)


definition aid :: "Value ⇒ ObjectId" where
"aid v = (case v of
            boolV  b   ⇒ undefined
          | intgV  i   ⇒ undefined
          | shortV s   ⇒ undefined
          | byteV  by  ⇒ undefined
          | objV   C a ⇒ undefined
          | arrV  T a  ⇒ a
          | nullV      ⇒ undefined)"

lemma aid_simps [simp]:
"aid (arrV T a) = a"
by (simp add: aid_def)

subsection‹Determining the Type of a Value›

text ‹To determine the type of a value, we define the function
‹typeof›. This function is
often written as $\tau$ in theoretical texts, therefore we add
the appropriate syntax support.›

definition typeof :: "Value ⇒ Javatype" where
"typeof v = (case v of
               boolV b  ⇒ BoolT 
             | intgV i  ⇒ IntgT
             | shortV sh  ⇒ ShortT
             | byteV by  ⇒ ByteT
             | objV C a ⇒ CClassT C
             | arrV T a ⇒ ArrT T
             | nullV    ⇒ NullT)"

abbreviation tau_syntax :: "Value ⇒ Javatype" (‹τ _›)
  where "τ v == typeof v"

lemma typeof_simps [simp]:
"(τ (boolV b)) = BoolT"
"(τ (intgV i)) = IntgT"
"(τ (shortV sh)) = ShortT"
"(τ (byteV by)) = ByteT"
"(τ (objV c a)) = CClassT c"
"(τ (arrV t a)) = ArrT t"
"(τ (nullV))   = NullT"
  by (simp_all add: typeof_def)


subsection ‹Default Initialization Values for Types›

text ‹The function ‹init› yields the default initialization values for each 
type. For boolean, the
default value is False, for the integral types, it is 0, and for the reference
types, it is nullV.
›

definition init :: "Javatype ⇒ Value" where
"init T = (case T of
             BoolT        ⇒ boolV  False
           | IntgT        ⇒ intgV  0
           | ShortT        ⇒ shortV 0
           | ByteT        ⇒ byteV  0
           | NullT        ⇒ nullV
           | ArrT T       ⇒ nullV
           | CClassT C     ⇒ nullV
           | AClassT C     ⇒ nullV
           | InterfaceT I ⇒ nullV)" 

lemma init_simps [simp]:
"init BoolT          = boolV False"
"init IntgT          = intgV 0"
"init ShortT         = shortV 0"
"init ByteT          = byteV 0"
"init NullT          = nullV"
"init (ArrT T)       = nullV"
"init (CClassT c)     = nullV"
"init (AClassT a)     = nullV"
"init (InterfaceT i) = nullV"
  by (simp_all add: init_def)

lemma typeof_init_widen [simp,intro]: "typeof (init T) ≤ T"
proof (cases T)
  assume c: "T = BoolT"
  show "(τ (init T)) ≤ T"
    using c by simp
next
  assume c: "T = IntgT"
  show "(τ (init T)) ≤ T"
    using c by simp
next
  assume c: "T = ShortT"
  show "(τ (init T)) ≤ T"
    using c by simp
next
  assume c: "T = ByteT"
  show "(τ (init T)) ≤ T"
    using c by simp
next
  assume c: "T = NullT"
  show "(τ (init T)) ≤ T"
    using c by simp
next
  fix x
  assume c: "T = CClassT x"
  show "(τ (init T)) ≤ T"
    using c by (cases x, simp_all)
next
  fix x
  assume c: "T = AClassT x"
  show "(τ (init T)) ≤ T"
    using c by (cases x, simp_all)
next
  fix x
  assume c: "T = InterfaceT x"
  show "(τ (init T)) ≤ T"
    using c by (cases x, simp_all)
next
  fix x
  assume c: "T = ArrT x"
  show "(τ (init T)) ≤ T"
    using c 
  proof (cases x)
    fix y
    assume c2: "x = CClassAT y"
    show "(τ (init T)) ≤ T"
      using c c2 by (cases y, simp_all)
  next
    fix y
    assume c2: "x = AClassAT y"
    show "(τ (init T)) ≤ T"
      using c c2 by (cases y, simp_all)
  next
    fix y
    assume c2: "x = InterfaceAT y"
    show "(τ (init T)) ≤ T"
      using c c2 by (cases y, simp_all)
  next
    assume c2: "x = BoolAT"
    show "(τ (init T)) ≤ T"
      using c c2 by simp
  next
    assume c2: "x = IntgAT"
    show "(τ (init T)) ≤ T"
      using c c2 by simp
  next
    assume c2: "x = ShortAT"
    show "(τ (init T)) ≤ T"
      using c c2 by simp
  next
    assume c2: "x = ByteAT"
    show "(τ (init T)) ≤ T"
      using c c2 by simp
  qed
qed

end