(* Title: Jinja/Compiler/WellType1.thy Author: Tobias Nipkow Copyright 2003 Technische Universitaet Muenchen *) 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 by (simp add:sees_field_is_type[OF _ wf]) 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))" (*<*)by (simp add:wf_J⇩_{1}_mdecl_def)(*>*) abbreviation "wf_J⇩_{1}_prog == wf_prog wf_J⇩_{1}_mdecl" end