src/HOL/Bali/DeclConcepts.thy
changeset 21765 89275a3ed7be
parent 19564 d3e2f532459a
child 22426 1c38ca2496c4
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Dec 11 12:28:16 2006 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Dec 11 16:06:14 2006 +0100
     1.3 @@ -536,26 +536,21 @@
     1.4  
     1.5  subsubsection "members"
     1.6  
     1.7 -consts
     1.8 -members:: "prog \<Rightarrow> (qtname \<times> (qtname \<times> memberdecl)) set"
     1.9  (* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because
    1.10     the class qtname changes to the superclass in the inductive definition
    1.11     below
    1.12  *)
    1.13  
    1.14 -syntax
    1.15 -member_of:: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    1.16 -                           ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
    1.17 -
    1.18 -translations
    1.19 - "G\<turnstile>m member_of C" \<rightleftharpoons> "(C,m) \<in> members G"
    1.20 +inductive2
    1.21 +  members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    1.22 +    ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
    1.23 +  for G :: prog
    1.24 +where
    1.25  
    1.26 -inductive "members G"  intros
    1.27 -
    1.28 -Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
    1.29 -Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 
    1.30 -             G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
    1.31 -            \<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
    1.32 +  Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
    1.33 +| Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 
    1.34 +               G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
    1.35 +              \<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
    1.36  text {* Note that in the case of an inherited member only the members of the
    1.37  direct superclass are concerned. If a member of a superclass of the direct
    1.38  superclass isn't inherited in the direct superclass (not member of the
    1.39 @@ -619,9 +614,6 @@
    1.40  translations
    1.41   "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 
    1.42  
    1.43 -consts stat_overridesR::
    1.44 -  "prog  \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"
    1.45 -
    1.46  lemma member_inD: "G\<turnstile>m member_in C 
    1.47   \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
    1.48  by (auto simp add: member_in_def)
    1.49 @@ -641,48 +633,43 @@
    1.50  *}
    1.51  
    1.52  text {* Static overriding (used during the typecheck of the compiler) *}
    1.53 -syntax
    1.54 -stat_overrides:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
    1.55 -                                  ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
    1.56 -translations
    1.57 - "G\<turnstile>new overrides\<^sub>S  old" == "(new,old) \<in> stat_overridesR G "
    1.58  
    1.59 -inductive "stat_overridesR G" intros
    1.60 +inductive2
    1.61 +  stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
    1.62 +    ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
    1.63 +  for G :: prog
    1.64 +where
    1.65  
    1.66 -Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 
    1.67 -         G\<turnstile>Method new declared_in (declclass new);  
    1.68 -         G\<turnstile>Method old declared_in (declclass old); 
    1.69 -         G\<turnstile>Method old inheritable_in pid (declclass new);
    1.70 -         G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew;
    1.71 -         G \<turnstile>Method old member_of superNew
    1.72 -         \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
    1.73 +  Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 
    1.74 +           G\<turnstile>Method new declared_in (declclass new);  
    1.75 +           G\<turnstile>Method old declared_in (declclass old); 
    1.76 +           G\<turnstile>Method old inheritable_in pid (declclass new);
    1.77 +           G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew;
    1.78 +           G \<turnstile>Method old member_of superNew
    1.79 +           \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
    1.80  
    1.81 -Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
    1.82 -           \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
    1.83 +| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
    1.84 +             \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
    1.85  
    1.86  text {* Dynamic overriding (used during the typecheck of the compiler) *}
    1.87 -consts overridesR::
    1.88 -  "prog  \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"
    1.89  
    1.90 -
    1.91 -overrides:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
    1.92 -                                  ("_ \<turnstile> _ overrides _" [61,61,61] 60)
    1.93 -translations
    1.94 - "G\<turnstile>new overrides old" == "(new,old) \<in> overridesR G "
    1.95 -
    1.96 -inductive "overridesR G" intros
    1.97 +inductive2
    1.98 +  overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
    1.99 +    ("_ \<turnstile> _ overrides _" [61,61,61] 60)
   1.100 +  for G :: prog
   1.101 +where
   1.102  
   1.103 -Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private;
   1.104 -         msig new = msig old; 
   1.105 -         G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
   1.106 -         G\<turnstile>Method new declared_in (declclass new);  
   1.107 -         G\<turnstile>Method old declared_in (declclass old);    
   1.108 -         G\<turnstile>Method old inheritable_in pid (declclass new);
   1.109 -         G\<turnstile>resTy new \<preceq> resTy old
   1.110 -         \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
   1.111 +  Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private;
   1.112 +           msig new = msig old; 
   1.113 +           G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
   1.114 +           G\<turnstile>Method new declared_in (declclass new);  
   1.115 +           G\<turnstile>Method old declared_in (declclass old);    
   1.116 +           G\<turnstile>Method old inheritable_in pid (declclass new);
   1.117 +           G\<turnstile>resTy new \<preceq> resTy old
   1.118 +           \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
   1.119  
   1.120 -Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
   1.121 -           \<Longrightarrow> G\<turnstile>new overrides old"
   1.122 +| Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
   1.123 +            \<Longrightarrow> G\<turnstile>new overrides old"
   1.124  
   1.125  syntax
   1.126  sig_stat_overrides:: 
   1.127 @@ -797,28 +784,31 @@
   1.128  \end{itemize} 
   1.129  *} 
   1.130  
   1.131 -
   1.132 -consts
   1.133 -accessible_fromR:: 
   1.134 - "prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times>  qtname) set"
   1.135 +inductive2
   1.136 +  accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   1.137 +  and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.138 +    ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
   1.139 +  and method_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.140 +    ("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60)
   1.141 +  for G :: prog and accclass :: qtname
   1.142 +where
   1.143 +  "G\<turnstile>membr of cls accessible_from accclass \<equiv> accessible_fromR G accclass membr cls"
   1.144  
   1.145 -syntax 
   1.146 -accessible_from:: 
   1.147 - "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.148 -                   ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
   1.149 +| "G\<turnstile>Method m of cls accessible_from accclass \<equiv>
   1.150 +   G\<turnstile>methdMembr m of cls accessible_from accclass"  
   1.151  
   1.152 -translations
   1.153 -"G\<turnstile>membr of cls accessible_from accclass"  
   1.154 - \<rightleftharpoons> "(membr,cls) \<in> accessible_fromR G accclass"
   1.155 +| Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
   1.156 +                G\<turnstile>(Class class) accessible_in (pid accclass);
   1.157 +                G\<turnstile>membr in class permits_acc_from accclass 
   1.158 +               \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   1.159  
   1.160 -syntax 
   1.161 -method_accessible_from:: 
   1.162 - "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.163 -                   ("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60)
   1.164 -
   1.165 -translations
   1.166 -"G\<turnstile>Method m of cls accessible_from accclass"  
   1.167 - \<rightleftharpoons> "G\<turnstile>methdMembr m of cls accessible_from accclass"  
   1.168 +| Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
   1.169 +                G\<turnstile>(Class class) accessible_in (pid accclass);
   1.170 +                membr=(C,mdecl new);
   1.171 +                G\<turnstile>(C,new) overrides\<^sub>S old; 
   1.172 +                G\<turnstile>class \<prec>\<^sub>C sup;
   1.173 +                G\<turnstile>Method old of sup accessible_from accclass
   1.174 +               \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   1.175  
   1.176  syntax 
   1.177  methd_accessible_from:: 
   1.178 @@ -838,41 +828,29 @@
   1.179  "G\<turnstile>Field fn f of C accessible_from accclass"  
   1.180   \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
   1.181  
   1.182 -inductive "accessible_fromR G accclass" intros
   1.183 -Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
   1.184 -              G\<turnstile>(Class class) accessible_in (pid accclass);
   1.185 -              G\<turnstile>membr in class permits_acc_from accclass 
   1.186 -             \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   1.187 -
   1.188 -Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
   1.189 -              G\<turnstile>(Class class) accessible_in (pid accclass);
   1.190 -              membr=(C,mdecl new);
   1.191 -              G\<turnstile>(C,new) overrides\<^sub>S old; 
   1.192 -              G\<turnstile>class \<prec>\<^sub>C sup;
   1.193 -              G\<turnstile>Method old of sup accessible_from accclass
   1.194 -             \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   1.195 -
   1.196 -consts
   1.197 -dyn_accessible_fromR:: 
   1.198 - "prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times>  qtname) set"
   1.199 +inductive2
   1.200 +  dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   1.201 +  and dyn_accessible_from' ::  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.202 +    ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   1.203 +  and method_dyn_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.204 +    ("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   1.205 +  for G :: prog and accclass :: qtname
   1.206 +where
   1.207 +  "G\<turnstile>membr in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC membr C"
   1.208  
   1.209 -syntax 
   1.210 -dyn_accessible_from:: 
   1.211 - "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.212 -                   ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   1.213 +| "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv>
   1.214 +   G\<turnstile>methdMembr m in C dyn_accessible_from accC"
   1.215  
   1.216 -translations
   1.217 -"G\<turnstile>membr in C dyn_accessible_from accC"  
   1.218 - \<rightleftharpoons> "(membr,C) \<in> dyn_accessible_fromR G accC"
   1.219 +| Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
   1.220 +                G\<turnstile>membr in class permits_acc_from accclass 
   1.221 +               \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   1.222  
   1.223 -syntax 
   1.224 -method_dyn_accessible_from:: 
   1.225 - "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.226 -                 ("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   1.227 -
   1.228 -translations
   1.229 -"G\<turnstile>Method m in C dyn_accessible_from accC"  
   1.230 - \<rightleftharpoons> "G\<turnstile>methdMembr m in C dyn_accessible_from accC"  
   1.231 +| Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
   1.232 +                membr=(C,mdecl new);
   1.233 +                G\<turnstile>(C,new) overrides old; 
   1.234 +                G\<turnstile>class \<prec>\<^sub>C sup;
   1.235 +                G\<turnstile>Method old in sup dyn_accessible_from accclass
   1.236 +               \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   1.237  
   1.238  syntax 
   1.239  methd_dyn_accessible_from:: 
   1.240 @@ -891,18 +869,6 @@
   1.241  translations
   1.242  "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"  
   1.243   \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
   1.244 -  
   1.245 -inductive "dyn_accessible_fromR G accclass" intros
   1.246 -Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
   1.247 -              G\<turnstile>membr in class permits_acc_from accclass 
   1.248 -             \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   1.249 -
   1.250 -Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
   1.251 -              membr=(C,mdecl new);
   1.252 -              G\<turnstile>(C,new) overrides old; 
   1.253 -              G\<turnstile>class \<prec>\<^sub>C sup;
   1.254 -              G\<turnstile>Method old in sup dyn_accessible_from accclass
   1.255 -             \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   1.256  
   1.257  
   1.258  lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
   1.259 @@ -967,13 +933,13 @@
   1.260    from n m eqid  
   1.261    show "n=m"
   1.262    proof (induct)
   1.263 -    case (Immediate C n)
   1.264 +    case (Immediate n C)
   1.265      assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C"
   1.266      assume eqid: "memberid n = memberid m"
   1.267      assume "G \<turnstile> m member_of C"
   1.268      then show "n=m"
   1.269      proof (cases)
   1.270 -      case (Immediate _ m')
   1.271 +      case (Immediate m' _)
   1.272        with eqid 
   1.273        have "m=m'"
   1.274             "memberid n = memberid m" 
   1.275 @@ -987,7 +953,7 @@
   1.276                             cdeclaredmethd_def cdeclaredfield_def
   1.277                      split: memberdecl.splits)
   1.278      next
   1.279 -      case (Inherited _ _ m')
   1.280 +      case (Inherited m' _ _)
   1.281        then have "G\<turnstile> memberid m undeclared_in C"
   1.282  	by simp
   1.283        with eqid member_n
   1.284 @@ -995,7 +961,7 @@
   1.285  	by (cases n) (auto dest: declared_not_undeclared)
   1.286      qed
   1.287    next
   1.288 -    case (Inherited C S n)
   1.289 +    case (Inherited n C S)
   1.290      assume undecl: "G\<turnstile> memberid n undeclared_in C"
   1.291      assume  super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S"
   1.292      assume    hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m"
   1.293 @@ -1021,13 +987,13 @@
   1.294  
   1.295  lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C"
   1.296  proof (induct set: members)
   1.297 -  case (Immediate C m)
   1.298 +  case (Immediate m C)
   1.299    assume "G\<turnstile> mbr m declared_in C"
   1.300    then show "is_class G C"
   1.301      by (cases "mbr m")
   1.302         (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
   1.303  next
   1.304 -  case (Inherited C S m)  
   1.305 +  case (Inherited m C S)  
   1.306    assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S"
   1.307    then show "is_class G C"
   1.308      by - (rule subcls_is_class2,auto)
   1.309 @@ -1046,10 +1012,10 @@
   1.310  lemma member_of_class_relation:
   1.311    "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
   1.312  proof (induct set: members)
   1.313 -  case (Immediate C m)
   1.314 +  case (Immediate m C)
   1.315    then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp
   1.316  next
   1.317 -  case (Inherited C S m)
   1.318 +  case (Inherited m C S)
   1.319    then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" 
   1.320      by (auto dest: r_into_rtrancl intro: rtrancl_trans)
   1.321  qed
   1.322 @@ -1152,12 +1118,12 @@
   1.323    from acc_C static
   1.324    show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
   1.325    proof (induct)
   1.326 -    case (Immediate C m)
   1.327 +    case (Immediate m C)
   1.328      then show ?case 
   1.329        by (auto intro!: dyn_accessible_fromR.Immediate
   1.330                   dest: member_in_declC permits_acc_static_declC) 
   1.331    next 
   1.332 -    case (Overriding declCNew C m new old sup)
   1.333 +    case (Overriding m C declCNew new old sup)
   1.334      then have "\<not> is_static m"
   1.335        by (auto dest: overrides_commonD)
   1.336      moreover
   1.337 @@ -1259,7 +1225,7 @@
   1.338    from m subclseq_D_C subclseq_C_m
   1.339    show ?thesis
   1.340    proof (induct)
   1.341 -    case (Immediate D m)
   1.342 +    case (Immediate m D)
   1.343      assume "declclass m = D" and
   1.344             "G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m"
   1.345      with ws have "D=C" 
   1.346 @@ -1268,7 +1234,7 @@
   1.347      show "G\<turnstile>m member_of C"
   1.348        by (auto intro: members.Immediate)
   1.349    next
   1.350 -    case (Inherited D S m)
   1.351 +    case (Inherited m D S)
   1.352      assume member_of_D_props: 
   1.353              "G \<turnstile> m inheritable_in pid D" 
   1.354              "G\<turnstile> memberid m undeclared_in D"  
   1.355 @@ -1714,7 +1680,7 @@
   1.356      from member_of
   1.357      show "?Methd C"
   1.358      proof (cases)
   1.359 -      case (Immediate Ca membr)
   1.360 +      case (Immediate membr Ca)
   1.361        then have "Ca=C" "membr = method sig m" and 
   1.362                  "G\<turnstile>Methd sig m declared_in C" "declclass m = C"
   1.363  	by (cases m,auto)
   1.364 @@ -1727,7 +1693,7 @@
   1.365        show ?thesis
   1.366  	by (simp add: methd_rec)
   1.367      next
   1.368 -      case (Inherited Ca S membr)
   1.369 +      case (Inherited membr Ca S)
   1.370        with clsC
   1.371        have eq_Ca_C: "Ca=C" and
   1.372              undecl: "G\<turnstile>mid sig undeclared_in C" and