src/HOL/MicroJava/Comp/LemmasComp.thy

 theory LemmasComp
 imports TranslComp
 begin
 
 
+context
+begin
+
 declare split_paired_All [simp del]
 declare split_paired_Ex [simp del]
 
 
 (**********************************************************************)
 (* misc lemmas *)
 
-
-
-lemma split_pairs: "(\<lambda>(a,b). (F a b)) (ab) = F (fst ab) (snd ab)"
-proof -
-  have "(\<lambda>(a,b). (F a b)) (fst ab,snd ab) = F (fst ab) (snd ab)"
-    by (simp add: split_def)
-  then show ?thesis by simp
-qed
-
-
 lemma c_hupd_conv: 
   "c_hupd h' (xo, (h,l)) = (xo, (if xo = None then h' else h),l)"
-by (simp add: c_hupd_def)
+  by (simp add: c_hupd_def)
 
 lemma gl_c_hupd [simp]: "(gl (c_hupd h xs)) = (gl xs)"
-by (simp add: gl_def c_hupd_def split_pairs)
+  by (simp add: gl_def c_hupd_def split_beta)
 
 lemma c_hupd_xcpt_invariant [simp]: "gx (c_hupd h' (xo, st)) = xo"
-by (cases st) (simp only: c_hupd_conv gx_conv)
+  by (cases st) (simp only: c_hupd_conv gx_conv)
 
 (* not added to simpset because of interference with c_hupd_conv *)
 lemma c_hupd_hp_invariant: "gh (c_hupd hp (None, st)) = hp"
-by (cases st) (simp add: c_hupd_conv gh_def)
+  by (cases st) (simp add: c_hupd_conv gh_def)
 
 
 lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow>
   unique (map f xs) = unique xs"
 proof (induct xs)

       by (simp add: unique_def fst_set image_comp)
   qed
 qed
 
 lemma comp_unique: "unique (comp G) = unique G"
-apply (simp add: comp_def)
-apply (rule unique_map_fst)
-apply (simp add: compClass_def split_beta)
-done
+  apply (simp add: comp_def)
+  apply (rule unique_map_fst)
+  apply (simp add: compClass_def split_beta)
+  done
 
 
 (**********************************************************************)
 (* invariance of properties under compilation *)
 
 lemma comp_class_imp:
   "(class G C = Some(D, fs, ms)) \<Longrightarrow> 
   (class (comp G) C = Some(D, fs, map (compMethod G C) ms))"
-apply (simp add: class_def comp_def compClass_def)
-apply (rule HOL.trans)
-apply (rule map_of_map2)
-apply auto
-done
+  apply (simp add: class_def comp_def compClass_def)
+  apply (rule trans)
+   apply (rule map_of_map2)
+   apply auto
+  done
 
 lemma comp_class_None: 
 "(class G C = None) = (class (comp G) C = None)"
-apply (simp add: class_def comp_def compClass_def)
-apply (simp add: map_of_in_set)
-apply (simp add: image_comp [symmetric] o_def split_beta)
-done
+  apply (simp add: class_def comp_def compClass_def)
+  apply (simp add: map_of_in_set)
+  apply (simp add: image_comp [symmetric] o_def split_beta)
+  done
 
 lemma comp_is_class: "is_class (comp G) C = is_class G C"
-by (cases "class G C") (auto simp: is_class_def comp_class_None dest: comp_class_imp)
+  by (cases "class G C") (auto simp: is_class_def comp_class_None dest: comp_class_imp)
 
 
 lemma comp_is_type: "is_type (comp G) T = is_type G T"
-  apply (cases T)
-  apply simp
+  apply (cases T, simp)
   apply (induct G)
-  apply simp
-  apply (simp only: comp_is_class)
+   apply simp
+   apply (simp only: comp_is_class)
   apply (simp add: comp_is_class)
   apply (simp only: comp_is_class)
   done
 
-lemma comp_classname: "is_class G C 
-  \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
-by (cases "class G C") (auto simp: is_class_def dest: comp_class_imp)
+lemma comp_classname:
+  "is_class G C \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
+  by (cases "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)
 
 lemma comp_widen: "widen (comp G) = widen G"
   apply (simp add: fun_eq_iff)
   apply (intro allI iffI)
-  apply (erule widen.cases) 
-  apply (simp_all add: comp_subcls1 widen.null)
-  apply (erule widen.cases) 
-  apply (simp_all add: comp_subcls1 widen.null)
+   apply (erule widen.cases)
+     apply (simp_all add: comp_subcls1 widen.null)
+  apply (erule widen.cases)
+    apply (simp_all add: comp_subcls1 widen.null)
   done
 
 lemma comp_cast: "cast (comp G) = cast G"
   apply (simp add: fun_eq_iff)
   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 (erule cast.cases)
+    apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
+   apply (rule cast.widen)
+   apply (simp add: comp_widen)
   apply (erule cast.cases)
-  apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
-  apply (rule cast.widen) apply (simp add: comp_widen)
+   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
+  apply (rule cast.widen)
+  apply (simp add: comp_widen)
   done
 
 lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G"
   by (simp add: fun_eq_iff cast_ok_def comp_widen)
 
 
 lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)"
-by (simp add: compClass_def split_beta)
+  by (simp add: compClass_def split_beta)
 
 lemma compClass_fst_snd [simp]: "(fst (snd (compClass G C))) = (fst (snd C))"
-by (simp add: compClass_def split_beta)
+  by (simp add: compClass_def split_beta)
 
 lemma compClass_fst_snd_snd [simp]: "(fst (snd (snd (compClass G C)))) = (fst (snd (snd C)))"
-by (simp add: compClass_def split_beta)
+  by (simp add: compClass_def split_beta)
 
 lemma comp_wf_fdecl [simp]: "wf_fdecl (comp G) fd = wf_fdecl G fd"
-by (cases fd) (simp add: wf_fdecl_def comp_is_type)
-
-
-lemma compClass_forall [simp]: "
-  (\<forall>x\<in>set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) =
+  by (cases fd) (simp add: wf_fdecl_def comp_is_type)
+
+
+lemma compClass_forall [simp]:
+  "(\<forall>x\<in>set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) =
   (\<forall>x\<in>set (snd (snd (snd C))). P (fst x) (fst (snd x)))"
-by (simp add: compClass_def compMethod_def split_beta)
+  by (simp add: compClass_def compMethod_def split_beta)
 
 lemma comp_wf_mhead: "wf_mhead (comp G) S rT =  wf_mhead G S rT"
-by (simp add: wf_mhead_def split_beta comp_is_type)
-
-lemma comp_ws_cdecl: "
-  ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C"
-apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1)
-apply (simp (no_asm_simp) add: comp_wf_mhead)
-apply (simp add: compClass_def compMethod_def split_beta unique_map_fst)
-done
+  by (simp add: wf_mhead_def split_beta comp_is_type)
+
+lemma comp_ws_cdecl:
+  "ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C"
+  apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1)
+  apply (simp (no_asm_simp) add: comp_wf_mhead)
+  apply (simp add: compClass_def compMethod_def split_beta unique_map_fst)
+  done
 
 
 lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
-apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
-apply (simp add: image_comp)
-apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
-  (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-apply simp
-apply (simp add: fun_eq_iff split_beta)
-done
+  apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
+  apply (simp add: image_comp)
+  apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
+                      (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
+   apply simp
+  apply (simp add: fun_eq_iff split_beta)
+  done
 
 
 lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G"
-apply (rule sym)
-apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
-apply (simp add: comp_wf_syscls)
-apply (auto simp add: comp_ws_cdecl [symmetric] TranslComp.comp_def)
-done
-
-
-lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow> 
-class_rec (comp G) C t f = 
+  apply (rule sym)
+  apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
+  apply (simp add: comp_wf_syscls)
+  apply (auto simp add: comp_ws_cdecl [symmetric] TranslComp.comp_def)
+  done
+
+
+lemma comp_class_rec: 
+  "wf ((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))^-1)")
-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 [where R="(subcls1 G)^-1", simplified])
-apply (simp add: comp_class_None)
-
-  (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
-apply (erule exE)+
-apply (frule comp_class_imp)
-apply (frule_tac G="comp G" and C=x and t=t and f=f in class_rec_lemma)
-  apply assumption
-apply (frule_tac G=G and C=x and t=t 
-   and f="(\<lambda>C' fs' ms'. f C' fs' (map (compMethod G C') ms'))" in class_rec_lemma)
-  apply assumption
-apply (simp only:)
-
-apply (case_tac "x = Object")
-  apply simp
-  apply (frule subcls1I, assumption)
+  apply (rule_tac a = C in  wf_induct)
+   apply assumption
+  apply (subgoal_tac "wf ((subcls1 (comp G))^-1)")
+   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 [where R="(subcls1 G)^-1", simplified])
+     apply (simp add: comp_class_None)
+
+    (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
+    apply (erule exE)+
+    apply (frule comp_class_imp)
+    apply (frule_tac G="comp G" and C=x and t=t and f=f in class_rec_lemma)
+     apply assumption
+    apply (frule_tac G=G and C=x and t=t
+                 and f="(\<lambda>C' fs' ms'. f C' fs' (map (compMethod G C') ms'))" in class_rec_lemma)
+     apply assumption
+    apply (simp only:)
+    apply (case_tac "x = Object")
+     apply simp
+    apply (frule subcls1I, assumption)
     apply (drule_tac x=D in spec, drule mp, simp)
     apply simp
 
-  (* subgoals *)
-apply (case_tac "class G x")
-apply auto
-apply (simp add: comp_subcls1)
-done
+   (* subgoals *)
+   apply (case_tac "class G x")
+    apply auto
+  apply (simp add: comp_subcls1)
+  done
 
 lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow> 
   fields (comp G,C) = fields (G,C)" 
-by (simp add: fields_def comp_class_rec)
+  by (simp add: fields_def comp_class_rec)
 
 lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow> 
   field (comp G,C) = field (G,C)" 
-by (simp add: TypeRel.field_def comp_fields)
-
+  by (simp add: TypeRel.field_def comp_fields)
 
 
 lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk>  ws_prog G;
-  \<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2);
-   \<forall> C fs ms r1 r2. (R r1 r2) \<longrightarrow> (R (f1 C fs ms r1) (f2 C fs ms r2)) \<rbrakk>
-  \<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 (intro strip)
-apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))")
-  apply (erule exE)+
-apply (frule_tac C=x and t=t1 and f=f1 in class_rec_lemma)
-  apply assumption
-apply (frule_tac C=x and t=t2 and f=f2 in class_rec_lemma)
-  apply assumption
-apply (simp only:)
-
-apply (case_tac "x = Object")
-  apply simp
-  apply (frule subcls1I, assumption)
-    apply (drule_tac x=D in spec, drule mp, simp)
+  \<forall>fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2);
+   \<forall>C fs ms r1 r2. (R r1 r2) \<longrightarrow> (R (f1 C fs ms r1) (f2 C fs ms r2)) \<rbrakk>
+  \<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 (intro strip)
+  apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))")
+   apply (erule exE)+
+   apply (frule_tac C=x and t=t1 and f=f1 in class_rec_lemma)
+    apply assumption
+   apply (frule_tac C=x and t=t2 and f=f2 in class_rec_lemma)
+    apply assumption
+   apply (simp only:)
+
+   apply (case_tac "x = Object")
     apply simp
-    apply (subgoal_tac "(\<exists>D' rT' mb'. class G D = Some (D', rT', mb'))")
+   apply (frule subcls1I, assumption)
+   apply (drule_tac x=D in spec, drule mp, simp)
+   apply simp
+   apply (subgoal_tac "(\<exists>D' rT' mb'. class G D = Some (D', rT', mb'))")
     apply blast
 
-  (* subgoals *)
-
-apply (frule class_wf_struct) apply assumption
-apply (simp add: ws_cdecl_def is_class_def)
-
-apply (simp add: subcls1_def2 is_class_def)
-apply auto
-done
+   (* subgoals *)
+   apply (frule class_wf_struct, assumption)
+   apply (simp add: ws_cdecl_def is_class_def)
+   apply (simp add: subcls1_def2 is_class_def)
+   apply auto
+  done
 
 
 abbreviation (input)
   "mtd_mb == snd o snd"
 
 lemma map_of_map:
   "map_of (map (\<lambda>(k, v). (k, f v)) xs) k = map_option f (map_of xs k)"
   by (simp add: map_of_map)
 
-lemma map_of_map_fst: "\<lbrakk> inj f;
-  \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
-  \<Longrightarrow>  map_of (map g xs) k 
-  = map_option (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
-apply (induct xs)
-apply simp
-apply simp
-apply (case_tac "k = fst a")
-apply simp
-apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
-apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
-apply (erule conjE)+
-apply (drule_tac s ="fst (f a)" and t="fst a" in sym)
-apply simp
-apply (simp add: surjective_pairing)
-done
-
-lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
+lemma map_of_map_fst:
+  "\<lbrakk> inj f; \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
+  \<Longrightarrow>  map_of (map g xs) k = map_option (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
+  apply (induct xs)
+   apply simp
+  apply simp
+  apply (case_tac "k = fst a")
+   apply simp
+   apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
+   apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
+   apply (erule conjE)+
+   apply (drule_tac s ="fst (f a)" and t="fst a" in sym)
+   apply simp
+  apply (simp add: surjective_pairing)
+  done
+
+lemma comp_method [rule_format (no_asm)]:
+  "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   ((method (comp G, C) S) = 
-  map_option (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
-             (method (G, C) S))"
-apply (simp add: method_def)
-apply (frule wf_subcls1)
-apply (simp add: comp_class_rec)
-apply (simp add: split_iter split_compose map_map [symmetric] del: map_map)
-apply (rule_tac R="%x y. ((x S) = (map_option (\<lambda>(D, rT, b). 
-  (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
-  in class_rec_relation)
-apply assumption
-
-apply (intro strip)
-apply simp
-
-apply (rule trans)
-
-apply (rule_tac f="(\<lambda>(s, m). (s, Object, m))" and
-  g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" 
-  in map_of_map_fst)
-defer                           (* inj \<dots> *)
-apply (simp add: inj_on_def split_beta) 
-apply (simp add: split_beta compMethod_def)
-apply (simp add: map_of_map [symmetric])
-apply (simp add: split_beta)
-apply (simp add: Fun.comp_def split_beta)
-apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
-                    (fst x, Object,
-                     snd (compMethod G Object
-                           (inv (\<lambda>(s\<Colon>sig, m\<Colon>ty \<times> vname list \<times> fdecl list \<times> stmt \<times> expr).
-                                    (s, Object, m))
-                             (S, Object, snd x)))))
-  = (\<lambda>x. (fst x, Object, fst (snd x),
-                        snd (snd (compMethod G Object (S, snd x)))))")
-apply (simp only:)
-apply (simp add: fun_eq_iff)
-apply (intro strip)
-apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
-apply (simp only:)
-apply (simp add: compMethod_def split_beta)
-apply (rule inv_f_eq) 
-defer
-defer
-
-apply (intro strip)
-apply (simp add: map_add_Some_iff map_of_map)
-apply (simp add: map_add_def)
-apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
-apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
-  and k=S in map_of_map_fst) 
-apply (simp add: split_beta) 
-apply (simp add: compMethod_def split_beta)
-apply (case_tac "(map_of (map (\<lambda>(s, m). (s, Ca, m)) ms) S)")
-apply simp
-apply simp apply (simp add: split_beta map_of_map) apply (erule exE) apply (erule conjE)+
-apply (drule_tac t=a in sym)
-apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Ca, m)) (S, a)) = (S, snd a)")
-apply simp
-apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
-   prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta)
-apply (simp add: map_of_map2)
-apply (simp (no_asm_simp) add: compMethod_def split_beta)
-
-  -- "remaining subgoals"
-apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def)
-done
+   map_option (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
+              (method (G, C) S))"
+  apply (simp add: method_def)
+  apply (frule wf_subcls1)
+  apply (simp add: comp_class_rec)
+  apply (simp add: split_iter split_compose map_map [symmetric] del: map_map)
+  apply (rule_tac R="\<lambda>x y. ((x S) = (map_option (\<lambda>(D, rT, b).
+                           (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))"
+                  in class_rec_relation)
+     apply assumption
+
+    apply (intro strip)
+    apply simp
+    apply (rule trans)
+
+     apply (rule_tac f="(\<lambda>(s, m). (s, Object, m))" and
+                     g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))"
+                  in map_of_map_fst)
+       defer  (* inj \<dots> *)
+       apply (simp add: inj_on_def split_beta)
+      apply (simp add: split_beta compMethod_def)
+     apply (simp add: map_of_map [symmetric])
+     apply (simp add: split_beta)
+     apply (simp add: Fun.comp_def split_beta)
+     apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
+                        (fst x, Object,
+                         snd (compMethod G Object
+                         (inv (\<lambda>(s\<Colon>sig, m\<Colon>ty \<times> vname list \<times> fdecl list \<times> stmt \<times> expr).
+                           (s, Object, m))
+                           (S, Object, snd x)))))
+                        = (\<lambda>x. (fst x, Object, fst (snd x),
+                                snd (snd (compMethod G Object (S, snd x)))))")
+      apply (simp only:)
+     apply (simp add: fun_eq_iff)
+     apply (intro strip)
+     apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
+      apply (simp only:)
+      apply (simp add: compMethod_def split_beta)
+     apply (rule inv_f_eq)
+      defer
+      defer
+
+      apply (intro strip)
+      apply (simp add: map_add_Some_iff map_of_map)
+      apply (simp add: map_add_def)
+      apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
+       apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
+                    and k=S in map_of_map_fst)
+         apply (simp add: split_beta)
+        apply (simp add: compMethod_def split_beta)
+       apply (case_tac "(map_of (map (\<lambda>(s, m). (s, Ca, m)) ms) S)")
+        apply simp
+       apply (simp add: split_beta map_of_map)
+       apply (elim exE conjE)
+       apply (drule_tac t=a in sym)
+       apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Ca, m)) (S, a)) = (S, snd a)")
+        apply simp
+        apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
+         prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta)
+        apply (simp add: map_of_map2)
+        apply (simp (no_asm_simp) add: compMethod_def split_beta)
+
+       -- "remaining subgoals"
+       apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def)
+  done
 
 
 
 lemma comp_wf_mrT: "\<lbrakk> ws_prog G; is_class G D\<rbrakk> \<Longrightarrow> 
   wf_mrT (TranslComp.comp G) (C, D, fs, map (compMethod G a) ms) =
   wf_mrT G (C, D, fs, ms)"
-apply (simp add: wf_mrT_def compMethod_def split_beta)
-apply (simp add: comp_widen)
-apply (rule iffI)
-apply (intro strip)
-apply simp
-apply (drule bspec) apply assumption
-apply (drule_tac x=D' in spec) apply (drule_tac x=rT' in spec) apply (drule mp)
-prefer 2 apply assumption
-apply (simp add: comp_method [of G D])
-apply (erule exE)+
-apply (simp add: split_paired_all)
-apply (intro strip)
-apply (simp add: comp_method)
-apply auto
-done
+  apply (simp add: wf_mrT_def compMethod_def split_beta)
+  apply (simp add: comp_widen)
+  apply (rule iffI)
+   apply (intro strip)
+   apply simp
+   apply (drule (1) bspec)
+   apply (drule_tac x=D' in spec)
+   apply (drule_tac x=rT' in spec)
+   apply (drule mp)
+    prefer 2 apply assumption
+   apply (simp add: comp_method [of G D])
+   apply (erule exE)+
+   apply (simp add: split_paired_all)
+  apply (auto simp: comp_method)
+  done
 
 
 (**********************************************************************)
   (* DIVERSE OTHER LEMMAS *)
 (**********************************************************************)
 
 lemma max_spec_preserves_length:
-  "max_spec G C (mn, pTs) = {((md,rT),pTs')} 
-  \<Longrightarrow> length pTs = length pTs'"
-apply (frule max_spec2mheads)
-apply (erule exE)+
-apply (simp add: list_all2_iff)
-done
+  "max_spec G C (mn, pTs) = {((md,rT),pTs')} \<Longrightarrow> length pTs = length pTs'"
+  apply (frule max_spec2mheads)
+  apply (clarsimp simp: list_all2_iff)
+  done
 
 
 lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
-apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
-apply blast
-apply (rule ty_expr_ty_exprs_wt_stmt.induct)
-apply auto
-done
+  apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
+   apply blast
+  apply (rule ty_expr_ty_exprs_wt_stmt.induct, auto)
+  done
 
 
 lemma max_spec_preserves_method_rT [simp]:
   "max_spec G C (mn, pTs) = {((md,rT),pTs')}
   \<Longrightarrow> method_rT (the (method (G, C) (mn, pTs'))) = rT"
-apply (frule max_spec2mheads)
-apply (erule exE)+
-apply (simp add: method_rT_def)
-done
+  apply (frule max_spec2mheads)
+  apply (clarsimp simp: method_rT_def)
+  done
 
   (**********************************************************************************)
+
+end (* context *)
 
 declare compClass_fst [simp del]
 declare compClass_fst_snd [simp del]
 declare compClass_fst_snd_snd [simp del]
 
-declare split_paired_All [simp add]
-declare split_paired_Ex [simp add]
-
 end