src/HOL/Bali/DeclConcepts.thy
changeset 13688 a0b16d42d489
parent 13585 db4005b40cc6
child 14025 d9b155757dc8
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -153,10 +153,6 @@
     1.4  axclass has_static < "type"
     1.5  consts is_static :: "'a::has_static \<Rightarrow> bool"
     1.6  
     1.7 -(*
     1.8 -consts is_static :: "'a \<Rightarrow> bool"
     1.9 -*)
    1.10 -
    1.11  instance access_field_type :: ("type","has_static") has_static ..
    1.12  
    1.13  defs (overloaded)
    1.14 @@ -205,48 +201,31 @@
    1.15  lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
    1.16  by (cases m) (simp add: mhead_def member_is_static_simp)
    1.17  
    1.18 -constdefs  (* some mnemotic selectors for (qtname \<times> ('a::more) decl_scheme) 
    1.19 -            * the first component is a class or interface name
    1.20 -            * the second component is a method, field or method head *)
    1.21 -(* "declclass":: "(qtname \<times> ('a::more) decl_scheme) \<Rightarrow> qtname"*)
    1.22 -(* "declclass \<equiv> fst" *)          (* get the class component *)
    1.23 -
    1.24 +constdefs  --{* some mnemotic selectors for various pairs *} 
    1.25 +           
    1.26   "decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
    1.27 - "decliface \<equiv> fst"          (* get the interface component *)
    1.28 + "decliface \<equiv> fst"          --{* get the interface component *}
    1.29  
    1.30 -(*
    1.31 - "member"::   "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
    1.32 -*)
    1.33   "mbr"::   "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
    1.34 - "mbr \<equiv> snd"            (* get the memberdecl component *)
    1.35 + "mbr \<equiv> snd"            --{* get the memberdecl component *}
    1.36  
    1.37   "mthd"::   "('b \<times> 'a) \<Rightarrow> 'a"
    1.38 -                           (* also used for mdecl,mhead *)
    1.39 - "mthd \<equiv> snd"              (* get the method component *)
    1.40 +                           --{* also used for mdecl, mhead *}
    1.41 + "mthd \<equiv> snd"              --{* get the method component *}
    1.42  
    1.43   "fld"::   "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
    1.44 -              (* also used for ((vname \<times> qtname)\<times> field) *)
    1.45 - "fld \<equiv> snd"               (* get the field component *)
    1.46 +              --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
    1.47 + "fld \<equiv> snd"               --{* get the field component *}
    1.48  
    1.49 -(* "accmodi" :: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> acc_modi"*)
    1.50 -                           (* also used for mdecl *)
    1.51 -(* "accmodi \<equiv> access \<circ> snd"*)  (* get the access modifier *) 
    1.52 -(*
    1.53 - "is_static" ::"('b \<times> ('a::type) member_scheme) \<Rightarrow> bool" *)
    1.54 -                            (* also defined for emhead cf. WellType *)
    1.55 - (*"is_static \<equiv> static \<circ> snd"*) (* get the static modifier *)
    1.56  
    1.57 -constdefs (* some mnemotic selectors for (vname \<times> qtname) *)
    1.58 - fname:: "(vname \<times> 'a) \<Rightarrow> vname" (* also used for fdecl *)
    1.59 +constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
    1.60 + fname:: "(vname \<times> 'a) \<Rightarrow> vname" --{* also used for fdecl *}
    1.61   "fname \<equiv> fst"
    1.62    
    1.63    declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
    1.64   "declclassf \<equiv> snd"
    1.65  
    1.66 -(*
    1.67 -lemma declclass_simp[simp]: "declclass (C,m) = C"
    1.68 -by (simp add: declclass_def)
    1.69 -*)
    1.70 +
    1.71  
    1.72  lemma decliface_simp[simp]: "decliface (I,m) = I"
    1.73  by (simp add: decliface_def) 
    1.74 @@ -272,11 +251,6 @@
    1.75  lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f"
    1.76  by (cases f) (simp add:  fld_def) 
    1.77  
    1.78 -(*
    1.79 -lemma is_static_simp[simp]: "is_static (C,m) = static m"
    1.80 -by (simp add: is_static_def)
    1.81 -*)
    1.82 -
    1.83  lemma static_mthd_simp[simp]: "static (mthd m) = is_static m"
    1.84  by (cases m) (simp add:  mthd_def member_is_static_simp)
    1.85  
    1.86 @@ -301,7 +275,7 @@
    1.87  lemma declclassf_simp[simp]:"declclassf (n,c) = c"
    1.88  by (simp add: declclassf_def)
    1.89  
    1.90 -constdefs  (* some mnemotic selectors for (vname \<times> qtname) *)
    1.91 +constdefs  --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
    1.92    "fldname"  :: "(vname \<times> qtname) \<Rightarrow> vname" 
    1.93    "fldname \<equiv> fst"
    1.94  
    1.95 @@ -1265,6 +1239,7 @@
    1.96    qed
    1.97  qed
    1.98  *)
    1.99 +
   1.100  lemma accessible_fieldD: 
   1.101   "\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>
   1.102   \<Longrightarrow> G\<turnstile>membr member_of C \<and>
   1.103 @@ -1272,34 +1247,7 @@
   1.104       G\<turnstile>membr in C permits_acc_to accC"
   1.105  by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
   1.106        
   1.107 -(* lemmata:
   1.108 - Wegen  G\<turnstile>Super accessible_in (pid C) folgt:
   1.109 -  G\<turnstile>m declared_in C; G\<turnstile>m member_of D; accmodi m = Package (G\<turnstile>D \<preceq>\<^sub>C C)
   1.110 -  \<Longrightarrow> pid C = pid D 
   1.111  
   1.112 -  C package
   1.113 -  m public in C
   1.114 -  für alle anderen D: G\<turnstile>m undeclared_in C
   1.115 -  m wird in alle subklassen vererbt, auch aus dem Package heraus!
   1.116 -
   1.117 -  G\<turnstile>m member_of C \<Longrightarrow> \<exists> D. G\<turnstile>C \<preceq>\<^sub>C D \<and> G\<turnstile>m declared_in D
   1.118 -*)
   1.119 -
   1.120 -(* Begriff (C,m) overrides (D,m)
   1.121 -    3 Fälle: Direkt,
   1.122 -             Indirekt über eine Zwischenklasse (ohne weiteres override)
   1.123 -             Indirekt über override
   1.124 -*)
   1.125 -   
   1.126 -(*
   1.127 -"G\<turnstile>m member_of C \<equiv> 
   1.128 -constdefs declares_method:: "prog \<Rightarrow> sig \<Rightarrow> qtname \<Rightarrow> methd \<Rightarrow> bool"
   1.129 -                                 ("_,_\<turnstile> _ declares'_method _" [61,61,61,61] 60)
   1.130 -"G,sig\<turnstile>C declares_method m \<equiv> cdeclaredmethd G C sig = Some m" 
   1.131 -
   1.132 -constdefs is_declared:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"
   1.133 -"is_declared G sig em \<equiv> G,sig\<turnstile>declclass em declares_method mthd em"
   1.134 -*)
   1.135  
   1.136  lemma member_of_Private:
   1.137  "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C"
   1.138 @@ -1541,23 +1489,7 @@
   1.139                        ) sig
   1.140                )
   1.141          else None)"
   1.142 -(*
   1.143 -"dynmethd G statC dynC  
   1.144 -  \<equiv> \<lambda> sig. 
   1.145 -     (if G\<turnstile>dynC \<preceq>\<^sub>C statC
   1.146 -        then (case methd G statC sig of
   1.147 -                None \<Rightarrow> None
   1.148 -              | Some statM 
   1.149 -                    \<Rightarrow> (class_rec (G,statC) empty
   1.150 -                         (\<lambda>C c subcls_mthds. 
   1.151 -                            subcls_mthds
   1.152 -                            ++
   1.153 -                            (filter_tab 
   1.154 -                              (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM)  
   1.155 -                              (table_of (map (\<lambda>(s,m). (s,C,m)) (methods c)))))
   1.156 -                        ) sig
   1.157 -              )
   1.158 -        else None)"*)
   1.159 +
   1.160  text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference 
   1.161          with dynamic class @{term dynC} and static class @{term statC} *}
   1.162  text {* Note some kind of duality between @{term methd} and @{term dynmethd} 
   1.163 @@ -2014,8 +1946,6 @@
   1.164  lemma dynmethdSomeD: 
   1.165   "\<lbrakk>dynmethd G statC dynC sig = Some dynM; is_class G dynC; ws_prog G\<rbrakk> 
   1.166    \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C statC \<and> (\<exists> statM. methd G statC sig = Some statM)"
   1.167 -apply clarify
   1.168 -apply rotate_tac
   1.169  by (auto simp add: dynmethd_rec)
   1.170   
   1.171  lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
   1.172 @@ -2243,31 +2173,6 @@
   1.173    qed
   1.174  qed
   1.175  
   1.176 -(*
   1.177 -lemma dom_dynmethd: 
   1.178 -  "dom (dynmethd G statC dynC) \<subseteq> dom (methd G statC) \<union> dom (methd G dynC)"
   1.179 -by (auto simp add: dynmethd_def dom_def)
   1.180 -
   1.181 -lemma finite_dom_dynmethd:
   1.182 - "\<lbrakk>ws_prog G; is_class G statC; is_class G dynC\<rbrakk> 
   1.183 -  \<Longrightarrow> finite (dom (dynmethd G statC dynC))"
   1.184 -apply (rule_tac B="dom (methd G statC) \<union> dom (methd G dynC)" in finite_subset)
   1.185 -apply (rule dom_dynmethd)
   1.186 -apply (rule finite_UnI)
   1.187 -apply (drule (2) finite_dom_methd)+
   1.188 -done
   1.189 -*)
   1.190 -(*
   1.191 -lemma dynmethd_SomeD: 
   1.192 -"\<lbrakk>ws_prog G; is_class G statC; is_class G dynC;
   1.193 - methd G statC sig = Some sm; dynmethd G statC dynC sig = Some dm; sm \<noteq> dm
   1.194 - \<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<prec>\<^sub>C statC \<and> 
   1.195 -       (declclass dm \<noteq> dynC \<longrightarrow> G \<turnstile> dm accessible_through_inheritance_in dynC)"
   1.196 -by (auto simp add: dynmethd_def 
   1.197 -         dest: methd_inheritedD methd_diff_cls
   1.198 -         intro: rtrancl_into_trancl3)
   1.199 -*)
   1.200 -
   1.201  subsection "dynlookup"
   1.202  
   1.203  lemma dynlookup_cases [consumes 1, case_names NullT IfaceT ClassT ArrayT]: