src/HOL/Bali/DeclConcepts.thy
changeset 32754 4e0256f7d219
parent 32134 ee143615019c
child 32960 69916a850301
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Thu Sep 24 11:33:05 2009 +1000
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Fri Sep 25 19:04:18 2009 +1000
     1.3 @@ -154,21 +154,14 @@
     1.4  
     1.5  instance decl_ext_type :: ("has_static") has_static ..
     1.6  
     1.7 -defs (overloaded)
     1.8 -decl_is_static_def: 
     1.9 - "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 
    1.10 -
    1.11  instance member_ext_type :: ("type") has_static ..
    1.12  
    1.13  defs (overloaded)
    1.14  static_field_type_is_static_def: 
    1.15 - "is_static (m::('b::type) member_ext_type) \<equiv> static_sel m"
    1.16 + "is_static (m::('b member_scheme)) \<equiv> static m"
    1.17  
    1.18  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
    1.19 -apply (cases m)
    1.20 -apply (simp add: static_field_type_is_static_def 
    1.21 -                 decl_is_static_def Decl.member.dest_convs)
    1.22 -done
    1.23 +by (simp add: static_field_type_is_static_def)
    1.24  
    1.25  instance * :: ("type","has_static") has_static ..
    1.26  
    1.27 @@ -402,30 +395,16 @@
    1.28  
    1.29  instance decl_ext_type :: ("has_resTy") has_resTy ..
    1.30  
    1.31 -defs (overloaded)
    1.32 -decl_resTy_def: 
    1.33 - "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 
    1.34 -
    1.35  instance member_ext_type :: ("has_resTy") has_resTy ..
    1.36  
    1.37 -defs (overloaded)
    1.38 -member_ext_type_resTy_def: 
    1.39 - "resTy (m::('b::has_resTy) member_ext_type) 
    1.40 -  \<equiv> resTy (member.more_sel m)" 
    1.41 -
    1.42  instance mhead_ext_type :: ("type") has_resTy ..
    1.43  
    1.44  defs (overloaded)
    1.45  mhead_ext_type_resTy_def: 
    1.46 - "resTy (m::('b mhead_ext_type)) 
    1.47 -  \<equiv> resT_sel m" 
    1.48 + "resTy (m::('b mhead_scheme)) \<equiv> resT m"
    1.49  
    1.50  lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
    1.51 -apply (cases m)
    1.52 -apply (simp add: decl_resTy_def member_ext_type_resTy_def 
    1.53 -                 mhead_ext_type_resTy_def 
    1.54 -                 member.dest_convs mhead.dest_convs)
    1.55 -done
    1.56 +by (simp add: mhead_ext_type_resTy_def)
    1.57  
    1.58  lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
    1.59  by (simp add: mhead_def mhead_resTy_simp)