90 acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a" |
90 acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a" |
91 |
91 |
92 lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" |
92 lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" |
93 by (simp add: acc_modi_accmodi_def) |
93 by (simp add: acc_modi_accmodi_def) |
94 |
94 |
95 instance access_field_type:: ("type","type") has_accmodi .. |
95 instance decl_ext_type:: ("type") has_accmodi .. |
96 |
96 |
97 defs (overloaded) |
97 defs (overloaded) |
98 decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d" |
98 decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d" |
99 |
99 |
100 |
100 |
128 out of various HOL types *} |
128 out of various HOL types *} |
129 |
129 |
130 axclass has_declclass < "type" |
130 axclass has_declclass < "type" |
131 consts declclass:: "'a::has_declclass \<Rightarrow> qtname" |
131 consts declclass:: "'a::has_declclass \<Rightarrow> qtname" |
132 |
132 |
133 instance pid_field_type::("type","type") has_declclass .. |
133 instance qtname_ext_type::("type") has_declclass .. |
134 |
134 |
135 defs (overloaded) |
135 defs (overloaded) |
136 qtname_declclass_def: "declclass (q::qtname) \<equiv> q" |
136 qtname_declclass_def: "declclass (q::qtname) \<equiv> q" |
137 |
137 |
138 lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" |
138 lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" |
151 |
151 |
152 |
152 |
153 axclass has_static < "type" |
153 axclass has_static < "type" |
154 consts is_static :: "'a::has_static \<Rightarrow> bool" |
154 consts is_static :: "'a::has_static \<Rightarrow> bool" |
155 |
155 |
156 instance access_field_type :: ("type","has_static") has_static .. |
156 instance decl_ext_type :: ("has_static") has_static .. |
157 |
157 |
158 defs (overloaded) |
158 defs (overloaded) |
159 decl_is_static_def: |
159 decl_is_static_def: |
160 "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" |
160 "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" |
161 |
161 |
162 instance static_field_type :: ("type","type") has_static .. |
162 instance member_ext_type :: ("type") has_static .. |
163 |
163 |
164 defs (overloaded) |
164 defs (overloaded) |
165 static_field_type_is_static_def: |
165 static_field_type_is_static_def: |
166 "is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m" |
166 "is_static (m::('b::type) member_ext_type) \<equiv> static_val m" |
167 |
167 |
168 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" |
168 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" |
169 apply (cases m) |
169 apply (cases m) |
170 apply (simp add: static_field_type_is_static_def |
170 apply (simp add: static_field_type_is_static_def |
171 decl_is_static_def Decl.member.dest_convs) |
171 decl_is_static_def Decl.member.dest_convs) |
399 out of various HOL types *} |
399 out of various HOL types *} |
400 |
400 |
401 axclass has_resTy < "type" |
401 axclass has_resTy < "type" |
402 consts resTy:: "'a::has_resTy \<Rightarrow> ty" |
402 consts resTy:: "'a::has_resTy \<Rightarrow> ty" |
403 |
403 |
404 instance access_field_type :: ("type","has_resTy") has_resTy .. |
404 instance decl_ext_type :: ("has_resTy") has_resTy .. |
405 |
405 |
406 defs (overloaded) |
406 defs (overloaded) |
407 decl_resTy_def: |
407 decl_resTy_def: |
408 "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" |
408 "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" |
409 |
409 |
410 instance static_field_type :: ("type","has_resTy") has_resTy .. |
410 instance member_ext_type :: ("has_resTy") has_resTy .. |
411 |
411 |
412 defs (overloaded) |
412 defs (overloaded) |
413 static_field_type_resTy_def: |
413 member_ext_type_resTy_def: |
414 "resTy (m::(bool,'b::has_resTy) static_field_type) |
414 "resTy (m::('b::has_resTy) member_ext_type) |
415 \<equiv> resTy (static_more m)" |
415 \<equiv> resTy (member.more_val m)" |
416 |
416 |
417 instance pars_field_type :: ("type","has_resTy") has_resTy .. |
417 instance mhead_ext_type :: ("type") has_resTy .. |
418 |
418 |
419 defs (overloaded) |
419 defs (overloaded) |
420 pars_field_type_resTy_def: |
420 mhead_ext_type_resTy_def: |
421 "resTy (m::(vname list,'b::has_resTy) pars_field_type) |
421 "resTy (m::('b mhead_ext_type)) |
422 \<equiv> resTy (pars_more m)" |
|
423 |
|
424 instance resT_field_type :: ("type","type") has_resTy .. |
|
425 |
|
426 defs (overloaded) |
|
427 resT_field_type_resTy_def: |
|
428 "resTy (m::(ty,'b::type) resT_field_type) |
|
429 \<equiv> resT_val m" |
422 \<equiv> resT_val m" |
430 |
423 |
431 lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" |
424 lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" |
432 apply (cases m) |
425 apply (cases m) |
433 apply (simp add: decl_resTy_def static_field_type_resTy_def |
426 apply (simp add: decl_resTy_def member_ext_type_resTy_def |
434 pars_field_type_resTy_def resT_field_type_resTy_def |
427 mhead_ext_type_resTy_def |
435 member.dest_convs mhead.dest_convs) |
428 member.dest_convs mhead.dest_convs) |
436 done |
429 done |
437 |
430 |
438 lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" |
431 lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" |
439 by (simp add: mhead_def mhead_resTy_simp) |
432 by (simp add: mhead_def mhead_resTy_simp) |