src/HOL/Bali/DeclConcepts.thy
changeset 35416 d8d7d1b785af
parent 35315 fbdc860d87a3
child 35431 8758fe1fc9f8
child 35440 bdf8ad377877
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -8,8 +8,7 @@
     1.4  
     1.5  section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
     1.6  
     1.7 -constdefs
     1.8 -is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
     1.9 +definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
    1.10  "is_public G qn \<equiv> (case class G qn of
    1.11                       None       \<Rightarrow> (case iface G qn of
    1.12                                        None       \<Rightarrow> False
    1.13 @@ -38,14 +37,16 @@
    1.14  
    1.15  declare accessible_in_RefT_simp [simp del]
    1.16  
    1.17 -constdefs
    1.18 -  is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    1.19 +definition is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
    1.20      "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
    1.21 -  is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    1.22 +
    1.23 +definition is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
    1.24      "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
    1.25 -  is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool"
    1.26 +
    1.27 +definition is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool" where
    1.28      "is_acc_type  G P T \<equiv> is_type G T  \<and> G\<turnstile>T accessible_in P"
    1.29 -  is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
    1.30 +
    1.31 +definition is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" where
    1.32    "is_acc_reftype  G P T \<equiv> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
    1.33  
    1.34  lemma is_acc_classD:
    1.35 @@ -336,8 +337,7 @@
    1.36  text {* Convert a qualified method declaration (qualified with its declaring 
    1.37  class) to a qualified member declaration:  @{text methdMembr}  *}
    1.38  
    1.39 -constdefs
    1.40 -methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)"
    1.41 +definition methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)" where
    1.42   "methdMembr m \<equiv> (fst m,mdecl (snd m))"
    1.43  
    1.44  lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
    1.45 @@ -355,8 +355,7 @@
    1.46  text {* Convert a qualified method (qualified with its declaring 
    1.47  class) to a qualified member declaration:  @{text method}  *}
    1.48  
    1.49 -constdefs
    1.50 -method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" 
    1.51 +definition method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" where 
    1.52  "method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
    1.53  
    1.54  lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
    1.55 @@ -377,8 +376,7 @@
    1.56  lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
    1.57    by (simp add: method_def) 
    1.58  
    1.59 -constdefs
    1.60 -fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" 
    1.61 +definition fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" where 
    1.62  "fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
    1.63  
    1.64  lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
    1.65 @@ -402,7 +400,7 @@
    1.66  text {* Select the signature out of a qualified method declaration:
    1.67   @{text msig} *}
    1.68  
    1.69 -constdefs msig:: "(qtname \<times> mdecl) \<Rightarrow> sig"
    1.70 +definition msig :: "(qtname \<times> mdecl) \<Rightarrow> sig" where
    1.71  "msig m \<equiv> fst (snd m)"
    1.72  
    1.73  lemma msig_simp[simp]: "msig (c,(s,m)) = s"
    1.74 @@ -411,7 +409,7 @@
    1.75  text {* Convert a qualified method (qualified with its declaring 
    1.76  class) to a qualified method declaration:  @{text qmdecl}  *}
    1.77  
    1.78 -constdefs qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
    1.79 +definition qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" where
    1.80  "qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
    1.81  
    1.82  lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
    1.83 @@ -504,10 +502,8 @@
    1.84        it is not accessible for inheritance at all.
    1.85  \end{itemize}
    1.86  *}
    1.87 -constdefs
    1.88 -inheritable_in:: 
    1.89 - "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool"
    1.90 -                  ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
    1.91 +definition inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) where
    1.92 +                  
    1.93  "G\<turnstile>membr inheritable_in pack 
    1.94    \<equiv> (case (accmodi membr) of
    1.95         Private   \<Rightarrow> False
    1.96 @@ -529,25 +525,21 @@
    1.97  
    1.98  subsubsection "declared-in/undeclared-in"
    1.99  
   1.100 -constdefs cdeclaredmethd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table"
   1.101 +definition cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
   1.102  "cdeclaredmethd G C 
   1.103    \<equiv> (case class G C of
   1.104         None \<Rightarrow> \<lambda> sig. None
   1.105       | Some c \<Rightarrow> table_of (methods c)
   1.106      )"
   1.107  
   1.108 -constdefs
   1.109 -cdeclaredfield:: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table"
   1.110 +definition cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
   1.111  "cdeclaredfield G C 
   1.112    \<equiv> (case class G C of
   1.113         None \<Rightarrow> \<lambda> sig. None
   1.114       | Some c \<Rightarrow> table_of (cfields c)
   1.115      )"
   1.116  
   1.117 -
   1.118 -constdefs
   1.119 -declared_in:: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool"
   1.120 -                                 ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
   1.121 +definition declared_in :: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60) where
   1.122  "G\<turnstile>m declared_in C \<equiv> (case m of
   1.123                          fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
   1.124                        | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
   1.125 @@ -567,10 +559,7 @@
   1.126  by (cases m) 
   1.127     (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
   1.128  
   1.129 -constdefs
   1.130 -undeclared_in:: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool"
   1.131 -                                 ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
   1.132 -
   1.133 +definition undeclared_in :: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) where
   1.134  "G\<turnstile>m undeclared_in C \<equiv> (case m of
   1.135                              fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
   1.136                            | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
   1.137 @@ -591,7 +580,7 @@
   1.138  
   1.139    Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
   1.140  | Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 
   1.141 -               G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
   1.142 +               G\<turnstile>C \<prec>\<^sub>C1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
   1.143                \<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
   1.144  text {* Note that in the case of an inherited member only the members of the
   1.145  direct superclass are concerned. If a member of a superclass of the direct
   1.146 @@ -617,19 +606,16 @@
   1.147                             ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
   1.148   where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
   1.149  
   1.150 -constdefs
   1.151 -inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
   1.152 -                           ("_ \<turnstile> _ inherits _" [61,61,61] 60)
   1.153 +definition inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60) where
   1.154  "G\<turnstile>C inherits m 
   1.155    \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
   1.156 -    (\<exists> S. G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)"
   1.157 +    (\<exists> S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)"
   1.158  
   1.159  lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
   1.160  by (auto simp add: inherits_def intro: members.Inherited)
   1.161  
   1.162  
   1.163 -constdefs member_in::"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   1.164 -                           ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
   1.165 +definition member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60) where
   1.166  "G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
   1.167  text {* A member is in a class if it is member of the class or a superclass.
   1.168  If a member is in a class we can select this member. This additional notion
   1.169 @@ -676,7 +662,7 @@
   1.170             G\<turnstile>Method new declared_in (declclass new);  
   1.171             G\<turnstile>Method old declared_in (declclass old); 
   1.172             G\<turnstile>Method old inheritable_in pid (declclass new);
   1.173 -           G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew;
   1.174 +           G\<turnstile>(declclass new) \<prec>\<^sub>C1 superNew;
   1.175             G \<turnstile>Method old member_of superNew
   1.176             \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
   1.177  
   1.178 @@ -716,9 +702,7 @@
   1.179  
   1.180  subsubsection "Hiding"
   1.181  
   1.182 -constdefs hides::
   1.183 -"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
   1.184 -                                ("_\<turnstile> _ hides _" [61,61,61] 60)
   1.185 +definition hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60) where 
   1.186  "G\<turnstile>new hides old
   1.187    \<equiv> is_static new \<and> msig new = msig old \<and>
   1.188      G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   1.189 @@ -777,11 +761,7 @@
   1.190  by (auto simp add: hides_def)
   1.191  
   1.192  subsubsection "permits access" 
   1.193 -constdefs 
   1.194 -permits_acc:: 
   1.195 - "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.196 -                   ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
   1.197 -
   1.198 +definition permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60) where
   1.199  "G\<turnstile>membr in cls permits_acc_from accclass 
   1.200    \<equiv> (case (accmodi membr) of
   1.201         Private   \<Rightarrow> (declclass membr = accclass)
   1.202 @@ -980,7 +960,7 @@
   1.203    next
   1.204      case (Inherited n C S)
   1.205      assume undecl: "G\<turnstile> memberid n undeclared_in C"
   1.206 -    assume  super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S"
   1.207 +    assume  super: "G\<turnstile>C\<prec>\<^sub>C1S"
   1.208      assume    hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m"
   1.209      assume   eqid: "memberid n = memberid m"
   1.210      assume "G \<turnstile> m member_of C"
   1.211 @@ -1011,7 +991,7 @@
   1.212         (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
   1.213  next
   1.214    case (Inherited m C S)  
   1.215 -  assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S"
   1.216 +  assume "G\<turnstile>C\<prec>\<^sub>C1S" and "is_class G S"
   1.217    then show "is_class G C"
   1.218      by - (rule subcls_is_class2,auto)
   1.219  qed
   1.220 @@ -1043,7 +1023,7 @@
   1.221          intro: rtrancl_trans)
   1.222  
   1.223  lemma stat_override_declclasses_relation: 
   1.224 -"\<lbrakk>G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew; G \<turnstile>Method old member_of superNew \<rbrakk>
   1.225 +"\<lbrakk>G\<turnstile>(declclass new) \<prec>\<^sub>C1 superNew; G \<turnstile>Method old member_of superNew \<rbrakk>
   1.226  \<Longrightarrow> G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old)"
   1.227  apply (rule trancl_rtrancl_trancl)
   1.228  apply (erule r_into_trancl)
   1.229 @@ -1257,7 +1237,7 @@
   1.230              "G\<turnstile> memberid m undeclared_in D"  
   1.231              "G \<turnstile> Class S accessible_in pid D" 
   1.232              "G \<turnstile> m member_of S"
   1.233 -    assume super: "G\<turnstile>D\<prec>\<^sub>C\<^sub>1S"
   1.234 +    assume super: "G\<turnstile>D\<prec>\<^sub>C1S"
   1.235      assume hyp: "\<lbrakk>G\<turnstile>S\<preceq>\<^sub>C C; G\<turnstile>C\<preceq>\<^sub>C declclass m\<rbrakk> \<Longrightarrow> G \<turnstile> m member_of C"
   1.236      assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m"
   1.237      assume "G\<turnstile>D\<preceq>\<^sub>C C"
   1.238 @@ -1399,24 +1379,21 @@
   1.239  translations 
   1.240    "fspec" <= (type) "vname \<times> qtname" 
   1.241  
   1.242 -constdefs
   1.243 -imethds:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables"
   1.244 +definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   1.245  "imethds G I 
   1.246    \<equiv> iface_rec (G,I)  
   1.247                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
   1.248                          (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
   1.249  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
   1.250  
   1.251 -constdefs
   1.252 -accimethds:: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables"
   1.253 +definition accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   1.254  "accimethds G pack I
   1.255    \<equiv> if G\<turnstile>Iface I accessible_in pack 
   1.256         then imethds G I
   1.257         else \<lambda> k. {}"
   1.258  text {* only returns imethds if the interface is accessible *}
   1.259  
   1.260 -constdefs
   1.261 -methd:: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table"
   1.262 +definition methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
   1.263  
   1.264  "methd G C 
   1.265   \<equiv> class_rec (G,C) empty
   1.266 @@ -1431,8 +1408,7 @@
   1.267       Every new method with the same signature coalesces the
   1.268       method of a superclass. *}
   1.269  
   1.270 -constdefs                      
   1.271 -accmethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table"
   1.272 +definition accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
   1.273  "accmethd G S C 
   1.274   \<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) 
   1.275                (methd G C)"
   1.276 @@ -1446,8 +1422,7 @@
   1.277      So we must test accessibility of method @{term m} of class @{term C} 
   1.278      (not @{term "declclass m"}) *}
   1.279  
   1.280 -constdefs 
   1.281 -dynmethd:: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
   1.282 +definition dynmethd :: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   1.283  "dynmethd G statC dynC  
   1.284    \<equiv> \<lambda> sig. 
   1.285       (if G\<turnstile>dynC \<preceq>\<^sub>C statC
   1.286 @@ -1473,8 +1448,7 @@
   1.287          filters the new methods (to get only those methods which actually
   1.288          override the methods of the static class) *}
   1.289  
   1.290 -constdefs 
   1.291 -dynimethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
   1.292 +definition dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   1.293  "dynimethd G I dynC 
   1.294    \<equiv> \<lambda> sig. if imethds G I sig \<noteq> {}
   1.295                 then methd G dynC sig
   1.296 @@ -1493,8 +1467,7 @@
   1.297     down to the actual dynamic class.
   1.298   *}
   1.299  
   1.300 -constdefs
   1.301 -dynlookup::"prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
   1.302 +definition dynlookup :: "prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
   1.303  "dynlookup G statT dynC
   1.304    \<equiv> (case statT of
   1.305         NullT        \<Rightarrow> empty
   1.306 @@ -1506,8 +1479,7 @@
   1.307      In a wellformd context statT will not be NullT and in case
   1.308      statT is an array type, dynC=Object *}
   1.309  
   1.310 -constdefs
   1.311 -fields:: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list"
   1.312 +definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
   1.313  "fields G C 
   1.314    \<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
   1.315  text {* @{term "fields G C"} 
   1.316 @@ -1515,8 +1487,7 @@
   1.317       (private, inherited and hidden ones) not only the accessible ones
   1.318       (an instance of a object allocates all these fields *}
   1.319  
   1.320 -constdefs
   1.321 -accfield:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table"
   1.322 +definition accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table" where
   1.323  "accfield G S C
   1.324    \<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
   1.325      in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
   1.326 @@ -1531,12 +1502,10 @@
   1.327     inheritance, too. So we must test accessibility of field @{term f} of class 
   1.328     @{term C} (not @{term "declclass f"}) *} 
   1.329  
   1.330 -constdefs
   1.331 -
   1.332 -  is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool"
   1.333 +definition is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool" where
   1.334   "is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None"
   1.335  
   1.336 -constdefs efname:: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
   1.337 +definition efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)" where
   1.338  "efname \<equiv> fst"
   1.339  
   1.340  lemma efname_simp[simp]:"efname (n,f) = n"
   1.341 @@ -2300,8 +2269,7 @@
   1.342  
   1.343  section "calculation of the superclasses of a class"
   1.344  
   1.345 -constdefs 
   1.346 - superclasses:: "prog \<Rightarrow> qtname \<Rightarrow> qtname set"
   1.347 +definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
   1.348   "superclasses G C \<equiv> class_rec (G,C) {} 
   1.349                         (\<lambda> C c superclss. (if C=Object 
   1.350                                              then {}