--- a/src/HOL/IsaMakefile Thu Jul 03 12:56:48 2003 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 03 18:07:50 2003 +0200
@@ -389,8 +389,7 @@
UNITY/Simple/Network.thy\
UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
- UNITY/Comp/AllocBase.thy \
- UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
+ UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
UNITY/Comp/PriorityAux.thy \
UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
--- a/src/HOL/UNITY/Comp/AllocImpl.ML Thu Jul 03 12:56:48 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(* Title: HOL/UNITY/AllocImpl
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
-
-Implementation of a multiple-client allocator from a single-client allocator
-*)
-
-AddIs [impOfSubs subset_preserves_o];
-Addsimps [funPair_o_distrib];
-Addsimps [Always_INT_distrib];
-Delsimps [o_apply];
-
-Open_locale "Merge";
-
-val Merge = thm "Merge_spec";
-
-Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
-by (cut_facts_tac [Merge] 1);
-by (auto_tac (claset(),
- simpset() addsimps [merge_spec_def, merge_allowed_acts_def,
- Allowed_def, safety_prop_Acts_iff]));
-qed "Merge_Allowed";
-
-Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
-\ M : Allowed G)";
-by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));
-qed "M_ok_iff";
-AddIffs [M_ok_iff];
-
-Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
-\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
-by (cut_facts_tac [Merge] 1);
-by (force_tac (claset() addDs [guaranteesD],
- simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1);
-qed "Merge_Always_Out_eq_iOut";
-
-Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
-\ ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
-by (cut_facts_tac [Merge] 1);
-by (force_tac (claset() addDs [guaranteesD],
- simpset() addsimps [merge_spec_def, merge_bounded_def]) 1);
-qed "Merge_Bounded";
-
-Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
-\ ==> M Join G : Always \
-\ {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s) \
-\ {k. k < length (iOut s) & iOut s ! k = i})) = \
-\ (bag_of o merge.Out) s}";
-by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
- UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
- by Auto_tac;
-by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
- by (Simp_tac 1);
- by (Blast_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
-by (subgoal_tac
- "(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \
-\ lessThan (length (iOut x))" 1);
- by (Blast_tac 2);
-by (asm_simp_tac (simpset() addsimps [o_def]) 1);
-qed "Merge_Bag_Follows_lemma";
-
-Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
-\ guarantees \
-\ (bag_of o merge.Out) Fols \
-\ (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)";
-by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
-by Auto_tac;
-by (rtac Follows_setsum 1);
-by (cut_facts_tac [Merge] 1);
-by (auto_tac (claset(),
- simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
-by (dtac guaranteesD 1);
-by (best_tac
- (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
-by Auto_tac;
-qed "Merge_Bag_Follows";
-
-Close_locale "Merge";
-
-
-(** Distributor **)
-
-Open_locale "Distrib";
-
-val Distrib = thm "Distrib_spec";
-
-
-Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
-\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\ guarantees \
-\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
-by (cut_facts_tac [Distrib] 1);
-by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1);
-by (Clarify_tac 1);
-by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
- addDs [guaranteesD]) 1);
-qed "Distr_Increasing_Out";
-
-Goal "[| G : preserves distr.Out; \
-\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
-\ ==> D Join G : Always \
-\ {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (distr.In s) \
-\ {k. k < length (iIn s) & iIn s ! k = i})) = \
-\ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
-by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
-by Auto_tac;
-by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
- by (Simp_tac 1);
- by (Blast_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
-by (subgoal_tac
- "(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \
-\ lessThan (length (iIn x))" 1);
- by (Blast_tac 2);
-by (Asm_simp_tac 1);
-qed "Distr_Bag_Follows_lemma";
-
-Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
-by (cut_facts_tac [Distrib] 1);
-by (auto_tac (claset(),
- simpset() addsimps [distr_spec_def, distr_allowed_acts_def,
- Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
-qed "D_ok_iff";
-AddIffs [D_ok_iff];
-
-Goal
- "D : Increasing distr.In Int Increasing distr.iIn Int \
-\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\ guarantees \
-\ (INT i : lessThan Nclients. \
-\ (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s) \
-\ Fols \
-\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
-by (rtac guaranteesI 1);
-by (Clarify_tac 1);
-by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
-by Auto_tac;
-by (rtac Follows_setsum 1);
-by (cut_facts_tac [Distrib] 1);
-by (auto_tac (claset(),
- simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
-by (dtac guaranteesD 1);
-by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
-by Auto_tac;
-qed "Distr_Bag_Follows";
-
-Close_locale "Distrib";
-
-
-Goal "!!f::nat=>nat. (INT i: lessThan n. {s. f i <= g i s}) \
-\ <= {s. (\\<Sum>x: lessThan n. f x) <= (\\<Sum>x: lessThan n. g x s)}";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
-qed "alloc_refinement_lemma";
-
-Goal
-"(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 : 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}) \
-\ <= \
-\(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 hf. (INT i : lessThan Nclients. \
-\ {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
-\ LeadsTo {s. (\\<Sum>i: lessThan Nclients. tokens (hf i)) <= \
-\ (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})";
-by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));
-by (rename_tac "F hf" 1);
-by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
- MRS LeadsTo_weaken_R) 1);
- by (Blast_tac 1);
- by (Blast_tac 1);
-by (subgoal_tac "F : Increasing (tokens o (sub i o allocRel))" 1);
- by (blast_tac
- (claset() addIs [impOfSubs (mono_tokens RS mono_Increasing_o)]) 2);
-by (asm_full_simp_tac (simpset() addsimps [Increasing_def, o_assoc]) 1);
-qed "alloc_refinement";
-
-
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Thu Jul 03 12:56:48 2003 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Thu Jul 03 18:07:50 2003 +0200
@@ -2,42 +2,42 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-
-Implementation of a multiple-client allocator from a single-client allocator
*)
-AllocImpl = AllocBase + Follows + PPROD +
+header{*Implementation of a multiple-client allocator from a single-client allocator*}
+
+theory AllocImpl = AllocBase + Follows + PPROD:
(** State definitions. OUTPUT variables are locals **)
(*Type variable 'b is the type of items being merged*)
record 'b merge =
- In :: nat => 'b list (*merge's INPUT histories: streams to merge*)
- Out :: 'b list (*merge's OUTPUT history: merged items*)
- iOut :: nat list (*merge's OUTPUT history: origins of merged items*)
+ In :: "nat => 'b list" (*merge's INPUT histories: streams to merge*)
+ Out :: "'b list" (*merge's OUTPUT history: merged items*)
+ iOut :: "nat list" (*merge's OUTPUT history: origins of merged items*)
record ('a,'b) merge_d =
- 'b merge +
+ "'b merge" +
dummy :: 'a (*dummy field for new variables*)
constdefs
- non_dummy :: ('a,'b) merge_d => 'b merge
+ non_dummy :: "('a,'b) merge_d => 'b merge"
"non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
record 'b distr =
- In :: 'b list (*items to distribute*)
- iIn :: nat list (*destinations of items to distribute*)
- Out :: nat => 'b list (*distributed items*)
+ In :: "'b list" (*items to distribute*)
+ iIn :: "nat list" (*destinations of items to distribute*)
+ Out :: "nat => 'b list" (*distributed items*)
record ('a,'b) distr_d =
- 'b distr +
+ "'b distr" +
dummy :: 'a (*dummy field for new variables*)
record allocState =
- giv :: nat list (*OUTPUT history: source of tokens*)
- ask :: nat list (*INPUT: tokens requested from allocator*)
- rel :: nat list (*INPUT: tokens released to allocator*)
+ giv :: "nat list" (*OUTPUT history: source of tokens*)
+ ask :: "nat list" (*INPUT: tokens requested from allocator*)
+ rel :: "nat list" (*INPUT: tokens released to allocator*)
record 'a allocState_d =
allocState +
@@ -45,9 +45,9 @@
record 'a systemState =
allocState +
- mergeRel :: nat merge
- mergeAsk :: nat merge
- distr :: nat distr
+ mergeRel :: "nat merge"
+ mergeAsk :: "nat merge"
+ distr :: "nat distr"
dummy :: 'a (*dummy field for new variables*)
@@ -56,154 +56,152 @@
(** Merge specification (the number of inputs is Nclients) ***)
(*spec (10)*)
- merge_increasing :: ('a,'b) merge_d program set
+ merge_increasing :: "('a,'b) merge_d program set"
"merge_increasing ==
UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
(*spec (11)*)
- merge_eqOut :: ('a,'b) merge_d program set
+ merge_eqOut :: "('a,'b) merge_d program set"
"merge_eqOut ==
UNIV guarantees
Always {s. length (merge.Out s) = length (merge.iOut s)}"
(*spec (12)*)
- merge_bounded :: ('a,'b) merge_d program set
+ merge_bounded :: "('a,'b) merge_d program set"
"merge_bounded ==
UNIV guarantees
- Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
+ Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
(*spec (13)*)
- merge_follows :: ('a,'b) merge_d program set
+ merge_follows :: "('a,'b) merge_d program set"
"merge_follows ==
- (INT i : lessThan Nclients. Increasing (sub i o merge.In))
+ (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
guarantees
- (INT i : lessThan Nclients.
+ (\<Inter>i \<in> lessThan Nclients.
(%s. sublist (merge.Out s)
{k. k < size(merge.iOut s) & merge.iOut s! k = i})
Fols (sub i o merge.In))"
(*spec: preserves part*)
- merge_preserves :: ('a,'b) merge_d program set
+ merge_preserves :: "('a,'b) merge_d program set"
"merge_preserves == preserves merge.In Int preserves merge_d.dummy"
(*environmental constraints*)
- merge_allowed_acts :: ('a,'b) merge_d program set
+ merge_allowed_acts :: "('a,'b) merge_d program set"
"merge_allowed_acts ==
{F. AllowedActs F =
insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
- merge_spec :: ('a,'b) merge_d program set
+ merge_spec :: "('a,'b) merge_d program set"
"merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
merge_follows Int merge_allowed_acts Int merge_preserves"
(** Distributor specification (the number of outputs is Nclients) ***)
(*spec (14)*)
- distr_follows :: ('a,'b) distr_d program set
+ distr_follows :: "('a,'b) distr_d program set"
"distr_follows ==
Increasing distr.In Int Increasing distr.iIn Int
- Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
+ Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
guarantees
- (INT i : lessThan Nclients.
+ (\<Inter>i \<in> lessThan Nclients.
(sub i o distr.Out) Fols
(%s. sublist (distr.In s)
{k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
- distr_allowed_acts :: ('a,'b) distr_d program set
+ distr_allowed_acts :: "('a,'b) distr_d program set"
"distr_allowed_acts ==
{D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
- distr_spec :: ('a,'b) distr_d program set
+ distr_spec :: "('a,'b) distr_d program set"
"distr_spec == distr_follows Int distr_allowed_acts"
(** Single-client allocator specification (required) ***)
(*spec (18)*)
- alloc_increasing :: 'a allocState_d program set
+ alloc_increasing :: "'a allocState_d program set"
"alloc_increasing == UNIV guarantees Increasing giv"
(*spec (19)*)
- alloc_safety :: 'a allocState_d program set
+ alloc_safety :: "'a allocState_d program set"
"alloc_safety ==
Increasing rel
guarantees Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
(*spec (20)*)
- alloc_progress :: 'a allocState_d program set
+ alloc_progress :: "'a allocState_d program set"
"alloc_progress ==
Increasing ask Int Increasing rel Int
- Always {s. ALL elt : set (ask s). elt <= NbT}
+ Always {s. \<forall>elt \<in> set (ask s). elt <= NbT}
Int
- (INT h. {s. h <= giv s & h pfixGe (ask s)}
+ (\<Inter>h. {s. h <= giv s & h pfixGe (ask s)}
LeadsTo
{s. tokens h <= tokens (rel s)})
- guarantees (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+ guarantees (\<Inter>h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
(*spec: preserves part*)
- alloc_preserves :: 'a allocState_d program set
+ alloc_preserves :: "'a allocState_d program set"
"alloc_preserves == preserves rel Int
preserves ask Int
preserves allocState_d.dummy"
(*environmental constraints*)
- alloc_allowed_acts :: 'a allocState_d program set
+ alloc_allowed_acts :: "'a allocState_d program set"
"alloc_allowed_acts ==
{F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
- alloc_spec :: 'a allocState_d program set
+ alloc_spec :: "'a allocState_d program set"
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
alloc_allowed_acts Int alloc_preserves"
locale Merge =
- fixes
- M :: ('a,'b::order) merge_d program
+ fixes M :: "('a,'b::order) merge_d program"
assumes
- Merge_spec "M : merge_spec"
+ Merge_spec: "M \<in> merge_spec"
locale Distrib =
- fixes
- D :: ('a,'b::order) distr_d program
+ fixes D :: "('a,'b::order) distr_d program"
assumes
- Distrib_spec "D : distr_spec"
+ Distrib_spec: "D \<in> distr_spec"
(****
-# (** Network specification ***)
+# {** Network specification ***}
-# (*spec (9.1)*)
-# network_ask :: 'a systemState program set
-# "network_ask == INT i : lessThan Nclients.
+# {*spec (9.1)*}
+# network_ask :: "'a systemState program set
+# "network_ask == \<Inter>i \<in> lessThan Nclients.
# Increasing (ask o sub i o client)
# guarantees[ask]
# (ask Fols (ask o sub i o client))"
-# (*spec (9.2)*)
-# network_giv :: 'a systemState program set
-# "network_giv == INT i : lessThan Nclients.
+# {*spec (9.2)*}
+# network_giv :: "'a systemState program set
+# "network_giv == \<Inter>i \<in> lessThan Nclients.
# Increasing giv
# guarantees[giv o sub i o client]
-# ((giv o sub i o client) Fols giv )"
+# ((giv o sub i o client) Fols giv)"
-# (*spec (9.3)*)
-# network_rel :: 'a systemState program set
-# "network_rel == INT i : lessThan Nclients.
+# {*spec (9.3)*}
+# network_rel :: "'a systemState program set
+# "network_rel == \<Inter>i \<in> lessThan Nclients.
# Increasing (rel o sub i o client)
# guarantees[rel]
# (rel Fols (rel o sub i o client))"
-# (*spec: preserves part*)
-# network_preserves :: 'a systemState program set
+# {*spec: preserves part*}
+# network_preserves :: "'a systemState program set
# "network_preserves == preserves giv Int
-# (INT i : lessThan Nclients.
+# (\<Inter>i \<in> lessThan Nclients.
# preserves (funPair rel ask o sub i o client))"
-# network_spec :: 'a systemState program set
+# network_spec :: "'a systemState program set
# "network_spec == network_ask Int network_giv Int
# network_rel Int network_preserves"
-# (** State mappings **)
+# {** State mappings **}
# sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
# "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
# in (| giv = giv s,
@@ -221,4 +219,171 @@
# systemState.dummy = allocState_d.dummy al|)"
****)
+
+declare subset_preserves_o [THEN subsetD, intro]
+declare funPair_o_distrib [simp]
+declare Always_INT_distrib [simp]
+declare o_apply [simp del]
+
+
+subsection{*Theorems for Merge*}
+
+lemma (in Merge) Merge_Allowed:
+ "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
+apply (cut_tac Merge_spec)
+apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
+done
+
+lemma (in Merge) M_ok_iff [iff]:
+ "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &
+ M \<in> Allowed G)"
+by (auto simp add: Merge_Allowed ok_iff_Allowed)
+
+
+lemma (in Merge) Merge_Always_Out_eq_iOut:
+ "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
+ ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
+apply (cut_tac Merge_spec)
+apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
+done
+
+lemma (in Merge) Merge_Bounded:
+ "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
+ ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
+apply (cut_tac Merge_spec)
+apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
+done
+
+lemma (in Merge) Merge_Bag_Follows_lemma:
+ "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
+ ==> M Join G \<in> Always
+ {s. (\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s)
+ {k. k < length (iOut s) & iOut s ! k = i})) =
+ (bag_of o merge.Out) s}"
+apply (rule Always_Compl_Un_eq [THEN iffD1])
+apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
+apply (rule UNIV_AlwaysI, clarify)
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+ apply (simp)
+ apply blast
+apply (simp add: set_conv_nth)
+apply (subgoal_tac
+ "(\<Union>i \<in> lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
+ lessThan (length (iOut x))")
+ apply (simp (no_asm_simp) add: o_def)
+apply blast
+done
+
+lemma (in Merge) Merge_Bag_Follows:
+ "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
+ guarantees
+ (bag_of o merge.Out) Fols
+ (%s. \<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)"
+apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
+apply (rule Follows_setsum)
+apply (cut_tac Merge_spec)
+apply (auto simp add: merge_spec_def merge_follows_def o_def)
+apply (drule guaranteesD)
+ prefer 3
+ apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
+done
+
+
+subsection{*Theorems for Distributor*}
+
+lemma (in Distrib) Distr_Increasing_Out:
+ "D \<in> Increasing distr.In Int Increasing distr.iIn Int
+ Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
+ guarantees
+ (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))"
+apply (cut_tac Distrib_spec)
+apply (simp add: distr_spec_def distr_follows_def)
+apply clarify
+apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
+done
+
+lemma (in Distrib) Distr_Bag_Follows_lemma:
+ "[| G \<in> preserves distr.Out;
+ D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
+ ==> D Join G \<in> Always
+ {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
+ {k. k < length (iIn s) & iIn s ! k = i})) =
+ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
+apply (erule Always_Compl_Un_eq [THEN iffD1])
+apply (rule UNIV_AlwaysI, clarify)
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+ apply (simp (no_asm))
+ apply blast
+apply (simp add: set_conv_nth)
+apply (subgoal_tac
+ "(\<Union>i \<in> lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) =
+ lessThan (length (iIn x))")
+ apply (simp (no_asm_simp))
+apply blast
+done
+
+lemma (in Distrib) D_ok_iff [iff]:
+ "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
+apply (cut_tac Distrib_spec)
+apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
+ safety_prop_Acts_iff ok_iff_Allowed)
+done
+
+lemma (in Distrib) Distr_Bag_Follows:
+ "D \<in> Increasing distr.In Int Increasing distr.iIn Int
+ Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
+ guarantees
+ (\<Inter>i \<in> lessThan Nclients.
+ (%s. \<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s)
+ Fols
+ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
+apply (rule guaranteesI, clarify)
+apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
+apply (rule Follows_setsum)
+apply (cut_tac Distrib_spec)
+apply (auto simp add: distr_spec_def distr_follows_def o_def)
+apply (drule guaranteesD)
+ prefer 3
+ apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
+done
+
+
+subsection{*Theorems for Allocator*}
+
+lemma alloc_refinement_lemma:
+ "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i <= g i s})
+ <= {s. (\<Sum>x \<in> lessThan n. f x) <= (\<Sum>x: lessThan n. g x s)}"
+apply (induct_tac "n")
+apply (auto simp add: lessThan_Suc)
+done
+
+lemma alloc_refinement:
+"(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
+ Increasing (sub i o allocRel))
+ Int
+ Always {s. \<forall>i. i<Nclients -->
+ (\<forall>elt \<in> set ((sub i o allocAsk) s). elt <= NbT)}
+ Int
+ (\<Inter>i \<in> lessThan Nclients.
+ \<Inter>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})
+ <=
+ (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
+ Increasing (sub i o allocRel))
+ Int
+ Always {s. \<forall>i. i<Nclients -->
+ (\<forall>elt \<in> set ((sub i o allocAsk) s). elt <= NbT)}
+ Int
+ (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.
+ {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})
+ LeadsTo {s. (\<Sum>i: lessThan Nclients. tokens (hf i)) <=
+ (\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})"
+apply (auto simp add: ball_conj_distrib)
+apply (rename_tac F hf)
+apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
+apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))")
+ apply (simp add: Increasing_def o_assoc)
+apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
+done
+
end
--- a/src/HOL/UNITY/Comp/Client.ML Thu Jul 03 12:56:48 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-(* Title: HOL/UNITY/Client
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Distributed Resource Management System: the Client
-*)
-
-Addsimps [Client_def RS def_prg_Init,
- Client_def RS def_prg_AllowedActs];
-Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
-
-Goal "(Client ok G) = \
-\ (G : preserves rel & G : preserves ask & G : preserves tok &\
-\ Client : Allowed G)";
-by (auto_tac (claset(),
- simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed]));
-qed "Client_ok_iff";
-AddIffs [Client_ok_iff];
-
-
-(*Safety property 1: ask, rel are increasing*)
-Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
-by (auto_tac
- (claset() addSIs [increasing_imp_Increasing],
- simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
-by (auto_tac (claset(), simpset() addsimps [Client_def, increasing_def]));
-by (ALLGOALS constrains_tac);
-by Auto_tac;
-qed "increasing_ask_rel";
-
-Addsimps [nth_append, append_one_prefix];
-
-
-(*Safety property 2: the client never requests too many tokens.
- With no Substitution Axiom, we must prove the two invariants
- simultaneously.
-*)
-Goal "Client ok G \
-\ ==> Client Join G : \
-\ Always ({s. tok s <= NbT} Int \
-\ {s. ALL elt : set (ask s). elt <= NbT})";
-by Auto_tac;
-by (rtac (invariantI RS stable_Join_Always2) 1);
-by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
- addSIs [stable_Int]) 3);
-by (asm_full_simp_tac (simpset() addsimps [Client_def]) 2);
-by (constrains_tac 2);
-by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
-by Auto_tac;
-qed "ask_bounded_lemma";
-
-(*export version, with no mention of tok in the postcondition, but
- unfortunately tok must be declared local.*)
-Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
-by (rtac guaranteesI 1);
-by (etac (ask_bounded_lemma RS Always_weaken) 1);
-by (rtac Int_lower2 1);
-qed "ask_bounded";
-
-
-(*** Towards proving the liveness property ***)
-
-Goal "Client: stable {s. rel s <= giv s}";
-by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "stable_rel_le_giv";
-
-Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
-\ ==> Client Join G : Stable {s. rel s <= giv s}";
-by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
-by Auto_tac;
-qed "Join_Stable_rel_le_giv";
-
-Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
-\ ==> Client Join G : Always {s. rel s <= giv s}";
-by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
-qed "Join_Always_rel_le_giv";
-
-Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
-by (simp_tac (simpset() addsimps [Client_def, mk_total_program_def]) 1);
-by (res_inst_tac [("act", "rel_act")] totalize_transientI 1);
-by (auto_tac (claset(),
- simpset() addsimps [Domain_def, Client_def]));
-by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
- strict_prefix_length_less]) 1);
-by (auto_tac (claset(),
- simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
-by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
-qed "transient_lemma";
-
-
-Goal "[| Client Join G : Increasing giv; Client ok G |] \
-\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \
-\ LeadsTo {s. k < rel s & rel s <= giv s & \
-\ h <= giv s & h pfixGe ask s}";
-by (rtac single_LeadsTo_I 1);
-by (ftac (increasing_ask_rel RS guaranteesD) 1);
-by Auto_tac;
-by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS
- leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
-by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
-by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
-by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
-by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
-by (etac Join_Stable_rel_le_giv 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addIs [sym, order_less_le RS iffD2,
- order_trans, prefix_imp_pfixGe,
- pfixGe_trans]) 2);
-by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
-qed "induct_lemma";
-
-
-Goal "[| Client Join G : Increasing giv; Client ok G |] \
-\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \
-\ LeadsTo {s. h <= rel s}";
-by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
-by (auto_tac (claset(), simpset() addsimps [vimage_def]));
-by (rtac single_LeadsTo_I 1);
-by (rtac (induct_lemma RS LeadsTo_weaken) 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [order_less_le RS iffD2]
- addDs [common_prefix_linear]) 1);
-by (REPEAT (dtac strict_prefix_length_less 1));
-by (arith_tac 1);
-qed "rel_progress_lemma";
-
-
-Goal "[| Client Join G : Increasing giv; Client ok G |] \
-\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s} \
-\ LeadsTo {s. h <= rel s}";
-by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
-by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS
- LeadsTo_Un RS LeadsTo_weaken_L) 3);
-by Auto_tac;
-by (blast_tac (claset() addIs [order_less_le RS iffD2]
- addDs [common_prefix_linear]) 1);
-qed "client_progress_lemma";
-
-(*Progress property: all tokens that are given will be released*)
-Goal "Client : \
-\ Increasing giv guarantees \
-\ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
-by (rtac guaranteesI 1);
-by (Clarify_tac 1);
-by (blast_tac (claset() addIs [client_progress_lemma]) 1);
-qed "client_progress";
-
-(*This shows that the Client won't alter other variables in any state
- that it is combined with*)
-Goal "Client : preserves dummy";
-by (asm_full_simp_tac (simpset() addsimps [Client_def, preserves_def]) 1);
-by (Clarify_tac 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "client_preserves_dummy";
-
-
-(** Obsolete lemmas from first version of the Client **)
-
-Goal "Client: stable {s. size (rel s) <= size (giv s)}";
-by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "stable_size_rel_le_giv";
-
-(*clients return the right number of tokens*)
-Goal "Client : Increasing giv guarantees Always {s. rel s <= giv s}";
-by (rtac guaranteesI 1);
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (blast_tac (claset() addIs [Increasing_preserves_Stable,
- stable_rel_le_giv]) 1);
-qed "ok_guar_rel_prefix_giv";
--- a/src/HOL/UNITY/Comp/Client.thy Thu Jul 03 12:56:48 2003 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy Thu Jul 03 18:07:50 2003 +0200
@@ -2,24 +2,24 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-
-Distributed Resource Management System: the Client
*)
-Client = Rename + AllocBase +
+header{*Distributed Resource Management System: the Client*}
+
+theory Client = Rename + AllocBase:
types
- tokbag = nat (*tokbags could be multisets...or any ordered type?*)
+ tokbag = nat --{*tokbags could be multisets...or any ordered type?*}
record state =
- giv :: tokbag list (*input history: tokens granted*)
- ask :: tokbag list (*output history: tokens requested*)
- rel :: tokbag list (*output history: tokens released*)
- tok :: tokbag (*current token request*)
+ giv :: "tokbag list" --{*input history: tokens granted*}
+ ask :: "tokbag list" --{*output history: tokens requested*}
+ rel :: "tokbag list" --{*output history: tokens released*}
+ tok :: tokbag --{*current token request*}
record 'a state_d =
state +
- dummy :: 'a (*new variables*)
+ dummy :: 'a --{*new variables*}
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -30,10 +30,10 @@
rel_act :: "('a state_d * 'a state_d) set"
"rel_act == {(s,s').
- \\<exists>nrel. nrel = size (rel s) &
+ \<exists>nrel. nrel = size (rel s) &
s' = s (| rel := rel s @ [giv s!nrel] |) &
nrel < size (giv s) &
- ask s!nrel <= giv s!nrel}"
+ ask s!nrel \<le> giv s!nrel}"
(** Choose a new token requirement **)
@@ -47,21 +47,172 @@
"ask_act == {(s,s'). s'=s |
(s' = s (|ask := ask s @ [tok s]|))}"
- Client :: 'a state_d program
+ Client :: "'a state_d program"
"Client ==
mk_total_program
- ({s. tok s : atMost NbT &
+ ({s. tok s \<in> atMost NbT &
giv s = [] & ask s = [] & rel s = []},
{rel_act, tok_act, ask_act},
- \\<Union>G \\<in> preserves rel Int preserves ask Int preserves tok.
+ \<Union>G \<in> preserves rel Int preserves ask Int preserves tok.
Acts G)"
(*Maybe want a special theory section to declare such maps*)
- non_dummy :: 'a state_d => state
+ non_dummy :: "'a state_d => state"
"non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
(*Renaming map to put a Client into the standard form*)
client_map :: "'a state_d => state*'a"
"client_map == funPair non_dummy dummy"
+
+declare Client_def [THEN def_prg_Init, simp]
+declare Client_def [THEN def_prg_AllowedActs, simp]
+declare rel_act_def [THEN def_act_simp, simp]
+declare tok_act_def [THEN def_act_simp, simp]
+declare ask_act_def [THEN def_act_simp, simp]
+
+lemma Client_ok_iff [iff]:
+ "(Client ok G) =
+ (G \<in> preserves rel & G \<in> preserves ask & G \<in> preserves tok &
+ Client \<in> Allowed G)"
+by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed])
+
+
+text{*Safety property 1: ask, rel are increasing*}
+lemma increasing_ask_rel:
+ "Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
+apply (auto simp add: Client_def increasing_def)
+apply (constrains, auto)+
+done
+
+declare nth_append [simp] append_one_prefix [simp]
+
+
+text{*Safety property 2: the client never requests too many tokens.
+ With no Substitution Axiom, we must prove the two invariants
+ simultaneously. *}
+lemma ask_bounded_lemma:
+ "Client ok G
+ ==> Client Join G \<in>
+ Always ({s. tok s \<le> NbT} Int
+ {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
+apply auto
+apply (rule invariantI [THEN stable_Join_Always2], force)
+ prefer 2
+ apply (fast elim!: preserves_subset_stable [THEN subsetD] intro!: stable_Int)
+apply (simp add: Client_def, constrains)
+apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
+done
+
+text{*export version, with no mention of tok in the postcondition, but
+ unfortunately tok must be declared local.*}
+lemma ask_bounded:
+ "Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}"
+apply (rule guaranteesI)
+apply (erule ask_bounded_lemma [THEN Always_weaken])
+apply (rule Int_lower2)
+done
+
+
+text{*** Towards proving the liveness property ***}
+
+lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
+by (simp add: Client_def, constrains, auto)
+
+lemma Join_Stable_rel_le_giv:
+ "[| Client Join G \<in> Increasing giv; G \<in> preserves rel |]
+ ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
+by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
+
+lemma Join_Always_rel_le_giv:
+ "[| Client Join G \<in> Increasing giv; G \<in> preserves rel |]
+ ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
+by (force intro: AlwaysI Join_Stable_rel_le_giv)
+
+lemma transient_lemma:
+ "Client \<in> transient {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}"
+apply (simp add: Client_def mk_total_program_def)
+apply (rule_tac act = rel_act in totalize_transientI)
+ apply (auto simp add: Domain_def Client_def)
+ apply (blast intro: less_le_trans prefix_length_le strict_prefix_length_less)
+apply (auto simp add: prefix_def genPrefix_iff_nth Ge_def)
+apply (blast intro: strict_prefix_length_less)
+done
+
+
+lemma induct_lemma:
+ "[| Client Join G \<in> Increasing giv; Client ok G |]
+ ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}
+ LeadsTo {s. k < rel s & rel s \<le> giv s &
+ h \<le> giv s & h pfixGe ask s}"
+apply (rule single_LeadsTo_I)
+apply (frule increasing_ask_rel [THEN guaranteesD], auto)
+apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
+ apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
+ apply (erule_tac f = giv and x = "giv s" in IncreasingD)
+ apply (erule_tac f = ask and x = "ask s" in IncreasingD)
+ apply (erule_tac f = rel and x = "rel s" in IncreasingD)
+ apply (erule Join_Stable_rel_le_giv, blast)
+ apply (blast intro: order_less_imp_le order_trans)
+apply (blast intro: sym order_less_le [THEN iffD2] order_trans
+ prefix_imp_pfixGe pfixGe_trans)
+done
+
+
+lemma rel_progress_lemma:
+ "[| Client Join G \<in> Increasing giv; Client ok G |]
+ ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}
+ LeadsTo {s. h \<le> rel s}"
+apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
+apply (auto simp add: vimage_def)
+apply (rule single_LeadsTo_I)
+apply (rule induct_lemma [THEN LeadsTo_weaken], auto)
+ apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
+apply (drule strict_prefix_length_less)+
+apply arith
+done
+
+
+lemma client_progress_lemma:
+ "[| Client Join G \<in> Increasing giv; Client ok G |]
+ ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}
+ LeadsTo {s. h \<le> rel s}"
+apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all)
+apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
+ apply (blast intro: rel_progress_lemma)
+ apply (rule subset_refl [THEN subset_imp_LeadsTo])
+apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
+done
+
+text{*Progress property: all tokens that are given will be released*}
+lemma client_progress:
+ "Client \<in>
+ Increasing giv guarantees
+ (INT h. {s. h \<le> giv s & h pfixGe ask s} LeadsTo {s. h \<le> rel s})"
+apply (rule guaranteesI, clarify)
+apply (blast intro: client_progress_lemma)
+done
+
+text{*This shows that the Client won't alter other variables in any state
+ that it is combined with*}
+lemma client_preserves_dummy: "Client \<in> preserves dummy"
+by (simp add: Client_def preserves_def, clarify, constrains, auto)
+
+
+text{** Obsolete lemmas from first version of the Client **}
+
+lemma stable_size_rel_le_giv:
+ "Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
+by (simp add: Client_def, constrains, auto)
+
+text{*clients return the right number of tokens*}
+lemma ok_guar_rel_prefix_giv:
+ "Client \<in> Increasing giv guarantees Always {s. rel s \<le> giv s}"
+apply (rule guaranteesI)
+apply (rule AlwaysI, force)
+apply (blast intro: Increasing_preserves_Stable stable_rel_le_giv)
+done
+
+
end