Theory WellType

(*  Title:      Jinja/J/WellType.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Well-typedness of Jinja expressions›

theory WellType
imports "../Common/Objects" Expr
begin

type_synonym
  env  = "vname ⇀ ty"

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

| WTCast:
  "⟦ P,E ⊢ e :: Class D;  is_class P C;  P ⊢ C ≼⇧* D ∨ P ⊢ D ≼⇧* C ⟧
  ⟹ P,E ⊢ Cast 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 ⇒ (P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1) ∧ T = Boolean
               | Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer ⟧
  ⟹ P,E ⊢ e⇩1 «bop» e⇩2 :: T"
*)
| WTBinOpEq:
  "⟦ P,E ⊢ e⇩1 :: T⇩1;  P,E ⊢ e⇩2 :: T⇩2; P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1 ⟧
  ⟹ P,E ⊢ e⇩1 «Eq» e⇩2 :: Boolean"

| WTBinOpAdd:
  "⟦ P,E ⊢ e⇩1 :: Integer;  P,E ⊢ e⇩2 :: Integer ⟧
  ⟹ P,E ⊢ e⇩1 «Add» e⇩2 :: Integer"

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

| WTFAcc:
  "⟦ P,E ⊢ e :: Class C;  P ⊢ C sees F:T in D ⟧
  ⟹ P,E ⊢ e∙F{D} :: T"

| WTFAss:
  "⟦ P,E ⊢ e⇩1 :: Class C;  P ⊢ C sees F:T in D;  P,E ⊢ e⇩2 :: T';  P ⊢ T' ≤ T ⟧
  ⟹ P,E ⊢ e⇩1∙F{D}:=e⇩2 :: Void"

| WTCall:
  "⟦ P,E ⊢ e :: Class C;  P ⊢ C sees M:Ts → T = (pns,body) in D;
     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⇩1;  P,E ⊢ e⇩2::T⇩2;
     P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1;  P ⊢ T⇩1 ≤ T⇩2 ⟶ T = T⇩2;  P ⊢ T⇩2 ≤ T⇩1 ⟶ T = T⇩1 ⟧
  ⟹ 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"

| WTTry:
  "⟦ P,E ⊢ e⇩1 :: T;  P,E(V ↦ Class C) ⊢ e⇩2 :: T; is_class P C ⟧
  ⟹ P,E ⊢ try e⇩1 catch(C V) e⇩2 :: T"

― ‹well-typed expression lists›

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

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

(*<*)
(*
lemmas [intro!] = WTNew WTCast WTVal WTVar WTBinOp WTLAss WTFAcc WTFAss WTCall WTBlock WTSeq
                  WTWhile WTThrow WTTry WTNil WTCons
lemmas [intro]  = WTCond1 WTCond2
*)
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)]
(*>*)

lemma [iff]: "(P,E ⊢ [] [::] Ts) = (Ts = [])"
(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)

lemma [iff]: "(P,E ⊢ e#es [::] T#Ts) = (P,E ⊢ e :: T ∧ P,E ⊢ es [::] Ts)"
(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)

lemma [iff]: "(P,E ⊢ (e#es) [::] Ts) =
  (∃U Us. Ts = U#Us ∧ P,E ⊢ e :: U ∧ P,E ⊢ es [::] Us)"
(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)

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)"
(*<*)
proof(induct es⇩1 type:list)
  case (Cons a list)
  let ?lhs = "(∃U Us. Ts = U # Us ∧ P,E ⊢ a :: U ∧
        (∃Ts⇩1 Ts⇩2. Us = Ts⇩1 @ Ts⇩2 ∧ P,E ⊢ list [::] Ts⇩1 ∧ P,E ⊢ es⇩2 [::] Ts⇩2))"
  let ?rhs = "(∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧
        (∃U Us. Ts⇩1 = U # Us ∧ P,E ⊢ a :: U ∧ P,E ⊢ list [::] Us) ∧ P,E ⊢ es⇩2 [::] Ts⇩2)"
  { assume ?lhs
    then have ?rhs by (auto intro: Cons_eq_appendI)
  }
  moreover {
    assume ?rhs
    then have ?lhs by fastforce
  }
  ultimately have "?lhs = ?rhs" by(rule iffI)
  then show ?case by (clarsimp simp: Cons)
qed simp
(*>*)

lemma [iff]: "P,E ⊢ Val v :: T = (typeof v = Some T)"
(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)

lemma [iff]: "P,E ⊢ Var V :: T = (E V = Some T)"
(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)

lemma [iff]: "P,E ⊢ e⇩1;;e⇩2 :: T⇩2 = (∃T⇩1. P,E ⊢ e⇩1::T⇩1 ∧ P,E ⊢ e⇩2::T⇩2)"
(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)

lemma [iff]: "(P,E ⊢ {V:T; e} :: T') = (is_type P T ∧ P,E(V↦T) ⊢ e :: T')"
(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)

(*<*)
inductive_cases WT_elim_cases[elim!]:
  "P,E ⊢ V :=e :: T"
  "P,E ⊢ if (e) e⇩1 else e⇩2 :: T"
  "P,E ⊢ while (e) c :: T"
  "P,E ⊢ throw e :: T"
  "P,E ⊢ try e⇩1 catch(C V) e⇩2 :: T"
  "P,E ⊢ Cast D e :: T"
  "P,E ⊢ a∙F{D} :: T"
  "P,E ⊢ a∙F{D} := v :: T"
  "P,E ⊢ e⇩1 «bop» e⇩2 :: T"
  "P,E ⊢ new C :: T"
  "P,E ⊢ e∙M(ps) :: 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)"
(*<*)
proof(induct rule: WT_WTs_inducts)
  case WTVar then show ?case by(simp add: map_le_def dom_def)
next
  case WTLAss then show ?case by(force simp:map_le_def)
qed fastforce+
(*>*)


lemma WT_fv: "P,E ⊢ e :: T ⟹ fv e ⊆ dom E"
and "P,E ⊢ es [::] Ts ⟹ fvs es ⊆ dom E"
(*<*)
proof(induct rule:WT_WTs.inducts)
  case WTVar then show ?case by fastforce
next
  case WTLAss then show ?case by fastforce
next
  case WTBlock then show ?case by fastforce
next
  case WTTry then show ?case by fastforce
qed simp_all

end
(*>*)