--- 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";
--- 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"];
--- 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 "
--- 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";
--- 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))"
--- 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]