1.1 --- a/src/HOL/Bali/WellType.thy Thu Feb 21 20:11:32 2002 +0100
1.2 +++ b/src/HOL/Bali/WellType.thy Fri Feb 22 11:26:44 2002 +0100
1.3 @@ -153,28 +153,30 @@
1.4 "empty_dt \<equiv> \<lambda>a. None"
1.5
1.6 invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
1.7 -"invmode m e \<equiv> if static m then Static else if e=Super then SuperM else IntVir"
1.8 +"invmode m e \<equiv> if is_static m
1.9 + then Static
1.10 + else if e=Super then SuperM else IntVir"
1.11
1.12 lemma invmode_nonstatic [simp]:
1.13 "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
1.14 apply (unfold invmode_def)
1.15 +apply (simp (no_asm) add: member_is_static_simp)
1.16 +done
1.17 +
1.18 +
1.19 +lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
1.20 +apply (unfold invmode_def)
1.21 apply (simp (no_asm))
1.22 done
1.23
1.24
1.25 -lemma invmode_Static_eq [simp]: "(invmode m e = Static) = static m"
1.26 -apply (unfold invmode_def)
1.27 -apply (simp (no_asm))
1.28 -done
1.29 -
1.30 -
1.31 -lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(static m) \<and> e\<noteq>Super)"
1.32 +lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
1.33 apply (unfold invmode_def)
1.34 apply (simp (no_asm))
1.35 done
1.36
1.37 lemma Null_staticD:
1.38 - "a'=Null \<longrightarrow> (static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
1.39 + "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
1.40 apply (clarsimp simp add: invmode_IntVir_eq)
1.41 done
1.42
1.43 @@ -337,7 +339,7 @@
1.44 max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
1.45 = {((statDeclT,m),pTs')}
1.46 \<rbrakk> \<Longrightarrow>
1.47 - E,dt\<Turnstile>{statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
1.48 + E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
1.49
1.50 Methd: "\<lbrakk>is_class (prg E) C;
1.51 methd (prg E) C sig = Some m;
1.52 @@ -367,8 +369,8 @@
1.53 E,dt\<Turnstile>LVar vn\<Colon>=T"
1.54 (* cf. 15.10.1 *)
1.55 FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C;
1.56 - accfield (prg E) (cls E) C fn = Some (fd,f)\<rbrakk> \<Longrightarrow>
1.57 - E,dt\<Turnstile>{fd,static f}e..fn\<Colon>=(type f)"
1.58 + accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
1.59 + E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
1.60 (* cf. 15.12 *)
1.61 AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[];
1.62 E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
1.63 @@ -395,7 +397,7 @@
1.64 inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
1.65 inductive_cases wt_elim_cases:
1.66 "E,dt\<Turnstile>In2 (LVar vn) \<Colon>T"
1.67 - "E,dt\<Turnstile>In2 ({fd,s}e..fn) \<Colon>T"
1.68 + "E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T"
1.69 "E,dt\<Turnstile>In2 (e.[i]) \<Colon>T"
1.70 "E,dt\<Turnstile>In1l (NewC C) \<Colon>T"
1.71 "E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T"
1.72 @@ -406,7 +408,7 @@
1.73 "E,dt\<Turnstile>In1l (Acc va) \<Colon>T"
1.74 "E,dt\<Turnstile>In1l (Ass va v) \<Colon>T"
1.75 "E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T"
1.76 - "E,dt\<Turnstile>In1l ({statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
1.77 + "E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
1.78 "E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T"
1.79 "E,dt\<Turnstile>In1l (Body D blk) \<Colon>T"
1.80 "E,dt\<Turnstile>In3 ([]) \<Colon>Ts"
1.81 @@ -463,15 +465,15 @@
1.82 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
1.83 by (auto elim: wt.Super)
1.84
1.85 +
1.86 lemma wt_Call:
1.87 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
1.88 max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
1.89 - = {((statDeclC,m),pTs')};rT=(resTy m);
1.90 - mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
1.91 + = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
1.92 + mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
1.93 by (auto elim: wt.Call)
1.94
1.95
1.96 -
1.97 lemma invocationTypeExpr_noClassD:
1.98 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
1.99 \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
1.100 @@ -493,11 +495,12 @@
1.101 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
1.102 by (auto elim: wt.Super)
1.103
1.104 +lemma wt_FVar:
1.105 +"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
1.106 + sf=is_static f; fT=(type f); accC=cls E\<rbrakk>
1.107 +\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
1.108 +by (auto dest: wt.FVar)
1.109
1.110 -lemma wt_FVar:
1.111 -"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (fd,f);
1.112 - sf=static f; fT=(type f)\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{fd,sf}e..fn\<Colon>=fT"
1.113 -by (auto elim: wt.FVar)
1.114
1.115 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
1.116 by (auto elim: wt_elim_cases intro: "wt.Init")