header {* \isaheader{Well-Formedness of Intermediate Language} *}
theory J1WellForm
imports "../J/JWellForm" J1
begin
subsection "Well-Typedness"
types
env1 = "ty list" --"type environment indexed by variable number"
inductive
WT1 :: "[J1_prog,env1, expr1 , ty ] => bool"
("(_,_ \<turnstile>1/ _ :: _)" [51,51,51]50)
and WTs1 :: "[J1_prog,env1, expr1 list, ty list] => bool"
("(_,_ \<turnstile>1/ _ [::] _)" [51,51,51]50)
for P :: J1_prog
where
WTNew1:
"is_class P C ==>
P,E \<turnstile>1 new C :: Class C"
| WTCast1:
"[| P,E \<turnstile>1 e :: Class D; is_class P C; P \<turnstile> C \<preceq>* D ∨ P \<turnstile> D \<preceq>* C |]
==> P,E \<turnstile>1 Cast C e :: Class C"
| WTVal1:
"typeof v = Some T ==>
P,E \<turnstile>1 Val v :: T"
| WTVar1:
"[| E!i = T; i < size E |]
==> P,E \<turnstile>1 Var i :: T"
| WTBinOp1:
"[| P,E \<turnstile>1 e1 :: T1; P,E \<turnstile>1 e2 :: T2;
case bop of Eq => (P \<turnstile> T1 ≤ T2 ∨ P \<turnstile> T2 ≤ T1) ∧ T = Boolean
| Add => T1 = Integer ∧ T2 = Integer ∧ T = Integer |]
==> P,E \<turnstile>1 e1 «bop» e2 :: T"
| WTLAss1:
"[| E!i = T; i < size E; P,E \<turnstile>1 e :: T'; P \<turnstile> T' ≤ T |]
==> P,E \<turnstile>1 i:=e :: Void"
| WTFAcc1:
"[| P,E \<turnstile>1 e :: Class C; P \<turnstile> C sees F:T in D |]
==> P,E \<turnstile>1 e•F{D} :: T"
| WTFAss1:
"[| P,E \<turnstile>1 e1 :: Class C; P \<turnstile> C sees F:T in D; P,E \<turnstile>1 e2 :: T'; P \<turnstile> T' ≤ T |]
==> P,E \<turnstile>1 e1•F{D} := e2 :: Void"
| WTCall1:
"[| P,E \<turnstile>1 e :: Class C; P \<turnstile> C sees M:Ts' -> T = m in D;
P,E \<turnstile>1 es [::] Ts; P \<turnstile> Ts [≤] Ts' |]
==> P,E \<turnstile>1 e•M(es) :: T"
| WTBlock1:
"[| is_type P T; P,E@[T] \<turnstile>1 e::T' |]
==> P,E \<turnstile>1 {i:T; e} :: T'"
| WTSeq1:
"[| P,E \<turnstile>1 e1::T1; P,E \<turnstile>1 e2::T2 |]
==> P,E \<turnstile>1 e1;;e2 :: T2"
| WTCond1:
"[| P,E \<turnstile>1 e :: Boolean; P,E \<turnstile>1 e1::T1; P,E \<turnstile>1 e2::T2;
P \<turnstile> T1 ≤ T2 ∨ P \<turnstile> T2 ≤ T1; P \<turnstile> T1 ≤ T2 --> T = T2; P \<turnstile> T2 ≤ T1 --> T = T1 |]
==> P,E \<turnstile>1 if (e) e1 else e2 :: T"
| WTWhile1:
"[| P,E \<turnstile>1 e :: Boolean; P,E \<turnstile>1 c::T |]
==> P,E \<turnstile>1 while (e) c :: Void"
| WTThrow1:
"P,E \<turnstile>1 e :: Class C ==>
P,E \<turnstile>1 throw e :: Void"
| WTTry1:
"[| P,E \<turnstile>1 e1 :: T; P,E@[Class C] \<turnstile>1 e2 :: T; is_class P C |]
==> P,E \<turnstile>1 try e1 catch(C i) e2 :: T"
| WTNil1:
"P,E \<turnstile>1 [] [::] []"
| WTCons1:
"[| P,E \<turnstile>1 e :: T; P,E \<turnstile>1 es [::] Ts |]
==> P,E \<turnstile>1 e#es [::] T#Ts"
declare WT1_WTs1.intros[intro!]
declare WTNil1[iff]
lemmas WT1_WTs1_induct = WT1_WTs1.induct [split_format (complete)]
and WT1_WTs1_inducts = WT1_WTs1.inducts [split_format (complete)]
inductive_cases eee[elim!]:
"P,E \<turnstile>1 Val v :: T"
"P,E \<turnstile>1 Var i :: T"
"P,E \<turnstile>1 Cast D e :: T"
"P,E \<turnstile>1 i:=e :: T"
"P,E \<turnstile>1 {i:U; e} :: T"
"P,E \<turnstile>1 e1;;e2 :: T"
"P,E \<turnstile>1 if (e) e1 else e2 :: T"
"P,E \<turnstile>1 while (e) c :: T"
"P,E \<turnstile>1 throw e :: T"
"P,E \<turnstile>1 try e1 catch(C i) e2 :: T"
"P,E \<turnstile>1 e•F{D} :: T"
"P,E \<turnstile>1 e1•F{D}:=e2 :: T"
"P,E \<turnstile>1 e1 «bop» e2 :: T"
"P,E \<turnstile>1 new C :: T"
"P,E \<turnstile>1 e•M(es) :: T"
"P,E \<turnstile>1 [] [::] Ts"
"P,E \<turnstile>1 e#es [::] Ts"
lemma WTs1_same_size: "!!Ts. P,E \<turnstile>1 es [::] Ts ==> size es = size Ts"
by (induct es type:list) auto
lemma WT1_unique:
"P,E \<turnstile>1 e :: T1 ==> (!!T2. P,E \<turnstile>1 e :: T2 ==> T1 = T2)" and
"P,E \<turnstile>1 es [::] Ts1 ==> (!!Ts2. P,E \<turnstile>1 es [::] Ts2 ==> Ts1 = Ts2)"
apply(induct rule:WT1_WTs1.inducts)
apply blast
apply blast
apply clarsimp
apply blast
apply clarsimp
apply(case_tac bop)
apply clarsimp
apply clarsimp
apply blast
apply (blast dest:sees_field_idemp sees_field_fun)
apply blast
apply (blast dest:sees_method_idemp sees_method_fun)
apply blast
apply blast
apply blast
apply blast
apply clarify
apply blast
apply blast
apply blast
done
lemma assumes wf: "wf_prog p P"
shows WT1_is_type: "P,E \<turnstile>1 e :: T ==> set E ⊆ types P ==> is_type P T"
and "P,E \<turnstile>1 es [::] Ts ==> True"
apply(induct rule:WT1_WTs1.inducts)
apply simp
apply simp
apply (simp add:typeof_lit_is_type)
apply (blast intro:nth_mem)
apply(simp split:bop.splits)
apply simp
apply (simp add:sees_field_is_type[OF _ wf])
apply simp
apply(fastsimp dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
apply simp
apply simp
apply blast
apply simp
apply simp
apply simp
apply simp
apply simp
done
subsection{* Well-formedness*}
--"Indices in blocks increase by 1"
consts
\<B> :: "expr1 => nat => bool"
\<B>s :: "expr1 list => nat => bool"
primrec
"\<B> (new C) i = True"
"\<B> (Cast C e) i = \<B> e i"
"\<B> (Val v) i = True"
"\<B> (e1 «bop» e2) i = (\<B> e1 i ∧ \<B> e2 i)"
"\<B> (Var j) i = True"
"\<B> (e•F{D}) i = \<B> e i"
"\<B> (j:=e) i = \<B> e i"
"\<B> (e1•F{D} := e2) i = (\<B> e1 i ∧ \<B> e2 i)"
"\<B> (e•M(es)) i = (\<B> e i ∧ \<B>s es i)"
"\<B> ({j:T ; e}) i = (i = j ∧ \<B> e (i+1))"
"\<B> (e1;;e2) i = (\<B> e1 i ∧ \<B> e2 i)"
"\<B> (if (e) e1 else e2) i = (\<B> e i ∧ \<B> e1 i ∧ \<B> e2 i)"
"\<B> (throw e) i = \<B> e i"
"\<B> (while (e) c) i = (\<B> e i ∧ \<B> c i)"
"\<B> (try e1 catch(C j) e2) i = (\<B> e1 i ∧ i=j ∧ \<B> e2 (i+1))"
"\<B>s [] i = True"
"\<B>s (e#es) i = (\<B> e i ∧ \<B>s es i)"
constdefs
wf_J1_mdecl :: "J1_prog => cname => expr1 mdecl => bool"
"wf_J1_mdecl P C ≡ λ(M,Ts,T,body).
(∃T'. P,Class C#Ts \<turnstile>1 body :: T' ∧ P \<turnstile> T' ≤ T) ∧
\<D> body ⌊{..size Ts}⌋ ∧ \<B> body (size Ts + 1)"
lemma wf_J1_mdecl[simp]:
"wf_J1_mdecl P C (M,Ts,T,body) ≡
((∃T'. P,Class C#Ts \<turnstile>1 body :: T' ∧ P \<turnstile> T' ≤ T) ∧
\<D> body ⌊{..size Ts}⌋ ∧ \<B> body (size Ts + 1))"
by (simp add:wf_J1_mdecl_def)
abbreviation "wf_J1_prog == wf_prog wf_J1_mdecl"
end