# HG changeset patch
# User paulson
# Date 894382102 -7200
# Node ID 4727272f3db6a560606f06e328ff16db277914bd
# Parent  0fad2acb45fb143667dccf7f6b6cf99b63568b3f
New syntax for function update; moved to main HOL directory

diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 05 13:27:18 1998 +0200
+++ b/src/HOL/IsaMakefile	Tue May 05 17:28:22 1998 +0200
@@ -46,7 +46,8 @@
   Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \
   RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
   Sum.ML Sum.thy Tools/record_package.ML Tools/typedef_package.ML \
-  Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \
+  Trancl.ML Trancl.thy Univ.ML Univ.thy \
+  Update.ML Update.thy Vimage.ML Vimage.thy WF.ML \
   WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \
   datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \
   indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \
@@ -155,7 +156,7 @@
   UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\
   UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\
   UNITY/Traces.ML UNITY/Traces.thy UNITY/UNITY.ML UNITY/UNITY.thy\
-  UNITY/Update.ML UNITY/Update.thy UNITY/WFair.ML UNITY/WFair.thy
+  UNITY/WFair.ML UNITY/WFair.thy
 	@$(ISATOOL) usedir $(OUT)/HOL UNITY
 
 
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue May 05 13:27:18 1998 +0200
+++ b/src/HOL/ROOT.ML	Tue May 05 17:28:22 1998 +0200
@@ -57,6 +57,7 @@
 use_thy "Sexp";
 use_thy "WF_Rel";
 use_thy "Map";
+use_thy "Update";
 
 (*TFL: recursive function definitions*)
 cd "$ISABELLE_HOME/src/TFL";
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Mutex.thy
--- a/src/HOL/UNITY/Mutex.thy	Tue May 05 13:27:18 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy	Tue May 05 17:28:22 1998 +0200
@@ -26,24 +26,24 @@
 
 constdefs
   cmd0 :: "[pvar,pvar] => (state*state) set"
-    "cmd0 u m == {(s,s'). s' = s[u|->1][m|->1] & s m = 0}"
+    "cmd0 u m == {(s,s'). s' = s[u:=1][m:=1] & s m = 0}"
 
   cmd1u :: "(state*state) set"
-    "cmd1u == {(s,s'). s' = s[PP|-> s VV][MM|->2] & s MM = 1}"
+    "cmd1u == {(s,s'). s' = s[PP:= s VV][MM:=2] & s MM = 1}"
 
   cmd1v :: "(state*state) set"
-    "cmd1v == {(s,s'). s' = s[PP|-> 1 - s UU][NN|->2] & s NN = 1}"
+    "cmd1v == {(s,s'). s' = s[PP:= 1 - s UU][NN:=2] & s NN = 1}"
 
   (*Put pv=0 for u's program and pv=1 for v's program*)
   cmd2 :: "[nat,pvar] => (state*state) set"
-    "cmd2 pv m == {(s,s'). s' = s[m|->3] & s PP = pv & s m = 2}"
+    "cmd2 pv m == {(s,s'). s' = s[m:=3] & s PP = pv & s m = 2}"
 
   cmd3 :: "[pvar,pvar] => (state*state) set"
-    "cmd3 u m == {(s,s'). s' = s[u|->0][m|->4] & s m = 3}"
+    "cmd3 u m == {(s,s'). s' = s[u:=0][m:=4] & s m = 3}"
 
   (*Put pv=1 for u's program and pv=0 for v's program*)
   cmd4 :: "[nat,pvar] => (state*state) set"
-    "cmd4 pv m == {(s,s'). s' = s[PP|->pv][m|->0] & s m = 4}"
+    "cmd4 pv m == {(s,s'). s' = s[PP:=pv][m:=0] & s m = 4}"
 
   mutex :: "(state*state) set set"
     "mutex == {id,
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Tue May 05 13:27:18 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Tue May 05 17:28:22 1998 +0200
@@ -4,6 +4,7 @@
     Copyright   1998  University of Cambridge
 
 Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
+	[ this example took only four days!]
 *)
 
 open Reach;
@@ -133,19 +134,19 @@
 
 (*** Progress ***)
 
-goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x|->True])) = metric s";
-by (subgoal_tac "{v. ~ (s[x|->True]) v} = {v. ~ s v} - {x}" 1);
+goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x:=True])) = metric s";
+by (subgoal_tac "{v. ~ (s[x:=True]) v} = {v. ~ s v} - {x}" 1);
 by Auto_tac;
 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
 qed "Suc_metric";
 
-goal thy "!!s. ~ s x ==> metric (s[x|->True]) < metric s";
+goal thy "!!s. ~ s x ==> metric (s[x:=True]) < metric s";
 by (etac (Suc_metric RS subst) 1);
 by (Blast_tac 1);
 qed "metric_less";
 AddSIs [metric_less];
 
-goal thy "metric (s[y|->s x | s y]) <= metric s";
+goal thy "metric (s[y:=s x | s y]) <= metric s";
 by (case_tac "s x --> s y" 1);
 by (auto_tac (claset() addIs [less_imp_le],
 	      simpset() addsimps [update_idem]));
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Reach.thy
--- a/src/HOL/UNITY/Reach.thy	Tue May 05 13:27:18 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy	Tue May 05 17:28:22 1998 +0200
@@ -21,7 +21,7 @@
 constdefs
 
   asgt  :: "[vertex,vertex] => (state*state) set"
-    "asgt u v == {(s,s'). s' = s[v|-> s u | s v]}"
+    "asgt u v == {(s,s'). s' = s[v:= s u | s v]}"
 
   racts :: "(state*state) set set"
     "racts == insert id (UN (u,v): edges. {asgt u v})"
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Update.ML
--- a/src/HOL/UNITY/Update.ML	Tue May 05 13:27:18 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      HOL/UNITY/Update.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Function updates: like the standard theory Map, but for ordinary functions
-*)
-
-open Update;
-
-goalw thy [update_def] "(f[x|->y] = f) = (f x = y)";
-by Safe_tac;
-by (etac subst 1);
-by (rtac ext 2);
-by Auto_tac;
-qed "update_idem_iff";
-
-(* f x = y ==> f[x|->y] = f *)
-bind_thm("update_idem", update_idem_iff RS iffD2);
-
-AddIffs [refl RS update_idem];
-
-goal thy "(f[x|->y])z = (if x=z then y else f z)";
-by (simp_tac (simpset() addsimps [update_def]) 1);
-qed "update_apply";
-Addsimps [update_apply];
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Update.thy
--- a/src/HOL/UNITY/Update.thy	Tue May 05 13:27:18 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      HOL/UNITY/Update.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Function updates: like the standard theory Map, but for ordinary functions
-*)
-
-Update = Fun +
-
-consts
-  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
-           ("_/[_/|->/_]" [900,0,0] 900)
-
-syntax (symbols)
-  update    :: "('a => 'b) => 'a => 'b => ('a => 'b)"
-               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
-
-defs
-  update_def "f[a|->b] == %x. if x=a then b else f x"
-
-end
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/Update.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Update.ML	Tue May 05 17:28:22 1998 +0200
@@ -0,0 +1,26 @@
+(*  Title:      HOL/UNITY/Update.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Function updates: like the standard theory Map, but for ordinary functions
+*)
+
+open Update;
+
+goalw thy [update_def] "(f[x:=y] = f) = (f x = y)";
+by Safe_tac;
+by (etac subst 1);
+by (rtac ext 2);
+by Auto_tac;
+qed "update_idem_iff";
+
+(* f x = y ==> f[x:=y] = f *)
+bind_thm("update_idem", update_idem_iff RS iffD2);
+
+AddIffs [refl RS update_idem];
+
+goal thy "(f[x:=y])z = (if x=z then y else f z)";
+by (simp_tac (simpset() addsimps [update_def]) 1);
+qed "update_apply";
+Addsimps [update_apply];
diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/Update.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Update.thy	Tue May 05 17:28:22 1998 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/UNITY/Update.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Function updates: like the standard theory Map, but for ordinary functions
+*)
+
+Update = Fun +
+
+consts
+  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+           ("_/[_/:=/_]" [900,0,0] 900)
+
+syntax (symbols)
+  update    :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
+
+defs
+  update_def "f[a:=b] == %x. if x=a then b else f x"
+
+end