# HG changeset patch
# User nipkow
# Date 894447960 -7200
# Node ID be11be0b6ea19a8c564c247756203a90f52f49e5
# Parent  4727272f3db6a560606f06e328ff16db277914bd
Changed [/] to [:=] and removed actual definition.

diff -r 4727272f3db6 -r be11be0b6ea1 src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed May 06 11:46:00 1998 +0200
@@ -20,7 +20,7 @@
 
 primrec C com
   C_skip    "C(SKIP) = id"
-  C_assign  "C(x := a) = {(s,t). t = s[a(s)/x]}"
+  C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
   C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
                                        {(s,t). (s,t) : C(c2) & ~ b(s)}"
diff -r 4727272f3db6 -r be11be0b6ea1 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Hoare.ML	Wed May 06 11:46:00 1998 +0200
@@ -27,7 +27,7 @@
 by (Simp_tac 1);
 qed "wp_SKIP";
 
-goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[a s/x]))";
+goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
 by (Simp_tac 1);
 qed "wp_Ass";
 
diff -r 4727272f3db6 -r be11be0b6ea1 src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Hoare.thy	Wed May 06 11:46:00 1998 +0200
@@ -20,7 +20,7 @@
 inductive hoare
 intrs
   skip "|- {P}SKIP{P}"
-  ass  "|- {%s. P(s[a s/x])} x:=a {P}"
+  ass  "|- {%s. P(s[x:=a s])} x:=a {P}"
   semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
   If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
       |- {P} IF b THEN c ELSE d {Q}"
diff -r 4727272f3db6 -r be11be0b6ea1 src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Natural.thy	Wed May 06 11:46:00 1998 +0200
@@ -14,15 +14,19 @@
 
 translations  "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
 
-constdefs assign :: [state,val,loc] => state    ("_[_'/_]" [95,0,0] 95)
-  "s[m/x] ==  (%y. if y=x then m else s y)"
-
+consts
+  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+           ("_/[_/:=/_]" [900,0,0] 900)
+(* update is NOT defined, only declared!
+   Thus the whole theory is independent of its meaning!
+   If theory Update is included, proofs break.
+*)
 
 inductive evalc
   intrs
     Skip    "<SKIP,s> -c-> s"
 
-    Assign  "<x := a,s> -c-> s[a(s)/x]"
+    Assign  "<x := a,s> -c-> s[x:=a(s)]"
 
     Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
             ==> <c0 ; c1, s> -c-> s1"
diff -r 4727272f3db6 -r be11be0b6ea1 src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Transition.ML	Wed May 06 11:46:00 1998 +0200
@@ -65,7 +65,7 @@
 goal Transition.thy
   "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
 \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
  (* case n = 0 *)
  by (fast_tac (claset() addss simpset()) 1);
 (* induction step *)
@@ -75,15 +75,14 @@
 qed_spec_mp "lemma2";
 
 goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
-by (com.induct_tac "c" 1);
+by (induct_tac "c" 1);
 by (safe_tac (claset() addSDs [rtrancl_imp_UN_rel_pow]));
 
 (* SKIP *)
 by (fast_tac (claset() addSEs [rel_pow_E2]) 1);
 
 (* ASSIGN *)
-by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]
-                       addss simpset()) 1);
+by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]) 1);
 
 (* SEMI *)
 by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
@@ -185,17 +184,18 @@
 of Lemma 1.
 *)
 
-
+(*Delsimps [update_apply];*)
 goal Transition.thy 
   "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
 by (etac evalc1.induct 1);
 by Auto_tac;
 qed_spec_mp "FB_lemma3";
+(*Addsimps [update_apply];*)
 
 val [major] = goal Transition.thy
   "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
 by (rtac (major RS rtrancl_induct2) 1);
-by (Fast_tac 1);
+ by (Fast_tac 1);
 by (fast_tac (claset() addIs [FB_lemma3]) 1);
 qed_spec_mp "FB_lemma2";
 
diff -r 4727272f3db6 -r be11be0b6ea1 src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Transition.thy	Wed May 06 11:46:00 1998 +0200
@@ -24,7 +24,7 @@
 
 inductive evalc1
   intrs
-    Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
+    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
 
     Semi1   "(SKIP;c,s) -1-> (c,s)"	
     Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
diff -r 4727272f3db6 -r be11be0b6ea1 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/VC.thy	Wed May 06 11:46:00 1998 +0200
@@ -23,7 +23,7 @@
 
 primrec awp acom
   "awp Askip Q = Q"
-  "awp (Aass x a) Q = (%s. Q(s[a s/x]))"
+  "awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
   "awp (Asemi c d) Q = awp c (awp d Q)"
   "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
   "awp (Awhile b I c) Q = I"
@@ -46,7 +46,7 @@
 (* simultaneous computation of vc and awp: *)
 primrec vcawp acom
   "vcawp Askip Q = (%s. True, Q)"
-  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[a s/x]))"
+  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
   "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
                               (vcc,wpc) = vcawp c wpd
                           in (%s. vcc s & vcd s, wpc))"