# HG changeset patch
# User paulson
# Date 990449524 -7200
# Node ID 56aa53caf3334ec93105668d4615610bc2999562
# Parent  8b84ee2cc79cf545c14f1ed0f5097b80ed09d5a4
X-symbols for set theory

diff -r 8b84ee2cc79c -r 56aa53caf333 src/ZF/AC.ML
--- a/src/ZF/AC.ML	Mon May 21 14:51:46 2001 +0200
+++ b/src/ZF/AC.ML	Mon May 21 14:52:04 2001 +0200
@@ -6,9 +6,9 @@
 The Axiom of Choice
 *)
 
-(*The same as AC, but no premise a:A*)
+(*The same as AC, but no premise a \\<in> A*)
 val [nonempty] = goal (the_context ())
-     "[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)";
+     "[| !!x. x \\<in> A ==> (\\<exists>y. y \\<in> B(x)) |] ==> \\<exists>z. z \\<in> Pi(A,B)";
 by (excluded_middle_tac "A=0" 1);
 by (asm_simp_tac (simpset() addsimps [Pi_empty1]) 2 THEN Blast_tac 2);
 (*The non-trivial case*)
@@ -16,37 +16,37 @@
 qed "AC_Pi";
 
 (*Using dtac, this has the advantage of DELETING the universal quantifier*)
-Goal "ALL x:A. EX y. y:B(x) ==> EX y. y : Pi(A,B)";
+Goal "\\<forall>x \\<in> A. \\<exists>y. y \\<in> B(x) ==> \\<exists>y. y \\<in> Pi(A,B)";
 by (rtac AC_Pi 1);
 by (etac bspec 1);
 by (assume_tac 1);
 qed "AC_ball_Pi";
 
-Goal "EX f. f: (PROD X: Pow(C)-{0}. X)";
+Goal "\\<exists>f. f \\<in> (\\<Pi>X \\<in> Pow(C)-{0}. X)";
 by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
 by (etac exI 2);
 by (Blast_tac 1);
 qed "AC_Pi_Pow";
 
 val [nonempty] = goal (the_context ())
-     "[| !!x. x:A ==> (EX y. y:x)       \
-\     |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
+     "[| !!x. x \\<in> A ==> (\\<exists>y. y \\<in> x)       \
+\     |] ==> \\<exists>f \\<in> A->Union(A). \\<forall>x \\<in> A. f`x \\<in> x";
 by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
 by (etac nonempty 1);
 by (blast_tac (claset() addDs [apply_type] addIs [Pi_type]) 1);
 qed "AC_func";
 
-goal ZF.thy "!!x A. [| 0 ~: A;  x: A |] ==> EX y. y:x";
-by (subgoal_tac "x ~= 0" 1);
+Goal "[| 0 \\<notin> A;  x \\<in> A |] ==> \\<exists>y. y \\<in> x";
+by (subgoal_tac "x \\<noteq> 0" 1);
 by (ALLGOALS Blast_tac);
 qed "non_empty_family";
 
-Goal "0 ~: A ==> EX f: A->Union(A). ALL x:A. f`x : x";
+Goal "0 \\<notin> A ==> \\<exists>f \\<in> A->Union(A). \\<forall>x \\<in> A. f`x \\<in> x";
 by (rtac AC_func 1);
 by (REPEAT (ares_tac [non_empty_family] 1));
 qed "AC_func0";
 
-Goal "EX f: (Pow(C)-{0}) -> C. ALL x:(Pow(C)-{0}). f`x : x";
+Goal "\\<exists>f \\<in> (Pow(C)-{0}) -> C. \\<forall>x \\<in> Pow(C)-{0}. f`x \\<in> x";
 by (resolve_tac [AC_func0 RS bexE] 1);
 by (rtac bexI 2);
 by (assume_tac 2);
@@ -54,13 +54,13 @@
 by (ALLGOALS Blast_tac);
 qed "AC_func_Pow";
 
-Goal "0 ~: A ==> EX f. f: (PROD x:A. x)";
+Goal "0 \\<notin> A ==> \\<exists>f. f \\<in> (\\<Pi>x \\<in> A. x)";
 by (rtac AC_Pi 1);
 by (REPEAT (ares_tac [non_empty_family] 1));
 qed "AC_Pi0";
 
 (*Used in Zorn.ML*)
-Goal "[| ch : (PROD X:Pow(S) - {0}. X);  X<=S;  X~=S |] ==> ch ` (S-X) : S-X";
+Goal "[| ch \\<in> (\\<Pi>X \\<in> Pow(S) - {0}. X);  X \\<subseteq> S;  X\\<noteq>S |] ==> ch ` (S-X) \\<in> S-X";
 by (etac apply_type 1);
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "choice_Diff";
diff -r 8b84ee2cc79c -r 56aa53caf333 src/ZF/IMP/Com.ML
--- a/src/ZF/IMP/Com.ML	Mon May 21 14:51:46 2001 +0200
+++ b/src/ZF/IMP/Com.ML	Mon May 21 14:52:04 2001 +0200
@@ -12,26 +12,26 @@
 
 val evala_type_intrs = 
  map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!a.<a,sigma> -a-> n ==> a:aexp",
-  "!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
-  "!!a.<a,sigma> -a-> n ==> n:nat"];
+ ["!!a.<a,sigma> -a-> n ==> a \\<in> aexp",
+  "!!a.<a,sigma> -a-> n ==> sigma \\<in> loc->nat",
+  "!!a.<a,sigma> -a-> n ==> n \\<in> nat"];
 
 
 (**********     type_intrs for evalb     **********)
 
 val evalb_type_intrs = 
  map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!b.<b,sigma> -b-> w ==> b:bexp",
-  "!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
-  "!!b.<b,sigma> -b-> w ==> w:bool"];
+ ["!!b.<b,sigma> -b-> w ==> b \\<in> bexp",
+  "!!b.<b,sigma> -b-> w ==> sigma \\<in> loc->nat",
+  "!!b.<b,sigma> -b-> w ==> w \\<in> bool"];
 
 
 (**********     type_intrs for evalb     **********)
 
 val evalc_type_intrs = 
  map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!c.<c,sigma> -c-> sigma' ==> c:com",
-  "!!c.<c,sigma> -c-> sigma' ==> sigma:loc->nat",
+ ["!!c.<c,sigma> -c-> sigma' ==> c \\<in> com",
+  "!!c.<c,sigma> -c-> sigma' ==> sigma \\<in> loc->nat",
   "!!c.<c,sigma> -c-> sigma' ==> sigma':loc->nat"];
 
 
diff -r 8b84ee2cc79c -r 56aa53caf333 src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Mon May 21 14:51:46 2001 +0200
+++ b/src/ZF/IMP/Com.thy	Mon May 21 14:52:04 2001 +0200
@@ -15,24 +15,24 @@
         aexp :: i
 
 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
-  "aexp" = N ("n: nat")
-         | X ("x: loc")
-         | Op1 ("f : nat -> nat", "a : aexp")
-         | Op2 ("f : (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")
+  "aexp" = N ("n \\<in> nat")
+         | X ("x \\<in> loc")
+         | Op1 ("f \\<in> nat -> nat", "a \\<in> aexp")
+         | Op2 ("f \\<in> (nat*nat) -> nat", "a0 \\<in> aexp", "a1 \\<in> aexp")
 
 
 (** Evaluation of arithmetic expressions **)
 consts  evala    :: i
         "-a->"   :: [i,i] => o                  (infixl 50)
 translations
-    "p -a-> n" == "<p,n> : evala"
+    "p -a-> n" == "<p,n> \\<in> evala"
 inductive
   domains "evala" <= "(aexp * (loc -> nat)) * nat"
   intrs 
-    N   "[| n:nat;  sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
-    X   "[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
-    Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
-    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
+    N   "[| n \\<in> nat;  sigma \\<in> loc->nat |] ==> <N(n),sigma> -a-> n"
+    X   "[| x \\<in> loc;  sigma \\<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
+    Op1 "[| <e,sigma> -a-> n;  f \\<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
+    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f \\<in> (nat*nat) -> nat |] 
            ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
 
   type_intrs "aexp.intrs@[apply_funtype]"
@@ -44,10 +44,10 @@
 datatype <= "univ(aexp Un ((nat*nat)->bool) )"
   "bexp" = true
          | false
-         | ROp  ("f : (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
-         | noti ("b : bexp")
-         | andi ("b0 : bexp", "b1 : bexp")      (infixl 60)
-         | ori  ("b0 : bexp", "b1 : bexp")      (infixl 60)
+         | ROp  ("f \\<in> (nat*nat)->bool", "a0 \\<in> aexp", "a1 \\<in> aexp")
+         | noti ("b \\<in> bexp")
+         | andi ("b0 \\<in> bexp", "b1 \\<in> bexp")      (infixl 60)
+         | ori  ("b0 \\<in> bexp", "b1 \\<in> bexp")      (infixl 60)
 
 
 (** Evaluation of boolean expressions **)
@@ -55,14 +55,14 @@
        "-b->"   :: [i,i] => o                   (infixl 50)
 
 translations
-    "p -b-> b" == "<p,b> : evalb"
+    "p -b-> b" == "<p,b> \\<in> evalb"
 
 inductive
   domains "evalb" <= "(bexp * (loc -> nat)) * bool"
   intrs (*avoid clash with ML constructors true, false*)
-    tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
-    fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
-    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] 
+    tru   "[| sigma \\<in> loc -> nat |] ==> <true,sigma> -b-> 1"
+    fls   "[| sigma \\<in> loc -> nat |] ==> <false,sigma> -b-> 0"
+    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \\<in> (nat*nat)->bool |] 
            ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
     noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
     andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
@@ -80,45 +80,45 @@
 
 datatype 
   "com" = skip
-        | asgt  ("x:loc", "a:aexp")             (infixl 60)
-        | semic ("c0:com", "c1:com")            ("_; _"  [60, 60] 10)
-        | while ("b:bexp", "c:com")             ("while _ do _"  60)
-        | ifc   ("b:bexp", "c0:com", "c1:com")  ("ifc _ then _ else _"  60)
+        | asgt  ("x \\<in> loc", "a \\<in> aexp")             (infixl 60)
+        | semic ("c0 \\<in> com", "c1 \\<in> com")            ("_; _"  [60, 60] 10)
+        | while ("b \\<in> bexp", "c \\<in> com")             ("while _ do _"  60)
+        | ifc   ("b \\<in> bexp", "c0 \\<in> com", "c1 \\<in> com")  ("ifc _ then _ else _"  60)
 
 (*Constructor ";" has low precedence to avoid syntactic ambiguities
-  with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
+  with [| m \\<in> nat; x \\<in> loc; ... |] ==> ...  It usually will need parentheses.*)
 
 (** Execution of commands **)
 consts  evalc    :: i
         "-c->"   :: [i,i] => o                   (infixl 50)
 
 translations
-       "p -c-> s" == "<p,s> : evalc"
+       "p -c-> s" == "<p,s> \\<in> evalc"
 
 
 inductive
   domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)"
   intrs
-    skip    "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"
+    skip    "[| sigma \\<in> loc -> nat |] ==> <skip,sigma> -c-> sigma"
 
-    assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> 
+    assign  "[| m \\<in> nat; x \\<in> loc; <a,sigma> -a-> m |] ==> 
             <x asgt a,sigma> -c-> sigma(x:=m)"
 
     semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> 
             <c0 ; c1, sigma> -c-> sigma1"
 
-    ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   
+    ifc1     "[| b \\<in> bexp; c1 \\<in> com; sigma \\<in> loc->nat;   
                  <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
              <ifc b then c0 else c1, sigma> -c-> sigma1"
 
-    ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   
+    ifc0     "[| b \\<in> bexp; c0 \\<in> com; sigma \\<in> loc->nat;   
                  <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
              <ifc b then c0 else c1, sigma> -c-> sigma1"
 
-    while0   "[| c: com; <b, sigma> -b-> 0 |] ==> 
+    while0   "[| c \\<in> com; <b, sigma> -b-> 0 |] ==> 
              <while b do c,sigma> -c-> sigma "
 
-    while1   "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 
+    while1   "[| c \\<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 
                 <while b do c, sigma2> -c-> sigma1 |] ==> 
              <while b do c, sigma> -c-> sigma1 "
 
diff -r 8b84ee2cc79c -r 56aa53caf333 src/ZF/IMP/Denotation.ML
--- a/src/ZF/IMP/Denotation.ML	Mon May 21 14:51:46 2001 +0200
+++ b/src/ZF/IMP/Denotation.ML	Mon May 21 14:52:04 2001 +0200
@@ -11,7 +11,7 @@
 
 (** Type_intr for A **)
 
-Goal "[|a:aexp; sigma:loc->nat|] ==> A(a,sigma):nat";
+Goal "[|a \\<in> aexp; sigma \\<in> loc->nat|] ==> A(a,sigma):nat";
 by (etac aexp.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS (fast_tac (claset() addSIs [apply_type])));
@@ -19,7 +19,7 @@
 
 (** Type_intr for B **)
 
-Goal "[|b:bexp; sigma:loc->nat|] ==> B(b,sigma):bool";
+Goal "[|b \\<in> bexp; sigma \\<in> loc->nat|] ==> B(b,sigma):bool";
 by (etac bexp.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS (fast_tac (claset() addSIs [apply_type,A_type]@bool_typechecks)));
@@ -27,7 +27,7 @@
 
 (** C_subset **)
 
-Goal "c:com ==> C(c) <= (loc->nat)*(loc->nat)";
+Goal "c \\<in> com ==> C(c) \\<subseteq> (loc->nat)*(loc->nat)";
 by (etac com.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS (fast_tac (claset() addDs [lfp_subset RS subsetD])));
@@ -35,11 +35,11 @@
 
 (** Type_elims for C **)
 
-Goal "[| <x,y>:C(c); c:com |] ==> x:loc->nat & y:loc->nat";
+Goal "[| <x,y>:C(c); c \\<in> com |] ==> x \\<in> loc->nat & y \\<in> loc->nat";
 by (blast_tac (claset() addDs [C_subset RS subsetD]) 1);
 qed "C_type_D";
 
-Goal "[| x:C(c); c:com |] ==> fst(x):loc->nat";
+Goal "[| x \\<in> C(c); c \\<in> com |] ==> fst(x):loc->nat";
 by (dtac (C_subset RS subsetD) 1);
 by (atac 1);
 by (etac SigmaE 1);
@@ -51,7 +51,7 @@
 (** bnd_mono (nat->nat*nat->nat,Gamma(b,c) **)
 
 Goalw [bnd_mono_def,Gamma_def]
-     "c:com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))";
+     "c \\<in> com ==> bnd_mono ((loc->nat)*(loc->nat),Gamma(b,c))";
 by (Blast_tac 1);
 qed "Gamma_bnd_mono";
 
diff -r 8b84ee2cc79c -r 56aa53caf333 src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Mon May 21 14:51:46 2001 +0200
+++ b/src/ZF/IMP/Denotation.thy	Mon May 21 14:52:04 2001 +0200
@@ -35,11 +35,11 @@
                                snd(io) = fst(io)(x := A(a,fst(io)))}"
 
   C_comp_def    "C(c0 ; c1) == C(c1) O C(c0)"
-  C_if_def      "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
-                                             {io:C(c1). B(b,fst(io))=0}"
+  C_if_def      "C(ifc b then c0 else c1) == {io \\<in> C(c0). B(b,fst(io))=1} Un 
+                                             {io \\<in> C(c1). B(b,fst(io))=0}"
 
-  Gamma_def     "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un 
-                                     {io : id(loc->nat). B(b,fst(io))=0})"
+  Gamma_def     "Gamma(b,c) == (%phi.{io \\<in> (phi O C(c)). B(b,fst(io))=1} Un 
+                                     {io \\<in> id(loc->nat). B(b,fst(io))=0})"
 
   C_while_def   "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
 
diff -r 8b84ee2cc79c -r 56aa53caf333 src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Mon May 21 14:51:46 2001 +0200
+++ b/src/ZF/IMP/Equiv.ML	Mon May 21 14:52:04 2001 +0200
@@ -4,7 +4,7 @@
     Copyright   1994 TUM
 *)
 
-Goal "[| a: aexp; sigma: loc -> nat |] ==> \
+Goal "[| a \\<in> aexp; sigma: loc -> nat |] ==> \
 \        <a,sigma> -a-> n <-> A(a,sigma) = n";
 by (res_inst_tac [("x","n")] spec 1);                       (* quantify n *)
 by (etac aexp.induct 1);
@@ -29,7 +29,7 @@
    ];
 
 
-Goal "[| b: bexp; sigma: loc -> nat |] ==> \
+Goal "[| b \\<in> bexp; sigma: loc -> nat |] ==> \
 \        <b,sigma> -b-> w <-> B(b,sigma) = w";
 by (res_inst_tac [("x","w")] spec 1);
 by (etac bexp.induct 1);
@@ -42,7 +42,7 @@
 val bexp2 = bexp_iff RS iffD2;
 
 
-Goal "<c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
+Goal "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \\<in> C(c)";
 by (etac evalc.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [bexp1])));
 (* skip *)
@@ -67,7 +67,7 @@
 AddIs  evalc.intrs;
 
 
-Goal "c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
+Goal "c \\<in> com ==> \\<forall>x \\<in> C(c). <c,fst(x)> -c-> snd(x)";
 by (etac com.induct 1);
 (* comp *)
 by (Force_tac 3); 
@@ -90,7 +90,7 @@
 
 (**** Proof of Equivalence ****)
 
-Goal "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
+Goal "\\<forall>c \\<in> com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
 by (fast_tac (claset() addIs [C_subset RS subsetD]
 		       addEs [com2 RS bspec]
 		       addDs [com1]