--- a/src/ZF/IsaMakefile Fri Jun 20 12:10:45 2003 +0200
+++ b/src/ZF/IsaMakefile Fri Jun 20 18:13:16 2003 +0200
@@ -121,7 +121,7 @@
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/AllocImpl.thy\
- UNITY/ClientImpl.ML UNITY/ClientImpl.thy\
+ UNITY/ClientImpl.thy\
UNITY/Distributor.ML UNITY/Distributor.thy\
UNITY/Follows.ML UNITY/Follows.thy\
UNITY/Increasing.ML UNITY/Increasing.thy\
--- a/src/ZF/UNITY/AllocImpl.thy Fri Jun 20 12:10:45 2003 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Fri Jun 20 18:13:16 2003 +0200
@@ -9,15 +9,20 @@
(*LOCALE NEEDED FOR PROOF OF GUARANTEES THEOREM*)
-theory AllocImpl = ClientImpl:
+(*????FIXME: sort out this mess
+FoldSet.cons_Int_right_lemma1:
+ ?x \<in> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = cons(?x, ?C \<inter> ?D)
+FoldSet.cons_Int_right_lemma2: ?x \<notin> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = ?C \<inter> ?D
+Multiset.cons_Int_right_cases:
+ cons(?x, ?A) \<inter> ?B = (if ?x \<in> ?B then cons(?x, ?A \<inter> ?B) else ?A \<inter> ?B)
+UNITYMisc.Int_cons_right:
+ ?A \<inter> cons(?a, ?B) = (if ?a \<in> ?A then cons(?a, ?A \<inter> ?B) else ?A \<inter> ?B)
+UNITYMisc.Int_succ_right:
+ ?A \<inter> succ(?k) = (if ?k \<in> ?A then cons(?k, ?A \<inter> ?k) else ?A \<inter> ?k)
+*)
-(*????MOVE UP*)
-method_setup constrains = {*
- Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- gen_constrains_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
- "for proving safety properties"
+
+theory AllocImpl = ClientImpl:
consts
@@ -62,21 +67,6 @@
preserves(lift(giv)). Acts(G))"
-
-
-(*????FIXME: sort out this mess
-FoldSet.cons_Int_right_lemma1:
- ?x \<in> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = cons(?x, ?C \<inter> ?D)
-FoldSet.cons_Int_right_lemma2: ?x \<notin> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = ?C \<inter> ?D
-Multiset.cons_Int_right_cases:
- cons(?x, ?A) \<inter> ?B = (if ?x \<in> ?B then cons(?x, ?A \<inter> ?B) else ?A \<inter> ?B)
-UNITYMisc.Int_cons_right:
- ?A \<inter> cons(?a, ?B) = (if ?a \<in> ?A then cons(?a, ?A \<inter> ?B) else ?A \<inter> ?B)
-UNITYMisc.Int_succ_right:
- ?A \<inter> succ(?k) = (if ?k \<in> ?A then cons(?k, ?A \<inter> ?k) else ?A \<inter> ?k)
-*)
-
-
declare alloc_type_assumes [simp] alloc_default_val_assumes [simp]
lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
@@ -591,14 +581,6 @@
apply auto
done
-(*For using "disjunction" (union over an index set) to eliminate a variable.
- ????move way up*)
-lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
- ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
-apply blast
-done
-
-
(*Fifth step in proof of (31): from the fourth step, taking the union over all
k\<in>nat *)
lemma alloc_prog_LeadsTo_length_giv_disj3:
--- a/src/ZF/UNITY/ClientImpl.ML Fri Jun 20 12:10:45 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,309 +0,0 @@
-(* 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 \\<in> state ==> s`ask \\<in> 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 \\<in> state ==> s`giv \\<in> 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 \\<in> state ==> s`rel \\<in> 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 \\<in> state ==> s`tok \\<in> 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 \\<in> 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 "\\<forall>G \\<in> program. (client_prog ok G) <-> \
-\ (G \\<in> preserves(lift(rel)) & G \\<in> preserves(lift(ask)) & \
-\ G \\<in> preserves(lift(tok)) & client_prog \\<in> 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:(\\<Inter>x \\<in> 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 \\<in> program |]\
-\ ==> client_prog Join G : \
-\ Always({s \\<in> state. s`tok le NbT} Int \
-\ {s \\<in> state. \\<forall>elt \\<in> 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 \\<in> program guarantees \
-\ Always({s \\<in> state. \\<forall>elt \\<in> 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 \\<in> stable({s \\<in> 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 \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \
-\ ==> client_prog Join G \\<in> Stable({s \\<in> 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 \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \
-\ ==> client_prog Join G \\<in> Always({s \\<in> 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 \\<in> 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 \\<in> \
-\ transient({s \\<in> 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 \\<in> 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)")] spec 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 \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \
-\ ==> client_prog Join G \\<in> \
-\ {s \\<in> state. s`rel = k & <k,h>:strict_prefix(nat) \
-\ & <h , s`giv>:prefix(nat) & h pfixGe s`ask} \
-\ LeadsTo {s \\<in> 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 \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \
-\ ==> client_prog Join G \\<in> \
-\ {s \\<in> state. <s`rel, h>:strict_prefix(nat) \
-\ & <h, s`giv>:prefix(nat) & h pfixGe s`ask} \
-\ LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)}";
-by (res_inst_tac [("f", "\\<lambda>x \\<in> 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 \\<in> 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 \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] ==> \
-\ client_prog Join G \\<in> \
-\ {s \\<in> state. <h, s`giv>:prefix(nat) & h pfixGe s`ask} \
-\ LeadsTo {s \\<in> 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 \\<in> Incr(lift(giv)) guarantees \
-\ (\\<Inter>h \\<in> list(nat). {s \\<in> state. <h, s`giv>:prefix(nat) &\
-\ h pfixGe s`ask} LeadsTo {s \\<in> 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";
-
--- a/src/ZF/UNITY/ClientImpl.thy Fri Jun 20 12:10:45 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Fri Jun 20 18:13:16 2003 +0200
@@ -7,7 +7,7 @@
*)
-ClientImpl = AllocBase + Guar +
+theory ClientImpl = AllocBase + Guar:
consts
ask :: i (* input history: tokens requested *)
giv :: i (* output history: tokens granted *)
@@ -20,11 +20,11 @@
"rel" == "Var([1])"
"tok" == "Var([2])"
-rules
- type_assumes
+axioms
+ 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_assumes:
"default_val(ask) = Nil & default_val(giv) = Nil &
default_val(rel) = Nil & default_val(tok) = 0"
@@ -36,29 +36,299 @@
client_rel_act ::i
"client_rel_act ==
- {<s,t> \\<in> state*state.
- \\<exists>nrel \\<in> nat. nrel = length(s`rel) &
+ {<s,t> \<in> state*state.
+ \<exists>nrel \<in> 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)}"
+ nth(nrel, s`ask) \<le> nth(nrel, s`giv)}"
(** Choose a new token requirement **)
(** Including t=s suppresses fairness, allowing the non-trivial part
of the action to be ignored **)
client_tok_act :: i
- "client_tok_act == {<s,t> \\<in> state*state. t=s |
+ "client_tok_act == {<s,t> \<in> state*state. t=s |
t = s(tok:=succ(s`tok mod NbT))}"
client_ask_act :: i
- "client_ask_act == {<s,t> \\<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
+ "client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
client_prog :: i
"client_prog ==
- mk_program({s \\<in> state. s`tok le NbT & s`giv = Nil &
+ mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil &
s`ask = Nil & s`rel = Nil},
{client_rel_act, client_tok_act, client_ask_act},
- \\<Union>G \\<in> preserves(lift(rel)) Int
+ \<Union>G \<in> preserves(lift(rel)) Int
preserves(lift(ask)) Int
preserves(lift(tok)). Acts(G))"
+
+
+declare type_assumes [simp] default_val_assumes [simp]
+(* This part should be automated *)
+
+(*????MOVE UP*)
+method_setup constrains = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_constrains_tac (Classical.get_local_claset ctxt,
+ Simplifier.get_local_simpset ctxt) 1)) *}
+ "for proving safety properties"
+
+(*For using "disjunction" (union over an index set) to eliminate a variable.
+ ????move way up*)
+lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
+ ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
+by blast
+
+lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)"
+apply (unfold state_def)
+apply (drule_tac a = ask in apply_type, auto)
+done
+
+lemma giv_value_type [simp,TC]: "s \<in> state ==> s`giv \<in> list(nat)"
+apply (unfold state_def)
+apply (drule_tac a = giv in apply_type, auto)
+done
+
+lemma rel_value_type [simp,TC]: "s \<in> state ==> s`rel \<in> list(nat)"
+apply (unfold state_def)
+apply (drule_tac a = rel in apply_type, auto)
+done
+
+lemma tok_value_type [simp,TC]: "s \<in> state ==> s`tok \<in> nat"
+apply (unfold state_def)
+apply (drule_tac a = tok in apply_type, auto)
+done
+
+(** The Client Program **)
+
+lemma client_type [simp,TC]: "client_prog \<in> program"
+apply (unfold client_prog_def)
+apply (simp (no_asm))
+done
+
+declare client_prog_def [THEN def_prg_Init, simp]
+declare client_prog_def [THEN def_prg_AllowedActs, simp]
+ML
+{*
+program_defs_ref := [thm"client_prog_def"]
+*}
+
+declare client_rel_act_def [THEN def_act_simp, simp]
+declare client_tok_act_def [THEN def_act_simp, simp]
+declare client_ask_act_def [THEN def_act_simp, simp]
+
+lemma client_prog_ok_iff:
+ "\<forall>G \<in> program. (client_prog ok G) <->
+ (G \<in> preserves(lift(rel)) & G \<in> preserves(lift(ask)) &
+ G \<in> preserves(lift(tok)) & client_prog \<in> Allowed(G))"
+by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed])
+
+lemma client_prog_preserves:
+ "client_prog:(\<Inter>x \<in> var-{ask, rel, tok}. preserves(lift(x)))"
+apply (rule Inter_var_DiffI, force)
+apply (rule ballI)
+apply (rule preservesI, constrains, auto)
+done
+
+
+lemma preserves_lift_imp_stable:
+ "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})";
+apply (drule preserves_imp_stable)
+apply (simp add: lift_def)
+done
+
+lemma preserves_imp_prefix:
+ "G \<in> preserves(lift(ff))
+ ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})";
+by (erule preserves_lift_imp_stable)
+
+(*Safety property 1: ask, rel are increasing: (24) *)
+lemma client_prog_Increasing_ask_rel:
+"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))"
+apply (unfold guar_def)
+apply (auto intro!: increasing_imp_Increasing
+ simp add: client_prog_ok_iff increasing_def preserves_imp_prefix)
+apply (constrains, force, force)+
+done
+
+declare nth_append [simp] append_one_prefix [simp]
+
+lemma NbT_pos2: "0<NbT"
+apply (cut_tac NbT_pos)
+apply (rule Ord_0_lt, auto)
+done
+
+(*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_prog ok G; G \<in> program |]
+ ==> client_prog Join G \<in>
+ Always({s \<in> state. s`tok \<le> NbT} Int
+ {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
+apply (rotate_tac -1)
+apply (auto simp add: client_prog_ok_iff)
+apply (rule invariantI [THEN stable_Join_Always2], force)
+ prefer 2
+ apply (fast intro: stable_Int preserves_lift_imp_stable, constrains)
+apply (auto dest: ActsD)
+apply (cut_tac NbT_pos)
+apply (rule NbT_pos2 [THEN mod_less_divisor])
+apply (auto dest: ActsD preserves_imp_eq simp add: set_of_list_append)
+done
+
+(* Export version, with no mention of tok in the postcondition, but
+ unfortunately tok must be declared local.*)
+lemma client_prog_ask_Bounded:
+ "client_prog \<in> program guarantees
+ Always({s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
+apply (rule guaranteesI)
+apply (erule ask_Bounded_lemma [THEN Always_weaken], auto)
+done
+
+(*** Towards proving the liveness property ***)
+
+lemma client_prog_stable_rel_le_giv:
+ "client_prog \<in> stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+by (constrains, auto)
+
+lemma client_prog_Join_Stable_rel_le_giv:
+"[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
+ ==> client_prog Join G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
+apply (auto simp add: lift_def)
+done
+
+lemma client_prog_Join_Always_rel_le_giv:
+ "[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
+ ==> client_prog Join G \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
+
+lemma def_act_eq:
+ "A == {<s, t> \<in> state*state. P(s, t)} ==> A={<s, t> \<in> state*state. P(s, t)}"
+by auto
+
+lemma act_subset: "A={<s,t> \<in> state*state. P(s, t)} ==> A<=state*state"
+by auto
+
+lemma transient_lemma:
+"client_prog \<in>
+ transient({s \<in> state. s`rel = k & <k, h> \<in> strict_prefix(nat)
+ & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask})"
+apply (rule_tac act = client_rel_act in transientI)
+apply (simp (no_asm) add: client_prog_def [THEN def_prg_Acts])
+apply (simp (no_asm) add: client_rel_act_def [THEN def_act_eq, THEN act_subset])
+apply (auto simp add: client_prog_def [THEN def_prg_Acts] domain_def)
+apply (rule ReplaceI)
+apply (rule_tac x = "x (rel:= x`rel @ [nth (length (x`rel), x`giv) ]) " in exI)
+apply (auto intro!: state_update_type app_type length_type nth_type, auto)
+apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
+apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
+apply (simp (no_asm_use) add: gen_prefix_iff_nth)
+apply (subgoal_tac "h \<in> list(nat)")
+ apply (simp_all (no_asm_simp) add: prefix_type [THEN subsetD, THEN SigmaD1])
+apply (auto simp add: prefix_def Ge_def)
+apply (drule strict_prefix_length_lt)
+apply (drule_tac x = "length (x`rel) " in spec)
+apply auto
+apply (simp (no_asm_use) add: gen_prefix_iff_nth)
+apply (auto simp add: id_def lam_def)
+done
+
+lemma strict_prefix_is_prefix:
+ "<xs, ys> \<in> strict_prefix(A) <-> <xs, ys> \<in> prefix(A) & xs\<noteq>ys"
+apply (unfold strict_prefix_def id_def lam_def)
+apply (auto dest: prefix_type [THEN subsetD])
+done
+
+lemma induct_lemma:
+"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
+ ==> client_prog Join G \<in>
+ {s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat)
+ & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
+ LeadsTo {s \<in> state. <k, s`rel> \<in> strict_prefix(nat)
+ & <s`rel, s`giv> \<in> prefix(nat) &
+ <h, s`giv> \<in> prefix(nat) &
+ h pfixGe s`ask}"
+apply (rule single_LeadsTo_I)
+ prefer 2 apply simp
+apply (frule client_prog_Increasing_ask_rel [THEN guaranteesD])
+apply (rotate_tac [3] 2)
+apply (auto simp add: client_prog_ok_iff)
+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 = "lift (giv) " and a = "s`giv" in Increasing_imp_Stable)
+apply (simp (no_asm_simp))
+apply (erule_tac f = "lift (ask) " and a = "s`ask" in Increasing_imp_Stable)
+apply (simp (no_asm_simp))
+apply (erule_tac f = "lift (rel) " and a = "s`rel" in Increasing_imp_Stable)
+apply (simp (no_asm_simp))
+apply (erule client_prog_Join_Stable_rel_le_giv, blast, simp_all)
+ prefer 2
+ apply (blast intro: sym strict_prefix_is_prefix [THEN iffD2] prefix_trans prefix_imp_pfixGe pfixGe_trans)
+apply (auto intro: strict_prefix_is_prefix [THEN iffD1, THEN conjunct1]
+ prefix_trans)
+done
+
+lemma rel_progress_lemma:
+"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
+ ==> client_prog Join G \<in>
+ {s \<in> state. <s`rel, h> \<in> strict_prefix(nat)
+ & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
+ LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
+apply (rule_tac f = "\<lambda>x \<in> state. length(h) #- length(x`rel)"
+ in LessThan_induct)
+apply (auto simp add: vimage_def)
+ prefer 2 apply (force simp add: lam_def)
+apply (rule single_LeadsTo_I)
+ prefer 2 apply simp
+apply (subgoal_tac "h \<in> list(nat)")
+ prefer 2 apply (blast dest: prefix_type [THEN subsetD])
+apply (rule induct_lemma [THEN LeadsTo_weaken])
+ apply (simp add: length_type lam_def)
+apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
+ dest: common_prefix_linear prefix_type [THEN subsetD])
+apply (erule swap)
+apply (rule imageI)
+ apply (force dest!: simp add: lam_def)
+apply (simp add: length_type lam_def, clarify)
+apply (drule strict_prefix_length_lt)+
+apply (drule less_imp_succ_add, simp)+
+apply clarify
+apply simp
+apply (erule diff_le_self [THEN ltD])
+done
+
+lemma progress_lemma:
+"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
+ ==> client_prog Join G \<in>
+ {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
+ LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
+apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], assumption)
+apply (force simp add: client_prog_ok_iff)
+apply (rule LeadsTo_weaken_L)
+apply (rule LeadsTo_Un [OF rel_progress_lemma
+ subset_refl [THEN subset_imp_LeadsTo]])
+apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
+ dest: common_prefix_linear prefix_type [THEN subsetD])
+done
+
+(*Progress property: all tokens that are given will be released*)
+lemma client_prog_progress:
+"client_prog \<in> Incr(lift(giv)) guarantees
+ (\<Inter>h \<in> list(nat). {s \<in> state. <h, s`giv> \<in> prefix(nat) &
+ h pfixGe s`ask} LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)})"
+apply (rule guaranteesI)
+apply (blast intro: progress_lemma, auto)
+done
+
+lemma client_prog_Allowed:
+ "Allowed(client_prog) =
+ preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))"
+apply (cut_tac v = "lift (ask)" in preserves_type)
+apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
+ cons_Int_distrib safety_prop_Acts_iff)
+done
+
end
\ No newline at end of file
--- a/src/ZF/UNITY/GenPrefix.ML Fri Jun 20 12:10:45 2003 +0200
+++ b/src/ZF/UNITY/GenPrefix.ML Fri Jun 20 18:13:16 2003 +0200
@@ -523,7 +523,13 @@
\ --><xs,ys> \\<in> prefix(A) | <ys,xs> \\<in> prefix(A)";
by (etac list_append_induct 1);
by Auto_tac;
-qed_spec_mp "common_prefix_linear";
+qed_spec_mp "common_prefix_linear_lemma";
+
+Goal "[|<xs, zs> \\<in> prefix(A); <ys,zs> \\<in> prefix(A) |] \
+\ ==> <xs,ys> \\<in> prefix(A) | <ys,xs> \\<in> prefix(A)";
+by (cut_facts_tac [prefix_type] 1);
+by (blast_tac (claset() delrules [disjCI] addIs [common_prefix_linear_lemma]) 1);
+qed "common_prefix_linear";
(*** pfixLe, pfixGe: properties inherited from the translations ***)