--- a/src/HOL/UNITY/Alloc.ML Fri May 26 18:05:34 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML Fri May 26 18:06:12 2000 +0200
@@ -260,20 +260,20 @@
Goal "Network Join \
\ ((rename sysOfClient \
-\ (plam x: {x. x<Nclients}. rename client_map Client)) Join \
+\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
\ rename sysOfAlloc Alloc) \
\ = System";
by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
qed "Network_component_System";
Goal "(rename sysOfClient \
-\ (plam x: {x. x<Nclients}. rename client_map Client)) Join \
+\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
\ (Network Join rename sysOfAlloc Alloc) = System";
by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
qed "Client_component_System";
Goal "rename sysOfAlloc Alloc Join \
-\ ((rename sysOfClient (plam x: {x. x<Nclients}. rename client_map Client)) Join \
+\ ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join \
\ Network) = System";
by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
qed "Alloc_component_System";
@@ -385,19 +385,19 @@
simpset()));
qed "System_Follows_allocGiv";
-Goal "System : Always (INT i: {x. x<Nclients}. \
+Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
by Auto_tac;
by (etac (System_Follows_allocGiv RS Follows_Bounded) 1);
qed "Always_giv_le_allocGiv";
-Goal "System : Always (INT i: {x. x<Nclients}. \
+Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
by Auto_tac;
by (etac (System_Follows_ask RS Follows_Bounded) 1);
qed "Always_allocAsk_le_ask";
-Goal "System : Always (INT i: {x. x<Nclients}. \
+Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})";
by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel],
simpset()));
@@ -431,7 +431,7 @@
(** Follows reasoning **)
-Goal "System : Always (INT i: {x. x<Nclients}. \
+Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (tokens o giv o sub i o client) s \
\ <= (tokens o sub i o allocGiv) s})";
by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1);
@@ -439,7 +439,7 @@
simpset() addsimps [o_apply]));
qed "Always_tokens_giv_le_allocGiv";
-Goal "System : Always (INT i: {x. x<Nclients}. \
+Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (tokens o sub i o allocRel) s \
\ <= (tokens o rel o sub i o client) s})";
by (rtac (Always_allocRel_le_rel RS Always_weaken) 1);
@@ -528,7 +528,7 @@
(*progress (2), step 7*)
Goal
- "System : (INT i : {x. x<Nclients}. \
+ "System : (INT i : (lessThan Nclients). \
\ INT h. {s. h <= (giv o sub i o client) s & \
\ h pfixGe (ask o sub i o client) s} \
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
@@ -591,7 +591,7 @@
(*progress (2), step 9*)
Goal
- "System : (INT i : {x. x<Nclients}. \
+ "System : (INT i : (lessThan Nclients). \
\ INT h. {s. h <= (sub i o allocAsk) s} \
\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
(*Can't use simpset(): the "INT h" must be kept*)
--- a/src/HOL/UNITY/Alloc.thy Fri May 26 18:05:34 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy Fri May 26 18:06:12 2000 +0200
@@ -57,7 +57,7 @@
(*spec (2)*)
system_progress :: 'a systemState program set
- "system_progress == INT i : {x. x<Nclients}.
+ "system_progress == INT i : lessThan Nclients.
INT h.
{s. h <= (ask o sub i o client)s} LeadsTo
{s. h pfixLe (giv o sub i o client) s}"
@@ -102,12 +102,12 @@
"alloc_increasing ==
UNIV
guarantees[allocGiv]
- (INT i : {x. x<Nclients}. Increasing (sub i o allocGiv))"
+ (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
(*spec (7)*)
alloc_safety :: 'a allocState_u program set
"alloc_safety ==
- (INT i : {x. x<Nclients}. Increasing (sub i o allocRel))
+ (INT i : lessThan Nclients. Increasing (sub i o allocRel))
guarantees[allocGiv]
Always {s. sum_below (%i. (tokens o sub i o allocGiv) s) Nclients
<= NbT + sum_below (%i. (tokens o sub i o allocRel) s) Nclients}"
@@ -115,18 +115,18 @@
(*spec (8)*)
alloc_progress :: 'a allocState_u program set
"alloc_progress ==
- (INT i : {x. x<Nclients}. Increasing (sub i o allocAsk) Int
+ (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
Increasing (sub i o allocRel))
Int
Always {s. ALL i. i<Nclients -->
(ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
Int
- (INT i : {x. x<Nclients}.
+ (INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
LeadsTo
{s. tokens h <= (tokens o sub i o allocRel)s})
guarantees[allocGiv]
- (INT i : {x. x<Nclients}.
+ (INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocAsk) s}
LeadsTo
{s. h pfixLe (sub i o allocGiv) s})"
@@ -144,21 +144,21 @@
(*spec (9.1)*)
network_ask :: 'a systemState program set
- "network_ask == INT i : {x. x<Nclients}.
+ "network_ask == INT i : lessThan Nclients.
Increasing (ask o sub i o client)
guarantees[allocAsk]
((sub i o allocAsk) Fols (ask o sub i o client))"
(*spec (9.2)*)
network_giv :: 'a systemState program set
- "network_giv == INT i : {x. x<Nclients}.
+ "network_giv == INT i : lessThan Nclients.
Increasing (sub i o allocGiv)
guarantees[giv o sub i o client]
((giv o sub i o client) Fols (sub i o allocGiv))"
(*spec (9.3)*)
network_rel :: 'a systemState program set
- "network_rel == INT i : {x. x<Nclients}.
+ "network_rel == INT i : lessThan Nclients.
Increasing (rel o sub i o client)
guarantees[allocRel]
((sub i o allocRel) Fols (rel o sub i o client))"
@@ -166,7 +166,7 @@
(*spec: preserves part*)
network_preserves :: 'a systemState program set
"network_preserves == preserves allocGiv Int
- (INT i : {x. x<Nclients}.
+ (INT i : lessThan Nclients.
preserves (funPair rel ask o sub i o client))"
network_spec :: 'a systemState program set
@@ -206,7 +206,7 @@
System_def
"System == rename sysOfAlloc Alloc Join Network Join
(rename sysOfClient
- (plam x: {x. x<Nclients}. rename client_map Client))"
+ (plam x: lessThan Nclients. rename client_map Client))"
(**
@@ -229,7 +229,7 @@
Network
Join
(rename sysOfClient
- (plam x: {x. x<Nclients}. rename client_map Client))"
+ (plam x: lessThan Nclients. rename client_map Client))"
**)