src/HOL/MicroJava/J/TypeRel.thy
changeset 10613 78b1d6c3ee9c
parent 10138 412a3ced6efd
child 11026 a50365d21144
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 06 19:09:34 2000 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 06 19:10:36 2000 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  defs
     1.5  
     1.6    (* direct subclass, cf. 8.1.3 *)
     1.7 -  subcls1_def	"subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
     1.8 + subcls1_def"subcls1 G \\<equiv> {(C,D). C\\<noteq>Object \\<and> (\\<exists>c. class G C=Some c \\<and> fst c=D)}"
     1.9    
    1.10  consts
    1.11  
    1.12 @@ -42,15 +42,15 @@
    1.13    field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
    1.14    fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
    1.15  
    1.16 -constdefs       (* auxiliary relations for recursive definitions below *)
    1.17 +constdefs       (* auxiliary relation for recursive definitions below *)
    1.18  
    1.19    subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
    1.20   "subcls1_rel == {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
    1.21  
    1.22  (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
    1.23  recdef method "subcls1_rel"
    1.24 - "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
    1.25 -                   | Some (sc,fs,ms) => (case sc of None => empty | Some D => 
    1.26 + "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
    1.27 +                   | Some (D,fs,ms) => (if C = Object then empty else 
    1.28                                             if is_class G D then method (G,D) 
    1.29                                                             else arbitrary) ++
    1.30                                             map_of (map (\\<lambda>(s,  m ). 
    1.31 @@ -59,9 +59,9 @@
    1.32  
    1.33  (* list of fields of a class, including inherited and hidden ones *)
    1.34  recdef fields  "subcls1_rel"
    1.35 - "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
    1.36 -                   | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
    1.37 -                                           (case sc of None => [] | Some D => 
    1.38 + "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
    1.39 +                   | Some (D,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
    1.40 +                                           (if C = Object then [] else 
    1.41                                             if is_class G D then fields (G,D) 
    1.42                                                             else arbitrary))
    1.43                    else arbitrary)"