src/HOL/Bali/DeclConcepts.thy
changeset 35067 af4c18c30593
parent 34990 81e8fdfeb849
child 35315 fbdc860d87a3
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Feb 09 16:07:09 2010 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Feb 10 00:45:16 2010 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4  "is_public G qn \<equiv> (case class G qn of
     1.5                       None       \<Rightarrow> (case iface G qn of
     1.6                                        None       \<Rightarrow> False
     1.7 -                                    | Some iface \<Rightarrow> access iface = Public)
     1.8 -                   | Some class \<Rightarrow> access class = Public)"
     1.9 +                                    | Some i \<Rightarrow> access i = Public)
    1.10 +                   | Some c \<Rightarrow> access c = Public)"
    1.11  
    1.12  subsection "accessibility of types (cf. 6.6.1)"
    1.13  text {* 
    1.14 @@ -445,21 +445,17 @@
    1.15       | Protected \<Rightarrow> True
    1.16       | Public    \<Rightarrow> True)"
    1.17  
    1.18 -syntax
    1.19 -Method_inheritable_in::
    1.20 +abbreviation
    1.21 +Method_inheritable_in_syntax::
    1.22   "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"
    1.23                  ("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60)
    1.24 + where "G\<turnstile>Method m inheritable_in p == G\<turnstile>methdMembr m inheritable_in p"
    1.25  
    1.26 -translations
    1.27 -"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"
    1.28 -
    1.29 -syntax
    1.30 +abbreviation
    1.31  Methd_inheritable_in::
    1.32   "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
    1.33                  ("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
    1.34 -
    1.35 -translations
    1.36 -"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"
    1.37 + where "G\<turnstile>Methd s m inheritable_in p == G\<turnstile>(method s m) inheritable_in p"
    1.38  
    1.39  subsubsection "declared-in/undeclared-in"
    1.40  
    1.41 @@ -486,17 +482,15 @@
    1.42                          fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
    1.43                        | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
    1.44  
    1.45 -syntax
    1.46 +abbreviation
    1.47  method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    1.48                                   ("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)
    1.49 -translations
    1.50 -"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"
    1.51 + where "G\<turnstile>Method m declared_in C == G\<turnstile>mdecl (mthd m) declared_in C"
    1.52  
    1.53 -syntax
    1.54 +abbreviation
    1.55  methd_declared_in:: "prog  \<Rightarrow> sig  \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
    1.56                                 ("_\<turnstile>Methd _  _ declared'_in _" [61,61,61,61] 60)
    1.57 -translations
    1.58 -"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"
    1.59 + where "G\<turnstile>Methd s m declared_in C == G\<turnstile>mdecl (s,mthd m) declared_in C"
    1.60  
    1.61  lemma declared_in_classD:
    1.62   "G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
    1.63 @@ -538,26 +532,20 @@
    1.64  of S will not inherit the member, regardless if they are in the same
    1.65  package as A or not.*}
    1.66  
    1.67 -syntax
    1.68 +abbreviation
    1.69  method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
    1.70                             ("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)
    1.71 + where "G\<turnstile>Method m member_of C == G\<turnstile>(methdMembr m) member_of C"
    1.72  
    1.73 -translations
    1.74 - "G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" 
    1.75 -
    1.76 -syntax
    1.77 +abbreviation
    1.78  methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
    1.79                             ("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
    1.80 + where "G\<turnstile>Methd s m member_of C == G\<turnstile>(method s m) member_of C" 
    1.81  
    1.82 -translations
    1.83 - "G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" 
    1.84 -
    1.85 -syntax
    1.86 +abbreviation
    1.87  fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"
    1.88                             ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
    1.89 -
    1.90 -translations
    1.91 - "G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" 
    1.92 + where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
    1.93  
    1.94  constdefs
    1.95  inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
    1.96 @@ -578,19 +566,15 @@
    1.97  is necessary since not all members are inherited to subclasses. So such
    1.98  members are not member-of the subclass but member-in the subclass.*}
    1.99  
   1.100 -syntax
   1.101 +abbreviation
   1.102  method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   1.103                             ("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)
   1.104 + where "G\<turnstile>Method m member_in C == G\<turnstile>(methdMembr m) member_in C"
   1.105  
   1.106 -translations
   1.107 - "G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" 
   1.108 -
   1.109 -syntax
   1.110 +abbreviation
   1.111  methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   1.112                             ("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
   1.113 -
   1.114 -translations
   1.115 - "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 
   1.116 + where "G\<turnstile>Methd s m member_in C == G\<turnstile>(method s m) member_in C"
   1.117  
   1.118  lemma member_inD: "G\<turnstile>m member_in C 
   1.119   \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
   1.120 @@ -649,18 +633,16 @@
   1.121  | Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
   1.122              \<Longrightarrow> G\<turnstile>new overrides old"
   1.123  
   1.124 -syntax
   1.125 +abbreviation (input)
   1.126  sig_stat_overrides:: 
   1.127   "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   1.128                                    ("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
   1.129 -translations
   1.130 - "G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
   1.131 + where "G,s\<turnstile>new overrides\<^sub>S old == G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
   1.132  
   1.133 -syntax
   1.134 +abbreviation (input)
   1.135  sig_overrides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   1.136                                    ("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)
   1.137 -translations
   1.138 - "G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 
   1.139 + where "G,s\<turnstile>new overrides old == G\<turnstile>(qmdecl s new) overrides (qmdecl s old)"
   1.140  
   1.141  subsubsection "Hiding"
   1.142  
   1.143 @@ -674,11 +656,10 @@
   1.144      G\<turnstile>Method old declared_in (declclass old) \<and> 
   1.145      G\<turnstile>Method old inheritable_in pid (declclass new)"
   1.146  
   1.147 -syntax
   1.148 -sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
   1.149 +abbreviation
   1.150 +sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   1.151                                    ("_,_\<turnstile> _ hides _" [61,61,61,61] 60)
   1.152 -translations
   1.153 - "G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 
   1.154 + where "G,s\<turnstile>new hides old == G\<turnstile>(qmdecl s new) hides (qmdecl s old)"
   1.155  
   1.156  lemma hidesI:
   1.157  "\<lbrakk>is_static new; msig new = msig old;
   1.158 @@ -731,14 +712,14 @@
   1.159   "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.160                     ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
   1.161  
   1.162 -"G\<turnstile>membr in class permits_acc_from accclass 
   1.163 +"G\<turnstile>membr in cls permits_acc_from accclass 
   1.164    \<equiv> (case (accmodi membr) of
   1.165         Private   \<Rightarrow> (declclass membr = accclass)
   1.166       | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
   1.167       | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
   1.168                      \<or>
   1.169                      (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
   1.170 -                     \<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) 
   1.171 +                     \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr)) 
   1.172       | Public    \<Rightarrow> True)"
   1.173  text {*
   1.174  The subcondition of the @{term "Protected"} case: 
   1.175 @@ -774,12 +755,14 @@
   1.176  
   1.177  | "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls"
   1.178  
   1.179 -| Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
   1.180 +| Immediate:  "!!membr class.
   1.181 +               \<lbrakk>G\<turnstile>membr member_of class;
   1.182                  G\<turnstile>(Class class) accessible_in (pid accclass);
   1.183                  G\<turnstile>membr in class permits_acc_from accclass 
   1.184                 \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   1.185  
   1.186 -| Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
   1.187 +| Overriding: "!!membr class C new old supr.
   1.188 +               \<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 @@ -787,23 +770,21 @@
   1.193                  G\<turnstile>Method old of supr accessible_from accclass
   1.194                 \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   1.195  
   1.196 -syntax 
   1.197 +abbreviation
   1.198  methd_accessible_from:: 
   1.199   "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.200                   ("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
   1.201 + where
   1.202 + "G\<turnstile>Methd s m of cls accessible_from accclass ==
   1.203 +   G\<turnstile>(method s m) of cls accessible_from accclass"
   1.204  
   1.205 -translations
   1.206 -"G\<turnstile>Methd s m of cls accessible_from accclass"  
   1.207 - \<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"  
   1.208 -
   1.209 -syntax 
   1.210 +abbreviation
   1.211  field_accessible_from:: 
   1.212   "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.213                   ("_ \<turnstile>Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
   1.214 -
   1.215 -translations
   1.216 -"G\<turnstile>Field fn f of C accessible_from accclass"  
   1.217 - \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
   1.218 + where
   1.219 + "G\<turnstile>Field fn f of C accessible_from accclass ==
   1.220 +  G\<turnstile>(fieldm fn f) of C accessible_from accclass"
   1.221  
   1.222  inductive
   1.223    dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   1.224 @@ -817,34 +798,32 @@
   1.225  
   1.226  | "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C"
   1.227  
   1.228 -| Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
   1.229 +| Immediate:  "!!class. \<lbrakk>G\<turnstile>membr member_in class;
   1.230                  G\<turnstile>membr in class permits_acc_from accclass 
   1.231                 \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   1.232  
   1.233 -| Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
   1.234 +| Overriding: "!!class. \<lbrakk>G\<turnstile>membr member_in class;
   1.235                  membr=(C,mdecl new);
   1.236                  G\<turnstile>(C,new) overrides old; 
   1.237                  G\<turnstile>class \<prec>\<^sub>C supr;
   1.238                  G\<turnstile>Method old in supr dyn_accessible_from accclass
   1.239                 \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   1.240  
   1.241 -syntax 
   1.242 +abbreviation
   1.243  methd_dyn_accessible_from:: 
   1.244   "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.245               ("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   1.246 + where
   1.247 + "G\<turnstile>Methd s m in C dyn_accessible_from accC ==
   1.248 +  G\<turnstile>(method s m) in C dyn_accessible_from accC"  
   1.249  
   1.250 -translations
   1.251 -"G\<turnstile>Methd s m in C dyn_accessible_from accC"  
   1.252 - \<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"  
   1.253 -
   1.254 -syntax 
   1.255 +abbreviation
   1.256  field_dyn_accessible_from:: 
   1.257   "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.258           ("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   1.259 -
   1.260 -translations
   1.261 -"G\<turnstile>Field fn f in dynC dyn_accessible_from accC"  
   1.262 - \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
   1.263 + where
   1.264 + "G\<turnstile>Field fn f in dynC dyn_accessible_from accC ==
   1.265 +  G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
   1.266  
   1.267  
   1.268  lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S