src/HOL/MicroJava/J/TypeRel.thy
changeset 12517 360e3215f029
parent 12443 e56ab6134b41
child 12911 704713ca07ea
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Sun Dec 16 00:17:44 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Sun Dec 16 00:18:17 2001 +0100
     1.3 @@ -9,9 +9,9 @@
     1.4  theory TypeRel = Decl:
     1.5  
     1.6  consts
     1.7 -  subcls1 :: "'c prog => (cname \<times> cname) set"  (* subclass *)
     1.8 -  widen   :: "'c prog => (ty    \<times> ty   ) set"  (* widening *)
     1.9 -  cast    :: "'c prog => (cname \<times> cname) set"  (* casting *)
    1.10 +  subcls1 :: "'c prog => (cname \<times> cname) set"  -- "subclass"
    1.11 +  widen   :: "'c prog => (ty    \<times> ty   ) set"  -- "widening"
    1.12 +  cast    :: "'c prog => (cname \<times> cname) set"  -- "casting"
    1.13  
    1.14  syntax (xsymbols)
    1.15    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    1.16 @@ -31,9 +31,8 @@
    1.17    "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
    1.18    "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
    1.19  
    1.20 +-- "direct subclass, cf. 8.1.3"
    1.21  inductive "subcls1 G" intros
    1.22 -
    1.23 -  (* direct subclass, cf. 8.1.3 *)
    1.24    subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
    1.25    
    1.26  lemma subcls1D: 
    1.27 @@ -91,7 +90,7 @@
    1.28    field  :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty     )" (* ###curry *)
    1.29    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    1.30  
    1.31 -(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
    1.32 +-- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
    1.33  defs method_def: "method \<equiv> \<lambda>(G,C). class_rec (G,C) empty (\<lambda>C fs ms ts.
    1.34                             ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
    1.35  
    1.36 @@ -105,7 +104,7 @@
    1.37  done
    1.38  
    1.39  
    1.40 -(* list of fields of a class, including inherited and hidden ones *)
    1.41 +-- "list of fields of a class, including inherited and hidden ones"
    1.42  defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec (G,C) []    (\<lambda>C fs ms ts.
    1.43                             map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
    1.44  
    1.45 @@ -129,14 +128,15 @@
    1.46  done
    1.47  
    1.48  
    1.49 -inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3
    1.50 -			     i.e. sort of syntactic subtyping *)
    1.51 -  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    1.52 +-- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
    1.53 +inductive "widen G" intros 
    1.54 +  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
    1.55    subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
    1.56    null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
    1.57  
    1.58 -inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *)
    1.59 -                          (* left out casts on primitve types    *)
    1.60 +-- "casting conversion, cf. 5.5 / 5.1.5"
    1.61 +-- "left out casts on primitve types"
    1.62 +inductive "cast G" intros
    1.63    widen:  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
    1.64    subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
    1.65  
    1.66 @@ -173,45 +173,11 @@
    1.67  apply (auto elim: widen.subcls)
    1.68  done
    1.69  
    1.70 -lemma widen_trans [rule_format (no_asm)]: "G\<turnstile>S\<preceq>U ==> \<forall>T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T"
    1.71 -apply (erule widen.induct)
    1.72 -apply   safe
    1.73 -apply  (frule widen_Class)
    1.74 -apply  (frule_tac [2] widen_RefT)
    1.75 -apply  safe
    1.76 -apply(erule (1) rtrancl_trans)
    1.77 -done
    1.78 -
    1.79 -
    1.80 -(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
    1.81 +theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
    1.82  proof -
    1.83 -  assume "G\<turnstile>S\<preceq>U"
    1.84 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" ( *(is "PROP ?P S U")* )
    1.85 -  proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1])
    1.86 -    case refl
    1.87 -    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
    1.88 -      ( * fix T' show "PROP ?P T T".* )
    1.89 -  next
    1.90 -    case subcls
    1.91 -    fix T assume "G\<turnstile>Class D\<preceq>T"
    1.92 -    then obtain E where "T = Class E" by (blast dest: widen_Class)
    1.93 -    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
    1.94 -  next
    1.95 -    case null
    1.96 -    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
    1.97 -    then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
    1.98 -    thus "G\<turnstile>NT\<preceq>RT" by auto
    1.99 -  qed
   1.100 -qed
   1.101 -*)
   1.102 -
   1.103 -theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   1.104 -proof -
   1.105 -  assume "G\<turnstile>S\<preceq>U"
   1.106 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
   1.107 +  assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
   1.108    proof induct
   1.109 -    case (refl T T')
   1.110 -    thus "G\<turnstile>T\<preceq>T'" .
   1.111 +    case (refl T T') thus "G\<turnstile>T\<preceq>T'" .
   1.112    next
   1.113      case (subcls C D T)
   1.114      then obtain E where "T = Class E" by (blast dest: widen_Class)