src/HOL/NanoJava/TypeRel.thy
changeset 23755 1c4672d130b1
parent 16417 9bc16273c2d4
child 28524 644b62cf678f
     1.1 --- a/src/HOL/NanoJava/TypeRel.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -9,22 +9,18 @@
     1.4  theory TypeRel imports Decl begin
     1.5  
     1.6  consts
     1.7 -  widen   :: "(ty    \<times> ty   ) set"  --{* widening *}
     1.8    subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
     1.9  
    1.10  syntax (xsymbols)
    1.11 -  widen   :: "[ty   , ty   ] => bool" ("_ \<preceq> _"    [71,71] 70)
    1.12    subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _"  [71,71] 70)
    1.13    subcls  :: "[cname, cname] => bool" ("_ \<preceq>C _"   [71,71] 70)
    1.14  syntax
    1.15 -  widen   :: "[ty   , ty   ] => bool" ("_ <= _"   [71,71] 70)
    1.16    subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
    1.17    subcls  :: "[cname, cname] => bool" ("_ <=C _"  [71,71] 70)
    1.18  
    1.19  translations
    1.20    "C \<prec>C1 D" == "(C,D) \<in> subcls1"
    1.21    "C \<preceq>C  D" == "(C,D) \<in> subcls1^*"
    1.22 -  "S \<preceq>   T" == "(S,T) \<in> widen"
    1.23  
    1.24  consts
    1.25    method :: "cname => (mname \<rightharpoonup> methd)"
    1.26 @@ -38,10 +34,12 @@
    1.27   subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
    1.28  
    1.29  text{* Widening, viz. method invocation conversion *}
    1.30 -inductive widen intros 
    1.31 -  refl   [intro!, simp]:           "T \<preceq> T"
    1.32 -  subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    1.33 -  null   [intro!]:                "NT \<preceq> R"
    1.34 +inductive
    1.35 +  widen :: "ty => ty => bool"  ("_ \<preceq> _" [71,71] 70)
    1.36 +where
    1.37 +  refl [intro!, simp]: "T \<preceq> T"
    1.38 +| subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    1.39 +| null [intro!]: "NT \<preceq> R"
    1.40  
    1.41  lemma subcls1D: 
    1.42    "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"