src/HOL/Bali/WellType.thy
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13337 f75dfc606ac7
     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")