src/HOL/MicroJava/J/WellType.thy
changeset 62145 5b946c81dfbf
parent 62042 6c6ccf573479
child 62390 842917225d56
     1.1 --- a/src/HOL/MicroJava/J/WellType.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -33,24 +33,20 @@
     1.4    localT :: "'c env => (vname \<rightharpoonup> ty)"
     1.5    where "localT == snd"
     1.6  
     1.7 -consts
     1.8 -  more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
     1.9 -                (ty \<times> 'x) \<times> ty list => bool"
    1.10 -  appl_methds :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
    1.11 -  max_spec :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
    1.12 +definition more_spec :: "'c prog \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> bool"
    1.13 +  where "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
    1.14 +                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
    1.15  
    1.16 -defs
    1.17 -  more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
    1.18 -                                list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
    1.19 -  
    1.20 +definition appl_methds :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
    1.21    \<comment> "applicable methods, cf. 15.11.2.1"
    1.22 -  appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
    1.23 +  where "appl_methds G C == \<lambda>(mn, pTs).
    1.24                       {((Class md,rT),pTs') |md rT mb pTs'.
    1.25                        method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
    1.26                        list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
    1.27  
    1.28 +definition max_spec :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
    1.29    \<comment> "maximally specific methods, cf. 15.11.2.2"
    1.30 -  max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
    1.31 +  where "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
    1.32                                         (\<forall>m'\<in>appl_methds G C sig.
    1.33                                           more_spec G m' m --> m' = m)}"
    1.34