src/HOL/MicroJava/J/TypeRel.thy
changeset 12443 e56ab6134b41
parent 11987 bf31b35949ce
child 12517 360e3215f029
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Dec 10 15:24:48 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Dec 10 15:26:42 2001 +0100
     1.3 @@ -31,27 +31,20 @@
     1.4    "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
     1.5    "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
     1.6  
     1.7 -defs
     1.8 +inductive "subcls1 G" intros
     1.9  
    1.10    (* direct subclass, cf. 8.1.3 *)
    1.11 - subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class G C=Some c \<and> fst c=D)}"
    1.12 +  subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
    1.13    
    1.14  lemma subcls1D: 
    1.15    "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
    1.16 -apply (unfold subcls1_def)
    1.17 -apply auto
    1.18 -done
    1.19 -
    1.20 -lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
    1.21 -apply (unfold subcls1_def)
    1.22 +apply (erule subcls1.elims)
    1.23  apply auto
    1.24  done
    1.25  
    1.26  lemma subcls1_def2: 
    1.27  "subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    1.28 -apply (unfold subcls1_def is_class_def)
    1.29 -apply auto
    1.30 -done
    1.31 +  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    1.32  
    1.33  lemma finite_subcls1: "finite (subcls1 G)"
    1.34  apply(subst subcls1_def2)