src/HOL/Bali/AxSound.thy
changeset 21765 89275a3ed7be
parent 18249 4398f0f12579
child 23350 50c5b0912a0c
     1.1 --- a/src/HOL/Bali/AxSound.thy	Mon Dec 11 12:28:16 2006 +0100
     1.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Dec 11 16:06:14 2006 +0100
     1.3 @@ -375,18 +375,18 @@
     1.4    thus ?case
     1.5      by (unfold ax_valids2_def) blast
     1.6  next
     1.7 -  case (asm A ts)
     1.8 +  case (asm ts A)
     1.9    have "ts \<subseteq> A" .
    1.10    then show "G,A|\<Turnstile>\<Colon>ts"
    1.11      by (auto simp add: ax_valids2_def triple_valid2_def)
    1.12  next
    1.13 -  case (weaken A ts ts')
    1.14 +  case (weaken A ts' ts)
    1.15    have "G,A|\<Turnstile>\<Colon>ts'" .
    1.16    moreover have "ts \<subseteq> ts'" .
    1.17    ultimately show "G,A|\<Turnstile>\<Colon>ts"
    1.18      by (unfold ax_valids2_def triple_valid2_def) blast
    1.19  next
    1.20 -  case (conseq A P Q t)
    1.21 +  case (conseq P A t Q)
    1.22    have con: "\<forall>Y s Z. P Y s Z \<longrightarrow> 
    1.23                (\<exists>P' Q'.
    1.24                    (G,A\<turnstile>{P'} t\<succ> {Q'} \<and> G,A|\<Turnstile>\<Colon>{ {P'} t\<succ> {Q'} }) \<and>
    1.25 @@ -431,7 +431,7 @@
    1.26      qed
    1.27    qed
    1.28  next
    1.29 -  case (hazard A P Q t)
    1.30 +  case (hazard A P t Q)
    1.31    show "G,A|\<Turnstile>\<Colon>{ {P \<and>. Not \<circ> type_ok G t} t\<succ> {Q} }"
    1.32      by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast
    1.33  next
    1.34 @@ -474,7 +474,7 @@
    1.35      qed
    1.36    qed
    1.37  next
    1.38 -  case (FVar A statDeclC P Q R accC e fn stat)
    1.39 +  case (FVar A P statDeclC Q e stat fn R accC)
    1.40    have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }" .
    1.41    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }" .
    1.42    show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC,statDeclC,stat}e..fn=\<succ> {R} }"
    1.43 @@ -569,7 +569,7 @@
    1.44      qed
    1.45    qed
    1.46  next
    1.47 -  case (AVar A P Q R e1 e2)
    1.48 +  case (AVar A P e1 Q e2 R)
    1.49    have valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" .
    1.50    have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
    1.51      using AVar.hyps by simp
    1.52 @@ -633,7 +633,7 @@
    1.53      qed
    1.54    qed
    1.55  next
    1.56 -  case (NewC A C P Q)
    1.57 +  case (NewC A P C Q)
    1.58    have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init C. {Alloc G (CInst C) Q} }".
    1.59    show "G,A|\<Turnstile>\<Colon>{ {Normal P} NewC C-\<succ> {Q} }"
    1.60    proof (rule valid_expr_NormalI)
    1.61 @@ -673,7 +673,7 @@
    1.62      qed
    1.63    qed
    1.64  next
    1.65 -  case (NewA A P Q R T e)
    1.66 +  case (NewA A P T Q e R)
    1.67    have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }" .
    1.68    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; 
    1.69                                              Alloc G (Arr T (the_Intg i)) R}}" .
    1.70 @@ -746,7 +746,7 @@
    1.71      qed
    1.72    qed
    1.73  next
    1.74 -  case (Cast A P Q T e)
    1.75 +  case (Cast A P e T Q)
    1.76    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> 
    1.77                   {\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
    1.78                    Q\<leftarrow>In1 v} }" .
    1.79 @@ -786,7 +786,7 @@
    1.80      qed
    1.81    qed
    1.82  next
    1.83 -  case (Inst A P Q T e)
    1.84 +  case (Inst A P e Q T)
    1.85    assume valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ>
    1.86                 {\<lambda>Val:v:. \<lambda>s.. Q\<leftarrow>In1 (Bool (v \<noteq> Null \<and> G,s\<turnstile>v fits RefT T))} }"
    1.87    show "G,A|\<Turnstile>\<Colon>{ {Normal P} e InstOf T-\<succ> {Q} }"
    1.88 @@ -841,7 +841,7 @@
    1.89      qed
    1.90    qed
    1.91  next
    1.92 -  case (UnOp A P Q e unop)
    1.93 +  case (UnOp A P e Q unop)
    1.94    assume valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P}e-\<succ>{\<lambda>Val:v:. Q\<leftarrow>In1 (eval_unop unop v)} }"
    1.95    show "G,A|\<Turnstile>\<Colon>{ {Normal P} UnOp unop e-\<succ> {Q} }"
    1.96    proof (rule valid_expr_NormalI)
    1.97 @@ -878,7 +878,7 @@
    1.98      qed
    1.99    qed
   1.100  next
   1.101 -  case (BinOp A P Q R binop e1 e2)
   1.102 +  case (BinOp A P e1 Q binop e2 R)
   1.103    assume valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" 
   1.104    have valid_e2: "\<And> v1.  G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 v1}
   1.105                (if need_second_arg binop v1 then In1l e2 else In1r Skip)\<succ>
   1.106 @@ -977,7 +977,7 @@
   1.107      qed
   1.108    qed
   1.109  next
   1.110 -  case (Acc A P Q var)
   1.111 +  case (Acc A P var Q)
   1.112    have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }" .
   1.113    show "G,A|\<Turnstile>\<Colon>{ {Normal P} Acc var-\<succ> {Q} }"
   1.114    proof (rule valid_expr_NormalI)
   1.115 @@ -1013,7 +1013,7 @@
   1.116      qed
   1.117    qed
   1.118  next
   1.119 -  case (Ass A P Q R e var)
   1.120 +  case (Ass A P var Q e R)
   1.121    have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }" .
   1.122    have valid_e: "\<And> vf. 
   1.123                    G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In2 vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R} }"
   1.124 @@ -1125,7 +1125,7 @@
   1.125      qed
   1.126    qed
   1.127  next
   1.128 -  case (Cond A P P' Q e0 e1 e2)
   1.129 +  case (Cond A P e0 P' e1 e2 Q)
   1.130    have valid_e0: "G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }" .
   1.131    have valid_then_else:"\<And> b.  G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q} }"
   1.132      using Cond.hyps by simp
   1.133 @@ -1215,7 +1215,7 @@
   1.134      qed
   1.135    qed
   1.136  next
   1.137 -  case (Call A P Q R S accC' args e mn mode pTs' statT)
   1.138 +  case (Call A P e Q args R mode statT mn pTs' S accC')
   1.139    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }" .
   1.140    have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
   1.141      using Call.hyps by simp
   1.142 @@ -1604,7 +1604,7 @@
   1.143    show "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
   1.144      by (rule Methd_sound)
   1.145  next
   1.146 -  case (Body A D P Q R c)
   1.147 +  case (Body A P D Q c R)
   1.148    have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }".
   1.149    have valid_c: "G,A|\<Turnstile>\<Colon>{ {Q} .c. 
   1.150                {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }".
   1.151 @@ -1697,7 +1697,7 @@
   1.152      qed
   1.153    qed
   1.154  next
   1.155 -  case (Cons A P Q R e es)
   1.156 +  case (Cons A P e Q es R)
   1.157    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }".
   1.158    have valid_es: "\<And> v. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>\<lfloor>v\<rfloor>\<^sub>e} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>\<lfloor>(v # vs)\<rfloor>\<^sub>l} }"
   1.159      using Cons.hyps by simp
   1.160 @@ -1779,7 +1779,7 @@
   1.161      qed
   1.162    qed
   1.163  next
   1.164 -  case (Expr A P Q e)
   1.165 +  case (Expr A P e Q)
   1.166    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }".
   1.167    show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Expr e. {Q} }"
   1.168    proof (rule valid_stmt_NormalI)
   1.169 @@ -1809,7 +1809,7 @@
   1.170      qed
   1.171    qed
   1.172  next
   1.173 -  case (Lab A P Q c l)
   1.174 +  case (Lab A P c l Q)
   1.175    have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }".
   1.176    show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
   1.177    proof (rule valid_stmt_NormalI)
   1.178 @@ -1846,7 +1846,7 @@
   1.179      qed
   1.180    qed
   1.181  next
   1.182 -  case (Comp A P Q R c1 c2)
   1.183 +  case (Comp A P c1 Q c2 R)
   1.184    have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }" .
   1.185    have valid_c2: "G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }" .
   1.186    show "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1;; c2. {R} }"
   1.187 @@ -1905,7 +1905,7 @@
   1.188      qed
   1.189    qed
   1.190  next
   1.191 -  case (If A P P' Q c1 c2 e)
   1.192 +  case (If A P e P' c1 c2 Q)
   1.193    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }" .
   1.194    have valid_then_else: "\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} .(if b then c1 else c2). {Q} }" 
   1.195      using If.hyps by simp
   1.196 @@ -1982,7 +1982,7 @@
   1.197      qed
   1.198    qed
   1.199  next
   1.200 -  case (Loop A P P' c e l)
   1.201 +  case (Loop A P e P' c l)
   1.202    have valid_e: "G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }".
   1.203    have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)} 
   1.204                           .c. 
   1.205 @@ -2020,7 +2020,7 @@
   1.206                  \<rbrakk>\<Longrightarrow> (P'\<leftarrow>=False\<down>=\<diamondsuit>) v s' Z"
   1.207  	  (is "PROP ?Hyp n t s v s'")
   1.208  	proof (induct)
   1.209 -	  case (Loop b c' e' l' n' s0' s1' s2' s3' Y' T E)
   1.210 +	  case (Loop s0' e' n' b s1' c' s2' l' s3' Y' T E)
   1.211  	  have while: "(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s" .
   1.212            hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
   1.213  	  have valid_A: "\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t". 
   1.214 @@ -2173,7 +2173,7 @@
   1.215  	    qed
   1.216  	  qed
   1.217  	next
   1.218 -	  case (Abrupt n' s t' abr Y' T E)
   1.219 +	  case (Abrupt abr s t' n' Y' T E)
   1.220  	  have t': "t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s".
   1.221  	  have conf: "(Some abr, s)\<Colon>\<preceq>(G, L)".
   1.222  	  have P: "P Y' (Some abr, s) Z".
   1.223 @@ -2212,7 +2212,7 @@
   1.224      qed
   1.225    qed
   1.226  next
   1.227 -  case (Jmp A P j)
   1.228 +  case (Jmp A j P)
   1.229    show "G,A|\<Turnstile>\<Colon>{ {Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P} }"
   1.230    proof (rule valid_stmt_NormalI)
   1.231      fix n s0 L accC C s1 Y Z
   1.232 @@ -2239,7 +2239,7 @@
   1.233      qed
   1.234    qed
   1.235  next
   1.236 -  case (Throw A P Q e)
   1.237 +  case (Throw A P e Q)
   1.238    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }".
   1.239    show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Throw e. {Q} }"
   1.240    proof (rule valid_stmt_NormalI)
   1.241 @@ -2277,7 +2277,7 @@
   1.242      qed
   1.243    qed
   1.244  next
   1.245 -  case (Try A C P Q R c1 c2 vn)
   1.246 +  case (Try A P c1 Q C vn c2 R)
   1.247    have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }".
   1.248    have valid_c2: "G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} 
   1.249                             .c2. 
   1.250 @@ -2409,7 +2409,7 @@
   1.251      qed
   1.252    qed
   1.253  next
   1.254 -  case (Fin A P Q R c1 c2)
   1.255 +  case (Fin A P c1 Q  c2 R)
   1.256    have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }".
   1.257    have valid_c2: "\<And> abr. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. abr = fst s) ;. abupd (\<lambda>x. None)} 
   1.258                                    .c2.
   1.259 @@ -2483,7 +2483,7 @@
   1.260      qed
   1.261    qed
   1.262  next
   1.263 -  case (Done A C P)
   1.264 +  case (Done A P C)
   1.265    show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P} }" 
   1.266    proof (rule valid_stmt_NormalI)
   1.267      fix n s0 L accC E s3 Y Z
   1.268 @@ -2506,7 +2506,7 @@
   1.269      qed
   1.270    qed
   1.271  next
   1.272 -  case (Init A C P Q R c)
   1.273 +  case (Init C c A P Q R)
   1.274    have c: "the (class G C) = c".
   1.275    have valid_super: 
   1.276          "G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
   1.277 @@ -2618,7 +2618,7 @@
   1.278      qed
   1.279    qed
   1.280  next
   1.281 -  case (InsInitV A P Q c v)
   1.282 +  case (InsInitV A P c v Q)
   1.283    show "G,A|\<Turnstile>\<Colon>{ {Normal P} InsInitV c v=\<succ> {Q} }"
   1.284    proof (rule valid_var_NormalI)
   1.285      fix s0 vf n s1 L Z
   1.286 @@ -2630,7 +2630,7 @@
   1.287      thus "Q \<lfloor>vf\<rfloor>\<^sub>v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
   1.288    qed
   1.289  next
   1.290 -  case (InsInitE A P Q c e)
   1.291 +  case (InsInitE A P c e Q)
   1.292    show "G,A|\<Turnstile>\<Colon>{ {Normal P} InsInitE c e-\<succ> {Q} }"
   1.293    proof (rule valid_expr_NormalI)
   1.294      fix s0 v n s1 L Z
   1.295 @@ -2642,7 +2642,7 @@
   1.296      thus "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
   1.297    qed
   1.298  next
   1.299 -  case (Callee A P Q e l)
   1.300 +  case (Callee A P l e Q)
   1.301    show "G,A|\<Turnstile>\<Colon>{ {Normal P} Callee l e-\<succ> {Q} }"
   1.302    proof (rule valid_expr_NormalI)
   1.303      fix s0 v n s1 L Z
   1.304 @@ -2654,7 +2654,7 @@
   1.305      thus "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
   1.306    qed
   1.307  next
   1.308 -  case (FinA A P Q a c)
   1.309 +  case (FinA A P a c Q)
   1.310    show "G,A|\<Turnstile>\<Colon>{ {Normal P} .FinA a c. {Q} }"
   1.311    proof (rule valid_stmt_NormalI)
   1.312      fix s0 v n s1 L Z