wenzelm@12857: (*  Title:      HOL/Bali/WellType.thy
schirmer@12854:     ID:         $Id$
schirmer@12854:     Author:     David von Oheimb
schirmer@12854: *)
schirmer@12854: header {* Well-typedness of Java programs *}
schirmer@12854: 
haftmann@16417: theory WellType imports DeclConcepts begin
schirmer@12854: 
schirmer@12854: text {*
schirmer@12854: improvements over Java Specification 1.0:
schirmer@12854: \begin{itemize}
schirmer@12854: \item methods of Object can be called upon references of interface or array type
schirmer@12854: \end{itemize}
schirmer@12854: simplifications:
schirmer@12854: \begin{itemize}
schirmer@12854: \item the type rules include all static checks on statements and expressions, 
schirmer@12854:       e.g. definedness of names (of parameters, locals, fields, methods)
schirmer@12854: \end{itemize}
schirmer@12854: design issues:
schirmer@12854: \begin{itemize}
schirmer@12854: \item unified type judgment for statements, variables, expressions, 
schirmer@12854:       expression lists
schirmer@12854: \item statements are typed like expressions with dummy type Void
schirmer@12854: \item the typing rules take an extra argument that is capable of determining 
schirmer@12854:   the dynamic type of objects. Therefore, they can be used for both 
schirmer@12854:   checking static types and determining runtime types in transition semantics.
schirmer@12854: \end{itemize}
schirmer@12854: *}
schirmer@12854: 
schirmer@12854: types	lenv
schirmer@13688: 	= "(lname, ty) table"  --{* local variables, including This and Result*}
schirmer@12854: 
schirmer@12854: record env = 
schirmer@13688:          prg:: "prog"    --{* program *}
schirmer@13688:          cls:: "qtname"  --{* current package and class name *}
schirmer@13688:          lcl:: "lenv"    --{* local environment *}     
schirmer@12854:   
schirmer@12854: translations
schirmer@12854:   "lenv" <= (type) "(lname, ty) table"
schirmer@12854:   "lenv" <= (type) "lname \<Rightarrow> ty option"
schirmer@12854:   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
schirmer@12854:   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
schirmer@12854: 
schirmer@12854: 
schirmer@12854: 
schirmer@12854: syntax
schirmer@13688:   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
schirmer@13688: translations 
schirmer@12854:   "pkg e" == "pid (cls e)"
schirmer@12854: 
schirmer@12854: section "Static overloading: maximally specific methods "
schirmer@12854: 
schirmer@12854: types
schirmer@12854:   emhead = "ref_ty \<times> mhead"
schirmer@12854: 
schirmer@13688: --{* Some mnemotic selectors for emhead *}
schirmer@12854: constdefs 
schirmer@12854:   "declrefT" :: "emhead \<Rightarrow> ref_ty"
schirmer@12854:   "declrefT \<equiv> fst"
schirmer@12854: 
schirmer@12854:   "mhd"     :: "emhead \<Rightarrow> mhead"
schirmer@12854:   "mhd \<equiv> snd"
schirmer@12854: 
schirmer@12854: lemma declrefT_simp[simp]:"declrefT (r,m) = r"
schirmer@12854: by (simp add: declrefT_def)
schirmer@12854: 
schirmer@12854: lemma mhd_simp[simp]:"mhd (r,m) = m"
schirmer@12854: by (simp add: mhd_def)
schirmer@12854: 
schirmer@12854: lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
schirmer@12854: by (cases m) (simp add: member_is_static_simp mhd_def)
schirmer@12854: 
schirmer@12854: lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
schirmer@12854: by (cases m) simp
schirmer@12854: 
schirmer@12854: lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
schirmer@12854: by (cases m) simp
schirmer@12854: 
schirmer@12854: lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
schirmer@12854: by (cases m) simp
schirmer@12854: 
schirmer@12854: consts
schirmer@12854:   cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
schirmer@12854:   Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
schirmer@12854:   accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
schirmer@12854:   mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
schirmer@12854: defs
schirmer@12854:  cmheads_def:
schirmer@12854: "cmheads G S C 
schirmer@12854:   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
schirmer@12854:   Objectmheads_def:
schirmer@12854: "Objectmheads G S  
schirmer@12854:   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
schirmer@12854:     ` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
schirmer@12854:   accObjectmheads_def:
schirmer@12854: "accObjectmheads G S T
schirmer@12854:    \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
schirmer@12854:         then Objectmheads G S
schirmer@12854:         else \<lambda>sig. {}"
schirmer@12854: primrec
schirmer@12854: "mheads G S  NullT     = (\<lambda>sig. {})"
schirmer@12854: "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
schirmer@12854:                          ` accimethds G (pid S) I sig \<union> 
schirmer@12854:                            accObjectmheads G S (IfaceT I) sig)"
schirmer@12854: "mheads G S (ClassT C) = cmheads G S C"
schirmer@12854: "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
schirmer@12854: 
schirmer@12854: constdefs
schirmer@13688:   --{* applicable methods, cf. 15.11.2.1 *}
schirmer@12854:   appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
schirmer@12854:  "appl_methds G S rt \<equiv> \<lambda> sig. 
schirmer@12854:       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
schirmer@12854:                            G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
schirmer@12854: 
schirmer@13688:   --{* more specific methods, cf. 15.11.2.2 *}
schirmer@12854:   more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
schirmer@12854:  "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
schirmer@12854: (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
schirmer@12854: 
schirmer@13688:   --{* maximally specific methods, cf. 15.11.2.2 *}
schirmer@12854:    max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
schirmer@12854: 
schirmer@12854:  "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
schirmer@12854: 		      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma max_spec2appl_meths: 
schirmer@12854:   "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
schirmer@12854: by (auto simp: max_spec_def)
schirmer@12854: 
schirmer@12854: lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
schirmer@12854:    mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
schirmer@12854: by (auto simp: appl_methds_def)
schirmer@12854: 
schirmer@12854: lemma max_spec2mheads: 
schirmer@12854: "max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
schirmer@12854:  \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
schirmer@12854: apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: constdefs
schirmer@12854:   empty_dt :: "dyn_ty"
schirmer@12854:  "empty_dt \<equiv> \<lambda>a. None"
schirmer@12854: 
schirmer@12854:   invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
schirmer@12925: "invmode m e \<equiv> if is_static m 
schirmer@12925:                   then Static 
schirmer@12925:                   else if e=Super then SuperM else IntVir"
schirmer@12854: 
schirmer@12854: lemma invmode_nonstatic [simp]: 
schirmer@12854:   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
schirmer@12854: apply (unfold invmode_def)
schirmer@12925: apply (simp (no_asm) add: member_is_static_simp)
schirmer@12925: done
schirmer@12925: 
schirmer@12925: 
schirmer@12925: lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
schirmer@12925: apply (unfold invmode_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12925: lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
schirmer@12854: apply (unfold invmode_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Null_staticD: 
schirmer@12925:   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
schirmer@12854: apply (clarsimp simp add: invmode_IntVir_eq)
schirmer@12854: done
schirmer@12854: 
schirmer@13688: section "Typing for unary operations"
schirmer@13688: 
schirmer@13337: consts unop_type :: "unop \<Rightarrow> prim_ty"
schirmer@13337: primrec 
schirmer@13337: "unop_type UPlus   = Integer"
schirmer@13337: "unop_type UMinus  = Integer"
schirmer@13337: "unop_type UBitNot = Integer"
schirmer@13337: "unop_type UNot    = Boolean"    
schirmer@12854: 
schirmer@13337: consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
schirmer@13337: primrec
schirmer@13337: "wt_unop UPlus   t = (t = PrimT Integer)"
schirmer@13337: "wt_unop UMinus  t = (t = PrimT Integer)"
schirmer@13337: "wt_unop UBitNot t = (t = PrimT Integer)"
schirmer@13337: "wt_unop UNot    t = (t = PrimT Boolean)"
schirmer@13337: 
schirmer@13688: section "Typing for binary operations"
schirmer@13688: 
schirmer@13337: consts binop_type :: "binop \<Rightarrow> prim_ty"
schirmer@13337: primrec
schirmer@13337: "binop_type Mul      = Integer"     
schirmer@13337: "binop_type Div      = Integer"
schirmer@13337: "binop_type Mod      = Integer"
schirmer@13337: "binop_type Plus     = Integer"
schirmer@13337: "binop_type Minus    = Integer"
schirmer@13337: "binop_type LShift   = Integer"
schirmer@13337: "binop_type RShift   = Integer"
schirmer@13337: "binop_type RShiftU  = Integer"
schirmer@13337: "binop_type Less     = Boolean"
schirmer@13337: "binop_type Le       = Boolean"
schirmer@13337: "binop_type Greater  = Boolean"
schirmer@13337: "binop_type Ge       = Boolean"
schirmer@13337: "binop_type Eq       = Boolean"
schirmer@13337: "binop_type Neq      = Boolean"
schirmer@13337: "binop_type BitAnd   = Integer"
schirmer@13337: "binop_type And      = Boolean"
schirmer@13337: "binop_type BitXor   = Integer"
schirmer@13337: "binop_type Xor      = Boolean"
schirmer@13337: "binop_type BitOr    = Integer"
schirmer@13337: "binop_type Or       = Boolean"
schirmer@13384: "binop_type CondAnd  = Boolean"
schirmer@13384: "binop_type CondOr   = Boolean"
schirmer@13337: 
schirmer@13337: consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
schirmer@13337: primrec
schirmer@13337: "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
schirmer@13337: "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
schirmer@13337: "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
schirmer@13337: "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
schirmer@13337: "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
schirmer@13337: "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
schirmer@13384: "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
schirmer@13384: "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
schirmer@13337: 
schirmer@13688: section "Typing for terms"
schirmer@13384: 
schirmer@12854: types tys  =        "ty + ty list"
schirmer@12854: translations
schirmer@12854:   "tys"   <= (type) "ty + ty list"
schirmer@12854: 
berghofe@21765: 
berghofe@21765: inductive2 
berghofe@21765:   wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
berghofe@21765:   and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
berghofe@21765:   and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
berghofe@21765:   and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
berghofe@21765:   and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
berghofe@21765:     ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
berghofe@21765: where
berghofe@21765: 
berghofe@21765:   "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
berghofe@21765: | "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T"
berghofe@21765: | "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
berghofe@21765: | "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
berghofe@21765: 
berghofe@21765: --{* well-typed statements *}
berghofe@21765: 
berghofe@21765: | Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
berghofe@21765: 
berghofe@21765: | Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
berghofe@21765:   --{* cf. 14.6 *}
berghofe@21765: | Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
berghofe@21765:                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
berghofe@21765: 
berghofe@21765: | Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
berghofe@21765: 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
berghofe@21765: 
berghofe@21765:   --{* cf. 14.8 *}
berghofe@21765: | If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
berghofe@21765: 	  E,dt\<Turnstile>c1\<Colon>\<surd>;
berghofe@21765: 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
berghofe@21765: 
berghofe@21765:   --{* cf. 14.10 *}
berghofe@21765: | Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
berghofe@21765: 	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
berghofe@21765:   --{* cf. 14.13, 14.15, 14.16 *}
berghofe@21765: | Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
schirmer@12854: 
berghofe@21765:   --{* cf. 14.16 *}
berghofe@21765: | Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
berghofe@21765: 	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
berghofe@21765:   --{* cf. 14.18 *}
berghofe@21765: | Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
berghofe@21765: 	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
berghofe@21765:           \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
berghofe@21765: 
berghofe@21765:   --{* cf. 14.18 *}
berghofe@21765: | Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
berghofe@21765: 
berghofe@21765: | Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
berghofe@21765:   --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
berghofe@21765:      The class isn't necessarily accessible from the points @{term Init} 
berghofe@21765:      is called. Therefor we only demand @{term is_class} and not 
berghofe@21765:      @{term is_acc_class} here. 
berghofe@21765:    *}
berghofe@21765: 
berghofe@21765: --{* well-typed expressions *}
berghofe@21765: 
berghofe@21765:   --{* cf. 15.8 *}
berghofe@21765: | NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
berghofe@21765:   --{* cf. 15.9 *}
berghofe@21765: | NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
berghofe@21765: 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.15 *}
berghofe@21765: | Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
berghofe@21765: 	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.19.2 *}
berghofe@21765: | Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
berghofe@21765: 	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.7.1 *}
berghofe@21765: | Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Lit x\<Colon>-T"
schirmer@12854: 
berghofe@21765: | UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
berghofe@21765:           \<Longrightarrow>
berghofe@21765: 	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
berghofe@21765:   
berghofe@21765: | BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
berghofe@21765:            T=PrimT (binop_type binop)\<rbrakk> 
berghofe@21765:            \<Longrightarrow>
berghofe@21765: 	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
berghofe@21765:   
berghofe@21765:   --{* cf. 15.10.2, 15.11.1 *}
berghofe@21765: | Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
berghofe@21765: 	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.13.1, 15.10.1, 15.12 *}
berghofe@21765: | Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Acc va\<Colon>-T"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.25, 15.25.1 *}
berghofe@21765: | Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
berghofe@21765: 	  E,dt\<Turnstile>v \<Colon>-T';
berghofe@21765: 	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>va:=v\<Colon>-T'"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.24 *}
berghofe@21765: | Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
berghofe@21765: 	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
berghofe@21765: 	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
berghofe@21765: | Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
berghofe@21765: 	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
berghofe@21765: 	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
berghofe@21765:             = {((statDeclT,m),pTs')}
berghofe@21765:          \<rbrakk> \<Longrightarrow>
berghofe@21765: 		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
schirmer@12854: 
berghofe@21765: | Methd: "\<lbrakk>is_class (prg E) C;
berghofe@21765: 	  methd (prg E) C sig = Some m;
berghofe@21765: 	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
berghofe@21765:  --{* The class @{term C} is the dynamic class of the method call 
berghofe@21765:     (cf. Eval.thy). 
berghofe@21765:     It hasn't got to be directly accessible from the current package 
berghofe@21765:     @{term "(pkg E)"}. 
berghofe@21765:     Only the static class must be accessible (enshured indirectly by 
berghofe@21765:     @{term Call}). 
berghofe@21765:     Note that l is just a dummy value. It is only used in the smallstep 
berghofe@21765:     semantics. To proof typesafety directly for the smallstep semantics 
berghofe@21765:     we would have to assume conformance of l here!
berghofe@21765:   *}
berghofe@21765: 
berghofe@21765: | Body:	"\<lbrakk>is_class (prg E) D;
berghofe@21765: 	  E,dt\<Turnstile>blk\<Colon>\<surd>;
berghofe@21765: 	  (lcl E) Result = Some T;
berghofe@21765:           is_type (prg E) T\<rbrakk> \<Longrightarrow>
berghofe@21765:    					 E,dt\<Turnstile>Body D blk\<Colon>-T"
berghofe@21765: --{* The class @{term D} implementing the method must not directly be 
berghofe@21765:      accessible  from the current package @{term "(pkg E)"}, but can also 
berghofe@21765:      be indirectly accessible due to inheritance (enshured in @{term Call})
berghofe@21765:     The result type hasn't got to be accessible in Java! (If it is not 
berghofe@21765:     accessible you can only assign it to Object).
berghofe@21765:     For dummy value l see rule @{term Methd}. 
berghofe@21765:    *}
berghofe@21765: 
berghofe@21765: --{* well-typed variables *}
berghofe@21765: 
berghofe@21765:   --{* cf. 15.13.1 *}
berghofe@21765: | LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>LVar vn\<Colon>=T"
berghofe@21765:   --{* cf. 15.10.1 *}
berghofe@21765: | FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
berghofe@21765: 	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
berghofe@21765: 			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
berghofe@21765:   --{* cf. 15.12 *}
berghofe@21765: | AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
berghofe@21765: 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>e.[i]\<Colon>=T"
berghofe@21765: 
berghofe@21765: 
berghofe@21765: --{* well-typed expression lists *}
berghofe@21765: 
berghofe@21765:   --{* cf. 15.11.??? *}
berghofe@21765: | Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
berghofe@21765: 
berghofe@21765:   --{* cf. 15.11.??? *}
berghofe@21765: | Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
berghofe@21765: 	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
berghofe@21765: 					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
berghofe@21765: 
schirmer@12854: 
schirmer@12854: syntax (* for purely static typing *)
schirmer@12854:   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
schirmer@12854:   wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
schirmer@12854:   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
schirmer@12854:   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
schirmer@12854:   ty_exprs_:: "env \<Rightarrow> [expr list,
schirmer@12854: 		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
schirmer@12854: 
schirmer@12854: syntax (xsymbols)
schirmer@12854:   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
schirmer@12854:   wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
schirmer@12854:   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
schirmer@12854:   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
schirmer@12854:   ty_exprs_ :: "env \<Rightarrow> [expr list,
schirmer@12854: 		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
schirmer@12854: 
schirmer@12854: translations
schirmer@12854: 	"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
schirmer@13688:         "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)"
schirmer@13688: 	"E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>Inl T"
schirmer@13688: 	"E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>Inl T"
schirmer@13688: 	"E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
schirmer@12854: 
schirmer@13337: 
schirmer@12854: declare not_None_eq [simp del] 
schirmer@12854: declare split_if [split del] split_if_asm [split del]
schirmer@12854: declare split_paired_All [simp del] split_paired_Ex [simp del]
schirmer@12854: ML_setup {*
wenzelm@17876: change_simpset (fn ss => ss delloop "split_all_tac")
schirmer@12854: *}
schirmer@13688: 
berghofe@21765: inductive_cases2 wt_elim_cases [cases set]:
schirmer@12854: 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
schirmer@12925: 	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
schirmer@13337:         "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
schirmer@13337:         "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
schirmer@12925: 	"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
schirmer@12854: 	"E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
schirmer@12854: 	"E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
schirmer@12854: 	"E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
schirmer@12854: 	"E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
schirmer@12854: 	"E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
schirmer@12854:         "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
schirmer@12854: 	"E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
schirmer@12854: 	"E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
schirmer@13688:         "E,dt\<Turnstile>In1r (Jmp jump)              \<Colon>x"
schirmer@12854: 	"E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
schirmer@12854: 	"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
schirmer@12854: 	"E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
schirmer@12854: 	"E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
schirmer@12854: declare not_None_eq [simp] 
schirmer@12854: declare split_if [split] split_if_asm [split]
schirmer@12854: declare split_paired_All [simp] split_paired_Ex [simp]
schirmer@12854: ML_setup {*
wenzelm@17876: change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
schirmer@12854: *}
schirmer@12854: 
schirmer@12854: lemma is_acc_class_is_accessible: 
schirmer@12854:   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
schirmer@12854: by (auto simp add: is_acc_class_def)
schirmer@12854: 
schirmer@12854: lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
schirmer@12854: by (auto simp add: is_acc_iface_def)
schirmer@12854: 
wenzelm@13524: lemma is_acc_iface_Iface_is_accessible: 
schirmer@12854:   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
schirmer@12854: by (auto simp add: is_acc_iface_def)
schirmer@12854: 
schirmer@12854: lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
schirmer@12854: by (auto simp add: is_acc_type_def)
schirmer@12854: 
wenzelm@13524: lemma is_acc_iface_is_accessible:
wenzelm@13524:   "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
schirmer@12854: by (auto simp add: is_acc_type_def)
schirmer@12854: 
schirmer@12854: lemma wt_Methd_is_methd: 
schirmer@12854:   "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
schirmer@12854: apply (erule_tac wt_elim_cases)
schirmer@12854: apply clarsimp
schirmer@12854: apply (erule is_methdI, assumption)
schirmer@12854: done
schirmer@12854: 
schirmer@13688: 
schirmer@13688: text {* Special versions of some typing rules, better suited to pattern 
schirmer@13688:         match the conclusion (no selectors in the conclusion)
schirmer@13688: *}
schirmer@12854: 
schirmer@12854: lemma wt_Call: 
schirmer@12854: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
schirmer@12854:   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
schirmer@12925:     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
schirmer@12925:  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
schirmer@12854: by (auto elim: wt.Call)
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma invocationTypeExpr_noClassD: 
schirmer@12854: "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
schirmer@12854:  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
schirmer@12854: proof -
schirmer@12854:   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
schirmer@12854:   show ?thesis
schirmer@12854:   proof (cases "e=Super")
schirmer@12854:     case True
schirmer@12854:     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
schirmer@12854:     then show ?thesis by blast
schirmer@12854:   next 
schirmer@12854:     case False then show ?thesis 
schirmer@12854:       by (auto simp add: invmode_def split: split_if_asm)
schirmer@12854:   qed
schirmer@12854: qed
schirmer@12854: 
schirmer@12854: lemma wt_Super: 
schirmer@12854: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
schirmer@12854: \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
schirmer@12854: by (auto elim: wt.Super)
schirmer@12854: 
schirmer@12925: lemma wt_FVar:	
schirmer@12925: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
schirmer@12925:   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
schirmer@12925: \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
schirmer@12925: by (auto dest: wt.FVar)
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
schirmer@12854: by (auto elim: wt_elim_cases intro: "wt.Init")
schirmer@12854: 
schirmer@12854: declare wt.Skip [iff]
schirmer@12854: 
schirmer@12854: lemma wt_StatRef: 
schirmer@12854:   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
schirmer@12854: apply (rule wt.Cast)
schirmer@12854: apply  (rule wt.Lit)
schirmer@12854: apply   (simp (no_asm))
schirmer@12854: apply  (simp (no_asm_simp))
schirmer@12854: apply (rule cast.widen)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma wt_Inj_elim: 
schirmer@12854:   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
schirmer@12854:                        In1 ec \<Rightarrow> (case ec of 
schirmer@12854:                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
schirmer@12854:                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
schirmer@12854:                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
schirmer@12854:                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
schirmer@12854: apply (erule wt.induct)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@13688: --{* In the special syntax to distinguish the typing judgements for expressions, 
schirmer@13688:      statements, variables and expression lists the kind of term corresponds
schirmer@13688:      to the kind of type in the end e.g. An statement (injection @{term In3} 
schirmer@13688:     into terms, always has type void (injection @{term Inl} into the generalised
schirmer@13688:     types. The following simplification procedures establish these kinds of
schirmer@13688:     correlation. 
schirmer@13688:  *}
schirmer@13688: 
berghofe@21765: lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)"
berghofe@21765:   by (auto, frule wt_Inj_elim, auto)
berghofe@21765: 
berghofe@21765: lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)"
berghofe@21765:   by (auto, frule wt_Inj_elim, auto)
berghofe@21765: 
berghofe@21765: lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)"
berghofe@21765:   by (auto, frule wt_Inj_elim, auto)
berghofe@21765: 
berghofe@21765: lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
berghofe@21765:   by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
berghofe@21765: 
schirmer@12854: ML {*
berghofe@21765: fun wt_fun name lhs =
schirmer@12854: let
schirmer@12854:   fun is_Inj (Const (inj,_) $ _) = true
schirmer@12854:     | is_Inj _                   = false
berghofe@21765:   fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x
schirmer@12854: in
wenzelm@13462:   cond_simproc name lhs pred (thm name)
schirmer@12854: end
schirmer@12854: 
berghofe@21765: val wt_expr_proc  = wt_fun "wt_expr_eq"  "E,dt\<Turnstile>In1l t\<Colon>U";
berghofe@21765: val wt_var_proc   = wt_fun "wt_var_eq"   "E,dt\<Turnstile>In2 t\<Colon>U";
berghofe@21765: val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\<Turnstile>In3 t\<Colon>U";
berghofe@21765: val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "E,dt\<Turnstile>In1r t\<Colon>U";
schirmer@12854: *}
schirmer@12854: 
schirmer@12854: ML {*
schirmer@12854: Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
schirmer@12854: *}
schirmer@12854: 
schirmer@13688: lemma wt_elim_BinOp:
schirmer@13688:   "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
schirmer@13688:     \<And>T1 T2 T3.
schirmer@13688:        \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
schirmer@13688:           E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
schirmer@13688:           T = Inl (PrimT (binop_type binop))\<rbrakk>
schirmer@13688:        \<Longrightarrow> P\<rbrakk>
schirmer@13688: \<Longrightarrow> P"
schirmer@13688: apply (erule wt_elim_cases)
schirmer@13688: apply (cases b)
schirmer@13688: apply auto
schirmer@13688: done
schirmer@13688: 
schirmer@12854: lemma Inj_eq_lemma [simp]: 
schirmer@12854:   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
schirmer@12854: by auto
schirmer@12854: 
schirmer@12854: (* unused *)
schirmer@12854: lemma single_valued_tys_lemma [rule_format (no_asm)]: 
schirmer@12854:   "\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow>  
schirmer@12854:      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
schirmer@12854: apply (cases "E", erule wt.induct)
schirmer@12854: apply (safe del: disjE)
schirmer@12854: apply (simp_all (no_asm_use) split del: split_if_asm)
schirmer@12854: apply (safe del: disjE)
schirmer@12854: (* 17 subgoals *)
schirmer@13337: apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
schirmer@12854: (*apply (safe del: disjE elim!: wt_elim_cases)*)
schirmer@12854: apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
schirmer@12854: apply (simp_all (no_asm_use) split del: split_if_asm)
schirmer@13337: apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
schirmer@12854: apply ((blast del: equalityCE dest: sym [THEN trans])+)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: (* unused *)
schirmer@12854: lemma single_valued_tys: 
schirmer@12854: "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
schirmer@12854: apply (unfold single_valued_def)
schirmer@12854: apply clarsimp
schirmer@12854: apply (rule single_valued_tys_lemma)
schirmer@12854: apply (auto intro!: widen_antisym)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma typeof_empty_is_type [rule_format (no_asm)]: 
schirmer@12854:   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
schirmer@12854: apply (rule val.induct)
schirmer@12854: apply    	auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: (* unused *)
schirmer@12854: lemma typeof_is_type [rule_format (no_asm)]: 
schirmer@12854:  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
schirmer@12854: apply (rule val.induct)
schirmer@12854: prefer 5 
schirmer@12854: apply     fast
schirmer@12854: apply  (simp_all (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: end