equal
deleted
inserted
replaced
18 obj_ty :: "obj => ty" |
18 obj_ty :: "obj => ty" |
19 "obj_ty obj == Class (fst obj)" |
19 "obj_ty obj == Class (fst obj)" |
20 |
20 |
21 init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" |
21 init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" |
22 "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))" |
22 "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))" |
23 |
|
24 lemma [code] (*manual eta expansion*): |
|
25 "init_vars xs = map_of (map (\<lambda>(n, T). (n, default_val T)) xs)" |
|
26 by (simp add: init_vars_def) |
|
27 |
23 |
28 types aheap = "loc \<rightharpoonup> obj" -- {* "@{text heap}" used in a translation below *} |
24 types aheap = "loc \<rightharpoonup> obj" -- {* "@{text heap}" used in a translation below *} |
29 locals = "vname \<rightharpoonup> val" -- "simple state, i.e. variable contents" |
25 locals = "vname \<rightharpoonup> val" -- "simple state, i.e. variable contents" |
30 |
26 |
31 state = "aheap \<times> locals" -- "heap, local parameter including This" |
27 state = "aheap \<times> locals" -- "heap, local parameter including This" |