src/HOL/MicroJava/J/TypeRel.thy
changeset 11987 bf31b35949ce
parent 11372 648795477bb5
child 12443 e56ab6134b41
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 30 17:33:56 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 30 17:37:25 2001 +0100
     1.3 @@ -193,11 +193,11 @@
     1.4  (*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
     1.5  proof -
     1.6    assume "G\<turnstile>S\<preceq>U"
     1.7 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
     1.8 -  proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1])
     1.9 +  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" ( *(is "PROP ?P S U")* )
    1.10 +  proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1])
    1.11      case refl
    1.12      fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
    1.13 -      (* fix T' show "PROP ?P T T".*)
    1.14 +      ( * fix T' show "PROP ?P T T".* )
    1.15    next
    1.16      case subcls
    1.17      fix T assume "G\<turnstile>Class D\<preceq>T"
    1.18 @@ -215,24 +215,19 @@
    1.19  theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
    1.20  proof -
    1.21    assume "G\<turnstile>S\<preceq>U"
    1.22 -  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
    1.23 -  proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *)
    1.24 -    case refl
    1.25 -    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
    1.26 -      (* fix T' show "PROP ?P T T".*)
    1.27 +  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
    1.28 +  proof induct
    1.29 +    case (refl T T')
    1.30 +    thus "G\<turnstile>T\<preceq>T'" .
    1.31    next
    1.32 -    case subcls
    1.33 -    fix T assume "G\<turnstile>Class D\<preceq>T"
    1.34 +    case (subcls C D T)
    1.35      then obtain E where "T = Class E" by (blast dest: widen_Class)
    1.36 -    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
    1.37 +    with subcls show "G\<turnstile>Class C\<preceq>T" by (auto elim: rtrancl_trans)
    1.38    next
    1.39 -    case null
    1.40 -    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
    1.41 +    case (null R RT)
    1.42      then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
    1.43      thus "G\<turnstile>NT\<preceq>RT" by auto
    1.44    qed
    1.45  qed
    1.46  
    1.47 -
    1.48 -
    1.49  end