Theory WellType

(*  Title:      Jinja/J/WellType.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Well-typedness of Jinja expressions} *}

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

type_synonym
  env  = "vname \<rightharpoonup> ty"

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

| WTCast:
  "[| P,E \<turnstile> e :: Class D;  is_class P C;  P \<turnstile> C \<preceq>⇧* D ∨ P \<turnstile> D \<preceq>⇧* C |]
  ==> P,E \<turnstile> Cast 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> e⇣1 :: T⇣1;  P,E \<turnstile> e⇣2 :: T⇣2;
     case bop of Eq => (P \<turnstile> T⇣1 ≤ T⇣2 ∨ P \<turnstile> T⇣2 ≤ T⇣1) ∧ T = Boolean
               | Add => T⇣1 = Integer ∧ T⇣2 = Integer ∧ T = Integer |]
  ==> P,E \<turnstile> e⇣1 «bop» e⇣2 :: T"
*)
| WTBinOpEq:
  "[| P,E \<turnstile> e⇣1 :: T⇣1;  P,E \<turnstile> e⇣2 :: T⇣2; P \<turnstile> T⇣1 ≤ T⇣2 ∨ P \<turnstile> T⇣2 ≤ T⇣1 |]
  ==> P,E \<turnstile> e⇣1 «Eq» e⇣2 :: Boolean"

| WTBinOpAdd:
  "[| P,E \<turnstile> e⇣1 :: Integer;  P,E \<turnstile> e⇣2 :: Integer |]
  ==> P,E \<turnstile> e⇣1 «Add» e⇣2 :: Integer"

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

| WTFAcc:
  "[| P,E \<turnstile> e :: Class C;  P \<turnstile> C sees F:T in D |]
  ==> P,E \<turnstile> e•F{D} :: T"

| WTFAss:
  "[| P,E \<turnstile> e⇣1 :: Class C;  P \<turnstile> C sees F:T in D;  P,E \<turnstile> e⇣2 :: T';  P \<turnstile> T' ≤ T |]
  ==> P,E \<turnstile> e⇣1•F{D}:=e⇣2 :: Void"

| WTCall:
  "[| P,E \<turnstile> e :: Class C;  P \<turnstile> C sees M:Ts -> T = (pns,body) in D;
     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> e⇣1::T⇣1;  P,E \<turnstile> e⇣2::T⇣2 |]
  ==>  P,E \<turnstile> e⇣1;;e⇣2 :: T⇣2"
| WTCond:
  "[| P,E \<turnstile> e :: Boolean;  P,E \<turnstile> e⇣1::T⇣1;  P,E \<turnstile> e⇣2::T⇣2;
     P \<turnstile> T⇣1 ≤ T⇣2 ∨ P \<turnstile> T⇣2 ≤ T⇣1;  P \<turnstile> T⇣1 ≤ T⇣2 --> T = T⇣2;  P \<turnstile> T⇣2 ≤ T⇣1 --> T = T⇣1 |]
  ==> P,E \<turnstile> if (e) e⇣1 else e⇣2 :: 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"

| WTTry:
  "[| P,E \<turnstile> e⇣1 :: T;  P,E(V \<mapsto> Class C) \<turnstile> e⇣2 :: T; is_class P C |]
  ==> P,E \<turnstile> try e⇣1 catch(C V) e⇣2 :: T"

-- "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"

(*<*)
(*
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 \<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> es⇣1 @ es⇣2 [::] Ts) =
  (∃Ts⇣1 Ts⇣2. Ts = Ts⇣1 @ Ts⇣2 ∧ P,E \<turnstile> es⇣1 [::] Ts⇣1 ∧ P,E \<turnstile> 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 \<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> e⇣1;;e⇣2 :: T⇣2 = (∃T⇣1. P,E \<turnstile> e⇣1::T⇣1 ∧ P,E \<turnstile> e⇣2::T⇣2)"
(*<*)
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> V :=e :: T"
  "P,E \<turnstile> if (e) e⇣1 else e⇣2 :: T"
  "P,E \<turnstile> while (e) c :: T"
  "P,E \<turnstile> throw e :: T"
  "P,E \<turnstile> try e⇣1 catch(C V) e⇣2 :: T"
  "P,E \<turnstile> Cast D e :: T"
  "P,E \<turnstile> a•F{D} :: T"
  "P,E \<turnstile> a•F{D} := v :: T"
  "P,E \<turnstile> e⇣1 «bop» e⇣2 :: T"
  "P,E \<turnstile> new C :: T"
  "P,E \<turnstile> e•M(ps) :: 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(fastforce simp: WTCast)
apply(fastforce simp: WTVal)
apply(simp add: WTVar map_le_def dom_def)
apply(fastforce simp: WTBinOpEq)
apply(fastforce simp: WTBinOpAdd)
apply(force simp:map_le_def)
apply(fastforce simp: WTFAcc)
apply(fastforce simp: WTFAss del:WT_WTs.intros WT_elim_cases)
apply(fastforce simp: WTCall)
apply(fastforce simp: map_le_def WTBlock)
apply(fastforce simp: WTSeq)
apply(fastforce simp: WTCond)
apply(fastforce simp: WTWhile)
apply(fastforce simp: WTThrow)
apply(fastforce simp: WTTry map_le_def dom_def)
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
(*>*)