src/HOL/Bali/WellType.thy
changeset 37956 ee939247b2fb
parent 37406 982f3e02f3c4
child 41778 5f79a9e42507
     1.1 --- a/src/HOL/Bali/WellType.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -53,11 +53,13 @@
     1.4    emhead = "ref_ty \<times> mhead"
     1.5  
     1.6  --{* Some mnemotic selectors for emhead *}
     1.7 -definition "declrefT" :: "emhead \<Rightarrow> ref_ty" where
     1.8 -  "declrefT \<equiv> fst"
     1.9 +definition
    1.10 +  "declrefT" :: "emhead \<Rightarrow> ref_ty"
    1.11 +  where "declrefT = fst"
    1.12  
    1.13 -definition "mhd"     :: "emhead \<Rightarrow> mhead" where
    1.14 -  "mhd \<equiv> snd"
    1.15 +definition
    1.16 +  "mhd" :: "emhead \<Rightarrow> mhead"
    1.17 +  where "mhd \<equiv> snd"
    1.18  
    1.19  lemma declrefT_simp[simp]:"declrefT (r,m) = r"
    1.20  by (simp add: declrefT_def)
    1.21 @@ -77,50 +79,51 @@
    1.22  lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
    1.23  by (cases m) simp
    1.24  
    1.25 -consts
    1.26 -  cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
    1.27 -  Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
    1.28 -  accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    1.29 -  mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    1.30 -defs
    1.31 - cmheads_def:
    1.32 -"cmheads G S C 
    1.33 -  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
    1.34 -  Objectmheads_def:
    1.35 -"Objectmheads G S  
    1.36 -  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    1.37 -    ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
    1.38 -  accObjectmheads_def:
    1.39 -"accObjectmheads G S T
    1.40 -   \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
    1.41 -        then Objectmheads G S
    1.42 -        else (\<lambda>sig. {})"
    1.43 -primrec
    1.44 -"mheads G S  NullT     = (\<lambda>sig. {})"
    1.45 -"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
    1.46 -                         ` accimethds G (pid S) I sig \<union> 
    1.47 -                           accObjectmheads G S (IfaceT I) sig)"
    1.48 -"mheads G S (ClassT C) = cmheads G S C"
    1.49 -"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
    1.50 +definition
    1.51 +  cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
    1.52 +  where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
    1.53 +
    1.54 +definition
    1.55 +  Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
    1.56 +  "Objectmheads G S =
    1.57 +    (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    1.58 +      ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
    1.59 +
    1.60 +definition
    1.61 +  accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    1.62 +where
    1.63 +  "accObjectmheads G S T =
    1.64 +    (if G\<turnstile>RefT T accessible_in (pid S)
    1.65 +     then Objectmheads G S
    1.66 +     else (\<lambda>sig. {}))"
    1.67 +
    1.68 +primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    1.69 +where
    1.70 +  "mheads G S  NullT     = (\<lambda>sig. {})"
    1.71 +| "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
    1.72 +                           ` accimethds G (pid S) I sig \<union> 
    1.73 +                             accObjectmheads G S (IfaceT I) sig)"
    1.74 +| "mheads G S (ClassT C) = cmheads G S C"
    1.75 +| "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
    1.76  
    1.77  definition
    1.78    --{* applicable methods, cf. 15.11.2.1 *}
    1.79 -  appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
    1.80 - "appl_methds G S rt = (\<lambda> sig. 
    1.81 +  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
    1.82 +  "appl_methds G S rt = (\<lambda> sig. 
    1.83        {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
    1.84                             G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
    1.85  
    1.86  definition
    1.87    --{* more specific methods, cf. 15.11.2.2 *}
    1.88 -  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
    1.89 - "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
    1.90 +  more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
    1.91 +  "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
    1.92  (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
    1.93  
    1.94  definition
    1.95    --{* maximally specific methods, cf. 15.11.2.2 *}
    1.96 -   max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
    1.97 - "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
    1.98 -                      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
    1.99 +  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
   1.100 +  "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
   1.101 +                          (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   1.102  
   1.103  
   1.104  lemma max_spec2appl_meths: 
   1.105 @@ -138,13 +141,15 @@
   1.106  done
   1.107  
   1.108  
   1.109 -definition empty_dt :: "dyn_ty" where
   1.110 - "empty_dt \<equiv> \<lambda>a. None"
   1.111 +definition
   1.112 +  empty_dt :: "dyn_ty"
   1.113 +  where "empty_dt = (\<lambda>a. None)"
   1.114  
   1.115 -definition invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
   1.116 -"invmode m e \<equiv> if is_static m 
   1.117 +definition
   1.118 +  invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
   1.119 +  "invmode m e = (if is_static m 
   1.120                    then Static 
   1.121 -                  else if e=Super then SuperM else IntVir"
   1.122 +                  else if e=Super then SuperM else IntVir)"
   1.123  
   1.124  lemma invmode_nonstatic [simp]: 
   1.125    "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
   1.126 @@ -171,71 +176,71 @@
   1.127  
   1.128  section "Typing for unary operations"
   1.129  
   1.130 -consts unop_type :: "unop \<Rightarrow> prim_ty"
   1.131 -primrec 
   1.132 -"unop_type UPlus   = Integer"
   1.133 -"unop_type UMinus  = Integer"
   1.134 -"unop_type UBitNot = Integer"
   1.135 -"unop_type UNot    = Boolean"    
   1.136 +primrec unop_type :: "unop \<Rightarrow> prim_ty"
   1.137 +where
   1.138 +  "unop_type UPlus   = Integer"
   1.139 +| "unop_type UMinus  = Integer"
   1.140 +| "unop_type UBitNot = Integer"
   1.141 +| "unop_type UNot    = Boolean"    
   1.142  
   1.143 -consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   1.144 -primrec
   1.145 -"wt_unop UPlus   t = (t = PrimT Integer)"
   1.146 -"wt_unop UMinus  t = (t = PrimT Integer)"
   1.147 -"wt_unop UBitNot t = (t = PrimT Integer)"
   1.148 -"wt_unop UNot    t = (t = PrimT Boolean)"
   1.149 +primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   1.150 +where
   1.151 +  "wt_unop UPlus   t = (t = PrimT Integer)"
   1.152 +| "wt_unop UMinus  t = (t = PrimT Integer)"
   1.153 +| "wt_unop UBitNot t = (t = PrimT Integer)"
   1.154 +| "wt_unop UNot    t = (t = PrimT Boolean)"
   1.155  
   1.156  section "Typing for binary operations"
   1.157  
   1.158 -consts binop_type :: "binop \<Rightarrow> prim_ty"
   1.159 -primrec
   1.160 -"binop_type Mul      = Integer"     
   1.161 -"binop_type Div      = Integer"
   1.162 -"binop_type Mod      = Integer"
   1.163 -"binop_type Plus     = Integer"
   1.164 -"binop_type Minus    = Integer"
   1.165 -"binop_type LShift   = Integer"
   1.166 -"binop_type RShift   = Integer"
   1.167 -"binop_type RShiftU  = Integer"
   1.168 -"binop_type Less     = Boolean"
   1.169 -"binop_type Le       = Boolean"
   1.170 -"binop_type Greater  = Boolean"
   1.171 -"binop_type Ge       = Boolean"
   1.172 -"binop_type Eq       = Boolean"
   1.173 -"binop_type Neq      = Boolean"
   1.174 -"binop_type BitAnd   = Integer"
   1.175 -"binop_type And      = Boolean"
   1.176 -"binop_type BitXor   = Integer"
   1.177 -"binop_type Xor      = Boolean"
   1.178 -"binop_type BitOr    = Integer"
   1.179 -"binop_type Or       = Boolean"
   1.180 -"binop_type CondAnd  = Boolean"
   1.181 -"binop_type CondOr   = Boolean"
   1.182 +primrec binop_type :: "binop \<Rightarrow> prim_ty"
   1.183 +where
   1.184 +  "binop_type Mul      = Integer"     
   1.185 +| "binop_type Div      = Integer"
   1.186 +| "binop_type Mod      = Integer"
   1.187 +| "binop_type Plus     = Integer"
   1.188 +| "binop_type Minus    = Integer"
   1.189 +| "binop_type LShift   = Integer"
   1.190 +| "binop_type RShift   = Integer"
   1.191 +| "binop_type RShiftU  = Integer"
   1.192 +| "binop_type Less     = Boolean"
   1.193 +| "binop_type Le       = Boolean"
   1.194 +| "binop_type Greater  = Boolean"
   1.195 +| "binop_type Ge       = Boolean"
   1.196 +| "binop_type Eq       = Boolean"
   1.197 +| "binop_type Neq      = Boolean"
   1.198 +| "binop_type BitAnd   = Integer"
   1.199 +| "binop_type And      = Boolean"
   1.200 +| "binop_type BitXor   = Integer"
   1.201 +| "binop_type Xor      = Boolean"
   1.202 +| "binop_type BitOr    = Integer"
   1.203 +| "binop_type Or       = Boolean"
   1.204 +| "binop_type CondAnd  = Boolean"
   1.205 +| "binop_type CondOr   = Boolean"
   1.206  
   1.207 -consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   1.208 -primrec
   1.209 -"wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.210 -"wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.211 -"wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.212 -"wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.213 -"wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.214 -"wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.215 -"wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.216 -"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.217 -"wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.218 -"wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.219 -"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.220 -"wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.221 -"wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   1.222 -"wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   1.223 -"wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.224 -"wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.225 -"wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.226 -"wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.227 -"wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.228 -"wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.229 -"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.230 -"wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.231 +primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   1.232 +where
   1.233 +  "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.234 +| "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.235 +| "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.236 +| "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.237 +| "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.238 +| "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.239 +| "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.240 +| "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.241 +| "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.242 +| "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.243 +| "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.244 +| "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.245 +| "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   1.246 +| "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   1.247 +| "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.248 +| "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.249 +| "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.250 +| "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.251 +| "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   1.252 +| "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.253 +| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.254 +| "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   1.255  
   1.256  section "Typing for terms"
   1.257  
   1.258 @@ -244,9 +249,8 @@
   1.259    (type) "tys" <= (type) "ty + ty list"
   1.260  
   1.261  
   1.262 -inductive
   1.263 -  wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   1.264 -  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   1.265 +inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   1.266 +  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51] 50)
   1.267    and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   1.268    and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   1.269    and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"