Conversion of UNITY/Distributor to Isar script. General tidy-up.
--- a/src/ZF/IsaMakefile Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/IsaMakefile Wed Jun 25 13:17:26 2003 +0200
@@ -121,8 +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.thy\
- UNITY/Distributor.ML UNITY/Distributor.thy\
+ UNITY/ClientImpl.thy UNITY/Distributor.thy\
UNITY/Follows.ML UNITY/Follows.thy\
UNITY/Increasing.ML UNITY/Increasing.thy\
UNITY/Merge.ML UNITY/Merge.thy\
--- a/src/ZF/UNITY/AllocImpl.thy Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Wed Jun 25 13:17:26 2003 +0200
@@ -28,7 +28,7 @@
constdefs
alloc_giv_act :: i
"alloc_giv_act ==
- {<s, t> : state*state.
+ {<s, t> \<in> state*state.
\<exists>k. k = length(s`giv) &
t = s(giv := s`giv @ [nth(k, s`ask)],
available_tok := s`available_tok #- nth(k, s`ask)) &
@@ -36,13 +36,13 @@
alloc_rel_act :: i
"alloc_rel_act ==
- {<s, t> : state*state.
+ {<s, t> \<in> state*state.
t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
NbR := succ(s`NbR)) &
s`NbR < length(s`rel)}"
(*The initial condition s`giv=[] is missing from the
- original definition -- S. O. Ehmety *)
+ original definition: S. O. Ehmety *)
alloc_prog :: i
"alloc_prog ==
mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
@@ -146,8 +146,8 @@
done
lemma giv_Bounded_lemma2:
-"[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
- ==> alloc_prog Join G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
+"[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
+ ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
{s\<in>state. s`available_tok #+ tokens(s`giv) =
NbT #+ tokens(take(s`NbR, s`rel))})"
apply (cut_tac giv_Bounded_lamma1)
@@ -203,11 +203,11 @@
asked for*)
lemma alloc_prog_ask_prefix_giv:
"alloc_prog \<in> Incr(lift(ask)) guarantees
- Always({s\<in>state. <s`giv, s`ask>:prefix(tokbag)})"
+ Always({s\<in>state. <s`giv, s`ask> \<in> prefix(tokbag)})"
apply (auto intro!: AlwaysI simp add: guar_def)
apply (subgoal_tac "G \<in> preserves (lift (giv))")
prefer 2 apply (simp add: alloc_prog_ok_iff)
-apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
+apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)"
in stable_Join_Stable)
apply constrains
prefer 2 apply (simp add: lift_def, clarify)
@@ -220,7 +220,7 @@
lemma alloc_prog_transient_lemma:
"[|G \<in> program; k\<in>nat|]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
transient({s\<in>state. k \<le> length(s`rel)} \<inter>
{s\<in>state. succ(s`NbR) = k})"
apply auto
@@ -238,7 +238,7 @@
lemma alloc_prog_rel_Stable_NbR_lemma:
"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
- ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
+ ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto)
apply (blast intro: le_trans leI)
apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
@@ -250,11 +250,11 @@
lemma alloc_prog_NbR_LeadsTo_lemma:
"[| G \<in> program; alloc_prog ok G;
- alloc_prog Join G \<in> Incr(lift(rel)); k\<in>nat |]
- ==> alloc_prog Join G \<in>
+ alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat |]
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
LeadsTo {s\<in>state. k \<le> s`NbR}"
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
apply (rule_tac [2] mono_length)
prefer 3 apply simp
@@ -269,9 +269,9 @@
done
lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
- "[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
+ "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
k\<in>nat; n \<in> nat; n < k |]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
(\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
@@ -279,7 +279,7 @@
apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
in LeadsTo_weaken_R)
apply safe
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
apply (rule_tac [2] mono_length)
prefer 3 apply simp
@@ -301,9 +301,9 @@
(* Lemma 49, page 28 *)
lemma alloc_prog_NbR_LeadsTo_lemma3:
- "[|G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
+ "[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
k\<in>nat|]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
(* Proof by induction over the difference between k and n *)
apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
@@ -326,8 +326,8 @@
lemma alloc_prog_giv_Ensures_lemma:
"[| G \<in> program; k\<in>nat; alloc_prog ok G;
- alloc_prog Join G \<in> Incr(lift(ask)) |] ==>
- alloc_prog Join G \<in>
+ alloc_prog \<squnion> G \<in> Incr(lift(ask)) |] ==>
+ alloc_prog \<squnion> G \<in>
{s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
{s\<in>state. k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
Ensures {s\<in>state. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
@@ -360,7 +360,7 @@
lemma alloc_prog_giv_Stable_lemma:
"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
- ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
+ ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains)
apply (auto intro: leI)
apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
@@ -374,15 +374,15 @@
lemma alloc_prog_giv_LeadsTo_lemma:
"[| G \<in> program; alloc_prog ok G;
- alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |]
- ==> alloc_prog Join G \<in>
+ alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat |]
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
{s\<in>state. k < length(s`ask)} \<inter>
{s\<in>state. length(s`giv) = k}
LeadsTo {s\<in>state. k < length(s`giv)}"
-apply (subgoal_tac "alloc_prog Join G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} LeadsTo {s\<in>state. ~ k <length(s`ask) } Un {s\<in>state. length(s`giv) \<noteq> k}")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} LeadsTo {s\<in>state. ~ k <length(s`ask) } Un {s\<in>state. length(s`giv) \<noteq> k}")
prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
apply (drule PSP_Stable, assumption)
apply (rule LeadsTo_weaken)
apply (rule PSP_Stable)
@@ -400,12 +400,12 @@
(NbT) does not exceed the number currently available.*)
lemma alloc_prog_Always_lemma:
"[| G \<in> program; alloc_prog ok G;
- alloc_prog Join G \<in> Incr(lift(ask));
- alloc_prog Join G \<in> Incr(lift(rel)) |]
- ==> alloc_prog Join G \<in>
+ alloc_prog \<squnion> G \<in> Incr(lift(ask));
+ alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
+ ==> alloc_prog \<squnion> G \<in>
Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
NbT \<le> s`available_tok})"
-apply (subgoal_tac "alloc_prog Join G \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> {s\<in>state. s`available_tok #+ tokens(s`giv) = NbT #+ tokens(take (s`NbR, s`rel))}) ")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> {s\<in>state. s`available_tok #+ tokens(s`giv) = NbT #+ tokens(take (s`NbR, s`rel))}) ")
apply (rule_tac [2] AlwaysI)
apply (rule_tac [3] giv_Bounded_lemma2, auto)
apply (rule Always_weaken, assumption, auto)
@@ -448,11 +448,11 @@
fixes G
assumes Gprog [intro,simp]: "G \<in> program"
and okG [iff]: "alloc_prog ok G"
- and Incr_rel [intro]: "alloc_prog Join G \<in> Incr(lift(rel))"
- and Incr_ask [intro]: "alloc_prog Join G \<in> Incr(lift(ask))"
- and safety: "alloc_prog Join G
+ and Incr_rel [intro]: "alloc_prog \<squnion> G \<in> Incr(lift(rel))"
+ and Incr_ask [intro]: "alloc_prog \<squnion> G \<in> Incr(lift(ask))"
+ and safety: "alloc_prog \<squnion> G
\<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
- and progress: "alloc_prog Join G
+ and progress: "alloc_prog \<squnion> G
\<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
{s\<in>state. k \<le> tokens(s`rel)})"
@@ -461,7 +461,7 @@
will eventually recognize that they've been released.*)
lemma (in alloc_progress) tokens_take_NbR_lemma:
"k \<in> tokbag
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. k \<le> tokens(s`rel)}
LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
apply (rule single_LeadsTo_I, safe)
@@ -480,7 +480,7 @@
LeadsTo *)
lemma (in alloc_progress) tokens_take_NbR_lemma2:
"k \<in> tokbag
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. tokens(s`giv) = k}
LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
apply (rule LeadsTo_Trans)
@@ -493,7 +493,7 @@
(*Third step in proof of (31): by PSP with the fact that giv increases *)
lemma (in alloc_progress) length_giv_disj:
"[| k \<in> tokbag; n \<in> nat |]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
LeadsTo
{s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
@@ -513,7 +513,7 @@
(*Fourth step in proof of (31): we apply lemma (51) *)
lemma (in alloc_progress) length_giv_disj2:
"[|k \<in> tokbag; n \<in> nat|]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
LeadsTo
{s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
@@ -526,7 +526,7 @@
k\<in>nat *)
lemma (in alloc_progress) length_giv_disj3:
"n \<in> nat
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n}
LeadsTo
{s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
@@ -541,7 +541,7 @@
assumption that ask increases *)
lemma (in alloc_progress) length_ask_giv:
"[|k \<in> nat; n < k|]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k & length(s`giv) = n}
LeadsTo
{s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
@@ -564,7 +564,7 @@
(*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
lemma (in alloc_progress) length_ask_giv2:
"[|k \<in> nat; n < k|]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k & length(s`giv) = n}
LeadsTo
{s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
@@ -581,7 +581,7 @@
(*Eighth step in proof of (31): by 50, we get |giv| > n. *)
lemma (in alloc_progress) extend_giv:
"[| k \<in> nat; n < k|]
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k & length(s`giv) = n}
LeadsTo {s\<in>state. n < length(s`giv)}"
apply (rule LeadsTo_Un_duplicate)
@@ -597,7 +597,7 @@
we can't expect |ask| to remain fixed until |giv| increases.*)
lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
"k \<in> nat
- ==> alloc_prog Join G \<in>
+ ==> alloc_prog \<squnion> G \<in>
{s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
(* Proof by induction over the difference between k and n *)
apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct)
@@ -622,9 +622,9 @@
(*Final lemma: combine previous result with lemma (30)*)
lemma (in alloc_progress) final:
"h \<in> list(tokbag)
- ==> alloc_prog Join G \<in>
- {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
- {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
+ ==> alloc_prog \<squnion> G
+ \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+ {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
apply (rule single_LeadsTo_I)
prefer 2 apply simp
apply (rename_tac s0)
--- a/src/ZF/UNITY/ClientImpl.thy Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Wed Jun 25 13:17:26 2003 +0200
@@ -8,6 +8,22 @@
theory ClientImpl = AllocBase + Guar:
+
+(*????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
+
+
consts
ask :: i (* input history: tokens requested *)
giv :: i (* output history: tokens granted *)
@@ -66,20 +82,6 @@
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)
@@ -164,7 +166,7 @@
lemma ask_Bounded_lemma:
"[| client_prog ok G; G \<in> program |]
- ==> client_prog Join G \<in>
+ ==> client_prog \<squnion> 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)
@@ -194,15 +196,15 @@
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)})"
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
+ ==> client_prog \<squnion> 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)})"
+ "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
+ ==> client_prog \<squnion> 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:
@@ -243,8 +245,8 @@
done
lemma induct_lemma:
-"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
- ==> client_prog Join G \<in>
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
+ ==> client_prog \<squnion> 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)
@@ -272,8 +274,8 @@
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>
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
+ ==> client_prog \<squnion> 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)}"
@@ -301,11 +303,12 @@
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)
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
+ ==> client_prog \<squnion> 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
@@ -331,4 +334,4 @@
cons_Int_distrib safety_prop_Acts_iff)
done
-end
\ No newline at end of file
+end
--- a/src/ZF/UNITY/Distributor.ML Tue Jun 24 16:32:59 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(* Title: ZF/UNITY/Distributor
- ID: $Id$
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2002 University of Cambridge
-
-A multiple-client allocator from a single-client allocator:
-Distributor specification
-*)
-
-Open_locale "Distributor";
-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 \\<in> state ==> s`In \\<in> list(A)";
-by (dres_inst_tac [("a", "In")] apply_type 1);
-by Auto_tac;
-qed "In_value_type";
-AddTCs [In_value_type];
-Addsimps [In_value_type];
-
-Goalw [state_def]
-"s \\<in> state ==> s`iIn \\<in> list(nat)";
-by (dres_inst_tac [("a", "iIn")] apply_type 1);
-by Auto_tac;
-qed "iIn_value_type";
-AddTCs [iIn_value_type];
-Addsimps [iIn_value_type];
-
-Goalw [state_def]
-"s \\<in> state ==> s`Out(n):list(A)";
-by (dres_inst_tac [("a", "Out(n)")] apply_type 1);
-by Auto_tac;
-qed "Out_value_type";
-AddTCs [Out_value_type];
-Addsimps [Out_value_type];
-
-val distrib = thm "distr_spec";
-
-Goal "D \\<in> program";
-by (cut_facts_tac [distrib] 1);
-by (auto_tac (claset(), simpset() addsimps
- [distr_spec_def, distr_allowed_acts_def]));
-qed "D_in_program";
-Addsimps [D_in_program];
-AddTCs [D_in_program];
-
-Goal "G \\<in> program ==> \
-\ D ok G <-> \
-\ ((\\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n)))) & D \\<in> Allowed(G))";
-by (cut_facts_tac [distrib] 1);
-by (auto_tac (claset(),
- simpset() addsimps [INT_iff, distr_spec_def, distr_allowed_acts_def,
- Allowed_def, ok_iff_Allowed]));
-by (rotate_tac ~1 2);
-by (dres_inst_tac [("x", "G")] bspec 2);
-by Auto_tac;
-by (dresolve_tac [rotate_prems 1 (safety_prop_Acts_iff RS iffD1)] 1);
-by (auto_tac (claset() addIs [safety_prop_Inter], simpset()));
-qed "D_ok_iff";
-
-Goal
-"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
-\ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
-\ Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt<Nclients})) \
-\ guarantees \
-\ (\\<Inter>n \\<in> Nclients. lift(Out(n)) IncreasingWrt \
-\ prefix(A)/list(A))";
-by (cut_facts_tac [D_in_program, distrib] 1);
-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()));
-qed "distr_Increasing_Out";
-
-val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
-
-Goal
-"[| \\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n))); \
-\ D Join G \\<in> Always({s \\<in> state. \
-\ \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients}) |] \
-\ ==> D Join G : Always \
-\ ({s \\<in> state. msetsum(%n. bag_of (sublist(s`In, \
-\ {k \\<in> nat. k < length(s`iIn) &\
-\ nth(k, s`iIn)= n})), \
-\ Nclients, A) = \
-\ bag_of(sublist(s`In, length(s`iIn)))})";
-by (cut_facts_tac [D_in_program] 1);
-by (subgoal_tac "G \\<in> program" 1);
-by (blast_tac (claset() addDs [preserves_type RS subsetD]) 2);
-by (etac ([asm_rl, state_AlwaysI2] MRS (Always_Diff_Un_eq RS iffD1)) 1);
-by Auto_tac;
-by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [nat_into_Finite]) 1);
-by (Blast_tac 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [set_of_list_conv_nth]) 1);
-by (subgoal_tac
- "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
-\ length(x`iIn)" 1);
-by (Asm_simp_tac 1);
-by (resolve_tac [equalityI] 1);
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [ltD]) 1);
-by (subgoal_tac "length(x ` iIn) : nat" 1);
-by Typecheck_tac;
-by (subgoal_tac "xa : nat" 1);
-by (dres_inst_tac [("x", "nth(xa, x`iIn)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec 1);
-by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt])));
-by (blast_tac (claset() addDs [ltD]) 1);
-by (blast_tac (claset() addIs [lt_trans]) 1);
-qed "distr_bag_Follows_lemma";
-
-Goal
- "D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
-\ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
-\ Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})) \
-\ guarantees \
-\ (\\<Inter>n \\<in> Nclients. \
-\ (%s. msetsum(%i. bag_of(s`Out(i)), Nclients, A)) \
-\ Fols \
-\ (%s. bag_of(sublist(s`In, length(s`iIn)))) \
-\ Wrt MultLe(A, r)/Mult(A))";
-by (cut_facts_tac [distrib] 1);
-by (rtac guaranteesI 1);
-by (Clarify_tac 1);
-by (Simp_tac 2);
-by (rtac (distr_bag_Follows_lemma RS Always_Follows2) 1);
-by Auto_tac;
-by (rtac Follows_state_ofD1 2);
-by (rtac Follows_msetsum_UN 2);
-by (ALLGOALS(Clarify_tac));
-by (resolve_tac [conjI] 3);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 3);
-by (resolve_tac [conjI] 4);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 4);
-by (resolve_tac [conjI] 5);
-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 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);
-by (auto_tac (claset(),
- simpset() addsimps [distr_spec_def, distr_follows_def]));
-by (dtac guaranteesD 1);
-by (assume_tac 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]
- addcongs [Follows_cong]) 1);
-qed "distr_bag_Follows";
-Close_locale "Distributor";
--- a/src/ZF/UNITY/Distributor.thy Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/Distributor.thy Wed Jun 25 13:17:26 2003 +0200
@@ -6,44 +6,160 @@
A multiple-client allocator from a single-client allocator:
Distributor specification
*)
-Distributor = AllocBase + Follows + Guar + GenPrefix +
-(** Distributor specification (the number of outputs is Nclients) ***)
- (*spec (14)*)
-constdefs
- distr_follows :: [i, i, i, i =>i] =>i
+
+theory Distributor = AllocBase + Follows + Guar + GenPrefix:
+
+text{*Distributor specification (the number of outputs is Nclients)*}
+
+text{*spec (14)*}
+constdefs
+ distr_follows :: "[i, i, i, i =>i] =>i"
"distr_follows(A, In, iIn, Out) ==
- (lift(In) IncreasingWrt prefix(A)/list(A)) Int
- (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int
- Always({s:state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})
+ (lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
+ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
+ Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients})
guarantees
- (\\<Inter>n \\<in> Nclients.
+ (\<Inter>n \<in> Nclients.
lift(Out(n))
Fols
- (%s. sublist(s`In, {k \\<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
+ (%s. sublist(s`In, {k \<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
Wrt prefix(A)/list(A))"
-
- distr_allowed_acts :: [i=>i]=>i
- "distr_allowed_acts(Out) ==
- {D:program. AllowedActs(D) =
- cons(id(state), \\<Union>G \\<in> (\\<Inter>n\\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
+
+ distr_allowed_acts :: "[i=>i]=>i"
+ "distr_allowed_acts(Out) ==
+ {D \<in> program. AllowedActs(D) =
+ cons(id(state), \<Union>G \<in> (\<Inter>n\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
+
+ distr_spec :: "[i, i, i, i =>i]=>i"
+ "distr_spec(A, In, iIn, Out) ==
+ distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)"
+
+locale distr =
+ fixes In --{*items to distribute*}
+ and iIn --{*destinations of items to distribute*}
+ and Out --{*distributed items*}
+ and A --{*the type of items being distributed *}
+ and D
+ assumes
+ var_assumes [simp]: "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)"
+ and all_distinct_vars: "\<forall>n. all_distinct([In, iIn, iOut(n)])"
+ and type_assumes [simp]: "type_of(In)=list(A) & type_of(iIn)=list(nat) &
+ (\<forall>n. type_of(Out(n))=list(A))"
+ and default_val_assumes [simp]:
+ "default_val(In)=Nil &
+ default_val(iIn)=Nil &
+ (\<forall>n. default_val(Out(n))=Nil)"
+ and distr_spec: "D \<in> distr_spec(A, In, iIn, Out)"
+
- distr_spec :: [i, i, i, i =>i]=>i
- "distr_spec(A, In, iIn, Out) ==
- distr_follows(A, In, iIn, Out) Int distr_allowed_acts(Out)"
+lemma (in distr) In_value_type [simp,TC]: "s \<in> state ==> s`In \<in> list(A)"
+apply (unfold state_def)
+apply (drule_tac a = In in apply_type, auto)
+done
+
+lemma (in distr) iIn_value_type [simp,TC]:
+ "s \<in> state ==> s`iIn \<in> list(nat)"
+apply (unfold state_def)
+apply (drule_tac a = iIn in apply_type, auto)
+done
+
+lemma (in distr) Out_value_type [simp,TC]:
+ "s \<in> state ==> s`Out(n):list(A)"
+apply (unfold state_def)
+apply (drule_tac a = "Out (n)" in apply_type)
+apply auto
+done
+
+lemma (in distr) D_in_program [simp,TC]: "D \<in> program"
+apply (cut_tac distr_spec)
+apply (auto simp add: distr_spec_def distr_allowed_acts_def)
+done
+
+lemma (in distr) D_ok_iff:
+ "G \<in> program ==>
+ D ok G <-> ((\<forall>n \<in> nat. G \<in> preserves(lift(Out(n)))) & D \<in> Allowed(G))"
+apply (cut_tac distr_spec)
+apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def
+ Allowed_def ok_iff_Allowed)
+apply (drule_tac [2] x = G and P = "%y. x \<notin> Acts(y)" in bspec)
+apply auto
+apply (drule safety_prop_Acts_iff [THEN [2] rev_iffD1])
+apply (auto intro: safety_prop_Inter)
+done
-locale Distributor =
- fixes In :: i (*items to distribute*)
- iIn :: i (*destinations of items to distribute*)
- Out :: i=>i (*distributed items*)
- A :: i (*the type of items being distributed *)
- D :: i
- assumes
- var_assumes "In:var & iIn:var & (\\<forall>n. Out(n):var)"
- all_distinct_vars "\\<forall>n. all_distinct([In, iIn, iOut(n)])"
- type_assumes "type_of(In)=list(A) & type_of(iIn)=list(nat) &
- (\\<forall>n. type_of(Out(n))=list(A))"
- default_val_assumes "default_val(In)=Nil &
- default_val(iIn)=Nil &
- (\\<forall>n. default_val(Out(n))=Nil)"
- distr_spec "D:distr_spec(A, In, iIn, Out)"
+lemma (in distr) distr_Increasing_Out:
+"D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
+ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
+ Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt<Nclients}))
+ guarantees
+ (\<Inter>n \<in> Nclients. lift(Out(n)) IncreasingWrt
+ prefix(A)/list(A))"
+apply (cut_tac D_in_program distr_spec)
+apply (simp (no_asm_use) add: distr_spec_def distr_follows_def)
+apply (auto intro!: guaranteesI intro: Follows_imp_Increasing_left
+ dest!: guaranteesD)
+done
+
+lemma (in distr) distr_bag_Follows_lemma:
+"[| \<forall>n \<in> nat. G \<in> preserves(lift(Out(n)));
+ D \<squnion> G \<in> Always({s \<in> state.
+ \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}) |]
+ ==> D \<squnion> G \<in> Always
+ ({s \<in> state. msetsum(%n. bag_of (sublist(s`In,
+ {k \<in> nat. k < length(s`iIn) &
+ nth(k, s`iIn)= n})),
+ Nclients, A) =
+ bag_of(sublist(s`In, length(s`iIn)))})"
+apply (cut_tac D_in_program)
+apply (subgoal_tac "G \<in> program")
+ prefer 2 apply (blast dest: preserves_type [THEN subsetD])
+apply (erule Always_Diff_Un_eq [THEN iffD1])
+apply (rule state_AlwaysI [THEN Always_weaken], auto)
+apply (rename_tac s)
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+ apply (simp (no_asm_simp) add: nat_into_Finite)
+ apply blast
+ apply (simp (no_asm_simp))
+apply (simp add: set_of_list_conv_nth [of _ nat])
+apply (subgoal_tac
+ "(\<Union>i \<in> Nclients. {k\<in>nat. k < length(s`iIn) & nth(k, s`iIn) = i}) =
+ length(s`iIn) ")
+apply (simp (no_asm_simp))
+apply (rule equalityI)
+apply (force simp add: ltD, safe)
+apply (rename_tac m)
+apply (subgoal_tac "length (s ` iIn) \<in> nat")
+apply typecheck
+apply (subgoal_tac "m \<in> nat")
+apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. ?X (elt) --> elt<Nclients" in bspec)
+apply (simp add: ltI)
+apply (simp_all add: Ord_mem_iff_lt)
+apply (blast dest: ltD)
+apply (blast intro: lt_trans)
+done
+
+theorem (in distr) distr_bag_Follows:
+ "D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
+ (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
+ Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}))
+ guarantees
+ (\<Inter>n \<in> Nclients.
+ (%s. msetsum(%i. bag_of(s`Out(i)), Nclients, A))
+ Fols
+ (%s. bag_of(sublist(s`In, length(s`iIn))))
+ Wrt MultLe(A, r)/Mult(A))"
+apply (cut_tac distr_spec)
+apply (rule guaranteesI, clarify)
+apply (rule distr_bag_Follows_lemma [THEN Always_Follows2])
+apply (simp add: D_ok_iff, auto)
+apply (rule Follows_state_ofD1)
+apply (rule Follows_msetsum_UN)
+ apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
+apply (auto simp add: distr_spec_def distr_follows_def)
+apply (drule guaranteesD, assumption)
+apply (simp_all cong add: Follows_cong
+ add: refl_prefix
+ mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
+done
+
end
--- a/src/ZF/UNITY/UNITYMisc.ML Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.ML Wed Jun 25 13:17:26 2003 +0200
@@ -7,11 +7,6 @@
*)
-Goalw [greaterThan_def]
-"i:greaterThan(k,A) <-> i:A & k<i";
-by Auto_tac;
-qed "greaterThan_iff";
-
(** Ad-hoc set-theory rules **)
Goal "Union(B) Int A = (UN b:B. b Int A)";
@@ -22,11 +17,6 @@
by Auto_tac;
qed "Int_Union_Union2";
-Goal "A Un B - (A - B) = B";
-by (Blast_tac 1);
-qed "Un_Diff_Diff";
-AddIffs [Un_Diff_Diff];
-
(** Needed in State theory for the current definition of variables
where they are indexed by lists **)
@@ -38,22 +28,17 @@
qed "list_nat_into_univ";
-(** Simplication rules for Collect; ????
- At least change to "{x:A. P(x)} Int A = {x : A Int B. P(x)} **)
-
-Goal "{x:A. P(x)} Int A = {x:A. P(x)}";
-by Auto_tac;
-qed "Collect_Int2";
+(** Simplication rules for Collect **)
-Goal "A Int {x:A. P(x)} = {x:A. P(x)}";
+(*Currently unused*)
+Goal "{x:A. P(x)} Int B = {x : A Int B. P(x)}";
by Auto_tac;
-qed "Collect_Int3";
+qed "Collect_Int_left";
-(*????????????????*)
-AddIffs [Collect_Int2, Collect_Int3];
-
-
-(*for main ZF????*)
+(*Currently unused*)
+Goal "A Int {x:B. P(x)} = {x : A Int B. P(x)}";
+by Auto_tac;
+qed "Collect_Int_right";
Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
by Auto_tac;
--- a/src/ZF/UNITY/UNITYMisc.thy Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.thy Wed Jun 25 13:17:26 2003 +0200
@@ -8,8 +8,4 @@
-UNITYMisc = Main +
-constdefs
- greaterThan :: [i,i]=> i
- "greaterThan(u,A) == {x:A. u<x}"
-end
\ No newline at end of file
+UNITYMisc = Main
\ No newline at end of file