# HG changeset patch # User berghofe # Date 1007994402 -3600 # Node ID e56ab6134b415f4e0edaca3122732ae39aaab6de # Parent 0ecba8660de777f8c4e62d13ecf12c756049c92a Turned subcls1 into an inductive relation to make it executable. diff -r 0ecba8660de7 -r e56ab6134b41 src/HOL/MicroJava/BV/JType.thy --- a/src/HOL/MicroJava/BV/JType.thy Mon Dec 10 15:24:48 2001 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Mon Dec 10 15:26:42 2001 +0100 @@ -66,9 +66,10 @@ moreover from R wf ty have "R \ ClassT Object \ ?thesis" - by (auto simp add: is_ty_def subcls1_def is_class_def + by (auto simp add: is_ty_def is_class_def split_tupled_all + elim!: subcls1.elims elim: converse_rtranclE - split: ref_ty.splits) + split: ref_ty.splits) ultimately show ?thesis by blast qed @@ -282,7 +283,8 @@ lemma single_valued_subcls1: "wf_prog wf_mb G ==> single_valued (subcls1 G)" - by (unfold wf_prog_def unique_def single_valued_def subcls1_def) auto + by (auto simp add: wf_prog_def unique_def single_valued_def + intro: subcls1I elim!: subcls1.elims) theorem err_semilat_JType_esl: "wf_prog wf_mb G ==> err_semilat (esl G)" diff -r 0ecba8660de7 -r e56ab6134b41 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Mon Dec 10 15:24:48 2001 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Dec 10 15:26:42 2001 +0100 @@ -31,27 +31,20 @@ "G\S \ T" == "(S,T) \ widen G" "G\C \? D" == "(C,D) \ cast G" -defs +inductive "subcls1 G" intros (* direct subclass, cf. 8.1.3 *) - subcls1_def: "subcls1 G \ {(C,D). C\Object \ (\c. class G C=Some c \ fst c=D)}" + subcls1I: "\class G C = Some (D,rest); C \ Object\ \ G\C\C1D" lemma subcls1D: "G\C\C1D \ C \ Object \ (\fs ms. class G C = Some (D,fs,ms))" -apply (unfold subcls1_def) -apply auto -done - -lemma subcls1I: "\class G C = Some (D,rest); C \ Object\ \ G\C\C1D" -apply (unfold subcls1_def) +apply (erule subcls1.elims) apply auto done lemma subcls1_def2: "subcls1 G = (\C\{C. is_class G C} . {D. C\Object \ fst (the (class G C))=D})" -apply (unfold subcls1_def is_class_def) -apply auto -done + by (auto simp add: is_class_def dest: subcls1D intro: subcls1I) lemma finite_subcls1: "finite (subcls1 G)" apply(subst subcls1_def2)