--- a/src/ZF/Bool.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/Bool.ML Thu Oct 07 10:48:16 1993 +0100
@@ -20,7 +20,7 @@
by (rtac consI1 1);
val bool_0I = result();
-goalw Bool.thy bool_defs "~ 1=0";
+goalw Bool.thy bool_defs "1~=0";
by (rtac succ_not_0 1);
val one_not_0 = result();
--- a/src/ZF/Ord.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/Ord.ML Thu Oct 07 10:48:16 1993 +0100
@@ -380,7 +380,7 @@
by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));
val Ord_0_le = result();
-goal Ord.thy "!!i. [| Ord(i); ~ i=0 |] ==> 0<i";
+goal Ord.thy "!!i. [| Ord(i); i~=0 |] ==> 0<i";
by (etac (not_le_iff_lt RS iffD1) 1);
by (rtac Ord_0 1);
by (fast_tac lt_cs 1);
--- a/src/ZF/Perm.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/Perm.ML Thu Oct 07 10:48:16 1993 +0100
@@ -421,7 +421,7 @@
val inj_succ_restrict = result();
goalw Perm.thy [inj_def]
- "!!f. [| f: inj(A,B); ~ a:A; ~ b:B |] ==> \
+ "!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
(*cannot use safe_tac: must preserve the implication*)
by (etac CollectE 1);
--- a/src/ZF/Univ.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/Univ.ML Thu Oct 07 10:48:16 1993 +0100
@@ -185,7 +185,7 @@
val Limit_nat = result();
goalw Univ.thy [Limit_def]
- "!!i. [| 0<i; ALL y. ~ succ(y)=i |] ==> Limit(i)";
+ "!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)";
by (safe_tac subset_cs);
by (rtac (not_le_iff_lt RS iffD1) 2);
by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
--- a/src/ZF/ZF.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/ZF.ML Thu Oct 07 10:48:16 1993 +0100
@@ -86,7 +86,7 @@
(resolve_tac prems 1) ]);
val ballE = prove_goalw ZF.thy [Ball_def]
- "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"
+ "[| ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"
(fn major::prems=>
[ (rtac (major RS allE) 1),
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
@@ -99,7 +99,7 @@
(*Instantiates x first: better for automatic theorem proving?*)
val rev_ballE = prove_goal ZF.thy
- "[| ALL x:A. P(x); ~ x:A ==> Q; P(x) ==> Q |] ==> Q"
+ "[| ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q"
(fn major::prems=>
[ (rtac (major RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
@@ -157,7 +157,7 @@
(*Classical elimination rule*)
val subsetCE = prove_goalw ZF.thy [subset_def]
- "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"
+ "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
@@ -203,7 +203,7 @@
[ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);
val equalityCE = prove_goal ZF.thy
- "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"
+ "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS equalityE) 1),
(REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);
@@ -360,7 +360,7 @@
(*"Classical" elimination rule -- does not require exhibiting B:C *)
val InterE = prove_goalw ZF.thy [Inter_def]
- "[| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R"
+ "[| A : Inter(C); A:B ==> R; B~:C ==> R |] ==> R"
(fn major::prems=>
[ (rtac (major RS CollectD2 RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
--- a/src/ZF/ZF.thy Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/ZF.thy Thu Oct 07 10:48:16 1993 +0100
@@ -100,6 +100,7 @@
" ->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
":" :: "[i, i] => o" (infixl 50) (*membership relation*)
+ "~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)
translations
@@ -124,6 +125,8 @@
"ALL x:A. P" == "Ball(A, %x. P)"
"EX x:A. P" == "Bex(A, %x. P)"
+ "x ~: y" == "~ (x:y)"
+
rules
@@ -145,7 +148,7 @@
infinity "0:Inf & (ALL y:Inf. succ(y): Inf)"
(*This formulation facilitates case analysis on A. *)
-foundation "A=0 | (EX x:A. ALL y:x. ~ y:A)"
+foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
(* Schema axiom since predicate P is a higher-order variable *)
replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
--- a/src/ZF/bool.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/bool.ML Thu Oct 07 10:48:16 1993 +0100
@@ -20,7 +20,7 @@
by (rtac consI1 1);
val bool_0I = result();
-goalw Bool.thy bool_defs "~ 1=0";
+goalw Bool.thy bool_defs "1~=0";
by (rtac succ_not_0 1);
val one_not_0 = result();
--- a/src/ZF/fin.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/fin.ML Thu Oct 07 10:48:16 1993 +0100
@@ -9,7 +9,7 @@
prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n)
card(0)=0
- [| ~ a:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b))
+ [| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b))
b: Fin(A) ==> inj(b,b)<=surj(b,b)
@@ -42,11 +42,11 @@
(** Induction on finite sets **)
-(*Discharging ~ x:y entails extra work*)
+(*Discharging x~:y entails extra work*)
val major::prems = goal Fin.thy
"[| b: Fin(A); \
\ P(0); \
-\ !!x y. [| x: A; y: Fin(A); ~ x:y; P(y) |] ==> P(cons(x,y)) \
+\ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) \
\ |] ==> P(b)";
by (rtac (major RS Fin.induct) 1);
by (res_inst_tac [("Q","a:b")] (excluded_middle RS disjE) 2);
--- a/src/ZF/func.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/func.ML Thu Oct 07 10:48:16 1993 +0100
@@ -339,20 +339,20 @@
val fun_single_lemma = result();
goalw ZF.thy [cons_def]
- "!!f A B. [| f: A->B; ~c:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
+ "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
by (rtac (fun_single_lemma RS fun_disjoint_Un) 1);
by (assume_tac 1);
by (rtac equals0I 1);
by (fast_tac ZF_cs 1);
val fun_extend = result();
-goal ZF.thy "!!f A B. [| f: A->B; a:A; ~ c:A |] ==> cons(<c,b>,f)`a = f`a";
+goal ZF.thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a";
by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
by (rtac fun_extend 3);
by (REPEAT (assume_tac 1));
val fun_extend_apply1 = result();
-goal ZF.thy "!!f A B. [| f: A->B; ~ c:A |] ==> cons(<c,b>,f)`c = b";
+goal ZF.thy "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b";
by (rtac (consI1 RS apply_equality) 1);
by (rtac fun_extend 1);
by (REPEAT (assume_tac 1));
--- a/src/ZF/ord.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/ord.ML Thu Oct 07 10:48:16 1993 +0100
@@ -380,7 +380,7 @@
by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));
val Ord_0_le = result();
-goal Ord.thy "!!i. [| Ord(i); ~ i=0 |] ==> 0<i";
+goal Ord.thy "!!i. [| Ord(i); i~=0 |] ==> 0<i";
by (etac (not_le_iff_lt RS iffD1) 1);
by (rtac Ord_0 1);
by (fast_tac lt_cs 1);
--- a/src/ZF/perm.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/perm.ML Thu Oct 07 10:48:16 1993 +0100
@@ -421,7 +421,7 @@
val inj_succ_restrict = result();
goalw Perm.thy [inj_def]
- "!!f. [| f: inj(A,B); ~ a:A; ~ b:B |] ==> \
+ "!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
(*cannot use safe_tac: must preserve the implication*)
by (etac CollectE 1);
--- a/src/ZF/univ.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/univ.ML Thu Oct 07 10:48:16 1993 +0100
@@ -185,7 +185,7 @@
val Limit_nat = result();
goalw Univ.thy [Limit_def]
- "!!i. [| 0<i; ALL y. ~ succ(y)=i |] ==> Limit(i)";
+ "!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)";
by (safe_tac subset_cs);
by (rtac (not_le_iff_lt RS iffD1) 2);
by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
--- a/src/ZF/upair.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/upair.ML Thu Oct 07 10:48:16 1993 +0100
@@ -56,7 +56,7 @@
(fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]);
(*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal ZF.thy "(~c : B ==> c : A) ==> c : A Un B"
+val UnCI = prove_goal ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
(fn [prem]=>
[ (rtac (disjCI RS (Un_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -91,7 +91,7 @@
(*** Rules for set difference -- defined via Upair ***)
val DiffI = prove_goalw ZF.thy [Diff_def]
- "[| c : A; ~ c : B |] ==> c : A - B"
+ "[| c : A; c ~: B |] ==> c : A - B"
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]);
val DiffD1 = prove_goalw ZF.thy [Diff_def]
@@ -103,12 +103,12 @@
(fn [major,minor]=> [ (rtac (minor RS (major RS CollectD2 RS notE)) 1) ]);
val DiffE = prove_goal ZF.thy
- "[| c : A - B; [| c:A; ~ c:B |] ==> P |] ==> P"
+ "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"
(fn prems=>
[ (resolve_tac prems 1),
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
-val Diff_iff = prove_goal ZF.thy "c : A-B <-> (c:A & ~ c:B)"
+val Diff_iff = prove_goal ZF.thy "c : A-B <-> (c:A & c~:B)"
(fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
(*** Rules for cons -- defined via Un and Upair ***)
@@ -129,7 +129,7 @@
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]);
(*Classical introduction rule*)
-val consCI = prove_goal ZF.thy "(~ a:B ==> a=b) ==> a: cons(b,B)"
+val consCI = prove_goal ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
(fn [prem]=>
[ (rtac (disjCI RS (cons_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -223,7 +223,7 @@
val mem_anti_refl = prove_goal ZF.thy "a:a ==> P"
(fn [major]=> [ (rtac (major RS (major RS mem_anti_sym)) 1) ]);
-val mem_not_refl = prove_goal ZF.thy "~ a:a"
+val mem_not_refl = prove_goal ZF.thy "a~:a"
(K [ (rtac notI 1), (etac mem_anti_refl 1) ]);
(*** Rules for succ ***)
@@ -245,7 +245,7 @@
(fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]);
(*Classical introduction rule*)
-val succCI = prove_goal ZF.thy "(~ i:j ==> i=j) ==> i: succ(j)"
+val succCI = prove_goal ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
(fn [prem]=>
[ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -256,7 +256,7 @@
(rtac succI1 1) ]);
(*Useful for rewriting*)
-val succ_not_0 = prove_goal ZF.thy "~ succ(n)=0"
+val succ_not_0 = prove_goal ZF.thy "succ(n) ~= 0"
(fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]);
(* succ(c) <= B ==> c : B *)
--- a/src/ZF/zf.ML Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/zf.ML Thu Oct 07 10:48:16 1993 +0100
@@ -86,7 +86,7 @@
(resolve_tac prems 1) ]);
val ballE = prove_goalw ZF.thy [Ball_def]
- "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"
+ "[| ALL x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"
(fn major::prems=>
[ (rtac (major RS allE) 1),
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
@@ -99,7 +99,7 @@
(*Instantiates x first: better for automatic theorem proving?*)
val rev_ballE = prove_goal ZF.thy
- "[| ALL x:A. P(x); ~ x:A ==> Q; P(x) ==> Q |] ==> Q"
+ "[| ALL x:A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q"
(fn major::prems=>
[ (rtac (major RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
@@ -157,7 +157,7 @@
(*Classical elimination rule*)
val subsetCE = prove_goalw ZF.thy [subset_def]
- "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"
+ "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
@@ -203,7 +203,7 @@
[ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);
val equalityCE = prove_goal ZF.thy
- "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"
+ "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS equalityE) 1),
(REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);
@@ -360,7 +360,7 @@
(*"Classical" elimination rule -- does not require exhibiting B:C *)
val InterE = prove_goalw ZF.thy [Inter_def]
- "[| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R"
+ "[| A : Inter(C); A:B ==> R; B~:C ==> R |] ==> R"
(fn major::prems=>
[ (rtac (major RS CollectD2 RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
--- a/src/ZF/zf.thy Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/zf.thy Thu Oct 07 10:48:16 1993 +0100
@@ -100,6 +100,7 @@
" ->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
":" :: "[i, i] => o" (infixl 50) (*membership relation*)
+ "~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)
translations
@@ -124,6 +125,8 @@
"ALL x:A. P" == "Ball(A, %x. P)"
"EX x:A. P" == "Bex(A, %x. P)"
+ "x ~: y" == "~ (x:y)"
+
rules
@@ -145,7 +148,7 @@
infinity "0:Inf & (ALL y:Inf. succ(y): Inf)"
(*This formulation facilitates case analysis on A. *)
-foundation "A=0 | (EX x:A. ALL y:x. ~ y:A)"
+foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
(* Schema axiom since predicate P is a higher-order variable *)
replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \