equal
deleted
inserted
replaced
131 apply simp |
131 apply simp |
132 done |
132 done |
133 |
133 |
134 |
134 |
135 --{* Fields of a class, with inheritance and hiding *} |
135 --{* Fields of a class, with inheritance and hiding *} |
136 defs field_def: "field C \<equiv> class_rec C fields" |
136 defs field_def: "field C \<equiv> class_rec C flds" |
137 |
137 |
138 lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
138 lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
139 field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)" |
139 field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)" |
140 apply (unfold field_def) |
140 apply (unfold field_def) |
141 apply (erule (1) class_rec [THEN trans]); |
141 apply (erule (1) class_rec [THEN trans]); |
142 apply simp |
142 apply simp |
143 done |
143 done |
144 |
144 |