--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/AllocImpl.ML Fri Jun 02 18:32:04 2000 +0200
@@ -0,0 +1,86 @@
+(* 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
+
+add_path "../Induct";
+time_use_thy "AllocImpl";
+*)
+
+AddIs [impOfSubs subset_preserves_o];
+Addsimps [funPair_o_distrib];
+Addsimps [Always_INT_distrib];
+Delsimps [o_apply];
+
+(*Eliminate the "o" operator*)
+val o_simp = simplify (simpset() addsimps [o_def]);
+
+Goalw [merge_spec_def,merge_eqOut_def]
+ "[| M: merge_spec; G: preserves merge.Out; G: preserves merge.iOut |] \
+\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
+by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
+qed "Merge_Always_Out_eq_iOut";
+
+
+Goal "M : merge_spec \
+\ ==> M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
+\ guarantees[funPair merge.Out merge.iOut] \
+\ (bag_of o merge.Out) Fols \
+\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
+\ (lessThan Nclients))";
+by (rtac guaranteesI 1);
+by (res_inst_tac [("f", "%s. bag_of (sublist (merge.Out s) {..length(merge.iOut s)(})")]
+ Always_Follows 1);
+by (etac (Merge_Always_Out_eq_iOut RS Always_Compl_Un_eq RS iffD1) 1);
+by (force_tac (claset() addIs [UNIV_AlwaysI], simpset() addsimps [o_apply]) 3);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [sublist_upt_eq_take]
+ addsimps [bag_of_sublist]) 1);
+by (rtac Follows_trans 1);
+by (rtac Follows_setsum 2);
+by (asm_full_simp_tac (simpset() addsimps []) 3);
+by (Clarify_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [o_assoc RS sym]) 2);
+by (rtac (impOfSubs (mono_bag_of RS mono_Follows_o)) 2);
+
+(*Now need to invoke the merge_follows guarantee*)
+
+by (asm_full_simp_tac (simpset() addsimps [merge_spec_def,merge_follows_def]) 2);
+
+
+by (res_inst_tac [("f", "%s. bag_of (sublist (merge.Out s) {..length(merge.iOut s)(})")]
+ Always_Follows 1);
+
+setsum (%i. if i < length l then {# nth l i #} else {#}) {..length (iOut s)(}
+
+ : (%s. bag_of
+ (sublist (merge.Out s) {..length (iOut s)(})) Fols
+ (%s. setsum (%i. (bag_of o sub i o merge.In) s)
+ {..Nclients(})
+
+
+ (%s. sublist (merge.Out s)
+ {k. k < size(merge.iOut s) & nth(merge.iOut s)k = i})
+ Fols (sub i o merge.In))"
+
+
+by Auto_tac;
+by (dtac guaranteesD 1);
+by Auto_tac;
+by (rtac guaranteesI 1);
+
+merge_eqOut
+
+Always_Int_eq
+
+
+by (simp_tac (simpset() addsimps [o_def]) 1);
+by (subgoal_tac
+ "ALL s. merge.Out s = sublist (merge.Out s) {..length(merge.iOut s)(}" 1);
+by (etac ssubst 1);
+by (asm_simp_tac (simpset() addsimps [bag_of_sublist]) 1);
+by (stac bag_of_sublist 1);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/AllocImpl.thy Fri Jun 02 18:32:04 2000 +0200
@@ -0,0 +1,213 @@
+(* Title: HOL/UNITY/AllocImpl
+ 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
+
+add_path "../Induct";
+with_path "../Induct" time_use_thy "AllocImpl";
+*)
+
+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*)
+
+record ('a,'b) merge_u =
+ 'b merge +
+ extra :: 'a (*dummy field for new variables*)
+
+constdefs
+ non_extra :: ('a,'b) merge_u => 'b merge
+ "non_extra 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*)
+
+record ('a,'b) distr_u =
+ 'b distr +
+ extra :: '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*)
+
+record 'a allocState_u =
+ allocState +
+ extra :: 'a (*dummy field for new variables*)
+
+record 'a systemState =
+ allocState +
+ mergeRel :: nat merge
+ mergeAsk :: nat merge
+ distr :: nat distr
+ extra :: 'a (*dummy field for new variables*)
+
+
+constdefs
+
+(** Merge specification (NbT is the number of inputs) ***)
+
+ (*spec (10)*)
+ merge_increasing :: ('a,'b) merge_u program set
+ "merge_increasing ==
+ UNIV guarantees[funPair merge.Out merge.iOut]
+ (Increasing merge.Out) Int (Increasing merge.iOut)"
+
+ (*spec (11)*)
+ merge_eqOut :: ('a,'b) merge_u program set
+ "merge_eqOut ==
+ UNIV guarantees[funPair merge.Out merge.iOut]
+ Always {s. length (merge.Out s) = length (merge.iOut s)}"
+
+ (*spec (12)*)
+ merge_bounded :: ('a,'b) merge_u program set
+ "merge_bounded ==
+ UNIV guarantees[merge.iOut]
+ Always {s. ALL elt : set (merge.iOut s). elt <= NbT}"
+
+ (*spec (13)*)
+ merge_follows :: ('a,'b) merge_u program set
+ "merge_follows ==
+ (INT i : lessThan Nclients. Increasing (sub i o merge.In))
+ guarantees[funPair merge.Out merge.iOut]
+ (INT i : lessThan Nclients.
+ (%s. sublist (merge.Out s)
+ {k. k < size(merge.iOut s) & nth(merge.iOut s)k = i})
+ Fols (sub i o merge.In))"
+
+(*
+ (%s. map fst (filter (%p. snd p = i)
+ (zip (merge.Out s) (merge.iOut s))))
+ Fols (sub i o merge.In)
+*)
+
+ (*spec: preserves part*)
+ merge_preserves :: ('a,'b) merge_u program set
+ "merge_preserves == preserves (funPair merge.In merge_u.extra)"
+
+ merge_spec :: ('a,'b) merge_u program set
+ "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
+ merge_follows Int merge_preserves"
+
+(** Single-client allocator specification (required) ***)
+
+ (*spec (18)*)
+ alloc_increasing :: 'a allocState_u program set
+ "alloc_increasing == UNIV guarantees[giv] Increasing giv"
+
+ (*spec (19)*)
+ alloc_safety :: 'a allocState_u program set
+ "alloc_safety ==
+ Increasing rel
+ guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
+
+ (*spec (20)*)
+ alloc_progress :: 'a allocState_u program set
+ "alloc_progress ==
+ Increasing ask Int Increasing rel Int
+ Always {s. ALL elt : set (ask s). elt <= NbT}
+ Int
+ (INT h. {s. h <= giv s & h pfixGe (ask s)}
+ LeadsTo
+ {s. tokens h <= tokens (rel s)})
+ guarantees[giv]
+ (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+
+ (*spec: preserves part*)
+ alloc_preserves :: 'a allocState_u program set
+ "alloc_preserves == preserves (funPair rel
+ (funPair ask allocState_u.extra))"
+
+ alloc_spec :: 'a allocState_u program set
+ "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
+ alloc_preserves"
+
+(****
+ (** Network specification ***)
+
+ (*spec (9.1)*)
+ network_ask :: 'a systemState program set
+ "network_ask == INT i : 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.
+ Increasing giv
+ guarantees[giv o sub i o client]
+ ((giv o sub i o client) Fols giv )"
+
+ (*spec (9.3)*)
+ network_rel :: 'a systemState program set
+ "network_rel == INT i : 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
+ "network_preserves == preserves giv Int
+ (INT i : lessThan Nclients.
+ preserves (funPair rel ask o sub i o client))"
+
+ network_spec :: 'a systemState program set
+ "network_spec == network_ask Int network_giv Int
+ network_rel Int network_preserves"
+
+
+ (** State mappings **)
+ sysOfAlloc :: "((nat => merge) * 'a) allocState_u => 'a systemState"
+ "sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+ in (| giv = giv s,
+ ask = ask s,
+ rel = rel s,
+ client = cl,
+ extra = xtr|)"
+
+
+ sysOfClient :: "(nat => merge) * 'a allocState_u => 'a systemState"
+ "sysOfClient == %(cl,al). (| giv = giv al,
+ ask = ask al,
+ rel = rel al,
+ client = cl,
+ systemState.extra = allocState_u.extra al|)"
+****)
+
+consts
+ Alloc :: 'a allocState_u program
+ Merge :: ('a,'b) merge_u program
+(*
+ Network :: 'a systemState program
+ System :: 'a systemState program
+ *)
+
+rules
+ Alloc "Alloc : alloc_spec"
+ Merge "Merge : merge_spec"
+(** Network "Network : network_spec"**)
+
+
+
+(**
+defs
+ System_def
+ "System == rename sysOfAlloc Alloc Join Network Join
+ (rename sysOfMerge
+ (plam x: lessThan Nclients. rename merge_map Merge))"
+**)
+
+
+end