diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -109,22 +109,24 @@
 by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
 
 lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
-by (auto simp add: subcls1_def2 comp_classname comp_is_class)
+by (auto simp add: subcls1_def2 comp_classname comp_is_class member2_inject)
 
-lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)"
-  apply rule
-  apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) 
+lemma comp_widen: "widen (comp G) = widen G"
+  apply (simp add: expand_fun_eq)
+  apply (intro allI iffI)
+  apply (erule widen.cases) 
   apply (simp_all add: comp_subcls1 widen.null)
-  apply (cases "(ty1,ty2)" G rule: widen.cases) 
+  apply (erule widen.cases) 
   apply (simp_all add: comp_subcls1 widen.null)
   done
 
-lemma comp_cast: "((ty1,ty2) \<in> cast (comp G)) = ((ty1,ty2) \<in> cast G)"
-  apply rule
-  apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) 
+lemma comp_cast: "cast (comp G) = cast G"
+  apply (simp add: expand_fun_eq)
+  apply (intro allI iffI)
+  apply (erule cast.cases) 
   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   apply (rule cast.widen) apply (simp add: comp_widen)
-  apply (cases "(ty1,ty2)" G rule: cast.cases)
+  apply (erule cast.cases)
   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   apply (rule cast.widen) apply (simp add: comp_widen)
   done
@@ -180,16 +182,16 @@
 done
 
 
-lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow> 
+lemma comp_class_rec: " wfP ((subcls1 G)^--1) \<Longrightarrow> 
 class_rec (comp G) C t f = 
   class_rec G C t (\<lambda> C' fs' ms' r'. f C' fs' (map (compMethod G C') ms') r')"
-apply (rule_tac a = C in  wf_induct) apply assumption
-apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)")
+apply (rule_tac a = C in  wfP_induct) apply assumption
+apply (subgoal_tac "wfP ((subcls1 (comp G))\<inverse>\<inverse>)")
 apply (subgoal_tac "(class G x = None) \<or> (\<exists> D fs ms. (class G x = Some (D, fs, ms)))")
 apply (erule disjE)
 
   (* case class G x = None *)
-apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec cut_apply)
+apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec [to_pred] cut_apply)
 apply (simp add: comp_class_None)
 
   (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
@@ -214,11 +216,11 @@
 apply (simp add: comp_subcls1)
 done
 
-lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow> 
+lemma comp_fields: "wfP ((subcls1 G)^--1) \<Longrightarrow> 
   fields (comp G,C) = fields (G,C)" 
 by (simp add: fields_def comp_class_rec)
 
-lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow> 
+lemma comp_field: "wfP ((subcls1 G)^--1) \<Longrightarrow> 
   field (comp G,C) = field (G,C)" 
 by (simp add: field_def comp_fields)
 
@@ -230,7 +232,7 @@
   \<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow> 
   R (class_rec G C t1 f1) (class_rec G C t2 f2)"
 apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *)
-apply (rule_tac a = C in  wf_induct) apply assumption
+apply (rule_tac a = C in  wfP_induct) apply assumption
 apply (intro strip)
 apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))")
   apply (erule exE)+