--- a/src/HOL/Datatype_Universe.thy Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Datatype_Universe.thy Tue Jan 09 15:22:13 2001 +0100
@@ -63,7 +63,7 @@
(*S-expression constructors*)
Atom_def "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
- Scons_def "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
+ Scons_def "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr 2) ` N)"
(*Leaf nodes, with arbitrary or nat labels*)
Leaf_def "Leaf == Atom o Inl"
@@ -74,7 +74,7 @@
In1_def "In1(M) == Scons (Numb 1) M"
(*Function spaces*)
- Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
+ Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
Funs_def "Funs S == {f. range f <= S}"
(*the set of nodes with depth less than k*)
@@ -83,7 +83,7 @@
(*products and sums for the "universe"*)
uprod_def "uprod A B == UN x:A. UN y:B. { Scons x y }"
- usum_def "usum A B == In0``A Un In1``B"
+ usum_def "usum A B == In0`A Un In1`B"
(*the corresponding eliminators*)
Split_def "Split c M == @u. ? x y. M = Scons x y & u = c x y"
--- a/src/HOL/Finite.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Finite.ML Tue Jan 09 15:22:13 2001 +0100
@@ -74,7 +74,7 @@
Addsimps[finite_insert];
(*The image of a finite set is finite *)
-Goal "finite F ==> finite(h``F)";
+Goal "finite F ==> finite(h`F)";
by (etac finite_induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
@@ -127,11 +127,11 @@
val lemma = result();
(*Lemma for proving finite_imageD*)
-Goal "finite B ==> ALL A. f``A = B --> inj_on f A --> finite A";
+Goal "finite B ==> ALL A. f`A = B --> inj_on f A --> finite A";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
-by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
+by (subgoal_tac "EX y:A. f y = x & F = f`(A-{y})" 1);
by (Clarify_tac 1);
by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
by (blast_tac (claset() addSDs [lemma RS iffD1]) 1);
@@ -143,7 +143,7 @@
(asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
val lemma = result();
-Goal "[| finite(f``A); inj_on f A |] ==> finite A";
+Goal "[| finite(f`A); inj_on f A |] ==> finite A";
by (dtac lemma 1);
by (Blast_tac 1);
qed "finite_imageD";
@@ -195,7 +195,7 @@
(** The powerset of a finite set **)
Goal "finite(Pow A) ==> finite A";
-by (subgoal_tac "finite ((%x.{x})``A)" 1);
+by (subgoal_tac "finite ((%x.{x})`A)" 1);
by (rtac finite_subset 2);
by (assume_tac 3);
by (ALLGOALS
@@ -214,7 +214,7 @@
AddIffs [finite_Pow_iff];
Goal "finite(r^-1) = finite r";
-by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
+by (subgoal_tac "r^-1 = (%(x,y).(y,x))`r" 1);
by (Asm_simp_tac 1);
by (rtac iffI 1);
by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
@@ -467,14 +467,14 @@
(*** Cardinality of image ***)
-Goal "finite A ==> card (f `` A) <= card A";
+Goal "finite A ==> card (f ` A) <= card A";
by (etac finite_induct 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [le_SucI, finite_imageI,
card_insert_if]) 1);
qed "card_image_le";
-Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
+Goal "finite(A) ==> inj_on f A --> card (f ` A) = card A";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by Safe_tac;
@@ -486,7 +486,7 @@
by (Blast_tac 1);
qed_spec_mp "card_image";
-Goal "[| finite A; f``A <= A; inj_on f A |] ==> f``A = A";
+Goal "[| finite A; f`A <= A; inj_on f A |] ==> f`A = A";
by (asm_simp_tac (simpset() addsimps [card_seteq, card_image]) 1);
qed "endo_inj_surj";
@@ -853,14 +853,14 @@
by (auto_tac (claset() addIs [finite_subset], simpset()));
qed "choose_deconstruct";
-Goal "[| finite(A); finite(B); f``A <= B; inj_on f A |] \
+Goal "[| finite(A); finite(B); f`A <= B; inj_on f A |] \
\ ==> card A <= card B";
by (auto_tac (claset() addIs [card_mono],
simpset() addsimps [card_image RS sym]));
qed "card_inj_on_le";
Goal "[| finite A; finite B; \
-\ f``A <= B; inj_on f A; g``B <= A; inj_on g B |] \
+\ f`A <= B; inj_on f A; g`B <= A; inj_on g B |] \
\ ==> card(A) = card(B)";
by (auto_tac (claset() addIs [le_anti_sym,card_inj_on_le], simpset()));
qed "card_bij_eq";
--- a/src/HOL/Fun.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Fun.ML Tue Jan 09 15:22:13 2001 +0100
@@ -65,15 +65,15 @@
qed "o_id";
Addsimps [o_id];
-Goalw [o_def] "(f o g)``r = f``(g``r)";
+Goalw [o_def] "(f o g)`r = f`(g`r)";
by (Blast_tac 1);
qed "image_compose";
-Goal "f``A = (UN x:A. {f x})";
+Goal "f`A = (UN x:A. {f x})";
by (Blast_tac 1);
qed "image_eq_UN";
-Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
+Goalw [o_def] "UNION A (g o f) = UNION (f`A) g";
by (Blast_tac 1);
qed "UN_o";
@@ -205,7 +205,7 @@
(*** Lemmas about injective functions and inv ***)
-Goalw [o_def] "[| inj_on f A; inj_on g (f``A) |] ==> inj_on (g o f) A";
+Goalw [o_def] "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A";
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
qed "comp_inj_on";
@@ -288,147 +288,147 @@
(** We seem to need both the id-forms and the (%x. x) forms; the latter can
arise by rewriting, while id may be used explicitly. **)
-Goal "(%x. x) `` Y = Y";
+Goal "(%x. x) ` Y = Y";
by (Blast_tac 1);
qed "image_ident";
-Goalw [id_def] "id `` Y = Y";
+Goalw [id_def] "id ` Y = Y";
by (Blast_tac 1);
qed "image_id";
Addsimps [image_ident, image_id];
-Goal "(%x. x) -`` Y = Y";
+Goal "(%x. x) -` Y = Y";
by (Blast_tac 1);
qed "vimage_ident";
-Goalw [id_def] "id -`` A = A";
+Goalw [id_def] "id -` A = A";
by Auto_tac;
qed "vimage_id";
Addsimps [vimage_ident, vimage_id];
-Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}";
+Goal "f -` (f ` A) = {y. EX x:A. f x = f y}";
by (blast_tac (claset() addIs [sym]) 1);
qed "vimage_image_eq";
-Goal "f `` (f -`` A) <= A";
+Goal "f ` (f -` A) <= A";
by (Blast_tac 1);
qed "image_vimage_subset";
-Goal "f `` (f -`` A) = A Int range f";
+Goal "f ` (f -` A) = A Int range f";
by (Blast_tac 1);
qed "image_vimage_eq";
Addsimps [image_vimage_eq];
-Goal "surj f ==> f `` (f -`` A) = A";
+Goal "surj f ==> f ` (f -` A) = A";
by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
qed "surj_image_vimage_eq";
-Goal "surj f ==> f `` (inv f `` A) = A";
+Goal "surj f ==> f ` (inv f ` A) = A";
by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
qed "image_surj_f_inv_f";
-Goalw [inj_on_def] "inj f ==> f -`` (f `` A) = A";
+Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
by (Blast_tac 1);
qed "inj_vimage_image_eq";
-Goal "inj f ==> (inv f) `` (f `` A) = A";
+Goal "inj f ==> (inv f) ` (f ` A) = A";
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
qed "image_inv_f_f";
-Goalw [surj_def] "surj f ==> f -`` B <= A ==> B <= f `` A";
+Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
by (blast_tac (claset() addIs [sym]) 1);
qed "vimage_subsetD";
-Goalw [inj_on_def] "inj f ==> B <= f `` A ==> f -`` B <= A";
+Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A";
by (Blast_tac 1);
qed "vimage_subsetI";
-Goalw [bij_def] "bij f ==> (f -`` B <= A) = (B <= f `` A)";
+Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)";
by (blast_tac (claset() delrules [subsetI]
addIs [vimage_subsetI, vimage_subsetD]) 1);
qed "vimage_subset_eq";
-Goal "f``(A Int B) <= f``A Int f``B";
+Goal "f`(A Int B) <= f`A Int f`B";
by (Blast_tac 1);
qed "image_Int_subset";
-Goal "f``A - f``B <= f``(A - B)";
+Goal "f`A - f`B <= f`(A - B)";
by (Blast_tac 1);
qed "image_diff_subset";
Goalw [inj_on_def]
- "[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B";
+ "[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B";
by (Blast_tac 1);
qed "inj_on_image_Int";
Goalw [inj_on_def]
- "[| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B";
+ "[| inj_on f C; A<=C; B<=C |] ==> f`(A-B) = f`A - f`B";
by (Blast_tac 1);
qed "inj_on_image_set_diff";
-Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
+Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B";
by (Blast_tac 1);
qed "image_Int";
-Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
+Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B";
by (Blast_tac 1);
qed "image_set_diff";
-Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
+Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
by Auto_tac;
qed "inv_image_comp";
-Goal "inj f ==> (f a : f``A) = (a : A)";
+Goal "inj f ==> (f a : f`A) = (a : A)";
by (blast_tac (claset() addDs [injD]) 1);
qed "inj_image_mem_iff";
-Goalw [inj_on_def] "inj f ==> (f``A <= f``B) = (A<=B)";
+Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)";
by (Blast_tac 1);
qed "inj_image_subset_iff";
-Goal "inj f ==> (f``A = f``B) = (A = B)";
+Goal "inj f ==> (f`A = f`B) = (A = B)";
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
qed "inj_image_eq_iff";
-Goal "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
+Goal "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
by (Blast_tac 1);
qed "image_UN";
(*injectivity's required. Left-to-right inclusion holds even if A is empty*)
Goalw [inj_on_def]
"[| inj_on f C; ALL x:A. B x <= C; j:A |] \
-\ ==> f `` (INTER A B) = (INT x:A. f `` B x)";
+\ ==> f ` (INTER A B) = (INT x:A. f ` B x)";
by (Blast_tac 1);
qed "image_INT";
(*Compare with image_INT: no use of inj_on, and if f is surjective then
it doesn't matter whether A is empty*)
-Goalw [bij_def] "bij f ==> f `` (INTER A B) = (INT x:A. f `` B x)";
+Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI],
simpset()) 1);
qed "bij_image_INT";
-Goal "bij f ==> f `` Collect P = {y. P (inv f y)}";
+Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
by Auto_tac;
by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
qed "bij_image_Collect_eq";
-Goal "bij f ==> f -`` A = inv f `` A";
+Goal "bij f ==> f -` A = inv f ` A";
by Safe_tac;
by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
qed "bij_vimage_eq_inv_image";
-Goal "surj f ==> -(f``A) <= f``(-A)";
+Goal "surj f ==> -(f`A) <= f`(-A)";
by (auto_tac (claset(), simpset() addsimps [surj_def]));
qed "surj_Compl_image_subset";
-Goal "inj f ==> f``(-A) <= -(f``A)";
+Goal "inj f ==> f`(-A) <= -(f`A)";
by (auto_tac (claset(), simpset() addsimps [inj_on_def]));
qed "inj_image_Compl_subset";
-Goalw [bij_def] "bij f ==> f``(-A) = -(f``A)";
+Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)";
by (rtac equalityI 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset,
surj_Compl_image_subset])));
@@ -552,13 +552,13 @@
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
qed "compose_eq";
-Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
-\ ==> compose A g f `` A = C";
+Goal "[| f : A funcset B; f ` A = B; g: B funcset C; g ` B = C |]\
+\ ==> compose A g f ` A = C";
by (auto_tac (claset(),
simpset() addsimps [image_def, compose_eq]));
qed "surj_compose";
-Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
+Goal "[| f : A funcset B; g: B funcset C; f ` A = B; inj_on f A; inj_on g B |]\
\ ==> inj_on (compose A g f) A";
by (auto_tac (claset(),
simpset() addsimps [inj_on_def, compose_eq]));
@@ -567,7 +567,7 @@
(*** restrict / lam ***)
-Goal "f``A <= B ==> (lam x: A. f x) : A funcset B";
+Goal "f`A <= B ==> (lam x: A. f x) : A funcset B";
by (auto_tac (claset(),
simpset() addsimps [restrict_def, Pi_def]));
qed "restrict_in_funcset";
@@ -603,17 +603,17 @@
(*** Inverse ***)
-Goal "[|f `` A = B; x: B |] ==> ? y: A. f y = x";
+Goal "[|f ` A = B; x: B |] ==> ? y: A. f y = x";
by (Blast_tac 1);
qed "surj_image";
-Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
+Goalw [Inv_def] "[| f ` A = B; f : A funcset B |] \
\ ==> (lam x: B. (Inv A f) x) : B funcset A";
by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
qed "Inv_funcset";
-Goal "[| f: A funcset B; inj_on f A; f `` A = B; x: A |] \
+Goal "[| f: A funcset B; inj_on f A; f ` A = B; x: A |] \
\ ==> (lam y: B. (Inv A f) y) (f x) = x";
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
@@ -621,13 +621,13 @@
by Auto_tac;
qed "Inv_f_f";
-Goal "[| f: A funcset B; f `` A = B; x: B |] \
+Goal "[| f: A funcset B; f ` A = B; x: B |] \
\ ==> f ((lam y: B. (Inv A f y)) x) = x";
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
by (fast_tac (claset() addIs [someI2]) 1);
qed "f_Inv_f";
-Goal "[| f: A funcset B; inj_on f A; f `` A = B |]\
+Goal "[| f: A funcset B; inj_on f A; f ` A = B |]\
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
by (rtac Pi_extensionality 1);
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
--- a/src/HOL/Inverse_Image.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Inverse_Image.ML Tue Jan 09 15:22:13 2001 +0100
@@ -8,32 +8,32 @@
(** Basic rules **)
-Goalw [vimage_def] "(a : f-``B) = (f a : B)";
+Goalw [vimage_def] "(a : f-`B) = (f a : B)";
by (Blast_tac 1) ;
qed "vimage_eq";
Addsimps [vimage_eq];
-Goal "(a : f-``{b}) = (f a = b)";
+Goal "(a : f-`{b}) = (f a = b)";
by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
qed "vimage_singleton_eq";
Goalw [vimage_def]
- "!!A B f. [| f a = b; b:B |] ==> a : f-``B";
+ "!!A B f. [| f a = b; b:B |] ==> a : f-`B";
by (Blast_tac 1) ;
qed "vimageI";
-Goalw [vimage_def] "f a : A ==> a : f -`` A";
+Goalw [vimage_def] "f a : A ==> a : f -` A";
by (Fast_tac 1);
qed "vimageI2";
val major::prems = Goalw [vimage_def]
- "[| a: f-``B; !!x.[| f a = x; x:B |] ==> P |] ==> P";
+ "[| a: f-`B; !!x.[| f a = x; x:B |] ==> P |] ==> P";
by (rtac (major RS CollectE) 1);
by (blast_tac (claset() addIs prems) 1) ;
qed "vimageE";
-Goalw [vimage_def] "a : f -`` A ==> f a : A";
+Goalw [vimage_def] "a : f -` A ==> f a : A";
by (Fast_tac 1);
qed "vimageD";
@@ -43,66 +43,66 @@
(*** Equations ***)
-Goal "f-``{} = {}";
+Goal "f-`{} = {}";
by (Blast_tac 1);
qed "vimage_empty";
-Goal "f-``(-A) = -(f-``A)";
+Goal "f-`(-A) = -(f-`A)";
by (Blast_tac 1);
qed "vimage_Compl";
-Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
+Goal "f-`(A Un B) = (f-`A) Un (f-`B)";
by (Blast_tac 1);
qed "vimage_Un";
-Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
+Goal "f -` (A Int B) = (f -` A) Int (f -` B)";
by (Fast_tac 1);
qed "vimage_Int";
-Goal "f -`` (Union A) = (UN X:A. f -`` X)";
+Goal "f -` (Union A) = (UN X:A. f -` X)";
by (Blast_tac 1);
qed "vimage_Union";
-Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
+Goal "f-`(UN x:A. B x) = (UN x:A. f -` B x)";
by (Blast_tac 1);
qed "vimage_UN";
-Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
+Goal "f-`(INT x:A. B x) = (INT x:A. f -` B x)";
by (Blast_tac 1);
qed "vimage_INT";
-Goal "f -`` Collect P = {y. P (f y)}";
+Goal "f -` Collect P = {y. P (f y)}";
by (Blast_tac 1);
qed "vimage_Collect_eq";
Addsimps [vimage_Collect_eq];
(*A strange result used in Tools/inductive_package*)
-val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
+val prems = Goal "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q";
by (force_tac (claset(), simpset() addsimps prems) 1);
qed "vimage_Collect";
Addsimps [vimage_empty, vimage_Un, vimage_Int];
(*NOT suitable for rewriting because of the recurrence of {a}*)
-Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
+Goal "f-`(insert a B) = (f-`{a}) Un (f-`B)";
by (Blast_tac 1);
qed "vimage_insert";
-Goal "f-``(A-B) = (f-``A) - (f-``B)";
+Goal "f-`(A-B) = (f-`A) - (f-`B)";
by (Blast_tac 1);
qed "vimage_Diff";
-Goal "f-``UNIV = UNIV";
+Goal "f-`UNIV = UNIV";
by (Blast_tac 1);
qed "vimage_UNIV";
Addsimps [vimage_UNIV];
(*NOT suitable for rewriting*)
-Goal "f-``B = (UN y: B. f-``{y})";
+Goal "f-`B = (UN y: B. f-`{y})";
by (Blast_tac 1);
qed "vimage_eq_UN";
(*monotonicity*)
-Goal "A<=B ==> f-``A <= f-``B";
+Goal "A<=B ==> f-`A <= f-`B";
by (Blast_tac 1);
qed "vimage_mono";
--- a/src/HOL/Inverse_Image.thy Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Inverse_Image.thy Tue Jan 09 15:22:13 2001 +0100
@@ -9,7 +9,7 @@
Inverse_Image = Set +
constdefs
- vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-``" 90)
- "f-``B == {x. f(x) : B}"
+ vimage :: ['a => 'b, 'b set] => ('a set) (infixr "-`" 90)
+ "f-`B == {x. f(x) : B}"
end
--- a/src/HOL/List.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/List.ML Tue Jan 09 15:22:13 2001 +0100
@@ -448,7 +448,7 @@
qed "set_rev";
Addsimps [set_rev];
-Goal "set(map f xs) = f``(set xs)";
+Goal "set(map f xs) = f`(set xs)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "set_map";
@@ -574,7 +574,7 @@
qed "Nil_eq_concat_conv";
AddIffs [Nil_eq_concat_conv];
-Goal "set(concat xs) = Union(set `` set xs)";
+Goal "set(concat xs) = Union(set ` set xs)";
by (induct_tac "xs" 1);
by Auto_tac;
qed"set_concat";
--- a/src/HOL/List.thy Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/List.thy Tue Jan 09 15:22:13 2001 +0100
@@ -177,7 +177,7 @@
lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
primrec
"lexn r 0 = {}"
-"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) `` (r <*lex*> lexn r n)) Int
+"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
{(xs,ys). length xs = Suc n & length ys = Suc n}"
constdefs
--- a/src/HOL/NatDef.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/NatDef.ML Tue Jan 09 15:22:13 2001 +0100
@@ -4,7 +4,7 @@
Copyright 1991 University of Cambridge
*)
-Goal "mono(%X. {Zero_Rep} Un (Suc_Rep``X))";
+Goal "mono(%X. {Zero_Rep} Un Suc_Rep`X)";
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
qed "Nat_fun_mono";
--- a/src/HOL/NatDef.thy Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/NatDef.thy Tue Jan 09 15:22:13 2001 +0100
@@ -36,7 +36,7 @@
(* type definition *)
typedef (Nat)
- nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (lfp_def)
+ nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep`X))" (lfp_def)
instance
nat :: {ord, zero}
--- a/src/HOL/Product_Type.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Product_Type.ML Tue Jan 09 15:22:13 2001 +0100
@@ -394,14 +394,14 @@
qed "prod_fun_ident";
Addsimps [prod_fun_ident];
-Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
+Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r";
by (rtac image_eqI 1);
by (rtac (prod_fun RS sym) 1);
by (assume_tac 1);
qed "prod_fun_imageI";
val major::prems = Goal
- "[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \
+ "[| c: (prod_fun f g)`r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \
\ |] ==> P";
by (rtac (major RS imageE) 1);
by (res_inst_tac [("p","x")] PairE 1);
--- a/src/HOL/Relation.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Relation.ML Tue Jan 09 15:22:13 2001 +0100
@@ -333,27 +333,27 @@
overload_1st_set "Relation.Image";
-Goalw [Image_def] "b : r```A = (? x:A. (x,b):r)";
+Goalw [Image_def] "b : r``A = (? x:A. (x,b):r)";
by (Blast_tac 1);
qed "Image_iff";
-Goalw [Image_def] "r```{a} = {b. (a,b):r}";
+Goalw [Image_def] "r``{a} = {b. (a,b):r}";
by (Blast_tac 1);
qed "Image_singleton";
-Goal "(b : r```{a}) = ((a,b):r)";
+Goal "(b : r``{a}) = ((a,b):r)";
by (rtac (Image_iff RS trans) 1);
by (Blast_tac 1);
qed "Image_singleton_iff";
AddIffs [Image_singleton_iff];
-Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r```A";
+Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r``A";
by (Blast_tac 1);
qed "ImageI";
val major::prems = Goalw [Image_def]
- "[| b: r```A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P";
+ "[| b: r``A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P";
by (rtac (major RS CollectE) 1);
by (Clarify_tac 1);
by (rtac (hd prems) 1);
@@ -364,58 +364,58 @@
AddSEs [ImageE];
(*This version's more effective when we already have the required "a"*)
-Goal "[| a:A; (a,b): r |] ==> b : r```A";
+Goal "[| a:A; (a,b): r |] ==> b : r``A";
by (Blast_tac 1);
qed "rev_ImageI";
-Goal "R```{} = {}";
+Goal "R``{} = {}";
by (Blast_tac 1);
qed "Image_empty";
Addsimps [Image_empty];
-Goal "Id ``` A = A";
+Goal "Id `` A = A";
by (Blast_tac 1);
qed "Image_Id";
-Goal "diag A ``` B = A Int B";
+Goal "diag A `` B = A Int B";
by (Blast_tac 1);
qed "Image_diag";
Addsimps [Image_Id, Image_diag];
-Goal "R ``` (A Int B) <= R ``` A Int R ``` B";
+Goal "R `` (A Int B) <= R `` A Int R `` B";
by (Blast_tac 1);
qed "Image_Int_subset";
-Goal "R ``` (A Un B) = R ``` A Un R ``` B";
+Goal "R `` (A Un B) = R `` A Un R `` B";
by (Blast_tac 1);
qed "Image_Un";
-Goal "r <= A <*> B ==> r```C <= B";
+Goal "r <= A <*> B ==> r``C <= B";
by (rtac subsetI 1);
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
qed "Image_subset";
(*NOT suitable for rewriting*)
-Goal "r```B = (UN y: B. r```{y})";
+Goal "r``B = (UN y: B. r``{y})";
by (Blast_tac 1);
qed "Image_eq_UN";
-Goal "[| r'<=r; A'<=A |] ==> (r' ``` A') <= (r ``` A)";
+Goal "[| r'<=r; A'<=A |] ==> (r' `` A') <= (r `` A)";
by (Blast_tac 1);
qed "Image_mono";
-Goal "(r ``` (UNION A B)) = (UN x:A.(r ``` (B x)))";
+Goal "(r `` (UNION A B)) = (UN x:A.(r `` (B x)))";
by (Blast_tac 1);
qed "Image_UN";
(*Converse inclusion fails*)
-Goal "(r ``` (INTER A B)) <= (INT x:A.(r ``` (B x)))";
+Goal "(r `` (INTER A B)) <= (INT x:A.(r `` (B x)))";
by (Blast_tac 1);
qed "Image_INT_subset";
-Goal "(r```A <= B) = (A <= - ((r^-1) ``` (-B)))";
+Goal "(r``A <= B) = (A <= - ((r^-1) `` (-B)))";
by (Blast_tac 1);
qed "Image_subset_eq";
@@ -442,7 +442,7 @@
by Auto_tac;
qed "Range_Collect_split";
-Goal "{(x,y). P x y} ``` A = {y. EX x:A. P x y}";
+Goal "{(x,y). P x y} `` A = {y. EX x:A. P x y}";
by Auto_tac;
qed "Image_Collect_split";
--- a/src/HOL/Relation.thy Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Relation.thy Tue Jan 09 15:22:13 2001 +0100
@@ -16,8 +16,8 @@
comp :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr "O" 60)
"r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
- Image :: "[('a*'b) set,'a set] => 'b set" (infixl "```" 90)
- "r ``` s == {y. ? x:s. (x,y):r}"
+ Image :: "[('a*'b) set,'a set] => 'b set" (infixl "``" 90)
+ "r `` s == {y. ? x:s. (x,y):r}"
Id :: "('a * 'a)set" (*the identity relation*)
"Id == {p. ? x. p = (x,x)}"
--- a/src/HOL/Set.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Set.ML Tue Jan 09 15:22:13 2001 +0100
@@ -531,7 +531,7 @@
Addsimps [singleton_conv2];
-section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
+section "Unions of families -- UNION x:A. B(x) is Union(B`A)";
Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
by (Blast_tac 1);
@@ -561,7 +561,7 @@
Addcongs [UN_cong];
-section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
+section "Intersections of families -- INTER x:A. B(x) is Inter(B`A)";
Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
by Auto_tac;
@@ -652,7 +652,7 @@
(*** Image of a set under a function ***)
(*Frequently b does not have the syntactic form of f(x).*)
-Goalw [image_def] "[| b=f(x); x:A |] ==> b : f``A";
+Goalw [image_def] "[| b=f(x); x:A |] ==> b : f`A";
by (Blast_tac 1);
qed "image_eqI";
Addsimps [image_eqI];
@@ -660,13 +660,13 @@
bind_thm ("imageI", refl RS image_eqI);
(*This version's more effective when we already have the required x*)
-Goalw [image_def] "[| x:A; b=f(x) |] ==> b : f``A";
+Goalw [image_def] "[| x:A; b=f(x) |] ==> b : f`A";
by (Blast_tac 1);
qed "rev_image_eqI";
(*The eta-expansion gives variable-name preservation.*)
val major::prems = Goalw [image_def]
- "[| b : (%x. f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P";
+ "[| b : (%x. f(x))`A; !!x.[| b=f(x); x:A |] ==> P |] ==> P";
by (rtac (major RS CollectD RS bexE) 1);
by (REPEAT (ares_tac prems 1));
qed "imageE";
@@ -674,22 +674,22 @@
AddIs [image_eqI];
AddSEs [imageE];
-Goal "f``(A Un B) = f``A Un f``B";
+Goal "f`(A Un B) = f`A Un f`B";
by (Blast_tac 1);
qed "image_Un";
-Goal "(z : f``A) = (EX x:A. z = f x)";
+Goal "(z : f`A) = (EX x:A. z = f x)";
by (Blast_tac 1);
qed "image_iff";
(*This rewrite rule would confuse users if made default.*)
-Goal "(f``A <= B) = (ALL x:A. f(x): B)";
+Goal "(f`A <= B) = (ALL x:A. f(x): B)";
by (Blast_tac 1);
qed "image_subset_iff";
(*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
many existing proofs.*)
-val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
+val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f`A <= B";
by (blast_tac (claset() addIs prems) 1);
qed "image_subsetI";
--- a/src/HOL/Set.thy Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Set.thy Tue Jan 09 15:22:13 2001 +0100
@@ -34,7 +34,7 @@
Union, Inter :: (('a set) set) => 'a set (*of a set*)
Pow :: 'a set => 'a set set (*powerset*)
Ball, Bex :: ['a set, 'a => bool] => bool (*bounded quantifiers*)
- "image" :: ['a => 'b, 'a set] => ('b set) (infixr "``" 90)
+ "image" :: ['a => 'b, 'a set] => ('b set) (infixr "`" 90)
(*membership*)
"op :" :: ['a, 'a set] => bool ("(_/ : _)" [50, 51] 50)
@@ -70,7 +70,7 @@
"_Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" [0, 0, 10] 10)
translations
- "range f" == "f``UNIV"
+ "range f" == "f`UNIV"
"x ~: y" == "~ (x : y)"
"{x, xs}" == "insert x {xs}"
"{x}" == "insert x {}"
@@ -145,7 +145,7 @@
empty_def "{} == {x. False}"
UNIV_def "UNIV == {x. True}"
insert_def "insert a B == {x. x=a} Un B"
- image_def "f``A == {y. ? x:A. y=f(x)}"
+ image_def "f`A == {y. ? x:A. y=f(x)}"
end
--- a/src/HOL/Sum_Type.thy Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Sum_Type.thy Tue Jan 09 15:22:13 2001 +0100
@@ -40,7 +40,7 @@
Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
- sum_def "A <+> B == (Inl``A) Un (Inr``B)"
+ sum_def "A <+> B == (Inl`A) Un (Inr`B)"
(*for selecting out the components of a mutually recursive definition*)
Part_def "Part A h == A Int {x. ? z. x = h(z)}"
--- a/src/HOL/Wellfounded_Recursion.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Wellfounded_Recursion.ML Tue Jan 09 15:22:13 2001 +0100
@@ -193,7 +193,7 @@
* Wellfoundedness of `image'
*---------------------------------------------------------------------------*)
-Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
+Goal "[| wf r; inj f |] ==> wf(prod_fun f f ` r)";
by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
by (Clarify_tac 1);
by (case_tac "EX p. f p : Q" 1);
--- a/src/HOL/equalities.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/equalities.ML Tue Jan 09 15:22:13 2001 +0100
@@ -112,49 +112,49 @@
by (Blast_tac 1);
qed "UN_insert_distrib";
-section "``";
+section "`";
-Goal "f``{} = {}";
+Goal "f`{} = {}";
by (Blast_tac 1);
qed "image_empty";
Addsimps[image_empty];
-Goal "f``insert a B = insert (f a) (f``B)";
+Goal "f`insert a B = insert (f a) (f`B)";
by (Blast_tac 1);
qed "image_insert";
Addsimps[image_insert];
-Goal "x:A ==> (%x. c) `` A = {c}";
+Goal "x:A ==> (%x. c) ` A = {c}";
by (Blast_tac 1);
qed "image_constant";
-Goal "f``(g``A) = (%x. f (g x)) `` A";
+Goal "f`(g`A) = (%x. f (g x)) ` A";
by (Blast_tac 1);
qed "image_image";
-Goal "x:A ==> insert (f x) (f``A) = f``A";
+Goal "x:A ==> insert (f x) (f`A) = f`A";
by (Blast_tac 1);
qed "insert_image";
Addsimps [insert_image];
-Goal "(f``A = {}) = (A = {})";
+Goal "(f`A = {}) = (A = {})";
by (blast_tac (claset() addSEs [equalityCE]) 1);
qed "image_is_empty";
AddIffs [image_is_empty];
-Goal "f `` {x. P x} = {f x | x. P x}";
+Goal "f ` {x. P x} = {f x | x. P x}";
by (Blast_tac 1);
qed "image_Collect";
Addsimps [image_Collect];
-Goalw [image_def] "(%x. if P x then f x else g x) `` S \
-\ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
+Goalw [image_def] "(%x. if P x then f x else g x) ` S \
+\ = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";
by (Simp_tac 1);
by (Blast_tac 1);
qed "if_image_distrib";
Addsimps[if_image_distrib];
-val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
+val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f`M = g`N";
by (simp_tac (simpset() addsimps image_def::prems) 1);
qed "image_cong";
@@ -165,7 +165,7 @@
by Auto_tac;
qed "full_SetCompr_eq";
-Goal "range (%x. f (g x)) = f``range g";
+Goal "range (%x. f (g x)) = f`range g";
by (stac image_image 1);
by (Simp_tac 1);
qed "range_composition";
@@ -563,16 +563,16 @@
by (Blast_tac 1);
qed "INT_insert_distrib";
-Goal "Union(B``A) = (UN x:A. B(x))";
+Goal "Union(B`A) = (UN x:A. B(x))";
by (Blast_tac 1);
qed "Union_image_eq";
Addsimps [Union_image_eq];
-Goal "f `` Union S = (UN x:S. f `` x)";
+Goal "f ` Union S = (UN x:S. f ` x)";
by (Blast_tac 1);
qed "image_Union";
-Goal "Inter(B``A) = (INT x:A. B(x))";
+Goal "Inter(B`A) = (INT x:A. B(x))";
by (Blast_tac 1);
qed "Inter_image_eq";
Addsimps [Inter_image_eq];
@@ -614,7 +614,7 @@
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
Union of a family of unions **)
-Goal "(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)";
+Goal "(UN x:C. A(x) Un B(x)) = Union(A`C) Un Union(B`C)";
by (Blast_tac 1);
qed "Un_Union_image";
@@ -627,7 +627,7 @@
by (Blast_tac 1);
qed "Un_Inter";
-Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
+Goal "(INT x:C. A(x) Int B(x)) = Inter(A`C) Int Inter(B`C)";
by (Blast_tac 1);
qed "Int_Inter_image";
@@ -842,7 +842,7 @@
qed "Pow_empty";
Addsimps [Pow_empty];
-Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
+Goal "Pow (insert a A) = Pow A Un (insert a ` Pow A)";
by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
qed "Pow_insert";
@@ -922,7 +922,7 @@
"(UN x:C. A - B x) = (A - (INT x:C. B x))",
"(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",
"(UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)",
- "(UN x:f``A. B x) = (UN a:A. B(f a))"];
+ "(UN x:f`A. B x) = (UN a:A. B(f a))"];
val INT_simps = map prover
["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
@@ -934,7 +934,7 @@
"(INT x:C. A Un B x) = (A Un (INT x:C. B x))",
"(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",
"(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",
- "(INT x:f``A. B x) = (INT a:A. B(f a))"];
+ "(INT x:f`A. B x) = (INT a:A. B(f a))"];
val ball_simps = map prover
@@ -948,7 +948,7 @@
"(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
"(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
"(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
- "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
+ "(ALL x:f`A. P x) = (ALL x:A. P(f x))",
"(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
val ball_conj_distrib =
@@ -963,7 +963,7 @@
"(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)",
"(EX x: UNION A B. P x) = (EX a:A. EX x: B a. P x)",
"(EX x:Collect Q. P x) = (EX x. Q x & P x)",
- "(EX x:f``A. P x) = (EX x:A. P(f x))",
+ "(EX x:f`A. P x) = (EX x:A. P(f x))",
"(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
val bex_disj_distrib =
--- a/src/HOL/mono.ML Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/mono.ML Tue Jan 09 15:22:13 2001 +0100
@@ -6,7 +6,7 @@
Monotonicity of various operations
*)
-Goal "A<=B ==> f``A <= f``B";
+Goal "A<=B ==> f`A <= f`B";
by (Blast_tac 1);
qed "image_mono";
@@ -107,7 +107,7 @@
(* Courtesy of Stephan Merz *)
Goalw [Least_def,mono_def]
"[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
-\ ==> (LEAST y. y : f``S) = f(LEAST x. x : S)";
+\ ==> (LEAST y. y : f`S) = f(LEAST x. x : S)";
by (etac bexE 1);
by (rtac someI2 1);
by (Force_tac 1);