src/HOL/Bali/WellType.thy
changeset 37406 982f3e02f3c4
parent 36367 49c7dee21a7f
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/WellType.thy	Fri Jun 11 17:14:01 2010 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Fri Jun 11 17:14:01 2010 +0200
     1.3 @@ -103,22 +103,23 @@
     1.4  "mheads G S (ClassT C) = cmheads G S C"
     1.5  "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    --{* applicable methods, cf. 15.11.2.1 *}
    1.10 -  appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
    1.11 - "appl_methds G S rt \<equiv> \<lambda> sig. 
    1.12 +  appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
    1.13 + "appl_methds G S rt = (\<lambda> sig. 
    1.14        {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
    1.15 -                           G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
    1.16 +                           G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
    1.17  
    1.18 +definition
    1.19    --{* more specific methods, cf. 15.11.2.2 *}
    1.20 -  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
    1.21 - "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
    1.22 +  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
    1.23 + "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
    1.24  (*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.25  
    1.26 +definition
    1.27    --{* maximally specific methods, cf. 15.11.2.2 *}
    1.28 -   max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
    1.29 -
    1.30 - "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
    1.31 +   max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
    1.32 + "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
    1.33                        (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
    1.34  
    1.35