simplified proofs concerning class_rec
authoroheimb
Tue Apr 24 14:26:05 2001 +0200 (2001-04-24)
changeset 1126670c9ebbffc49
parent 11265 4f2e6c87a57f
child 11267 f9506f60aa7b
simplified proofs concerning class_rec
src/HOL/MicroJava/J/TypeRel.thy
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Apr 24 12:19:58 2001 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Apr 24 14:26:05 2001 +0200
     1.3 @@ -66,30 +66,30 @@
     1.4  apply (auto dest!: subcls1D)
     1.5  done
     1.6  
     1.7 -lemma subcls_is_class2 [rule_format (no_asm)]: "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
     1.8 +lemma subcls_is_class2 [rule_format (no_asm)]: 
     1.9 +  "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
    1.10  apply (unfold is_class_def)
    1.11  apply (erule rtrancl_induct)
    1.12  apply  (drule_tac [2] subcls1D)
    1.13  apply  auto
    1.14  done
    1.15  
    1.16 +declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
    1.17 +
    1.18  consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
    1.19          'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.20 +
    1.21  recdef class_rec "same_fst (\<lambda>G. wf ((subcls1 G)^-1)) (\<lambda>G. (subcls1 G)^-1)"
    1.22        "class_rec (G,C) = (\<lambda>t f. case class G C of None \<Rightarrow> arbitrary 
    1.23                           | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then 
    1.24        f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
    1.25 -recdef_tc class_rec_tc: class_rec
    1.26 -  apply (unfold same_fst_def)
    1.27 -  apply (auto intro: subcls1I)
    1.28 -  done
    1.29 +(hints intro: subcls1I)
    1.30 +declare class_rec.simps [simp del]
    1.31  
    1.32  lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
    1.33   class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
    1.34 -  apply (rule class_rec_tc [THEN class_rec.simps 
    1.35 -              [THEN trans [THEN fun_cong [THEN fun_cong]]]])
    1.36 -  apply (rule ext, rule ext)
    1.37 -  apply auto
    1.38 +  apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
    1.39 +  apply simp
    1.40    done
    1.41  
    1.42  consts