--- 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
--- 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";
--- 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,
--- 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]));
--- 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})"
--- 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];
--- 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
--- /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];
--- /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