diff -r 1bd21b082466 -r f75dfc606ac7 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Evaln.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -103,6 +103,12 @@
 
   Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
 
+  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
+         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
+
+  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n\<rightarrow> s2\<rbrakk> 
+         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
+
   Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
 
   Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
@@ -128,7 +134,8 @@
 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
 
   Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
+         G\<turnstile>Norm s0 \<midarrow>Body D c
+          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
 
 (* evaluation of expression lists *)
 
@@ -148,7 +155,7 @@
 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
 
   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
-                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
+                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
 
   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
 	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
@@ -203,6 +210,8 @@
 	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
+        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> vs'"
+        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
@@ -262,6 +271,62 @@
 *}
 declare evaln_AbruptIs [intro!]
 
+lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1l (Callee l e)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }
+  then show ?thesis
+    by (cases s') fastsimp 
+qed
+
+lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1l (InsInitE c e)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
+lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In2 (InsInitV c w)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }  
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
+lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1r (FinA a c)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  } 
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
 lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
  fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
 apply (erule evaln_cases , auto)
@@ -437,6 +502,14 @@
     case Lit
     show ?case by (rule eval.Lit)
   next
+    case UnOp
+    with wf show ?case
+      by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
+  next
+    case BinOp
+    with wf show ?case
+      by - (erule wt_elim_cases, blast intro!: eval.BinOp dest: eval_type_sound)
+  next
     case Super
     show ?case by (rule eval.Super)
   next
@@ -494,11 +567,11 @@
          check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
       by simp
     have evaln_methd: 
-           "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
+     "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
     have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
     have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
     have hyp_methd: "PROP ?EqEval ?InitLvars s4 
-                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
+              (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
@@ -556,7 +629,7 @@
       moreover
       from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
       obtain "s4=s3'"
-	 "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	by auto
       moreover note False
       ultimately have
@@ -591,7 +664,7 @@
 	moreover
 	from eq_s3'_s3 np evaln_methd init_lvars
 	obtain "s4=s3'"
-	  "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	  by auto
 	moreover note np 
 	ultimately have
@@ -674,7 +747,7 @@
             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
 	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
 	  by - (drule wf_mdecl_bodyD,
-                simp cong add: lname.case_cong ename.case_cong)
+                auto simp: cong add: lname.case_cong ename.case_cong)
 	with dynM' iscls_invDeclC invDeclC'
 	have
 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
@@ -873,10 +946,28 @@
     show ?case
       by (rule eval.Try)
   next
-    case Fin
-    with wf show ?case
-      by -(erule wt_elim_cases, blast intro!: eval.Fin
-           dest: eval_type_sound intro: conforms_NormI)
+    case (Fin c1 c2 n s0 s1 s2 x1 L accC T)
+    have hyp_c1: "PROP ?EqEval (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
+    have hyp_c2: "PROP ?EqEval (Norm s1) (s2) (In1r c2) \<diamondsuit>" .
+    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
+    then obtain
+      wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
+      wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>" 
+      by (rule wt_elim_cases) blast
+    from conf_s0 wt_c1
+    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)"
+      by (rule hyp_c1)
+    with wf wt_c1 conf_s0
+    obtain       conf_s1: "Norm s1\<Colon>\<preceq>(G, L)" and 
+           error_free_s1: "error_free (x1,s1)"
+      by (auto dest!: eval_type_sound intro: conforms_NormI)
+    from conf_s1 wt_c2
+    have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2"
+      by (rule hyp_c2)
+    with eval_c1 error_free_s1
+    show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
+      by (auto intro: eval.Fin simp add: error_free_def)
   next
     case (Init C c n s0 s1 s2 s3 L accC T)
     have     cls: "the (class G C) = c" .
@@ -994,8 +1085,6 @@
   show ?thesis .
 qed
 
-text {* *} (* FIXME *)
-
 lemma eval_evaln: 
   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
@@ -1029,7 +1118,7 @@
     then obtain n where
       "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
       by (rules elim!: wt_elim_cases)
-    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
+    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
       by (rule evaln.Lab)
     then show ?case ..
   next
@@ -1209,16 +1298,22 @@
       by (auto intro!: evaln.Try le_maxI1 le_maxI2)
     then show ?case ..
   next
-    case (Fin c1 c2 s0 s1 s2 x1 L accC T)
-    with wf obtain n1 n2 where 
+    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
+    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
+                       then (x1, s1)
+                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+    from Fin wf obtain n1 n2 where 
       "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
-      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
+      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" and
+      error_free_s1: "error_free (x1,s1)"
       by (blast elim!: wt_elim_cases 
 	         dest: eval_type_sound intro: conforms_NormI)
     then have 
      "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
       by (blast intro: evaln.Fin dest: evaln_max2)
-    then show ?case ..
+    with error_free_s1 s3
+    show "\<exists>n. G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
+      by (auto simp add: error_free_def)
   next
     case (Init C c s0 s1 s2 s3 L accC T)
     have     cls: "the (class G C) = c" .
@@ -1340,6 +1435,24 @@
       by (rule evaln.Lit)
     then show ?case ..
   next
+    case (UnOp e s0 s1 unop v L accC T)
+    with wf obtain n where
+      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
+      by (rules elim!: wt_elim_cases)
+    hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
+      by (rule evaln.UnOp)
+    then show ?case ..
+  next
+    case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
+    with wf obtain n1 n2 where 
+      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
+      "G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n2\<rightarrow> s2"    
+      by (blast elim!: wt_elim_cases dest: eval_type_sound)
+    hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
+           \<rightarrow> s2"
+      by (blast intro!: evaln.BinOp dest: evaln_max2)
+    then show ?case ..
+  next
     case (Super s L accC T)
     have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
       by (rule evaln.Super)
@@ -1414,7 +1527,7 @@
     have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
     have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
     have hyp_methd: "PROP ?EqEval s3' s4 
-                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
+             (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
@@ -1475,7 +1588,7 @@
       moreover
       from eq_s3'_s3 False keep_abrupt eval_methd init_lvars
       obtain "s4=s3'"
-	 "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	by auto
       moreover note False evaln.Abrupt
       ultimately obtain m where 
@@ -1514,7 +1627,7 @@
 	moreover
 	from eq_s3'_s3 np eval_methd init_lvars
 	obtain "s4=s3'"
-	  "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	  by auto
 	moreover note np
 	ultimately obtain m where 
@@ -1600,7 +1713,7 @@
 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" 
 	  by - (drule wf_mdecl_bodyD,
-                simp cong add: lname.case_cong ename.case_cong)
+                auto simp: cong add: lname.case_cong ename.case_cong)
 	with dynM' iscls_invDeclC invDeclC'
 	have
 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>