src/HOL/Bali/WellForm.thy
changeset 37956 ee939247b2fb
parent 37678 0040bafffdef
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Bali/WellForm.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -31,8 +31,9 @@
     1.4  text  {* well-formed field declaration (common part for classes and interfaces),
     1.5          cf. 8.3 and (9.3) *}
     1.6  
     1.7 -definition wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" where
     1.8 - "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
     1.9 +definition
    1.10 +  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
    1.11 +  where "wf_fdecl G P = (\<lambda>(fn,f). is_acc_type G P (type f))"
    1.12  
    1.13  lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    1.14  apply (unfold wf_fdecl_def)
    1.15 @@ -54,11 +55,12 @@
    1.16  \item the parameter names are unique
    1.17  \end{itemize} 
    1.18  *}
    1.19 -definition wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
    1.20 - "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
    1.21 +definition
    1.22 +  wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
    1.23 +  "wf_mhead G P = (\<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
    1.24                              \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
    1.25                              is_acc_type G P (resTy mh) \<and>
    1.26 -                            \<spacespace> distinct (pars mh)"
    1.27 +                            \<spacespace> distinct (pars mh))"
    1.28  
    1.29  
    1.30  text {*
    1.31 @@ -76,23 +78,25 @@
    1.32  \end{itemize}
    1.33  *}
    1.34  
    1.35 -definition callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
    1.36 -"callee_lcl C sig m 
    1.37 - \<equiv> \<lambda> k. (case k of
    1.38 +definition
    1.39 +  callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
    1.40 +  "callee_lcl C sig m =
    1.41 +    (\<lambda>k. (case k of
    1.42              EName e 
    1.43              \<Rightarrow> (case e of 
    1.44                    VNam v 
    1.45                    \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
    1.46                  | Res \<Rightarrow> Some (resTy m))
    1.47 -          | This \<Rightarrow> if is_static m then None else Some (Class C))"
    1.48 +          | This \<Rightarrow> if is_static m then None else Some (Class C)))"
    1.49  
    1.50 -definition parameters :: "methd \<Rightarrow> lname set" where
    1.51 -"parameters m \<equiv>  set (map (EName \<circ> VNam) (pars m)) 
    1.52 -                  \<union> (if (static m) then {} else {This})"
    1.53 +definition
    1.54 +  parameters :: "methd \<Rightarrow> lname set" where
    1.55 +  "parameters m = set (map (EName \<circ> VNam) (pars m)) \<union> (if (static m) then {} else {This})"
    1.56  
    1.57 -definition wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
    1.58 - "wf_mdecl G C \<equiv> 
    1.59 -      \<lambda>(sig,m).
    1.60 +definition
    1.61 +  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
    1.62 +  "wf_mdecl G C =
    1.63 +      (\<lambda>(sig,m).
    1.64            wf_mhead G (pid C) sig (mhead m) \<and> 
    1.65            unique (lcls (mbody m)) \<and> 
    1.66            (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
    1.67 @@ -102,7 +106,7 @@
    1.68            \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and>
    1.69            (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 
    1.70                  \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 
    1.71 -               \<and> Result \<in> nrm A)"
    1.72 +               \<and> Result \<in> nrm A))"
    1.73  
    1.74  lemma callee_lcl_VNam_simp [simp]:
    1.75  "callee_lcl C sig m (EName (VNam v)) 
    1.76 @@ -216,9 +220,10 @@
    1.77        superinterfaces widens to each of the corresponding result types
    1.78  \end{itemize}
    1.79  *}
    1.80 -definition wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
    1.81 - "wf_idecl G \<equiv> 
    1.82 -    \<lambda>(I,i). 
    1.83 +definition
    1.84 +  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
    1.85 + "wf_idecl G =
    1.86 +    (\<lambda>(I,i). 
    1.87          ws_idecl G I (isuperIfs i) \<and> 
    1.88          \<not>is_class G I \<and>
    1.89          (\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
    1.90 @@ -233,7 +238,7 @@
    1.91                               is_static new = is_static old)) \<and> 
    1.92          (Option.set \<circ> table_of (imethods i) 
    1.93                 hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
    1.94 -               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
    1.95 +               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
    1.96  
    1.97  lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>  
    1.98    wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
    1.99 @@ -317,8 +322,9 @@
   1.100  \end{itemize}
   1.101  *}
   1.102  (* to Table *)
   1.103 -definition entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) where
   1.104 -"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
   1.105 +definition
   1.106 +  entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20)
   1.107 +  where "(t entails P) = (\<forall>k. \<forall> x \<in> t k: P x)"
   1.108  
   1.109  lemma entailsD:
   1.110   "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
   1.111 @@ -327,9 +333,10 @@
   1.112  lemma empty_entails[simp]: "empty entails P"
   1.113  by (simp add: entails_def)
   1.114  
   1.115 -definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
   1.116 -"wf_cdecl G \<equiv> 
   1.117 -   \<lambda>(C,c).
   1.118 +definition
   1.119 +  wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
   1.120 +  "wf_cdecl G =
   1.121 +     (\<lambda>(C,c).
   1.122        \<not>is_iface G C \<and>
   1.123        (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
   1.124          (\<forall>s. \<forall> im \<in> imethds G I s.
   1.125 @@ -352,7 +359,7 @@
   1.126                         (G,sig\<turnstile>new hides old 
   1.127                           \<longrightarrow> (accmodi old \<le> accmodi new \<and>
   1.128                                is_static old)))) 
   1.129 -            ))"
   1.130 +            )))"
   1.131  
   1.132  (*
   1.133  definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
   1.134 @@ -511,13 +518,14 @@
   1.135  \item all defined classes are wellformed
   1.136  \end{itemize}
   1.137  *}
   1.138 -definition wf_prog :: "prog \<Rightarrow> bool" where
   1.139 - "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
   1.140 +definition
   1.141 +  wf_prog :: "prog \<Rightarrow> bool" where
   1.142 + "wf_prog G = (let is = ifaces G; cs = classes G in
   1.143                   ObjectC \<in> set cs \<and> 
   1.144                  (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
   1.145                  (\<forall>xn. SXcptC xn \<in> set cs) \<and>
   1.146                  (\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
   1.147 -                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
   1.148 +                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs)"
   1.149  
   1.150  lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
   1.151  apply (unfold wf_prog_def Let_def)
   1.152 @@ -2095,16 +2103,16 @@
   1.153   Class    dynC 
   1.154   Array    Object
   1.155  *}
   1.156 -consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
   1.157 +primrec valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
   1.158                          ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
   1.159 -primrec
   1.160 -"G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
   1.161 -"G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
   1.162 -              = (if static_membr 
   1.163 -                    then dynC=Object 
   1.164 -                    else G\<turnstile>Class dynC\<preceq> Iface I)"
   1.165 -"G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
   1.166 -"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
   1.167 +where
   1.168 +  "G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
   1.169 +| "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
   1.170 +                = (if static_membr 
   1.171 +                      then dynC=Object 
   1.172 +                      else G\<turnstile>Class dynC\<preceq> Iface I)"
   1.173 +| "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
   1.174 +| "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
   1.175  
   1.176  lemma valid_lookup_cls_is_class:
   1.177    assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and