# HG changeset patch
# User wenzelm
# Date 1191764965 -7200
# Node ID c663e675e1773831d4aa85363b2ef42073ce1f70
# Parent  df3581710b9bab972f0c2803f5f4b673c025eb8b
replaced some 'translations' by 'abbreviation';

diff -r df3581710b9b -r c663e675e177 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Bool.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -9,13 +9,13 @@
 
 theory Bool imports pair begin
 
-syntax
-    "1"         :: i             ("1")
-    "2"         :: i             ("2")
+abbreviation
+  one  ("1") where
+  "1 == succ(0)"
 
-translations
-   "1"  == "succ(0)"
-   "2"  == "succ(1)"
+abbreviation
+  two  ("2") where
+  "2 == succ(1)"
 
 text{*2 is equal to bool, but is used as a number rather than a type.*}
 
@@ -60,7 +60,7 @@
 
 lemma boolE:
     "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P"
-by (simp add: bool_defs, blast)  
+by (simp add: bool_defs, blast)
 
 (** cond **)
 
@@ -134,7 +134,7 @@
 lemma and_assoc: "a: bool ==> (a and b) and c  =  a and (b and c)"
 by (elim boolE, auto)
 
-lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>  
+lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
        (a or b) and c  =  (a and c) or (b and c)"
 by (elim boolE, auto)
 
@@ -149,7 +149,7 @@
 lemma or_assoc: "a: bool ==> (a or b) or c  =  a or (b or c)"
 by (elim boolE, auto)
 
-lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>  
+lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
            (a and b) or c  =  (a or c) and (b or c)"
 by (elim boolE, auto)
 
@@ -158,19 +158,19 @@
    "bool_of_o(P) == (if P then 1 else 0)"
 
 lemma [simp]: "bool_of_o(True) = 1"
-by (simp add: bool_of_o_def) 
+by (simp add: bool_of_o_def)
 
 lemma [simp]: "bool_of_o(False) = 0"
-by (simp add: bool_of_o_def) 
+by (simp add: bool_of_o_def)
 
 lemma [simp,TC]: "bool_of_o(P) \<in> bool"
-by (simp add: bool_of_o_def) 
+by (simp add: bool_of_o_def)
 
 lemma [simp]: "(bool_of_o(P) = 1) <-> P"
-by (simp add: bool_of_o_def) 
+by (simp add: bool_of_o_def)
 
 lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
-by (simp add: bool_of_o_def) 
+by (simp add: bool_of_o_def)
 
 ML
 {*
diff -r df3581710b9b -r c663e675e177 src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/EquivClass.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -21,14 +21,15 @@
       "congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
            <y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
 
-syntax
-  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80)
-  RESPECTS2 ::"[i=>i, i] => o"  (infixr "respects2 " 80)
+abbreviation
+  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80) where
+  "f respects r == congruent(r,f)"
+
+abbreviation
+  RESPECTS2 ::"[i=>i=>i, i] => o"  (infixr "respects2 " 80) where
+  "f respects2 r == congruent2(r,r,f)"
     --{*Abbreviation for the common case where the relations are identical*}
 
-translations
-  "f respects r" == "congruent(r,f)"
-  "f respects2 r" => "congruent2(r,r,f)"
 
 subsection{*Suppes, Theorem 70:
     @{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}
diff -r df3581710b9b -r c663e675e177 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Induct/Multiset.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -12,11 +12,10 @@
 imports FoldSet Acc
 begin
 
-consts
-  (* Short cut for multiset space *)
-  Mult :: "i=>i"
-translations
-  "Mult(A)" => "A -||> nat-{0}"
+abbreviation (input)
+  -- {* Short cut for multiset space *}
+  Mult :: "i=>i" where
+  "Mult(A) == A -||> nat-{0}"
 
 constdefs
 
@@ -64,15 +63,15 @@
   msize :: "i => i"
   "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"
 
+abbreviation
+  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)  where
+  "a :# M == a \<in> mset_of(M)"
+
 syntax
-  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)
   "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
-
 syntax (xsymbols)
   "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
-
 translations
-  "a :# M" == "a \<in> mset_of(M)"
   "{#x \<in> M. P#}" == "MCollect(M, %x. P)"
 
   (* multiset orderings *)
diff -r df3581710b9b -r c663e675e177 src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Induct/Primrec.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -42,10 +42,9 @@
   "ACK(0) = SC"
   "ACK(succ(i)) = PREC (CONSTANT (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"
 
-syntax
-  ack :: "[i,i]=>i"
-translations
-  "ack(x,y)" == "ACK(x) ` [y]"
+abbreviation
+  ack :: "[i,i]=>i" where
+  "ack(x,y) == ACK(x) ` [y]"
 
 
 text {*
diff -r df3581710b9b -r c663e675e177 src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Resid/Reduction.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -12,10 +12,10 @@
 consts
   lambda        :: "i"
   unmark        :: "i=>i"
-  Apl           :: "[i,i]=>i"
 
-translations
-  "Apl(n,m)" == "App(0,n,m)"
+abbreviation
+  Apl :: "[i,i]=>i" where
+  "Apl(n,m) == App(0,n,m)"
   
 inductive
   domains       "lambda" <= redexes
diff -r df3581710b9b -r c663e675e177 src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Resid/Substitution.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -7,27 +7,11 @@
 
 theory Substitution imports Redex begin
 
-consts
-  lift_aux      :: "i=>i"
-  lift          :: "i=>i"
-  subst_aux     :: "i=>i"
-  subst         :: "[i,i]=>i"  (infixl "'/" 70)
-
-constdefs
-  lift_rec      :: "[i,i]=> i"
-    "lift_rec(r,k) == lift_aux(r)`k"
-
-  subst_rec     :: "[i,i,i]=> i"	(**NOTE THE ARGUMENT ORDER BELOW**)
-    "subst_rec(u,r,k) == subst_aux(r)`u`k"
-
-translations
-  "lift(r)"  == "lift_rec(r,0)"
-  "u/v"      == "subst_rec(u,v,0)"
-  
-
 (** The clumsy _aux functions are required because other arguments vary
     in the recursive calls ***)
 
+consts
+  lift_aux      :: "i=>i"
 primrec
   "lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))"
 
@@ -35,18 +19,36 @@
 
   "lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
 
+constdefs
+  lift_rec      :: "[i,i]=> i"
+    "lift_rec(r,k) == lift_aux(r)`k"
 
-  
+abbreviation
+  lift :: "i=>i" where
+  "lift(r) == lift_rec(r,0)"
+
+
+consts
+  subst_aux     :: "i=>i"
 primrec
   "subst_aux(Var(i)) =
-     (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1) 
+     (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1)
 				else if k=i then r else Var(i))"
   "subst_aux(Fun(t)) =
      (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
 
-  "subst_aux(App(b,f,a)) = 
+  "subst_aux(App(b,f,a)) =
      (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
 
+constdefs
+  subst_rec     :: "[i,i,i]=> i"	(**NOTE THE ARGUMENT ORDER BELOW**)
+    "subst_rec(u,r,k) == subst_aux(r)`u`k"
+
+abbreviation
+  subst :: "[i,i]=>i"  (infixl "'/" 70)  where
+  "u/v == subst_rec(u,v,0)"
+
+
 
 (* ------------------------------------------------------------------------- *)
 (*   Arithmetic extensions                                                   *)
@@ -100,8 +102,8 @@
 (* ------------------------------------------------------------------------- *)
 
 lemma subst_Var:
-     "[|k \<in> nat; u \<in> redexes|]   
-      ==> subst_rec(u,Var(i),k) =   
+     "[|k \<in> nat; u \<in> redexes|]
+      ==> subst_rec(u,Var(i),k) =
           (if k<i then Var(i #- 1) else if k=i then u else Var(i))"
 by (simp add: subst_rec_def gt_not_eq leI)
 
@@ -148,8 +150,8 @@
 
 (*The i\<in>nat is redundant*)
 lemma lift_lift_rec [rule_format]:
-     "u \<in> redexes 
-      ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->    
+     "u \<in> redexes
+      ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->
            (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
 apply (erule redexes.induct, auto)
 apply (case_tac "n < i")
@@ -158,7 +160,7 @@
 done
 
 lemma lift_lift:
-     "[|u \<in> redexes; n \<in> nat|] 
+     "[|u \<in> redexes; n \<in> nat|]
       ==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
 by (simp add: lift_lift_rec)
 
@@ -166,13 +168,13 @@
 by (erule natE, auto)
 
 lemma lift_rec_subst_rec [rule_format]:
-     "v \<in> redexes ==>   
-       \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m--> 
-          lift_rec(subst_rec(u,v,n),m) =  
+     "v \<in> redexes ==>
+       \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m-->
+          lift_rec(subst_rec(u,v,n),m) =
                subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
 apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
 apply safe
-apply (rename_tac n n' m u) 
+apply (rename_tac n n' m u)
 apply (case_tac "n < n'")
  apply (frule_tac j = n' in lt_trans2, assumption)
  apply (simp add: leI, simp)
@@ -182,19 +184,19 @@
 
 
 lemma lift_subst:
-     "[|v \<in> redexes; u \<in> redexes; n \<in> nat|] 
+     "[|v \<in> redexes; u \<in> redexes; n \<in> nat|]
       ==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
 by (simp add: lift_rec_subst_rec)
 
 
 lemma lift_rec_subst_rec_lt [rule_format]:
-     "v \<in> redexes ==>   
-       \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n--> 
-          lift_rec(subst_rec(u,v,n),m) =  
+     "v \<in> redexes ==>
+       \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n-->
+          lift_rec(subst_rec(u,v,n),m) =
                subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
 apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
 apply safe
-apply (rename_tac n n' m u) 
+apply (rename_tac n n' m u)
 apply (case_tac "n < n'")
 apply (case_tac "n < m")
 apply (simp_all add: leI)
@@ -205,20 +207,20 @@
 
 
 lemma subst_rec_lift_rec [rule_format]:
-     "u \<in> redexes ==>   
+     "u \<in> redexes ==>
         \<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
 apply (erule redexes.induct, auto)
 apply (case_tac "n < na", auto)
 done
 
 lemma subst_rec_subst_rec [rule_format]:
-     "v \<in> redexes ==>   
-        \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->  
-	  subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) = 
+     "v \<in> redexes ==>
+        \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->
+	  subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) =
 	  subst_rec(w,subst_rec(u,v,m),n)"
 apply (erule redexes.induct)
 apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt, safe)
-apply (rename_tac n' u w) 
+apply (rename_tac n' u w)
 apply (case_tac "n \<le> succ(n') ")
  apply (erule_tac i = n in leE)
  apply (simp_all add: succ_pred subst_rec_lift_rec leI)
@@ -231,7 +233,7 @@
 apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans], assumption)
 apply (erule leE)
  apply (frule succ_leI [THEN lt_trans], assumption)
- apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans], 
+ apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans],
         assumption)
  apply (simp_all add: succ_pred lt_pred)
 done
@@ -254,9 +256,9 @@
 by (erule Scomp.induct, simp_all add: comp_refl)
 
 lemma subst_rec_preserve_comp [rule_format, simp]:
-     "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes. 
+     "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes.
                   u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
-by (erule Scomp.induct, 
+by (erule Scomp.induct,
     simp_all add: subst_Var lift_rec_preserve_comp comp_refl)
 
 lemma lift_rec_preserve_reg [simp]:
@@ -264,7 +266,7 @@
 by (erule Sreg.induct, simp_all add: lift_rec_Var)
 
 lemma subst_rec_preserve_reg [simp]:
-     "regular(v) ==>   
+     "regular(v) ==>
         \<forall>m \<in> nat. \<forall>u \<in> redexes. regular(u)-->regular(subst_rec(u,v,m))"
 by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
 
diff -r df3581710b9b -r c663e675e177 src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/AllocBase.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -10,11 +10,13 @@
 theory AllocBase imports Follows MultisetSum Guar begin
 
 consts
-  tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
   NbT      :: i  (* Number of tokens in system *)
   Nclients :: i  (* Number of clients *)
 
-translations "tokbag" => "nat" 
+abbreviation (input)
+  tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
+where
+  "tokbag == nat"
 
 axioms
   NbT_pos:      "NbT \<in> nat-{0}"
diff -r df3581710b9b -r c663e675e177 src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -9,14 +9,13 @@
 
 theory AllocImpl imports ClientImpl begin
 
-consts
+abbreviation
+  NbR :: i            (*number of consumed messages*)  where
+  "NbR == Var([succ(2)])"
 
-  NbR :: i            (*number of consumed messages*)
-  available_tok :: i  (*number of free tokens (T in paper)*)
-
-translations
-  "NbR" == "Var([succ(2)])"
-  "available_tok" == "Var([succ(succ(2))])"
+abbreviation
+  available_tok :: i  (*number of free tokens (T in paper)*)  where
+  "available_tok == Var([succ(succ(2))])"
 
 axioms
   alloc_type_assumes [simp]:
diff -r df3581710b9b -r c663e675e177 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -6,20 +6,12 @@
 Distributed Resource Management System:  Client Implementation
 *)
 
-
 theory ClientImpl imports AllocBase Guar begin
 
-consts
-  ask :: i (* input history:  tokens requested *)
-  giv :: i (* output history: tokens granted *)
-  rel :: i (* input history: tokens released *)
-  tok :: i (* the number of available tokens *)
-
-translations
-  "ask" == "Var(Nil)"
-  "giv" == "Var([0])"
-  "rel" == "Var([1])"
-  "tok" == "Var([2])"
+abbreviation "ask == Var(Nil)" (* input history:  tokens requested *)
+abbreviation "giv == Var([0])" (* output history: tokens granted *)
+abbreviation "rel == Var([1])" (* input history: tokens released *)
+abbreviation "tok == Var([2])" (* the number of available tokens *)
 
 axioms
   type_assumes:
diff -r df3581710b9b -r c663e675e177 src/ZF/UNITY/Follows.thy
--- a/src/ZF/UNITY/Follows.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/Follows.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -12,60 +12,64 @@
 
 constdefs
   Follows :: "[i, i, i=>i, i=>i] => i"
-  "Follows(A, r, f, g) == 
+  "Follows(A, r, f, g) ==
             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})"
-consts
-  Incr :: "[i=>i]=>i"   
-  n_Incr :: "[i=>i]=>i"
-  m_Incr :: "[i=>i]=>i"
-  s_Incr :: "[i=>i]=>i"
-  n_Fols :: "[i=>i, i=>i]=>i"   (infixl "n'_Fols" 65)
+
+abbreviation
+  Incr :: "[i=>i]=>i" where
+  "Incr(f) == Increasing(list(nat), prefix(nat), f)"
 
-syntax
-  Follows' :: "[i=>i, i=>i, i, i] => i"
-        ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)
+abbreviation
+  n_Incr :: "[i=>i]=>i" where
+  "n_Incr(f) == Increasing(nat, Le, f)"
+
+abbreviation
+  s_Incr :: "[i=>i]=>i" where
+  "s_Incr(f) == Increasing(Pow(nat), SetLe(nat), f)"
 
-  
-translations
-  "Incr(f)" == "Increasing(list(nat), prefix(nat), f)"
-  "n_Incr(f)" == "Increasing(nat, Le, f)"
-  "s_Incr(f)" == "Increasing(Pow(nat), SetLe(nat), f)"
-  "m_Incr(f)" == "Increasing(Mult(nat), MultLe(nat, Le), f)"
-  
-  "f n_Fols g" == "Follows(nat, Le, f, g)"
+abbreviation
+  m_Incr :: "[i=>i]=>i" where
+  "m_Incr(f) == Increasing(Mult(nat), MultLe(nat, Le), f)"
 
-  "Follows'(f,g,r,A)" == "Follows(A,r,f,g)"
+abbreviation
+  n_Fols :: "[i=>i, i=>i]=>i"   (infixl "n'_Fols" 65)  where
+  "f n_Fols g == Follows(nat, Le, f, g)"
+
+abbreviation
+  Follows' :: "[i=>i, i=>i, i, i] => i"
+        ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)  where
+  "f Fols g Wrt r/A == Follows(A,r,f,g)"
 
 
 (*Does this hold for "invariant"?*)
 
-lemma Follows_cong: 
+lemma Follows_cong:
      "[|A=A'; r=r'; !!x. x \<in> state ==> f(x)=f'(x); !!x. x \<in> state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')"
 by (simp add: Increasing_def Follows_def)
 
 
-lemma subset_Always_comp: 
-"[| mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>  
+lemma subset_Always_comp:
+"[| mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
    Always({x \<in> state. <f(x), g(x)> \<in> r})<=Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
 apply (unfold mono1_def metacomp_def)
 apply (auto simp add: Always_eq_includes_reachable)
 done
 
-lemma imp_Always_comp: 
-"[| F \<in> Always({x \<in> state. <f(x), g(x)> \<in> r});  
-    mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>  
+lemma imp_Always_comp:
+"[| F \<in> Always({x \<in> state. <f(x), g(x)> \<in> r});
+    mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>
     F \<in> Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
 by (blast intro: subset_Always_comp [THEN subsetD])
 
 
-lemma imp_Always_comp2: 
-"[| F \<in> Always({x \<in> state. <f1(x), f(x)> \<in> r});   
-    F \<in> Always({x \<in> state. <g1(x), g(x)> \<in> s});  
-    mono2(A, r, B, s, C, t, h);  
-    \<forall>x \<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |]  
+lemma imp_Always_comp2:
+"[| F \<in> Always({x \<in> state. <f1(x), f(x)> \<in> r});
+    F \<in> Always({x \<in> state. <g1(x), g(x)> \<in> s});
+    mono2(A, r, B, s, C, t, h);
+    \<forall>x \<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |]
   ==> F \<in> Always({x \<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \<in> t})"
 apply (auto simp add: Always_eq_includes_reachable mono2_def)
 apply (auto dest!: subsetD)
@@ -73,10 +77,10 @@
 
 (* comp LeadsTo *)
 
-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}) <=  
+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})"
 
 apply (unfold mono1_def metacomp_def, clarify)
@@ -93,19 +97,19 @@
 apply auto
 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});  
-    mono1(A, r, B, s, h); refl(A,r); trans[B](s);  
-    \<forall>x \<in> state. f(x):A & g(x):A |] ==>  
+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});
+    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})"
 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};  
-  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 |] ==>  
+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};
+  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}"
 apply (unfold mono2_def Increasing_def)
 apply (rule single_LeadsTo_I, auto)
@@ -124,11 +128,11 @@
 apply (auto simp add: part_order_def)
 done
 
-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};  
-  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 |] ==>  
+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};
+  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}"
 apply (unfold mono2_def Increasing_def)
 apply (rule single_LeadsTo_I, auto)
@@ -148,12 +152,12 @@
 done
 
 (**  This general result is used to prove Follows Un, munion, etc. **)
-lemma imp_LeadsTo_comp2: 
-"[| F \<in> Increasing(A, r, f1) Int  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};  
-  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 |] 
+lemma imp_LeadsTo_comp2:
+"[| F \<in> Increasing(A, r, f1) Int  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};
+  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}"
 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)
@@ -169,21 +173,21 @@
 lemma Follows_into_program [TC]: "F \<in> Follows(A, r, f, g) ==> F \<in> program"
 by (blast dest: Follows_type [THEN subsetD])
 
-lemma FollowsD: 
-"F \<in> Follows(A, r, f, g)==>  
+lemma FollowsD:
+"F \<in> Follows(A, r, f, g)==>
   F \<in> program & (\<exists>a. a \<in> A) & (\<forall>x \<in> state. f(x):A & g(x):A)"
 apply (unfold Follows_def)
 apply (blast dest: IncreasingD)
 done
 
-lemma Follows_constantI: 
+lemma Follows_constantI:
  "[| F \<in> program; c \<in> A; refl(A, r) |] ==> F \<in> Follows(A, r, %x. c, %x. c)"
 apply (unfold Follows_def, auto)
 apply (auto simp add: refl_def)
 done
 
-lemma subset_Follows_comp: 
-"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]  
+lemma subset_Follows_comp:
+"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
    ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)"
 apply (unfold Follows_def, clarify)
 apply (frule_tac f = g in IncreasingD)
@@ -194,19 +198,19 @@
 apply (auto intro: imp_Increasing_comp imp_Always_comp simp del: INT_simps)
 done
 
-lemma imp_Follows_comp: 
-"[| F \<in> Follows(A, r, f, g);  mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]  
+lemma imp_Follows_comp:
+"[| F \<in> Follows(A, r, f, g);  mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]
   ==>  F \<in> Follows(B, s,  h comp f, h comp g)"
 apply (blast intro: subset_Follows_comp [THEN subsetD])
 done
 
 (* 2-place monotone operation \<in> this general result is used to prove Follows_Un, Follows_munion *)
 
-(* 2-place monotone operation \<in> this general result is 
+(* 2-place monotone operation \<in> this general result is
    used to prove Follows_Un, Follows_munion *)
-lemma imp_Follows_comp2: 
-"[| F \<in> Follows(A, r, f1, f);  F \<in> Follows(B, s, g1, g);  
-   mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |]  
+lemma imp_Follows_comp2:
+"[| F \<in> Follows(A, r, f1, f);  F \<in> Follows(B, s, g1, g);
+   mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |]
    ==> F \<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))"
 apply (unfold Follows_def, clarify)
 apply (frule_tac f = g in IncreasingD)
@@ -223,13 +227,13 @@
 apply (rule_tac h = h in imp_LeadsTo_comp2)
 prefer 4 apply assumption
 apply auto
-  prefer 3 apply (simp add: mono2_def) 
+  prefer 3 apply (simp add: mono2_def)
 apply (blast dest: IncreasingD)+
 done
 
 
 lemma Follows_trans:
-     "[| F \<in> Follows(A, r, f, g);  F \<in> Follows(A,r, g, h);  
+     "[| F \<in> Follows(A, r, f, g);  F \<in> Follows(A,r, g, h);
          trans[A](r) |] ==> F \<in> Follows(A, r, f, h)"
 apply (frule_tac f = f in FollowsD)
 apply (frule_tac f = g in FollowsD)
@@ -242,64 +246,64 @@
 
 (** Destruction rules for Follows **)
 
-lemma Follows_imp_Increasing_left: 
+lemma Follows_imp_Increasing_left:
      "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, f)"
 by (unfold Follows_def, blast)
 
-lemma Follows_imp_Increasing_right: 
+lemma Follows_imp_Increasing_right:
      "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, g)"
 by (unfold Follows_def, blast)
 
-lemma Follows_imp_Always: 
+lemma Follows_imp_Always:
  "F :Follows(A, r, f, g) ==> F \<in> Always({s \<in> state. <f(s),g(s)> \<in> r})"
 by (unfold Follows_def, blast)
 
-lemma Follows_imp_LeadsTo: 
- "[| F \<in> Follows(A, r, f, g); k \<in> A |]  ==>  
+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}"
 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> 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)}"
 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> 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)}"
 by (blast intro: Follows_imp_LeadsTo)
 
-lemma Always_Follows1: 
-"[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);   
+lemma Always_Follows1:
+"[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);
     \<forall>x \<in> state. g(x):A |] ==> F \<in> Follows(A, r, g, h)"
 apply (unfold Follows_def Increasing_def Stable_def)
 apply (simp add: INT_iff, auto)
-apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}" 
-	and A = "{s \<in> state. <k, h (s)> \<in> r}" 
+apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}"
+	and A = "{s \<in> state. <k, h (s)> \<in> r}"
 	and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken)
-apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}" 
+apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}"
            and A' = "{s \<in> state. <k,f(s) > \<in> r}" in Always_Constrains_weaken)
 apply auto
 apply (drule Always_Int_I, assumption)
-apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}" 
+apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}"
        in Always_weaken)
 apply auto
 done
 
 
-lemma Always_Follows2: 
-"[| F \<in> Always({s \<in> state. g(s) = h(s)});  
+lemma Always_Follows2:
+"[| F \<in> Always({s \<in> state. g(s) = h(s)});
   F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A |] ==> F \<in> Follows(A, r, f, h)"
 apply (unfold Follows_def Increasing_def Stable_def)
 apply (simp add: INT_iff, auto)
-apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }" 
-            and A = "{s \<in> state. <k, g (s) > \<in> r}" 
+apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }"
+            and A = "{s \<in> state. <k, g (s) > \<in> r}"
             and A' = "{s \<in> state. <k, f (s) > \<in> r}" in Always_LeadsTo_weaken)
-apply (erule_tac A = "{s \<in> state. <k, g(s)> \<in> r}" 
+apply (erule_tac A = "{s \<in> state. <k, g(s)> \<in> r}"
          and A' = "{s \<in> state. <k, g(s)> \<in> r}" in Always_Constrains_weaken)
 apply auto
 apply (drule Always_Int_I, assumption)
-apply (erule_tac A = "{s \<in> state. g(s)=h(s)} \<inter> {s \<in> state. <f(s), g(s)> \<in> r}" 
+apply (erule_tac A = "{s \<in> state. g(s)=h(s)} \<inter> {s \<in> state. <f(s), g(s)> \<in> r}"
        in Always_weaken)
 apply auto
 done
@@ -319,26 +323,26 @@
 by (unfold part_order_def, auto)
 
 lemma increasing_Un:
-     "[| F \<in> Increasing.increasing(Pow(A), SetLe(A), f);   
-         F \<in> Increasing.increasing(Pow(A), SetLe(A), g) |]  
+     "[| F \<in> Increasing.increasing(Pow(A), SetLe(A), f);
+         F \<in> Increasing.increasing(Pow(A), SetLe(A), g) |]
      ==> F \<in> Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
 by (rule_tac h = "op Un" in imp_increasing_comp2, auto)
 
 lemma Increasing_Un:
-     "[| F \<in> Increasing(Pow(A), SetLe(A), f);   
-         F \<in> Increasing(Pow(A), SetLe(A), g) |]  
+     "[| F \<in> Increasing(Pow(A), SetLe(A), f);
+         F \<in> Increasing(Pow(A), SetLe(A), g) |]
      ==> F \<in> Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
 by (rule_tac h = "op Un" in imp_Increasing_comp2, auto)
 
 lemma Always_Un:
-     "[| F \<in> Always({s \<in> state. f1(s) <= f(s)});  
-     F \<in> Always({s \<in> state. g1(s) <= g(s)}) |]  
+     "[| F \<in> Always({s \<in> state. f1(s) <= f(s)});
+     F \<in> Always({s \<in> state. g1(s) <= g(s)}) |]
       ==> F \<in> Always({s \<in> state. f1(s) Un g1(s) <= f(s) Un g(s)})"
 by (simp add: Always_eq_includes_reachable, blast)
 
-lemma Follows_Un: 
-"[| F \<in> Follows(Pow(A), SetLe(A), f1, f);  
-     F \<in> Follows(Pow(A), SetLe(A), g1, g) |]  
+lemma Follows_Un:
+"[| F \<in> Follows(Pow(A), SetLe(A), f1, f);
+     F \<in> Follows(Pow(A), SetLe(A), g1, g) |]
      ==> F \<in> Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))"
 by (rule_tac h = "op Un" in imp_Follows_comp2, auto)
 
@@ -347,7 +351,7 @@
 lemma refl_MultLe [simp]: "refl(Mult(A), MultLe(A,r))"
 by (unfold MultLe_def refl_def, auto)
 
-lemma MultLe_refl1 [simp]: 
+lemma MultLe_refl1 [simp]:
  "[| multiset(M); mset_of(M)<=A |] ==> <M, M> \<in> MultLe(A, r)"
 apply (unfold MultLe_def id_def lam_def)
 apply (auto simp add: Mult_iff_multiset)
@@ -374,7 +378,7 @@
 apply (auto dest: MultLe_type [THEN subsetD])
 done
 
-lemma part_order_imp_part_ord: 
+lemma part_order_imp_part_ord:
      "part_order(A, r) ==> part_ord(A, r-id(A))"
 apply (unfold part_order_def part_ord_def)
 apply (simp add: refl_def id_def lam_def irrefl_def, auto)
@@ -385,7 +389,7 @@
 apply auto
 done
 
-lemma antisym_MultLe [simp]: 
+lemma antisym_MultLe [simp]:
   "part_order(A, r) ==> antisym(MultLe(A,r))"
 apply (unfold MultLe_def antisym_def)
 apply (drule part_order_imp_part_ord, auto)
@@ -401,7 +405,7 @@
 apply (auto simp add: part_order_def)
 done
 
-lemma empty_le_MultLe [simp]: 
+lemma empty_le_MultLe [simp]:
 "[| multiset(M); mset_of(M)<= A|] ==> <0, M> \<in> MultLe(A, r)"
 apply (unfold MultLe_def)
 apply (case_tac "M=0")
@@ -414,8 +418,8 @@
 lemma empty_le_MultLe2 [simp]: "M \<in> Mult(A) ==> <0, M> \<in> MultLe(A, r)"
 by (simp add: Mult_iff_multiset)
 
-lemma munion_mono: 
-"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==> 
+lemma munion_mono:
+"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==>
   <M +# K, N +# L> \<in> MultLe(A, r)"
 apply (unfold MultLe_def)
 apply (auto intro: munion_multirel_mono1 munion_multirel_mono2
@@ -423,41 +427,41 @@
 done
 
 lemma increasing_munion:
-     "[| F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f);   
-         F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |]  
+     "[| F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f);
+         F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |]
      ==> F \<in> Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
 by (rule_tac h = munion in imp_increasing_comp2, auto)
 
 lemma Increasing_munion:
-     "[| F \<in> Increasing(Mult(A), MultLe(A,r), f);   
-         F \<in> Increasing(Mult(A), MultLe(A,r), g)|]  
+     "[| F \<in> Increasing(Mult(A), MultLe(A,r), f);
+         F \<in> Increasing(Mult(A), MultLe(A,r), g)|]
      ==> F \<in> Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
 by (rule_tac h = munion in imp_Increasing_comp2, auto)
 
-lemma Always_munion: 
-"[| F \<in> Always({s \<in> state. <f1(s),f(s)> \<in> MultLe(A,r)});  
-          F \<in> Always({s \<in> state. <g1(s), g(s)> \<in> MultLe(A,r)}); 
-  \<forall>x \<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|]  
+lemma Always_munion:
+"[| F \<in> Always({s \<in> state. <f1(s),f(s)> \<in> MultLe(A,r)});
+          F \<in> Always({s \<in> state. <g1(s), g(s)> \<in> MultLe(A,r)});
+  \<forall>x \<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|]
       ==> F \<in> Always({s \<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \<in> MultLe(A,r)})"
 apply (rule_tac h = munion in imp_Always_comp2, simp_all)
 apply (blast intro: munion_mono, simp_all)
 done
 
-lemma Follows_munion: 
-"[| F \<in> Follows(Mult(A), MultLe(A, r), f1, f);  
-    F \<in> Follows(Mult(A), MultLe(A, r), g1, g) |]  
+lemma Follows_munion:
+"[| F \<in> Follows(Mult(A), MultLe(A, r), f1, f);
+    F \<in> Follows(Mult(A), MultLe(A, r), g1, g) |]
   ==> F \<in> Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))"
 by (rule_tac h = munion in imp_Follows_comp2, auto)
 
 (** Used in ClientImp **)
 
-lemma Follows_msetsum_UN: 
-"!!f. [| \<forall>i \<in> I. F \<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i));  
-  \<forall>s. \<forall>i \<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A &  
-                        multiset(f(i, s)) & mset_of(f(i, s))<=A ;  
-   Finite(I); F \<in> program |]  
-        ==> F \<in> Follows(Mult(A),  
-                        MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A),  
+lemma Follows_msetsum_UN:
+"!!f. [| \<forall>i \<in> I. F \<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i));
+  \<forall>s. \<forall>i \<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A &
+                        multiset(f(i, s)) & mset_of(f(i, s))<=A ;
+   Finite(I); F \<in> program |]
+        ==> F \<in> Follows(Mult(A),
+                        MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A),
                                       %x. msetsum(%i. f(i,  x), I, A))"
 apply (erule rev_mp)
 apply (drule Finite_into_Fin)
diff -r df3581710b9b -r c663e675e177 src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -12,8 +12,7 @@
 header{*Charpentier's Generalized Prefix Relation*}
 
 theory GenPrefix
-imports Main 
-
+imports Main
 begin
 
 constdefs (*really belongs in ZF/Trancl*)
@@ -22,12 +21,12 @@
 
 consts
   gen_prefix :: "[i, i] => i"
-  
+
 inductive
   (* Parameter A is the domain of zs's elements *)
-  
+
   domains "gen_prefix(A, r)" <= "list(A)*list(A)"
-  
+
   intros
     Nil:     "<[],[]>:gen_prefix(A, r)"
 
@@ -45,17 +44,19 @@
    strict_prefix :: "i=>i"
   "strict_prefix(A) == prefix(A) - id(list(A))"
 
-syntax
-  (* less or equal and greater or equal over prefixes *)
-  pfixLe :: "[i, i] => o"               (infixl "pfixLe" 50)
-  pfixGe :: "[i, i] => o"               (infixl "pfixGe" 50)
+
+(* less or equal and greater or equal over prefixes *)
+
+abbreviation
+  pfixLe :: "[i, i] => o"  (infixl "pfixLe" 50)  where
+  "xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)"
 
-translations
-   "xs pfixLe ys" == "<xs, ys>:gen_prefix(nat, Le)"
-   "xs pfixGe ys" == "<xs, ys>:gen_prefix(nat, Ge)"
-  
+abbreviation
+  pfixGe :: "[i, i] => o"  (infixl "pfixGe" 50)  where
+  "xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)"
 
-lemma reflD: 
+
+lemma reflD:
  "[| refl(A, r); x \<in> A |] ==> <x,x>:r"
 apply (unfold refl_def, auto)
 done
@@ -76,25 +77,25 @@
 
 
 lemma Cons_gen_prefix_aux:
-  "[| <xs', ys'> \<in> gen_prefix(A, r) |]  
-   ==> (\<forall>x xs. x \<in> A --> xs'= Cons(x,xs) -->  
-       (\<exists>y ys. y \<in> A & ys' = Cons(y,ys) & 
+  "[| <xs', ys'> \<in> gen_prefix(A, r) |]
+   ==> (\<forall>x xs. x \<in> A --> xs'= Cons(x,xs) -->
+       (\<exists>y ys. y \<in> A & ys' = Cons(y,ys) &
        <x,y>:r & <xs, ys> \<in> gen_prefix(A, r)))"
 apply (erule gen_prefix.induct)
-prefer 3 apply (force intro: gen_prefix.append, auto) 
+prefer 3 apply (force intro: gen_prefix.append, auto)
 done
 
 lemma Cons_gen_prefixE:
-  "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r);  
-    !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;  
+  "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r);
+    !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;
       <xs,ys> \<in> gen_prefix(A, r) |] ==> P |] ==> P"
-apply (frule gen_prefix.dom_subset [THEN subsetD], auto) 
-apply (blast dest: Cons_gen_prefix_aux) 
+apply (frule gen_prefix.dom_subset [THEN subsetD], auto)
+apply (blast dest: Cons_gen_prefix_aux)
 done
 declare Cons_gen_prefixE [elim!]
 
-lemma Cons_gen_prefix_Cons: 
-"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r))  
+lemma Cons_gen_prefix_Cons:
+"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r))
   <-> (x \<in> A & y \<in> A & <x,y>:r & <xs,ys> \<in> gen_prefix(A, r))"
 apply (auto intro: gen_prefix.prepend)
 done
@@ -142,7 +143,7 @@
 (* Transitivity *)
 (* A lemma for proving gen_prefix_trans_comp *)
 
-lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==>  
+lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==>
    \<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)"
 apply (erule list.induct)
 apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
@@ -151,7 +152,7 @@
 (* Lemma proving transitivity and more*)
 
 lemma gen_prefix_trans_comp [rule_format (no_asm)]:
-     "<x, y>: gen_prefix(A, r) ==>  
+     "<x, y>: gen_prefix(A, r) ==>
    (\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)--><x, z> \<in> gen_prefix(A, s O r))"
 apply (erule gen_prefix.induct)
 apply (auto elim: ConsE simp add: Nil_gen_prefix)
@@ -171,14 +172,14 @@
 apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
 done
 
-lemma trans_on_gen_prefix: 
+lemma trans_on_gen_prefix:
  "trans(r) ==> trans[list(A)](gen_prefix(A, r))"
 apply (drule_tac A = A in trans_gen_prefix)
 apply (unfold trans_def trans_on_def, blast)
 done
 
 lemma prefix_gen_prefix_trans:
-    "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |]  
+    "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |]
       ==>  <x, z> \<in> gen_prefix(A, r)"
 apply (unfold prefix_def)
 apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst])
@@ -186,8 +187,8 @@
 done
 
 
-lemma gen_prefix_prefix_trans: 
-"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |]  
+lemma gen_prefix_prefix_trans:
+"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |]
   ==>  <x, z> \<in> gen_prefix(A, r)"
 apply (unfold prefix_def)
 apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst])
@@ -202,7 +203,7 @@
 lemma antisym_gen_prefix: "antisym(r) ==> antisym(gen_prefix(A, r))"
 apply (simp (no_asm) add: antisym_def)
 apply (rule impI [THEN allI, THEN allI])
-apply (erule gen_prefix.induct, blast) 
+apply (erule gen_prefix.induct, blast)
 apply (simp add: antisym_def, blast)
 txt{*append case is hardest*}
 apply clarify
@@ -227,8 +228,8 @@
 by (induct_tac "xs", auto)
 declare gen_prefix_Nil [simp]
 
-lemma same_gen_prefix_gen_prefix: 
- "[| refl(A, r);  xs \<in> list(A) |] ==>  
+lemma same_gen_prefix_gen_prefix:
+ "[| refl(A, r);  xs \<in> list(A) |] ==>
     <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs> \<in> gen_prefix(A, r)"
 apply (unfold refl_def)
 apply (induct_tac "xs")
@@ -236,13 +237,13 @@
 done
 declare same_gen_prefix_gen_prefix [simp]
 
-lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>  
-    <xs, Cons(y,ys)> \<in> gen_prefix(A,r)  <->  
+lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+    <xs, Cons(y,ys)> \<in> gen_prefix(A,r)  <->
       (xs=[] | (\<exists>z zs. xs=Cons(z,zs) & z \<in> A & <z,y>:r & <zs,ys> \<in> gen_prefix(A,r)))"
 apply (induct_tac "xs", auto)
 done
 
-lemma gen_prefix_take_append: "[| refl(A,r);  <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |]  
+lemma gen_prefix_take_append: "[| refl(A,r);  <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |]
       ==>  <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)"
 apply (erule gen_prefix.induct)
 apply (simp (no_asm_simp))
@@ -252,8 +253,8 @@
 apply (simp_all (no_asm_simp) add: diff_is_0_iff [THEN iffD2] take_type)
 done
 
-lemma gen_prefix_append_both: "[| refl(A, r);  <xs,ys> \<in> gen_prefix(A,r);    
-         length(xs) = length(ys); zs \<in> list(A) |]  
+lemma gen_prefix_append_both: "[| refl(A, r);  <xs,ys> \<in> gen_prefix(A,r);
+         length(xs) = length(ys); zs \<in> list(A) |]
       ==>  <xs@zs, ys @ zs> \<in> gen_prefix(A, r)"
 apply (drule_tac zs = zs in gen_prefix_take_append, assumption+)
 apply (subgoal_tac "take (length (xs), ys) =ys")
@@ -265,8 +266,8 @@
 by (auto simp add: app_assoc)
 
 lemma append_one_gen_prefix_lemma [rule_format]:
-     "[| <xs,ys> \<in> gen_prefix(A, r);  refl(A, r) |]  
-      ==> length(xs) < length(ys) -->  
+     "[| <xs,ys> \<in> gen_prefix(A, r);  refl(A, r) |]
+      ==> length(xs) < length(ys) -->
           <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
 apply (erule gen_prefix.induct, blast)
 apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
@@ -286,9 +287,9 @@
 apply (simplesubst append_cons_conv)
 apply (rule_tac [2] gen_prefix.append)
 apply (auto elim: ConsE simp add: gen_prefix_append_both)
-done 
+done
 
-lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r);  length(xs) < length(ys);  refl(A, r) |]  
+lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r);  length(xs) < length(ys);  refl(A, r) |]
       ==> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
 apply (blast intro: append_one_gen_prefix_lemma)
 done
@@ -296,24 +297,24 @@
 
 (** Proving the equivalence with Charpentier's definition **)
 
-lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==>   
-  \<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs)  
+lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==>
+  \<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs)
           --> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r"
-apply (induct_tac "xs", simp, clarify) 
-apply simp 
-apply (erule natE, auto) 
+apply (induct_tac "xs", simp, clarify)
+apply simp
+apply (erule natE, auto)
 done
 
-lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|]  
+lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|]
       ==> <nth(i, xs), nth(i, ys)>:r"
 apply (cut_tac A = A in gen_prefix.dom_subset)
 apply (rule gen_prefix_imp_nth_lemma)
 apply (auto simp add: lt_nat_in_nat)
 done
 
-lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==>  
-  \<forall>ys \<in> list(A). length(xs) \<le> length(ys)   
-      --> (\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r)   
+lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==>
+  \<forall>ys \<in> list(A). length(xs) \<le> length(ys)
+      --> (\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r)
       --> <xs, ys> \<in> gen_prefix(A, r)"
 apply (induct_tac "xs")
 apply (simp_all (no_asm_simp))
@@ -322,12 +323,12 @@
 apply (force intro!: nat_0_le simp add: lt_nat_in_nat)
 done
 
-lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) <->  
-      (xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) &  
+lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) <->
+      (xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) &
       (\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))"
 apply (rule iffI)
 apply (frule gen_prefix.dom_subset [THEN subsetD])
-apply (frule gen_prefix_length_le, auto) 
+apply (frule gen_prefix_length_le, auto)
 apply (rule_tac [2] nth_imp_gen_prefix)
 apply (drule gen_prefix_imp_nth)
 apply (auto simp add: lt_nat_in_nat)
@@ -360,7 +361,7 @@
 
 (* Monotonicity of "set" operator WRT prefix *)
 
-lemma set_of_list_prefix_mono: 
+lemma set_of_list_prefix_mono:
 "<xs,ys> \<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)"
 
 apply (unfold prefix_def)
@@ -389,13 +390,13 @@
 done
 declare prefix_Nil [iff]
 
-lemma Cons_prefix_Cons: 
+lemma Cons_prefix_Cons:
 "<Cons(x,xs), Cons(y,ys)> \<in> prefix(A) <-> (x=y & <xs,ys> \<in> prefix(A) & y \<in> A)"
 apply (unfold prefix_def, auto)
 done
 declare Cons_prefix_Cons [iff]
 
-lemma same_prefix_prefix: 
+lemma same_prefix_prefix:
 "xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) <-> (<ys,zs> \<in> prefix(A))"
 apply (unfold prefix_def)
 apply (subgoal_tac "refl (A,id (A))")
@@ -410,23 +411,23 @@
 done
 declare same_prefix_prefix_Nil [simp]
 
-lemma prefix_appendI: 
+lemma prefix_appendI:
 "[| <xs,ys> \<in> prefix(A); zs \<in> list(A) |] ==> <xs,ys@zs> \<in> prefix(A)"
 apply (unfold prefix_def)
 apply (erule gen_prefix.append, assumption)
 done
 declare prefix_appendI [simp]
 
-lemma prefix_Cons: 
-"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>  
-  <xs,Cons(y,ys)> \<in> prefix(A) <->  
+lemma prefix_Cons:
+"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+  <xs,Cons(y,ys)> \<in> prefix(A) <->
   (xs=[] | (\<exists>zs. xs=Cons(y,zs) & <zs,ys> \<in> prefix(A)))"
 apply (unfold prefix_def)
 apply (auto simp add: gen_prefix_Cons)
 done
 
-lemma append_one_prefix: 
-  "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |]  
+lemma append_one_prefix:
+  "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |]
   ==> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
 apply (unfold prefix_def)
 apply (subgoal_tac "refl (A, id (A))")
@@ -434,7 +435,7 @@
 apply (auto simp add: refl_def)
 done
 
-lemma prefix_length_le: 
+lemma prefix_length_le:
 "<xs,ys> \<in> prefix(A) ==> length(xs) \<le> length(ys)"
 apply (unfold prefix_def)
 apply (blast dest: gen_prefix_length_le)
@@ -445,13 +446,13 @@
 apply (blast intro!: gen_prefix.dom_subset)
 done
 
-lemma strict_prefix_type: 
+lemma strict_prefix_type:
 "strict_prefix(A) <= list(A)*list(A)"
 apply (unfold strict_prefix_def)
 apply (blast intro!: prefix_type [THEN subsetD])
 done
 
-lemma strict_prefix_length_lt_aux: 
+lemma strict_prefix_length_lt_aux:
      "<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys --> length(xs) < length(ys)"
 apply (unfold prefix_def)
 apply (erule gen_prefix.induct, clarify)
@@ -464,7 +465,7 @@
 apply auto
 done
 
-lemma strict_prefix_length_lt: 
+lemma strict_prefix_length_lt:
      "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)"
 apply (unfold strict_prefix_def)
 apply (rule strict_prefix_length_lt_aux [THEN mp])
@@ -472,7 +473,7 @@
 done
 
 (*Equivalence to the definition used in Lex/Prefix.thy*)
-lemma prefix_iff: 
+lemma prefix_iff:
     "<xs,zs> \<in> prefix(A) <-> (\<exists>ys \<in> list(A). zs = xs@ys) & xs \<in> list(A)"
 apply (unfold prefix_def)
 apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app)
@@ -490,8 +491,8 @@
 apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split)
 done
 
-lemma prefix_snoc: 
-"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>  
+lemma prefix_snoc:
+"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
    <xs, ys@[y]> \<in> prefix(A) <-> (xs = ys@[y] | <xs,ys> \<in> prefix(A))"
 apply (simp (no_asm) add: prefix_iff)
 apply (rule iffI, clarify)
@@ -501,28 +502,28 @@
 done
 declare prefix_snoc [simp]
 
-lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).  
-   (<xs, ys@zs> \<in> prefix(A)) <->  
+lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).
+   (<xs, ys@zs> \<in> prefix(A)) <->
   (<xs,ys> \<in> prefix(A) | (\<exists>us. xs = ys@us & <us,zs> \<in> prefix(A)))"
-apply (erule list_append_induct, force, clarify) 
-apply (rule iffI) 
+apply (erule list_append_induct, force, clarify)
+apply (rule iffI)
 apply (simp add: add: app_assoc [symmetric])
-apply (erule disjE)  
-apply (rule disjI2) 
-apply (rule_tac x = "y @ [x]" in exI) 
+apply (erule disjE)
+apply (rule disjI2)
+apply (rule_tac x = "y @ [x]" in exI)
 apply (simp add: add: app_assoc [symmetric], force+)
 done
 
 
 (*Although the prefix ordering is not linear, the prefixes of a list
   are linearly ordered.*)
-lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |]  
-   ==> <xs, zs> \<in> prefix(A) --> <ys,zs> \<in> prefix(A)  
+lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |]
+   ==> <xs, zs> \<in> prefix(A) --> <ys,zs> \<in> prefix(A)
   --><xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
 apply (erule list_append_induct, auto)
 done
 
-lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |]    
+lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |]
       ==> <xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
 apply (cut_tac prefix_type)
 apply (blast del: disjCI intro: common_prefix_linear_lemma)
@@ -574,7 +575,7 @@
 by (blast intro: antisym_gen_prefix [THEN antisymE] antisym_Le)
 
 
-lemma prefix_imp_pfixLe: 
+lemma prefix_imp_pfixLe:
 "<xs,ys>:prefix(nat)==> xs pfixLe ys"
 
 apply (unfold prefix_def)
@@ -607,14 +608,14 @@
 lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
 by (blast intro: antisym_gen_prefix [THEN antisymE])
 
-lemma prefix_imp_pfixGe: 
+lemma prefix_imp_pfixGe:
   "<xs,ys>:prefix(nat) ==> xs pfixGe ys"
 apply (unfold prefix_def Ge_def)
 apply (rule gen_prefix_mono [THEN subsetD], auto)
 done
 (* Added by Sidi \<in> prefix and take *)
 
-lemma prefix_imp_take: 
+lemma prefix_imp_take:
 "<xs, ys> \<in> prefix(A) ==> xs = take(length(xs), ys)"
 
 apply (unfold prefix_def)
@@ -655,9 +656,9 @@
 lemma prefix_imp_nth: "[| <xs,ys> \<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)"
 by (auto dest!: gen_prefix_imp_nth simp add: prefix_def)
 
-lemma nth_imp_prefix: 
-     "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);   
-        !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]   
+lemma nth_imp_prefix:
+     "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);
+        !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]
       ==> <xs,ys> \<in> prefix(A)"
 apply (auto simp add: prefix_def nth_imp_gen_prefix)
 apply (auto intro!: nth_imp_gen_prefix simp add: prefix_def)
@@ -665,7 +666,7 @@
 done
 
 
-lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys);  
+lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys);
         <xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)|] ==> <xs,ys> \<in> prefix(A)"
 apply (cut_tac A = A in prefix_type)
 apply (rule nth_imp_prefix, blast, blast)
diff -r df3581710b9b -r c663e675e177 src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/Increasing.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -23,11 +23,9 @@
     {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
                 (\<forall>x \<in> state. f(x):A)}"
 
-syntax
-  IncWrt ::  "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
-
-translations
-  "IncWrt(f,r,A)" => "Increasing[A](r,f)"
+abbreviation (input)
+  IncWrt ::  "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)  where
+  "f IncreasingWrt r/A == Increasing[A](r,f)"
 
 
 (** increasing **)
diff -r df3581710b9b -r c663e675e177 src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/Mutex.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -15,27 +15,19 @@
 the usual ZF typechecking: an ill-tyed expressions reduce to the empty set.
 *}
 
-consts
-  p :: i
-  m :: i
-  n :: i
-  u :: i
-  v :: i
-  
-translations
-  "p" == "Var([0])"
-  "m" == "Var([1])"
-  "n" == "Var([0,0])"
-  "u" == "Var([0,1])"
-  "v" == "Var([1,0])"
-  
+abbreviation "p == Var([0])"
+abbreviation "m == Var([1])"
+abbreviation "n == Var([0,0])"
+abbreviation "u == Var([0,1])"
+abbreviation "v == Var([1,0])"
+
 axioms --{** Type declarations  **}
   p_type:  "type_of(p)=bool & default_val(p)=0"
   m_type:  "type_of(m)=int  & default_val(m)=#0"
   n_type:  "type_of(n)=int  & default_val(n)=#0"
   u_type:  "type_of(u)=bool & default_val(u)=0"
   v_type:  "type_of(v)=bool & default_val(v)=0"
-  
+
 constdefs
   (** The program for process U **)
    U0 :: i
@@ -53,9 +45,9 @@
   U4 :: i
     "U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}"
 
-  
+
    (** The program for process V **)
-  
+
   V0 :: i
     "V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}"
 
@@ -180,18 +172,18 @@
 declare  bad_IU_def [THEN def_set_simp, simp]
 
 lemma IU: "Mutex \<in> Always(IU)"
-apply (rule AlwaysI, force) 
-apply (unfold Mutex_def, safety, auto) 
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, safety, auto)
 done
 
 lemma IV: "Mutex \<in> Always(IV)"
-apply (rule AlwaysI, force) 
-apply (unfold Mutex_def, safety) 
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, safety)
 done
 
 (*The safety property: mutual exclusion*)
 lemma mutual_exclusion: "Mutex \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})"
-apply (rule Always_weaken) 
+apply (rule Always_weaken)
 apply (rule Always_Int_I [OF IU IV], auto)
 done
 
@@ -203,13 +195,13 @@
 done
 
 lemma "Mutex \<in> Always(bad_IU)"
-apply (rule AlwaysI, force) 
+apply (rule AlwaysI, force)
 apply (unfold Mutex_def, safety, auto)
 apply (subgoal_tac "#1 $<= #3")
 apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto)
 apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym])
 apply auto
-(*Resulting state: n=1, p=false, m=4, u=false.  
+(*Resulting state: n=1, p=false, m=4, u=false.
   Execution of V1 (the command of process v guarded by n=1) sets p:=true,
   violating the invariant!*)
 oops
@@ -291,7 +283,7 @@
 lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {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 (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
 apply (auto dest!: p_value_type simp add: bool_def)
 done
 
diff -r df3581710b9b -r c663e675e177 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/Univ.thy	Sun Oct 07 15:49:25 2007 +0200
@@ -17,9 +17,9 @@
   Vfrom       :: "[i,i]=>i"
     "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
 
-syntax   Vset :: "i=>i"
-translations
-    "Vset(x)"   ==      "Vfrom(0,x)"
+abbreviation
+  Vset :: "i=>i" where
+  "Vset(x) == Vfrom(0,x)"
 
 
 constdefs