Theory WellForm

(*  Title:      JinjaThreads/Common/WellForm.thy
    Author:     Tobias Nipkow, Andreas Lochbihler

    Based on the Jinja theory Common/WellForm.thy by Tobias Nipkow
*)

header {* \isaheader{Generic Well-formedness of programs} *}

theory WellForm imports SystemClasses ExternalCall begin

text {*\noindent This theory defines global well-formedness conditions
for programs but does not look inside method bodies.  Hence it works
for both Jinja and JVM programs. Well-typing of expressions is defined
elsewhere (in theory @{text WellType}).

Because JinjaThreads does not have method overloading, its policy for method
overriding is the classical one: \emph{covariant in the result type
but contravariant in the argument types.} This means the result type
of the overriding method becomes more specific, the argument types
become more general.
*}

types 'm wf_mdecl_test = "'m prog => cname => 'm mdecl => bool"

definition wf_extCall :: "'m prog => cname => mname => bool" where
  "wf_extCall P C M ≡
   ∀D. P \<turnstile> D \<preceq>* C ∨ P \<turnstile> C \<preceq>* D --> ¬ is_external_call P (Class D) M"

definition wf_fdecl :: "'m prog => fdecl => bool"
where "wf_fdecl P ≡ λ(F,T). is_type P T"

definition wf_mdecl :: "'m wf_mdecl_test => 'm wf_mdecl_test"
where "wf_mdecl wf_md P C ≡ λ(M,Ts,T,mb). (∀T∈set Ts. is_type P T) ∧ is_type P T ∧ wf_md P C (M,Ts,T,mb)"

definition wf_cdecl :: "'m wf_mdecl_test => 'm prog => 'm cdecl => bool"
where
  "wf_cdecl wf_md P  ≡  λ(C,(D,fs,ms)).
  (∀f∈set fs. wf_fdecl P f) ∧  distinct_fst fs ∧
  (∀m∈set ms. wf_mdecl wf_md P C m) ∧  distinct_fst ms ∧
  (C ≠ Object -->
   is_class P D ∧ ¬ P \<turnstile> D \<preceq>* C ∧
   (∀(M,Ts,T,m)∈set ms. wf_extCall P C M ∧
      (∀D' Ts' T' m'. P \<turnstile> D sees M:Ts' -> T' = m' in D' -->
                       P \<turnstile> Ts' [≤] Ts ∧ P \<turnstile> T ≤ T'))) ∧
  (C = Object --> (fs = []) ∧ (ms = [])) ∧ (* require object to implement no fields/methods because of array subtype of Object *)

  (C = Thread --> (∃m. (run, [], Void, m) ∈ set ms))"

definition wf_syscls :: "'m prog => bool"
where "wf_syscls P ≡ {Object, Throwable, Thread} ∪ sys_xcpts ⊆ set(map fst P) ∧ (∀C ∈ sys_xcpts. P \<turnstile> C \<preceq>* Throwable)"

definition wf_prog :: "'m wf_mdecl_test => 'm prog => bool"
where "wf_prog wf_md P  ≡  wf_syscls P ∧ (∀c ∈ set P. wf_cdecl wf_md P c) ∧ distinct_fst P"

subsection{* Well-formedness lemmas *}

lemma class_wf: 
  "[|class P C = Some c; wf_prog wf_md P|] ==> wf_cdecl wf_md P (C,c)"
(*<*)
apply (unfold wf_prog_def class_def)
apply (fast dest: map_of_SomeD)
done
(*>*)


lemma class_Object [simp]: 
  "wf_prog wf_md P ==> ∃C fs ms. class P Object = Some (C,fs,ms)"
(*<*)
apply (unfold wf_prog_def wf_syscls_def class_def)
apply (auto simp: map_of_SomeI)
done
(*>*)

lemma class_Thread [simp]: 
  "wf_prog wf_md P ==> ∃C fs ms. class P Thread = Some (C,fs,ms)"
(*<*)
apply (unfold wf_prog_def wf_syscls_def class_def)
apply (auto simp: map_of_SomeI)
done
(*>*)

lemma is_class_Object [simp]:
  "wf_prog wf_md P ==> is_class P Object"
(*<*)by (simp add: is_class_def)(*>*)

lemma is_class_Thread [simp]:
  "wf_prog wf_md P ==> is_class P Thread"
(*<*)by (simp add: is_class_def)(*>*)

lemma is_class_xcpt:
  "[| C ∈ sys_xcpts; wf_prog wf_md P |] ==> is_class P C"
(*<*)
  apply (simp add: wf_prog_def wf_syscls_def is_class_def class_def)
  apply (fastsimp intro!: map_of_SomeI)
  done
(*>*)

lemma xcpt_subcls_Throwable:
  "[| C ∈ sys_xcpts; wf_prog wf_md P |] ==> P \<turnstile> C \<preceq>* Throwable"
by (simp add: wf_prog_def wf_syscls_def is_class_def class_def)


lemma subcls1_wfD:
  "[| P \<turnstile> C \<prec>1 D; wf_prog wf_md P |] ==> D ≠ C ∧ ¬ (subcls1 P)++ D C"
apply( frule tranclp.r_into_trancl[where r="subcls1 P"])
apply( drule subcls1D)
apply(clarify)
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def)
apply(rule conjI)
 apply(force)
apply(unfold reflcl_tranclp[symmetric, where r="subcls1 P"])
apply(blast)
done


lemma wf_cdecl_supD: 
  "[|wf_cdecl wf_md P (C,D,r); C ≠ Object|] ==> is_class P D"
(*<*)by (auto simp: wf_cdecl_def)(*>*)


lemma subcls_asym:
  "[| wf_prog wf_md P; (subcls1 P)++ C D |] ==> ¬ (subcls1 P)++ D C"
(*<*)
apply(erule tranclp.cases)
apply(fast dest!: subcls1_wfD )
apply(fast dest!: subcls1_wfD intro: tranclp_trans)
done
(*>*)


lemma subcls_irrefl:
  "[| wf_prog wf_md P; (subcls1 P)++ C D|] ==> C ≠ D"
(*<*)
apply (erule tranclp_trans_induct)
apply  (auto dest: subcls1_wfD subcls_asym)
done
(*>*)

lemma acyclicP_def:
  "acyclicP r <-> (∀x. ¬ r^++ x x)"
  unfolding acyclic_def trancl_def
by(auto)

lemma acyclic_subcls1:
  "wf_prog wf_md P ==> acyclicP (subcls1 P)"
(*<*)
apply (unfold acyclicP_def)
apply (fast dest: subcls_irrefl)
done
(*>*)



lemma wf_subcls1:
  "wf_prog wf_md P ==> wfP ((subcls1 P)¯¯)"
unfolding wfP_def
apply (rule finite_acyclic_wf)
 apply(subst finite_converse[unfolded converse_def, symmetric])
 apply(simp)
 apply(rule finite_subcls1)
apply(subst acyclic_converse[unfolded converse_def, symmetric])
apply(simp)
apply (erule acyclic_subcls1)
done
(*>*)


lemma single_valued_subcls1:
  "wf_prog wf_md G ==> single_valuedP (subcls1 G)"
(*<*)
by(auto simp:wf_prog_def distinct_fst_def single_valued_def dest!:subcls1D)
(*>*)


lemma subcls_induct: 
  "[| wf_prog wf_md P; !!C. ∀D. (subcls1 P)++ C D --> Q D ==> Q C |] ==> Q C"
(*<*)
  (is "?A ==> PROP ?P ==> _")
proof -
  assume p: "PROP ?P"
  assume ?A thus ?thesis apply -
apply(drule wf_subcls1)
apply(drule wfP_trancl)
apply(simp only: tranclp_converse)
apply(erule_tac a = C in wfP_induct)
apply(rule p)
apply(auto)
done
qed
(*>*)


lemma subcls1_induct_aux:
  "[| is_class P C; wf_prog wf_md P; Q Object;
    !!C D fs ms.
    [| C ≠ Object; is_class P C; class P C = Some (D,fs,ms) ∧
      wf_cdecl wf_md P (C,D,fs,ms) ∧ P \<turnstile> C \<prec>1 D ∧ is_class P D ∧ Q D|] ==> Q C |]
  ==> Q 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 safe
apply( frule (1) class_wf)
apply( frule (1) wf_cdecl_supD)

apply( subgoal_tac "P \<turnstile> C \<prec>1 a")
apply( erule_tac [2] subcls1I)
apply(  rule p)
apply (unfold is_class_def)
apply auto
done
qed
(*>*)

lemma subcls1_induct [consumes 2, case_names Object Subcls]:
  "[| wf_prog wf_md P; is_class P C; Q Object;
    !!C D. [|C ≠ Object; P \<turnstile> C \<prec>1 D; is_class P D; Q D|] ==> Q C |]
  ==> Q C"
(*<*)
  apply (erule subcls1_induct_aux, assumption, assumption)
  apply blast
  done
(*>*)


lemma subcls_C_Object:
  "[| is_class P C; wf_prog wf_md P |] ==> P \<turnstile> C \<preceq>* Object"
(*<*)
apply(erule (1) subcls1_induct)
 apply( fast)
apply(erule (1) converse_rtranclp_into_rtranclp)
done
(*>*)

lemma converse_subcls_is_class:
  assumes wf: "wf_prog wf_md P"
  shows "[| P \<turnstile> C \<preceq>* D; is_class P C |] ==> is_class P D"
proof(induct rule: rtranclp_induct)
  assume "is_class P C"
  thus "is_class P C" .
next
  fix D E
  assume PDE: "P \<turnstile> D \<prec>1 E"
    and IH: "is_class P C ==> is_class P D"
    and iPC: "is_class P C"
  have "is_class P D" by (rule IH[OF iPC])
  with PDE obtain fsD MsD where classD: "class P D = ⌊(E, fsD, MsD)⌋"
    by(auto simp add: is_class_def elim!: subcls1.cases)
  thus "is_class P E" using wf PDE
    apply -
    apply(erule subcls1.cases, clarsimp)
    apply(clarsimp simp: wf_prog_def)
    apply(drule_tac x="(D, E, fsD, MsD)" in bspec)
    apply(clarsimp simp add: class_def)
    apply(erule map_of_is_SomeD)
    apply(erule_tac C="D" in wf_cdecl_supD)
    .
qed

lemma is_class_is_subcls:
  "wf_prog m P ==> is_class P C = P \<turnstile> C \<preceq>* Object"
(*<*)by (fastsimp simp:is_class_def
                  elim: subcls_C_Object converse_rtranclpE subcls1I
                  dest: subcls1D)
(*>*)

lemma subcls_antisym:
  "[|wf_prog m P; P \<turnstile> C \<preceq>* D; P \<turnstile> D \<preceq>* C|] ==> C = D"
apply(drule acyclic_subcls1)
apply(drule acyclic_impl_antisym_rtrancl)
apply(drule antisymD)
apply(unfold Transitive_Closure.rtrancl_def)
apply(auto)
done

lemma is_type_pTs:
assumes "wf_prog wf_md P" and "(C,S,fs,ms) ∈ set P" and "(M,Ts,T,m) ∈ set ms"
shows "set Ts ⊆ is_type P"
(*<*)
proof
  from prems have "wf_mdecl wf_md P C (M,Ts,T,m)" 
    by (unfold wf_prog_def wf_cdecl_def) auto  
  hence "∀t ∈ set Ts. is_type P t" by (unfold wf_mdecl_def) auto
  moreover fix t assume "t ∈ set Ts"
  ultimately have "is_type P t" by blast
  thus "t ∈ is_type P" by(simp add: mem_def)
qed
(*>*)

lemma widen_asym_1: 
  assumes wfP: "wf_prog wf_md P"
  shows "P \<turnstile> C ≤ D ==> C = D ∨ ¬ (P \<turnstile> D ≤ C)"
proof (erule widen.induct)
  fix T
  show "T = T ∨ ¬ (P \<turnstile> T ≤ T)" by simp
next
  fix C D
  assume CscD: "P \<turnstile> C \<preceq>* D"
  then have CpscD: "C = D ∨ (C ≠ D ∧ (subcls1 P)++ C D)" by (simp add: rtranclpD)
  { assume "P \<turnstile> D \<preceq>* C"
    then have DpscC: "D = C ∨ (D ≠ C ∧ (subcls1 P)++ D C)" by (simp add: rtranclpD)
    { assume "(subcls1 P)++ D C"
      with wfP have CnscD: "¬ (subcls1 P)++ C D" by (rule subcls_asym)
      with CpscD have "C = D" by simp
    }
    with DpscC have "C = D" by blast
  }
  hence "Class C = Class D ∨ ¬ (P \<turnstile> D \<preceq>* C)" by blast
  thus "Class C = Class D ∨ ¬ P \<turnstile> Class D ≤ Class C" by simp
next
  fix C
  show "NT = Class C ∨ ¬ P \<turnstile> Class C ≤ NT" by simp
next
  fix A
  { assume "P \<turnstile> A⌊⌉ ≤ NT"
    hence "A⌊⌉ = NT" by fastsimp
    hence "False" by simp }
  hence "¬ (P \<turnstile> A⌊⌉ ≤ NT)" by blast
  thus "NT = A⌊⌉ ∨ ¬ P \<turnstile> A⌊⌉ ≤ NT" by simp
next
  fix A
  show "A⌊⌉ = Class Object ∨ ¬ P \<turnstile> Class Object ≤ A⌊⌉"
    by(auto dest: Object_widen)
next
  fix A B
  assume AsU: "P \<turnstile> A ≤ B" and BnpscA: "A = B ∨ ¬ P \<turnstile> B ≤ A"
  { assume "P \<turnstile> B⌊⌉ ≤ A⌊⌉"
    hence "P \<turnstile> B ≤ A" by (auto dest: Array_Array_widen)
    with BnpscA have "A = B" by blast
    hence "A⌊⌉ = B⌊⌉" by simp }
  thus "A⌊⌉ = B⌊⌉ ∨ ¬ P \<turnstile> B⌊⌉ ≤ A⌊⌉" by blast
qed

lemma widen_asym: "[| wf_prog wf_md P; P \<turnstile> C ≤ D; C ≠ D |] ==> ¬ (P \<turnstile> D ≤ C)"
proof -
  assume wfP: "wf_prog wf_md P" and CsD: "P \<turnstile> C ≤ D" and CneqD: "C ≠ D"
  from wfP CsD have "C = D ∨ ¬ (P \<turnstile> D ≤ C)" by (rule widen_asym_1)
  with CneqD show ?thesis by simp
qed

lemma widen_antisym:
  "[| wf_prog m P; P \<turnstile> T ≤ U; P \<turnstile> U ≤ T |] ==> T = U"
by(auto dest: widen_asym)

lemma widen_C_Object: "[| wf_prog wf_md P; is_class P C |] ==> P \<turnstile> Class C ≤ Class Object"
by(simp add: subcls_C_Object)

lemma is_refType_widen_Object:
  assumes wfP: "wf_prog wfmc P"
  shows "[| is_type P A; is_refT A |] ==> P \<turnstile> A ≤ Class Object"
by(induct A)(auto elim: refTE intro: subcls_C_Object[OF _ wfP] widen_array_object)

subsection{* Well-formedness and method lookup *}

lemma sees_wf_mdecl:
  "[| wf_prog wf_md P; P \<turnstile> C sees M:Ts->T = m in D |] ==> wf_mdecl wf_md P D (M,Ts,T,m)"
(*<*)
apply(drule visible_method_exists)
apply(clarify)
apply(drule class_wf, assumption)
apply(drule map_of_SomeD)
apply(simp add: wf_cdecl_def)
done
(*>*)


lemma sees_method_mono [rule_format (no_asm)]: 
  "[| P \<turnstile> C' \<preceq>* C; wf_prog wf_md P |] ==>
  ∀D Ts T m. P \<turnstile> C sees M:Ts->T = m in D -->
     (∃D' Ts' T' m'. P \<turnstile> C' sees M:Ts'->T' = m' in D' ∧ P \<turnstile> Ts [≤] Ts' ∧ P \<turnstile> T' ≤ T)"
apply( drule rtranclpD)
apply( erule disjE)
apply(  fastsimp intro: widen_refl widens_refl)
apply( erule conjE)
apply( erule tranclp_trans_induct)
prefer 2
apply(  clarify)
apply(  drule spec, drule spec, drule spec, drule spec, erule (1) impE)
apply clarify
apply(  fast elim: widen_trans widens_trans)
apply( clarify)
apply( drule subcls1D)
apply( clarify)
apply(clarsimp simp:Method_def)
apply(frule (2) sees_methods_rec)
apply(rule refl)
apply(case_tac "map_of ms M")
apply(rule_tac x = D in exI)
apply(rule_tac x = Ts in exI)
apply(rule_tac x = T in exI)
apply(clarsimp simp add: widens_refl)
apply(rule_tac x = m in exI)
apply(fastsimp simp add:map_add_def split:option.split)
apply clarsimp
apply(rename_tac Ts' T' m')
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def Method_def)
apply( frule map_of_SomeD)
apply(clarsimp)
apply(drule (1) bspec)+
apply clarsimp
apply( erule_tac x=D in allE, erule_tac x=Ts in allE, erule_tac x=T in allE, fastsimp simp:map_add_def split:option.split)
done
(*>*)


lemma sees_method_mono2:
  "[| P \<turnstile> C' \<preceq>* C; wf_prog wf_md P;
     P \<turnstile> C sees M:Ts->T = m in D; P \<turnstile> C' sees M:Ts'->T' = m' in D' |]
  ==> P \<turnstile> Ts [≤] Ts' ∧ P \<turnstile> T' ≤ T"
(*<*)by(blast dest:sees_method_mono sees_method_fun)(*>*)


lemma mdecls_visible:
assumes wf: "wf_prog wf_md P" and "class": "is_class P C"
shows "!!D fs ms. class P C = Some(D,fs,ms)
         ==> ∃Mm. P \<turnstile> C sees_methods Mm ∧ (∀(M,Ts,T,m) ∈ set ms. Mm M = Some((Ts,T,m),C))"
(*<*)
using wf "class"
proof (induct rule:subcls1_induct)
  case Object
  with wf have "distinct_fst ms"
    by (unfold class_def wf_prog_def wf_cdecl_def) (fastsimp dest:map_of_SomeD)
  with Object show ?case by(fastsimp intro!: sees_methods_Object map_of_SomeI)
next
  case Subcls
  with wf have "distinct_fst ms"
    by (unfold class_def wf_prog_def wf_cdecl_def) (fastsimp dest:map_of_SomeD)
  with Subcls show ?case
    by(fastsimp elim:sees_methods_rec dest:subcls1D map_of_SomeI
                simp:is_class_def)
qed
(*>*)


lemma mdecl_visible:
assumes wf: "wf_prog wf_md P" and C: "(C,S,fs,ms) ∈ set P" and  m: "(M,Ts,T,m) ∈ set ms"
shows "P \<turnstile> C sees M:Ts->T = m in C"
(*<*)
proof -
  from wf C have "class": "class P C = Some (S,fs,ms)"
    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
  from "class" have "is_class P C" by(auto simp:is_class_def)                   
  with prems "class" show ?thesis
    by(bestsimp simp:Method_def dest:mdecls_visible)
qed
(*>*)

lemma external_call_not_sees:
  assumes wf: "wf_prog wf_md P"
  and sees: "P \<turnstile> C sees_methods Mm" "Mm M = ⌊mthd⌋"
  and subcls: "P \<turnstile> C \<preceq>* C' ∨ P \<turnstile> C' \<preceq>* C"
  and ext: "is_external_call P (Class C') M"
  shows False
using sees subcls
proof(induct rule: Methods.induct)
  case (sees_methods_Object D' fs ms Mm)
  from `class P Object = ⌊(D', fs, ms)⌋` wf
  have "wf_cdecl wf_md P (Object, (D', fs, ms))" by(rule class_wf)
  hence "ms = []" by(simp add: wf_cdecl_def)
  with `Mm = Option.map (λm. (m, Object)) o map_of ms` `Mm M = ⌊mthd⌋`
  show False by simp
next
  case (sees_methods_rec C D' fs ms Mm Mm')
  from `class P C = ⌊(D', fs, ms)⌋` wf have wfC: "wf_cdecl wf_md P (C, D', fs, ms)" by(rule class_wf)
  show False
  proof(cases "map_of ms M")
    case (Some a)
    moreover obtain Ts T meth where a: "a = (Ts, T, meth)" by(cases a)
    ultimately have "(M, Ts, T, meth) ∈ set ms" by(auto dest: map_of_SomeD)
    with wfC `C ≠ Object` have "wf_extCall P C M" by(auto simp add: wf_cdecl_def)
    with `P \<turnstile> C \<preceq>* C' ∨ P \<turnstile> C' \<preceq>* C` `is_external_call P (Class C') M`
    show False by(auto simp add: wf_extCall_def)
  next
    case None
    with `Mm' = Mm ++ (Option.map (λm. (m, C)) o map_of ms)` `Mm' M = ⌊mthd⌋`
    have "Mm M = ⌊mthd⌋" by auto
    moreover from `class P C = ⌊(D', fs, ms)⌋` `C ≠ Object`
    have CsubD': "P \<turnstile> C \<prec>1 D'" by(rule subcls1I)
    from `P \<turnstile> C \<preceq>* C' ∨ P \<turnstile> C' \<preceq>* C` have "P \<turnstile> D' \<preceq>* C' ∨ P \<turnstile> C' \<preceq>* D'"
    proof
      assume "P \<turnstile> C \<preceq>* C'"
      thus ?thesis
      proof(cases rule: converse_rtranclpE[consumes 1])
        assume "C = C'"
        with CsubD' show ?thesis by auto
      next
        fix D
        assume "P \<turnstile> C \<prec>1 D" "P \<turnstile> D \<preceq>* C'"
        with CsubD' show ?thesis by(auto elim!: subcls1.cases)
      qed
    next
      assume "P \<turnstile> C' \<preceq>* C"
      with CsubD' show ?thesis by(blast intro: rtranclp.rtrancl_into_rtrancl)
    qed
    ultimately show False by(rule `[|Mm M = ⌊mthd⌋; P \<turnstile> D' \<preceq>* C' ∨ P \<turnstile> C' \<preceq>* D'|] ==> False`)
  qed
qed

lemma external_call_not_sees_method:
  "[| wf_prog wf_md P; P \<turnstile> C sees M: Ts -> T = mthd in D; is_external_call P (Class C') M; P \<turnstile> C \<preceq>* C' ∨ P \<turnstile> C' \<preceq>* C |]
  ==> False"
by(auto simp add: Method_def elim: external_call_not_sees)
   
lemma Call_lemma:
  "[| P \<turnstile> C sees M:Ts->T = m in D; P \<turnstile> C' \<preceq>* C; wf_prog wf_md P |]
  ==> ∃D' Ts' T' m'.
       P \<turnstile> C' sees M:Ts'->T' = m' in D' ∧ P \<turnstile> Ts [≤] Ts' ∧ P \<turnstile> T' ≤ T ∧ P \<turnstile> C' \<preceq>* D'
       ∧ is_type P T' ∧ (∀T∈set Ts'. is_type P T) ∧ wf_md P D' (M,Ts',T',m')"
apply(frule (2) sees_method_mono)
apply(fastsimp intro:sees_method_decl_above dest:sees_wf_mdecl
               simp: wf_mdecl_def)
done

lemma sub_Thread_sees_run:
  assumes wf: "wf_prog wf_md P"
  and PCThread: "P \<turnstile> C \<preceq>* Thread"
  shows "∃D mthd. P \<turnstile> C sees run: []->Void = mthd in D"
proof -
  from class_Thread[OF wf] obtain T' fsT MsT
    where classT: "class P Thread = ⌊(T', fsT, MsT)⌋" by blast
  with wf have wfcThread: "wf_cdecl wf_md P (Thread, T', fsT, MsT)"
    by(auto dest: map_of_is_SomeD bspec simp add: wf_prog_def class_def)
  then obtain mrunT where runThread: "(run, [], Void, mrunT) ∈ set MsT"
    by(auto simp add: wf_cdecl_def)
  moreover have "∃MmT. P \<turnstile> Thread sees_methods MmT ∧
                       (∀(M,Ts,T,m) ∈ set MsT. MmT M = Some((Ts,T,m),Thread))"
    by(rule mdecls_visible[OF wf is_class_Thread[OF wf] classT])
  then obtain MmT where ThreadMmT: "P \<turnstile> Thread sees_methods MmT"
    and MmT: "∀(M,Ts,T,m) ∈ set MsT. MmT M = Some((Ts,T,m),Thread)"
    by blast
  ultimately obtain mthd
    where "MmT run = ⌊(([], Void, mthd), Thread)⌋"
    by(fastsimp)
  with ThreadMmT have Tseesrun: "P \<turnstile> Thread sees run: []->Void = mthd in Thread"
    by(auto simp add: Method_def)
  from sees_method_mono[OF PCThread wf Tseesrun] show ?thesis by auto
qed

lemma wf_Object_method_empty:
  assumes wf: "wf_prog wf_md P"
  and sees: "P \<turnstile> Object sees M: Ts->T = m in D"
  shows False
proof -
  from wf obtain O' fs ms
    where classO: "class P Object = ⌊(O', fs, ms)⌋"
    by(fastsimp dest!: is_class_Object simp add: is_class_def)
  from wf classO have "ms = []"
    by(auto simp add: wf_prog_def wf_cdecl_def class_def dest: map_of_is_SomeD bspec)
  with classO sees show False
    by(auto elim: Methods.cases simp: Method_def)
qed

lemma wf_prog_lift:
  assumes wf: "wf_prog (λP C bd. A P C bd) P"
  and rule:
  "!!wf_md C M Ts C T m bd.
   wf_prog wf_md P ==>
   P \<turnstile> C sees M:Ts->T = m in C ==>   
   set Ts ⊆  is_type P ==>
   bd = (M,Ts,T,m) ==>
   A P C bd ==>
   B P C bd"
  shows "wf_prog (λP C bd. B P C bd) P"
(*<*)
proof -
  from wf show ?thesis
    apply (unfold wf_prog_def wf_cdecl_def)
    apply clarsimp
    apply (drule bspec, assumption)
    apply (unfold wf_mdecl_def)
    apply clarsimp
    apply (drule bspec, assumption)
    apply clarsimp
    apply (frule mdecl_visible [OF wf], assumption+)
    apply (frule is_type_pTs [OF wf], assumption+)
    apply(rule rule[OF wf], assumption+)
    apply auto
    done
qed


subsection{* Well-formedness and field lookup *}

lemma wf_Fields_Ex:
  "[| wf_prog wf_md P; is_class P C |] ==> ∃FDTs. P \<turnstile> C has_fields FDTs"
(*<*)
apply(frule class_Object)
apply(erule (1) subcls1_induct)
 apply(blast intro:has_fields_Object)
apply(blast intro:has_fields_rec dest:subcls1D)
done
(*>*)


lemma has_fields_types:
  "[| P \<turnstile> C has_fields FDTs; (FD,T) ∈ set FDTs; wf_prog wf_md P |] ==> is_type P T"
(*<*)
apply(induct rule:Fields.induct)
 apply(fastsimp dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
apply(fastsimp dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
done
(*>*)


lemma sees_field_is_type:
  "[| P \<turnstile> C sees F:T in D; wf_prog wf_md P |] ==> is_type P T"
(*<*)
by(fastsimp simp: sees_field_def
            elim: has_fields_types map_of_SomeD[OF map_of_remap_SomeD])
(*>*)

lemma wf_Object_field_empty:
  assumes wf: "wf_prog wf_md P"
  shows "P \<turnstile> Object has_fields []"
proof -
  from wf obtain O' fs ms where classO: "class P Object = ⌊(O', fs, ms)⌋"
    by -(drule is_class_Object,auto simp add: is_class_def)
  from wf classO have "fs = []"
    by(auto simp add: wf_prog_def wf_cdecl_def class_def dest: map_of_is_SomeD bspec)
  with classO show ?thesis
    by(auto intro: has_fields_Object)
qed

lemma wf_Object_not_has_field [dest]:
  "[| P \<turnstile> Object has F:T in D; wf_prog wf_md P |] ==> False"
by(auto dest: wf_Object_field_empty has_fields_fun simp add: has_field_def)


lemma wf_has_field_mono2:
  assumes wf: "wf_prog wf_md P"
  and has: "P \<turnstile> C has F:T in E"
  shows "[| P \<turnstile> C \<preceq>* D; P \<turnstile> D \<preceq>* E |] ==> P \<turnstile> D has F:T in E"
proof(induct rule: rtranclp_induct)
  case base show ?case using has .
next
  case (step D D')
  note DsubD' = `P \<turnstile> D \<prec>1 D'`
  from DsubD' obtain rest where classD: "class P D = ⌊(D', rest)⌋"
    and DObj: "D ≠ Object" by(auto elim!: subcls1.cases)
  from DsubD' `P \<turnstile> D' \<preceq>* E` have DsubE: "P \<turnstile> D \<preceq>* E" and DsubE2: "(subcls1 P)^++ D E"
    by(rule converse_rtranclp_into_rtranclp rtranclp_into_tranclp2)+
  from wf DsubE2 have DnE: "D ≠ E" by(rule subcls_irrefl)
  from DsubE have hasD: "P \<turnstile> D has F:T in E" by(rule `P \<turnstile> D \<preceq>* E ==> P \<turnstile> D has F:T in E`)
  then obtain FDTs where hasf: "P \<turnstile> D has_fields FDTs" and FE: "map_of FDTs (F, E) = ⌊T⌋"
    unfolding has_field_def by blast
  from hasf show ?case
  proof cases
    case has_fields_Object with DObj show ?thesis by simp
  next
    case (has_fields_rec DD DD' fs ms FDTs' FDTs'')
    with classD have [simp]: "DD = D" "FDTs'' = FDTs" "DD' = D'" "rest = (fs, ms)"
      and hasf': "P \<turnstile> D' has_fields FDTs'"
      and FDTs: "FDTs = map (λ(F, T). ((F, D), T)) fs @ FDTs'" by auto
    from FDTs FE DnE hasf' show ?thesis by(auto dest: map_of_SomeD simp add: has_field_def)
  qed
qed

lemma wf_has_field_idemp:
  "[| wf_prog wf_md P; P \<turnstile> C has F:T in D |] ==> P \<turnstile> D has F:T in D"
apply(frule has_field_decl_above)
apply(erule (2) wf_has_field_mono2)
apply(rule rtranclp.rtrancl_refl)
done

lemma map_of_remap_conv:
  "[| distinct_fst fs; map_of (map (λ(F, y). ((F, D), y)) fs) (F, D) = ⌊T⌋ |]
  ==> map_of (map (λ((F, D), T). (F, D, T)) (map (λ(F, y). ((F, D), y)) fs)) F = ⌊(D, T)⌋"
apply(induct fs)
apply auto
done

lemma has_field_idemp_sees_field:
  assumes wf: "wf_prog wf_md P"
  and has: "P \<turnstile> D has F:T in D"
  shows "P \<turnstile> D sees F:T in D"
proof -
  from has obtain FDTs where hasf: "P \<turnstile> D has_fields FDTs"
    and FD: "map_of FDTs (F, D) = ⌊T⌋" unfolding has_field_def by blast
  from hasf have "map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = ⌊(D, T)⌋"
  proof cases
    case (has_fields_Object D' fs ms FDTs')
    from `class P Object = ⌊(D', fs, ms)⌋` wf
    have "wf_cdecl wf_md P (Object, D', fs, ms)" by(rule class_wf)
    hence "distinct_fst fs" by(simp add: wf_cdecl_def)
    with FD has_fields_Object show ?thesis by(auto intro: map_of_remap_conv simp del: map_map)
  next
    case (has_fields_rec DD D' fs ms FDTs' FDTs'')
    hence [simp]: "DD = D" "FDTs'' = FDTs" "FDTs = map (λ(F, T). ((F, D), T)) fs @ FDTs'"
      and classD: "class P D = ⌊(D', fs, ms)⌋" and DnObj: "D ≠ Object"
      and hasf': "P \<turnstile> D' has_fields FDTs'" by auto
    from `class P D = ⌊(D', fs, ms)⌋` wf
    have "wf_cdecl wf_md P (D, D', fs, ms)" by(rule class_wf)
    hence "distinct_fst fs" by(simp add: wf_cdecl_def)
    moreover have "map_of FDTs' (F, D) = None"
    proof(rule ccontr)
      assume "map_of FDTs' (F, D) ≠ None"
      then obtain T' where "map_of FDTs' (F, D) = ⌊T'⌋" by(auto)
      with hasf' have "P \<turnstile> D' \<preceq>* D" by(auto dest!: map_of_SomeD intro: has_fields_decl_above)
      with classD DnObj have "(subcls1 P)^++ D D"
        by(auto intro: subcls1.intros rtranclp_into_tranclp2)
      with wf show False by(auto dest: subcls_irrefl)
    qed
    ultimately show ?thesis using FD hasf'
      by(auto simp add: map_add_Some_iff intro: map_of_remap_conv simp del: map_map)
  qed
  with hasf show ?thesis unfolding sees_field_def by blast
qed

end