Theory WellForm

(*  Title:      HOL/MicroJava/J/WellForm.thy
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Well-formedness of Java programs›

theory WellForm
imports TypeRel SystemClasses
begin

text ‹
for static checks on expressions and statements, see WellType.

\begin{description}
\item[improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):]\ \\
\begin{itemize}
\item a method implementing or overwriting another method may have a result type
that widens to the result type of the other method (instead of identical type)
\end{itemize}

\item[simplifications:]\ \\
\begin{itemize}
\item for uniformity, Object is assumed to be declared like any other class
\end{itemize}
\end{description}
›
type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"

definition wf_syscls :: "'c prog => bool" where
"wf_syscls G == let cs = set G in Object ∈ fst ` cs ∧ (∀x. Xcpt x ∈ fst ` cs)"

definition wf_fdecl :: "'c prog => fdecl => bool" where
"wf_fdecl G == λ(fn,ft). is_type G ft"

definition wf_mhead :: "'c prog => sig => ty => bool" where
"wf_mhead G == λ(mn,pTs) rT. (∀T∈set pTs. is_type G T) ∧ is_type G rT"

definition ws_cdecl :: "'c prog => 'c cdecl => bool" where
"ws_cdecl G ==
   λ(C,(D,fs,ms)).
  (∀f∈set fs. wf_fdecl G         f) ∧  unique fs ∧
  (∀(sig,rT,mb)∈set ms. wf_mhead G sig rT) ∧ unique ms ∧
  (C ≠ Object ⟶ is_class G D ∧  ¬G⊢D≼C C)"

definition ws_prog :: "'c prog => bool" where
"ws_prog G == 
  wf_syscls G ∧ (∀c∈set G. ws_cdecl G c) ∧ unique G"

definition wf_mrT   :: "'c prog => 'c cdecl => bool" where
"wf_mrT G ==
   λ(C,(D,fs,ms)).
  (C ≠ Object ⟶ (∀(sig,rT,b)∈set ms. ∀D' rT' b'.
                      method(G,D) sig = Some(D',rT',b') --> G⊢rT≼rT'))"

definition wf_cdecl_mdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" where
"wf_cdecl_mdecl wf_mb G ==
   λ(C,(D,fs,ms)). (∀m∈set ms. wf_mb G C m)"

definition wf_prog :: "'c wf_mb => 'c prog => bool" where
"wf_prog wf_mb G == 
     ws_prog G ∧ (∀c∈ set G. wf_mrT G c ∧ wf_cdecl_mdecl wf_mb G c)"

definition wf_mdecl :: "'c wf_mb => 'c wf_mb" where
"wf_mdecl wf_mb G C == λ(sig,rT,mb). wf_mhead G sig rT ∧ wf_mb G C (sig,rT,mb)"

definition wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" where
"wf_cdecl wf_mb G ==
   λ(C,(D,fs,ms)).
  (∀f∈set fs. wf_fdecl G         f) ∧  unique fs ∧
  (∀m∈set ms. wf_mdecl wf_mb G C m) ∧  unique ms ∧
  (C ≠ Object ⟶ is_class G D ∧  ¬G⊢D≼C C ∧
                   (∀(sig,rT,b)∈set ms. ∀D' rT' b'.
                      method(G,D) sig = Some(D',rT',b') --> G⊢rT≼rT'))"

lemma wf_cdecl_mrT_cdecl_mdecl:
  "(wf_cdecl wf_mb G c) = (ws_cdecl G c ∧ wf_mrT G c ∧ wf_cdecl_mdecl wf_mb G c)"
apply (rule iffI)
apply (simp add: wf_cdecl_def ws_cdecl_def wf_mrT_def wf_cdecl_mdecl_def 
  wf_mdecl_def wf_mhead_def split_beta)+
done

lemma wf_cdecl_ws_cdecl [intro]: "wf_cdecl wf_mb G cd ⟹ ws_cdecl G cd"
by (simp add: wf_cdecl_mrT_cdecl_mdecl)

lemma wf_prog_ws_prog [intro]: "wf_prog wf_mb G ⟹ ws_prog G"
by (simp add: wf_prog_def ws_prog_def)

lemma wf_prog_wf_mdecl: 
  "⟦ wf_prog wf_mb G; (C,S,fs,mdecls) ∈ set G; ((mn,pTs),rT,code) ∈ set mdecls⟧
  ⟹ wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
by (auto simp add: wf_prog_def ws_prog_def wf_mdecl_def  
  wf_cdecl_mdecl_def ws_cdecl_def)

lemma class_wf: 
 "[|class G C = Some c; wf_prog wf_mb G|] 
  ==> wf_cdecl wf_mb G (C,c) ∧ wf_mrT G (C,c)"
apply (unfold wf_prog_def ws_prog_def wf_cdecl_def class_def)
apply clarify
apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
apply (simp add: wf_cdecl_def ws_cdecl_def wf_mdecl_def
  wf_cdecl_mdecl_def wf_mrT_def split_beta)
done

lemma class_wf_struct: 
 "[|class G C = Some c; ws_prog G|] 
  ==> ws_cdecl G (C,c)"
apply (unfold ws_prog_def class_def)
apply (fast dest: map_of_SomeD)
done

lemma class_Object [simp]: 
  "ws_prog G ==> ∃X fs ms. class G Object = Some (X,fs,ms)"
apply (unfold ws_prog_def wf_syscls_def class_def)
apply (auto simp: map_of_SomeI)
done

lemma class_Object_syscls [simp]: 
  "wf_syscls G ==> unique G ⟹ ∃X fs ms. class G Object = Some (X,fs,ms)"
apply (unfold wf_syscls_def class_def)
apply (auto simp: map_of_SomeI)
done

lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
  by (simp add: is_class_def)

lemma is_class_xcpt [simp]: "ws_prog G ⟹ is_class G (Xcpt x)"
  apply (simp add: ws_prog_def wf_syscls_def)
  apply (simp add: is_class_def class_def)
  apply clarify
  apply (erule_tac x = x in allE)
  apply clarify
  apply (auto intro!: map_of_SomeI)
  done

lemma subcls1_wfD: "[|G⊢C≺C1D; ws_prog G|] ==> D ≠ C ∧ (D, C) ∉ (subcls1 G)⇧+"
apply( frule trancl.r_into_trancl [where r="subcls1 G"])
apply( drule subcls1D)
apply(clarify)
apply( drule (1) class_wf_struct)
apply( unfold ws_cdecl_def)
apply(force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
done

lemma wf_cdecl_supD: 
"!!r. ⟦ws_cdecl G (C,D,r); C ≠ Object⟧ ⟹ is_class G D"
apply (unfold ws_cdecl_def)
apply (auto split: option.split_asm)
done

lemma subcls_asym: "[|ws_prog G; (C, D) ∈ (subcls1 G)⇧+|] ==> (D, C) ∉ (subcls1 G)⇧+"
apply(erule trancl.cases)
apply(fast dest!: subcls1_wfD )
apply(fast dest!: subcls1_wfD intro: trancl_trans)
done

lemma subcls_irrefl: "[|ws_prog G; (C, D) ∈ (subcls1 G)⇧+|] ==> C ≠ D"
apply (erule trancl_trans_induct)
apply  (auto dest: subcls1_wfD subcls_asym)
done

lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
apply (simp add: acyclic_def)
apply (fast dest: subcls_irrefl)
done

lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)¯)"
apply (rule finite_acyclic_wf)
apply ( subst finite_converse)
apply ( rule finite_subcls1)
apply (subst acyclic_converse)
apply (erule acyclic_subcls1)
done

lemma subcls_induct_struct: 
"[|ws_prog G; !!C. ∀D. (C, D) ∈ (subcls1 G)⇧+ --> P D ==> P C|] ==> P C"
(is "?A ⟹ PROP ?P ⟹ _")
proof -
  assume p: "PROP ?P"
  assume ?A thus ?thesis apply -
apply(drule wf_subcls1)
apply(drule wf_trancl)
apply(simp only: trancl_converse)
apply(erule_tac a = C in wf_induct)
apply(rule p)
apply(auto)
done
qed

lemma subcls_induct: 
"[|wf_prog wf_mb G; !!C. ∀D. (C, D) ∈ (subcls1 G)⇧+ --> P D ==> P C|] ==> P C"
(is "?A ⟹ PROP ?P ⟹ _")
by (fact subcls_induct_struct [OF wf_prog_ws_prog])

lemma subcls1_induct:
"[|is_class G C; wf_prog wf_mb G; P Object;  
   !!C D fs ms. [|C ≠ Object; is_class G C; class G C = Some (D,fs,ms) ∧  
    wf_cdecl wf_mb G (C,D,fs,ms) ∧ G⊢C≺C1D ∧ is_class G D ∧ P D|] ==> P C 
 |] ==> P C"
(is "?A ⟹ ?B ⟹ ?C ⟹ PROP ?P ⟹ _")
proof -
  assume p: "PROP ?P"
  assume ?A ?B ?C thus ?thesis apply -
apply(unfold is_class_def)
apply( rule impE)
prefer 2
apply(   assumption)
prefer 2
apply(  assumption)
apply( erule thin_rl)
apply( rule subcls_induct)
apply(  assumption)
apply( rule impI)
apply( case_tac "C = Object")
apply(  fast)
apply auto
apply( frule (1) class_wf) apply (erule conjE)+
apply (frule wf_cdecl_ws_cdecl)
apply( frule (1) wf_cdecl_supD)

apply( subgoal_tac "G⊢C≺C1a")
apply( erule_tac [2] subcls1I)
apply(  rule p)
apply (unfold is_class_def)
apply auto
done
qed

lemma subcls1_induct_struct:
"[|is_class G C; ws_prog G; P Object;  
   !!C D fs ms. [|C ≠ Object; is_class G C; class G C = Some (D,fs,ms) ∧  
    ws_cdecl G (C,D,fs,ms) ∧ G⊢C≺C1D ∧ is_class G D ∧ P D|] ==> P C 
 |] ==> P C"
(is "?A ⟹ ?B ⟹ ?C ⟹ PROP ?P ⟹ _")
proof -
  assume p: "PROP ?P"
  assume ?A ?B ?C thus ?thesis apply -
apply(unfold is_class_def)
apply( rule impE)
prefer 2
apply(   assumption)
prefer 2
apply(  assumption)
apply( erule thin_rl)
apply( rule subcls_induct_struct)
apply(  assumption)
apply( rule impI)
apply( case_tac "C = Object")
apply(  fast)
apply auto
apply( frule (1) class_wf_struct)
apply( frule (1) wf_cdecl_supD)

apply( subgoal_tac "G⊢C≺C1a")
apply( erule_tac [2] subcls1I)
apply(  rule p)
apply (unfold is_class_def)
apply auto
done
qed

lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma]

lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma]

lemma field_rec: "⟦class G C = Some (D, fs, ms); ws_prog G⟧
⟹ field (G, C) =
   (if C = Object then Map.empty else field (G, D)) ++
   map_of (map (λ(s, f). (s, C, f)) fs)"
apply (simp only: field_def)
apply (frule fields_rec, assumption)
apply (rule HOL.trans)
apply (simp add: o_def)
apply (simp (no_asm_use) add: split_beta split_def o_def)
done

lemma method_Object [simp]:
  "method (G, Object) sig = Some (D, mh, code) ⟹ ws_prog G ⟹ D = Object"  
  apply (frule class_Object, clarify)
  apply (drule method_rec, assumption)
  apply (auto dest: map_of_SomeD)
  done


lemma fields_Object [simp]: "⟦ ((vn, C), T) ∈ set (fields (G, Object)); ws_prog G ⟧
  ⟹ C = Object"
apply (frule class_Object)
apply clarify
apply (subgoal_tac "fields (G, Object) = map (λ(fn,ft). ((fn,Object),ft)) fs")
apply (simp add: image_iff split_beta)
apply auto
apply (rule trans)
apply (rule fields_rec, assumption+)
apply simp
done

lemma subcls_C_Object: "[|is_class G C; ws_prog G|] ==> G⊢C≼C Object"
apply(erule subcls1_induct_struct)
apply(  assumption)
apply( fast)
apply(auto dest!: wf_cdecl_supD)
done

lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
apply (unfold wf_mhead_def)
apply auto
done

lemma widen_fields_defpl': "[|is_class G C; ws_prog G|] ==>  
  ∀((fn,fd),fT)∈set (fields (G,C)). G⊢C≼C fd"
apply( erule subcls1_induct_struct)
apply(   assumption)
apply(  frule class_Object)
apply(  clarify)
apply(  frule fields_rec, assumption)
apply(  fastforce)
apply( tactic "safe_tac (put_claset HOL_cs \<^context>)")
apply( subst fields_rec)
apply(   assumption)
apply(  assumption)
apply( simp (no_asm) split del: if_split)
apply( rule ballI)
apply( simp (no_asm_simp) only: split_tupled_all)
apply( simp (no_asm))
apply( erule UnE)
apply(  force)
apply( erule r_into_rtrancl [THEN rtrancl_trans])
apply auto
done

lemma widen_fields_defpl: 
  "[|((fn,fd),fT) ∈ set (fields (G,C)); ws_prog G; is_class G C|] ==>  
  G⊢C≼C fd"
apply( drule (1) widen_fields_defpl')
apply (fast)
done

lemma unique_fields: 
  "[|is_class G C; ws_prog G|] ==> unique (fields (G,C))"
apply( erule subcls1_induct_struct)
apply(   assumption)
apply(  frule class_Object)
apply(  clarify)
apply(  frule fields_rec, assumption)
apply(  drule class_wf_struct, assumption)
apply(  simp add: ws_cdecl_def)
apply(  rule unique_map_inj)
apply(   simp)
apply(  rule inj_onI)
apply(  simp)
apply( safe dest!: wf_cdecl_supD)
apply( drule subcls1_wfD)
apply(  assumption)
apply( subst fields_rec)
apply   auto
apply( rotate_tac -1)
apply( frule class_wf_struct)
apply  auto
apply( simp add: ws_cdecl_def)
apply( erule unique_append)
apply(  rule unique_map_inj)
apply(   clarsimp)
apply  (rule inj_onI)
apply(  simp)
apply(auto dest!: widen_fields_defpl)
done

lemma fields_mono_lemma [rule_format (no_asm)]: 
  "[|ws_prog G; (C', C) ∈ (subcls1 G)⇧*|] ==>  
  x ∈ set (fields (G,C)) --> x ∈ set (fields (G,C'))"
apply(erule converse_rtrancl_induct)
apply( safe dest!: subcls1D)
apply(subst fields_rec)
apply(  auto)
done

lemma fields_mono: 
"⟦map_of (fields (G,C)) fn = Some f; G⊢D≼C C; is_class G D; ws_prog G⟧ 
  ⟹ map_of (fields (G,D)) fn = Some f"
apply (rule map_of_SomeI)
apply  (erule (1) unique_fields)
apply (erule (1) fields_mono_lemma)
apply (erule map_of_SomeD)
done

lemma widen_cfs_fields: 
"[|field (G,C) fn = Some (fd, fT); G⊢D≼C C; ws_prog G|]==>  
  map_of (fields (G,D)) (fn, fd) = Some fT"
apply (drule field_fields)
apply (drule rtranclD)
apply safe
apply (frule subcls_is_class)
apply (drule trancl_into_rtrancl)
apply (fast dest: fields_mono)
done

lemma method_wf_mdecl [rule_format (no_asm)]: 
  "wf_prog wf_mb G ==> is_class G C ⟹   
     method (G,C) sig = Some (md,mh,m) 
   --> G⊢C≼C md ∧ wf_mdecl wf_mb G md (sig,(mh,m))"
apply (frule wf_prog_ws_prog)
apply( erule subcls1_induct)
apply(   assumption)
apply(  clarify) 
apply(  frule class_Object)
apply(  clarify)
apply(  frule method_rec, assumption)
apply(  drule class_wf, assumption)
apply(  simp add: wf_cdecl_def)
apply(  drule map_of_SomeD)
apply(  subgoal_tac "md = Object")
apply(   fastforce) 
apply(  fastforce)
apply( clarify)
apply( frule_tac C = C in method_rec)
apply(  assumption)
apply( rotate_tac -1)
apply( simp)
apply( drule map_add_SomeD)
apply( erule disjE)
apply(  erule_tac V = "P --> Q" for P Q in thin_rl)
apply (frule map_of_SomeD)
apply (clarsimp simp add: wf_cdecl_def)
apply( clarify)
apply( rule rtrancl_trans)
prefer 2
apply(  assumption)
apply( rule r_into_rtrancl)
apply( fast intro: subcls1I)
done


lemma method_wf_mhead [rule_format (no_asm)]: 
  "ws_prog G ==> is_class G C ⟹   
     method (G,C) sig = Some (md,rT,mb) 
   --> G⊢C≼C md ∧ wf_mhead G sig rT"
apply( erule subcls1_induct_struct)
apply(   assumption)
apply(  clarify) 
apply(  frule class_Object)
apply(  clarify)
apply(  frule method_rec, assumption)
apply(  drule class_wf_struct, assumption)
apply(  simp add: ws_cdecl_def)
apply(  drule map_of_SomeD)
apply(  subgoal_tac "md = Object")
apply(   fastforce)
apply(  fastforce)
apply( clarify)
apply( frule_tac C = C in method_rec)
apply(  assumption)
apply( rotate_tac -1)
apply( simp)
apply( drule map_add_SomeD)
apply( erule disjE)
apply(  erule_tac V = "P --> Q" for P Q in thin_rl)
apply (frule map_of_SomeD)
apply (clarsimp simp add: ws_cdecl_def)
apply blast
apply clarify
apply( rule rtrancl_trans)
prefer 2
apply(  assumption)
apply( rule r_into_rtrancl)
apply( fast intro: subcls1I)
done

lemma subcls_widen_methd [rule_format (no_asm)]: 
  "[|G⊢T'≼C T; wf_prog wf_mb G|] ==>  
   ∀D rT b. method (G,T) sig = Some (D,rT ,b) --> 
  (∃D' rT' b'. method (G,T') sig = Some (D',rT',b') ∧ G⊢D'≼C D ∧ G⊢rT'≼rT)"
apply( drule rtranclD)
apply( erule disjE)
apply(  fast)
apply( erule conjE)
apply( erule trancl_trans_induct)
prefer 2
apply(  clarify)
apply(  drule spec, drule spec, drule spec, erule (1) impE)
apply(  fast elim: widen_trans rtrancl_trans)
apply( clarify)
apply( drule subcls1D)
apply( clarify)
apply( subst method_rec)
apply(  assumption)
apply( unfold map_add_def)
apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex)
apply( case_tac "∃z. map_of(map (λ(s,m). (s, C, m)) ms) sig = Some z" for C)
apply(  erule exE)
apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
prefer 2
apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
apply(  tactic "asm_full_simp_tac
  (put_simpset HOL_ss \<^context> addsimps [@{thm not_None_eq} RS sym]) 1")
apply(  simp_all (no_asm_simp) del: split_paired_Ex)
apply( frule (1) class_wf)
apply( simp (no_asm_simp) only: split_tupled_all)
apply( unfold wf_cdecl_def)
apply( drule map_of_SomeD)
apply (auto simp add: wf_mrT_def)
apply (rule rtrancl_trans)
defer
apply (rule method_wf_mhead [THEN conjunct1])
apply (simp only: wf_prog_def)
apply (simp add: is_class_def)
apply assumption
apply (auto intro: subcls1I)
done


lemma subtype_widen_methd: 
 "[| G⊢ C≼C D; wf_prog wf_mb G;  
     method (G,D) sig = Some (md, rT, b) |]  
  ==> ∃mD' rT' b'. method (G,C) sig= Some(mD',rT',b') ∧ G⊢rT'≼rT"
apply(auto dest: subcls_widen_methd 
           simp add: wf_mdecl_def wf_mhead_def split_def)
done


lemma method_in_md [rule_format (no_asm)]: 
  "ws_prog G ==> is_class G C ⟹ ∀D. method (G,C) sig = Some(D,mh,code) 
  --> is_class G D ∧ method (G,D) sig = Some(D,mh,code)"
apply (erule (1) subcls1_induct_struct)
 apply clarify
 apply (frule method_Object, assumption)
 apply hypsubst
 apply simp
apply (erule conjE)
apply (simplesubst method_rec, assumption+)
apply (clarify)
apply (erule_tac x = "Da" in allE)
apply (clarsimp)
 apply (simp add: map_of_map)
 apply (subst method_rec, assumption+)
 apply (simp add: map_add_def map_of_map split: option.split)
done


lemma method_in_md_struct [rule_format (no_asm)]: 
  "ws_prog G ==> is_class G C ⟹ ∀D. method (G,C) sig = Some(D,mh,code) 
  --> is_class G D ∧ method (G,D) sig = Some(D,mh,code)"
apply (erule (1) subcls1_induct_struct)
 apply clarify
 apply (frule method_Object, assumption)
 apply hypsubst
 apply simp
apply (erule conjE)
apply (simplesubst method_rec, assumption+)
apply (clarify)
apply (erule_tac x = "Da" in allE)
apply (clarsimp)
 apply (simp add: map_of_map)
 apply (subst method_rec, assumption+)
 apply (simp add: map_add_def map_of_map split: option.split)
done

lemma fields_in_fd [rule_format (no_asm)]: "⟦ wf_prog wf_mb G; is_class G C⟧
  ⟹ ∀ vn D T. (((vn,D),T) ∈ set (fields (G,C))
  ⟶ (is_class G D ∧ ((vn,D),T) ∈ set (fields (G,D))))"
apply (erule (1) subcls1_induct)

apply clarify
apply (frule wf_prog_ws_prog)
apply (frule fields_Object, assumption+)
apply (simp only: is_class_Object)

apply clarify
apply (frule fields_rec)
apply (simp (no_asm_simp) add: wf_prog_ws_prog)

apply (case_tac "Da=C")
apply blast                     (* case Da=C *)

apply (subgoal_tac "((vn, Da), T) ∈ set (fields (G, D))") apply blast
apply (erule thin_rl)
apply (rotate_tac 1)
apply (erule thin_rl, erule thin_rl, erule thin_rl, 
      erule thin_rl, erule thin_rl, erule thin_rl)
apply auto
done

lemma field_in_fd [rule_format (no_asm)]: "⟦ wf_prog wf_mb G; is_class G C⟧
  ⟹ ∀ vn D T. (field (G,C) vn = Some(D,T) 
  ⟶ is_class G D ∧ field (G,D) vn = Some(D,T))"
apply (erule (1) subcls1_induct)

apply clarify
apply (frule field_fields)
apply (drule map_of_SomeD)
apply (frule wf_prog_ws_prog)
apply (drule fields_Object, assumption+)
apply simp

apply clarify
apply (subgoal_tac "((field (G, D)) ++ map_of (map (λ(s, f). (s, C, f)) fs)) vn = Some (Da, T)")
apply (simp (no_asm_use) only: map_add_Some_iff)
apply (erule disjE)
apply (simp (no_asm_use) add: map_of_map) apply blast
apply (rule trans [symmetric], rule sym, assumption)
apply (rule_tac x=vn in fun_cong)
apply (rule trans, rule field_rec, assumption+)
apply (simp (no_asm_simp) add: wf_prog_ws_prog) 
apply (simp (no_asm_use)) apply blast
done


lemma widen_methd: 
"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G⊢T''≼C C|] 
  ==> ∃md' rT' b'. method (G,T'') sig = Some (md',rT',b') ∧ G⊢rT'≼rT"
apply( drule subcls_widen_methd)
apply   auto
done

lemma widen_field: "⟦ (field (G,C) fn) = Some (fd, fT); wf_prog wf_mb G; is_class G C ⟧
  ⟹ G⊢C≼C fd"
apply (rule widen_fields_defpl)
apply (simp add: field_def)
apply (rule map_of_SomeD)
apply (rule table_of_remap_SomeD) 
apply assumption+
apply (simp (no_asm_simp) add: wf_prog_ws_prog)+
done

lemma Call_lemma: 
"[|method (G,C) sig = Some (md,rT,b); G⊢T''≼C C; wf_prog wf_mb G;  
  class G C = Some y|] ==> ∃T' rT' b. method (G,T'') sig = Some (T',rT',b) ∧  
  G⊢rT'≼rT ∧ G⊢T''≼C T' ∧ wf_mhead G sig rT' ∧ wf_mb G T' (sig,rT',b)"
apply( drule (2) widen_methd)
apply( clarify)
apply( frule subcls_is_class2)
apply (unfold is_class_def)
apply (simp (no_asm_simp))
apply( drule method_wf_mdecl)
apply( unfold wf_mdecl_def)
apply( unfold is_class_def)
apply auto
done

lemma fields_is_type_lemma [rule_format (no_asm)]: 
  "[|is_class G C; ws_prog G|] ==>  
  ∀f∈set (fields (G,C)). is_type G (snd f)"
apply( erule (1) subcls1_induct_struct)
apply(  frule class_Object)
apply(  clarify)
apply(  frule fields_rec, assumption)
apply(  drule class_wf_struct, assumption)
apply(  simp add: ws_cdecl_def wf_fdecl_def)
apply(  fastforce)
apply( subst fields_rec)
apply(   fast)
apply(  assumption)
apply( clarsimp)
apply( safe)
prefer 2
apply(  force)
apply( drule (1) class_wf_struct)
apply( unfold ws_cdecl_def)
apply( clarsimp)
apply( drule (1) bspec)
apply( unfold wf_fdecl_def)
apply auto
done


lemma fields_is_type: 
  "[|map_of (fields (G,C)) fn = Some f; ws_prog G; is_class G C|] ==>  
  is_type G f"
apply(drule map_of_SomeD)
apply(drule (2) fields_is_type_lemma)
apply(auto)
done


lemma field_is_type: "⟦ ws_prog G; is_class G C; field (G, C) fn = Some (fd, fT) ⟧
  ⟹ is_type G fT"
apply (frule_tac f="((fn, fd), fT)" in fields_is_type_lemma)
apply (auto simp add: field_def dest: map_of_SomeD)
done


lemma methd:
  "[| ws_prog G; (C,S,fs,mdecls) ∈ set G; (sig,rT,code) ∈ set mdecls |]
  ==> method (G,C) sig = Some(C,rT,code) ∧ is_class G C"
proof -
  assume wf: "ws_prog G" and C:  "(C,S,fs,mdecls) ∈ set G" and
         m: "(sig,rT,code) ∈ set mdecls"
  moreover
  from wf C have "class G C = Some (S,fs,mdecls)"
    by (auto simp add: ws_prog_def class_def is_class_def intro: map_of_SomeI)
  moreover
  from wf C 
  have "unique mdecls" by (unfold ws_prog_def ws_cdecl_def) auto
  hence "unique (map (λ(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)  
  with m 
  have "map_of (map (λ(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
    by (force intro: map_of_SomeI)
  ultimately
  show ?thesis by (auto simp add: is_class_def dest: method_rec)
qed


lemma wf_mb'E:
  "⟦ wf_prog wf_mb G; ⋀C S fs ms m.⟦(C,S,fs,ms) ∈ set G; m ∈ set ms⟧ ⟹ wf_mb' G C m ⟧
  ⟹ wf_prog wf_mb' G"
  apply (simp only: wf_prog_def)
  apply auto
  apply (simp add: wf_cdecl_mdecl_def)
  apply safe
  apply (drule bspec, assumption) apply simp
  done


lemma fst_mono: "A ⊆ B ⟹ fst ` A ⊆ fst ` B" by fast

lemma wf_syscls:
  "set SystemClasses ⊆ set G ⟹ wf_syscls G"
  apply (drule fst_mono)
  apply (simp add: SystemClasses_def wf_syscls_def)
  apply (simp add: ObjectC_def) 
  apply (rule allI, case_tac x)
  apply (auto simp add: NullPointerC_def ClassCastC_def OutOfMemoryC_def)
  done

end