src/HOL/MicroJava/J/State.thy

 (*  Title:      HOL/MicroJava/J/State.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Program State} *}
 
-theory State imports TypeRel Value begin
+theory State
+imports TypeRel Value
+begin
 
 types 
   fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
 
   obj = "cname \<times> fields'"    -- "class instance with class name and fields"

   obj_ty  :: "obj => ty"
  "obj_ty obj  == Class (fst obj)"
 
   init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
  "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-  
+
+lemma [code] (*manual eta expansion*):
+  "init_vars xs = map_of (map (\<lambda>(n, T). (n, default_val T)) xs)"
+  by (simp add: init_vars_def)
 
 types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
       locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
 
       state  = "aheap \<times> locals"      -- "heap, local parameter including This"