Theory WellType

(*  Title:       CoreC++
    ID:          $Id: WellType.thy,v 1.11 2007-07-11 10:07:50 stefanberghofer Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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


header {* \isaheader{Well-typedness of CoreC++ expressions} *}

theory WellType imports Syntax TypeRel begin


section {* The rules *}

inductive
  WT :: "[prog,env,expr     ,ty     ] => bool"
         ("_,_ \<turnstile> _ :: _"   [51,51,51]50)
  and WTs :: "[prog,env,expr list,ty list] => bool"
         ("_,_ \<turnstile> _ [::] _" [51,51,51]50)
  for P :: prog
where
  
  WTNew:
  "is_class P C ==>
  P,E \<turnstile> new C :: Class C"

| WTDynCast: (* not more than one path between classes *)
  "[|P,E \<turnstile> e :: Class D; is_class P C;
    P \<turnstile> Path D to C unique ∨ (∀Cs. ¬ P \<turnstile> Path D to C via Cs)|] 
  ==> P,E \<turnstile> Cast C e :: Class C"

| WTStaticCast:
  "[|P,E \<turnstile> e :: Class D; is_class P C;
    P \<turnstile> Path D to C unique ∨ 
   (P \<turnstile> C \<preceq>* D ∧ (∀Cs. P \<turnstile> Path C to D via Cs --> SubobjsR P C Cs)) |] 
  ==> P,E \<turnstile> (|C|)),e :: Class C"

| WTVal:
  "typeof v = Some T ==>
  P,E \<turnstile> Val v :: T"

| WTVar:
  "E V = Some T ==>
  P,E \<turnstile> Var V :: T"

| WTBinOp:
  "[| P,E \<turnstile> e1 :: T1;  P,E \<turnstile> e2 :: T2;
     case bop of Eq => T1 = T2 ∧ T = Boolean
               | Add => T1 = Integer ∧ T2 = Integer ∧ T = Integer |]
  ==> P,E \<turnstile> e1 «bop» e2 :: T"

| WTLAss:
  "[| E V = Some T;  P,E \<turnstile> e :: T'; P \<turnstile> T' ≤ T|]
  ==> P,E \<turnstile> V:=e :: T"

| WTFAcc:
  "[| P,E \<turnstile> e :: Class C;  P \<turnstile> C has least F:T via Cs|] 
  ==> P,E \<turnstile> e•F{Cs} :: T"

| WTFAss:
  "[| P,E \<turnstile> e1 :: Class C;  P \<turnstile> C has least F:T via Cs; 
     P,E \<turnstile> e2 :: T'; P \<turnstile> T' ≤ T|]
  ==> P,E \<turnstile> e1•F{Cs}:=e2 :: T"

| WTStaticCall:
  "[| P,E \<turnstile> e :: Class C'; P \<turnstile> Path C' to C unique;
     P \<turnstile> C has least M = (Ts,T,m) via Cs; P,E \<turnstile> es [::] Ts'; P \<turnstile> Ts' [≤] Ts |]
  ==> P,E \<turnstile> e•(C::)M(es) :: T"

| WTCall:
  "[| P,E \<turnstile> e :: Class C;  P \<turnstile> C has least M = (Ts,T,m) via Cs;
     P,E \<turnstile> es [::] Ts'; P \<turnstile> Ts' [≤] Ts |]
  ==> P,E \<turnstile> e•M(es) :: T" 

| WTBlock:
  "[| is_type P T;  P,E(V \<mapsto> T) \<turnstile> e :: T' |]
  ==>  P,E \<turnstile> {V:T; e} :: T'"

| WTSeq:
  "[| P,E \<turnstile> e1::T1;  P,E \<turnstile> e2::T2 |]
  ==>  P,E \<turnstile> e1;;e2 :: T2"

| WTCond:
  "[| P,E \<turnstile> e :: Boolean;  P,E \<turnstile> e1::T;  P,E \<turnstile> e2::T |]
  ==> P,E \<turnstile> if (e) e1 else e2 :: T"

| WTWhile:
  "[| P,E \<turnstile> e :: Boolean;  P,E \<turnstile> c::T |]
  ==> P,E \<turnstile> while (e) c :: Void"

| WTThrow:
  "P,E \<turnstile> e :: Class C  ==> 
  P,E \<turnstile> throw e :: Void"


-- "well-typed expression lists"

| WTNil:
  "P,E \<turnstile> [] [::] []"

| WTCons:
  "[| P,E \<turnstile> e :: T;  P,E \<turnstile> es [::] Ts |]
  ==>  P,E \<turnstile> 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)]


section{* Easy consequences *}

lemma [iff]: "(P,E \<turnstile> [] [::] Ts) = (Ts = [])"

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


lemma [iff]: "(P,E \<turnstile> e#es [::] T#Ts) = (P,E \<turnstile> e :: T ∧ P,E \<turnstile> es [::] Ts)"

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


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

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


lemma [iff]: "!!Ts. (P,E \<turnstile> es1 @ es2 [::] Ts) =
  (∃Ts1 Ts2. Ts = Ts1 @ Ts2 ∧ P,E \<turnstile> es1 [::] Ts1 ∧ P,E \<turnstile> es2[::]Ts2)"

apply(induct es1 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 fastsimp
done


lemma [iff]: "P,E \<turnstile> Val v :: T = (typeof v = Some T)"

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


lemma [iff]: "P,E \<turnstile> Var V :: T = (E V = Some T)"

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


lemma [iff]: "P,E \<turnstile> e1;;e2 :: T2 = (∃T1. P,E \<turnstile> e1::T1 ∧ P,E \<turnstile> e2::T2)"

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


lemma [iff]: "(P,E \<turnstile> {V:T; e} :: T') = (is_type P T ∧ P,E(V\<mapsto>T) \<turnstile> e :: T')"

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



inductive_cases WT_elim_cases[elim!]:
  "P,E \<turnstile> new C :: T"
  "P,E \<turnstile> Cast C e :: T"
  "P,E \<turnstile> (|C|)),e :: T"
  "P,E \<turnstile> e1 «bop» e2 :: T"
  "P,E \<turnstile> V:= e :: T"
  "P,E \<turnstile> e•F{Cs} :: T"
  "P,E \<turnstile> e•F{Cs} := v :: T"
  "P,E \<turnstile> e•M(ps) :: T"
  "P,E \<turnstile> e•(C::)M(ps) :: T"
  "P,E \<turnstile> if (e) e1 else e2 :: T"
  "P,E \<turnstile> while (e) c :: T"
  "P,E \<turnstile> throw e :: T"



lemma wt_env_mono:
  "P,E \<turnstile> e :: T ==> (!!E'. E ⊆m E' ==> P,E' \<turnstile> e :: T)" and 
  "P,E \<turnstile> es [::] Ts ==> (!!E'. E ⊆m E' ==> P,E' \<turnstile> es [::] Ts)"

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



lemma WT_fv: "P,E \<turnstile> e :: T ==> fv e ⊆ dom E"
and "P,E \<turnstile> es [::] Ts ==> fvs es ⊆ dom E"

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

end