1(* Title: HOL/Bali/Value.thy 2 Author: David von Oheimb 3*) 4subsection \<open>Java values\<close> 5 6 7 8theory Value imports Type begin 9 10typedecl loc \<comment> \<open>locations, i.e. abstract references on objects\<close> 11 12datatype val 13 = Unit \<comment> \<open>dummy result value of void methods\<close> 14 | Bool bool \<comment> \<open>Boolean value\<close> 15 | Intg int \<comment> \<open>integer value\<close> 16 | Null \<comment> \<open>null reference\<close> 17 | Addr loc \<comment> \<open>addresses, i.e. locations of objects\<close> 18 19 20primrec the_Bool :: "val \<Rightarrow> bool" 21 where "the_Bool (Bool b) = b" 22 23primrec the_Intg :: "val \<Rightarrow> int" 24 where "the_Intg (Intg i) = i" 25 26primrec the_Addr :: "val \<Rightarrow> loc" 27 where "the_Addr (Addr a) = a" 28 29type_synonym dyn_ty = "loc \<Rightarrow> ty option" 30 31primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" 32where 33 "typeof dt Unit = Some (PrimT Void)" 34| "typeof dt (Bool b) = Some (PrimT Boolean)" 35| "typeof dt (Intg i) = Some (PrimT Integer)" 36| "typeof dt Null = Some NT" 37| "typeof dt (Addr a) = dt a" 38 39primrec defpval :: "prim_ty \<Rightarrow> val" \<comment> \<open>default value for primitive types\<close> 40where 41 "defpval Void = Unit" 42| "defpval Boolean = Bool False" 43| "defpval Integer = Intg 0" 44 45primrec default_val :: "ty \<Rightarrow> val" \<comment> \<open>default value for all types\<close> 46where 47 "default_val (PrimT pt) = defpval pt" 48| "default_val (RefT r ) = Null" 49 50end 51