--- a/HOL.thy Mon Oct 04 15:43:54 1993 +0100
+++ b/HOL.thy Thu Oct 07 10:20:30 1993 +0100
@@ -54,7 +54,7 @@
(* Infixes *)
o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50)
- "=" :: "['a, 'a] => bool" (infixl 50)
+ "=", "~=" :: "['a, 'a] => bool" (infixl 50)
"&" :: "[bool, bool] => bool" (infixr 35)
"|" :: "[bool, bool] => bool" (infixr 30)
"-->" :: "[bool, bool] => bool" (infixr 25)
@@ -65,10 +65,6 @@
"-" :: "['a::minus, 'a] => 'a" (infixl 65)
"*" :: "['a::times, 'a] => 'a" (infixl 70)
- (* Rewriting Gadget *)
-
- NORM :: "'a => 'a"
-
translations
"THE xs. P" => "@ xs. P"
@@ -76,6 +72,7 @@
"EX xs. P" => "? xs. P"
"EX! xs. P" => "?! xs. P"
+ "x ~= y" == "~ (x=y)"
"let x = s in t" == "Let(s, %x. t)"
rules
@@ -116,10 +113,6 @@
if_def "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
- (* Rewriting -- special constant to flag normalized terms *)
-
- NORM_def "NORM(x) = x"
-
end
--- a/List.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/List.ML Thu Oct 07 10:20:30 1993 +0100
@@ -96,7 +96,7 @@
(** Distinctness of constructors **)
-goalw List.thy [NIL_def,CONS_def] "~ CONS(M,N) = NIL";
+goalw List.thy [NIL_def,CONS_def] "CONS(M,N) ~= NIL";
by (rtac In1_not_In0 1);
val CONS_not_NIL = result();
val NIL_not_CONS = standard (CONS_not_NIL RS not_sym);
@@ -104,7 +104,7 @@
val CONS_neq_NIL = standard (CONS_not_NIL RS notE);
val NIL_neq_CONS = sym RS CONS_neq_NIL;
-goalw List.thy [Nil_def,Cons_def] "~ Cons(x,xs) = Nil";
+goalw List.thy [Nil_def,Cons_def] "Cons(x,xs) ~= Nil";
by (rtac (CONS_not_NIL RS (inj_onto_Abs_List RS inj_onto_contraD)) 1);
by (REPEAT (resolve_tac [rangeI, NIL_I, CONS_I, Rep_List] 1));
val Cons_not_Nil = result();
@@ -152,12 +152,12 @@
NIL_I, CONS_I];
val list_free_ss = HOL_ss addsimps list_free_simps;
-goal List.thy "!!N. N: List(A) ==> !M. ~ N = CONS(M,N)";
+goal List.thy "!!N. N: List(A) ==> !M. N ~= CONS(M,N)";
by (etac List_induct 1);
by (ALLGOALS (asm_simp_tac list_free_ss));
val not_CONS_self = result();
-goal List.thy "!x. ~ l=Cons(x,l)";
+goal List.thy "!x. l ~= Cons(x,l)";
by (list_ind_tac "l" 1);
by (ALLGOALS (asm_simp_tac list_free_ss));
val not_Cons_self = result();
--- a/Nat.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/Nat.ML Thu Oct 07 10:20:30 1993 +0100
@@ -90,7 +90,7 @@
(*** Distinctness of constructors ***)
-goalw Nat.thy [Zero_def,Suc_def] "~ Suc(m)=0";
+goalw Nat.thy [Zero_def,Suc_def] "Suc(m) ~= 0";
by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
by (rtac Suc_Rep_not_Zero_Rep 1);
by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
@@ -117,7 +117,7 @@
by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]);
val Suc_Suc_eq = result();
-goal Nat.thy "~ n=Suc(n)";
+goal Nat.thy "n ~= Suc(n)";
by (nat_ind_tac "n" 1);
by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [Zero_not_Suc,Suc_Suc_eq])));
val n_not_Suc_n = result();
--- a/Set.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/Set.ML Thu Oct 07 10:20:30 1993 +0100
@@ -42,7 +42,7 @@
val bspec = result();
val major::prems = goalw Set.thy [Ball_def]
- "[| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q";
+ "[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q";
by (rtac (major RS spec RS impCE) 1);
by (REPEAT (eresolve_tac prems 1));
val ballE = result();
@@ -109,7 +109,7 @@
(*Classical elimination rule*)
val major::prems = goalw Set.thy [subset_def]
- "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P";
+ "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P";
by (rtac (major RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
val subsetCE = result();
@@ -153,7 +153,7 @@
val equalityE = result();
val major::prems = goal Set.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";
by (rtac (major RS equalityE) 1);
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
val equalityCE = result();
@@ -179,7 +179,7 @@
Negated assumptions behave like formulae on the right side of the notional
turnstile...*)
val major::prems = goalw Set.thy [Compl_def]
- "[| c : Compl(A) |] ==> ~c:A";
+ "[| c : Compl(A) |] ==> c~:A";
by (rtac (major RS CollectD) 1);
val ComplD = result();
@@ -197,7 +197,7 @@
val UnI2 = result();
(*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal Set.thy "(~c:B ==> c:A) ==> c : A Un B"
+val UnCI = prove_goal Set.thy "(c~:B ==> c:A) ==> c : A Un B"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
@@ -236,7 +236,7 @@
(*** Set difference ***)
val DiffI = prove_goalw Set.thy [set_diff_def]
- "[| c : A; ~ c : B |] ==> c : A - B"
+ "[| c : A; c ~: B |] ==> c : A - B"
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]);
val DiffD1 = prove_goalw Set.thy [set_diff_def]
@@ -249,12 +249,12 @@
[rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]);
val DiffE = prove_goal Set.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 Set.thy "(c : A-B) = (c:A & ~ c:B)"
+val Diff_iff = prove_goal Set.thy "(c : A-B) = (c:A & c~:B)"
(fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
@@ -294,7 +294,7 @@
(fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]);
(*Classical introduction rule*)
-val insertCI = prove_goal Set.thy "(~a:B ==> a=b) ==> a: insert(b,B)"
+val insertCI = prove_goal Set.thy "(a~:B ==> a=b) ==> a: insert(b,B)"
(fn [prem]=>
[ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -358,7 +358,7 @@
(*"Classical" elimination -- by the Excluded Middle on a:A *)
val major::prems = goalw Set.thy [INTER_def]
- "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R";
+ "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R";
by (rtac (major RS CollectD RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
val INT_E = result();
@@ -430,7 +430,7 @@
(*"Classical" elimination rule -- does not require proving X:C *)
val major::prems = goalw Set.thy [Inter_def]
- "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R";
+ "[| A : Inter(C); A:X ==> R; X~:C ==> R |] ==> R";
by (rtac (major RS INT_E) 1);
by (REPEAT (eresolve_tac prems 1));
val InterE = result();
--- a/Set.thy Mon Oct 04 15:43:54 1993 +0100
+++ b/Set.thy Thu Oct 07 10:20:30 1993 +0100
@@ -19,20 +19,20 @@
(* Constants *)
- Collect :: "('a => bool) => 'a set" (*comprehension*)
- Compl :: "('a set) => 'a set" (*complement*)
- Int :: "['a set, 'a set] => 'a set" (infixl 70)
- Un :: "['a set, 'a set] => 'a set" (infixl 65)
- UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)
- UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
- INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
- Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
- range :: "('a => 'b) => 'b set" (*of function*)
- Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
- inj, surj :: "('a => 'b) => bool" (*injective/surjective*)
+ Collect :: "('a => bool) => 'a set" (*comprehension*)
+ Compl :: "('a set) => 'a set" (*complement*)
+ Int :: "['a set, 'a set] => 'a set" (infixl 70)
+ Un :: "['a set, 'a set] => 'a set" (infixl 65)
+ UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)
+ UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
+ INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
+ Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
+ range :: "('a => 'b) => 'b set" (*of function*)
+ Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
+ inj, surj :: "('a => 'b) => bool" (*inj/surjective*)
inj_onto :: "['a => 'b, 'a set] => bool"
- "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90)
- ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*)
+ "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90)
+ ":", "~:" :: "['a, 'a set] => bool" (infixl 50) (*membership*)
(* Finite Sets *)
@@ -43,7 +43,7 @@
(** Binding Constants **)
- "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
+ "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
(* Big Intersection / Union *)
@@ -67,6 +67,8 @@
"ALL x:A. P" => "Ball(A, %x. P)"
"EX x:A. P" => "Bex(A, %x. P)"
+ "x ~: y" == "~ (x:y)"
+
"{x, xs}" == "insert(x, {xs})"
"{x}" == "insert(x, {})"
--- a/Sum.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/Sum.ML Thu Oct 07 10:20:30 1993 +0100
@@ -26,14 +26,14 @@
(** Distinctness of Inl and Inr **)
-goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "~ (Inl_Rep(a) = Inr_Rep(b))";
+goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
by (EVERY1 [rtac notI,
etac (fun_cong RS fun_cong RS fun_cong RS iffE),
rtac (notE RS ccontr), etac (mp RS conjunct2),
REPEAT o (ares_tac [refl,conjI]) ]);
val Inl_Rep_not_Inr_Rep = result();
-goalw Sum.thy [Inl_def,Inr_def] "~ Inl(a)=Inr(b)";
+goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1);
by (rtac Inl_Rep_not_Inr_Rep 1);
by (rtac Inl_RepI 1);
--- a/Univ.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/Univ.ML Thu Oct 07 10:20:30 1993 +0100
@@ -123,7 +123,7 @@
(** Scons vs Atom **)
-goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "~ ((M.N) = Atom(a))";
+goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M.N) ~= Atom(a)";
by (rtac notI 1);
by (etac (equalityD2 RS subsetD RS UnE) 1);
by (rtac singletonI 1);
@@ -223,7 +223,7 @@
(** Scons vs Leaf **)
-goalw Univ.thy [Leaf_def] "~ ((M.N) = Leaf(a))";
+goalw Univ.thy [Leaf_def] "(M.N) ~= Leaf(a)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Leaf = result();
@@ -234,7 +234,7 @@
(** Scons vs Numb **)
-goalw Univ.thy [Numb_def] "~ ((M.N) = Numb(k))";
+goalw Univ.thy [Numb_def] "(M.N) ~= Numb(k)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Numb = result();
@@ -245,7 +245,7 @@
(** Leaf vs Numb **)
-goalw Univ.thy [Leaf_def,Numb_def] "~ (Leaf(a) = Numb(k))";
+goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
by (simp_tac (HOL_ss addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
val Leaf_not_Numb = result();
val Numb_not_Leaf = standard (Leaf_not_Numb RS not_sym);
@@ -267,7 +267,7 @@
by (etac less_zeroE 1);
val ndepth_K0 = result();
-goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> ~ nat_case(k, Suc(i), f) = 0";
+goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case(k, Suc(i), f) ~= 0";
by (nat_ind_tac "k" 1);
by (ALLGOALS (simp_tac nat_ss));
by (rtac impI 1);
@@ -393,7 +393,7 @@
(** Injection **)
-goalw Univ.thy [In0_def,In1_def] "~ (In0(M) = In1(N))";
+goalw Univ.thy [In0_def,In1_def] "In0(M) ~= In1(N)";
by (rtac notI 1);
by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
val In0_not_In1 = result();
--- a/hol.thy Mon Oct 04 15:43:54 1993 +0100
+++ b/hol.thy Thu Oct 07 10:20:30 1993 +0100
@@ -54,7 +54,7 @@
(* Infixes *)
o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50)
- "=" :: "['a, 'a] => bool" (infixl 50)
+ "=", "~=" :: "['a, 'a] => bool" (infixl 50)
"&" :: "[bool, bool] => bool" (infixr 35)
"|" :: "[bool, bool] => bool" (infixr 30)
"-->" :: "[bool, bool] => bool" (infixr 25)
@@ -65,10 +65,6 @@
"-" :: "['a::minus, 'a] => 'a" (infixl 65)
"*" :: "['a::times, 'a] => 'a" (infixl 70)
- (* Rewriting Gadget *)
-
- NORM :: "'a => 'a"
-
translations
"THE xs. P" => "@ xs. P"
@@ -76,6 +72,7 @@
"EX xs. P" => "? xs. P"
"EX! xs. P" => "?! xs. P"
+ "x ~= y" == "~ (x=y)"
"let x = s in t" == "Let(s, %x. t)"
rules
@@ -116,10 +113,6 @@
if_def "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
- (* Rewriting -- special constant to flag normalized terms *)
-
- NORM_def "NORM(x) = x"
-
end
--- a/nat.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/nat.ML Thu Oct 07 10:20:30 1993 +0100
@@ -90,7 +90,7 @@
(*** Distinctness of constructors ***)
-goalw Nat.thy [Zero_def,Suc_def] "~ Suc(m)=0";
+goalw Nat.thy [Zero_def,Suc_def] "Suc(m) ~= 0";
by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
by (rtac Suc_Rep_not_Zero_Rep 1);
by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
@@ -117,7 +117,7 @@
by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]);
val Suc_Suc_eq = result();
-goal Nat.thy "~ n=Suc(n)";
+goal Nat.thy "n ~= Suc(n)";
by (nat_ind_tac "n" 1);
by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [Zero_not_Suc,Suc_Suc_eq])));
val n_not_Suc_n = result();
--- a/set.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/set.ML Thu Oct 07 10:20:30 1993 +0100
@@ -42,7 +42,7 @@
val bspec = result();
val major::prems = goalw Set.thy [Ball_def]
- "[| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q";
+ "[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q";
by (rtac (major RS spec RS impCE) 1);
by (REPEAT (eresolve_tac prems 1));
val ballE = result();
@@ -109,7 +109,7 @@
(*Classical elimination rule*)
val major::prems = goalw Set.thy [subset_def]
- "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P";
+ "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P";
by (rtac (major RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
val subsetCE = result();
@@ -153,7 +153,7 @@
val equalityE = result();
val major::prems = goal Set.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";
by (rtac (major RS equalityE) 1);
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
val equalityCE = result();
@@ -179,7 +179,7 @@
Negated assumptions behave like formulae on the right side of the notional
turnstile...*)
val major::prems = goalw Set.thy [Compl_def]
- "[| c : Compl(A) |] ==> ~c:A";
+ "[| c : Compl(A) |] ==> c~:A";
by (rtac (major RS CollectD) 1);
val ComplD = result();
@@ -197,7 +197,7 @@
val UnI2 = result();
(*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal Set.thy "(~c:B ==> c:A) ==> c : A Un B"
+val UnCI = prove_goal Set.thy "(c~:B ==> c:A) ==> c : A Un B"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
@@ -236,7 +236,7 @@
(*** Set difference ***)
val DiffI = prove_goalw Set.thy [set_diff_def]
- "[| c : A; ~ c : B |] ==> c : A - B"
+ "[| c : A; c ~: B |] ==> c : A - B"
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]);
val DiffD1 = prove_goalw Set.thy [set_diff_def]
@@ -249,12 +249,12 @@
[rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]);
val DiffE = prove_goal Set.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 Set.thy "(c : A-B) = (c:A & ~ c:B)"
+val Diff_iff = prove_goal Set.thy "(c : A-B) = (c:A & c~:B)"
(fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
@@ -294,7 +294,7 @@
(fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]);
(*Classical introduction rule*)
-val insertCI = prove_goal Set.thy "(~a:B ==> a=b) ==> a: insert(b,B)"
+val insertCI = prove_goal Set.thy "(a~:B ==> a=b) ==> a: insert(b,B)"
(fn [prem]=>
[ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
(etac prem 1) ]);
@@ -358,7 +358,7 @@
(*"Classical" elimination -- by the Excluded Middle on a:A *)
val major::prems = goalw Set.thy [INTER_def]
- "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R";
+ "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R";
by (rtac (major RS CollectD RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
val INT_E = result();
@@ -430,7 +430,7 @@
(*"Classical" elimination rule -- does not require proving X:C *)
val major::prems = goalw Set.thy [Inter_def]
- "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R";
+ "[| A : Inter(C); A:X ==> R; X~:C ==> R |] ==> R";
by (rtac (major RS INT_E) 1);
by (REPEAT (eresolve_tac prems 1));
val InterE = result();
--- a/set.thy Mon Oct 04 15:43:54 1993 +0100
+++ b/set.thy Thu Oct 07 10:20:30 1993 +0100
@@ -19,20 +19,20 @@
(* Constants *)
- Collect :: "('a => bool) => 'a set" (*comprehension*)
- Compl :: "('a set) => 'a set" (*complement*)
- Int :: "['a set, 'a set] => 'a set" (infixl 70)
- Un :: "['a set, 'a set] => 'a set" (infixl 65)
- UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)
- UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
- INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
- Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
- range :: "('a => 'b) => 'b set" (*of function*)
- Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
- inj, surj :: "('a => 'b) => bool" (*injective/surjective*)
+ Collect :: "('a => bool) => 'a set" (*comprehension*)
+ Compl :: "('a set) => 'a set" (*complement*)
+ Int :: "['a set, 'a set] => 'a set" (infixl 70)
+ Un :: "['a set, 'a set] => 'a set" (infixl 65)
+ UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)
+ UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
+ INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
+ Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
+ range :: "('a => 'b) => 'b set" (*of function*)
+ Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
+ inj, surj :: "('a => 'b) => bool" (*inj/surjective*)
inj_onto :: "['a => 'b, 'a set] => bool"
- "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90)
- ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*)
+ "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90)
+ ":", "~:" :: "['a, 'a set] => bool" (infixl 50) (*membership*)
(* Finite Sets *)
@@ -43,7 +43,7 @@
(** Binding Constants **)
- "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
+ "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
(* Big Intersection / Union *)
@@ -67,6 +67,8 @@
"ALL x:A. P" => "Ball(A, %x. P)"
"EX x:A. P" => "Bex(A, %x. P)"
+ "x ~: y" == "~ (x:y)"
+
"{x, xs}" == "insert(x, {xs})"
"{x}" == "insert(x, {})"
--- a/sum.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/sum.ML Thu Oct 07 10:20:30 1993 +0100
@@ -26,14 +26,14 @@
(** Distinctness of Inl and Inr **)
-goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "~ (Inl_Rep(a) = Inr_Rep(b))";
+goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
by (EVERY1 [rtac notI,
etac (fun_cong RS fun_cong RS fun_cong RS iffE),
rtac (notE RS ccontr), etac (mp RS conjunct2),
REPEAT o (ares_tac [refl,conjI]) ]);
val Inl_Rep_not_Inr_Rep = result();
-goalw Sum.thy [Inl_def,Inr_def] "~ Inl(a)=Inr(b)";
+goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1);
by (rtac Inl_Rep_not_Inr_Rep 1);
by (rtac Inl_RepI 1);
--- a/univ.ML Mon Oct 04 15:43:54 1993 +0100
+++ b/univ.ML Thu Oct 07 10:20:30 1993 +0100
@@ -123,7 +123,7 @@
(** Scons vs Atom **)
-goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "~ ((M.N) = Atom(a))";
+goalw Univ.thy [Atom_def,Scons_def,Push_Node_def] "(M.N) ~= Atom(a)";
by (rtac notI 1);
by (etac (equalityD2 RS subsetD RS UnE) 1);
by (rtac singletonI 1);
@@ -223,7 +223,7 @@
(** Scons vs Leaf **)
-goalw Univ.thy [Leaf_def] "~ ((M.N) = Leaf(a))";
+goalw Univ.thy [Leaf_def] "(M.N) ~= Leaf(a)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Leaf = result();
@@ -234,7 +234,7 @@
(** Scons vs Numb **)
-goalw Univ.thy [Numb_def] "~ ((M.N) = Numb(k))";
+goalw Univ.thy [Numb_def] "(M.N) ~= Numb(k)";
by (stac o_def 1);
by (rtac Scons_not_Atom 1);
val Scons_not_Numb = result();
@@ -245,7 +245,7 @@
(** Leaf vs Numb **)
-goalw Univ.thy [Leaf_def,Numb_def] "~ (Leaf(a) = Numb(k))";
+goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
by (simp_tac (HOL_ss addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
val Leaf_not_Numb = result();
val Numb_not_Leaf = standard (Leaf_not_Numb RS not_sym);
@@ -267,7 +267,7 @@
by (etac less_zeroE 1);
val ndepth_K0 = result();
-goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> ~ nat_case(k, Suc(i), f) = 0";
+goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case(k, Suc(i), f) ~= 0";
by (nat_ind_tac "k" 1);
by (ALLGOALS (simp_tac nat_ss));
by (rtac impI 1);
@@ -393,7 +393,7 @@
(** Injection **)
-goalw Univ.thy [In0_def,In1_def] "~ (In0(M) = In1(N))";
+goalw Univ.thy [In0_def,In1_def] "In0(M) ~= In1(N)";
by (rtac notI 1);
by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
val In0_not_In1 = result();