splitted Loop rule

--- a/src/HOL/MicroJava/J/Eval.thy	Thu Jan 18 18:39:43 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Thu Jan 18 20:23:51 2001 +0100
@@ -112,7 +112,7 @@
 (* execution of statements *)
 
   (* cf. 14.1 *)
-  XcptS "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
+  XcptS "G\\<turnstile>(Some xc,s) -c-> (Some xc,s)"
 
   (* cf. 14.5 *)
   Skip  "G\\<turnstile>Norm s -Skip-> Norm s"
@@ -122,20 +122,21 @@
          G\\<turnstile>Norm s0 -Expr e-> s1"
 
   (* cf. 14.2 *)
-  Comp  "[| G\\<turnstile>Norm s0 -s-> s1;
-            G\\<turnstile> s1 -t -> s2|] ==>
-         G\\<turnstile>Norm s0 -s;; t-> s2"
+  Comp  "[| G\\<turnstile>Norm s0 -c1-> s1;
+            G\\<turnstile>     s1 -c2-> s2|] ==>
+         G\\<turnstile>Norm s0 -c1;; c2-> s2"
 
   (* cf. 14.8.2 *)
   Cond  "[| G\\<turnstile>Norm s0  -e\\<succ>v-> s1;
-            G\\<turnstile> s1 -(if the_Bool v then s else t)-> s2|] ==>
-         G\\<turnstile>Norm s0 -If(e) s Else t-> s2"
+            G\\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
+         G\\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
 
   (* cf. 14.10, 14.10.1 *)
-  Loop  "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1;
-	    if the_Bool v then G\\<turnstile>s1 -s-> s2 \\<and> G\\<turnstile>s2 -While(e) s-> s3
-	                  else s3 = s1 |] ==>
-         G\\<turnstile>Norm s0 -While(e) s-> s3"
+  LoopF "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; \\<not>the_Bool v |] ==>
+         G\\<turnstile>Norm s0 -While(e) c-> s1"
+  LoopT "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1;  the_Bool v;
+	    G\\<turnstile>s1 -c-> s2; G\\<turnstile>s2 -While(e) c-> s3 |] ==>
+         G\\<turnstile>Norm s0 -While(e) c-> s3"
 
 monos
   if_def2

--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Thu Jan 18 18:39:43 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Thu Jan 18 20:23:51 2001 +0100
@@ -176,7 +176,7 @@
 by( rtac eval_evals_exec.induct 1);
 by( rewtac c_hupd_def);
 
-(* several simplifications, XcptE, XcptEs, XcptS, Skip *)
+(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
 by( ALLGOALS Asm_full_simp_tac);
 by( ALLGOALS strip_tac);
 by( ALLGOALS (eresolve_tac ty_expr_ty_exprs_wt_stmt.elims 
@@ -186,7 +186,7 @@
 
 (* Level 7 *)
 
-(* 14 NewC *)
+(* 15 NewC *)
 by( dtac new_AddrD 1);
 by( etac disjE 1);
 by(  Asm_simp_tac 2);
@@ -200,10 +200,10 @@
 (* for Cast *)
 by( defer_tac 1);
 
-(* 13 Lit *)
+(* 14 Lit *)
 by( etac conf_litval 1);
 
-(* 12 BinOp *)
+(* 13 BinOp *)
 by forward_hyp_tac;
 by forward_hyp_tac;
 by( EVERY'[rtac conjI, eatac hext_trans 1] 1);
@@ -212,12 +212,9 @@
 by( dtac eval_no_xcpt 1);
 by( asm_full_simp_tac (simpset() addsplits [binop.split]) 1);
 
-(* 11 LAcc *)
+(* 12 LAcc *)
 by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
 
-(* 10 Nil *)
-by( Simp_tac 5);
-
 (* for FAss *)
 by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac, 
 			REPEAT o (etac conjE), hyp_subst_tac] 3);
@@ -227,13 +224,14 @@
 
 by forward_hyp_tac;
 
-(* 10+1 if *)
+(* 11+1 if *)
 by(  fast_tac (HOL_cs addIs [hext_trans]) 8);
 by( fast_tac (HOL_cs addIs [hext_trans]) 8);
 
-(* 9 Expr *)
+(* 10 Expr *)
 by( Fast_tac 6);
 
+(* 9 ??? *)
 by( ALLGOALS Asm_full_simp_tac);
 
 (* 8 Cast *)
@@ -251,7 +249,7 @@
 (* 5 While *)
 by(thin_tac "?a \\<longrightarrow> ?b" 5);
 by(datac ty_expr_ty_exprs_wt_stmt.Loop 1 5);
-by(force_tac (claset() addEs [hext_trans], simpset()addsplits[split_if_asm]) 5);
+by(force_tac (claset() addEs [hext_trans], simpset()) 5);
 
 by forward_hyp_tac;