--- 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)
--- a/src/ZF/UNITY/ClientImpl.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Sat Oct 10 22:02:23 2015 +0200
@@ -219,7 +219,7 @@
==> 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)
+ \<longmapsto>w {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}"
@@ -248,7 +248,7 @@
==> 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)}"
+ \<longmapsto>w {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)
@@ -276,7 +276,7 @@
"[| 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)}"
+ \<longmapsto>w {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)
@@ -291,7 +291,7 @@
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)})"
+ h pfixGe s`ask} \<longmapsto>w {s \<in> state. <h, s`rel> \<in> prefix(nat)})"
apply (rule guaranteesI)
apply (blast intro: progress_lemma, auto)
done
--- a/src/ZF/UNITY/Comp.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/Comp.thy Sat Oct 10 22:02:23 2015 +0200
@@ -19,7 +19,7 @@
definition
component :: "[i,i]=>o" (infixl "component" 65) where
- "F component H == (\<exists>G. F Join G = H)"
+ "F component H == (\<exists>G. F \<squnion> G = H)"
definition
strict_component :: "[i,i]=>o" (infixl "strict'_component" 65) where
@@ -28,7 +28,7 @@
definition
(* A stronger form of the component relation *)
component_of :: "[i,i]=>o" (infixl "component'_of" 65) where
- "F component_of H == (\<exists>G. F ok G & F Join G = H)"
+ "F component_of H == (\<exists>G. F ok G & F \<squnion> G = H)"
definition
strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65) where
@@ -52,10 +52,10 @@
(*** component and strict_component relations ***)
lemma componentI:
- "H component F | H component G ==> H component (F Join G)"
+ "H component F | H component G ==> H component (F \<squnion> G)"
apply (unfold component_def, auto)
-apply (rule_tac x = "Ga Join G" in exI)
-apply (rule_tac [2] x = "G Join F" in exI)
+apply (rule_tac x = "Ga \<squnion> G" in exI)
+apply (rule_tac [2] x = "G \<squnion> F" in exI)
apply (auto simp add: Join_ac)
done
@@ -84,22 +84,22 @@
apply (simp_all add: component_eq_subset, blast)
done
-lemma component_Join1: "F component (F Join G)"
+lemma component_Join1: "F component (F \<squnion> G)"
by (unfold component_def, blast)
-lemma component_Join2: "G component (F Join G)"
+lemma component_Join2: "G component (F \<squnion> G)"
apply (unfold component_def)
apply (simp (no_asm) add: Join_commute)
apply blast
done
-lemma Join_absorb1: "F component G ==> F Join G = G"
+lemma Join_absorb1: "F component G ==> F \<squnion> G = G"
by (auto simp add: component_def Join_left_absorb)
-lemma Join_absorb2: "G component F ==> F Join G = F"
+lemma Join_absorb2: "G component F ==> F \<squnion> G = F"
by (auto simp add: Join_ac component_def)
-lemma JN_component_iff:
+lemma JOIN_component_iff:
"H \<in> program==>(JOIN(I,F) component H) \<longleftrightarrow> (\<forall>i \<in> I. F(i) component H)"
apply (case_tac "I=0", force)
apply (simp (no_asm_simp) add: component_eq_subset)
@@ -110,9 +110,9 @@
apply (blast elim!: not_emptyE)+
done
-lemma component_JN: "i \<in> I ==> F(i) component (\<Squnion>i \<in> I. (F(i)))"
+lemma component_JOIN: "i \<in> I ==> F(i) component (\<Squnion>i \<in> I. (F(i)))"
apply (unfold component_def)
-apply (blast intro: JN_absorb)
+apply (blast intro: JOIN_absorb)
done
lemma component_trans: "[| F component G; G component H |] ==> F component H"
@@ -129,7 +129,7 @@
lemma Join_component_iff:
"H \<in> program ==>
- ((F Join G) component H) \<longleftrightarrow> (F component H & G component H)"
+ ((F \<squnion> G) component H) \<longleftrightarrow> (F component H & G component H)"
apply (simp (no_asm_simp) add: component_eq_subset)
apply blast
done
@@ -163,13 +163,13 @@
done
lemma Join_preserves [iff]:
-"(F Join G \<in> preserves(v)) \<longleftrightarrow>
+"(F \<squnion> G \<in> preserves(v)) \<longleftrightarrow>
(programify(F) \<in> preserves(v) & programify(G) \<in> preserves(v))"
by (auto simp add: preserves_def INT_iff)
-lemma JN_preserves [iff]:
+lemma JOIN_preserves [iff]:
"(JOIN(I,F): preserves(v)) \<longleftrightarrow> (\<forall>i \<in> I. programify(F(i)):preserves(v))"
-by (auto simp add: JN_stable preserves_def INT_iff)
+by (auto simp add: JOIN_stable preserves_def INT_iff)
lemma SKIP_preserves [iff]: "SKIP \<in> preserves(v)"
by (auto simp add: preserves_def INT_iff)
@@ -286,7 +286,7 @@
lemma stable_localTo_stable2:
"[| F \<in> stable({s \<in> state. P(f(s), g(s))}); G \<in> preserves(f); G \<in> preserves(g) |]
- ==> F Join G \<in> stable({s \<in> state. P(f(s), g(s))})"
+ ==> F \<squnion> G \<in> stable({s \<in> state. P(f(s), g(s))})"
apply (auto dest: ActsD preserves_into_program simp add: stable_def constrains_def)
apply (case_tac "act \<in> Acts (F) ")
apply auto
@@ -296,9 +296,9 @@
lemma Increasing_preserves_Stable:
"[| F \<in> stable({s \<in> state. <f(s), g(s)>:r}); G \<in> preserves(f);
- F Join G \<in> Increasing(A, r, g);
+ F \<squnion> G \<in> Increasing(A, r, g);
\<forall>x \<in> state. f(x):A & g(x):A |]
- ==> F Join G \<in> Stable({s \<in> state. <f(s), g(s)>:r})"
+ ==> F \<squnion> G \<in> Stable({s \<in> state. <f(s), g(s)>:r})"
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
apply (simp_all add: constrains_type [THEN subsetD] preserves_type [THEN subsetD])
apply (blast intro: constrains_weaken)
@@ -321,9 +321,9 @@
lemma stable_Join_Stable:
"[| F \<in> stable({s \<in> state. P(f(s), g(s))});
- \<forall>k \<in> A. F Join G \<in> Stable({s \<in> state. P(k, g(s))});
+ \<forall>k \<in> A. F \<squnion> G \<in> Stable({s \<in> state. P(k, g(s))});
G \<in> preserves(f); \<forall>s \<in> state. f(s):A|]
- ==> F Join G \<in> Stable({s \<in> state. P(f(s), g(s))})"
+ ==> F \<squnion> G \<in> Stable({s \<in> state. P(f(s), g(s))})"
apply (unfold stable_def Stable_def preserves_def)
apply (rule_tac A = "(\<Union>k \<in> A. {s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))})" in Constrains_weaken_L)
prefer 2 apply blast
--- a/src/ZF/UNITY/Follows.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/Follows.thy Sat Oct 10 22:02:23 2015 +0200
@@ -15,7 +15,7 @@
Increasing(A, r, g) Int
Increasing(A, r,f) Int
Always({s \<in> state. <f(s), g(s)>:r}) Int
- (\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} LeadsTo {s \<in> state. <k,f(s)>:r})"
+ (\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} \<longmapsto>w {s \<in> state. <k,f(s)>:r})"
abbreviation
Incr :: "[i=>i]=>i" where
@@ -79,8 +79,8 @@
lemma subset_LeadsTo_comp:
"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s);
\<forall>x \<in> state. f(x):A & g(x):A |] ==>
- (\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r}) <=
- (\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})"
+ (\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} \<longmapsto>w {s \<in> state. <j,f(s)> \<in> r}) <=
+ (\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} \<longmapsto>w {x \<in> state. <k, (h comp f)(x)> \<in> s})"
apply (unfold mono1_def metacomp_def, clarify)
apply (simp_all (no_asm_use) add: INT_iff)
@@ -97,19 +97,19 @@
done
lemma imp_LeadsTo_comp:
-"[| F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r});
+"[| F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} \<longmapsto>w {s \<in> state. <j,f(s)> \<in> r});
mono1(A, r, B, s, h); refl(A,r); trans[B](s);
\<forall>x \<in> state. f(x):A & g(x):A |] ==>
- F:(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} LeadsTo {x \<in> state. <k, (h comp f)(x)> \<in> s})"
+ F:(\<Inter>k \<in> B. {x \<in> state. <k, (h comp g)(x)> \<in> s} \<longmapsto>w {x \<in> state. <k, (h comp f)(x)> \<in> s})"
apply (rule subset_LeadsTo_comp [THEN subsetD], auto)
done
lemma imp_LeadsTo_comp_right:
"[| F \<in> Increasing(B, s, g);
- \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
+ \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} \<longmapsto>w {s \<in> state. <j,f1(s)> \<in> r};
mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t);
\<forall>x \<in> state. f1(x):A & f(x):A & g(x):B; k \<in> C |] ==>
- F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g(x))> \<in> t}"
+ F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f1(x), g(x))> \<in> t}"
apply (unfold mono2_def Increasing_def)
apply (rule single_LeadsTo_I, auto)
apply (drule_tac x = "g (sa) " and A = B in bspec)
@@ -129,10 +129,10 @@
lemma imp_LeadsTo_comp_left:
"[| F \<in> Increasing(A, r, f);
- \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
+ \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} \<longmapsto>w {x \<in> state. <j,g1(x)> \<in> s};
mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
\<forall>x \<in> state. f(x):A & g1(x):B & g(x):B; k \<in> C |] ==>
- F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
+ F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
apply (unfold mono2_def Increasing_def)
apply (rule single_LeadsTo_I, auto)
apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (X (k))" for X in bspec)
@@ -153,11 +153,11 @@
(** This general result is used to prove Follows Un, munion, etc. **)
lemma imp_LeadsTo_comp2:
"[| F \<in> Increasing(A, r, f1) \<inter> Increasing(B, s, g);
- \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};
- \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};
+ \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} \<longmapsto>w {s \<in> state. <j,f1(s)> \<in> r};
+ \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} \<longmapsto>w {x \<in> state. <j,g1(x)> \<in> s};
mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
\<forall>x \<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \<in> C |]
- ==> F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g1(x))> \<in> t}"
+ ==> F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f1(x), g1(x))> \<in> t}"
apply (rule_tac B = "{x \<in> state. <k, h (f1 (x), g (x))> \<in> t}" in LeadsTo_Trans)
apply (blast intro: imp_LeadsTo_comp_right)
apply (blast intro: imp_LeadsTo_comp_left)
@@ -259,17 +259,17 @@
lemma Follows_imp_LeadsTo:
"[| F \<in> Follows(A, r, f, g); k \<in> A |] ==>
- F: {s \<in> state. <k,g(s)> \<in> r } LeadsTo {s \<in> state. <k,f(s)> \<in> r}"
+ F: {s \<in> state. <k,g(s)> \<in> r } \<longmapsto>w {s \<in> state. <k,f(s)> \<in> r}"
by (unfold Follows_def, blast)
lemma Follows_LeadsTo_pfixLe:
"[| F \<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \<in> list(nat) |]
- ==> F \<in> {s \<in> state. k pfixLe g(s)} LeadsTo {s \<in> state. k pfixLe f(s)}"
+ ==> F \<in> {s \<in> state. k pfixLe g(s)} \<longmapsto>w {s \<in> state. k pfixLe f(s)}"
by (blast intro: Follows_imp_LeadsTo)
lemma Follows_LeadsTo_pfixGe:
"[| F \<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \<in> list(nat) |]
- ==> F \<in> {s \<in> state. k pfixGe g(s)} LeadsTo {s \<in> state. k pfixGe f(s)}"
+ ==> F \<in> {s \<in> state. k pfixGe g(s)} \<longmapsto>w {s \<in> state. k pfixGe f(s)}"
by (blast intro: Follows_imp_LeadsTo)
lemma Always_Follows1:
--- a/src/ZF/UNITY/Guar.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/Guar.thy Sat Oct 10 22:02:23 2015 +0200
@@ -25,7 +25,7 @@
(* To be moved to theory WFair???? *)
-lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) |] ==> F \<in> A leadsTo B"
+lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) |] ==> F \<in> A \<longmapsto> B"
apply (frule constrainsD2)
apply (drule_tac B = "A-B" in constrains_weaken_L, blast)
apply (drule_tac B = "A-B" in transient_strengthen, blast)
@@ -39,27 +39,27 @@
definition
ex_prop :: "i => o" where
"ex_prop(X) == X<=program &
- (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X | G \<in> X \<longrightarrow> (F Join G) \<in> X)"
+ (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X | G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X)"
definition
strict_ex_prop :: "i => o" where
"strict_ex_prop(X) == X<=program &
- (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<in> X | G \<in> X) \<longleftrightarrow> (F Join G \<in> X))"
+ (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<in> X | G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X))"
definition
uv_prop :: "i => o" where
"uv_prop(X) == X<=program &
- (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X & G \<in> X \<longrightarrow> (F Join G) \<in> X))"
+ (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X & G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X))"
definition
strict_uv_prop :: "i => o" where
"strict_uv_prop(X) == X<=program &
- (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F Join G \<in> X)))"
+ (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X)))"
definition
guar :: "[i, i] => i" (infixl "guarantees" 55) where
(*higher than membership, lower than Co*)
- "X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X \<longrightarrow> F Join G \<in> Y}"
+ "X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X \<longrightarrow> F \<squnion> G \<in> Y}"
definition
(* Weakest guarantees *)
@@ -72,15 +72,15 @@
"wx(X) == \<Union>({Y \<in> Pow(program). Y<=X & ex_prop(Y)})"
definition
- (*Ill-defined programs can arise through "Join"*)
+ (*Ill-defined programs can arise through "\<squnion>"*)
welldef :: i where
"welldef == {F \<in> program. Init(F) \<noteq> 0}"
definition
refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10) where
"G refines F wrt X ==
- \<forall>H \<in> program. (F ok H & G ok H & F Join H \<in> welldef \<inter> X)
- \<longrightarrow> (G Join H \<in> welldef \<inter> X)"
+ \<forall>H \<in> program. (F ok H & G ok H & F \<squnion> H \<in> welldef \<inter> X)
+ \<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"
definition
iso_refines :: "[i,i, i] => o" ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) where
@@ -166,14 +166,14 @@
(*** guarantees ***)
lemma guaranteesI:
- "[| (!!G. [| F ok G; F Join G \<in> X; G \<in> program |] ==> F Join G \<in> Y);
+ "[| (!!G. [| F ok G; F \<squnion> G \<in> X; G \<in> program |] ==> F \<squnion> G \<in> Y);
F \<in> program |]
==> F \<in> X guarantees Y"
by (simp add: guar_def component_def)
lemma guaranteesD:
- "[| F \<in> X guarantees Y; F ok G; F Join G \<in> X; G \<in> program |]
- ==> F Join G \<in> Y"
+ "[| F \<in> X guarantees Y; F ok G; F \<squnion> G \<in> X; G \<in> program |]
+ ==> F \<squnion> G \<in> Y"
by (simp add: guar_def component_def)
@@ -181,7 +181,7 @@
The major premise can no longer be F\<subseteq>H since we need to reason about G*)
lemma component_guaranteesD:
- "[| F \<in> X guarantees Y; F Join G = H; H \<in> X; F ok G; G \<in> program |]
+ "[| F \<in> X guarantees Y; F \<squnion> G = H; H \<in> X; F ok G; G \<in> program |]
==> H \<in> Y"
by (simp add: guar_def, blast)
@@ -198,10 +198,10 @@
"[| X \<subseteq> Y; F \<in> program |] ==> F \<in> X guarantees Y"
by (unfold guar_def, blast)
-lemma component_of_Join1: "F ok G ==> F component_of (F Join G)"
+lemma component_of_Join1: "F ok G ==> F component_of (F \<squnion> G)"
by (unfold component_of_def, blast)
-lemma component_of_Join2: "F ok G ==> G component_of (F Join G)"
+lemma component_of_Join2: "F ok G ==> G component_of (F \<squnion> G)"
apply (subst Join_commute)
apply (blast intro: ok_sym component_of_Join1)
done
@@ -305,82 +305,82 @@
lemma guarantees_Join_Int:
"[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
- ==> F Join G: (U \<inter> X) guarantees (V \<inter> Y)"
+ ==> F \<squnion> G: (U \<inter> X) guarantees (V \<inter> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
-apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (subgoal_tac "F \<squnion> G \<squnion> Ga = G \<squnion> (F \<squnion> Ga) ")
apply (simp add: ok_commute)
apply (simp (no_asm_simp) add: Join_ac)
done
lemma guarantees_Join_Un:
"[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
- ==> F Join G: (U \<union> X) guarantees (V \<union> Y)"
+ ==> F \<squnion> G: (U \<union> X) guarantees (V \<union> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
-apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (subgoal_tac "F \<squnion> G \<squnion> Ga = G \<squnion> (F \<squnion> Ga) ")
apply (rotate_tac 4)
-apply (drule_tac x = "F Join Ga" in bspec)
+apply (drule_tac x = "F \<squnion> Ga" in bspec)
apply (simp (no_asm))
apply (force simp add: ok_commute)
apply (simp (no_asm_simp) add: Join_ac)
done
-lemma guarantees_JN_INT:
+lemma guarantees_JOIN_INT:
"[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i); OK(I,F); i \<in> I |]
==> (\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. X(i)) guarantees (\<Inter>i \<in> I. Y(i))"
apply (unfold guar_def, safe)
prefer 2 apply blast
apply (drule_tac x = xa in bspec)
apply (simp_all add: INT_iff, safe)
-apply (drule_tac x = "(\<Squnion>x \<in> (I-{xa}) . F (x)) Join G" and A=program in bspec)
-apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
+apply (drule_tac x = "(\<Squnion>x \<in> (I-{xa}) . F (x)) \<squnion> G" and A=program in bspec)
+apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JOIN_Join_diff JOIN_absorb)
done
-lemma guarantees_JN_UN:
+lemma guarantees_JOIN_UN:
"[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i); OK(I,F) |]
==> JOIN(I,F) \<in> (\<Union>i \<in> I. X(i)) guarantees (\<Union>i \<in> I. Y(i))"
apply (unfold guar_def, auto)
apply (drule_tac x = y in bspec, simp_all, safe)
apply (rename_tac G y)
-apply (drule_tac x = "JOIN (I-{y}, F) Join G" and A=program in bspec)
-apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
+apply (drule_tac x = "JOIN (I-{y}, F) \<squnion> G" and A=program in bspec)
+apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JOIN_Join_diff JOIN_absorb)
done
(*** guarantees laws for breaking down the program, by lcp ***)
lemma guarantees_Join_I1:
- "[| F \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
+ "[| F \<in> X guarantees Y; F ok G |] ==> F \<squnion> G \<in> X guarantees Y"
apply (simp add: guar_def, safe)
apply (simp add: Join_assoc)
done
lemma guarantees_Join_I2:
- "[| G \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
+ "[| G \<in> X guarantees Y; F ok G |] ==> F \<squnion> G \<in> X guarantees Y"
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
apply (blast intro: guarantees_Join_I1)
done
-lemma guarantees_JN_I:
+lemma guarantees_JOIN_I:
"[| i \<in> I; F(i) \<in> X guarantees Y; OK(I,F) |]
==> (\<Squnion>i \<in> I. F(i)) \<in> X guarantees Y"
apply (unfold guar_def, safe)
-apply (drule_tac x = "JOIN (I-{i},F) Join G" in bspec)
+apply (drule_tac x = "JOIN (I-{i},F) \<squnion> G" in bspec)
apply (simp (no_asm))
-apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric])
+apply (auto intro: OK_imp_ok simp add: JOIN_Join_diff Join_assoc [symmetric])
done
(*** well-definedness ***)
-lemma Join_welldef_D1: "F Join G \<in> welldef ==> programify(F) \<in> welldef"
+lemma Join_welldef_D1: "F \<squnion> G \<in> welldef ==> programify(F) \<in> welldef"
by (unfold welldef_def, auto)
-lemma Join_welldef_D2: "F Join G \<in> welldef ==> programify(G) \<in> welldef"
+lemma Join_welldef_D2: "F \<squnion> G \<in> welldef ==> programify(G) \<in> welldef"
by (unfold welldef_def, auto)
(*** refinement ***)
@@ -435,7 +435,7 @@
apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD])
apply (simp_all add: component_of_def)
apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
-apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
+apply (auto intro: JOIN_Join_diff dest: ok_sym simp add: OK_iff_ok)
done
lemma wg_ex_prop:
@@ -461,17 +461,17 @@
(* Proposition 6 *)
lemma wx'_ex_prop:
- "ex_prop({F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X})"
+ "ex_prop({F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X})"
apply (unfold ex_prop_def, safe)
- apply (drule_tac x = "G Join Ga" in bspec)
+ apply (drule_tac x = "G \<squnion> Ga" in bspec)
apply (simp (no_asm))
apply (force simp add: Join_assoc)
-apply (drule_tac x = "F Join Ga" in bspec)
+apply (drule_tac x = "F \<squnion> Ga" in bspec)
apply (simp (no_asm))
apply (simp (no_asm_use))
apply safe
apply (simp (no_asm_simp) add: ok_commute)
-apply (subgoal_tac "F Join G = G Join F")
+apply (subgoal_tac "F \<squnion> G = G \<squnion> F")
apply (simp (no_asm_simp) add: Join_assoc)
apply (simp (no_asm) add: Join_commute)
done
@@ -479,12 +479,12 @@
(* Equivalence with the other definition of wx *)
lemma wx_equiv:
- "wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F Join G) \<in> X}"
+ "wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<squnion> G) \<in> X}"
apply (unfold wx_def)
apply (rule equalityI, safe, blast)
apply (simp (no_asm_use) add: ex_prop_def)
apply blast
-apply (rule_tac B = "{F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F Join G \<in> X}"
+apply (rule_tac B = "{F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X}"
in UnionI,
safe)
apply (rule_tac [2] wx'_ex_prop)
@@ -521,7 +521,7 @@
lemma constrains_guarantees_leadsTo:
"[| F \<in> transient(A); st_set(B) |]
- ==> F: (A co A \<union> B) guarantees (A leadsTo (B-A))"
+ ==> F: (A co A \<union> B) guarantees (A \<longmapsto> (B-A))"
apply (rule guaranteesI)
prefer 2 apply (blast dest: transient_type [THEN subsetD])
apply (rule leadsTo_Basis')
--- a/src/ZF/UNITY/Mutex.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/Mutex.thy Sat Oct 10 22:02:23 2015 +0200
@@ -206,15 +206,15 @@
by (unfold op_Unless_def Mutex_def, safety)
lemma U_F1:
- "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
+ "Mutex \<in> {s \<in> state. s`m=#1} \<longmapsto>w {s \<in> state. s`p = s`v & s`m = #2}"
by (unfold Mutex_def, ensures U1)
-lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}"
+lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} \<longmapsto>w {s \<in> state. s`m = #3}"
apply (cut_tac IU)
apply (unfold Mutex_def, ensures U2)
done
-lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}"
+lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} \<longmapsto>w {s \<in> state. s`p=1}"
apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
apply (unfold Mutex_def)
apply (ensures U3)
@@ -222,14 +222,14 @@
done
-lemma U_lemma2: "Mutex \<in> {s \<in> state. s`m = #2} LeadsTo {s \<in> state. s`p=1}"
+lemma U_lemma2: "Mutex \<in> {s \<in> state. s`m = #2} \<longmapsto>w {s \<in> state. s`p=1}"
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
Int_lower2 [THEN subset_imp_LeadsTo]])
apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
apply (auto dest!: p_value_type simp add: bool_def)
done
-lemma U_lemma1: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`p =1}"
+lemma U_lemma1: "Mutex \<in> {s \<in> state. s`m = #1} \<longmapsto>w {s \<in> state. s`p =1}"
by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
lemma eq_123: "i \<in> int ==> (#1 $<= i & i $<= #3) \<longleftrightarrow> (i=#1 | i=#2 | i=#3)"
@@ -243,12 +243,12 @@
done
-lemma U_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \<in> state. s`p=1}"
+lemma U_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`m & s`m $<= #3} \<longmapsto>w {s \<in> state. s`p=1}"
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3)
(*Misra's F4*)
-lemma u_Leadsto_p: "Mutex \<in> {s \<in> state. s`u = 1} LeadsTo {s \<in> state. s`p=1}"
+lemma u_Leadsto_p: "Mutex \<in> {s \<in> state. s`u = 1} \<longmapsto>w {s \<in> state. s`p=1}"
by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
@@ -257,43 +257,43 @@
lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}"
by (unfold op_Unless_def Mutex_def, safety)
-lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
+lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} \<longmapsto>w {s \<in> state. s`p = not(s`u) & s`n = #2}"
by (unfold Mutex_def, ensures "V1")
-lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}"
+lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} \<longmapsto>w {s \<in> state. s`n = #3}"
apply (cut_tac IV)
apply (unfold Mutex_def, ensures "V2")
done
-lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}"
+lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} \<longmapsto>w {s \<in> state. s`p=0}"
apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
apply (unfold Mutex_def)
apply (ensures V3)
apply (ensures V4)
done
-lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}"
+lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} \<longmapsto>w {s \<in> state. s`p=0}"
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
Int_lower2 [THEN subset_imp_LeadsTo]])
apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
apply (auto dest!: p_value_type simp add: bool_def)
done
-lemma V_lemma1: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`p = 0}"
+lemma V_lemma1: "Mutex \<in> {s \<in> state. s`n = #1} \<longmapsto>w {s \<in> state. s`p = 0}"
by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
-lemma V_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \<in> state. s`p = 0}"
+lemma V_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`n & s`n $<= #3} \<longmapsto>w {s \<in> state. s`p = 0}"
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3)
(*Misra's F4*)
-lemma v_Leadsto_not_p: "Mutex \<in> {s \<in> state. s`v = 1} LeadsTo {s \<in> state. s`p = 0}"
+lemma v_Leadsto_not_p: "Mutex \<in> {s \<in> state. s`v = 1} \<longmapsto>w {s \<in> state. s`p = 0}"
by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
(** Absence of starvation **)
(*Misra's F6*)
-lemma m1_Leadsto_3: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`m = #3}"
+lemma m1_Leadsto_3: "Mutex \<in> {s \<in> state. s`m = #1} \<longmapsto>w {s \<in> state. s`m = #3}"
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
apply (rule_tac [2] U_F2)
apply (simp add: Collect_conj_eq)
@@ -306,7 +306,7 @@
(*The same for V*)
-lemma n1_Leadsto_3: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`n = #3}"
+lemma n1_Leadsto_3: "Mutex \<in> {s \<in> state. s`n = #1} \<longmapsto>w {s \<in> state. s`n = #3}"
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
apply (rule_tac [2] V_F2)
apply (simp add: Collect_conj_eq)
--- a/src/ZF/UNITY/SubstAx.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Sat Oct 10 22:02:23 2015 +0200
@@ -17,58 +17,54 @@
"A Ensures B == {F \<in> program. F \<in> (reachable(F) \<inter> A) ensures (reachable(F) \<inter> B) }"
definition
- LeadsTo :: "[i, i] => i" (infixl "LeadsTo" 60) where
- "A LeadsTo B == {F \<in> program. F:(reachable(F) \<inter> A) leadsTo (reachable(F) \<inter> B)}"
-
-notation (xsymbols)
- LeadsTo (infixl " \<longmapsto>w " 60)
-
+ LeadsTo :: "[i, i] => i" (infixl "\<longmapsto>w" 60) where
+ "A \<longmapsto>w B == {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> (reachable(F) \<inter> B)}"
(*Resembles the previous definition of LeadsTo*)
(* Equivalence with the HOL-like definition *)
lemma LeadsTo_eq:
-"st_set(B)==> A LeadsTo B = {F \<in> program. F:(reachable(F) \<inter> A) leadsTo B}"
+"st_set(B)==> A \<longmapsto>w B = {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> B}"
apply (unfold LeadsTo_def)
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
done
-lemma LeadsTo_type: "A LeadsTo B <=program"
+lemma LeadsTo_type: "A \<longmapsto>w B <=program"
by (unfold LeadsTo_def, auto)
(*** Specialized laws for handling invariants ***)
(** Conjoining an Always property **)
-lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) LeadsTo A') \<longleftrightarrow> (F \<in> A LeadsTo A')"
+lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) \<longmapsto>w A') \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
-lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A LeadsTo (I \<inter> A')) \<longleftrightarrow> (F \<in> A LeadsTo A')"
+lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A \<longmapsto>w (I \<inter> A')) \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
apply (unfold LeadsTo_def)
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
done
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
-lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A'"
+lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C \<inter> A) \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w A'"
by (blast intro: Always_LeadsTo_pre [THEN iffD1])
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
-lemma Always_LeadsToD: "[| F \<in> Always(C); F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (C \<inter> A')"
+lemma Always_LeadsToD: "[| F \<in> Always(C); F \<in> A \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w (C \<inter> A')"
by (blast intro: Always_LeadsTo_post [THEN iffD2])
(*** Introduction rules \<in> Basis, Trans, Union ***)
-lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
+lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A \<longmapsto>w B"
by (auto simp add: Ensures_def LeadsTo_def)
lemma LeadsTo_Trans:
- "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
+ "[| F \<in> A \<longmapsto>w B; F \<in> B \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C"
apply (simp (no_asm_use) add: LeadsTo_def)
apply (blast intro: leadsTo_Trans)
done
lemma LeadsTo_Union:
-"[|(!!A. A \<in> S ==> F \<in> A LeadsTo B); F \<in> program|]==>F \<in> \<Union>(S) LeadsTo B"
+"[|(!!A. A \<in> S ==> F \<in> A \<longmapsto>w B); F \<in> program|]==>F \<in> \<Union>(S) \<longmapsto>w B"
apply (simp add: LeadsTo_def)
apply (subst Int_Union_Union2)
apply (rule leadsTo_UN, auto)
@@ -76,23 +72,23 @@
(*** Derived rules ***)
-lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
+lemma leadsTo_imp_LeadsTo: "F \<in> A \<longmapsto> B ==> F \<in> A \<longmapsto>w B"
apply (frule leadsToD2, clarify)
apply (simp (no_asm_simp) add: LeadsTo_eq)
apply (blast intro: leadsTo_weaken_L)
done
(*Useful with cancellation, disjunction*)
-lemma LeadsTo_Un_duplicate: "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
+lemma LeadsTo_Un_duplicate: "F \<in> A \<longmapsto>w (A' \<union> A') ==> F \<in> A \<longmapsto>w A'"
by (simp add: Un_ac)
lemma LeadsTo_Un_duplicate2:
- "F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)"
+ "F \<in> A \<longmapsto>w (A' \<union> C \<union> C) ==> F \<in> A \<longmapsto>w (A' \<union> C)"
by (simp add: Un_ac)
lemma LeadsTo_UN:
- "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo B); F \<in> program|]
- ==>F:(\<Union>i \<in> I. A(i)) LeadsTo B"
+ "[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w B); F \<in> program|]
+ ==>F:(\<Union>i \<in> I. A(i)) \<longmapsto>w B"
apply (simp add: LeadsTo_def)
apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)
apply (rule leadsTo_UN, auto)
@@ -100,7 +96,7 @@
(*Binary union introduction rule*)
lemma LeadsTo_Un:
- "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
+ "[| F \<in> A \<longmapsto>w C; F \<in> B \<longmapsto>w C |] ==> F \<in> (A \<union> B) \<longmapsto>w C"
apply (subst Un_eq_Union)
apply (rule LeadsTo_Union)
apply (auto dest: LeadsTo_type [THEN subsetD])
@@ -108,63 +104,63 @@
(*Lets us look at the starting state*)
lemma single_LeadsTo_I:
- "[|(!!s. s \<in> A ==> F:{s} LeadsTo B); F \<in> program|]==>F \<in> A LeadsTo B"
+ "[|(!!s. s \<in> A ==> F:{s} \<longmapsto>w B); F \<in> program|]==>F \<in> A \<longmapsto>w B"
apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)
done
-lemma subset_imp_LeadsTo: "[| A \<subseteq> B; F \<in> program |] ==> F \<in> A LeadsTo B"
+lemma subset_imp_LeadsTo: "[| A \<subseteq> B; F \<in> program |] ==> F \<in> A \<longmapsto>w B"
apply (simp (no_asm_simp) add: LeadsTo_def)
apply (blast intro: subset_imp_leadsTo)
done
-lemma empty_LeadsTo: "F \<in> 0 LeadsTo A \<longleftrightarrow> F \<in> program"
+lemma empty_LeadsTo: "F \<in> 0 \<longmapsto>w A \<longleftrightarrow> F \<in> program"
by (auto dest: LeadsTo_type [THEN subsetD]
intro: empty_subsetI [THEN subset_imp_LeadsTo])
declare empty_LeadsTo [iff]
-lemma LeadsTo_state: "F \<in> A LeadsTo state \<longleftrightarrow> F \<in> program"
+lemma LeadsTo_state: "F \<in> A \<longmapsto>w state \<longleftrightarrow> F \<in> program"
by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
declare LeadsTo_state [iff]
-lemma LeadsTo_weaken_R: "[| F \<in> A LeadsTo A'; A'<=B'|] ==> F \<in> A LeadsTo B'"
+lemma LeadsTo_weaken_R: "[| F \<in> A \<longmapsto>w A'; A'<=B'|] ==> F \<in> A \<longmapsto>w B'"
apply (unfold LeadsTo_def)
apply (auto intro: leadsTo_weaken_R)
done
-lemma LeadsTo_weaken_L: "[| F \<in> A LeadsTo A'; B \<subseteq> A |] ==> F \<in> B LeadsTo A'"
+lemma LeadsTo_weaken_L: "[| F \<in> A \<longmapsto>w A'; B \<subseteq> A |] ==> F \<in> B \<longmapsto>w A'"
apply (unfold LeadsTo_def)
apply (auto intro: leadsTo_weaken_L)
done
-lemma LeadsTo_weaken: "[| F \<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \<in> B LeadsTo B'"
+lemma LeadsTo_weaken: "[| F \<in> A \<longmapsto>w A'; B<=A; A'<=B' |] ==> F \<in> B \<longmapsto>w B'"
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
lemma Always_LeadsTo_weaken:
-"[| F \<in> Always(C); F \<in> A LeadsTo A'; C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |]
- ==> F \<in> B LeadsTo B'"
+"[| F \<in> Always(C); F \<in> A \<longmapsto>w A'; C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |]
+ ==> F \<in> B \<longmapsto>w B'"
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
done
(** Two theorems for "proof lattices" **)
-lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F:(A \<union> B) LeadsTo B"
+lemma LeadsTo_Un_post: "F \<in> A \<longmapsto>w B ==> F:(A \<union> B) \<longmapsto>w B"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_Un subset_imp_LeadsTo)
-lemma LeadsTo_Trans_Un: "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |]
- ==> F \<in> (A \<union> B) LeadsTo C"
+lemma LeadsTo_Trans_Un: "[| F \<in> A \<longmapsto>w B; F \<in> B \<longmapsto>w C |]
+ ==> F \<in> (A \<union> B) \<longmapsto>w C"
apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
done
(** Distributive laws **)
-lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) LeadsTo C) \<longleftrightarrow> (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
+lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) \<longmapsto>w C) \<longleftrightarrow> (F \<in> A \<longmapsto>w C & F \<in> B \<longmapsto>w C)"
by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
-lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) LeadsTo B) \<longleftrightarrow> (\<forall>i \<in> I. F \<in> A(i) LeadsTo B) & F \<in> program"
+lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w B) \<longleftrightarrow> (\<forall>i \<in> I. F \<in> A(i) \<longmapsto>w B) & F \<in> program"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_UN LeadsTo_weaken_L)
-lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) LeadsTo B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A LeadsTo B) & F \<in> program"
+lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto>w B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A \<longmapsto>w B) & F \<in> program"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_Union LeadsTo_weaken_L)
@@ -177,7 +173,7 @@
lemma Always_LeadsTo_Basis: "[| F \<in> Always(I); F \<in> (I \<inter> (A-A')) Co (A \<union> A');
F \<in> transient (I \<inter> (A-A')) |]
- ==> F \<in> A LeadsTo A'"
+ ==> F \<in> A \<longmapsto>w A'"
apply (rule Always_LeadsToI, assumption)
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done
@@ -185,36 +181,36 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
lemma LeadsTo_Diff:
- "[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |] ==> F \<in> A LeadsTo C"
+ "[| F \<in> (A-B) \<longmapsto>w C; F \<in> (A \<inter> B) \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C"
by (blast intro: LeadsTo_Un LeadsTo_weaken)
lemma LeadsTo_UN_UN:
- "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i)); F \<in> program |]
- ==> F \<in> (\<Union>i \<in> I. A(i)) LeadsTo (\<Union>i \<in> I. A'(i))"
+ "[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i)); F \<in> program |]
+ ==> F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w (\<Union>i \<in> I. A'(i))"
apply (rule LeadsTo_Union, auto)
apply (blast intro: LeadsTo_weaken_R)
done
(*Binary union version*)
lemma LeadsTo_Un_Un:
- "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] ==> F:(A \<union> B) LeadsTo (A' \<union> B')"
+ "[| F \<in> A \<longmapsto>w A'; F \<in> B \<longmapsto>w B' |] ==> F:(A \<union> B) \<longmapsto>w (A' \<union> B')"
by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
(** The cancellation law **)
-lemma LeadsTo_cancel2: "[| F \<in> A LeadsTo(A' \<union> B); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (A' \<union> B')"
+lemma LeadsTo_cancel2: "[| F \<in> A \<longmapsto>w(A' \<union> B); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')"
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
lemma Un_Diff: "A \<union> (B - A) = A \<union> B"
by auto
-lemma LeadsTo_cancel_Diff2: "[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (A' \<union> B')"
+lemma LeadsTo_cancel_Diff2: "[| F \<in> A \<longmapsto>w (A' \<union> B); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')"
apply (rule LeadsTo_cancel2)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: Un_Diff)
done
-lemma LeadsTo_cancel1: "[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (B' \<union> A')"
+lemma LeadsTo_cancel1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')"
apply (simp add: Un_commute)
apply (blast intro!: LeadsTo_cancel2)
done
@@ -222,7 +218,7 @@
lemma Diff_Un2: "(B - A) \<union> A = B \<union> A"
by auto
-lemma LeadsTo_cancel_Diff1: "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (B' \<union> A')"
+lemma LeadsTo_cancel_Diff1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')"
apply (rule LeadsTo_cancel1)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: Diff_Un2)
@@ -231,7 +227,7 @@
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
-lemma LeadsTo_empty: "F \<in> A LeadsTo 0 ==> F \<in> Always (state -A)"
+lemma LeadsTo_empty: "F \<in> A \<longmapsto>w 0 ==> F \<in> Always (state -A)"
apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
apply (cut_tac reachable_type)
apply (auto dest!: leadsTo_empty)
@@ -240,26 +236,26 @@
(** PSP \<in> Progress-Safety-Progress **)
(*Special case of PSP \<in> Misra's "stable conjunction"*)
-lemma PSP_Stable: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |]==> F:(A \<inter> B) LeadsTo (A' \<inter> B)"
+lemma PSP_Stable: "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(B) |]==> F:(A \<inter> B) \<longmapsto>w (A' \<inter> B)"
apply (simp add: LeadsTo_def Stable_eq_stable, clarify)
apply (drule psp_stable, assumption)
apply (simp add: Int_ac)
done
-lemma PSP_Stable2: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |] ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')"
+lemma PSP_Stable2: "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(B) |] ==> F \<in> (B \<inter> A) \<longmapsto>w (B \<inter> A')"
apply (simp (no_asm_simp) add: PSP_Stable Int_ac)
done
-lemma PSP: "[| F \<in> A LeadsTo A'; F \<in> B Co B'|]==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))"
+lemma PSP: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B'|]==> F \<in> (A \<inter> B') \<longmapsto>w ((A' \<inter> B) \<union> (B' - B))"
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
apply (blast dest: psp intro: leadsTo_weaken)
done
-lemma PSP2: "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]==> F:(B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))"
+lemma PSP2: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B' |]==> F:(B' \<inter> A) \<longmapsto>w ((B \<inter> A') \<union> (B' - B))"
by (simp (no_asm_simp) add: PSP Int_ac)
lemma PSP_Unless:
-"[| F \<in> A LeadsTo A'; F \<in> B Unless B'|]==> F:(A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')"
+"[| F \<in> A \<longmapsto>w A'; F \<in> B Unless B'|]==> F:(A \<inter> B) \<longmapsto>w ((A' \<inter> B) \<union> B')"
apply (unfold op_Unless_def)
apply (drule PSP, assumption)
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
@@ -269,10 +265,10 @@
(** Meta or object quantifier ????? **)
lemma LeadsTo_wf_induct: "[| wf(r);
- \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) LeadsTo
+ \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto>w
((A \<inter> f-``(converse(r) `` {m})) \<union> B);
field(r)<=I; A<=f-``I; F \<in> program |]
- ==> F \<in> A LeadsTo B"
+ ==> F \<in> A \<longmapsto>w B"
apply (simp (no_asm_use) add: LeadsTo_def)
apply auto
apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe)
@@ -282,8 +278,8 @@
done
-lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A \<inter> f-``{m}) LeadsTo ((A \<inter> f-``m) \<union> B);
- A<=f-``nat; F \<in> program |] ==> F \<in> A LeadsTo B"
+lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A \<inter> f-``{m}) \<longmapsto>w ((A \<inter> f-``m) \<union> B);
+ A<=f-``nat; F \<in> program |] ==> F \<in> A \<longmapsto>w B"
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN LeadsTo_wf_induct])
apply (simp_all add: nat_measure_field)
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
@@ -301,18 +297,18 @@
(*** Completion \<in> Binary and General Finite versions ***)
-lemma Completion: "[| F \<in> A LeadsTo (A' \<union> C); F \<in> A' Co (A' \<union> C);
- F \<in> B LeadsTo (B' \<union> C); F \<in> B' Co (B' \<union> C) |]
- ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)"
+lemma Completion: "[| F \<in> A \<longmapsto>w (A' \<union> C); F \<in> A' Co (A' \<union> C);
+ F \<in> B \<longmapsto>w (B' \<union> C); F \<in> B' Co (B' \<union> C) |]
+ ==> F \<in> (A \<inter> B) \<longmapsto>w ((A' \<inter> B') \<union> C)"
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib)
apply (blast intro: completion leadsTo_weaken)
done
lemma Finite_completion_aux:
"[| I \<in> Fin(X);F \<in> program |]
- ==> (\<forall>i \<in> I. F \<in> (A(i)) LeadsTo (A'(i) \<union> C)) \<longrightarrow>
+ ==> (\<forall>i \<in> I. F \<in> (A(i)) \<longmapsto>w (A'(i) \<union> C)) \<longrightarrow>
(\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) \<union> C)) \<longrightarrow>
- F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
+ F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)"
apply (erule Fin_induct)
apply (auto simp del: INT_simps simp add: Inter_0)
apply (rule Completion, auto)
@@ -321,16 +317,16 @@
done
lemma Finite_completion:
- "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) LeadsTo (A'(i) \<union> C);
+ "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w (A'(i) \<union> C);
!!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) \<union> C);
F \<in> program |]
- ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)"
by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
lemma Stable_completion:
- "[| F \<in> A LeadsTo A'; F \<in> Stable(A');
- F \<in> B LeadsTo B'; F \<in> Stable(B') |]
- ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')"
+ "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(A');
+ F \<in> B \<longmapsto>w B'; F \<in> Stable(B') |]
+ ==> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')"
apply (unfold Stable_def)
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
prefer 5
@@ -340,9 +336,9 @@
lemma Finite_stable_completion:
"[| I \<in> Fin(X);
- (!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i));
+ (!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i));
(!!i. i \<in> I ==>F \<in> Stable(A'(i))); F \<in> program |]
- ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo (\<Inter>i \<in> I. A'(i))"
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))"
apply (unfold Stable_def)
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
apply (rule_tac [3] subset_refl, auto)
--- a/src/ZF/UNITY/UNITY.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/UNITY.thy Sat Oct 10 22:02:23 2015 +0200
@@ -27,7 +27,7 @@
cons(id(state), allowed \<inter> Pow(state*state))>"
definition
- SKIP :: i where
+ SKIP :: i ("\<bottom>") where
"SKIP == mk_program(state, 0, Pow(state*state))"
(* Coercion from anything to program *)
--- a/src/ZF/UNITY/Union.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/Union.thy Sat Oct 10 22:02:23 2015 +0200
@@ -31,8 +31,8 @@
\<Inter>i \<in> I. AllowedActs(F(i)))"
definition
- Join :: "[i, i] => i" (infixl "Join" 65) where
- "F Join G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G),
+ Join :: "[i, i] => i" (infixl "\<squnion>" 65) where
+ "F \<squnion> G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G),
AllowedActs(F) \<inter> AllowedActs(G))"
definition
(*Characterizes safety properties. Used with specifying AllowedActs*)
@@ -40,21 +40,14 @@
"safety_prop(X) == X\<subseteq>program &
SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
-notation (xsymbols)
- SKIP ("\<bottom>") and
- Join (infixl "\<squnion>" 65)
-
syntax
- "_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10)
- "_JOIN" :: "[pttrn, i, i] => i" ("(3JN _ \<in> _./ _)" 10)
-syntax (xsymbols)
- "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
- "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
+ "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion>_./ _)" 10)
+ "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion>_ \<in> _./ _)" 10)
translations
- "JN x \<in> A. B" == "CONST JOIN(A, (%x. B))"
- "JN x y. B" == "JN x. JN y. B"
- "JN x. B" == "CONST JOIN(CONST state,(%x. B))"
+ "\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))"
+ "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
+ "\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))"
subsection\<open>SKIP\<close>
@@ -62,7 +55,7 @@
lemma reachable_SKIP [simp]: "reachable(SKIP) = state"
by (force elim: reachable.induct intro: reachable.intros)
-text\<open>Elimination programify from ok and Join\<close>
+text\<open>Elimination programify from ok and \<squnion>\<close>
lemma ok_programify_left [iff]: "programify(F) ok G \<longleftrightarrow> F ok G"
by (simp add: ok_def)
@@ -70,10 +63,10 @@
lemma ok_programify_right [iff]: "F ok programify(G) \<longleftrightarrow> F ok G"
by (simp add: ok_def)
-lemma Join_programify_left [simp]: "programify(F) Join G = F Join G"
+lemma Join_programify_left [simp]: "programify(F) \<squnion> G = F \<squnion> G"
by (simp add: Join_def)
-lemma Join_programify_right [simp]: "F Join programify(G) = F Join G"
+lemma Join_programify_right [simp]: "F \<squnion> programify(G) = F \<squnion> G"
by (simp add: Join_def)
subsection\<open>SKIP and safety properties\<close>
@@ -92,79 +85,79 @@
subsection\<open>Join and JOIN types\<close>
-lemma Join_in_program [iff,TC]: "F Join G \<in> program"
+lemma Join_in_program [iff,TC]: "F \<squnion> G \<in> program"
by (unfold Join_def, auto)
lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \<in> program"
by (unfold JOIN_def, auto)
subsection\<open>Init, Acts, and AllowedActs of Join and JOIN\<close>
-lemma Init_Join [simp]: "Init(F Join G) = Init(F) \<inter> Init(G)"
+lemma Init_Join [simp]: "Init(F \<squnion> G) = Init(F) \<inter> Init(G)"
by (simp add: Int_assoc Join_def)
-lemma Acts_Join [simp]: "Acts(F Join G) = Acts(F) \<union> Acts(G)"
+lemma Acts_Join [simp]: "Acts(F \<squnion> G) = Acts(F) \<union> Acts(G)"
by (simp add: Int_Un_distrib2 cons_absorb Join_def)
-lemma AllowedActs_Join [simp]: "AllowedActs(F Join G) =
+lemma AllowedActs_Join [simp]: "AllowedActs(F \<squnion> G) =
AllowedActs(F) \<inter> AllowedActs(G)"
apply (simp add: Int_assoc cons_absorb Join_def)
done
subsection\<open>Join's algebraic laws\<close>
-lemma Join_commute: "F Join G = G Join F"
+lemma Join_commute: "F \<squnion> G = G \<squnion> F"
by (simp add: Join_def Un_commute Int_commute)
-lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
+lemma Join_left_commute: "A \<squnion> (B \<squnion> C) = B \<squnion> (A \<squnion> C)"
apply (simp add: Join_def Int_Un_distrib2 cons_absorb)
apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb)
done
-lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
+lemma Join_assoc: "(F \<squnion> G) \<squnion> H = F \<squnion> (G \<squnion> H)"
by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2)
subsection\<open>Needed below\<close>
lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)"
by auto
-lemma Join_SKIP_left [simp]: "SKIP Join F = programify(F)"
+lemma Join_SKIP_left [simp]: "SKIP \<squnion> F = programify(F)"
apply (unfold Join_def SKIP_def)
apply (auto simp add: Int_absorb cons_eq)
done
-lemma Join_SKIP_right [simp]: "F Join SKIP = programify(F)"
+lemma Join_SKIP_right [simp]: "F \<squnion> SKIP = programify(F)"
apply (subst Join_commute)
apply (simp add: Join_SKIP_left)
done
-lemma Join_absorb [simp]: "F Join F = programify(F)"
+lemma Join_absorb [simp]: "F \<squnion> F = programify(F)"
by (rule program_equalityI, auto)
-lemma Join_left_absorb: "F Join (F Join G) = F Join G"
+lemma Join_left_absorb: "F \<squnion> (F \<squnion> G) = F \<squnion> G"
by (simp add: Join_assoc [symmetric])
subsection\<open>Join is an AC-operator\<close>
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
-subsection\<open>Eliminating programify form JN and OK expressions\<close>
+subsection\<open>Eliminating programify form JOIN and OK expressions\<close>
lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) \<longleftrightarrow> OK(I, F)"
by (simp add: OK_def)
-lemma JN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"
+lemma JOIN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"
by (simp add: JOIN_def)
-subsection\<open>JN\<close>
+subsection\<open>JOIN\<close>
-lemma JN_empty [simp]: "JOIN(0, F) = SKIP"
+lemma JOIN_empty [simp]: "JOIN(0, F) = SKIP"
by (unfold JOIN_def, auto)
-lemma Init_JN [simp]:
+lemma Init_JOIN [simp]:
"Init(\<Squnion>i \<in> I. F(i)) = (if I=0 then state else (\<Inter>i \<in> I. Init(F(i))))"
by (simp add: JOIN_def INT_extend_simps del: INT_simps)
-lemma Acts_JN [simp]:
+lemma Acts_JOIN [simp]:
"Acts(JOIN(I,F)) = cons(id(state), \<Union>i \<in> I. Acts(F(i)))"
apply (unfold JOIN_def)
apply (auto simp del: INT_simps UN_simps)
@@ -172,7 +165,7 @@
apply (auto dest: Acts_type [THEN subsetD])
done
-lemma AllowedActs_JN [simp]:
+lemma AllowedActs_JOIN [simp]:
"AllowedActs(\<Squnion>i \<in> I. F(i)) =
(if I=0 then Pow(state*state) else (\<Inter>i \<in> I. AllowedActs(F(i))))"
apply (unfold JOIN_def, auto)
@@ -180,42 +173,42 @@
apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD])
done
-lemma JN_cons [simp]: "(\<Squnion>i \<in> cons(a,I). F(i)) = F(a) Join (\<Squnion>i \<in> I. F(i))"
+lemma JOIN_cons [simp]: "(\<Squnion>i \<in> cons(a,I). F(i)) = F(a) \<squnion> (\<Squnion>i \<in> I. F(i))"
by (rule program_equalityI, auto)
-lemma JN_cong [cong]:
+lemma JOIN_cong [cong]:
"[| I=J; !!i. i \<in> J ==> F(i) = G(i) |] ==>
(\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))"
by (simp add: JOIN_def)
-subsection\<open>JN laws\<close>
-lemma JN_absorb: "k \<in> I ==>F(k) Join (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> I. F(i))"
-apply (subst JN_cons [symmetric])
+subsection\<open>JOIN laws\<close>
+lemma JOIN_absorb: "k \<in> I ==>F(k) \<squnion> (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> I. F(i))"
+apply (subst JOIN_cons [symmetric])
apply (auto simp add: cons_absorb)
done
-lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F(i)) = ((\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> J. F(i)))"
+lemma JOIN_Un: "(\<Squnion>i \<in> I \<union> J. F(i)) = ((\<Squnion>i \<in> I. F(i)) \<squnion> (\<Squnion>i \<in> J. F(i)))"
apply (rule program_equalityI)
apply (simp_all add: UN_Un INT_Un)
apply (simp_all del: INT_simps add: INT_extend_simps, blast)
done
-lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I=0 then SKIP else programify(c))"
+lemma JOIN_constant: "(\<Squnion>i \<in> I. c) = (if I=0 then SKIP else programify(c))"
by (rule program_equalityI, auto)
-lemma JN_Join_distrib:
- "(\<Squnion>i \<in> I. F(i) Join G(i)) = (\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> I. G(i))"
+lemma JOIN_Join_distrib:
+ "(\<Squnion>i \<in> I. F(i) \<squnion> G(i)) = (\<Squnion>i \<in> I. F(i)) \<squnion> (\<Squnion>i \<in> I. G(i))"
apply (rule program_equalityI)
apply (simp_all add: INT_Int_distrib, blast)
done
-lemma JN_Join_miniscope: "(\<Squnion>i \<in> I. F(i) Join G) = ((\<Squnion>i \<in> I. F(i) Join G))"
-by (simp add: JN_Join_distrib JN_constant)
+lemma JOIN_Join_miniscope: "(\<Squnion>i \<in> I. F(i) \<squnion> G) = ((\<Squnion>i \<in> I. F(i) \<squnion> G))"
+by (simp add: JOIN_Join_distrib JOIN_constant)
-text\<open>Used to prove guarantees_JN_I\<close>
-lemma JN_Join_diff: "i \<in> I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)"
+text\<open>Used to prove guarantees_JOIN_I\<close>
+lemma JOIN_Join_diff: "i \<in> I==>F(i) \<squnion> JOIN(I - {i}, F) = JOIN(I, F)"
apply (rule program_equalityI)
apply (auto elim!: not_emptyE)
done
@@ -227,7 +220,7 @@
alternative precondition is A\<subseteq>B, but most proofs using this rule require
I to be nonempty for other reasons anyway.*)
-lemma JN_constrains:
+lemma JOIN_constrains:
"i \<in> I==>(\<Squnion>i \<in> I. F(i)) \<in> A co B \<longleftrightarrow> (\<forall>i \<in> I. programify(F(i)) \<in> A co B)"
apply (unfold constrains_def JOIN_def st_set_def, auto)
@@ -238,34 +231,34 @@
done
lemma Join_constrains [iff]:
- "(F Join G \<in> A co B) \<longleftrightarrow> (programify(F) \<in> A co B & programify(G) \<in> A co B)"
+ "(F \<squnion> G \<in> A co B) \<longleftrightarrow> (programify(F) \<in> A co B & programify(G) \<in> A co B)"
by (auto simp add: constrains_def)
lemma Join_unless [iff]:
- "(F Join G \<in> A unless B) \<longleftrightarrow>
+ "(F \<squnion> G \<in> A unless B) \<longleftrightarrow>
(programify(F) \<in> A unless B & programify(G) \<in> A unless B)"
by (simp add: Join_constrains unless_def)
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
- reachable (F Join G) could be much bigger than reachable F, reachable G
+ reachable (F \<squnion> G) could be much bigger than reachable F, reachable G
*)
lemma Join_constrains_weaken:
"[| F \<in> A co A'; G \<in> B co B' |]
- ==> F Join G \<in> (A \<inter> B) co (A' \<union> B')"
+ ==> F \<squnion> G \<in> (A \<inter> B) co (A' \<union> B')"
apply (subgoal_tac "st_set (A) & st_set (B) & F \<in> program & G \<in> program")
prefer 2 apply (blast dest: constrainsD2, simp)
apply (blast intro: constrains_weaken)
done
(*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*)
-lemma JN_constrains_weaken:
+lemma JOIN_constrains_weaken:
assumes major: "(!!i. i \<in> I ==> F(i) \<in> A(i) co A'(i))"
and minor: "i \<in> I"
shows "(\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))"
apply (cut_tac minor)
-apply (simp (no_asm_simp) add: JN_constrains)
+apply (simp (no_asm_simp) add: JOIN_constrains)
apply clarify
apply (rename_tac "j")
apply (frule_tac i = j in major)
@@ -273,14 +266,14 @@
apply (blast intro: constrains_weaken)
done
-lemma JN_stable:
+lemma JOIN_stable:
"(\<Squnion>i \<in> I. F(i)) \<in> stable(A) \<longleftrightarrow> ((\<forall>i \<in> I. programify(F(i)) \<in> stable(A)) & st_set(A))"
apply (auto simp add: stable_def constrains_def JOIN_def)
apply (cut_tac F = "F (i) " in Acts_type)
apply (drule_tac x = act in bspec, auto)
done
-lemma initially_JN_I:
+lemma initially_JOIN_I:
assumes major: "(!!i. i \<in> I ==>F(i) \<in> initially(A))"
and minor: "i \<in> I"
shows "(\<Squnion>i \<in> I. F(i)) \<in> initially(A)"
@@ -290,12 +283,12 @@
apply (auto simp add: initially_def)
done
-lemma invariant_JN_I:
+lemma invariant_JOIN_I:
assumes major: "(!!i. i \<in> I ==> F(i) \<in> invariant(A))"
and minor: "i \<in> I"
shows "(\<Squnion>i \<in> I. F(i)) \<in> invariant(A)"
apply (cut_tac minor)
-apply (auto intro!: initially_JN_I dest: major simp add: invariant_def JN_stable)
+apply (auto intro!: initially_JOIN_I dest: major simp add: invariant_def JOIN_stable)
apply (erule_tac V = "i \<in> I" in thin_rl)
apply (frule major)
apply (drule_tac [2] major)
@@ -304,17 +297,17 @@
done
lemma Join_stable [iff]:
- " (F Join G \<in> stable(A)) \<longleftrightarrow>
+ " (F \<squnion> G \<in> stable(A)) \<longleftrightarrow>
(programify(F) \<in> stable(A) & programify(G) \<in> stable(A))"
by (simp add: stable_def)
lemma initially_JoinI [intro!]:
- "[| F \<in> initially(A); G \<in> initially(A) |] ==> F Join G \<in> initially(A)"
+ "[| F \<in> initially(A); G \<in> initially(A) |] ==> F \<squnion> G \<in> initially(A)"
by (unfold initially_def, auto)
lemma invariant_JoinI:
"[| F \<in> invariant(A); G \<in> invariant(A) |]
- ==> F Join G \<in> invariant(A)"
+ ==> F \<squnion> G \<in> invariant(A)"
apply (subgoal_tac "F \<in> program&G \<in> program")
prefer 2 apply (blast dest: invariantD2)
apply (simp add: invariant_def)
@@ -323,12 +316,12 @@
(* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *)
-lemma FP_JN: "i \<in> I ==> FP(\<Squnion>i \<in> I. F(i)) = (\<Inter>i \<in> I. FP (programify(F(i))))"
-by (auto simp add: FP_def Inter_def st_set_def JN_stable)
+lemma FP_JOIN: "i \<in> I ==> FP(\<Squnion>i \<in> I. F(i)) = (\<Inter>i \<in> I. FP (programify(F(i))))"
+by (auto simp add: FP_def Inter_def st_set_def JOIN_stable)
subsection\<open>Progress: transient, ensures\<close>
-lemma JN_transient:
+lemma JOIN_transient:
"i \<in> I ==>
(\<Squnion>i \<in> I. F(i)) \<in> transient(A) \<longleftrightarrow> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))"
apply (auto simp add: transient_def JOIN_def)
@@ -338,29 +331,29 @@
done
lemma Join_transient [iff]:
- "F Join G \<in> transient(A) \<longleftrightarrow>
+ "F \<squnion> G \<in> transient(A) \<longleftrightarrow>
(programify(F) \<in> transient(A) | programify(G) \<in> transient(A))"
apply (auto simp add: transient_def Join_def Int_Un_distrib2)
done
-lemma Join_transient_I1: "F \<in> transient(A) ==> F Join G \<in> transient(A)"
+lemma Join_transient_I1: "F \<in> transient(A) ==> F \<squnion> G \<in> transient(A)"
by (simp add: Join_transient transientD2)
-lemma Join_transient_I2: "G \<in> transient(A) ==> F Join G \<in> transient(A)"
+lemma Join_transient_I2: "G \<in> transient(A) ==> F \<squnion> G \<in> transient(A)"
by (simp add: Join_transient transientD2)
(*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *)
-lemma JN_ensures:
+lemma JOIN_ensures:
"i \<in> I ==>
(\<Squnion>i \<in> I. F(i)) \<in> A ensures B \<longleftrightarrow>
((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A \<union> B)) &
(\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))"
-by (auto simp add: ensures_def JN_constrains JN_transient)
+by (auto simp add: ensures_def JOIN_constrains JOIN_transient)
lemma Join_ensures:
- "F Join G \<in> A ensures B \<longleftrightarrow>
+ "F \<squnion> G \<in> A ensures B \<longleftrightarrow>
(programify(F) \<in> (A-B) co (A \<union> B) & programify(G) \<in> (A-B) co (A \<union> B) &
(programify(F) \<in> transient (A-B) | programify(G) \<in> transient (A-B)))"
@@ -370,7 +363,7 @@
lemma stable_Join_constrains:
"[| F \<in> stable(A); G \<in> A co A' |]
- ==> F Join G \<in> A co A'"
+ ==> F \<squnion> G \<in> A co A'"
apply (unfold stable_def constrains_def Join_def st_set_def)
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = G in Acts_type, force)
@@ -379,7 +372,7 @@
(*Premise for G cannot use Always because F \<in> Stable A is
weaker than G \<in> stable A *)
lemma stable_Join_Always1:
- "[| F \<in> stable(A); G \<in> invariant(A) |] ==> F Join G \<in> Always(A)"
+ "[| F \<in> stable(A); G \<in> invariant(A) |] ==> F \<squnion> G \<in> Always(A)"
apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ")
prefer 2 apply (blast dest: invariantD2 stableD2)
apply (simp add: Always_def invariant_def initially_def Stable_eq_stable)
@@ -388,7 +381,7 @@
(*As above, but exchanging the roles of F and G*)
lemma stable_Join_Always2:
- "[| F \<in> invariant(A); G \<in> stable(A) |] ==> F Join G \<in> Always(A)"
+ "[| F \<in> invariant(A); G \<in> stable(A) |] ==> F \<squnion> G \<in> Always(A)"
apply (subst Join_commute)
apply (blast intro: stable_Join_Always1)
done
@@ -396,7 +389,7 @@
lemma stable_Join_ensures1:
- "[| F \<in> stable(A); G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
+ "[| F \<in> stable(A); G \<in> A ensures B |] ==> F \<squnion> G \<in> A ensures B"
apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ")
prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD])
apply (simp (no_asm_simp) add: Join_ensures)
@@ -407,7 +400,7 @@
(*As above, but exchanging the roles of F and G*)
lemma stable_Join_ensures2:
- "[| F \<in> A ensures B; G \<in> stable(A) |] ==> F Join G \<in> A ensures B"
+ "[| F \<in> A ensures B; G \<in> stable(A) |] ==> F \<squnion> G \<in> A ensures B"
apply (subst Join_commute)
apply (blast intro: stable_Join_ensures1)
done
@@ -421,7 +414,7 @@
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)
lemma ok_Join_commute:
- "(F ok G & (F Join G) ok H) \<longleftrightarrow> (G ok H & F ok (G Join H))"
+ "(F ok G & (F \<squnion> G) ok H) \<longleftrightarrow> (G ok H & F ok (G \<squnion> H))"
by (auto simp add: ok_def)
lemma ok_commute: "(F ok G) \<longleftrightarrow>(G ok F)"
@@ -429,24 +422,24 @@
lemmas ok_sym = ok_commute [THEN iffD1]
-lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) \<longleftrightarrow> (F ok G & (F Join G) ok H)"
+lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) \<longleftrightarrow> (F ok G & (F \<squnion> G) ok H)"
by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
Int_Un_distrib2 Ball_def, safe, force+)
-lemma ok_Join_iff1 [iff]: "F ok (G Join H) \<longleftrightarrow> (F ok G & F ok H)"
+lemma ok_Join_iff1 [iff]: "F ok (G \<squnion> H) \<longleftrightarrow> (F ok G & F ok H)"
by (auto simp add: ok_def)
-lemma ok_Join_iff2 [iff]: "(G Join H) ok F \<longleftrightarrow> (G ok F & H ok F)"
+lemma ok_Join_iff2 [iff]: "(G \<squnion> H) ok F \<longleftrightarrow> (G ok F & H ok F)"
by (auto simp add: ok_def)
(*useful? Not with the previous two around*)
-lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
+lemma ok_Join_commute_I: "[| F ok G; (F \<squnion> G) ok H |] ==> F ok (G \<squnion> H)"
by (auto simp add: ok_def)
-lemma ok_JN_iff1 [iff]: "F ok JOIN(I,G) \<longleftrightarrow> (\<forall>i \<in> I. F ok G(i))"
+lemma ok_JOIN_iff1 [iff]: "F ok JOIN(I,G) \<longleftrightarrow> (\<forall>i \<in> I. F ok G(i))"
by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def)
-lemma ok_JN_iff2 [iff]: "JOIN(I,G) ok F \<longleftrightarrow> (\<forall>i \<in> I. G(i) ok F)"
+lemma ok_JOIN_iff2 [iff]: "JOIN(I,G) ok F \<longleftrightarrow> (\<forall>i \<in> I. G(i) ok F)"
apply (auto elim!: not_emptyE simp add: ok_def)
apply (blast dest: Acts_type [THEN subsetD])
done
@@ -475,12 +468,12 @@
by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def)
lemma Allowed_Join [simp]:
- "Allowed(F Join G) =
+ "Allowed(F \<squnion> G) =
Allowed(programify(F)) \<inter> Allowed(programify(G))"
apply (auto simp add: Allowed_def)
done
-lemma Allowed_JN [simp]:
+lemma Allowed_JOIN [simp]:
"i \<in> I ==>
Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))"
apply (auto simp add: Allowed_def, blast)
--- a/src/ZF/UNITY/WFair.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/WFair.thy Sat Oct 10 22:02:23 2015 +0200
@@ -43,16 +43,13 @@
definition
(* The Visible version of the LEADS-TO relation*)
- leadsTo :: "[i, i] => i" (infixl "leadsTo" 60) where
- "A leadsTo B == {F \<in> program. <A,B>:leads(state, F)}"
+ leadsTo :: "[i, i] => i" (infixl "\<longmapsto>" 60) where
+ "A \<longmapsto> B == {F \<in> program. <A,B>:leads(state, F)}"
definition
(* wlt(F, B) is the largest set that leads to B*)
wlt :: "[i, i] => i" where
- "wlt(F, B) == \<Union>({A \<in> Pow(state). F \<in> A leadsTo B})"
-
-notation (xsymbols)
- leadsTo (infixl "\<longmapsto>" 60)
+ "wlt(F, B) == \<Union>({A \<in> Pow(state). F \<in> A \<longmapsto> B})"
(** Ad-hoc set-theory rules **)
@@ -163,17 +160,17 @@
lemmas leads_left = leads.dom_subset [THEN subsetD, THEN SigmaD1]
lemmas leads_right = leads.dom_subset [THEN subsetD, THEN SigmaD2]
-lemma leadsTo_type: "A leadsTo B \<subseteq> program"
+lemma leadsTo_type: "A \<longmapsto> B \<subseteq> program"
by (unfold leadsTo_def, auto)
lemma leadsToD2:
-"F \<in> A leadsTo B ==> F \<in> program & st_set(A) & st_set(B)"
+"F \<in> A \<longmapsto> B ==> F \<in> program & st_set(A) & st_set(B)"
apply (unfold leadsTo_def st_set_def)
apply (blast dest: leads_left leads_right)
done
lemma leadsTo_Basis:
- "[|F \<in> A ensures B; st_set(A); st_set(B)|] ==> F \<in> A leadsTo B"
+ "[|F \<in> A ensures B; st_set(A); st_set(B)|] ==> F \<in> A \<longmapsto> B"
apply (unfold leadsTo_def st_set_def)
apply (cut_tac ensures_type)
apply (auto intro: leads.Basis)
@@ -181,152 +178,152 @@
declare leadsTo_Basis [intro]
(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
-(* [| F \<in> program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *)
+(* [| F \<in> program; A<=B; st_set(A); st_set(B) |] ==> A \<longmapsto> B *)
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
-lemma leadsTo_Trans: "[|F \<in> A leadsTo B; F \<in> B leadsTo C |]==>F \<in> A leadsTo C"
+lemma leadsTo_Trans: "[|F \<in> A \<longmapsto> B; F \<in> B \<longmapsto> C |]==>F \<in> A \<longmapsto> C"
apply (unfold leadsTo_def)
apply (auto intro: leads.Trans)
done
(* Better when used in association with leadsTo_weaken_R *)
-lemma transient_imp_leadsTo: "F \<in> transient(A) ==> F \<in> A leadsTo (state-A)"
+lemma transient_imp_leadsTo: "F \<in> transient(A) ==> F \<in> A \<longmapsto> (state-A)"
apply (unfold transient_def)
apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI)
done
(*Useful with cancellation, disjunction*)
-lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
+lemma leadsTo_Un_duplicate: "F \<in> A \<longmapsto> (A' \<union> A') ==> F \<in> A \<longmapsto> A'"
by simp
lemma leadsTo_Un_duplicate2:
- "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
+ "F \<in> A \<longmapsto> (A' \<union> C \<union> C) ==> F \<in> A \<longmapsto> (A' \<union> C)"
by (simp add: Un_ac)
(*The Union introduction rule as we should have liked to state it*)
lemma leadsTo_Union:
- "[|!!A. A \<in> S ==> F \<in> A leadsTo B; F \<in> program; st_set(B)|]
- ==> F \<in> \<Union>(S) leadsTo B"
+ "[|!!A. A \<in> S ==> F \<in> A \<longmapsto> B; F \<in> program; st_set(B)|]
+ ==> F \<in> \<Union>(S) \<longmapsto> B"
apply (unfold leadsTo_def st_set_def)
apply (blast intro: leads.Union dest: leads_left)
done
lemma leadsTo_Union_Int:
- "[|!!A. A \<in> S ==>F \<in> (A \<inter> C) leadsTo B; F \<in> program; st_set(B)|]
- ==> F \<in> (\<Union>(S)Int C)leadsTo B"
+ "[|!!A. A \<in> S ==>F \<in> (A \<inter> C) \<longmapsto> B; F \<in> program; st_set(B)|]
+ ==> F \<in> (\<Union>(S)Int C)\<longmapsto> B"
apply (unfold leadsTo_def st_set_def)
apply (simp only: Int_Union_Union)
apply (blast dest: leads_left intro: leads.Union)
done
lemma leadsTo_UN:
- "[| !!i. i \<in> I ==> F \<in> A(i) leadsTo B; F \<in> program; st_set(B)|]
- ==> F:(\<Union>i \<in> I. A(i)) leadsTo B"
+ "[| !!i. i \<in> I ==> F \<in> A(i) \<longmapsto> B; F \<in> program; st_set(B)|]
+ ==> F:(\<Union>i \<in> I. A(i)) \<longmapsto> B"
apply (simp add: Int_Union_Union leadsTo_def st_set_def)
apply (blast dest: leads_left intro: leads.Union)
done
(* Binary union introduction rule *)
lemma leadsTo_Un:
- "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
+ "[| F \<in> A \<longmapsto> C; F \<in> B \<longmapsto> C |] ==> F \<in> (A \<union> B) \<longmapsto> C"
apply (subst Un_eq_Union)
apply (blast intro: leadsTo_Union dest: leadsToD2)
done
lemma single_leadsTo_I:
- "[|!!x. x \<in> A==> F:{x} leadsTo B; F \<in> program; st_set(B) |]
- ==> F \<in> A leadsTo B"
+ "[|!!x. x \<in> A==> F:{x} \<longmapsto> B; F \<in> program; st_set(B) |]
+ ==> F \<in> A \<longmapsto> B"
apply (rule_tac b = A in UN_singleton [THEN subst])
apply (rule leadsTo_UN, auto)
done
-lemma leadsTo_refl: "[| F \<in> program; st_set(A) |] ==> F \<in> A leadsTo A"
+lemma leadsTo_refl: "[| F \<in> program; st_set(A) |] ==> F \<in> A \<longmapsto> A"
by (blast intro: subset_imp_leadsTo)
-lemma leadsTo_refl_iff: "F \<in> A leadsTo A \<longleftrightarrow> F \<in> program & st_set(A)"
+lemma leadsTo_refl_iff: "F \<in> A \<longmapsto> A \<longleftrightarrow> F \<in> program & st_set(A)"
by (auto intro: leadsTo_refl dest: leadsToD2)
-lemma empty_leadsTo: "F \<in> 0 leadsTo B \<longleftrightarrow> (F \<in> program & st_set(B))"
+lemma empty_leadsTo: "F \<in> 0 \<longmapsto> B \<longleftrightarrow> (F \<in> program & st_set(B))"
by (auto intro: subset_imp_leadsTo dest: leadsToD2)
declare empty_leadsTo [iff]
-lemma leadsTo_state: "F \<in> A leadsTo state \<longleftrightarrow> (F \<in> program & st_set(A))"
+lemma leadsTo_state: "F \<in> A \<longmapsto> state \<longleftrightarrow> (F \<in> program & st_set(A))"
by (auto intro: subset_imp_leadsTo dest: leadsToD2 st_setD)
declare leadsTo_state [iff]
-lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B'; st_set(B') |] ==> F \<in> A leadsTo B'"
+lemma leadsTo_weaken_R: "[| F \<in> A \<longmapsto> A'; A'<=B'; st_set(B') |] ==> F \<in> A \<longmapsto> B'"
by (blast dest: leadsToD2 intro: subset_imp_leadsTo leadsTo_Trans)
-lemma leadsTo_weaken_L: "[| F \<in> A leadsTo A'; B<=A |] ==> F \<in> B leadsTo A'"
+lemma leadsTo_weaken_L: "[| F \<in> A \<longmapsto> A'; B<=A |] ==> F \<in> B \<longmapsto> A'"
apply (frule leadsToD2)
apply (blast intro: leadsTo_Trans subset_imp_leadsTo st_set_subset)
done
-lemma leadsTo_weaken: "[| F \<in> A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F \<in> B leadsTo B'"
+lemma leadsTo_weaken: "[| F \<in> A \<longmapsto> A'; B<=A; A'<=B'; st_set(B')|]==> F \<in> B \<longmapsto> B'"
apply (frule leadsToD2)
apply (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans leadsTo_refl)
done
(* This rule has a nicer conclusion *)
-lemma transient_imp_leadsTo2: "[| F \<in> transient(A); state-A<=B; st_set(B)|] ==> F \<in> A leadsTo B"
+lemma transient_imp_leadsTo2: "[| F \<in> transient(A); state-A<=B; st_set(B)|] ==> F \<in> A \<longmapsto> B"
apply (frule transientD2)
apply (rule leadsTo_weaken_R)
apply (auto simp add: transient_imp_leadsTo)
done
(*Distributes over binary unions*)
-lemma leadsTo_Un_distrib: "F:(A \<union> B) leadsTo C \<longleftrightarrow> (F \<in> A leadsTo C & F \<in> B leadsTo C)"
+lemma leadsTo_Un_distrib: "F:(A \<union> B) \<longmapsto> C \<longleftrightarrow> (F \<in> A \<longmapsto> C & F \<in> B \<longmapsto> C)"
by (blast intro: leadsTo_Un leadsTo_weaken_L)
lemma leadsTo_UN_distrib:
-"(F:(\<Union>i \<in> I. A(i)) leadsTo B)\<longleftrightarrow> ((\<forall>i \<in> I. F \<in> A(i) leadsTo B) & F \<in> program & st_set(B))"
+"(F:(\<Union>i \<in> I. A(i)) \<longmapsto> B)\<longleftrightarrow> ((\<forall>i \<in> I. F \<in> A(i) \<longmapsto> B) & F \<in> program & st_set(B))"
apply (blast dest: leadsToD2 intro: leadsTo_UN leadsTo_weaken_L)
done
-lemma leadsTo_Union_distrib: "(F \<in> \<Union>(S) leadsTo B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A leadsTo B) & F \<in> program & st_set(B)"
+lemma leadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto> B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A \<longmapsto> B) & F \<in> program & st_set(B)"
by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)
text\<open>Set difference: maybe combine with @{text leadsTo_weaken_L}??\<close>
lemma leadsTo_Diff:
- "[| F: (A-B) leadsTo C; F \<in> B leadsTo C; st_set(C) |]
- ==> F \<in> A leadsTo C"
+ "[| F: (A-B) \<longmapsto> C; F \<in> B \<longmapsto> C; st_set(C) |]
+ ==> F \<in> A \<longmapsto> C"
by (blast intro: leadsTo_Un leadsTo_weaken dest: leadsToD2)
lemma leadsTo_UN_UN:
- "[|!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i); F \<in> program |]
- ==> F: (\<Union>i \<in> I. A(i)) leadsTo (\<Union>i \<in> I. A'(i))"
+ "[|!!i. i \<in> I ==> F \<in> A(i) \<longmapsto> A'(i); F \<in> program |]
+ ==> F: (\<Union>i \<in> I. A(i)) \<longmapsto> (\<Union>i \<in> I. A'(i))"
apply (rule leadsTo_Union)
apply (auto intro: leadsTo_weaken_R dest: leadsToD2)
done
(*Binary union version*)
-lemma leadsTo_Un_Un: "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |] ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
+lemma leadsTo_Un_Un: "[| F \<in> A \<longmapsto> A'; F \<in> B \<longmapsto> B' |] ==> F \<in> (A \<union> B) \<longmapsto> (A' \<union> B')"
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') ")
prefer 2 apply (blast dest: leadsToD2)
apply (blast intro: leadsTo_Un leadsTo_weaken_R)
done
(** The cancellation law **)
-lemma leadsTo_cancel2: "[|F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B'|] ==> F \<in> A leadsTo (A' \<union> B')"
+lemma leadsTo_cancel2: "[|F \<in> A \<longmapsto> (A' \<union> B); F \<in> B \<longmapsto> B'|] ==> F \<in> A \<longmapsto> (A' \<union> B')"
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') &F \<in> program")
prefer 2 apply (blast dest: leadsToD2)
apply (blast intro: leadsTo_Trans leadsTo_Un_Un leadsTo_refl)
done
-lemma leadsTo_cancel_Diff2: "[|F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B'|]==> F \<in> A leadsTo (A' \<union> B')"
+lemma leadsTo_cancel_Diff2: "[|F \<in> A \<longmapsto> (A' \<union> B); F \<in> (B-A') \<longmapsto> B'|]==> F \<in> A \<longmapsto> (A' \<union> B')"
apply (rule leadsTo_cancel2)
prefer 2 apply assumption
apply (blast dest: leadsToD2 intro: leadsTo_weaken_R)
done
-lemma leadsTo_cancel1: "[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |] ==> F \<in> A leadsTo (B' \<union> A')"
+lemma leadsTo_cancel1: "[| F \<in> A \<longmapsto> (B \<union> A'); F \<in> B \<longmapsto> B' |] ==> F \<in> A \<longmapsto> (B' \<union> A')"
apply (simp add: Un_commute)
apply (blast intro!: leadsTo_cancel2)
done
lemma leadsTo_cancel_Diff1:
- "[|F \<in> A leadsTo (B \<union> A'); F: (B-A') leadsTo B'|]==> F \<in> A leadsTo (B' \<union> A')"
+ "[|F \<in> A \<longmapsto> (B \<union> A'); F: (B-A') \<longmapsto> B'|]==> F \<in> A \<longmapsto> (B' \<union> A')"
apply (rule leadsTo_cancel1)
prefer 2 apply assumption
apply (blast intro: leadsTo_weaken_R dest: leadsToD2)
@@ -334,11 +331,11 @@
(*The INDUCTION rule as we should have liked to state it*)
lemma leadsTo_induct:
- assumes major: "F \<in> za leadsTo zb"
+ assumes major: "F \<in> za \<longmapsto> zb"
and basis: "!!A B. [|F \<in> A ensures B; st_set(A); st_set(B)|] ==> P(A,B)"
- and trans: "!!A B C. [| F \<in> A leadsTo B; P(A, B);
- F \<in> B leadsTo C; P(B, C) |] ==> P(A,C)"
- and union: "!!B S. [| \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);
+ and trans: "!!A B C. [| F \<in> A \<longmapsto> B; P(A, B);
+ F \<in> B \<longmapsto> C; P(B, C) |] ==> P(A,C)"
+ and union: "!!B S. [| \<forall>A \<in> S. F \<in> A \<longmapsto> B; \<forall>A \<in> S. P(A,B);
st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(\<Union>(S), B)"
shows "P(za, zb)"
apply (cut_tac major)
@@ -352,13 +349,13 @@
(* Added by Sidi, an induction rule without ensures *)
lemma leadsTo_induct2:
- assumes major: "F \<in> za leadsTo zb"
+ assumes major: "F \<in> za \<longmapsto> zb"
and basis1: "!!A B. [| A<=B; st_set(B) |] ==> P(A, B)"
and basis2: "!!A B. [| F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) |]
==> P(A, B)"
- and trans: "!!A B C. [| F \<in> A leadsTo B; P(A, B);
- F \<in> B leadsTo C; P(B, C) |] ==> P(A,C)"
- and union: "!!B S. [| \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);
+ and trans: "!!A B C. [| F \<in> A \<longmapsto> B; P(A, B);
+ F \<in> B \<longmapsto> C; P(B, C) |] ==> P(A,C)"
+ and union: "!!B S. [| \<forall>A \<in> S. F \<in> A \<longmapsto> B; \<forall>A \<in> S. P(A,B);
st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(\<Union>(S), B)"
shows "P(za, zb)"
apply (cut_tac major)
@@ -382,7 +379,7 @@
(** Variant induction rule: on the preconditions for B **)
(*Lemma is the weak version: can't see how to do it in one step*)
lemma leadsTo_induct_pre_aux:
- "[| F \<in> za leadsTo zb;
+ "[| F \<in> za \<longmapsto> zb;
P(zb);
!!A B. [| F \<in> A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A);
!!S. [| \<forall>A \<in> S. P(A); \<forall>A \<in> S. st_set(A) |] ==> P(\<Union>(S))
@@ -397,12 +394,12 @@
lemma leadsTo_induct_pre:
- "[| F \<in> za leadsTo zb;
+ "[| F \<in> za \<longmapsto> zb;
P(zb);
- !!A B. [| F \<in> A ensures B; F \<in> B leadsTo zb; P(B); st_set(A) |] ==> P(A);
- !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P(A) & st_set(A) ==> P(\<Union>(S))
+ !!A B. [| F \<in> A ensures B; F \<in> B \<longmapsto> zb; P(B); st_set(A) |] ==> P(A);
+ !!S. \<forall>A \<in> S. F \<in> A \<longmapsto> zb & P(A) & st_set(A) ==> P(\<Union>(S))
|] ==> P(za)"
-apply (subgoal_tac " (F \<in> za leadsTo zb) & P (za) ")
+apply (subgoal_tac " (F \<in> za \<longmapsto> zb) & P (za) ")
apply (erule conjunct2)
apply (frule leadsToD2)
apply (erule leadsTo_induct_pre_aux)
@@ -413,7 +410,7 @@
(** The impossibility law **)
lemma leadsTo_empty:
- "F \<in> A leadsTo 0 ==> A=0"
+ "F \<in> A \<longmapsto> 0 ==> A=0"
apply (erule leadsTo_induct_pre)
apply (auto simp add: ensures_def constrains_def transient_def st_set_def)
apply (drule bspec, assumption)+
@@ -426,7 +423,7 @@
text\<open>Special case of PSP: Misra's "stable conjunction"\<close>
lemma psp_stable:
- "[| F \<in> A leadsTo A'; F \<in> stable(B) |] ==> F:(A \<inter> B) leadsTo (A' \<inter> B)"
+ "[| F \<in> A \<longmapsto> A'; F \<in> stable(B) |] ==> F:(A \<inter> B) \<longmapsto> (A' \<inter> B)"
apply (unfold stable_def)
apply (frule leadsToD2)
apply (erule leadsTo_induct)
@@ -438,7 +435,7 @@
done
-lemma psp_stable2: "[|F \<in> A leadsTo A'; F \<in> stable(B) |]==>F: (B \<inter> A) leadsTo (B \<inter> A')"
+lemma psp_stable2: "[|F \<in> A \<longmapsto> A'; F \<in> stable(B) |]==>F: (B \<inter> A) \<longmapsto> (B \<inter> A')"
apply (simp (no_asm_simp) add: psp_stable Int_ac)
done
@@ -451,7 +448,7 @@
done
lemma psp:
-"[|F \<in> A leadsTo A'; F \<in> B co B'; st_set(B')|]==> F:(A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
+"[|F \<in> A \<longmapsto> A'; F \<in> B co B'; st_set(B')|]==> F:(A \<inter> B') \<longmapsto> ((A' \<inter> B) \<union> (B' - B))"
apply (subgoal_tac "F \<in> program & st_set (A) & st_set (A') & st_set (B) ")
prefer 2 apply (blast dest!: constrainsD2 leadsToD2)
apply (erule leadsTo_induct)
@@ -466,13 +463,13 @@
done
-lemma psp2: "[| F \<in> A leadsTo A'; F \<in> B co B'; st_set(B') |]
- ==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))"
+lemma psp2: "[| F \<in> A \<longmapsto> A'; F \<in> B co B'; st_set(B') |]
+ ==> F \<in> (B' \<inter> A) \<longmapsto> ((B \<inter> A') \<union> (B' - B))"
by (simp (no_asm_simp) add: psp Int_ac)
lemma psp_unless:
- "[| F \<in> A leadsTo A'; F \<in> B unless B'; st_set(B); st_set(B') |]
- ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')"
+ "[| F \<in> A \<longmapsto> A'; F \<in> B unless B'; st_set(B); st_set(B') |]
+ ==> F \<in> (A \<inter> B) \<longmapsto> ((A' \<inter> B) \<union> B')"
apply (unfold unless_def)
apply (subgoal_tac "st_set (A) &st_set (A') ")
prefer 2 apply (blast dest: leadsToD2)
@@ -488,11 +485,11 @@
m \<in> I;
field(r)<=I;
F \<in> program; st_set(B);
- \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) leadsTo
+ \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto>
((A \<inter> f-``(converse(r)``{m})) \<union> B) |]
- ==> F \<in> (A \<inter> f-``{m}) leadsTo B"
+ ==> F \<in> (A \<inter> f-``{m}) \<longmapsto> B"
apply (erule_tac a = m in wf_induct2, simp_all)
-apply (subgoal_tac "F \<in> (A \<inter> (f-`` (converse (r) ``{x}))) leadsTo B")
+apply (subgoal_tac "F \<in> (A \<inter> (f-`` (converse (r) ``{x}))) \<longmapsto> B")
apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
apply (subst vimage_eq_UN)
apply (simp del: UN_simps add: Int_UN_distrib)
@@ -504,9 +501,9 @@
field(r)<=I;
A<=f-``I;
F \<in> program; st_set(A); st_set(B);
- \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) leadsTo
+ \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto>
((A \<inter> f-``(converse(r)``{m})) \<union> B) |]
- ==> F \<in> A leadsTo B"
+ ==> F \<in> A \<longmapsto> B"
apply (rule_tac b = A in subst)
defer 1
apply (rule_tac I = I in leadsTo_UN)
@@ -535,12 +532,12 @@
apply (blast intro: lt_trans)
done
-(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
+(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) \<longmapsto> B*)
lemma lessThan_induct:
"[| A<=f-``nat;
F \<in> program; st_set(A); st_set(B);
- \<forall>m \<in> nat. F:(A \<inter> f-``{m}) leadsTo ((A \<inter> f -`` m) \<union> B) |]
- ==> F \<in> A leadsTo B"
+ \<forall>m \<in> nat. F:(A \<inter> f-``{m}) \<longmapsto> ((A \<inter> f -`` m) \<union> B) |]
+ ==> F \<in> A \<longmapsto> B"
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN leadsTo_wf_induct])
apply (simp_all add: nat_measure_field)
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
@@ -559,22 +556,22 @@
done
declare wlt_st_set [iff]
-lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) leadsTo B \<longleftrightarrow> (F \<in> program & st_set(B))"
+lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) \<longmapsto> B \<longleftrightarrow> (F \<in> program & st_set(B))"
apply (unfold wlt_def)
apply (blast dest: leadsToD2 intro!: leadsTo_Union)
done
-(* [| F \<in> program; st_set(B) |] ==> F \<in> wlt(F, B) leadsTo B *)
+(* [| F \<in> program; st_set(B) |] ==> F \<in> wlt(F, B) \<longmapsto> B *)
lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]
-lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt(F, B)"
+lemma leadsTo_subset: "F \<in> A \<longmapsto> B ==> A \<subseteq> wlt(F, B)"
apply (unfold wlt_def)
apply (frule leadsToD2)
apply (auto simp add: st_set_def)
done
(*Misra's property W2*)
-lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B \<longleftrightarrow> (A \<subseteq> wlt(F,B) & F \<in> program & st_set(B))"
+lemma leadsTo_eq_subset_wlt: "F \<in> A \<longmapsto> B \<longleftrightarrow> (A \<subseteq> wlt(F,B) & F \<in> program & st_set(B))"
apply auto
apply (blast dest: leadsToD2 leadsTo_subset intro: leadsTo_weaken_L wlt_leadsTo)+
done
@@ -596,8 +593,8 @@
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
(* slightly different from the HOL one \<in> B here is bounded *)
-lemma leadsTo_123: "F \<in> A leadsTo A'
- ==> \<exists>B \<in> Pow(state). A<=B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
+lemma leadsTo_123: "F \<in> A \<longmapsto> A'
+ ==> \<exists>B \<in> Pow(state). A<=B & F \<in> B \<longmapsto> A' & F \<in> (B-A') co (B \<union> A')"
apply (frule leadsToD2)
apply (erule leadsTo_induct)
txt\<open>Basis\<close>
@@ -608,7 +605,7 @@
apply (blast intro: leadsTo_123_aux leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate, blast)
txt\<open>Union\<close>
apply (clarify dest!: ball_conj_distrib [THEN iffD1])
-apply (subgoal_tac "\<exists>y. y \<in> Pi (S, %A. {Ba \<in> Pow (state) . A<=Ba & F \<in> Ba leadsTo B & F \<in> Ba - B co Ba \<union> B}) ")
+apply (subgoal_tac "\<exists>y. y \<in> Pi (S, %A. {Ba \<in> Pow (state) . A<=Ba & F \<in> Ba \<longmapsto> B & F \<in> Ba - B co Ba \<union> B}) ")
defer 1
apply (rule AC_ball_Pi, safe)
apply (rotate_tac 1)
@@ -634,9 +631,9 @@
subsection\<open>Completion: Binary and General Finite versions\<close>
lemma completion_aux: "[| W = wlt(F, (B' \<union> C));
- F \<in> A leadsTo (A' \<union> C); F \<in> A' co (A' \<union> C);
- F \<in> B leadsTo (B' \<union> C); F \<in> B' co (B' \<union> C) |]
- ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)"
+ F \<in> A \<longmapsto> (A' \<union> C); F \<in> A' co (A' \<union> C);
+ F \<in> B \<longmapsto> (B' \<union> C); F \<in> B' co (B' \<union> C) |]
+ ==> F \<in> (A \<inter> B) \<longmapsto> ((A' \<inter> B') \<union> C)"
apply (subgoal_tac "st_set (C) &st_set (W) &st_set (W-C) &st_set (A') &st_set (A) & st_set (B) & st_set (B') & F \<in> program")
prefer 2
apply simp
@@ -647,10 +644,10 @@
apply (subgoal_tac "F \<in> (W-C) co W")
prefer 2
apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]] Un_assoc)
-apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ")
+apply (subgoal_tac "F \<in> (A \<inter> W - C) \<longmapsto> (A' \<inter> W \<union> C) ")
prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
(** step 13 **)
-apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ")
+apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) \<longmapsto> (A' \<inter> B' \<union> C) ")
apply (drule leadsTo_Diff)
apply (blast intro: subset_imp_leadsTo dest: leadsToD2 constrainsD2)
apply (force simp add: st_set_def)
@@ -669,9 +666,9 @@
lemma finite_completion_aux:
"[| I \<in> Fin(X); F \<in> program; st_set(C) |] ==>
- (\<forall>i \<in> I. F \<in> (A(i)) leadsTo (A'(i) \<union> C)) \<longrightarrow>
+ (\<forall>i \<in> I. F \<in> (A(i)) \<longmapsto> (A'(i) \<union> C)) \<longrightarrow>
(\<forall>i \<in> I. F \<in> (A'(i)) co (A'(i) \<union> C)) \<longrightarrow>
- F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
+ F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> ((\<Inter>i \<in> I. A'(i)) \<union> C)"
apply (erule Fin_induct)
apply (auto simp add: Inter_0)
apply (rule completion)
@@ -681,15 +678,15 @@
lemma finite_completion:
"[| I \<in> Fin(X);
- !!i. i \<in> I ==> F \<in> A(i) leadsTo (A'(i) \<union> C);
+ !!i. i \<in> I ==> F \<in> A(i) \<longmapsto> (A'(i) \<union> C);
!!i. i \<in> I ==> F \<in> A'(i) co (A'(i) \<union> C); F \<in> program; st_set(C)|]
- ==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> ((\<Inter>i \<in> I. A'(i)) \<union> C)"
by (blast intro: finite_completion_aux [THEN mp, THEN mp])
lemma stable_completion:
- "[| F \<in> A leadsTo A'; F \<in> stable(A');
- F \<in> B leadsTo B'; F \<in> stable(B') |]
- ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')"
+ "[| F \<in> A \<longmapsto> A'; F \<in> stable(A');
+ F \<in> B \<longmapsto> B'; F \<in> stable(B') |]
+ ==> F \<in> (A \<inter> B) \<longmapsto> (A' \<inter> B')"
apply (unfold stable_def)
apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)
apply (blast dest: leadsToD2)
@@ -698,9 +695,9 @@
lemma finite_stable_completion:
"[| I \<in> Fin(X);
- (!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i));
+ (!!i. i \<in> I ==> F \<in> A(i) \<longmapsto> A'(i));
(!!i. i \<in> I ==> F \<in> stable(A'(i))); F \<in> program |]
- ==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo (\<Inter>i \<in> I. A'(i))"
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> (\<Inter>i \<in> I. A'(i))"
apply (unfold stable_def)
apply (subgoal_tac "st_set (\<Inter>i \<in> I. A' (i))")
prefer 2 apply (blast dest: leadsToD2)