# Theory J1WellForm

```(*  Title:      Jinja/Compiler/WellType1.thy

Author:     Tobias Nipkow
*)

section ‹Well-Formedness of Intermediate Language›

theory J1WellForm
imports "../J/JWellForm" J1
begin

subsection "Well-Typedness"

type_synonym
env⇩1  = "ty list"   ― ‹type environment indexed by variable number›

inductive
WT⇩1 :: "[J⇩1_prog,env⇩1, expr⇩1     , ty     ] ⇒ bool"
("(_,_ ⊢⇩1/ _ :: _)"   [51,51,51]50)
and WTs⇩1 :: "[J⇩1_prog,env⇩1, expr⇩1 list, ty list] ⇒ bool"
("(_,_ ⊢⇩1/ _ [::] _)" [51,51,51]50)
for P :: J⇩1_prog
where

WTNew⇩1:
"is_class P C  ⟹
P,E ⊢⇩1 new C :: Class C"

| WTCast⇩1:
"⟦ P,E ⊢⇩1 e :: Class D;  is_class P C;  P ⊢ C ≼⇧* D ∨ P ⊢ D ≼⇧* C ⟧
⟹ P,E ⊢⇩1 Cast C e :: Class C"

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

| WTVar⇩1:
"⟦ E!i = T; i < size E ⟧
⟹ P,E ⊢⇩1 Var i :: T"

| WTBinOp⇩1:
"⟦ P,E ⊢⇩1 e⇩1 :: T⇩1;  P,E ⊢⇩1 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 ⊢⇩1 e⇩1 «bop» e⇩2 :: T"

| WTLAss⇩1:
"⟦ E!i = T;  i < size E; P,E ⊢⇩1 e :: T';  P ⊢ T' ≤ T ⟧
⟹ P,E ⊢⇩1 i:=e :: Void"

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

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

| WTCall⇩1:
"⟦ P,E ⊢⇩1 e :: Class C; P ⊢ C sees M:Ts' → T = m in D;
P,E ⊢⇩1 es [::] Ts;  P ⊢ Ts [≤] Ts' ⟧
⟹ P,E ⊢⇩1 e∙M(es) :: T"

| WTBlock⇩1:
"⟦ is_type P T; P,E@[T] ⊢⇩1 e::T' ⟧
⟹  P,E ⊢⇩1 {i:T; e} :: T'"

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

| WTCond⇩1:
"⟦ P,E ⊢⇩1 e :: Boolean;  P,E ⊢⇩1 e⇩1::T⇩1;  P,E ⊢⇩1 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 ⊢⇩1 if (e) e⇩1 else e⇩2 :: T"

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

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

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

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

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

(*<*)
declare  WT⇩1_WTs⇩1.intros[intro!]
declare WTNil⇩1[iff]

lemmas WT⇩1_WTs⇩1_induct = WT⇩1_WTs⇩1.induct [split_format (complete)]
and WT⇩1_WTs⇩1_inducts = WT⇩1_WTs⇩1.inducts [split_format (complete)]

inductive_cases eee[elim!]:
"P,E ⊢⇩1 Val v :: T"
"P,E ⊢⇩1 Var i :: T"
"P,E ⊢⇩1 Cast D e :: T"
"P,E ⊢⇩1 i:=e :: T"
"P,E ⊢⇩1 {i:U; e} :: T"
"P,E ⊢⇩1 e⇩1;;e⇩2 :: T"
"P,E ⊢⇩1 if (e) e⇩1 else e⇩2 :: T"
"P,E ⊢⇩1 while (e) c :: T"
"P,E ⊢⇩1 throw e :: T"
"P,E ⊢⇩1 try e⇩1 catch(C i) e⇩2 :: T"
"P,E ⊢⇩1 e∙F{D} :: T"
"P,E ⊢⇩1 e⇩1∙F{D}:=e⇩2 :: T"
"P,E ⊢⇩1 e⇩1 «bop» e⇩2 :: T"
"P,E ⊢⇩1 new C :: T"
"P,E ⊢⇩1 e∙M(es) :: T"
"P,E ⊢⇩1 [] [::] Ts"
"P,E ⊢⇩1 e#es [::] Ts"
(*>*)

lemma WTs⇩1_same_size: "⋀Ts. P,E ⊢⇩1 es [::] Ts ⟹ size es = size Ts"
(*<*)by (induct es type:list) auto(*>*)

lemma WT⇩1_unique:
"P,E ⊢⇩1 e :: T⇩1 ⟹ (⋀T⇩2. P,E ⊢⇩1 e :: T⇩2 ⟹ T⇩1 = T⇩2)" and
"P,E ⊢⇩1 es [::] Ts⇩1 ⟹ (⋀Ts⇩2. P,E ⊢⇩1 es [::] Ts⇩2 ⟹ Ts⇩1 = Ts⇩2)"
(*<*)
proof(induct rule:WT⇩1_WTs⇩1.inducts)
case WTVal⇩1 then show ?case by clarsimp
next
case (WTBinOp⇩1 E e⇩1 T⇩1 e⇩2 T⇩2 bop T)
then show ?case by(case_tac bop) force+
next
case WTFAcc⇩1 then show ?case
by (blast dest:sees_field_idemp sees_field_fun)
next
case WTCall⇩1 then show ?case
by (blast dest:sees_method_idemp sees_method_fun)
qed blast+
(*>*)

lemma assumes wf: "wf_prog p P"
shows WT⇩1_is_type: "P,E ⊢⇩1 e :: T ⟹ set E ⊆ types P ⟹ is_type P T"
and "P,E ⊢⇩1 es [::] Ts ⟹ True"
(*<*)
proof(induct rule:WT⇩1_WTs⇩1.inducts)
case WTVal⇩1 then show ?case by (simp add:typeof_lit_is_type)
next
case WTVar⇩1 then show ?case by (blast intro:nth_mem)
next
case WTBinOp⇩1 then show ?case by (simp split:bop.splits)
next
case WTFAcc⇩1 then show ?case
next
case WTCall⇩1 then show ?case
by (fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
next
case WTCond⇩1 then show ?case by blast
qed simp+
(*>*)

subsection‹Well-formedness›

― ‹Indices in blocks increase by 1›

primrec ℬ :: "expr⇩1 ⇒ nat ⇒ bool"
and ℬs :: "expr⇩1 list ⇒ nat ⇒ bool" where
"ℬ (new C) i = True" |
"ℬ (Cast C e) i = ℬ e i" |
"ℬ (Val v) i = True" |
"ℬ (e⇩1 «bop» e⇩2) i = (ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (Var j) i = True" |
"ℬ (e∙F{D}) i = ℬ e i" |
"ℬ (j:=e) i = ℬ e i" |
"ℬ (e⇩1∙F{D} := e⇩2) i = (ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (e∙M(es)) i = (ℬ e i ∧ ℬs es i)" |
"ℬ ({j:T ; e}) i = (i = j ∧ ℬ e (i+1))" |
"ℬ (e⇩1;;e⇩2) i = (ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (if (e) e⇩1 else e⇩2) i = (ℬ e i ∧ ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (throw e) i = ℬ e i" |
"ℬ (while (e) c) i = (ℬ e i ∧ ℬ c i)" |
"ℬ (try e⇩1 catch(C j) e⇩2) i = (ℬ e⇩1 i ∧ i=j ∧ ℬ e⇩2 (i+1))" |

"ℬs [] i = True" |
"ℬs (e#es) i = (ℬ e i ∧ ℬs es i)"

definition wf_J⇩1_mdecl :: "J⇩1_prog ⇒ cname ⇒ expr⇩1 mdecl ⇒ bool"
where
"wf_J⇩1_mdecl P C  ≡  λ(M,Ts,T,body).
(∃T'. P,Class C#Ts ⊢⇩1 body :: T' ∧ P ⊢ T' ≤ T) ∧
𝒟 body ⌊{..size Ts}⌋ ∧ ℬ body (size Ts + 1)"

lemma wf_J⇩1_mdecl[simp]:
"wf_J⇩1_mdecl P C (M,Ts,T,body) ≡
((∃T'. P,Class C#Ts ⊢⇩1 body :: T' ∧ P ⊢ T' ≤ T) ∧
𝒟 body ⌊{..size Ts}⌋ ∧ ℬ body (size Ts + 1))"