# HG changeset patch # User lcp # Date 749987296 -3600 # Node ID cebe01deba80257c5a2614ea494387a93bb76b35 # Parent 70c6014c9b6f795f290abeefd4a9d746edbbe8e8 added ~: for "not in" diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/Bool.ML --- 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(); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/Ord.ML --- 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 0 \ + "!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \ \ cons(,f) : inj(cons(a,A), cons(b,B))"; (*cannot use safe_tac: must preserve the implication*) by (etac CollectE 1); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/Univ.ML --- 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 Limit(i)"; + "!!i. [| 0 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); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/ZF.ML --- 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)) ]); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/ZF.thy --- 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) ==> \ diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/bool.ML --- 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(); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/fin.ML --- 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); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/func.ML --- 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(,f) : cons(c,A) -> cons(b,B)"; + "!!f A B. [| f: A->B; c~:A |] ==> cons(,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(,f)`a = f`a"; +goal ZF.thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(,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(,f)`c = b"; +goal ZF.thy "!!f A B. [| f: A->B; c~:A |] ==> cons(,f)`c = b"; by (rtac (consI1 RS apply_equality) 1); by (rtac fun_extend 1); by (REPEAT (assume_tac 1)); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/ord.ML --- 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 0 \ + "!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \ \ cons(,f) : inj(cons(a,A), cons(b,B))"; (*cannot use safe_tac: must preserve the implication*) by (etac CollectE 1); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/univ.ML --- 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 Limit(i)"; + "!!i. [| 0 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); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/upair.ML --- 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 *) diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/zf.ML --- 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)) ]); diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/zf.thy --- 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) ==> \