src/HOL/MicroJava/J/Value.thy

the theory of Equipollence, and moving Fpow from Cardinals into Main

(*  Title:      HOL/MicroJava/J/Value.thy
    Author:     David von Oheimb, Technische Universitaet Muenchen
*)

section \<open>Java Values\<close>

theory Value imports Type begin

typedecl loc' \<comment> \<open>locations, i.e. abstract references on objects\<close> 

datatype loc 
  = XcptRef xcpt \<comment> \<open>special locations for pre-allocated system exceptions\<close>
  | Loc loc'     \<comment> \<open>usual locations (references on objects)\<close>

datatype val
  = Unit        \<comment> \<open>dummy result value of void methods\<close>
  | Null        \<comment> \<open>null reference\<close>
  | Bool bool   \<comment> \<open>Boolean value\<close>
  | Intg int    \<comment> \<open>integer value, name Intg instead of Int because
                   of clash with HOL/Set.thy\<close> 
  | Addr loc    \<comment> \<open>addresses, i.e. locations of objects\<close>

primrec the_Bool :: "val => bool" where
  "the_Bool (Bool b) = b"

primrec the_Intg :: "val => int" where
  "the_Intg (Intg i) = i"

primrec the_Addr :: "val => loc" where
  "the_Addr (Addr a) = a"

primrec defpval :: "prim_ty => val"  \<comment> \<open>default value for primitive types\<close> where
  "defpval Void    = Unit"
| "defpval Boolean = Bool False"
| "defpval Integer = Intg 0"

primrec default_val :: "ty => val"   \<comment> \<open>default value for all types\<close> where
  "default_val (PrimT pt) = defpval pt"
| "default_val (RefT  r ) = Null"

end