# HG changeset patch
# User wenzelm
# Date 1444507343 -7200
# Node ID 331be2820f902cd19bac42babe4288ff468e6eb0
# Parent  2332d9be352b0c33abce4959dde3ab5ac835ea8f
tuned syntax -- more symbols;

diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/AllocImpl.thy
--- 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)
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/ClientImpl.thy
--- 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
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/Comp.thy
--- 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
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/Follows.thy
--- 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:
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/Guar.thy
--- 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')
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/Mutex.thy
--- 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)
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/SubstAx.thy
--- 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)
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/UNITY.thy
--- 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 *)
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/Union.thy
--- 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)
diff -r 2332d9be352b -r 331be2820f90 src/ZF/UNITY/WFair.thy
--- 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)