# HG changeset patch
# User oheimb
# Date 880109878 -3600
# Node ID 5e21f41ccd21245a5427786e8bdc3e725cbd8f33
# Parent  a434327aef8b29853c06981fc9590ed7702c4a3c
minor improvements of formulation and proofs

diff -r a434327aef8b -r 5e21f41ccd21 src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Fri Nov 21 11:54:23 1997 +0100
+++ b/src/HOL/Induct/Com.thy	Fri Nov 21 11:57:58 1997 +0100
@@ -34,6 +34,12 @@
 
 translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
 
+syntax  eval'   :: "[exp*state,nat*state] => 
+		    ((exp*state) * (nat*state)) set => bool"
+						   ("_/ -|[_]-> _" [50,0,50] 50)
+translations
+    "esig -|[eval]-> ns" => "(esig,ns) : eval"
+
 constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
   "s[m/x] ==  (%y. if y=x then m else s y)"
 
@@ -43,20 +49,20 @@
   intrs
     Skip    "(SKIP,s) -[eval]-> s"
 
-    Assign  "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
+    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
 
     Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
             ==> (c0 ;; c1, s) -[eval]-> s1"
 
-    IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
+    IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
+    IfFalse "[| (e,s) -|[eval]->  (1,s');  (c1,s') -[eval]-> s1 |] 
              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
+    WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1"
 
-    WhileTrue  "[| ((e,s), (0,s1)) : eval;
+    WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
                 (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
                 ==> (WHILE e DO c, s) -[eval]-> s3"
 
diff -r a434327aef8b -r 5e21f41ccd21 src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Fri Nov 21 11:54:23 1997 +0100
+++ b/src/HOL/Induct/Exp.ML	Fri Nov 21 11:57:58 1997 +0100
@@ -57,7 +57,7 @@
 by (blast_tac (claset() addIs prems) 1);
 by (blast_tac (claset() addIs prems) 1);
 by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
-by (fast_tac (claset() addIs prems addss (simpset() addsimps [split_lemma])) 1);
+by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma]));
 qed "eval_induct";
 
 
@@ -87,10 +87,9 @@
 
 
 (*Expression evaluation is functional, or deterministic*)
-goal thy "Function eval";
-by (simp_tac (simpset() addsimps [Function_def]) 1);
-by (REPEAT (rtac allI 1));
-by (rtac impI 1);
+goalw thy [Function_def] "Function eval";
+by (strip_tac 1);
+by (split_all_tac 1);
 by (etac eval_induct 1);
 by (dtac com_Unique 4);
 by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def])));
diff -r a434327aef8b -r 5e21f41ccd21 src/HOL/Induct/Exp.thy
--- a/src/HOL/Induct/Exp.thy	Fri Nov 21 11:54:23 1997 +0100
+++ b/src/HOL/Induct/Exp.thy	Fri Nov 21 11:57:58 1997 +0100
@@ -13,7 +13,7 @@
        "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
 translations
     "esig -|-> (n,s)" <= "(esig,n,s) : eval"
-    "esig -|-> ns"    == "(esig,ns) : eval"
+    "esig -|-> ns"    == "(esig,ns ) : eval"
   
 inductive eval
   intrs