--- a/src/HOL/UNITY/Alloc.ML Tue May 23 12:32:24 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML Tue May 23 12:34:26 2000 +0200
@@ -40,23 +40,6 @@
handle THM _ => th;
-Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (dres_inst_tac [("x","n")] bspec 1);
-by Auto_tac;
-by (arith_tac 1);
-qed_spec_mp "sum_mono";
-
-Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
-by (induct_tac "ys" 1);
-by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
-qed_spec_mp "tokens_mono_prefix";
-
-Goalw [mono_def] "mono tokens";
-by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
-qed "mono_tokens";
-
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
@@ -274,20 +257,20 @@
Goal "Network Join \
\ ((rename sysOfClient \
-\ (plam x: lessThan Nclients. rename client_map Client)) Join \
+\ (plam x: {x. x<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: lessThan Nclients. rename client_map Client)) Join \
+\ (plam x: {x. x<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: lessThan Nclients. rename client_map Client)) Join \
+\ ((rename sysOfClient (plam x: {x. x<Nclients}. rename client_map Client)) Join \
\ Network) = System";
by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
qed "Alloc_component_System";
@@ -399,19 +382,19 @@
simpset()));
qed "System_Follows_allocGiv";
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<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: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<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: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<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()));
@@ -433,8 +416,9 @@
|> simplify (simpset() addsimps [o_def]);
(*safety (1), step 3*)
-Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
-\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
+Goal
+ "System : 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}";
by (simp_tac (simpset() addsimps [o_apply]) 1);
by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
by (auto_tac (claset(),
@@ -444,7 +428,7 @@
(** Follows reasoning **)
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<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);
@@ -452,7 +436,7 @@
simpset() addsimps [o_apply]));
qed "Always_tokens_giv_le_allocGiv";
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<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);
@@ -504,11 +488,15 @@
by Auto_tac;
qed "System_Bounded_ask";
+Goal "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})";
+by (Blast_tac 1);
+qed "Collect_all_imp_eq";
+
(*progress (2), step 4*)
-Goal "System : Always {s. ALL i : lessThan Nclients. \
-\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
+Goal "System : Always {s. ALL i. i<Nclients --> \
+\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}";
by (auto_tac (claset(),
- simpset() addsimps [Collect_ball_eq]));
+ simpset() addsimps [Collect_all_imp_eq]));
by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask]
RS Always_weaken) 1);
by (auto_tac (claset() addDs [set_mono], simpset()));
@@ -537,7 +525,7 @@
(*progress (2), step 7*)
Goal
- "System : (INT i : lessThan Nclients. \
+ "System : (INT i : {x. x<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})";
@@ -600,7 +588,7 @@
(*progress (2), step 9*)
Goal
- "System : (INT i : lessThan Nclients. \
+ "System : (INT i : {x. x<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 Tue May 23 12:32:24 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy Tue May 23 12:34:26 2000 +0200
@@ -4,33 +4,9 @@
Copyright 1998 University of Cambridge
Specification of Chandy and Charpentier's Allocator
-
-CONSIDER CHANGING "sum" to work on type "int", not "nat"
- --then can use subtraction in spec (1),
- --but need invariants that values are non-negative
*)
-Alloc = Follows + PPROD +
-
-(*Duplicated from HOL/ex/NatSum.thy.
- Maybe type should be [nat=>int, nat] => int**)
-consts sum :: [nat=>nat, nat] => nat
-primrec
- "sum f 0 = 0"
- "sum f (Suc n) = f(n) + sum f n"
-
-
-(*This function merely sums the elements of a list*)
-consts tokens :: nat list => nat
-primrec
- "tokens [] = 0"
- "tokens (x#xs) = x + tokens xs"
-
-
-consts
- NbT :: nat (*Number of tokens in system*)
- Nclients :: nat (*Number of clients*)
-
+Alloc = AllocBase + PPROD +
(** State definitions. OUTPUT variables are locals **)
@@ -76,12 +52,12 @@
(*spec (1)*)
system_safety :: 'a systemState program set
"system_safety ==
- Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients
- <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}"
+ Always {s. sum_below (%i. (tokens o giv o sub i o client) s) Nclients
+ <= NbT + sum_below (%i. (tokens o rel o sub i o client) s) Nclients}"
(*spec (2)*)
system_progress :: 'a systemState program set
- "system_progress == INT i : lessThan Nclients.
+ "system_progress == INT i : {x. x<Nclients}.
INT h.
{s. h <= (ask o sub i o client)s} LeadsTo
{s. h pfixLe (giv o sub i o client) s}"
@@ -126,31 +102,31 @@
"alloc_increasing ==
UNIV
guarantees[allocGiv]
- (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
+ (INT i : {x. x<Nclients}. Increasing (sub i o allocGiv))"
(*spec (7)*)
alloc_safety :: 'a allocState_u program set
"alloc_safety ==
- (INT i : lessThan Nclients. Increasing (sub i o allocRel))
+ (INT i : {x. x<Nclients}. Increasing (sub i o allocRel))
guarantees[allocGiv]
- Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
- <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
+ 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}"
(*spec (8)*)
alloc_progress :: 'a allocState_u program set
"alloc_progress ==
- (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
+ (INT i : {x. x<Nclients}. Increasing (sub i o allocAsk) Int
Increasing (sub i o allocRel))
Int
- Always {s. ALL i : lessThan Nclients.
- ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
+ Always {s. ALL i. i<Nclients -->
+ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
Int
- (INT i : lessThan Nclients.
+ (INT i : {x. x<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 : lessThan Nclients.
+ (INT i : {x. x<Nclients}.
INT h. {s. h <= (sub i o allocAsk) s}
LeadsTo
{s. h pfixLe (sub i o allocGiv) s})"
@@ -168,21 +144,21 @@
(*spec (9.1)*)
network_ask :: 'a systemState program set
- "network_ask == INT i : lessThan Nclients.
+ "network_ask == INT i : {x. x<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 : lessThan Nclients.
+ "network_giv == INT i : {x. x<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 : lessThan Nclients.
+ "network_rel == INT i : {x. x<Nclients}.
Increasing (rel o sub i o client)
guarantees[allocRel]
((sub i o allocRel) Fols (rel o sub i o client))"
@@ -190,7 +166,7 @@
(*spec: preserves part*)
network_preserves :: 'a systemState program set
"network_preserves == preserves allocGiv Int
- (INT i : lessThan Nclients.
+ (INT i : {x. x<Nclients}.
preserves (funPair rel ask o sub i o client))"
network_spec :: 'a systemState program set
@@ -230,7 +206,7 @@
System_def
"System == rename sysOfAlloc Alloc Join Network Join
(rename sysOfClient
- (plam x: lessThan Nclients. rename client_map Client))"
+ (plam x: {x. x<Nclients}. rename client_map Client))"
(**
@@ -253,7 +229,7 @@
Network
Join
(rename sysOfClient
- (plam x: lessThan Nclients. rename client_map Client))"
+ (plam x: {x. x<Nclients}. rename client_map Client))"
**)