src/HOL/MicroJava/J/TypeRel.thy
changeset 11284 981ea92a86dd
parent 11266 70c9ebbffc49
child 11372 648795477bb5
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu May 03 18:22:36 2001 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri May 04 15:38:48 2001 +0200
     1.3 @@ -74,8 +74,6 @@
     1.4  apply  auto
     1.5  done
     1.6  
     1.7 -declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
     1.8 -
     1.9  consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
    1.10          'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.11  
    1.12 @@ -84,8 +82,10 @@
    1.13                           | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then 
    1.14        f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
    1.15  (hints intro: subcls1I)
    1.16 +
    1.17  declare class_rec.simps [simp del]
    1.18  
    1.19 +
    1.20  lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
    1.21   class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
    1.22    apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])