src/HOL/Bali/Evaln.thy
changeset 17589 58eeffd73be1
parent 16417 9bc16273c2d4
child 17876 b9c92f384109
     1.1 --- a/src/HOL/Bali/Evaln.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -554,7 +554,7 @@
     1.4    case (Abrupt s t xc)
     1.5    obtain n where
     1.6      "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
     1.7 -    by (rules intro: evaln.Abrupt)
     1.8 +    by (iprover intro: evaln.Abrupt)
     1.9    then show ?case ..
    1.10  next
    1.11    case Skip
    1.12 @@ -563,7 +563,7 @@
    1.13    case (Expr e s0 s1 v)
    1.14    then obtain n where
    1.15      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
    1.16 -    by (rules)
    1.17 +    by (iprover)
    1.18    then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
    1.19      by (rule evaln.Expr) 
    1.20    then show ?case ..
    1.21 @@ -571,7 +571,7 @@
    1.22    case (Lab c l s0 s1)
    1.23    then obtain n where
    1.24      "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
    1.25 -    by (rules)
    1.26 +    by (iprover)
    1.27    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
    1.28      by (rule evaln.Lab)
    1.29    then show ?case ..
    1.30 @@ -580,7 +580,7 @@
    1.31    then obtain n1 n2 where
    1.32      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
    1.33      "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
    1.34 -    by (rules)
    1.35 +    by (iprover)
    1.36    then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
    1.37      by (blast intro: evaln.Comp dest: evaln_max2 )
    1.38    then show ?case ..
    1.39 @@ -589,7 +589,7 @@
    1.40    then obtain n1 n2 where
    1.41      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
    1.42      "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
    1.43 -    by (rules)
    1.44 +    by (iprover)
    1.45    then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
    1.46      by (blast intro: evaln.If dest: evaln_max2)
    1.47    then show ?case ..
    1.48 @@ -597,18 +597,18 @@
    1.49    case (Loop b c e l s0 s1 s2 s3)
    1.50    from Loop.hyps obtain n1 where
    1.51      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
    1.52 -    by (rules)
    1.53 +    by (iprover)
    1.54    moreover from Loop.hyps obtain n2 where
    1.55      "if the_Bool b 
    1.56          then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
    1.57                G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
    1.58  	else s3 = s1"
    1.59 -    by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
    1.60 +    by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
    1.61    ultimately
    1.62    have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
    1.63      apply -
    1.64      apply (rule evaln.Loop)
    1.65 -    apply   (rules intro: evaln_nonstrict intro: le_maxI1)
    1.66 +    apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
    1.67  
    1.68      apply   (auto intro: evaln_nonstrict intro: le_maxI2)
    1.69      done
    1.70 @@ -622,7 +622,7 @@
    1.71    case (Throw a e s0 s1)
    1.72    then obtain n where
    1.73      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
    1.74 -    by (rules)
    1.75 +    by (iprover)
    1.76    then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
    1.77      by (rule evaln.Throw)
    1.78    then show ?case ..
    1.79 @@ -630,7 +630,7 @@
    1.80    case (Try catchC c1 c2 s0 s1 s2 s3 vn)
    1.81    from Try.hyps obtain n1 where
    1.82      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
    1.83 -    by (rules)
    1.84 +    by (iprover)
    1.85    moreover 
    1.86    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
    1.87    moreover
    1.88 @@ -646,7 +646,7 @@
    1.89    from Fin obtain n1 n2 where 
    1.90      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
    1.91      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
    1.92 -    by rules
    1.93 +    by iprover
    1.94    moreover
    1.95    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
    1.96                       then (x1, s1)
    1.97 @@ -673,17 +673,17 @@
    1.98    case (NewC C a s0 s1 s2)
    1.99    then obtain n where 
   1.100      "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
   1.101 -    by (rules)
   1.102 +    by (iprover)
   1.103    with NewC 
   1.104    have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
   1.105 -    by (rules intro: evaln.NewC)
   1.106 +    by (iprover intro: evaln.NewC)
   1.107    then show ?case ..
   1.108  next
   1.109    case (NewA T a e i s0 s1 s2 s3)
   1.110    then obtain n1 n2 where 
   1.111      "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
   1.112      "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   1.113 -    by (rules)
   1.114 +    by (iprover)
   1.115    moreover
   1.116    have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
   1.117    ultimately
   1.118 @@ -694,7 +694,7 @@
   1.119    case (Cast castT e s0 s1 s2 v)
   1.120    then obtain n where
   1.121      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.122 -    by (rules)
   1.123 +    by (iprover)
   1.124    moreover 
   1.125    have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
   1.126    ultimately
   1.127 @@ -705,7 +705,7 @@
   1.128    case (Inst T b e s0 s1 v)
   1.129    then obtain n where
   1.130      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.131 -    by (rules)
   1.132 +    by (iprover)
   1.133    moreover 
   1.134    have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
   1.135    ultimately
   1.136 @@ -721,7 +721,7 @@
   1.137    case (UnOp e s0 s1 unop v )
   1.138    then obtain n where
   1.139      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.140 -    by (rules)
   1.141 +    by (iprover)
   1.142    hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
   1.143      by (rule evaln.UnOp)
   1.144    then show ?case ..
   1.145 @@ -731,7 +731,7 @@
   1.146      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
   1.147      "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   1.148                 else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
   1.149 -    by (rules)
   1.150 +    by (iprover)
   1.151    hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
   1.152            \<rightarrow> s2"
   1.153      by (blast intro!: evaln.BinOp dest: evaln_max2)
   1.154 @@ -749,7 +749,7 @@
   1.155    case (Acc f s0 s1 v va)
   1.156    then obtain n where
   1.157      "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
   1.158 -    by (rules)
   1.159 +    by (iprover)
   1.160    then
   1.161    have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.162      by (rule evaln.Acc)
   1.163 @@ -759,7 +759,7 @@
   1.164    then obtain n1 n2 where 
   1.165      "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
   1.166      "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
   1.167 -    by (rules)
   1.168 +    by (iprover)
   1.169    then
   1.170    have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
   1.171      by (blast intro: evaln.Ass dest: evaln_max2)
   1.172 @@ -769,7 +769,7 @@
   1.173    then obtain n1 n2 where 
   1.174      "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
   1.175      "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
   1.176 -    by (rules)
   1.177 +    by (iprover)
   1.178    then
   1.179    have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
   1.180      by (blast intro: evaln.Cond dest: evaln_max2)
   1.181 @@ -780,7 +780,7 @@
   1.182    then obtain n1 n2 where
   1.183      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
   1.184      "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
   1.185 -    by rules
   1.186 +    by iprover
   1.187    moreover
   1.188    have "invDeclC = invocation_declclass G mode (store s2) a' statT 
   1.189                         \<lparr>name=mn,parTs=pTs'\<rparr>" .
   1.190 @@ -792,7 +792,7 @@
   1.191    from Call.hyps
   1.192    obtain m where 
   1.193      "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
   1.194 -    by rules
   1.195 +    by iprover
   1.196    ultimately
   1.197    have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
   1.198              (set_lvars (locals (store s2))) s4"
   1.199 @@ -802,7 +802,7 @@
   1.200    case (Methd D s0 s1 sig v )
   1.201    then obtain n where
   1.202      "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.203 -    by rules
   1.204 +    by iprover
   1.205    then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   1.206      by (rule evaln.Methd)
   1.207    then show ?case ..
   1.208 @@ -811,7 +811,7 @@
   1.209    from Body.hyps obtain n1 n2 where 
   1.210      evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
   1.211      evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
   1.212 -    by (rules)
   1.213 +    by (iprover)
   1.214    moreover
   1.215    have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
   1.216                       fst s2 = Some (Jump (Cont l))
   1.217 @@ -821,33 +821,33 @@
   1.218    have
   1.219       "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
   1.220         \<rightarrow> abupd (absorb Ret) s3"
   1.221 -    by (rules intro: evaln.Body dest: evaln_max2)
   1.222 +    by (iprover intro: evaln.Body dest: evaln_max2)
   1.223    then show ?case ..
   1.224  next
   1.225    case (LVar s vn )
   1.226    obtain n where
   1.227      "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
   1.228 -    by (rules intro: evaln.LVar)
   1.229 +    by (iprover intro: evaln.LVar)
   1.230    then show ?case ..
   1.231  next
   1.232    case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
   1.233    then obtain n1 n2 where
   1.234      "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
   1.235      "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
   1.236 -    by rules
   1.237 +    by iprover
   1.238    moreover
   1.239    have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
   1.240         "(v, s2') = fvar statDeclC stat fn a s2" .
   1.241    ultimately
   1.242    have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
   1.243 -    by (rules intro: evaln.FVar dest: evaln_max2)
   1.244 +    by (iprover intro: evaln.FVar dest: evaln_max2)
   1.245    then show ?case ..
   1.246  next
   1.247    case (AVar a e1 e2 i s0 s1 s2 s2' v )
   1.248    then obtain n1 n2 where 
   1.249      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
   1.250      "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   1.251 -    by rules
   1.252 +    by iprover
   1.253    moreover 
   1.254    have "(v, s2') = avar G i a s2" .
   1.255    ultimately 
   1.256 @@ -856,13 +856,13 @@
   1.257    then show ?case ..
   1.258  next
   1.259    case (Nil s0)
   1.260 -  show ?case by (rules intro: evaln.Nil)
   1.261 +  show ?case by (iprover intro: evaln.Nil)
   1.262  next
   1.263    case (Cons e es s0 s1 s2 v vs)
   1.264    then obtain n1 n2 where 
   1.265      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
   1.266      "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
   1.267 -    by rules
   1.268 +    by iprover
   1.269    then
   1.270    have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
   1.271      by (blast intro!: evaln.Cons dest: evaln_max2)