src/HOL/MicroJava/J/TypeRel.thy
changeset 14045 a34d89ce6097
parent 13090 4fb7a2f2c1df
child 14134 0fdf5708c7a8
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon May 26 11:42:41 2003 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon May 26 18:36:15 2003 +0200
     1.3 @@ -11,19 +11,19 @@
     1.4  consts
     1.5    subcls1 :: "'c prog => (cname \<times> cname) set"  -- "subclass"
     1.6    widen   :: "'c prog => (ty    \<times> ty   ) set"  -- "widening"
     1.7 -  cast    :: "'c prog => (cname \<times> cname) set"  -- "casting"
     1.8 +  cast    :: "'c prog => (ty    \<times> ty   ) set"  -- "casting"
     1.9  
    1.10  syntax (xsymbols)
    1.11    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    1.12    subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
    1.13    widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
    1.14 -  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
    1.15 +  cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
    1.16  
    1.17  syntax
    1.18    subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
    1.19    subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _"  [71,71,71] 70)
    1.20    widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _"   [71,71,71] 70)
    1.21 -  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
    1.22 +  cast    :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
    1.23  
    1.24  translations
    1.25    "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
    1.26 @@ -132,8 +132,8 @@
    1.27  -- "casting conversion, cf. 5.5 / 5.1.5"
    1.28  -- "left out casts on primitve types"
    1.29  inductive "cast G" intros
    1.30 -  widen:  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
    1.31 -  subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
    1.32 +  widen:  "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
    1.33 +  subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
    1.34  
    1.35  lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
    1.36  apply (rule iffI)
    1.37 @@ -168,6 +168,21 @@
    1.38  apply (auto elim: widen.subcls)
    1.39  done
    1.40  
    1.41 +lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
    1.42 +by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
    1.43 +
    1.44 +lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
    1.45 +apply (rule iffI)
    1.46 +apply (erule cast.elims)
    1.47 +apply auto
    1.48 +done
    1.49 +
    1.50 +lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT"
    1.51 +apply (erule cast.cases)
    1.52 +apply simp apply (erule widen.cases) 
    1.53 +apply auto
    1.54 +done
    1.55 +
    1.56  theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
    1.57  proof -
    1.58    assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"