src/HOL/MicroJava/J/TypeRel.thy
changeset 20970 c2a342e548a9
parent 18576 8d98b7711e47
child 22271 51a80e238b29
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Oct 11 10:17:42 2006 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Oct 11 10:49:28 2006 +0200
     1.3 @@ -80,6 +80,37 @@
     1.4   class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
     1.5    by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
     1.6  
     1.7 +definition
     1.8 +  "wf_class G = wf ((subcls1 G)^-1)"
     1.9 +
    1.10 +lemma class_rec_func [code func]:
    1.11 +  "class_rec G C t f = (if wf_class G then
    1.12 +    (case class G C
    1.13 +      of None \<Rightarrow> arbitrary
    1.14 +       | Some (D, fs, ms) \<Rightarrow> f C fs ms (if C = Object then t else class_rec G D t f))
    1.15 +    else class_rec G C t f)"
    1.16 +proof (cases "wf_class G")
    1.17 +  case False then show ?thesis by auto
    1.18 +next
    1.19 +  case True
    1.20 +  from `wf_class G` have wf: "wf ((subcls1 G)^-1)"
    1.21 +    unfolding wf_class_def .
    1.22 +  show ?thesis
    1.23 +  proof (cases "class G C")
    1.24 +    case None
    1.25 +    with wf show ?thesis
    1.26 +      by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
    1.27 +  next
    1.28 +    case (Some x) show ?thesis
    1.29 +    proof (cases x)
    1.30 +      case (fields D fs ms)
    1.31 +      then have is_some: "class G C = Some (D, fs, ms)" using Some by simp
    1.32 +      note class_rec = class_rec_lemma [OF wf is_some]
    1.33 +      show ?thesis unfolding class_rec by (simp add: is_some)
    1.34 +    qed
    1.35 +  qed
    1.36 +qed
    1.37 +
    1.38  consts
    1.39  
    1.40    method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)