Theory WellType

(*  Title:       CoreC++

    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

    Based on the Jinja theory J/WellType.thy by Tobias Nipkow 
*)

section ‹Well-typedness of CoreC++ expressions›

theory WellType imports Syntax TypeRel begin


subsection ‹The rules›

inductive
  WT :: "[prog,env,expr     ,ty     ] ⇒ bool"
         ("_,_ ⊢ _ :: _"   [51,51,51]50)
  and WTs :: "[prog,env,expr list,ty list] ⇒ bool"
         ("_,_ ⊢ _ [::] _" [51,51,51]50)
  for P :: prog
where
  
  WTNew:
  "is_class P C ⟹
  P,E ⊢ new C :: Class C"

| WTDynCast: (* not more than one path between classes *)
  "⟦P,E ⊢ e :: Class D; is_class P C;
    P ⊢ Path D to C unique ∨ (∀Cs. ¬ P ⊢ Path D to C via Cs)⟧ 
  ⟹ P,E ⊢ Cast C e :: Class C"

| WTStaticCast:
  "⟦P,E ⊢ e :: Class D; is_class P C;
    P ⊢ Path D to C unique ∨ 
   (P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs)) ⟧ 
  ⟹ P,E ⊢ ⦇C⦈e :: Class C"

| WTVal:
  "typeof v = Some T ⟹
  P,E ⊢ Val v :: T"

| WTVar:
  "E V = Some T ⟹
  P,E ⊢ Var V :: T"

| WTBinOp:
  "⟦ P,E ⊢ e⇩1 :: T⇩1;  P,E ⊢ e⇩2 :: T⇩2;
     case bop of Eq ⇒ T⇩1 = T⇩2 ∧ T = Boolean
               | Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer ⟧
  ⟹ P,E ⊢ e⇩1 «bop» e⇩2 :: T"

| WTLAss:
  "⟦ E V = Some T;  P,E ⊢ e :: T'; P ⊢ T' ≤ T⟧
  ⟹ P,E ⊢ V:=e :: T"

| WTFAcc:
  "⟦ P,E ⊢ e :: Class C;  P ⊢ C has least F:T via Cs⟧ 
  ⟹ P,E ⊢ e∙F{Cs} :: T"

| WTFAss:
  "⟦ P,E ⊢ e⇩1 :: Class C;  P ⊢ C has least F:T via Cs; 
     P,E ⊢ e⇩2 :: T'; P ⊢ T' ≤ T⟧
  ⟹ P,E ⊢ e⇩1∙F{Cs}:=e⇩2 :: T"

| WTStaticCall:
  "⟦ P,E ⊢ e :: Class C'; P ⊢ Path C' to C unique;
     P ⊢ C has least M = (Ts,T,m) via Cs; P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
  ⟹ P,E ⊢ e∙(C::)M(es) :: T"

| WTCall:
  "⟦ P,E ⊢ e :: Class C;  P ⊢ C has least M = (Ts,T,m) via Cs;
     P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
  ⟹ P,E ⊢ e∙M(es) :: T" 

| WTBlock:
  "⟦ is_type P T;  P,E(V ↦ T) ⊢ e :: T' ⟧
  ⟹  P,E ⊢ {V:T; e} :: T'"

| WTSeq:
  "⟦ P,E ⊢ e⇩1::T⇩1;  P,E ⊢ e⇩2::T⇩2 ⟧
  ⟹  P,E ⊢ e⇩1;;e⇩2 :: T⇩2"

| WTCond:
  "⟦ P,E ⊢ e :: Boolean;  P,E ⊢ e⇩1::T;  P,E ⊢ e⇩2::T ⟧
  ⟹ P,E ⊢ if (e) e⇩1 else e⇩2 :: T"

| WTWhile:
  "⟦ P,E ⊢ e :: Boolean;  P,E ⊢ c::T ⟧
  ⟹ P,E ⊢ while (e) c :: Void"

| WTThrow:
  "P,E ⊢ e :: Class C  ⟹ 
  P,E ⊢ throw e :: Void"


― ‹well-typed expression lists›

| WTNil:
  "P,E ⊢ [] [::] []"

| WTCons:
  "⟦ P,E ⊢ e :: T;  P,E ⊢ es [::] Ts ⟧
  ⟹  P,E ⊢ e#es [::] T#Ts"


declare WT_WTs.intros[intro!] WTNil[iff]

lemmas WT_WTs_induct = WT_WTs.induct [split_format (complete)]
  and WT_WTs_inducts = WT_WTs.inducts [split_format (complete)]


subsection‹Easy consequences›

lemma [iff]: "(P,E ⊢ [] [::] Ts) = (Ts = [])"

apply(rule iffI)
apply (auto elim: WTs.cases)
done


lemma [iff]: "(P,E ⊢ e#es [::] T#Ts) = (P,E ⊢ e :: T ∧ P,E ⊢ es [::] Ts)"

apply(rule iffI)
apply (auto elim: WTs.cases)
done


lemma [iff]: "(P,E ⊢ (e#es) [::] Ts) =
  (∃U Us. Ts = U#Us ∧ P,E ⊢ e :: U ∧ P,E ⊢ es [::] Us)"

apply(rule iffI)
apply (auto elim: WTs.cases)
done


lemma [iff]: "⋀Ts. (P,E ⊢ es⇩1 @ es⇩2 [::] Ts) =
  (∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧ P,E ⊢ es⇩1 [::] Ts⇩1 ∧ P,E ⊢ es⇩2[::]Ts⇩2)"

apply(induct es⇩1 type:list)
 apply simp
apply clarsimp
apply(erule thin_rl)
apply (rule iffI)
 apply clarsimp
 apply(rule exI)+
 apply(rule conjI)
  prefer 2 apply blast
 apply simp
apply fastforce
done


lemma [iff]: "P,E ⊢ Val v :: T = (typeof v = Some T)"

apply(rule iffI)
apply (auto elim: WT.cases)
done


lemma [iff]: "P,E ⊢ Var V :: T = (E V = Some T)"

apply(rule iffI)
apply (auto elim: WT.cases)
done


lemma [iff]: "P,E ⊢ e⇩1;;e⇩2 :: T⇩2 = (∃T⇩1. P,E ⊢ e⇩1::T⇩1 ∧ P,E ⊢ e⇩2::T⇩2)"

apply(rule iffI)
apply (auto elim: WT.cases)
done


lemma [iff]: "(P,E ⊢ {V:T; e} :: T') = (is_type P T ∧ P,E(V↦T) ⊢ e :: T')"

apply(rule iffI)
apply (auto elim: WT.cases)
done



inductive_cases WT_elim_cases[elim!]:
  "P,E ⊢ new C :: T"
  "P,E ⊢ Cast C e :: T"
  "P,E ⊢ ⦇C⦈e :: T"
  "P,E ⊢ e⇩1 «bop» e⇩2 :: T"
  "P,E ⊢ V:= e :: T"
  "P,E ⊢ e∙F{Cs} :: T"
  "P,E ⊢ e∙F{Cs} := v :: T"
  "P,E ⊢ e∙M(ps) :: T"
  "P,E ⊢ e∙(C::)M(ps) :: T"
  "P,E ⊢ if (e) e⇩1 else e⇩2 :: T"
  "P,E ⊢ while (e) c :: T"
  "P,E ⊢ throw e :: T"



lemma wt_env_mono:
  "P,E ⊢ e :: T ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E' ⊢ e :: T)" and 
  "P,E ⊢ es [::] Ts ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E' ⊢ es [::] Ts)"

apply(induct rule: WT_WTs_inducts)
apply(simp add: WTNew)
apply(fastforce simp: WTDynCast)
apply(fastforce simp: WTStaticCast)
apply(fastforce simp: WTVal)
apply(simp add: WTVar map_le_def dom_def)
apply(fastforce simp: WTBinOp)
apply(force simp:map_le_def)
apply(fastforce simp: WTFAcc)
apply(fastforce simp: WTFAss)
apply(fastforce simp: WTCall)
apply(fastforce simp: WTStaticCall)
apply(fastforce simp: map_le_def WTBlock)
apply(fastforce simp: WTSeq)
apply(fastforce simp: WTCond)
apply(fastforce simp: WTWhile)
apply(fastforce simp: WTThrow)
apply(simp add: WTNil)
apply(simp add: WTCons)
done



lemma WT_fv: "P,E ⊢ e :: T ⟹ fv e ⊆ dom E"
and "P,E ⊢ es [::] Ts ⟹ fvs es ⊆ dom E"

apply(induct rule:WT_WTs.inducts)
apply(simp_all del: fun_upd_apply)
apply fast+
done

end