# HG changeset patch # User haftmann # Date 1160556568 -7200 # Node ID c2a342e548a9281a1847b11a4d8acbf6733fd917 # Parent 341808e0b7f2314bb081b6b317ed0a27b238213c added code lemma diff -r 341808e0b7f2 -r c2a342e548a9 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Wed Oct 11 10:17:42 2006 +0200 +++ b/src/HOL/MicroJava/J/TypeRel.thy Wed Oct 11 10:49:28 2006 +0200 @@ -80,6 +80,37 @@ class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)" by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]]) +definition + "wf_class G = wf ((subcls1 G)^-1)" + +lemma class_rec_func [code func]: + "class_rec G C t f = (if wf_class G then + (case class G C + of None \<Rightarrow> arbitrary + | Some (D, fs, ms) \<Rightarrow> f C fs ms (if C = Object then t else class_rec G D t f)) + else class_rec G C t f)" +proof (cases "wf_class G") + case False then show ?thesis by auto +next + case True + from `wf_class G` have wf: "wf ((subcls1 G)^-1)" + unfolding wf_class_def . + show ?thesis + proof (cases "class G C") + case None + with wf show ?thesis + by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]]) + next + case (Some x) show ?thesis + proof (cases x) + case (fields D fs ms) + then have is_some: "class G C = Some (D, fs, ms)" using Some by simp + note class_rec = class_rec_lemma [OF wf is_some] + show ?thesis unfolding class_rec by (simp add: is_some) + qed + qed +qed + consts method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)