--- 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)+