--- a/src/ZF/IsaMakefile Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/IsaMakefile Thu May 29 17:10:00 2003 +0200
@@ -121,9 +121,11 @@
UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
UNITY/AllocBase.ML UNITY/AllocBase.thy\
+ UNITY/ClientImpl.ML UNITY/ClientImpl.thy\
UNITY/Distributor.ML UNITY/Distributor.thy\
UNITY/Follows.ML UNITY/Follows.thy\
UNITY/Increasing.ML UNITY/Increasing.thy\
+ UNITY/Merge.ML UNITY/Merge.thy\
UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
UNITY/WFair.ML UNITY/WFair.thy
--- a/src/ZF/UNITY/AllocBase.ML Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.ML Thu May 29 17:10:00 2003 +0200
@@ -42,7 +42,7 @@
\ (ALL i:nat. i<n --> f(i) $<= g(i)) --> \
\ setsum(f, n) $<= setsum(g,n)";
by (induct_tac "n" 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [])));
+by (ALLGOALS Asm_full_simp_tac);
by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x~:x" 1);
by (Clarify_tac 1);
by (Asm_simp_tac 1);
@@ -54,8 +54,7 @@
by (Clarify_tac 1);
by (dtac leI 1);
by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [nat_into_Finite,
- mem_not_refl, succ_def]) 1);
+by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1);
qed_spec_mp "setsum_fun_mono";
Goal "l:list(A) ==> tokens(l):nat";
@@ -218,7 +217,7 @@
by (subgoal_tac
"B Int C Int length(l) = \
\ (B Int length(l)) Int (C Int length(l))" 1);
-by (blast_tac (claset() addIs []) 2);
+by (Blast_tac 2);
by (asm_simp_tac (simpset() addsimps [bag_of_sublist,
Int_Un_distrib2, msetsum_Un_Int]) 1);
by (resolve_tac [msetsum_Un_Int] 1);
@@ -314,7 +313,8 @@
bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD);
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
-fun list_of_Int th =
+fun list_of_Int th = list_of_Int_aux (Drule.freeze_all th)
+and list_of_Int_aux th =
(list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
handle THM _ => (list_of_Int (th RS InterD))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/ClientImpl.ML Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,309 @@
+(* Title: ZF/UNITY/Client.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+Distributed Resource Management System: the Client
+*)
+Addsimps [type_assumes, default_val_assumes];
+(* This part should be automated *)
+
+Goalw [state_def] "s:state ==> s`ask:list(nat)";
+by (dres_inst_tac [("a", "ask")] apply_type 1);
+by Auto_tac;
+qed "ask_value_type";
+AddTCs [ask_value_type];
+Addsimps [ask_value_type];
+
+Goalw [state_def] "s:state ==> s`giv:list(nat)";
+by (dres_inst_tac [("a", "giv")] apply_type 1);
+by Auto_tac;
+qed "giv_value_type";
+AddTCs [giv_value_type];
+Addsimps [giv_value_type];
+
+Goalw [state_def]
+"s:state ==> s`rel:list(nat)";
+by (dres_inst_tac [("a", "rel")] apply_type 1);
+by Auto_tac;
+qed "rel_value_type";
+AddTCs [rel_value_type];
+Addsimps [rel_value_type];
+
+Goalw [state_def] "s:state ==> s`tok:nat";
+by (dres_inst_tac [("a", "tok")] apply_type 1);
+by Auto_tac;
+qed "tok_value_type";
+AddTCs [tok_value_type];
+Addsimps [tok_value_type];
+
+(** The Client Program **)
+
+Goalw [client_prog_def] "client_prog:program";
+by (Simp_tac 1);
+qed "client_type";
+Addsimps [client_type];
+AddTCs [client_type];
+
+Addsimps [client_prog_def RS def_prg_Init,
+ client_prog_def RS def_prg_AllowedActs];
+program_defs_ref := [client_prog_def];
+
+Addsimps (map simp_of_act [client_rel_act_def,
+client_tok_act_def, client_ask_act_def]);
+
+Goal "ALL G:program. (client_prog ok G) <-> \
+\ (G:preserves(lift(rel)) & G:preserves(lift(ask)) & \
+\ G:preserves(lift(tok)) & client_prog:Allowed(G))";
+by (auto_tac (claset(),
+ simpset() addsimps [ok_iff_Allowed, client_prog_def RS def_prg_Allowed]));
+qed "client_prog_ok_iff";
+
+Goal "client_prog:(INT x:var-{ask, rel, tok}. preserves(lift(x)))";
+by (rtac Inter_var_DiffI 1);
+by (rtac ballI 2);
+by (rtac preservesI 2);
+by (constrains_tac 2);
+by Auto_tac;
+qed "client_prog_preserves";
+
+
+(*Safety property 1: ask, rel are increasing : (24) *)
+Goalw [guar_def]
+"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))";
+by (auto_tac (claset() addSIs [increasing_imp_Increasing],
+ simpset() addsimps [client_prog_ok_iff, increasing_def]));
+by (ALLGOALS(constrains_tac));
+by (ALLGOALS(thin_tac "mk_program(?u, ?v, ?w):Allowed(?x)"));
+by (auto_tac (claset() addDs [ActsD], simpset()));
+by (dres_inst_tac [("f", "lift(rel)")] preserves_imp_eq 2);
+by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_eq 1);
+by (TRYALL(assume_tac));
+by (ALLGOALS(dtac ActsD));
+by (TRYALL(assume_tac));
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(rotate_tac ~2));
+by Auto_tac;
+qed "client_prog_Increasing_ask_rel";
+
+Addsimps [nth_append, append_one_prefix];
+
+Goal "0<NbT";
+by (cut_facts_tac [NbT_pos] 1);
+by (resolve_tac [Ord_0_lt] 1);
+by Auto_tac;
+qed "NbT_pos2";
+
+(*Safety property 2: the client never requests too many tokens.
+With no Substitution Axiom, we must prove the two invariants simultaneously. *)
+
+Goal
+"[| client_prog ok G; G:program |]\
+\ ==> client_prog Join G : \
+\ Always({s:state. s`tok le NbT} Int \
+\ {s:state. ALL elt:set_of_list(s`ask). elt le NbT})";
+by (rotate_tac ~1 1);
+by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
+by (rtac (invariantI RS stable_Join_Always2) 1);
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(Asm_full_simp_tac));
+by (rtac stable_Int 2);
+by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_stable 3);
+by (dres_inst_tac [("f", "lift(tok)")] preserves_imp_stable 2);
+by (REPEAT(Force_tac 2));
+by (constrains_tac 1);
+by (auto_tac (claset() addDs [ActsD], simpset()));
+by (cut_facts_tac [NbT_pos] 1);
+by (resolve_tac [NbT_pos2 RS mod_less_divisor] 1);
+by (auto_tac (claset() addDs [ActsD, preserves_imp_eq],
+ simpset() addsimps [set_of_list_append]));
+qed "ask_Bounded_lemma";
+
+(* Export version, with no mention of tok in the postcondition, but
+ unfortunately tok must be declared local.*)
+Goal
+"client_prog: program guarantees \
+\ Always({s:state. ALL elt: set_of_list(s`ask). elt le NbT})";
+by (rtac guaranteesI 1);
+by (etac (ask_Bounded_lemma RS Always_weaken) 1);
+by Auto_tac;
+qed "client_prog_ask_Bounded";
+
+(*** Towards proving the liveness property ***)
+
+Goal
+"client_prog: stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+by (constrains_tac 1);
+by Auto_tac;
+qed "client_prog_stable_rel_le_giv";
+
+Goal
+"[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
+\ ==> client_prog Join G: Stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+by (rtac (client_prog_stable_rel_le_giv RS Increasing_preserves_Stable) 1);
+by (auto_tac (claset(), simpset() addsimps [lift_def]));
+qed "client_prog_Join_Stable_rel_le_giv";
+
+Goal "[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
+\ ==> client_prog Join G : Always({s:state. <s`rel, s`giv>:prefix(nat)})";
+by (force_tac (claset() addSIs [AlwaysI, client_prog_Join_Stable_rel_le_giv],
+ simpset()) 1);
+qed "client_prog_Join_Always_rel_le_giv";
+
+Goal "xs:list(A) ==> xs@[a]=xs --> False";
+by (etac list.induct 1);
+by Auto_tac;
+qed "list_app_lemma";
+
+Goal "A == {<s, t>:state*state. P(s, t)} ==> A={<s, t>:state*state. P(s, t)}";
+by Auto_tac;
+qed "def_act_eq";
+
+Goal "A={<s,t>:state*state. P(s, t)} ==> A<=state*state";
+by Auto_tac;
+qed "act_subset";
+
+Goal
+"client_prog: \
+\ transient({s:state. s`rel = k & <k, h>:strict_prefix(nat) \
+\ & <h, s`giv>:prefix(nat) & h pfixGe s`ask})";
+by (res_inst_tac [("act", "client_rel_act")] transientI 1);
+by (simp_tac (simpset() addsimps
+ [client_prog_def RS def_prg_Acts]) 1);
+by (simp_tac (simpset() addsimps
+ [client_rel_act_def RS def_act_eq RS act_subset]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [client_prog_def RS def_prg_Acts,domain_def]));
+by (resolve_tac [ReplaceI] 1);
+by (res_inst_tac [("x", "x(rel:= x`rel @\
+ \ [nth(length(x`rel), x`giv)])")] exI 1);
+by (auto_tac (claset() addSIs [state_update_type,
+ app_type, length_type, nth_type],
+ simpset()));
+by Auto_tac;
+by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
+ strict_prefix_length_lt]) 1);
+by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
+ strict_prefix_length_lt]) 1);
+by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
+by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
+by (auto_tac (claset(),
+ simpset() addsimps [prefix_def, Ge_def]));
+by (dtac strict_prefix_length_lt 1);
+by (dres_inst_tac [("x", "length(x`rel)")] bspec 1);
+by Auto_tac;
+by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
+by (auto_tac (claset(), simpset() addsimps [id_def, lam_def]));
+qed "transient_lemma";
+
+Goalw [strict_prefix_def,id_def, lam_def]
+"<xs, ys>:strict_prefix(A) <-> <xs, ys>:prefix(A) & xs~=ys";
+by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset()));
+qed "strict_prefix_is_prefix";
+
+Goal
+"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] \
+\ ==> client_prog Join G: \
+\ {s:state. s`rel = k & <k,h>:strict_prefix(nat) \
+\ & <h , s`giv>:prefix(nat) & h pfixGe s`ask} \
+\ LeadsTo {s:state. <k, s`rel>:strict_prefix(nat) \
+\ & <s`rel, s`giv>:prefix(nat) & \
+\ <h, s`giv>:prefix(nat) & \
+\ h pfixGe s`ask}";
+by (rtac single_LeadsTo_I 1);
+by (Asm_simp_tac 2);
+by (ftac (client_prog_Increasing_ask_rel RS guaranteesD) 1);
+by (rotate_tac 2 3);
+by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
+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", "lift(giv)"), ("a", "s`giv")] Increasing_imp_Stable 1);
+by (Asm_simp_tac 1);
+by (eres_inst_tac [("f", "lift(ask)"), ("a", "s`ask")] Increasing_imp_Stable 1);
+by (Asm_simp_tac 1);
+by (eres_inst_tac [("f", "lift(rel)"), ("a", "s`rel")] Increasing_imp_Stable 1);
+by (Asm_simp_tac 1);
+by (etac client_prog_Join_Stable_rel_le_giv 1);
+by (Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 2);
+by (blast_tac (claset() addIs [sym, strict_prefix_is_prefix RS iffD2,
+ prefix_trans, prefix_imp_pfixGe,
+ pfixGe_trans]) 2);
+by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD1 RS conjunct1,
+ prefix_trans], simpset()));
+qed "induct_lemma";
+
+Goal
+"[| client_prog Join G : Incr(lift(giv)); client_prog ok G; G:program |] \
+\ ==> client_prog Join G : \
+\ {s:state. <s`rel, h>:strict_prefix(nat) \
+\ & <h, s`giv>:prefix(nat) & h pfixGe s`ask} \
+\ LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
+by (res_inst_tac [("f", "lam x:state. length(h) #- length(x`rel)")]
+ 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 (resolve_tac [imageI] 3);
+by (resolve_tac [converseI] 3);
+by (asm_simp_tac (simpset() addsimps [lam_def]) 3);
+by (asm_simp_tac (simpset() addsimps [length_type]) 3);
+by (etac swap 2);
+by (resolve_tac [imageI] 2);
+by (resolve_tac [converseI] 2);
+by (asm_full_simp_tac (simpset() addsimps [lam_def]) 2);
+by (REPEAT (dtac strict_prefix_length_lt 2));
+by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 2);
+by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
+by (dtac less_imp_succ_add 2);
+by (dtac less_imp_succ_add 3);
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(Asm_simp_tac));
+by (etac (diff_le_self RS ltD) 2);
+by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 1);
+by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2]
+ addDs [rotate_prems 2 common_prefix_linear,
+ prefix_type RS subsetD], simpset()));
+qed "rel_progress_lemma";
+
+Goal
+"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] ==> \
+\ client_prog Join G : \
+\ {s:state. <h, s`giv>:prefix(nat) & h pfixGe s`ask} \
+\ LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
+by (rtac (client_prog_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 (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2]
+ addDs [rotate_prems 3 common_prefix_linear,
+ prefix_type RS subsetD], simpset()));
+by (rotate_tac ~1 1);
+by (force_tac (claset(), simpset() addsimps [client_prog_ok_iff]) 1);
+qed "progress_lemma";
+
+(*Progress property: all tokens that are given will be released*)
+Goal
+"client_prog: Incr(lift(giv)) guarantees \
+\ (INT h:list(nat). {s:state. <h, s`giv>:prefix(nat) &\
+\ h pfixGe s`ask} LeadsTo {s:state. <h, s`rel>:prefix(nat)})";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [progress_lemma]) 1);
+by Auto_tac;
+qed "client_prog_progress";
+
+Goal "Allowed(client_prog) = \
+\ preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))";
+by (cut_facts_tac [inst "v" "lift(ask)" preserves_type] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def,
+ client_prog_def RS def_prg_Allowed,
+ cons_Int_distrib, safety_prop_Acts_iff]));
+qed "client_prog_Allowed";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/ClientImpl.thy Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,63 @@
+(* Title: ZF/UNITY/ClientImpl.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+Distributed Resource Management System: Client Implementation
+*)
+
+
+ClientImpl = AllocBase + Guar +
+consts
+ ask :: i (* input history: tokens requested *)
+ giv :: i (* output history: tokens granted *)
+ rel :: i (* input history: tokens released *)
+ tok :: i (* the number of available tokens *)
+
+translations
+ "ask" == "Var(Nil)"
+ "giv" == "Var([0])"
+ "rel" == "Var([1])"
+ "tok" == "Var([2])"
+
+rules
+ type_assumes
+ "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) &
+ type_of(rel) = list(tokbag) & type_of(tok) = nat"
+ default_val_assumes
+ "default_val(ask) = Nil & default_val(giv) = Nil &
+ default_val(rel) = Nil & default_val(tok) = 0"
+
+
+(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
+
+constdefs
+ (** Release some client_tokens **)
+
+ client_rel_act ::i
+ "client_rel_act ==
+ {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel)
+ & t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
+ nrel < length(s`giv) &
+ nth(nrel, s`ask) le nth(nrel, s`giv)}"
+
+ (** Choose a new token requirement **)
+ (** Including s'=s suppresses fairness, allowing the non-trivial part
+ of the action to be ignored **)
+
+ client_tok_act :: i
+ "client_tok_act == {<s,t>:state*state. t=s |
+ (t = s(tok:=succ(s`tok mod NbT)))}"
+
+ client_ask_act :: i
+ "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
+
+ client_prog :: i
+ "client_prog ==
+ mk_program({s:state. s`tok le NbT & s`giv = Nil &
+ s`ask = Nil & s`rel = Nil},
+ {client_rel_act, client_tok_act, client_ask_act},
+ UN G: preserves(lift(rel)) Int
+ preserves(lift(ask)) Int
+ preserves(lift(tok)). Acts(G))"
+end
\ No newline at end of file
--- a/src/ZF/UNITY/Distributor.ML Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/Distributor.ML Thu May 29 17:10:00 2003 +0200
@@ -74,7 +74,7 @@
by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1);
by (auto_tac (claset() addSIs [guaranteesI] addIs [Follows_imp_Increasing_left]
addSDs [guaranteesD],
- simpset() addsimps []));
+ simpset()));
qed "distr_Increasing_Out";
val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
@@ -116,13 +116,6 @@
by (blast_tac (claset() addIs [lt_trans]) 1);
qed "distr_bag_Follows_lemma";
-
-val prems =
-Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')";
-by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
-qed "Follows_cong";
-(*????????????????*)
-
Goal
"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
\ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
@@ -150,8 +143,8 @@
by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 5);
by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 6);
by (Clarify_tac 4);
-by (asm_full_simp_tac (simpset() addsimps []) 3);
-by (asm_full_simp_tac (simpset() addsimps []) 3);
+by (Asm_full_simp_tac 3);
+by (Asm_full_simp_tac 3);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [nat_into_Finite])));
by (rotate_tac 2 1);
by (asm_full_simp_tac (simpset() addsimps [D_ok_iff]) 1);
@@ -159,8 +152,8 @@
simpset() addsimps [distr_spec_def, distr_follows_def]));
by (dtac guaranteesD 1);
by (assume_tac 1);
-by (force_tac (claset(), simpset() addsimps []) 1);
-by (force_tac (claset(), simpset() addsimps []) 1);
+by (Force_tac 1);
+by (Force_tac 1);
by (asm_full_simp_tac
(simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD),
refl_prefix, trans_on_MultLe]
--- a/src/ZF/UNITY/Follows.ML Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/Follows.ML Thu May 29 17:10:00 2003 +0200
@@ -8,6 +8,10 @@
(*Does this hold for "invariant"?*)
+val prems =
+Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')";
+by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
+qed "Follows_cong";
Goalw [mono1_def, comp_def]
"[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Merge.ML Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,163 @@
+(* Title: ZF/UNITY/Merge
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+A multiple-client allocator from a single-client allocator:
+Merge specification
+*)
+Open_locale "Merge";
+val all_distinct_vars = thm "all_distinct_vars";
+val var_assumes = thm "var_assumes";
+val type_assumes = thm "type_assumes";
+val default_val_assumes = thm "default_val_assumes";
+
+Addsimps [var_assumes, default_val_assumes, type_assumes];
+
+Goalw [state_def]
+"s:state ==> s`In(n):list(A)";
+by (dres_inst_tac [("a", "In(n)")] apply_type 1);
+by Auto_tac;
+qed "In_value_type";
+AddTCs [In_value_type];
+Addsimps [In_value_type];
+
+Goalw [state_def]
+"s:state ==> s`Out:list(A)";
+by (dres_inst_tac [("a", "Out")] apply_type 1);
+by Auto_tac;
+qed "Out_value_type";
+AddTCs [Out_value_type];
+Addsimps [Out_value_type];
+
+Goalw [state_def]
+"s:state ==> s`iOut:list(nat)";
+by (dres_inst_tac [("a", "iOut")] apply_type 1);
+by Auto_tac;
+qed "Out_value_type";
+AddTCs [Out_value_type];
+Addsimps [Out_value_type];
+
+
+val merge = thm "merge_spec";
+
+Goal "M:program";
+by (cut_facts_tac [merge] 1);
+by (auto_tac (claset() addDs [guarantees_type RS subsetD],
+ simpset() addsimps [merge_spec_def, merge_increasing_def]));
+qed "M_in_program";
+Addsimps [M_in_program];
+AddTCs [M_in_program];
+
+Goal
+"Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))";
+by (cut_facts_tac [merge, inst "v" "lift(Out)" preserves_type] 1);
+by (auto_tac (claset(), simpset() addsimps
+ [merge_spec_def, merge_allowed_acts_def,
+ Allowed_def, safety_prop_Acts_iff]));
+qed "merge_Allowed";
+
+Goal
+"G:program ==> \
+\ M ok G <-> (G:preserves(lift(Out)) & \
+\ G:preserves(lift(iOut)) & M:Allowed(G))";
+by (cut_facts_tac [merge] 1);
+by (auto_tac (claset(), simpset()
+ addsimps [merge_Allowed, ok_iff_Allowed]));
+qed "M_ok_iff";
+
+Goal
+"[| G:preserves(lift(Out)); G:preserves(lift(iOut)); \
+\ M:Allowed(G) |] ==> \
+\ M Join G:Always({s:state. length(s`Out)=length(s`iOut)})";
+by (ftac (preserves_type RS subsetD) 1);
+by (subgoal_tac "G:program" 1);
+by (assume_tac 2);
+by (ftac M_ok_iff 1);
+by (cut_facts_tac [merge] 1);
+by (force_tac (claset() addDs [guaranteesD],
+ simpset() addsimps [merge_spec_def, merge_eq_Out_def]) 1);
+qed "merge_Always_Out_eq_iOut";
+
+Goal
+"[| G:preserves(lift(iOut)); G:preserves(lift(Out)); \
+\ M:Allowed(G) |] ==> \
+\ M Join G: Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})";
+by (ftac (preserves_type RS subsetD) 1);
+by (ftac M_ok_iff 1);
+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(lift(iOut)); \
+\ G: preserves(lift(Out)); M:Allowed(G) |] \
+\ ==> M Join G : Always \
+\ ({s:state. msetsum(%i. bag_of(sublist(s`Out, \
+\ {k:nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
+\ Nclients, A) = bag_of(s`Out)})";
+by (rtac ([[merge_Always_Out_eq_iOut, merge_Bounded] MRS Always_Int_I,
+ state_AlwaysI RS Always_weaken] MRS (Always_Diff_Un_eq RS iffD1)) 1)
+;
+by Auto_tac;
+by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
+by (auto_tac (claset(), simpset()
+ addsimps [nat_into_Finite, set_of_list_conv_nth]));
+by (subgoal_tac
+ "(UN i:Nclients. {k:nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
+by Auto_tac;
+by (resolve_tac [equalityI] 1);
+by (blast_tac (claset() addDs [ltD]) 1);
+by (Clarify_tac 1);
+by (subgoal_tac "length(x ` iOut) : nat" 1);
+by Typecheck_tac;
+by (subgoal_tac "xa : nat" 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt])));
+by (blast_tac (claset() addIs [lt_trans]) 2);
+by (dres_inst_tac [("x", "nth(xa, x`iOut)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec 1);
+by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1);
+by (blast_tac (claset() addDs [ltD]) 1);
+qed "merge_bag_Follows_lemma";
+
+Goal
+"M : (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
+\ guarantees \
+\ (%s. bag_of(s`Out)) Fols \
+\ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)";
+by (cut_facts_tac [merge] 1);
+by (rtac (merge_bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
+by (ALLGOALS(rotate_tac ~1 ));
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [M_ok_iff])));
+by Auto_tac;
+by (rtac Follows_state_ofD1 1);
+by (rtac Follows_msetsum_UN 1);
+by (ALLGOALS(Clarify_tac));
+by (resolve_tac [conjI] 2);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 2);
+by (resolve_tac [conjI] 3);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 3);
+by (resolve_tac [conjI] 4);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 4);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 5);
+by (ALLGOALS(Asm_simp_tac));
+by (resolve_tac [nat_into_Finite] 2);
+by (Asm_simp_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff,
+ merge_spec_def, merge_follows_def]) 1);
+by Auto_tac;
+by (cut_facts_tac [merge] 1);
+by (subgoal_tac "M ok G" 1);
+by (dtac guaranteesD 1);
+by (assume_tac 1);
+by (force_tac (claset() addIs[M_ok_iff RS iffD2], simpset()) 4);
+by (rewrite_goal_tac [merge_spec_def, merge_follows_def] 1);
+by (Blast_tac 1);
+by (Asm_simp_tac 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD),
+ refl_prefix, trans_on_MultLe]
+ addcongs [Follows_cong]) 1);
+qed "merge_bag_Follows";
+Close_locale "Merge";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Merge.thy Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,78 @@
+(* Title: ZF/UNITY/Merge
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+A multiple-client allocator from a single-client allocator:
+Merge specification
+*)
+
+Merge = AllocBase + Follows + Guar + GenPrefix +
+(** Merge specification (the number of inputs is Nclients) ***)
+(** Parameter A represents the type of items to Merge **)
+constdefs
+ (*spec (10)*)
+ merge_increasing :: [i, i, i] =>i
+ "merge_increasing(A, Out, iOut) == program guarantees
+ (lift(Out) IncreasingWrt prefix(A)/list(A)) Int
+ (lift(iOut) IncreasingWrt prefix(nat)/list(nat))"
+
+ (*spec (11)*)
+ merge_eq_Out :: [i, i] =>i
+ "merge_eq_Out(Out, iOut) == program guarantees
+ Always({s:state. length(s`Out) = length(s`iOut)})"
+
+ (*spec (12)*)
+ merge_bounded :: i=>i
+ "merge_bounded(iOut) == program guarantees
+ Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})"
+
+ (*spec (13)*)
+ (* Parameter A represents the type of tokens *)
+ merge_follows :: [i, i=>i, i, i] =>i
+ "merge_follows(A, In, Out, iOut) ==
+ (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
+ guarantees
+ (INT n:Nclients.
+ (%s. sublist(s`Out, {k:nat. k < length(s`iOut) &
+ nth(k, s`iOut) = n})) Fols lift(In(n))
+ Wrt prefix(A)/list(A))"
+
+ (*spec: preserves part*)
+ merge_preserves :: [i=>i] =>i
+ "merge_preserves(In) == INT n:nat. preserves(lift(In(n)))"
+
+(* environmental constraints*)
+ merge_allowed_acts :: [i, i] =>i
+ "merge_allowed_acts(Out, iOut) ==
+ {F:program. AllowedActs(F) =
+ cons(id(state), (UN G:preserves(lift(Out)) Int
+ preserves(lift(iOut)). Acts(G)))}"
+
+ merge_spec :: [i, i =>i, i, i]=>i
+ "merge_spec(A, In, Out, iOut) ==
+ merge_increasing(A, Out, iOut) Int merge_eq_Out(Out, iOut) Int
+ merge_bounded(iOut) Int merge_follows(A, In, Out, iOut)
+ Int merge_allowed_acts(Out, iOut) Int merge_preserves(In)"
+
+(** State definitions. OUTPUT variables are locals **)
+locale Merge =
+ fixes In :: i=>i (*merge's INPUT histories: streams to merge*)
+ Out :: i (*merge's OUTPUT history: merged items*)
+ iOut :: i (*merge's OUTPUT history: origins of merged items*)
+ A :: i (*the type of items being merged *)
+ M :: i
+ assumes
+ var_assumes "(ALL n. In(n):var) & Out:var & iOut:var"
+ all_distinct_vars "ALL n. all_distinct([In(n), Out, iOut])"
+ type_assumes "(ALL n. type_of(In(n))=list(A))&
+ type_of(Out)=list(A) &
+ type_of(iOut)=list(nat)"
+ default_val_assumes "(ALL n. default_val(In(n))=Nil) &
+ default_val(Out)=Nil &
+ default_val(iOut)=Nil"
+
+ merge_spec "M:merge_spec(A, In, Out, iOut)"
+end
+
+
\ No newline at end of file
--- a/src/ZF/UNITY/ROOT.ML Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/ROOT.ML Thu May 29 17:10:00 2003 +0200
@@ -18,4 +18,5 @@
time_use_thy "GenPrefix";
time_use_thy "Distributor";
-
+time_use_thy "Merge";
+time_use_thy "ClientImpl";
--- a/src/ZF/UNITY/WFair.ML Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/WFair.ML Thu May 29 17:10:00 2003 +0200
@@ -544,7 +544,7 @@
by (auto_tac (claset(), simpset() addsimps [measure_def]));
by (blast_tac (claset() addIs [ltD]) 1);
by (rtac vimageI 1);
-by (blast_tac (claset() addIs []) 2);
+by (Blast_tac 2);
by (asm_full_simp_tac (simpset() addsimps [lt_Ord, lt_Ord2, Ord_mem_iff_lt]) 1);
by (blast_tac (claset() addIs [lt_trans]) 1);
qed "Image_inverse_lessThan";