--- a/src/HOL/Bali/WellType.thy Thu Feb 21 20:11:32 2002 +0100
+++ b/src/HOL/Bali/WellType.thy Fri Feb 22 11:26:44 2002 +0100
@@ -153,28 +153,30 @@
"empty_dt \<equiv> \<lambda>a. None"
invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
-"invmode m e \<equiv> if static m then Static else if e=Super then SuperM else IntVir"
+"invmode m e \<equiv> if is_static m
+ then Static
+ else if e=Super then SuperM else IntVir"
lemma invmode_nonstatic [simp]:
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
apply (unfold invmode_def)
+apply (simp (no_asm) add: member_is_static_simp)
+done
+
+
+lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
+apply (unfold invmode_def)
apply (simp (no_asm))
done
-lemma invmode_Static_eq [simp]: "(invmode m e = Static) = static m"
-apply (unfold invmode_def)
-apply (simp (no_asm))
-done
-
-
-lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(static m) \<and> e\<noteq>Super)"
+lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
apply (unfold invmode_def)
apply (simp (no_asm))
done
lemma Null_staticD:
- "a'=Null \<longrightarrow> (static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
+ "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
apply (clarsimp simp add: invmode_IntVir_eq)
done
@@ -337,7 +339,7 @@
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
= {((statDeclT,m),pTs')}
\<rbrakk> \<Longrightarrow>
- E,dt\<Turnstile>{statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
+ E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
Methd: "\<lbrakk>is_class (prg E) C;
methd (prg E) C sig = Some m;
@@ -367,8 +369,8 @@
E,dt\<Turnstile>LVar vn\<Colon>=T"
(* cf. 15.10.1 *)
FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C;
- accfield (prg E) (cls E) C fn = Some (fd,f)\<rbrakk> \<Longrightarrow>
- E,dt\<Turnstile>{fd,static f}e..fn\<Colon>=(type f)"
+ accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
+ E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
(* cf. 15.12 *)
AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[];
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
@@ -395,7 +397,7 @@
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 ({accC,statDeclC,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"
@@ -406,7 +408,7 @@
"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 ({statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
+ "E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T"
"E,dt\<Turnstile>In1l (Body D blk) \<Colon>T"
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts"
@@ -463,15 +465,15 @@
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
by (auto elim: wt.Super)
+
lemma wt_Call:
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
- = {((statDeclC,m),pTs')};rT=(resTy m);
- mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
+ = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
+ mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
by (auto elim: wt.Call)
-
lemma invocationTypeExpr_noClassD:
"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
\<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
@@ -493,11 +495,12 @@
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
by (auto elim: wt.Super)
+lemma wt_FVar:
+"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
+ sf=is_static f; fT=(type f); accC=cls E\<rbrakk>
+\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
+by (auto dest: wt.FVar)
-lemma wt_FVar:
-"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (fd,f);
- sf=static f; fT=(type f)\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{fd,sf}e..fn\<Colon>=fT"
-by (auto elim: wt.FVar)
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")