equal
deleted
inserted
replaced
101 apply (drule wf_subcls1) |
101 apply (drule wf_subcls1) |
102 apply (subst def_wfrec[OF class_rec_def], auto) |
102 apply (subst def_wfrec[OF class_rec_def], auto) |
103 apply (subst cut_apply, auto intro: subcls1I) |
103 apply (subst cut_apply, auto intro: subcls1I) |
104 done |
104 done |
105 |
105 |
106 \<comment>\<open>Methods of a class, with inheritance and hiding\<close> |
106 \<comment> \<open>Methods of a class, with inheritance and hiding\<close> |
107 definition "method" :: "cname => (mname \<rightharpoonup> methd)" where |
107 definition "method" :: "cname => (mname \<rightharpoonup> methd)" where |
108 "method C \<equiv> class_rec C methods" |
108 "method C \<equiv> class_rec C methods" |
109 |
109 |
110 lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
110 lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
111 method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)" |
111 method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)" |
113 apply (erule (1) class_rec [THEN trans]) |
113 apply (erule (1) class_rec [THEN trans]) |
114 apply simp |
114 apply simp |
115 done |
115 done |
116 |
116 |
117 |
117 |
118 \<comment>\<open>Fields of a class, with inheritance and hiding\<close> |
118 \<comment> \<open>Fields of a class, with inheritance and hiding\<close> |
119 definition field :: "cname => (fname \<rightharpoonup> ty)" where |
119 definition field :: "cname => (fname \<rightharpoonup> ty)" where |
120 "field C \<equiv> class_rec C flds" |
120 "field C \<equiv> class_rec C flds" |
121 |
121 |
122 lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
122 lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
123 field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)" |
123 field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)" |