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)
```