src/HOL/Bali/WellForm.thy
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 14025 d9b155757dc8
     1.1 --- a/src/HOL/Bali/WellForm.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -5,8 +5,7 @@
     1.4  *)
     1.5  
     1.6  header {* Well-formedness of Java programs *}
     1.7 -
     1.8 -theory WellForm = WellType:
     1.9 +theory WellForm = DefiniteAssignment:
    1.10  
    1.11  text {*
    1.12  For static checks on expressions and statements, see WellType.thy
    1.13 @@ -81,6 +80,20 @@
    1.14  \end{itemize}
    1.15  *}
    1.16  
    1.17 +constdefs callee_lcl:: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv"
    1.18 +"callee_lcl C sig m 
    1.19 + \<equiv> \<lambda> k. (case k of
    1.20 +            EName e 
    1.21 +            \<Rightarrow> (case e of 
    1.22 +                  VNam v 
    1.23 +                  \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
    1.24 +                | Res \<Rightarrow> Some (resTy m))
    1.25 +	  | This \<Rightarrow> if is_static m then None else Some (Class C))"
    1.26 +
    1.27 +constdefs parameters :: "methd \<Rightarrow> lname set"
    1.28 +"parameters m \<equiv>  set (map (EName \<circ> VNam) (pars m)) 
    1.29 +                  \<union> (if (static m) then {} else {This})"
    1.30 +
    1.31  constdefs
    1.32    wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool"
    1.33   "wf_mdecl G C \<equiv> 
    1.34 @@ -89,17 +102,33 @@
    1.35            unique (lcls (mbody m)) \<and> 
    1.36            (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
    1.37  	  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and>
    1.38 +          jumpNestingOkS {Ret} (stmt (mbody m)) \<and> 
    1.39            is_class G C \<and>
    1.40 -          \<lparr>prg=G,cls=C,
    1.41 -           lcl=\<lambda> k. 
    1.42 -               (case k of
    1.43 -                  EName e 
    1.44 -                  \<Rightarrow> (case e of 
    1.45 -                        VNam v 
    1.46 -                        \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
    1.47 -                      | Res \<Rightarrow> Some (resTy m))
    1.48 -	        | This \<Rightarrow> if is_static m then None else Some (Class C))
    1.49 -          \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>"
    1.50 +          \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and>
    1.51 +          (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 
    1.52 +                \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 
    1.53 +               \<and> Result \<in> nrm A)"
    1.54 +
    1.55 +lemma callee_lcl_VNam_simp [simp]:
    1.56 +"callee_lcl C sig m (EName (VNam v)) 
    1.57 +  = (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v"
    1.58 +by (simp add: callee_lcl_def)
    1.59 + 
    1.60 +lemma callee_lcl_Res_simp [simp]:
    1.61 +"callee_lcl C sig m (EName Res) = Some (resTy m)" 
    1.62 +by (simp add: callee_lcl_def)
    1.63 +
    1.64 +lemma callee_lcl_This_simp [simp]:
    1.65 +"callee_lcl C sig m (This) = (if is_static m then None else Some (Class C))" 
    1.66 +by (simp add: callee_lcl_def)
    1.67 +
    1.68 +lemma callee_lcl_This_static_simp:
    1.69 +"is_static m \<Longrightarrow> callee_lcl C sig m (This) = None"
    1.70 +by simp
    1.71 +
    1.72 +lemma callee_lcl_This_not_static_simp:
    1.73 +"\<not> is_static m \<Longrightarrow> callee_lcl C sig m (This) = Some (Class C)"
    1.74 +by simp
    1.75  
    1.76  lemma wf_mheadI: 
    1.77  "\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T;
    1.78 @@ -113,23 +142,31 @@
    1.79    wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
    1.80    (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 
    1.81    \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T;
    1.82 +  jumpNestingOkS {Ret} (stmt (mbody m));
    1.83    is_class G C;
    1.84 -  \<lparr>prg=G,cls=C,
    1.85 -   lcl=\<lambda> k. 
    1.86 -       (case k of
    1.87 -          EName e 
    1.88 -          \<Rightarrow> (case e of 
    1.89 -                VNam v 
    1.90 -                \<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
    1.91 -              | Res \<Rightarrow> Some (resTy m))
    1.92 -        | This \<Rightarrow> if is_static m then None else Some (Class C))
    1.93 -  \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>
    1.94 +  \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>;
    1.95 +  (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A
    1.96 +        \<and> Result \<in> nrm A)
    1.97    \<rbrakk> \<Longrightarrow>  
    1.98    wf_mdecl G C (sig,m)"
    1.99  apply (unfold wf_mdecl_def)
   1.100  apply simp
   1.101  done
   1.102  
   1.103 +lemma wf_mdeclE [consumes 1]:  
   1.104 +  "\<lbrakk>wf_mdecl G C (sig,m); 
   1.105 +    \<lbrakk>wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
   1.106 +     \<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None; 
   1.107 +     \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T;
   1.108 +     jumpNestingOkS {Ret} (stmt (mbody m));
   1.109 +     is_class G C;
   1.110 +     \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>;
   1.111 +   (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A
   1.112 +        \<and> Result \<in> nrm A)
   1.113 +    \<rbrakk> \<Longrightarrow> P
   1.114 +  \<rbrakk> \<Longrightarrow> P"
   1.115 +by (unfold wf_mdecl_def) simp
   1.116 +
   1.117  
   1.118  lemma wf_mdeclD1: 
   1.119  "wf_mdecl G C (sig,m) \<Longrightarrow>  
   1.120 @@ -137,20 +174,13 @@
   1.121    (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 
   1.122    (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)"
   1.123  apply (unfold wf_mdecl_def)
   1.124 -apply auto
   1.125 +apply simp
   1.126  done
   1.127  
   1.128  lemma wf_mdecl_bodyD: 
   1.129  "wf_mdecl G C (sig,m) \<Longrightarrow>  
   1.130 - (\<exists>T. \<lparr>prg=G,cls=C,
   1.131 -       lcl = \<lambda> k. 
   1.132 -         (case k of
   1.133 -            EName e 
   1.134 -            \<Rightarrow> (case e of 
   1.135 -                VNam v \<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   1.136 -                | Res  \<Rightarrow> Some (resTy m))
   1.137 -          | This \<Rightarrow> if is_static m then None else Some (Class C))
   1.138 -       \<rparr>\<turnstile>Body C (stmt (mbody m))\<Colon>-T \<and> G\<turnstile>T\<preceq>(resTy m))"
   1.139 + (\<exists>T. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>Body C (stmt (mbody m))\<Colon>-T \<and> 
   1.140 +      G\<turnstile>T\<preceq>(resTy m))"
   1.141  apply (unfold wf_mdecl_def)
   1.142  apply clarify
   1.143  apply (rule_tac x="(resTy m)" in exI)
   1.144 @@ -315,7 +345,9 @@
   1.145        	                             \<not> is_static cm \<and>
   1.146                                       accmodi im \<le> accmodi cm))) \<and>
   1.147        (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 
   1.148 -      (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 
   1.149 +      (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and>
   1.150 +      jumpNestingOkS {} (init c) \<and>
   1.151 +      (\<exists> A. \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A) \<and>
   1.152        \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
   1.153        (C \<noteq> Object \<longrightarrow> 
   1.154              (is_acc_class G (pid C) (super c) \<and>
   1.155 @@ -362,6 +394,35 @@
   1.156                entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))"
   1.157  *)
   1.158  
   1.159 +lemma wf_cdeclE [consumes 1]: 
   1.160 + "\<lbrakk>wf_cdecl G (C,c);
   1.161 +   \<lbrakk>\<not>is_iface G C;
   1.162 +    (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
   1.163 +        (\<forall>s. \<forall> im \<in> imethds G I s.
   1.164 +      	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and>
   1.165 +      	                             \<not> is_static cm \<and>
   1.166 +                                     accmodi im \<le> accmodi cm))); 
   1.167 +      \<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f; unique (cfields c); 
   1.168 +      \<forall>m\<in>set (methods c). wf_mdecl G C m; unique (methods c);
   1.169 +      jumpNestingOkS {} (init c);
   1.170 +      \<exists> A. \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A;
   1.171 +      \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>; 
   1.172 +      ws_cdecl G C (super c); 
   1.173 +      (C \<noteq> Object \<longrightarrow> 
   1.174 +            (is_acc_class G (pid C) (super c) \<and>
   1.175 +            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   1.176 +             entails (\<lambda> new. \<forall> old sig. 
   1.177 +                       (G,sig\<turnstile>new overrides\<^sub>S old 
   1.178 +                        \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
   1.179 +                             accmodi old \<le> accmodi new \<and>
   1.180 +      	                     \<not>is_static old)) \<and>
   1.181 +                       (G,sig\<turnstile>new hides old 
   1.182 +                         \<longrightarrow> (accmodi old \<le> accmodi new \<and>
   1.183 +      	                      is_static old)))) 
   1.184 +            ))\<rbrakk> \<Longrightarrow> P
   1.185 +  \<rbrakk> \<Longrightarrow> P"
   1.186 +by (unfold wf_cdecl_def) simp
   1.187 +
   1.188  lemma wf_cdecl_unique: 
   1.189  "wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)"
   1.190  apply (unfold wf_cdecl_def)
   1.191 @@ -535,7 +596,7 @@
   1.192  	"wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls)
   1.193    (wf_mdecl G Object) \<and> unique Object_mdecls)"
   1.194  apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def)
   1.195 -apply (simp (no_asm))
   1.196 +apply (auto intro: da.Skip)
   1.197  done
   1.198  
   1.199  lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object"
   1.200 @@ -1691,19 +1752,7 @@
   1.201                 intro: order_trans)
   1.202    qed
   1.203  qed
   1.204 - 	  
   1.205 -(* ### Probleme: Die tollen methd_subcls_cases Lemma wird warscheinlich
   1.206 -  kaum gebraucht: 
   1.207 -Redundanz: stat_overrides.Direct old declared in declclass old folgt aus
   1.208 -           member of 
   1.209 -   Problem: Predikate wie overrides, sind global üper die Hierarchie hinweg
   1.210 -            definiert, aber oft barucht man eben zusätlich Induktion
   1.211 -            : von super c auf C; Dann ist aber auss dem Kontext
   1.212 -            die Unterscheidung in die 5 fälle overkill,
   1.213 -            da man dann warscheinlich meistens eh in einem speziellen
   1.214 -            Fall kommt (durch die Hypothesen)
   1.215 -*)
   1.216 -    
   1.217 + 	      
   1.218  (* local lemma *)
   1.219  ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
   1.220  ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
   1.221 @@ -2419,7 +2468,7 @@
   1.222  apply (auto split del: split_if_asm simp del: snd_conv 
   1.223              simp add: is_acc_class_def is_acc_type_def)
   1.224  apply    (erule typeof_empty_is_type)
   1.225 -apply   (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], rotate_tac -1, 
   1.226 +apply   (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], 
   1.227          force simp del: snd_conv, clarsimp simp add: is_acc_class_def)
   1.228  apply  (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD])
   1.229  apply  (drule_tac [2] accfield_fields) 
   1.230 @@ -2476,16 +2525,7 @@
   1.231  "\<lbrakk>methd G C sig = Some m; wf_prog G;  
   1.232    class G C = Some c\<rbrakk> \<Longrightarrow>  
   1.233   \<exists>T. \<lparr>prg=G,cls=(declclass m),
   1.234 -      lcl=\<lambda> k. 
   1.235 -          (case k of
   1.236 -             EName e 
   1.237 -             \<Rightarrow> (case e of 
   1.238 -                   VNam v 
   1.239 -                   \<Rightarrow> (table_of (lcls (mbody (mthd m)))
   1.240 -                                ((pars (mthd m))[\<mapsto>](parTs sig))) v
   1.241 -                 | Res \<Rightarrow> Some (resTy (mthd m)))
   1.242 -           | This \<Rightarrow> if is_static m then None else Some (Class (declclass m)))
   1.243 -     \<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m"
   1.244 +      lcl=callee_lcl (declclass m) sig (mthd m)\<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m"
   1.245  apply (frule (2) methd_wf_mdecl, clarify)
   1.246  apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd)
   1.247  done