Turned subcls1 into an inductive relation to make it executable.

--- 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 \<noteq> ClassT Object \<Longrightarrow> ?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)"

--- 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\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
   "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
 
-defs
+inductive "subcls1 G" intros
 
   (* direct subclass, cf. 8.1.3 *)
- subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class G C=Some c \<and> fst c=D)}"
+  subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
   
 lemma subcls1D: 
   "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
-apply (unfold subcls1_def)
-apply auto
-done
-
-lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
-apply (unfold subcls1_def)
+apply (erule subcls1.elims)
 apply auto
 done
 
 lemma subcls1_def2: 
 "subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> 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)