Improved definition of class_rec: no longer mixes algorithm and
authorberghofe
Fri Apr 19 14:43:16 2002 +0200 (2002-04-19)
changeset 130904fb7a2f2c1df
parent 13089 c8c28a1dc787
child 13091 3d12669e599c
Improved definition of class_rec: no longer mixes algorithm and
termination check.
src/HOL/MicroJava/J/TypeRel.thy
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Apr 19 14:33:04 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Apr 19 14:43:16 2002 +0200
     1.3 @@ -66,23 +66,18 @@
     1.4  apply  auto
     1.5  done
     1.6  
     1.7 -consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
     1.8 -        'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
     1.9 -
    1.10 -recdef class_rec "same_fst (\<lambda>G. wf ((subcls1 G)^-1)) (\<lambda>G. (subcls1 G)^-1)"
    1.11 -      "class_rec (G,C) = (\<lambda>t f. case class G C of None \<Rightarrow> arbitrary 
    1.12 -                         | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then 
    1.13 -      f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
    1.14 -(hints intro: subcls1I)
    1.15 +constdefs
    1.16 +  class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
    1.17 +    (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.18 +  "class_rec G == wfrec ((subcls1 G)^-1)
    1.19 +    (\<lambda>r C t f. case class G C of
    1.20 +         None \<Rightarrow> arbitrary
    1.21 +       | Some (D,fs,ms) \<Rightarrow> 
    1.22 +           f C fs ms (if C = Object then t else r D t f))"
    1.23  
    1.24 -declare class_rec.simps [simp del]
    1.25 -
    1.26 -
    1.27 -lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
    1.28 - class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
    1.29 -  apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
    1.30 -  apply simp
    1.31 -  done
    1.32 +lemma class_rec_lemma: "wf ((subcls1 G)^-1) \<Longrightarrow> class G C = Some (D,fs,ms) \<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 +  by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
    1.35  
    1.36  consts
    1.37  
    1.38 @@ -91,7 +86,7 @@
    1.39    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    1.40  
    1.41  -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
    1.42 -defs method_def: "method \<equiv> \<lambda>(G,C). class_rec (G,C) empty (\<lambda>C fs ms ts.
    1.43 +defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
    1.44                             ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
    1.45  
    1.46  lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
    1.47 @@ -105,7 +100,7 @@
    1.48  
    1.49  
    1.50  -- "list of fields of a class, including inherited and hidden ones"
    1.51 -defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec (G,C) []    (\<lambda>C fs ms ts.
    1.52 +defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
    1.53                             map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
    1.54  
    1.55  lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>