src/HOL/Bali/Evaln.thy
changeset 23350 50c5b0912a0c
parent 22218 30a8890d2967
child 23747 b07cff284683
     1.1 --- a/src/HOL/Bali/Evaln.thy	Wed Jun 13 00:01:38 2007 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Jun 13 00:01:41 2007 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4  using evaln 
     1.5  proof (induct)
     1.6    case (Loop s0 e n b s1 c s2 l s3)
     1.7 -  have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
     1.8 +  note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
     1.9    moreover
    1.10    have "if the_Bool b
    1.11          then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
    1.12 @@ -420,16 +420,16 @@
    1.13    ultimately show ?case by (rule eval.Loop)
    1.14  next
    1.15    case (Try s0 c1 n s1 s2 C vn c2 s3)
    1.16 -  have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
    1.17 +  note `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
    1.18    moreover
    1.19 -  have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
    1.20 +  note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
    1.21    moreover
    1.22    have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
    1.23      using Try.hyps by simp
    1.24    ultimately show ?case by (rule eval.Try)
    1.25  next
    1.26    case (Init C c s0 s3 n s1 s2)
    1.27 -  have "the (class G C) = c".
    1.28 +  note `the (class G C) = c`
    1.29    moreover
    1.30    have "if inited C (globs s0) 
    1.31             then s3 = Norm s0
    1.32 @@ -600,7 +600,7 @@
    1.33      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
    1.34      by (iprover)
    1.35    moreover 
    1.36 -  have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
    1.37 +  note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
    1.38    moreover
    1.39    from Try.hyps obtain n2 where
    1.40      "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
    1.41 @@ -616,9 +616,9 @@
    1.42      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
    1.43      by iprover
    1.44    moreover
    1.45 -  have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
    1.46 -                     then (x1, s1)
    1.47 -                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
    1.48 +  note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) 
    1.49 +                   then (x1, s1)
    1.50 +                   else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
    1.51    ultimately 
    1.52    have 
    1.53      "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
    1.54 @@ -626,7 +626,7 @@
    1.55    then show ?case ..
    1.56  next
    1.57    case (Init C c s0 s3 s1 s2)
    1.58 -  have     cls: "the (class G C) = c" .
    1.59 +  note cls = `the (class G C) = c`
    1.60    moreover from Init.hyps obtain n where
    1.61        "if inited C (globs s0) then s3 = Norm s0
    1.62         else (G\<turnstile>Norm (init_class_obj G C s0)
    1.63 @@ -653,7 +653,7 @@
    1.64      "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
    1.65      by (iprover)
    1.66    moreover
    1.67 -  have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
    1.68 +  note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
    1.69    ultimately
    1.70    have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
    1.71      by (blast intro: evaln.NewA dest: evaln_max2)
    1.72 @@ -664,7 +664,7 @@
    1.73      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
    1.74      by (iprover)
    1.75    moreover 
    1.76 -  have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
    1.77 +  note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1`
    1.78    ultimately
    1.79    have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
    1.80      by (rule evaln.Cast)
    1.81 @@ -675,7 +675,7 @@
    1.82      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
    1.83      by (iprover)
    1.84    moreover 
    1.85 -  have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
    1.86 +  note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)`
    1.87    ultimately
    1.88    have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
    1.89      by (rule evaln.Inst)
    1.90 @@ -745,12 +745,12 @@
    1.91      "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
    1.92      by iprover
    1.93    moreover
    1.94 -  have "invDeclC = invocation_declclass G mode (store s2) a' statT 
    1.95 -                       \<lparr>name=mn,parTs=pTs'\<rparr>" .
    1.96 +  note `invDeclC = invocation_declclass G mode (store s2) a' statT 
    1.97 +                       \<lparr>name=mn,parTs=pTs'\<rparr>`
    1.98    moreover
    1.99 -  have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
   1.100 +  note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2`
   1.101    moreover
   1.102 -  have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
   1.103 +  note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3`
   1.104    moreover 
   1.105    from Call.hyps
   1.106    obtain m where 
   1.107 @@ -776,10 +776,10 @@
   1.108      evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
   1.109      by (iprover)
   1.110    moreover
   1.111 -  have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
   1.112 +  note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
   1.113                       fst s2 = Some (Jump (Cont l))
   1.114 -                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
   1.115 -                 else s2)".
   1.116 +              then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
   1.117 +              else s2)`
   1.118    ultimately
   1.119    have
   1.120       "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
   1.121 @@ -799,8 +799,8 @@
   1.122      "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
   1.123      by iprover
   1.124    moreover
   1.125 -  have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
   1.126 -       "(v, s2') = fvar statDeclC stat fn a s2" .
   1.127 +  note `s3 = check_field_access G accC statDeclC fn stat a s2'`
   1.128 +    and `(v, s2') = fvar statDeclC stat fn a s2`
   1.129    ultimately
   1.130    have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
   1.131      by (iprover intro: evaln.FVar dest: evaln_max2)
   1.132 @@ -812,7 +812,7 @@
   1.133      "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   1.134      by iprover
   1.135    moreover 
   1.136 -  have "(v, s2') = avar G i a s2" .
   1.137 +  note `(v, s2') = avar G i a s2`
   1.138    ultimately 
   1.139    have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
   1.140      by (blast intro!: evaln.AVar dest: evaln_max2)