Up to index of Isabelle/Bali5
theory WellType = TypeRel:(* Title: isabelle/Bali/WellType.thy
ID: $Id: WellType.thy,v 1.45 2001/05/11 14:42:01 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Well-typedness of Java programs
improvements over Java Specification 1.0:
* methods of Object can be called upon references of interface or array type
simplifications:
* the type rules include all static checks on statements and expressions, e.g.
definedness of names (of parameters, locals, fields, methods)
design issues:
* unified type judgment for statements, variables, expressions, expression lists
* statements are typed like expressions with dummy type Void
* the typing rules take an extra argument that is capable of determining
the dynamic type of objects. Therefore, they can be used for both
checking static types and determining runtime types in transition semantics.
*)
theory WellType = TypeRel:
types lenv
= "(lname, ty) table" (* local variables, including This *)
env
= "prog × lenv" (* program, locals *)
syntax
prg :: "env \<Rightarrow> prog"
lcl :: "env \<Rightarrow> lenv"
translations
"lenv" <= (type) "(lname, ty) table"
"env" <= (type) "prog × lenv"
"prg" => "fst"
"lcl" => "snd"
section "maximally specific methods"
types
emhead = "ref_ty × mhead"
consts
cmheads :: "prog \<Rightarrow> tname \<Rightarrow> sig \<Rightarrow> emhead set"
mheads :: "prog \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
defs
cmheads_def:
"cmheads G C \<equiv> \<lambda>sig. (\<lambda>(C,(h,b)). (ClassT C,h)) ` o2s (cmethd G C sig)"
primrec
"mheads G NullT = (\<lambda>sig. {})"
"mheads G (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) ` imethds G I sig \<union>
cmheads G Object sig)"
"mheads G (ClassT C) = cmheads G C"
"mheads G (ArrayT T) = cmheads G Object"
(* more detailed than necessary for type-safety, see below. *)
constdefs
(* applicable methods, cf. 15.11.2.1 *)
appl_methds :: "prog \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead × ty list) set"
"appl_methds G rt \<equiv> \<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
mh \<in> mheads G rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'}"
(* more specific methods, cf. 15.11.2.2 *)
more_spec :: "prog \<Rightarrow> emhead × ty list \<Rightarrow> emhead × ty list \<Rightarrow> bool"
"more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
(*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'*)
(* maximally specific methods, cf. 15.11.2.2 *)
max_spec :: "prog \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead × ty list) set"
" max_spec G rt sig \<equiv>{m. m \<in>appl_methds G rt sig \<and>
(\<forall>m'\<in>appl_methds G rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
(*
rules (* all properties of more_spec, appl_methods and max_spec we actually need
these can easily be proven from the above definitions *)
max_spec2mheads "max_spec G rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow>
mh\<in>mheads G rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
*)
lemma max_spec2appl_meths: "x \<in> max_spec G T sig \<Longrightarrow> x \<in> appl_methds G T sig"
by (auto simp: max_spec_def)
lemma appl_methsD: "(mh,pTs')\<in>appl_methds G T (mn, pTs) \<Longrightarrow>
mh \<in> mheads G T (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
by (auto simp: appl_methds_def)
lemma max_spec2mheads: "max_spec G rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow>
mh \<in> mheads G rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
done
constdefs
empty_dt :: "dyn_ty"
"empty_dt \<equiv> \<lambda>a. None"
invmode :: "modi \<Rightarrow> expr \<Rightarrow> inv_mode"
"invmode m e \<equiv> if static m then Static else if e=Super then SuperM else IntVir"
lemma invmode_nonstatic: "invmode False (Acc (LVar e)) = IntVir"
apply (unfold invmode_def)
apply (simp (no_asm))
done
declare invmode_nonstatic [simp]
lemma invmode_Static_eq: "(invmode m e = Static) = m"
apply (unfold invmode_def)
apply (simp (no_asm))
done
declare invmode_Static_eq [simp]
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (¬m \<and> e\<noteq>Super)"
apply (unfold invmode_def)
apply (simp (no_asm))
done
lemma Null_staticD: "a'=Null \<longrightarrow> m \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
apply (clarsimp simp add: invmode_IntVir_eq)
done
types tys = "ty + ty list"
translations
"tys" <= (type) "ty + ty list"
consts
wt :: "(env × dyn_ty × term × tys) set"
(*wt :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term × tys) set" not feasible because of
changing env in Try stmt *)
syntax
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51 ] 50)
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
syntax (xsymbols)
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50)
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50)
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
translations
"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
"E,dt\<Turnstile>s\<Colon>\<surd>" == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2 e\<Colon>Inl T"
"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3 e\<Colon>Inr T"
syntax (* for purely static typing *)
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
ty_exprs_:: "env \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
syntax (xsymbols)
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
ty_exprs_ :: "env \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
translations
"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
inductive wt intros
(* well-typed statements *)
Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>"
Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Expr e\<Colon>\<surd>"
Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>;
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
(* cf. 14.8 *)
If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
E,dt\<Turnstile>c1\<Colon>\<surd>;
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
(* cf. 14.10 *)
Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>While(e) c\<Colon>\<surd>"
(* cf. 14.16 *)
Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
prg E\<turnstile>tn\<preceq>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Throw e\<Colon>\<surd>"
(* cf. 14.18 *)
Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>C SXcpt Throwable;
lcl E (EName vn)=None; (prg E,lcl E(EName vn\<mapsto>Class tn)),dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
(* cf. 14.18 *)
Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>init C\<Colon>\<surd>"
(* well-typed expressions *)
(* cf. 15.8 *)
NewC: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>NewC C\<Colon>-Class C"
(* cf. 15.9 *)
NewA: "\<lbrakk>is_type (prg E) T;
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
(* cf. 15.15 *)
Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_type (prg E) T';
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Cast T' e\<Colon>-T'"
(* cf. 15.19.2 *)
Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T;
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
(* cf. 15.7.1 *)
Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Lit x\<Colon>-T"
(* cf. 15.10.2, 15.11.1 *)
Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
class (prg E) C = Some (D, rest)\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Super\<Colon>-Class D"
(* cf. 15.13.1, 15.10.1, 15.12 *)
Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Acc va\<Colon>-T"
(* cf. 15.25, 15.25.1 *)
Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
E,dt\<Turnstile>v \<Colon>-T';
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>va:=v\<Colon>-T'"
(* cf. 15.24 *)
Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT t;
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
max_spec (prg E) t (mn, pTs) = {((md,(m,pns,rT)),pTs')}\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>{t,md,invmode m e}e..mn({pTs'}ps)\<Colon>-rT"
Methd: "\<lbrakk>is_class (prg E) C;
cmethd (prg E) C sig = Some (md,mh,lvars,blk,res);
E,dt\<Turnstile>Body md blk res\<Colon>-T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Methd C sig\<Colon>-T"
Body: "\<lbrakk>is_class (prg E) D;
E,dt\<Turnstile>blk\<Colon>\<surd>;
E,dt\<Turnstile>res\<Colon>-T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Body D blk res\<Colon>-T"
(* well-typed variables *)
(* cf. 15.13.1 *)
LVar: "\<lbrakk>lcl E vn = Some T; is_type (prg E) T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>LVar vn\<Colon>=T"
(* cf. 15.10.1 *)
FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C;
cfield (prg E) C fn = Some (fd,(m,fT))\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>{fd,static m}e..fn\<Colon>=fT"
(* cf. 15.12 *)
AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[];
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e.[i]\<Colon>=T"
(* well-typed expression lists *)
(* cf. 15.11.??? *)
Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
(* cf. 15.11.??? *)
Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
declare not_None_eq [simp del]
declare split_if [split del] split_if_asm [split del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
simpset_ref() := simpset() delloop "split_all_tac"
*}
inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
inductive_cases wt_elim_cases:
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T"
"E,dt\<Turnstile>In2 ({fd,s}e..fn) \<Colon>T"
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T"
"E,dt\<Turnstile>In1l (NewC C) \<Colon>T"
"E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T"
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T"
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T"
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T"
"E,dt\<Turnstile>In1l (Super) \<Colon>T"
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T"
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T"
"E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T"
"E,dt\<Turnstile>In1l ({t,md,mode}e..mn({pT'}p))\<Colon>T"
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T"
"E,dt\<Turnstile>In1l (Body D blk res) \<Colon>T"
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts"
"E,dt\<Turnstile>In3 (e#es) \<Colon>Ts"
"E,dt\<Turnstile>In1r Skip \<Colon>x"
"E,dt\<Turnstile>In1r (Expr e) \<Colon>x"
"E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x"
"E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x"
"E,dt\<Turnstile>In1r (While(e) c) \<Colon>x"
"E,dt\<Turnstile>In1r (Throw e) \<Colon>x"
"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x"
"E,dt\<Turnstile>In1r (init C) \<Colon>x"
declare not_None_eq [simp]
declare split_if [split] split_if_asm [split]
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
*}
lemma wt_Methd_is_methd: "(G,L)\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd G C sig"
apply (erule_tac wt_elim_cases)
apply clarsimp
apply (erule is_methdI, assumption)
done
lemma wt_Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT t; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
max_spec (prg E) t (mn, pTs) = {((md,(m,pns,rT)),pTs')};
mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{t,md,mode}e..mn({pTs'}ps)\<Colon>-rT"
apply (rotate_tac -1)
apply (erule ssubst)
apply (erule wt.Call)
apply auto
done
lemma wt_init [iff]: "E,dt\<Turnstile>init C\<Colon>\<surd> = is_class (prg E) C"
by (auto elim: wt_elim_cases intro: "wt.Init")
declare wt.Skip [iff]
lemma wt_StatRef: "isrtype (fst E) rt \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
apply (rule wt.Cast)
apply (rule wt.Lit)
apply (simp (no_asm))
apply (simp (no_asm_simp))
apply (rule cast.widen)
apply (simp (no_asm))
done
lemma wt_Inj_elim: "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of In1 ec \<Rightarrow> (case ec of Inl e \<Rightarrow> \<exists>T. U=Inl T
| Inr s \<Rightarrow> U=Inl (PrimT Void))
| In2 e \<Rightarrow> (\<exists>T. U=Inl T) | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule wt.induct)
apply auto
done
ML {*
fun wt_fun name inj rhs =
let
val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
fun is_Inj (Const (inj,_) $ _) = true
| is_Inj _ = false
fun pred (t as (_ $ (Const ("Pair",_) $
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
x))) $ _ )) = is_Inj x
in
make_simproc name lhs pred (thm name)
end
val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T"
val wt_var_proc = wt_fun "wt_var_eq" "In2" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T"
val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3" "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
val wt_stmt_proc = wt_fun "wt_stmt_eq" "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
*}
ML {*
Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
*}
lemma Inj_eq_lemma [simp]:
"(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
by auto
(* unused *)
lemma single_valued_tys_lemma [rule_format (no_asm)]: "\<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>
G = fst E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')"
apply (case_tac "E", case_tac "a", erule wt.induct)
apply (safe del: disjE)
apply (simp_all (no_asm_use) split del: split_if_asm)
apply (safe del: disjE)
(* 17 subgoals *)
apply (tactic {* ALLGOALS (fn i => if i = 9 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) *})
(*apply (safe del: disjE elim!: wt_elim_cases)*)
apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
apply (simp_all (no_asm_use) split del: split_if_asm)
apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
apply ((blast del: equalityCE dest: sym [THEN trans])+)
done
(* unused *)
lemma single_valued_tys:
"ws_prog (fst E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
apply (unfold single_valued_def)
apply clarsimp
apply (rule single_valued_tys_lemma)
apply (auto intro!: widen_antisym)
done
lemma typeof_empty_is_type [rule_format (no_asm)]: "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
apply (rule val.induct)
apply auto
done
(* unused *)
lemma typeof_is_type [rule_format (no_asm)]: "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
apply (rule val.induct)
prefer 5
apply fast
apply (simp_all (no_asm))
done
end
lemma max_spec2appl_meths:
x : max_spec G T sig ==> x : appl_methds G T sig
lemma appl_methsD:
(mh, pTs') : appl_methds G T (mn, pTs) ==> mh : mheads G T (mn, pTs') & G\<turnstile>pTs[\<preceq>]pTs'
lemma max_spec2mheads:
max_spec G rt (mn, pTs) = insert (mh, pTs') A ==> mh : mheads G rt (mn, pTs') & G\<turnstile>pTs[\<preceq>]pTs'
lemma invmode_nonstatic:
invmode False (Acc (LVar e)) = IntVir [!]
lemma invmode_Static_eq:
(invmode m e = Static) = m
lemma invmode_IntVir_eq:
(invmode m e = IntVir) = (¬ m & e ~= Super)
lemma Null_staticD:
a' = Null --> m ==> invmode m e = IntVir --> a' ~= Null
lemma wt_Methd_is_methd:
(G, L)|-In1l (Methd C sig)::T ==> is_methd G C sig [!]
lemma wt_Call:
[| E,dt|=e:-RefT t; E,dt|=ps:#pTs;
max_spec (fst E) t (mn, pTs) = {((md, m, pns, rT), pTs')};
mode = invmode m e |]
==> E,dt|={t,md,mode}e..mn( {pTs'}ps):-rT
[!]
lemma wt_init:
(E,dt|=init C:<>) = is_class (fst E) C [!]
lemma wt_StatRef:
isrtype (fst E) rt ==> E|-StatRef rt:-RefT rt [!]
lemma wt_Inj_elim:
E,dt|=t::U
==> sum3_case ((%e. EX T. U = Inl T) (+) (%s. U = Inl (PrimT Void)))
(%e. EX T. U = Inl T) (%e. EX T. U = Inr T) t
[!]
theorem wt_expr_eq:
(E,dt|=In1l t::U) = (EX T. U = Inl T & E,dt|=t:-T) [!]
theorem wt_var_eq:
(E,dt|=In2 t::U) = (EX T. U = Inl T & E,dt|=t:=T) [!]
theorem wt_exprs_eq:
(E,dt|=In3 t::U) = (EX Ts. U = Inr Ts & E,dt|=t:#Ts) [!]
theorem wt_stmt_eq:
(E,dt|=In1r t::U) = (U = Inl (PrimT Void) & E,dt|=t:<>) [!]
lemma Inj_eq_lemma:
(ALL T. (EX T'. T = Inj T' & P T') --> Q T) = (ALL T'. P T' --> Q (Inj T'))
lemma single_valued_tys_lemma:
[| ALL S T. G|-S<=:T --> G|-T<=:S --> S = T; E,dt|=t::T; G = fst E;
E,dt|=t::T' |]
==> T = T'
[!]
lemma single_valued_tys:
ws_prog (fst E) ==> single_valued {(t, T). E,dt|=t::T} [!]
lemma typeof_empty_is_type:
typeof (%a. None) v = Some T ==> is_type G T
lemma typeof_is_type:
ALL a. v ~= Addr a ==> EX T. typeof dt v = Some T & is_type G T