src/HOL/MicroJava/J/TypeRel.thy
changeset 62145 5b946c81dfbf
parent 62042 6c6ccf573479
child 62390 842917225d56
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -176,14 +176,18 @@
     1.4      by(rule finite_acyclic_wf_converse[OF finite_subcls1])
     1.5  qed
     1.6  
     1.7 -consts
     1.8 -  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     1.9 -  field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    1.10 -  fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    1.11 +definition "method" :: "'c prog \<times> cname => (sig \<rightharpoonup> cname \<times> ty \<times> 'c)"
    1.12 +  \<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
    1.13 +  where [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
    1.14 +                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
    1.15  
    1.16 -\<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
    1.17 -defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
    1.18 -                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
    1.19 +definition fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list"
    1.20 +  \<comment> "list of fields of a class, including inherited and hidden ones"
    1.21 +  where [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
    1.22 +                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
    1.23 +
    1.24 +definition field :: "'c prog \<times> cname => (vname \<rightharpoonup> cname \<times> ty)"
    1.25 +  where [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    1.26  
    1.27  lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
    1.28    method (G,C) = (if C = Object then empty else method (G,D)) ++  
    1.29 @@ -194,11 +198,6 @@
    1.30  apply auto
    1.31  done
    1.32  
    1.33 -
    1.34 -\<comment> "list of fields of a class, including inherited and hidden ones"
    1.35 -defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
    1.36 -                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
    1.37 -
    1.38  lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
    1.39   fields (G,C) = 
    1.40    map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
    1.41 @@ -208,9 +207,6 @@
    1.42  apply auto
    1.43  done
    1.44  
    1.45 -
    1.46 -defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    1.47 -
    1.48  lemma field_fields: 
    1.49  "field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
    1.50  apply (unfold field_def)