src/HOL/MicroJava/J/WellType.thy
changeset 10042 7164dc0d24d8
parent 9348 f495dba0cb07
child 10061 fe82134773dc
     1.1 --- a/src/HOL/MicroJava/J/WellType.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -24,8 +24,8 @@
     1.4  
     1.5  syntax
     1.6  
     1.7 -  prg		:: "'c env \\<Rightarrow> 'c prog"
     1.8 -  localT	:: "'c env \\<Rightarrow> (vname \\<leadsto> ty)"
     1.9 +  prg		:: "'c env => 'c prog"
    1.10 +  localT	:: "'c env => (vname \\<leadsto> ty)"
    1.11  
    1.12  translations	
    1.13  
    1.14 @@ -34,29 +34,29 @@
    1.15  
    1.16  consts
    1.17  
    1.18 -  more_spec	:: "'c prog \\<Rightarrow> (ty \\<times> 'x) \\<times> ty list \\<Rightarrow>
    1.19 -		               (ty \\<times> 'x) \\<times> ty list \\<Rightarrow> bool"
    1.20 -  appl_methds	:: "'c prog \\<Rightarrow>  cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
    1.21 -  max_spec	:: "'c prog \\<Rightarrow>  cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
    1.22 +  more_spec	:: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
    1.23 +		               (ty \\<times> 'x) \\<times> ty list => bool"
    1.24 +  appl_methds	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
    1.25 +  max_spec	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
    1.26  
    1.27  defs
    1.28  
    1.29 -  more_spec_def	  "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
    1.30 +  more_spec_def	  "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
    1.31  		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
    1.32    
    1.33    (* applicable methods, cf. 15.11.2.1 *)
    1.34 -  appl_methds_def "appl_methds G C \\<equiv> \\<lambda>(mn, pTs).
    1.35 +  appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
    1.36  		                 {((Class md,rT),pTs') |md rT mb pTs'.
    1.37  		                  method (G,C)  (mn, pTs') = Some (md,rT,mb) \\<and>
    1.38  		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
    1.39  
    1.40    (* maximally specific methods, cf. 15.11.2.2 *)
    1.41 -   max_spec_def	  "max_spec G C sig \\<equiv> {m. m \\<in>appl_methds G C sig \\<and> 
    1.42 +   max_spec_def	  "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and> 
    1.43  				          (\\<forall>m'\\<in>appl_methds G C sig.
    1.44 -				                   more_spec G m' m \\<longrightarrow> m' = m)}"
    1.45 +				                   more_spec G m' m --> m' = m)}"
    1.46  consts
    1.47  
    1.48 -  typeof :: "(loc \\<Rightarrow> ty option) \\<Rightarrow> val \\<Rightarrow> ty option"
    1.49 +  typeof :: "(loc => ty option) => val => ty option"
    1.50  
    1.51  primrec
    1.52  	"typeof dt  Unit    = Some (PrimT Void)"
    1.53 @@ -71,19 +71,19 @@
    1.54  
    1.55  consts
    1.56  
    1.57 -  ty_expr :: "java_mb env \\<Rightarrow> (expr      \\<times> ty     ) set"
    1.58 -  ty_exprs:: "java_mb env \\<Rightarrow> (expr list \\<times> ty list) set"
    1.59 -  wt_stmt :: "java_mb env \\<Rightarrow>  stmt                 set"
    1.60 +  ty_expr :: "java_mb env => (expr      \\<times> ty     ) set"
    1.61 +  ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
    1.62 +  wt_stmt :: "java_mb env =>  stmt                 set"
    1.63  
    1.64  syntax
    1.65  
    1.66 -ty_expr :: "java_mb env \\<Rightarrow> [expr     , ty     ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_"  [51,51,51]50)
    1.67 -ty_exprs:: "java_mb env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
    1.68 -wt_stmt :: "java_mb env \\<Rightarrow>  stmt                \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51   ]50)
    1.69 +ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_\\<turnstile>_::_"  [51,51,51]50)
    1.70 +ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_\\<turnstile>_[::]_"[51,51,51]50)
    1.71 +wt_stmt :: "java_mb env =>  stmt                => bool" ("_\\<turnstile>_ \\<surd>" [51,51   ]50)
    1.72  
    1.73  translations
    1.74 -	"E\\<turnstile>e \\<Colon> T" == "(e,T) \\<in> ty_expr  E"
    1.75 -	"E\\<turnstile>e[\\<Colon>]T" == "(e,T) \\<in> ty_exprs E"
    1.76 +	"E\\<turnstile>e :: T" == "(e,T) \\<in> ty_expr  E"
    1.77 +	"E\\<turnstile>e[::]T" == "(e,T) \\<in> ty_exprs E"
    1.78  	"E\\<turnstile>c \\<surd>"    == "c     \\<in> wt_stmt  E"
    1.79    
    1.80  inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
    1.81 @@ -91,98 +91,98 @@
    1.82  (* well-typed expressions *)
    1.83  
    1.84    (* cf. 15.8 *)
    1.85 -  NewC	"\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow>
    1.86 -						 E\\<turnstile>NewC C\\<Colon>Class C"
    1.87 +  NewC	"[|is_class (prg E) C|] ==>
    1.88 +						 E\\<turnstile>NewC C::Class C"
    1.89  
    1.90    (* cf. 15.15 *)
    1.91 -  Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>Class C;
    1.92 -	  prg E\\<turnstile>C\\<preceq>? D\\<rbrakk> \\<Longrightarrow>
    1.93 -						 E\\<turnstile>Cast D e\\<Colon>Class D"
    1.94 +  Cast	"[|E\\<turnstile>e::Class C;
    1.95 +	  prg E\\<turnstile>C\\<preceq>? D|] ==>
    1.96 +						 E\\<turnstile>Cast D e::Class D"
    1.97  
    1.98    (* cf. 15.7.1 *)
    1.99 -  Lit	"\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
   1.100 -						 E\\<turnstile>Lit x\\<Colon>T"
   1.101 +  Lit	"[|typeof (\\<lambda>v. None) x = Some T|] ==>
   1.102 +						 E\\<turnstile>Lit x::T"
   1.103  
   1.104    
   1.105    (* cf. 15.13.1 *)
   1.106 -  LAcc	"\\<lbrakk>localT E v = Some T; is_type (prg E) T\\<rbrakk> \\<Longrightarrow>
   1.107 -						 E\\<turnstile>LAcc v\\<Colon>T"
   1.108 +  LAcc	"[|localT E v = Some T; is_type (prg E) T|] ==>
   1.109 +						 E\\<turnstile>LAcc v::T"
   1.110  
   1.111 -  BinOp "\\<lbrakk>E\\<turnstile>e1\\<Colon>T;
   1.112 -	  E\\<turnstile>e2\\<Colon>T;
   1.113 +  BinOp "[|E\\<turnstile>e1::T;
   1.114 +	  E\\<turnstile>e2::T;
   1.115  	  if bop = Eq then T' = PrimT Boolean
   1.116 -	              else T' = T \\<and> T = PrimT Integer\\<rbrakk> \\<Longrightarrow>
   1.117 -						 E\\<turnstile>BinOp bop e1 e2\\<Colon>T'"
   1.118 +	              else T' = T \\<and> T = PrimT Integer|] ==>
   1.119 +						 E\\<turnstile>BinOp bop e1 e2::T'"
   1.120  
   1.121    (* cf. 15.25, 15.25.1 *)
   1.122 -  LAss  "\\<lbrakk>E\\<turnstile>LAcc v\\<Colon>T;
   1.123 -	  E\\<turnstile>e\\<Colon>T';
   1.124 -	  prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
   1.125 -						 E\\<turnstile>v\\<Colon>=e\\<Colon>T'"
   1.126 +  LAss  "[|E\\<turnstile>LAcc v::T;
   1.127 +	  E\\<turnstile>e::T';
   1.128 +	  prg E\\<turnstile>T'\\<preceq>T|] ==>
   1.129 +						 E\\<turnstile>v::=e::T'"
   1.130  
   1.131    (* cf. 15.10.1 *)
   1.132 -  FAcc	"\\<lbrakk>E\\<turnstile>a\\<Colon>Class C; 
   1.133 -	  field (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
   1.134 -						 E\\<turnstile>{fd}a..fn\\<Colon>fT"
   1.135 +  FAcc	"[|E\\<turnstile>a::Class C; 
   1.136 +	  field (prg E,C) fn = Some (fd,fT)|] ==>
   1.137 +						 E\\<turnstile>{fd}a..fn::fT"
   1.138  
   1.139    (* cf. 15.25, 15.25.1 *)
   1.140 -  FAss  "\\<lbrakk>E\\<turnstile>{fd}a..fn\\<Colon>T;
   1.141 -	  E\\<turnstile>v       \\<Colon>T';
   1.142 -	  prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
   1.143 -					 	 E\\<turnstile>{fd}a..fn:=v\\<Colon>T'"
   1.144 +  FAss  "[|E\\<turnstile>{fd}a..fn::T;
   1.145 +	  E\\<turnstile>v       ::T';
   1.146 +	  prg E\\<turnstile>T'\\<preceq>T|] ==>
   1.147 +					 	 E\\<turnstile>{fd}a..fn:=v::T'"
   1.148  
   1.149  
   1.150    (* cf. 15.11.1, 15.11.2, 15.11.3 *)
   1.151 -  Call	"\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
   1.152 -	  E\\<turnstile>ps[\\<Colon>]pTs;
   1.153 -	  max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
   1.154 -						 E\\<turnstile>a..mn({pTs'}ps)\\<Colon>rT"
   1.155 +  Call	"[|E\\<turnstile>a::Class C;
   1.156 +	  E\\<turnstile>ps[::]pTs;
   1.157 +	  max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}|] ==>
   1.158 +						 E\\<turnstile>a..mn({pTs'}ps)::rT"
   1.159  
   1.160  (* well-typed expression lists *)
   1.161  
   1.162    (* cf. 15.11.??? *)
   1.163 -  Nil						"E\\<turnstile>[][\\<Colon>][]"
   1.164 +  Nil						"E\\<turnstile>[][::][]"
   1.165  
   1.166    (* cf. 15.11.??? *)
   1.167 -  Cons	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
   1.168 -	   E\\<turnstile>es[\\<Colon>]Ts\\<rbrakk> \\<Longrightarrow>
   1.169 -						 E\\<turnstile>e#es[\\<Colon>]T#Ts"
   1.170 +  Cons	"[|E\\<turnstile>e::T;
   1.171 +	   E\\<turnstile>es[::]Ts|] ==>
   1.172 +						 E\\<turnstile>e#es[::]T#Ts"
   1.173  
   1.174  (* well-typed statements *)
   1.175  
   1.176    Skip					"E\\<turnstile>Skip\\<surd>"
   1.177  
   1.178 -  Expr	"\\<lbrakk>E\\<turnstile>e\\<Colon>T\\<rbrakk> \\<Longrightarrow>
   1.179 +  Expr	"[|E\\<turnstile>e::T|] ==>
   1.180  					 E\\<turnstile>Expr e\\<surd>"
   1.181  
   1.182 -  Comp	"\\<lbrakk>E\\<turnstile>s1\\<surd>; 
   1.183 -	  E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
   1.184 +  Comp	"[|E\\<turnstile>s1\\<surd>; 
   1.185 +	  E\\<turnstile>s2\\<surd>|] ==>
   1.186  					 E\\<turnstile>s1;; s2\\<surd>"
   1.187  
   1.188    (* cf. 14.8 *)
   1.189 -  Cond	"\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
   1.190 +  Cond	"[|E\\<turnstile>e::PrimT Boolean;
   1.191  	  E\\<turnstile>s1\\<surd>;
   1.192 -	  E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
   1.193 +	  E\\<turnstile>s2\\<surd>|] ==>
   1.194  					 E\\<turnstile>If(e) s1 Else s2\\<surd>"
   1.195  
   1.196    (* cf. 14.10 *)
   1.197 -  Loop "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
   1.198 -	 E\\<turnstile>s\\<surd>\\<rbrakk> \\<Longrightarrow>
   1.199 +  Loop "[|E\\<turnstile>e::PrimT Boolean;
   1.200 +	 E\\<turnstile>s\\<surd>|] ==>
   1.201  					 E\\<turnstile>While(e) s\\<surd>"
   1.202  
   1.203  constdefs
   1.204  
   1.205   wf_java_mdecl :: java_mb prog => cname => java_mb mdecl => bool
   1.206 -"wf_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
   1.207 +"wf_java_mdecl G C == \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
   1.208  	length pTs = length pns \\<and>
   1.209  	nodups pns \\<and>
   1.210  	unique lvars \\<and>
   1.211  	(\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
   1.212  	(\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
   1.213  	(let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
   1.214 -	 E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"
   1.215 +	 E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res::T \\<and> G\\<turnstile>T\\<preceq>rT))"
   1.216  
   1.217   wf_java_prog :: java_mb prog => bool
   1.218 -"wf_java_prog G \\<equiv> wf_prog wf_java_mdecl G"
   1.219 +"wf_java_prog G == wf_prog wf_java_mdecl G"
   1.220  
   1.221  end