src/HOL/Bali/Decl.thy
changeset 37956 ee939247b2fb
parent 37678 0040bafffdef
child 41525 a42cbf5b44c8
     1.1 --- a/src/HOL/Bali/Decl.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/Decl.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -206,8 +206,9 @@
     1.4    (type) "mdecl" <= (type) "sig \<times> methd"
     1.5  
     1.6  
     1.7 -definition mhead :: "methd \<Rightarrow> mhead" where
     1.8 -  "mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
     1.9 +definition
    1.10 +  mhead :: "methd \<Rightarrow> mhead"
    1.11 +  where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
    1.12  
    1.13  lemma access_mhead [simp]:"access (mhead m) = access m"
    1.14  by (simp add: mhead_def)
    1.15 @@ -237,7 +238,7 @@
    1.16  
    1.17  definition
    1.18  memberdecl_memberid_def:
    1.19 -  "memberid m \<equiv> (case m of
    1.20 +  "memberid m = (case m of
    1.21                      fdecl (vn,f)  \<Rightarrow> fid vn
    1.22                    | mdecl (sig,m) \<Rightarrow> mid sig)"
    1.23  
    1.24 @@ -262,7 +263,7 @@
    1.25  
    1.26  definition
    1.27  pair_memberid_def:
    1.28 -  "memberid p \<equiv> memberid (snd p)"
    1.29 +  "memberid p = memberid (snd p)"
    1.30  
    1.31  instance ..
    1.32  
    1.33 @@ -274,8 +275,9 @@
    1.34  lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
    1.35  by (simp add: pair_memberid_def)
    1.36  
    1.37 -definition is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" where
    1.38 -"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
    1.39 +definition
    1.40 +  is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
    1.41 +  where "is_field m = (\<exists> declC f. m=(declC,fdecl f))"
    1.42    
    1.43  lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
    1.44  by (simp add: is_field_def)
    1.45 @@ -283,8 +285,9 @@
    1.46  lemma is_fieldI: "is_field (C,fdecl f)"
    1.47  by (simp add: is_field_def)
    1.48  
    1.49 -definition is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" where
    1.50 -"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
    1.51 +definition
    1.52 +  is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
    1.53 +  where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))"
    1.54    
    1.55  lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
    1.56  by (simp add: is_method_def)
    1.57 @@ -314,8 +317,9 @@
    1.58                        isuperIfs::qtname list,\<dots>::'a\<rparr>"
    1.59    (type) "idecl" <= (type) "qtname \<times> iface"
    1.60  
    1.61 -definition ibody :: "iface \<Rightarrow> ibody" where
    1.62 -  "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
    1.63 +definition
    1.64 +  ibody :: "iface \<Rightarrow> ibody"
    1.65 +  where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>"
    1.66  
    1.67  lemma access_ibody [simp]: "(access (ibody i)) = access i"
    1.68  by (simp add: ibody_def)
    1.69 @@ -349,8 +353,9 @@
    1.70                        super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
    1.71    (type) "cdecl" <= (type) "qtname \<times> class"
    1.72  
    1.73 -definition cbody :: "class \<Rightarrow> cbody" where
    1.74 -  "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
    1.75 +definition
    1.76 +  cbody :: "class \<Rightarrow> cbody"
    1.77 +  where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
    1.78  
    1.79  lemma access_cbody [simp]:"access (cbody c) = access c"
    1.80  by (simp add: cbody_def)
    1.81 @@ -368,18 +373,17 @@
    1.82  section "standard classes"
    1.83  
    1.84  consts
    1.85 -
    1.86    Object_mdecls  ::  "mdecl list" --{* methods of Object *}
    1.87    SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
    1.88 -  ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
    1.89 -  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *}
    1.90 -
    1.91 -defs 
    1.92  
    1.93 +definition
    1.94 +  ObjectC ::         "cdecl"      --{* declaration  of root      class   *} where
    1.95 +  "ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
    1.96 +                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
    1.97  
    1.98 -ObjectC_def:"ObjectC  \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
    1.99 -                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
   1.100 -SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
   1.101 +definition
   1.102 +  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *} where
   1.103 +  "SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
   1.104                                     init=Skip,
   1.105                                     super=if xn = Throwable then Object 
   1.106                                                             else SXcpt Throwable,
   1.107 @@ -391,8 +395,9 @@
   1.108  lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
   1.109  by (simp add: SXcptC_def)
   1.110  
   1.111 -definition standard_classes :: "cdecl list" where
   1.112 -         "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
   1.113 +definition
   1.114 +  standard_classes :: "cdecl list" where
   1.115 +  "standard_classes = [ObjectC, SXcptC Throwable,
   1.116                  SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
   1.117                  SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
   1.118  
   1.119 @@ -426,16 +431,15 @@
   1.120  
   1.121  section "is type"
   1.122  
   1.123 -consts
   1.124 -  is_type :: "prog \<Rightarrow>     ty \<Rightarrow> bool"
   1.125 -  isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
   1.126 -
   1.127 -primrec "is_type G (PrimT pt)  = True"
   1.128 -        "is_type G (RefT  rt)  = isrtype G rt"
   1.129 -        "isrtype G (NullT    ) = True"
   1.130 -        "isrtype G (IfaceT tn) = is_iface G tn"
   1.131 -        "isrtype G (ClassT tn) = is_class G tn"
   1.132 -        "isrtype G (ArrayT T ) = is_type  G T"
   1.133 +primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
   1.134 +  and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
   1.135 +where
   1.136 +  "is_type G (PrimT pt)  = True"
   1.137 +| "is_type G (RefT  rt)  = isrtype G rt"
   1.138 +| "isrtype G (NullT) = True"
   1.139 +| "isrtype G (IfaceT tn) = is_iface G tn"
   1.140 +| "isrtype G (ClassT tn) = is_class G tn"
   1.141 +| "isrtype G (ArrayT T ) = is_type  G T"
   1.142  
   1.143  lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
   1.144  by auto
   1.145 @@ -446,13 +450,13 @@
   1.146  
   1.147  section "subinterface and subclass relation, in anticipation of TypeRel.thy"
   1.148  
   1.149 -consts 
   1.150 +definition
   1.151    subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
   1.152 -  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass     *}
   1.153 +  where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
   1.154  
   1.155 -defs
   1.156 -  subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
   1.157 -  subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
   1.158 +definition
   1.159 +  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
   1.160 +  where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
   1.161  
   1.162  abbreviation
   1.163    subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
   1.164 @@ -517,15 +521,18 @@
   1.165  
   1.166  section "well-structured programs"
   1.167  
   1.168 -definition ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" where
   1.169 - "ws_idecl G I si \<equiv> \<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+"
   1.170 +definition
   1.171 +  ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
   1.172 +  where "ws_idecl G I si = (\<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+)"
   1.173    
   1.174 -definition ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" where
   1.175 - "ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
   1.176 +definition
   1.177 +  ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   1.178 +  where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)"
   1.179    
   1.180 -definition ws_prog  :: "prog \<Rightarrow> bool" where
   1.181 - "ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
   1.182 -              (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
   1.183 +definition
   1.184 +  ws_prog  :: "prog \<Rightarrow> bool" where
   1.185 +  "ws_prog G = ((\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
   1.186 +                 (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c)))"
   1.187  
   1.188  
   1.189  lemma ws_progI: 
   1.190 @@ -810,10 +817,10 @@
   1.191  apply simp
   1.192  done
   1.193  
   1.194 -definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   1.195 +definition
   1.196 +  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   1.197    --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
   1.198 -"imethds G I 
   1.199 -  \<equiv> iface_rec G I  
   1.200 +  "imethds G I = iface_rec G I
   1.201                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
   1.202                          (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
   1.203