--- a/src/ZF/UNITY/AllocImpl.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Sat Oct 10 22:02:23 2015 +0200
@@ -248,7 +248,7 @@
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}"
+ \<longmapsto>w {s\<in>state. k \<le> s`NbR}"
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)
@@ -268,7 +268,7 @@
k\<in>nat; n \<in> nat; n < k |]
==> 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>
+ \<longmapsto>w {x \<in> state. k \<le> length(x`rel)} \<inter>
(\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
apply (unfold greater_than_def)
apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
@@ -301,7 +301,7 @@
"[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
k\<in>nat|]
==> alloc_prog \<squnion> G \<in>
- {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
+ {s\<in>state. k \<le> length(s`rel)} \<longmapsto>w {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)
apply (simp_all add: lam_def, auto)
@@ -376,8 +376,8 @@
{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 \<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) } \<union> {s\<in>state. length(s`giv) \<noteq> k}")
+ \<longmapsto>w {s\<in>state. k < length(s`giv)}"
+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} \<longmapsto>w {s\<in>state. ~ k <length(s`ask) } \<union> {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 \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
apply (drule PSP_Stable, assumption)
@@ -424,12 +424,12 @@
subsubsection\<open>Main lemmas towards proving property (31)\<close>
lemma LeadsTo_strength_R:
- "[| F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo B"
+ "[| F \<in> C \<longmapsto>w B'; F \<in> A-C \<longmapsto>w B; B'<=B |] ==> F \<in> A \<longmapsto>w B"
by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
lemma PSP_StableI:
-"[| F \<in> Stable(C); F \<in> A - C LeadsTo B;
- F \<in> A \<inter> C LeadsTo B \<union> (state - C) |] ==> F \<in> A LeadsTo B"
+"[| F \<in> Stable(C); F \<in> A - C \<longmapsto>w B;
+ F \<in> A \<inter> C \<longmapsto>w B \<union> (state - C) |] ==> F \<in> A \<longmapsto>w B"
apply (rule_tac A = " (A-C) \<union> (A \<inter> C)" in LeadsTo_weaken_L)
prefer 2 apply blast
apply (rule LeadsTo_Un, assumption)
@@ -453,7 +453,7 @@
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 \<squnion> G
- \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
+ \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} \<longmapsto>w
{s\<in>state. k \<le> tokens(s`rel)})"
(*First step in proof of (31) -- the corrected version from Charpentier.
@@ -463,7 +463,7 @@
"k \<in> tokbag
==> 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))}"
+ \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
apply (rule single_LeadsTo_I, safe)
apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI])
apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
@@ -477,12 +477,12 @@
(*** Rest of proofs done by lcp ***)
(*Second step in proof of (31): by LHS of the guarantee and transivity of
- LeadsTo *)
+ \<longmapsto>w *)
lemma (in alloc_progress) tokens_take_NbR_lemma2:
"k \<in> tokbag
==> alloc_prog \<squnion> G \<in>
{s\<in>state. tokens(s`giv) = k}
- LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
+ \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
apply (rule LeadsTo_Trans)
apply (rule_tac [2] tokens_take_NbR_lemma)
prefer 2 apply assumption
@@ -495,7 +495,7 @@
"[| k \<in> tokbag; n \<in> nat |]
==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
- LeadsTo
+ \<longmapsto>w
{s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
apply (rule single_LeadsTo_I, safe)
@@ -515,7 +515,7 @@
"[|k \<in> tokbag; n \<in> nat|]
==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
- LeadsTo
+ \<longmapsto>w
{s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
n < length(s`giv)}"
apply (rule LeadsTo_weaken_R)
@@ -528,7 +528,7 @@
"n \<in> nat
==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n}
- LeadsTo
+ \<longmapsto>w
{s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
n < length(s`giv)}"
apply (rule LeadsTo_weaken_L)
@@ -543,7 +543,7 @@
"[|k \<in> nat; n < k|]
==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k & length(s`giv) = n}
- LeadsTo
+ \<longmapsto>w
{s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
length(s`giv) = n) |
n < length(s`giv)}"
@@ -566,7 +566,7 @@
"[|k \<in> nat; n < k|]
==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k & length(s`giv) = n}
- LeadsTo
+ \<longmapsto>w
{s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
length(s`giv) < length(s`ask) & length(s`giv) = n) |
n < length(s`giv)}"
@@ -583,7 +583,7 @@
"[| k \<in> nat; n < k|]
==> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k & length(s`giv) = n}
- LeadsTo {s\<in>state. n < length(s`giv)}"
+ \<longmapsto>w {s\<in>state. n < length(s`giv)}"
apply (rule LeadsTo_Un_duplicate)
apply (rule LeadsTo_cancel1)
apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
@@ -598,7 +598,7 @@
lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
"k \<in> nat
==> alloc_prog \<squnion> G \<in>
- {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
+ {s\<in>state. k \<le> length(s`ask)} \<longmapsto>w {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)
apply (auto simp add: lam_def Collect_vimage_eq)
@@ -623,7 +623,7 @@
lemma (in alloc_progress) final:
"h \<in> list(tokbag)
==> alloc_prog \<squnion> G
- \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+ \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} \<longmapsto>w
{s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
apply (rule single_LeadsTo_I)
prefer 2 apply simp
@@ -647,10 +647,10 @@
"alloc_prog \<in>
Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} \<longmapsto>w
{s\<in>state. k \<le> tokens(s`rel)})
guarantees (\<Inter>h \<in> list(tokbag).
- {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+ {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} \<longmapsto>w
{s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
apply (rule guaranteesI)
apply (rule INT_I)