--- a/src/HOL/BCV/SemiLattice.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/BCV/SemiLattice.ML Thu Apr 13 15:01:50 2000 +0200
@@ -150,6 +150,6 @@
(* product *)
-Goalw [semilat_def,plus_prod] "[| semilat A; semilat B |] ==> semilat (A Times B)";
+Goalw [semilat_def,plus_prod] "[| semilat A; semilat B |] ==> semilat (A <*> B)";
by (Asm_simp_tac 1);
qed "semilat_Times";
--- a/src/HOL/Induct/LList.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Induct/LList.ML Thu Apr 13 15:01:50 2000 +0200
@@ -616,20 +616,20 @@
(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
Goalw [LListD_Fun_def]
- "r <= (llist A) Times (llist A) ==> \
-\ LListD_Fun (diag A) r <= (llist A) Times (llist A)";
+ "r <= (llist A) <*> (llist A) ==> \
+\ LListD_Fun (diag A) r <= (llist A) <*> (llist A)";
by (stac llist_unfold 1);
by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
by (Fast_tac 1);
qed "LListD_Fun_subset_Times_llist";
Goal "prod_fun Rep_LList Rep_LList `` r <= \
-\ (llist(range Leaf)) Times (llist(range Leaf))";
+\ (llist(range Leaf)) <*> (llist(range Leaf))";
by (fast_tac (claset() delrules [image_subsetI]
addIs [Rep_LList RS LListD]) 1);
qed "subset_Times_llist";
-Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
+Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
\ prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
by Safe_tac;
by (etac (subsetD RS SigmaE2) 1);
--- a/src/HOL/Induct/Mutil.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Induct/Mutil.ML Thu Apr 13 15:01:50 2000 +0200
@@ -32,22 +32,22 @@
Addsimps [below_0];
Goalw [below_def]
- "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
+ "below(Suc n) <*> B = ({n} <*> B) Un ((below n) <*> B)";
by Auto_tac;
qed "Sigma_Suc1";
Goalw [below_def]
- "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
+ "A <*> below(Suc n) = (A <*> {n}) Un (A <*> (below n))";
by Auto_tac;
qed "Sigma_Suc2";
Addsimps [Sigma_Suc1, Sigma_Suc2];
-Goal "({i} Times {n}) Un ({i} Times {m}) = {(i,m), (i,n)}";
+Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
by Auto_tac;
qed "sing_Times_lemma";
-Goal "{i} Times below(n+n) : tiling domino";
+Goal "{i} <*> below(n+n) : tiling domino";
by (induct_tac "n" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
by (rtac tiling.Un 1);
@@ -56,7 +56,7 @@
AddSIs [dominoes_tile_row];
-Goal "(below m) Times below(n+n) : tiling domino";
+Goal "(below m) <*> below(n+n) : tiling domino";
by (induct_tac "m" 1);
by Auto_tac;
qed "dominoes_tile_matrix";
@@ -121,7 +121,7 @@
qed "gen_mutil_not_tiling";
(*Apply the general theorem to the well-known case*)
-Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n) |] \
+Goal "[| t = below(Suc m + Suc m) <*> below(Suc n + Suc n) |] \
\ ==> t - {(0,0)} - {(Suc(m+m), Suc(n+n))} ~: tiling domino";
by (rtac gen_mutil_not_tiling 1);
by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1);
--- a/src/HOL/Integ/Equiv.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Integ/Equiv.ML Thu Apr 13 15:01:50 2000 +0200
@@ -73,7 +73,7 @@
qed "equiv_class_nondisjoint";
val [major] = goalw Equiv.thy [equiv_def,refl_def]
- "equiv A r ==> r <= A Times A";
+ "equiv A r ==> r <= A <*> A";
by (rtac (major RS conjunct1 RS conjunct1) 1);
qed "equiv_type";
@@ -241,8 +241,8 @@
(*** Cardinality results suggested by Florian Kammueller ***)
-(*Recall that equiv A r implies r <= A Times A (equiv_type) *)
-Goal "[| finite A; r <= A Times A |] ==> finite (A/r)";
+(*Recall that equiv A r implies r <= A <*> A (equiv_type) *)
+Goal "[| finite A; r <= A <*> A |] ==> finite (A/r)";
by (rtac finite_subset 1);
by (etac (finite_Pow_iff RS iffD2) 2);
by (rewtac quotient_def);
@@ -250,7 +250,7 @@
qed "finite_quotient";
Goalw [quotient_def]
- "[| finite A; r <= A Times A; X : A/r |] ==> finite X";
+ "[| finite A; r <= A <*> A; X : A/r |] ==> finite X";
by (rtac finite_subset 1);
by (assume_tac 2);
by (Blast_tac 1);
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Apr 13 15:01:50 2000 +0200
@@ -67,11 +67,11 @@
by (simp add: below_def);
lemma Sigma_Suc1:
- "below (Suc n) Times B = ({n} Times B) Un (below n Times B)";
+ "below (Suc n) <*> B = ({n} <*> B) Un (below n <*> B)";
by (simp add: below_def less_Suc_eq) blast;
lemma Sigma_Suc2:
- "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))";
+ "A <*> below (Suc n) = (A <*> {n}) Un (A <*> (below n))";
by (simp add: below_def less_Suc_eq) blast;
lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
@@ -122,13 +122,13 @@
vertl: "{(i, j), (i + 1, j)} : domino";
lemma dominoes_tile_row:
- "{i} Times below (2 * n) : tiling domino"
+ "{i} <*> below (2 * n) : tiling domino"
(is "?P n" is "?B n : ?T");
proof (induct n);
show "?P 0"; by (simp add: below_0 tiling.empty);
fix n; assume hyp: "?P n";
- let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
+ let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}";
have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
also; have "... : ?T";
@@ -144,13 +144,13 @@
qed;
lemma dominoes_tile_matrix:
- "below m Times below (2 * n) : tiling domino"
+ "below m <*> below (2 * n) : tiling domino"
(is "?P m" is "?B m : ?T");
proof (induct m);
show "?P 0"; by (simp add: below_0 tiling.empty);
fix m; assume hyp: "?P m";
- let ?t = "{m} Times below (2 * n)";
+ let ?t = "{m} <*> below (2 * n)";
have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
also; have "... : ?T";
@@ -249,13 +249,13 @@
constdefs
mutilated_board :: "nat => nat => (nat * nat) set"
"mutilated_board m n ==
- below (2 * (m + 1)) Times below (2 * (n + 1))
+ below (2 * (m + 1)) <*> below (2 * (n + 1))
- {(0, 0)} - {(2 * m + 1, 2 * n + 1)}";
theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
proof (unfold mutilated_board_def);
let ?T = "tiling domino";
- let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
+ let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))";
let ?t' = "?t - {(0, 0)}";
let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
--- a/src/HOL/Lex/AutoChopper1.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Lex/AutoChopper1.thy Thu Apr 13 15:01:50 2000 +0200
@@ -22,7 +22,7 @@
consts
acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
=> 'a list list * 'a list"
-recdef acc "inv_image (less_than ** less_than)
+recdef acc "inv_image (less_than <*lex*> less_than)
(%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
length ys))"
"acc(A,[],s,xss,zs,[]) = (xss, zs)"
--- a/src/HOL/List.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/List.thy Thu Apr 13 15:01:50 2000 +0200
@@ -176,7 +176,7 @@
lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
primrec
"lexn r 0 = {}"
-"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
+"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r <*lex*> lexn r n)) Int
{(xs,ys). length xs = Suc n & length ys = Suc n}"
constdefs
@@ -184,7 +184,7 @@
"lex r == UN n. lexn r n"
lexico :: "('a * 'a)set => ('a list * 'a list)set"
-"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
+"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
end
--- a/src/HOL/Prod.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Prod.ML Thu Apr 13 15:01:50 2000 +0200
@@ -401,22 +401,37 @@
by (Blast_tac 1) ;
qed "Sigma_empty1";
-Goal "A Times {} = {}";
+Goal "A <*> {} = {}";
by (Blast_tac 1) ;
qed "Sigma_empty2";
-Addsimps [Sigma_empty1,Sigma_empty2];
+Addsimps [Sigma_empty1,Sigma_empty2];
+
+Goal "UNIV <*> UNIV = UNIV";
+by Auto_tac;
+qed "UNIV_Times_UNIV";
+Addsimps [UNIV_Times_UNIV];
+
+Goal "- (UNIV <*> A) = UNIV <*> (-A)";
+by Auto_tac;
+qed "Compl_Times_UNIV1";
+
+Goal "- (A <*> UNIV) = (-A) <*> UNIV";
+by Auto_tac;
+qed "Compl_Times_UNIV2";
+
+Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
by (Blast_tac 1);
qed "mem_Sigma_iff";
AddIffs [mem_Sigma_iff];
-Goal "x:C ==> (A Times C <= B Times C) = (A <= B)";
+Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
by (Blast_tac 1);
qed "Times_subset_cancel2";
-Goal "x:C ==> (A Times C = B Times C) = (A = B)";
+Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
by (blast_tac (claset() addEs [equalityE]) 1);
qed "Times_eq_cancel2";
@@ -426,14 +441,14 @@
(*** Complex rules for Sigma ***)
-Goal "{(a,b). P a & Q b} = Collect P Times Collect Q";
+Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
by (Blast_tac 1);
qed "Collect_split";
Addsimps [Collect_split];
(*Suggested by Pierre Chartier*)
-Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
+Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
by (Blast_tac 1);
qed "UN_Times_distrib";
@@ -477,15 +492,15 @@
(*Non-dependent versions are needed to avoid the need for higher-order
matching, especially when the rules are re-oriented*)
-Goal "(A Un B) Times C = (A Times C) Un (B Times C)";
+Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
by (Blast_tac 1);
qed "Times_Un_distrib1";
-Goal "(A Int B) Times C = (A Times C) Int (B Times C)";
+Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
by (Blast_tac 1);
qed "Times_Int_distrib1";
-Goal "(A - B) Times C = (A Times C) - (B Times C)";
+Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
by (Blast_tac 1);
qed "Times_Diff_distrib1";
--- a/src/HOL/Prod.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Prod.thy Thu Apr 13 15:01:50 2000 +0200
@@ -55,7 +55,7 @@
"_patterns" :: [pttrn, patterns] => patterns ("_,/_")
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)
translations
"(x, y, z)" == "(x, (y, z))"
@@ -68,7 +68,7 @@
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
"SIGMA x:A. B" => "Sigma A (%x. B)"
- "A Times B" => "Sigma A (_K B)"
+ "A <*> B" => "Sigma A (_K B)"
syntax (symbols)
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10)
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Apr 13 15:01:50 2000 +0200
@@ -66,7 +66,7 @@
constdefs
B :: "[ 'a set, 'a => real, 'a => real ] => real set"
"B V norm f ==
- {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= <0> & x:V}";
+ {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= 00 & x:V}";
text{* $n$ is the function norm of $f$, iff
$n$ is the supremum of $B$.
@@ -141,7 +141,7 @@
next;
fix x y;
- assume "x:V" "x ~= <0>"; (***
+ assume "x:V" "x ~= 00"; (***
have ge: "0r <= rinv (norm x)";
by (rule real_less_imp_le, rule real_rinv_gt_zero,
@@ -207,7 +207,7 @@
proof (intro ballI, unfold B_def,
elim UnE singletonE CollectE exE conjE);
fix x r;
- assume "x : V" "x ~= <0>"
+ assume "x : V" "x ~= 00"
and r: "r = rabs (f x) * rinv (norm x)";
have ge: "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
@@ -259,9 +259,9 @@
from the linearity of $f$: for every linear function
holds $f\ap \zero = 0$. *};
- assume "x = <0>";
- have "rabs (f x) = rabs (f <0>)"; by (simp!);
- also; from v continuous_linearform; have "f <0> = 0r"; ..;
+ assume "x = 00";
+ have "rabs (f x) = rabs (f 00)"; by (simp!);
+ also; from v continuous_linearform; have "f 00 = 0r"; ..;
also; note rabs_zero;
also; have "0r <= function_norm V norm f * norm x";
proof (rule real_le_mult_order);
@@ -272,7 +272,7 @@
show "rabs (f x) <= function_norm V norm f * norm x"; .;
next;
- assume "x ~= <0>";
+ assume "x ~= 00";
have n: "0r <= norm x"; ..;
have nz: "norm x ~= 0r";
proof (rule lt_imp_not_eq [RS not_sym]);
@@ -356,7 +356,7 @@
next;
fix x;
- assume "x : V" "x ~= <0>";
+ assume "x : V" "x ~= 00";
have lz: "0r < norm x";
by (simp! add: normed_vs_norm_gt_zero);
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Apr 13 15:01:50 2000 +0200
@@ -145,9 +145,9 @@
qed;
thus ?thesis; by blast;
qed;
- have x0: "x0 ~= <0>";
+ have x0: "x0 ~= 00";
proof (rule classical);
- presume "x0 = <0>";
+ presume "x0 = 00";
with h; have "x0:H"; by simp;
thus ?thesis; by contradiction;
qed blast;
@@ -190,7 +190,7 @@
txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$. *};
- def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0
+ def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a (*) x0
& y:H
in (h y) + a * xi";
show ?thesis;
@@ -205,7 +205,7 @@
have "graph H h <= graph H0 h0";
proof (rule graph_extI);
fix t; assume "t:H";
- have "(SOME (y, a). t = y + a <*> x0 & y : H)
+ have "(SOME (y, a). t = y + a (*) x0 & y : H)
= (t,0r)";
by (rule decomp_H0_H [OF _ _ _ _ _ x0]);
thus "h t = h0 t"; by (simp! add: Let_def);
@@ -228,8 +228,8 @@
assume e: "graph H h = graph H0 h0";
have "x0 : H0";
proof (unfold H0_def, rule vs_sumI);
- show "x0 = <0> + x0"; by (simp!);
- from h; show "<0> : H"; ..;
+ show "x0 = 00 + x0"; by (simp!);
+ from h; show "00 : H"; ..;
show "x0 : lin x0"; by (rule x_lin_x);
qed;
hence "(x0, h0 x0) : graph H0 h0"; ..;
@@ -265,10 +265,10 @@
also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
by (simp add: Let_def);
also; have
- "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
+ "(x, 0r) = (SOME (y, a). x = y + a (*) x0 & y : H)";
by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+;
also; have
- "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
+ "(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H)
in h y + a * xi)
= h0 x"; by (simp!);
finally; show "f x = h0 x"; .;
@@ -427,9 +427,9 @@
proof;
fix x0; assume "x0:E" "x0~:H";
- have x0: "x0 ~= <0>";
+ have x0: "x0 ~= 00";
proof (rule classical);
- presume "x0 = <0>";
+ presume "x0 = 00";
with h; have "x0:H"; by simp;
thus ?thesis; by contradiction;
qed blast;
@@ -471,7 +471,7 @@
of $h$ on $H_0$:*};
def h0 ==
- "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a ( * ) x0 & y:H
in (h y) + a * xi";
txt {* We get that the graph of $h_0$ extends that of
@@ -480,7 +480,7 @@
have "graph H h <= graph H0 h0";
proof (rule graph_extI);
fix t; assume "t:H";
- have "(SOME (y, a). t = y + a <*> x0 & y : H) = (t,0r)";
+ have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,0r)";
by (rule decomp_H0_H, rule x0);
thus "h t = h0 t"; by (simp! add: Let_def);
next;
@@ -502,8 +502,8 @@
assume e: "graph H h = graph H0 h0";
have "x0 : H0";
proof (unfold H0_def, rule vs_sumI);
- show "x0 = <0> + x0"; by (simp!);
- from h; show "<0> : H"; ..;
+ show "x0 = 00 + x0"; by (simp!);
+ from h; show "00 : H"; ..;
show "x0 : lin x0"; by (rule x_lin_x);
qed;
hence "(x0, h0 x0) : graph H0 h0"; ..;
@@ -545,10 +545,10 @@
also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
by (simp add: Let_def);
also; have
- "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
+ "(x, 0r) = (SOME (y, a). x = y + a ( * ) x0 & y : H)";
by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
also; have
- "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
+ "(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H)
in h y + a * xi)
= h0 x"; by (simp!);
finally; show "f x = h0 x"; .;
@@ -672,11 +672,11 @@
txt{* $p$ is absolutely homogenous: *};
- show "p (a <*> x) = rabs a * p x";
+ show "p (a (*) x) = rabs a * p x";
proof -;
- have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
+ have "p (a (*) x) = function_norm F norm f * norm (a (*) x)";
by (simp!);
- also; have "norm (a <*> x) = rabs a * norm x";
+ also; have "norm (a (*) x) = rabs a * norm x";
by (rule normed_vs_norm_rabs_homogenous);
also; have "function_norm F norm f * (rabs a * norm x)
= rabs a * (function_norm F norm f * norm x)";
@@ -801,4 +801,4 @@
qed;
qed;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Apr 13 15:01:50 2000 +0200
@@ -52,27 +52,27 @@
txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
- from vs; have "a <0> : ?S"; by force;
+ from vs; have "a 00 : ?S"; by force;
thus "EX X. X : ?S"; ..;
txt {* $b\ap \zero$ is an upper bound of $S$: *};
show "EX Y. isUb UNIV ?S Y";
proof;
- show "isUb UNIV ?S (b <0>)";
+ show "isUb UNIV ?S (b 00)";
proof (intro isUbI setleI ballI);
- show "b <0> : UNIV"; ..;
+ show "b 00 : UNIV"; ..;
next;
txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
fix y; assume y: "y : ?S";
from y; have "EX u:F. y = a u"; by fast;
- thus "y <= b <0>";
+ thus "y <= b 00";
proof;
fix u; assume "u:F";
assume "y = a u";
- also; have "a u <= b <0>"; by (rule r) (simp!)+;
+ also; have "a u <= b 00"; by (rule r) (simp!)+;
finally; show ?thesis; .;
qed;
qed;
@@ -121,18 +121,18 @@
is a linear extension of $h$ to $H_0$. *};
lemma h0_lf:
- "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi);
H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
- x0 : E; x0 ~= <0>; is_vectorspace E |]
+ x0 : E; x0 ~= 00; is_vectorspace E |]
==> is_linearform H0 h0";
proof -;
assume h0_def:
- "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi)"
and H0_def: "H0 == H + lin x0"
and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
- "x0 ~= <0>" "x0 : E" "is_vectorspace E";
+ "x0 ~= 00" "x0 : E" "is_vectorspace E";
have h0: "is_vectorspace H0";
proof (unfold H0_def, rule vs_sum_vs);
@@ -150,27 +150,27 @@
have x1x2: "x1 + x2 : H0";
by (rule vs_add_closed, rule h0);
from x1;
- have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
+ have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
by (unfold H0_def vs_sum_def lin_def) fast;
from x2;
- have ex_x2: "EX y2 a2. x2 = y2 + a2 <*> x0 & y2 : H";
+ have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H";
by (unfold H0_def vs_sum_def lin_def) fast;
from x1x2;
- have ex_x1x2: "EX y a. x1 + x2 = y + a <*> x0 & y : H";
+ have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H";
by (unfold H0_def vs_sum_def lin_def) fast;
from ex_x1 ex_x2 ex_x1x2;
show "h0 (x1 + x2) = h0 x1 + h0 x2";
proof (elim exE conjE);
fix y1 y2 y a1 a2 a;
- assume y1: "x1 = y1 + a1 <*> x0" and y1': "y1 : H"
- and y2: "x2 = y2 + a2 <*> x0" and y2': "y2 : H"
- and y: "x1 + x2 = y + a <*> x0" and y': "y : H";
+ assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
+ and y2: "x2 = y2 + a2 (*) x0" and y2': "y2 : H"
+ and y: "x1 + x2 = y + a (*) x0" and y': "y : H";
have ya: "y1 + y2 = y & a1 + a2 = a";
proof (rule decomp_H0);;
txt_raw {* \label{decomp-H0-use} *};;
- show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0";
+ show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0";
by (simp! add: vs_add_mult_distrib2 [of E]);
show "y1 + y2 : H"; ..;
qed;
@@ -199,31 +199,31 @@
next;
fix c x1; assume x1: "x1 : H0";
- have ax1: "c <*> x1 : H0";
+ have ax1: "c (*) x1 : H0";
by (rule vs_mult_closed, rule h0);
from x1; have ex_x: "!! x. x: H0
- ==> EX y a. x = y + a <*> x0 & y : H";
+ ==> EX y a. x = y + a (*) x0 & y : H";
by (unfold H0_def vs_sum_def lin_def) fast;
- from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
+ from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
by (unfold H0_def vs_sum_def lin_def) fast;
- with ex_x [of "c <*> x1", OF ax1];
- show "h0 (c <*> x1) = c * (h0 x1)";
+ with ex_x [of "c (*) x1", OF ax1];
+ show "h0 (c (*) x1) = c * (h0 x1)";
proof (elim exE conjE);
fix y1 y a1 a;
- assume y1: "x1 = y1 + a1 <*> x0" and y1': "y1 : H"
- and y: "c <*> x1 = y + a <*> x0" and y': "y : H";
+ assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
+ and y: "c (*) x1 = y + a (*) x0" and y': "y : H";
- have ya: "c <*> y1 = y & c * a1 = a";
+ have ya: "c (*) y1 = y & c * a1 = a";
proof (rule decomp_H0);
- show "c <*> y1 + (c * a1) <*> x0 = y + a <*> x0";
+ show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0";
by (simp! add: add: vs_add_mult_distrib1);
- show "c <*> y1 : H"; ..;
+ show "c (*) y1 : H"; ..;
qed;
- have "h0 (c <*> x1) = h y + a * xi";
+ have "h0 (c (*) x1) = h y + a * xi";
by (rule h0_definite);
- also; have "... = h (c <*> y1) + (c * a1) * xi";
+ also; have "... = h (c (*) y1) + (c * a1) * xi";
by (simp add: ya);
also; from vs y1'; have "... = c * h y1 + c * a1 * xi";
by (simp add: linearform_mult [of H]);
@@ -240,31 +240,31 @@
is bounded by the seminorm $p$. *};
lemma h0_norm_pres:
- "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi);
- H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E;
+ H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E;
is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y;
ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
==> ALL x:H0. h0 x <= p x";
proof;
assume h0_def:
- "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in (h y) + a * xi)"
and H0_def: "H0 == H + lin x0"
- and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E"
+ and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E"
"is_subspace H E" "is_seminorm E p" "is_linearform H h"
and a: "ALL y:H. h y <= p y";
presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
fix x; assume "x : H0";
have ex_x:
- "!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
+ "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H";
by (unfold H0_def vs_sum_def lin_def) fast;
- have "EX y a. x = y + a <*> x0 & y : H";
+ have "EX y a. x = y + a (*) x0 & y : H";
by (rule ex_x);
thus "h0 x <= p x";
proof (elim exE conjE);
- fix y a; assume x: "x = y + a <*> x0" and y: "y : H";
+ fix y a; assume x: "x = y + a (*) x0" and y: "y : H";
have "h0 x = h y + a * xi";
by (rule h0_definite);
@@ -272,7 +272,7 @@
$h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
by case analysis on $a$. \label{linorder_linear_split}*};
- also; have "... <= p (y + a <*> x0)";
+ also; have "... <= p (y + a (*) x0)";
proof (rule linorder_linear_split);
assume z: "a = 0r";
@@ -284,27 +284,27 @@
next;
assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
from a1;
- have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
+ have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
by (rule bspec) (simp!);
txt {* The thesis for this case now follows by a short
calculation. *};
hence "a * xi
- <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
+ <= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))";
by (rule real_mult_less_le_anti [OF lz]);
- also; have "... = - a * (p (rinv a <*> y + x0))
- - a * (h (rinv a <*> y))";
+ also; have "... = - a * (p (rinv a (*) y + x0))
+ - a * (h (rinv a (*) y))";
by (rule real_mult_diff_distrib);
- also; from lz vs y; have "- a * (p (rinv a <*> y + x0))
- = p (a <*> (rinv a <*> y + x0))";
+ also; from lz vs y; have "- a * (p (rinv a (*) y + x0))
+ = p (a (*) (rinv a (*) y + x0))";
by (simp add: seminorm_rabs_homogenous rabs_minus_eqI2);
- also; from nz vs y; have "... = p (y + a <*> x0)";
+ also; from nz vs y; have "... = p (y + a (*) x0)";
by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * (h (rinv a <*> y)) = h y";
+ also; from nz vs y; have "a * (h (rinv a (*) y)) = h y";
by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
- hence "h y + a * xi <= h y + p (y + a <*> x0) - h y";
+ hence "h y + a * xi <= h y + p (y + a (*) x0) - h y";
by (simp add: real_add_left_cancel_le);
thus ?thesis; by simp;
@@ -314,30 +314,30 @@
next;
assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
from a2;
- have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
+ have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
by (rule bspec) (simp!);
txt {* The thesis for this case follows by a short
calculation: *};
with gz; have "a * xi
- <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
+ <= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))";
by (rule real_mult_less_le_mono);
- also; have "... = a * p (rinv a <*> y + x0)
- - a * h (rinv a <*> y)";
+ also; have "... = a * p (rinv a (*) y + x0)
+ - a * h (rinv a (*) y)";
by (rule real_mult_diff_distrib2);
also; from gz vs y;
- have "a * p (rinv a <*> y + x0)
- = p (a <*> (rinv a <*> y + x0))";
+ have "a * p (rinv a (*) y + x0)
+ = p (a (*) (rinv a (*) y + x0))";
by (simp add: seminorm_rabs_homogenous rabs_eqI2);
also; from nz vs y;
- have "... = p (y + a <*> x0)";
+ have "... = p (y + a (*) x0)";
by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * h (rinv a <*> y) = h y";
+ also; from nz vs y; have "a * h (rinv a (*) y) = h y";
by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
+ finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
- hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
+ hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)";
by (simp add: real_add_left_cancel_le);
thus ?thesis; by simp;
qed;
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Apr 13 15:01:50 2000 +0200
@@ -437,16 +437,16 @@
txt{* We have to show that $h$ is multiplicative. *};
- thus "h (a <*> x) = a * h x";
+ thus "h (a (*) x) = a * h x";
proof (elim exE conjE);
fix H' h'; assume "x:H'"
and b: "graph H' h' <= graph H h"
and "is_linearform H' h'" "is_subspace H' E";
- have "h' (a <*> x) = a * h' x";
+ have "h' (a (*) x) = a * h' x";
by (rule linearform_mult);
also; have "h' x = h x"; ..;
- also; have "a <*> x : H'"; ..;
- with b; have "h' (a <*> x) = h (a <*> x)"; ..;
+ also; have "a (*) x : H'"; ..;
+ with b; have "h' (a (*) x) = h (a (*) x)"; ..;
finally; show ?thesis; .;
qed;
qed;
@@ -507,7 +507,7 @@
show ?thesis;
proof;
- show "<0> : F"; ..;
+ show "00 : F"; ..;
show "F <= H";
proof (rule graph_extD2);
show "graph F f <= graph H h";
@@ -518,10 +518,10 @@
fix x y; assume "x:F" "y:F";
show "x + y : F"; by (simp!);
qed;
- show "ALL x:F. ALL a. a <*> x : F";
+ show "ALL x:F. ALL a. a (*) x : F";
proof (intro ballI allI);
fix x a; assume "x:F";
- show "a <*> x : F"; by (simp!);
+ show "a (*) x : F"; by (simp!);
qed;
qed;
qed;
@@ -542,10 +542,10 @@
txt {* The $\zero$ element is in $H$, as $F$ is a subset
of $H$: *};
- have "<0> : F"; ..;
+ have "00 : F"; ..;
also; have "is_subspace F H"; by (rule sup_supF);
hence "F <= H"; ..;
- finally; show "<0> : H"; .;
+ finally; show "00 : H"; .;
txt{* $H$ is a subset of $E$: *};
@@ -588,7 +588,7 @@
txt{* $H$ is closed under scalar multiplication: *};
- show "ALL x:H. ALL a. a <*> x : H";
+ show "ALL x:H. ALL a. a (*) x : H";
proof (intro ballI allI);
fix x a; assume "x:H";
have "EX H' h'. x:H' & graph H' h' <= graph H h
@@ -596,11 +596,11 @@
& is_subspace F H' & graph F f <= graph H' h'
& (ALL x:H'. h' x <= p x)";
by (rule some_H'h');
- thus "a <*> x : H";
+ thus "a (*) x : H";
proof (elim exE conjE);
fix H' h';
assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h";
- have "a <*> x : H'"; ..;
+ have "a (*) x : H'"; ..;
also; have "H' <= H"; ..;
finally; show ?thesis; .;
qed;
--- a/src/HOL/Real/HahnBanach/Linearform.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Apr 13 15:01:50 2000 +0200
@@ -14,11 +14,11 @@
is_linearform :: "['a::{minus, plus} set, 'a => real] => bool"
"is_linearform V f ==
(ALL x: V. ALL y: V. f (x + y) = f x + f y) &
- (ALL x: V. ALL a. f (a <*> x) = a * (f x))";
+ (ALL x: V. ALL a. f (a (*) x) = a * (f x))";
lemma is_linearformI [intro]:
"[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
- !! x c. x : V ==> f (c <*> x) = c * f x |]
+ !! x c. x : V ==> f (c (*) x) = c * f x |]
==> is_linearform V f";
by (unfold is_linearform_def) force;
@@ -27,7 +27,7 @@
by (unfold is_linearform_def) fast;
lemma linearform_mult [intro??]:
- "[| is_linearform V f; x:V |] ==> f (a <*> x) = a * (f x)";
+ "[| is_linearform V f; x:V |] ==> f (a (*) x) = a * (f x)";
by (unfold is_linearform_def) fast;
lemma linearform_neg [intro??]:
@@ -35,7 +35,7 @@
==> f (- x) = - f x";
proof -;
assume "is_linearform V f" "is_vectorspace V" "x:V";
- have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
+ have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
also; have "... = - (f x)"; by (simp!);
finally; show ?thesis; .;
@@ -56,14 +56,14 @@
text{* Every linear form yields $0$ for the $\zero$ vector.*};
lemma linearform_zero [intro??, simp]:
- "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";
+ "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r";
proof -;
assume "is_vectorspace V" "is_linearform V f";
- have "f <0> = f (<0> - <0>)"; by (simp!);
- also; have "... = f <0> - f <0>";
+ have "f 00 = f (00 - 00)"; by (simp!);
+ also; have "... = f 00 - f 00";
by (rule linearform_diff) (simp!)+;
also; have "... = 0r"; by simp;
- finally; show "f <0> = 0r"; .;
+ finally; show "f 00 = 0r"; .;
qed;
end;
\ No newline at end of file
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Thu Apr 13 15:01:50 2000 +0200
@@ -19,12 +19,12 @@
is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
"is_seminorm V norm == ALL x: V. ALL y:V. ALL a.
0r <= norm x
- & norm (a <*> x) = (rabs a) * (norm x)
+ & norm (a (*) x) = (rabs a) * (norm x)
& norm (x + y) <= norm x + norm y";
lemma is_seminormI [intro]:
"[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
- !! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x);
+ !! x a. x:V ==> norm (a (*) x) = (rabs a) * (norm x);
!! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |]
==> is_seminorm V norm";
by (unfold is_seminorm_def, force);
@@ -35,7 +35,7 @@
lemma seminorm_rabs_homogenous:
"[| is_seminorm V norm; x:V |]
- ==> norm (a <*> x) = (rabs a) * (norm x)";
+ ==> norm (a (*) x) = (rabs a) * (norm x)";
by (unfold is_seminorm_def, force);
lemma seminorm_subadditive:
@@ -48,11 +48,11 @@
==> norm (x - y) <= norm x + norm y";
proof -;
assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
- have "norm (x - y) = norm (x + - 1r <*> y)";
+ have "norm (x - y) = norm (x + - 1r (*) y)";
by (simp! add: diff_eq2 negate_eq2);
- also; have "... <= norm x + norm (- 1r <*> y)";
+ also; have "... <= norm x + norm (- 1r (*) y)";
by (simp! add: seminorm_subadditive);
- also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y";
+ also; have "norm (- 1r (*) y) = rabs (- 1r) * norm y";
by (rule seminorm_rabs_homogenous);
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
finally; show "norm (x - y) <= norm x + norm y"; by simp;
@@ -63,7 +63,7 @@
==> norm (- x) = norm x";
proof -;
assume "is_seminorm V norm" "x:V" "is_vectorspace V";
- have "norm (- x) = norm (- 1r <*> x)"; by (simp! only: negate_eq1);
+ have "norm (- x) = norm (- 1r (*) x)"; by (simp! only: negate_eq1);
also; have "... = rabs (- 1r) * norm x";
by (rule seminorm_rabs_homogenous);
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
@@ -79,10 +79,10 @@
constdefs
is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
"is_norm V norm == ALL x: V. is_seminorm V norm
- & (norm x = 0r) = (x = <0>)";
+ & (norm x = 0r) = (x = 00)";
lemma is_normI [intro]:
- "ALL x: V. is_seminorm V norm & (norm x = 0r) = (x = <0>)
+ "ALL x: V. is_seminorm V norm & (norm x = 0r) = (x = 00)
==> is_norm V norm"; by (simp only: is_norm_def);
lemma norm_is_seminorm [intro??]:
@@ -90,7 +90,7 @@
by (unfold is_norm_def, force);
lemma norm_zero_iff:
- "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)";
+ "[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = 00)";
by (unfold is_norm_def, force);
lemma norm_ge_zero [intro??]:
@@ -128,15 +128,15 @@
by (unfold is_normed_vectorspace_def, rule, elim conjE);
lemma normed_vs_norm_gt_zero [intro??]:
- "[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x";
+ "[| is_normed_vectorspace V norm; x:V; x ~= 00 |] ==> 0r < norm x";
proof (unfold is_normed_vectorspace_def, elim conjE);
- assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm";
+ assume "x : V" "x ~= 00" "is_vectorspace V" "is_norm V norm";
have "0r <= norm x"; ..;
also; have "0r ~= norm x";
proof;
presume "norm x = 0r";
- also; have "?this = (x = <0>)"; by (rule norm_zero_iff);
- finally; have "x = <0>"; .;
+ also; have "?this = (x = 00)"; by (rule norm_zero_iff);
+ finally; have "x = 00"; .;
thus "False"; by contradiction;
qed (rule sym);
finally; show "0r < norm x"; .;
@@ -144,7 +144,7 @@
lemma normed_vs_norm_rabs_homogenous [intro??]:
"[| is_normed_vectorspace V norm; x:V |]
- ==> norm (a <*> x) = (rabs a) * (norm x)";
+ ==> norm (a (*) x) = (rabs a) * (norm x)";
by (rule seminorm_rabs_homogenous, rule norm_is_seminorm,
rule normed_vs_norm);
@@ -170,13 +170,13 @@
proof;
fix x y a; presume "x : E";
show "0r <= norm x"; ..;
- show "norm (a <*> x) = rabs a * norm x"; ..;
+ show "norm (a (*) x) = rabs a * norm x"; ..;
presume "y : E";
show "norm (x + y) <= norm x + norm y"; ..;
qed (simp!)+;
fix x; assume "x : F";
- show "(norm x = 0r) = (x = <0>)";
+ show "(norm x = 0r) = (x = 00)";
proof (rule norm_zero_iff);
show "is_norm E norm"; ..;
qed (simp!);
--- a/src/HOL/Real/HahnBanach/Subspace.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Apr 13 15:01:50 2000 +0200
@@ -18,14 +18,14 @@
constdefs
is_subspace :: "['a::{minus, plus} set, 'a set] => bool"
"is_subspace U V == U ~= {} & U <= V
- & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
+ & (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)";
lemma subspaceI [intro]:
- "[| <0> : U; U <= V; ALL x:U. ALL y:U. (x + y : U);
- ALL x:U. ALL a. a <*> x : U |]
+ "[| 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U);
+ ALL x:U. ALL a. a (*) x : U |]
==> is_subspace U V";
proof (unfold is_subspace_def, intro conjI);
- assume "<0> : U"; thus "U ~= {}"; by fast;
+ assume "00 : U"; thus "U ~= {}"; by fast;
qed (simp+);
lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}";
@@ -43,7 +43,7 @@
by (unfold is_subspace_def) simp;
lemma subspace_mult_closed [simp, intro??]:
- "[| is_subspace U V; x:U |] ==> a <*> x : U";
+ "[| is_subspace U V; x:U |] ==> a (*) x : U";
by (unfold is_subspace_def) simp;
lemma subspace_diff_closed [simp, intro??]:
@@ -56,7 +56,7 @@
of the carrier set and by vector space laws.*};
lemma zero_in_subspace [intro??]:
- "[| is_subspace U V; is_vectorspace V |] ==> <0> : U";
+ "[| is_subspace U V; is_vectorspace V |] ==> 00 : U";
proof -;
assume "is_subspace U V" and v: "is_vectorspace V";
have "U ~= {}"; ..;
@@ -65,7 +65,7 @@
proof;
fix x; assume u: "x:U";
hence "x:V"; by (simp!);
- with v; have "<0> = x - x"; by (simp!);
+ with v; have "00 = x - x"; by (simp!);
also; have "... : U"; by (rule subspace_diff_closed);
finally; show ?thesis; .;
qed;
@@ -84,10 +84,10 @@
assume "is_subspace U V" "is_vectorspace V";
show ?thesis;
proof;
- show "<0> : U"; ..;
- show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
+ show "00 : U"; ..;
+ show "ALL x:U. ALL a. a (*) x : U"; by (simp!);
show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
- show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
+ show "ALL x:U. - x = -1r (*) x"; by (simp! add: negate_eq1);
show "ALL x:U. ALL y:U. x - y = x + - y";
by (simp! add: diff_eq1);
qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
@@ -98,10 +98,10 @@
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
proof;
assume "is_vectorspace V";
- show "<0> : V"; ..;
+ show "00 : V"; ..;
show "V <= V"; ..;
show "ALL x:V. ALL y:V. x + y : V"; by (simp!);
- show "ALL x:V. ALL a. a <*> x : V"; by (simp!);
+ show "ALL x:V. ALL a. a (*) x : V"; by (simp!);
qed;
text {* The subspace relation is transitive. *};
@@ -111,7 +111,7 @@
==> is_subspace U W";
proof;
assume "is_subspace U V" "is_subspace V W" "is_vectorspace V";
- show "<0> : U"; ..;
+ show "00 : U"; ..;
have "U <= V"; ..;
also; have "V <= W"; ..;
@@ -123,10 +123,10 @@
show "x + y : U"; by (simp!);
qed;
- show "ALL x:U. ALL a. a <*> x : U";
+ show "ALL x:U. ALL a. a (*) x : U";
proof (intro ballI allI);
fix x a; assume "x:U";
- show "a <*> x : U"; by (simp!);
+ show "a (*) x : U"; by (simp!);
qed;
qed;
@@ -139,12 +139,12 @@
constdefs
lin :: "'a => 'a set"
- "lin x == {a <*> x | a. True}";
+ "lin x == {a (*) x | a. True}";
-lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
+lemma linD: "x : lin v = (EX a::real. x = a (*) v)";
by (unfold lin_def) fast;
-lemma linI [intro??]: "a <*> x0 : lin x0";
+lemma linI [intro??]: "a (*) x0 : lin x0";
by (unfold lin_def) fast;
text {* Every vector is contained in its linear closure. *};
@@ -152,7 +152,7 @@
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
proof (unfold lin_def, intro CollectI exI conjI);
assume "is_vectorspace V" "x:V";
- show "x = 1r <*> x"; by (simp!);
+ show "x = 1r (*) x"; by (simp!);
qed simp;
text {* Any linear closure is a subspace. *};
@@ -161,14 +161,14 @@
"[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
proof;
assume "is_vectorspace V" "x:V";
- show "<0> : lin x";
+ show "00 : lin x";
proof (unfold lin_def, intro CollectI exI conjI);
- show "<0> = 0r <*> x"; by (simp!);
+ show "00 = 0r (*) x"; by (simp!);
qed simp;
show "lin x <= V";
proof (unfold lin_def, intro subsetI, elim CollectE exE conjE);
- fix xa a; assume "xa = a <*> x";
+ fix xa a; assume "xa = a (*) x";
show "xa:V"; by (simp!);
qed;
@@ -178,20 +178,20 @@
thus "x1 + x2 : lin x";
proof (unfold lin_def, elim CollectE exE conjE,
intro CollectI exI conjI);
- fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
- show "x1 + x2 = (a1 + a2) <*> x";
+ fix a1 a2; assume "x1 = a1 (*) x" "x2 = a2 (*) x";
+ show "x1 + x2 = (a1 + a2) (*) x";
by (simp! add: vs_add_mult_distrib2);
qed simp;
qed;
- show "ALL xa:lin x. ALL a. a <*> xa : lin x";
+ show "ALL xa:lin x. ALL a. a (*) xa : lin x";
proof (intro ballI allI);
fix x1 a; assume "x1 : lin x";
- thus "a <*> x1 : lin x";
+ thus "a (*) x1 : lin x";
proof (unfold lin_def, elim CollectE exE conjE,
intro CollectI exI conjI);
- fix a1; assume "x1 = a1 <*> x";
- show "a <*> x1 = (a * a1) <*> x"; by (simp!);
+ fix a1; assume "x1 = a1 (*) x";
+ show "a (*) x1 = (a * a1) (*) x"; by (simp!);
qed simp;
qed;
qed;
@@ -240,20 +240,20 @@
==> is_subspace U (U + V)";
proof;
assume "is_vectorspace U" "is_vectorspace V";
- show "<0> : U"; ..;
+ show "00 : U"; ..;
show "U <= U + V";
proof (intro subsetI vs_sumI);
fix x; assume "x:U";
- show "x = x + <0>"; by (simp!);
- show "<0> : V"; by (simp!);
+ show "x = x + 00"; by (simp!);
+ show "00 : V"; by (simp!);
qed;
show "ALL x:U. ALL y:U. x + y : U";
proof (intro ballI);
fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!);
qed;
- show "ALL x:U. ALL a. a <*> x : U";
+ show "ALL x:U. ALL a. a (*) x : U";
proof (intro ballI allI);
- fix x a; assume "x:U"; show "a <*> x : U"; by (simp!);
+ fix x a; assume "x:U"; show "a (*) x : U"; by (simp!);
qed;
qed;
@@ -264,11 +264,11 @@
==> is_subspace (U + V) E";
proof;
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
- show "<0> : U + V";
+ show "00 : U + V";
proof (intro vs_sumI);
- show "<0> : U"; ..;
- show "<0> : V"; ..;
- show "(<0>::'a) = <0> + <0>"; by (simp!);
+ show "00 : U"; ..;
+ show "00 : V"; ..;
+ show "(00::'a) = 00 + 00"; by (simp!);
qed;
show "U + V <= E";
@@ -289,13 +289,13 @@
qed (simp!)+;
qed;
- show "ALL x : U + V. ALL a. a <*> x : U + V";
+ show "ALL x : U + V. ALL a. a (*) x : U + V";
proof (intro ballI allI);
fix x a; assume "x : U + V";
- thus "a <*> x : U + V";
+ thus "a (*) x : U + V";
proof (elim vs_sumE bexE, intro vs_sumI);
fix a x u v; assume "u : U" "v : V" "x = u + v";
- show "a <*> x = (a <*> u) + (a <*> v)";
+ show "a (*) x = (a (*) u) + (a (*) v)";
by (simp! add: vs_add_mult_distrib1);
qed (simp!)+;
qed;
@@ -323,11 +323,11 @@
lemma decomp:
"[| is_vectorspace E; is_subspace U E; is_subspace V E;
- U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |]
+ U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |]
==> u1 = u2 & v1 = v2";
proof;
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"
- "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V"
+ "U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V"
"u1 + v1 = u2 + v2";
have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap);
have u: "u1 - u2 : U"; by (simp!);
@@ -337,14 +337,14 @@
show "u1 = u2";
proof (rule vs_add_minus_eq);
- show "u1 - u2 = <0>"; by (rule Int_singletonD [OF _ u u']);
+ show "u1 - u2 = 00"; by (rule Int_singletonD [OF _ u u']);
show "u1 : E"; ..;
show "u2 : E"; ..;
qed;
show "v1 = v2";
proof (rule vs_add_minus_eq [RS sym]);
- show "v2 - v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
+ show "v2 - v1 = 00"; by (rule Int_singletonD [OF _ v' v]);
show "v1 : E"; ..;
show "v2 : E"; ..;
qed;
@@ -358,44 +358,44 @@
lemma decomp_H0:
"[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
- x0 ~: H; x0 : E; x0 ~= <0>; y1 + a1 <*> x0 = y2 + a2 <*> x0 |]
+ x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |]
==> y1 = y2 & a1 = a2";
proof;
assume "is_vectorspace E" and h: "is_subspace H E"
- and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>"
- "y1 + a1 <*> x0 = y2 + a2 <*> x0";
+ and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00"
+ "y1 + a1 (*) x0 = y2 + a2 (*) x0";
- have c: "y1 = y2 & a1 <*> x0 = a2 <*> x0";
+ have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0";
proof (rule decomp);
- show "a1 <*> x0 : lin x0"; ..;
- show "a2 <*> x0 : lin x0"; ..;
- show "H Int (lin x0) = {<0>}";
+ show "a1 (*) x0 : lin x0"; ..;
+ show "a2 (*) x0 : lin x0"; ..;
+ show "H Int (lin x0) = {00}";
proof;
- show "H Int lin x0 <= {<0>}";
+ show "H Int lin x0 <= {00}";
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
fix x; assume "x:H" "x : lin x0";
- thus "x = <0>";
+ thus "x = 00";
proof (unfold lin_def, elim CollectE exE conjE);
- fix a; assume "x = a <*> x0";
+ fix a; assume "x = a (*) x0";
show ?thesis;
proof cases;
assume "a = 0r"; show ?thesis; by (simp!);
next;
assume "a ~= 0r";
- from h; have "rinv a <*> a <*> x0 : H";
+ from h; have "rinv a (*) a (*) x0 : H";
by (rule subspace_mult_closed) (simp!);
- also; have "rinv a <*> a <*> x0 = x0"; by (simp!);
+ also; have "rinv a (*) a (*) x0 = x0"; by (simp!);
finally; have "x0 : H"; .;
thus ?thesis; by contradiction;
qed;
qed;
qed;
- show "{<0>} <= H Int lin x0";
+ show "{00} <= H Int lin x0";
proof -;
- have "<0>: H Int lin x0";
+ have "00: H Int lin x0";
proof (rule IntI);
- show "<0>:H"; ..;
- from lin_vs; show "<0> : lin x0"; ..;
+ show "00:H"; ..;
+ from lin_vs; show "00 : lin x0"; ..;
qed;
thus ?thesis; by simp;
qed;
@@ -407,7 +407,7 @@
show "a1 = a2";
proof (rule vs_mult_right_cancel [RS iffD1]);
- from c; show "a1 <*> x0 = a2 <*> x0"; by simp;
+ from c; show "a1 (*) x0 = a2 (*) x0"; by simp;
qed;
qed;
@@ -418,13 +418,13 @@
lemma decomp_H0_H:
"[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
- x0 ~= <0> |]
- ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
+ x0 ~= 00 |]
+ ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, 0r)";
proof (rule, unfold split_paired_all);
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
- "x0 ~= <0>";
+ "x0 ~= 00";
have h: "is_vectorspace H"; ..;
- fix y a; presume t1: "t = y + a <*> x0" and "y:H";
+ fix y a; presume t1: "t = y + a (*) x0" and "y:H";
have "y = t & a = 0r";
by (rule decomp_H0) (assumption | (simp!))+;
thus "(y, a) = (t, 0r)"; by (simp!);
@@ -435,40 +435,40 @@
$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
lemma h0_definite:
- "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+ "[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
in (h y) + a * xi);
- x = y + a <*> x0; is_vectorspace E; is_subspace H E;
- y:H; x0 ~: H; x0:E; x0 ~= <0> |]
+ x = y + a (*) x0; is_vectorspace E; is_subspace H E;
+ y:H; x0 ~: H; x0:E; x0 ~= 00 |]
==> h0 x = h y + a * xi";
proof -;
assume
- "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
+ "h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H)
in (h y) + a * xi)"
- "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
- "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
+ "x = y + a (*) x0" "is_vectorspace E" "is_subspace H E"
+ "y:H" "x0 ~: H" "x0:E" "x0 ~= 00";
have "x : H + (lin x0)";
by (simp! add: vs_sum_def lin_def) force+;
- have "EX! xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
+ have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)";
proof;
- show "EX xa. ((\\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
+ show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)";
by (force!);
next;
fix xa ya;
- assume "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
- "(\\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
+ assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa"
+ "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya";
show "xa = ya"; ;
proof -;
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";
by (rule Pair_fst_snd_eq [RS iffD2]);
- have x: "x = fst xa + snd xa <*> x0 & fst xa : H";
+ have x: "x = fst xa + snd xa (*) x0 & fst xa : H";
by (force!);
- have y: "x = fst ya + snd ya <*> x0 & fst ya : H";
+ have y: "x = fst ya + snd ya (*) x0 & fst ya : H";
by (force!);
from x y; show "fst xa = fst ya & snd xa = snd ya";
by (elim conjE) (rule decomp_H0, (simp!)+);
qed;
qed;
- hence eq: "(SOME (y, a). x = y + a <*> x0 & y:H) = (y, a)";
+ hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)";
by (rule select1_equality) (force!);
thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
qed;
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Thu Apr 13 15:01:50 2000 +0200
@@ -15,8 +15,8 @@
element $\zero$ is defined. *};
consts
- prod :: "[real, 'a] => 'a" (infixr "<*>" 70)
- zero :: 'a ("<0>");
+ prod :: "[real, 'a] => 'a" (infixr "'(*')" 70)
+ zero :: 'a ("00");
syntax (symbols)
prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70)
@@ -29,7 +29,7 @@
(***
constdefs
negate :: "'a => 'a" ("- _" [100] 100)
- "- x == (- 1r) <*> x"
+ "- x == (- 1r) ( * ) x"
diff :: "'a => 'a => 'a" (infixl "-" 68)
"x - y == x + - y";
***)
@@ -51,34 +51,34 @@
"is_vectorspace V == V ~= {}
& (ALL x:V. ALL y:V. ALL z:V. ALL a b.
x + y : V
- & a <*> x : V
+ & a (*) x : V
& (x + y) + z = x + (y + z)
& x + y = y + x
- & x - x = <0>
- & <0> + x = x
- & a <*> (x + y) = a <*> x + a <*> y
- & (a + b) <*> x = a <*> x + b <*> x
- & (a * b) <*> x = a <*> b <*> x
- & 1r <*> x = x
- & - x = (- 1r) <*> x
+ & x - x = 00
+ & 00 + x = x
+ & a (*) (x + y) = a (*) x + a (*) y
+ & (a + b) (*) x = a (*) x + b (*) x
+ & (a * b) (*) x = a (*) b (*) x
+ & 1r (*) x = x
+ & - x = (- 1r) (*) x
& x - y = x + - y)";
text_raw {* \medskip *};
text {* The corresponding introduction rule is:*};
lemma vsI [intro]:
- "[| <0>:V;
+ "[| 00:V;
ALL x:V. ALL y:V. x + y : V;
- ALL x:V. ALL a. a <*> x : V;
+ ALL x:V. ALL a. a (*) x : V;
ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
ALL x:V. ALL y:V. x + y = y + x;
- ALL x:V. x - x = <0>;
- ALL x:V. <0> + x = x;
- ALL x:V. ALL y:V. ALL a. a <*> (x + y) = a <*> x + a <*> y;
- ALL x:V. ALL a b. (a + b) <*> x = a <*> x + b <*> x;
- ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x;
- ALL x:V. 1r <*> x = x;
- ALL x:V. - x = (- 1r) <*> x;
+ ALL x:V. x - x = 00;
+ ALL x:V. 00 + x = x;
+ ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
+ ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
+ ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x;
+ ALL x:V. 1r (*) x = x;
+ ALL x:V. - x = (- 1r) (*) x;
ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
proof (unfold is_vectorspace_def, intro conjI ballI allI);
fix x y z;
@@ -91,7 +91,7 @@
text {* The corresponding destruction rules are: *};
lemma negate_eq1:
- "[| is_vectorspace V; x:V |] ==> - x = (- 1r) <*> x";
+ "[| is_vectorspace V; x:V |] ==> - x = (- 1r) (*) x";
by (unfold is_vectorspace_def) simp;
lemma diff_eq1:
@@ -99,7 +99,7 @@
by (unfold is_vectorspace_def) simp;
lemma negate_eq2:
- "[| is_vectorspace V; x:V |] ==> (- 1r) <*> x = - x";
+ "[| is_vectorspace V; x:V |] ==> (- 1r) (*) x = - x";
by (unfold is_vectorspace_def) simp;
lemma diff_eq2:
@@ -114,7 +114,7 @@
by (unfold is_vectorspace_def) simp;
lemma vs_mult_closed [simp, intro??]:
- "[| is_vectorspace V; x:V |] ==> a <*> x : V";
+ "[| is_vectorspace V; x:V |] ==> a (*) x : V";
by (unfold is_vectorspace_def) simp;
lemma vs_diff_closed [simp, intro??]:
@@ -149,13 +149,13 @@
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
lemma vs_diff_self [simp]:
- "[| is_vectorspace V; x:V |] ==> x - x = <0>";
+ "[| is_vectorspace V; x:V |] ==> x - x = 00";
by (unfold is_vectorspace_def) simp;
text {* The existence of the zero element of a vector space
follows from the non-emptiness of carrier set. *};
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V";
proof -;
assume "is_vectorspace V";
have "V ~= {}"; ..;
@@ -163,64 +163,64 @@
thus ?thesis;
proof;
fix x; assume "x:V";
- have "<0> = x - x"; by (simp!);
+ have "00 = x - x"; by (simp!);
also; have "... : V"; by (simp! only: vs_diff_closed);
finally; show ?thesis; .;
qed;
qed;
lemma vs_add_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> <0> + x = x";
+ "[| is_vectorspace V; x:V |] ==> 00 + x = x";
by (unfold is_vectorspace_def) simp;
lemma vs_add_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> x + <0> = x";
+ "[| is_vectorspace V; x:V |] ==> x + 00 = x";
proof -;
assume "is_vectorspace V" "x:V";
- hence "x + <0> = <0> + x"; by simp;
+ hence "x + 00 = 00 + x"; by simp;
also; have "... = x"; by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_add_mult_distrib1:
"[| is_vectorspace V; x:V; y:V |]
- ==> a <*> (x + y) = a <*> x + a <*> y";
+ ==> a (*) (x + y) = a (*) x + a (*) y";
by (unfold is_vectorspace_def) simp;
lemma vs_add_mult_distrib2:
"[| is_vectorspace V; x:V |]
- ==> (a + b) <*> x = a <*> x + b <*> x";
+ ==> (a + b) (*) x = a (*) x + b (*) x";
by (unfold is_vectorspace_def) simp;
lemma vs_mult_assoc:
- "[| is_vectorspace V; x:V |] ==> (a * b) <*> x = a <*> (b <*> x)";
+ "[| is_vectorspace V; x:V |] ==> (a * b) (*) x = a (*) (b (*) x)";
by (unfold is_vectorspace_def) simp;
lemma vs_mult_assoc2 [simp]:
- "[| is_vectorspace V; x:V |] ==> a <*> b <*> x = (a * b) <*> x";
+ "[| is_vectorspace V; x:V |] ==> a (*) b (*) x = (a * b) (*) x";
by (simp only: vs_mult_assoc);
lemma vs_mult_1 [simp]:
- "[| is_vectorspace V; x:V |] ==> 1r <*> x = x";
+ "[| is_vectorspace V; x:V |] ==> 1r (*) x = x";
by (unfold is_vectorspace_def) simp;
lemma vs_diff_mult_distrib1:
"[| is_vectorspace V; x:V; y:V |]
- ==> a <*> (x - y) = a <*> x - a <*> y";
+ ==> a (*) (x - y) = a (*) x - a (*) y";
by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1);
lemma vs_diff_mult_distrib2:
"[| is_vectorspace V; x:V |]
- ==> (a - b) <*> x = a <*> x - (b <*> x)";
+ ==> (a - b) (*) x = a (*) x - (b (*) x)";
proof -;
assume "is_vectorspace V" "x:V";
- have " (a - b) <*> x = (a + - b ) <*> x";
+ have " (a - b) (*) x = (a + - b ) (*) x";
by (unfold real_diff_def, simp);
- also; have "... = a <*> x + (- b) <*> x";
+ also; have "... = a (*) x + (- b) (*) x";
by (rule vs_add_mult_distrib2);
- also; have "... = a <*> x + - (b <*> x)";
+ also; have "... = a (*) x + - (b (*) x)";
by (simp! add: negate_eq1);
- also; have "... = a <*> x - (b <*> x)";
+ also; have "... = a (*) x - (b (*) x)";
by (simp! add: diff_eq1);
finally; show ?thesis; .;
qed;
@@ -230,34 +230,34 @@
text{* Further derived laws: *};
lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> 0r <*> x = <0>";
+ "[| is_vectorspace V; x:V |] ==> 0r (*) x = 00";
proof -;
assume "is_vectorspace V" "x:V";
- have "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
- also; have "... = (1r + - 1r) <*> x"; by simp;
- also; have "... = 1r <*> x + (- 1r) <*> x";
+ have "0r (*) x = (1r - 1r) (*) x"; by (simp only: real_diff_self);
+ also; have "... = (1r + - 1r) (*) x"; by simp;
+ also; have "... = 1r (*) x + (- 1r) (*) x";
by (rule vs_add_mult_distrib2);
- also; have "... = x + (- 1r) <*> x"; by (simp!);
+ also; have "... = x + (- 1r) (*) x"; by (simp!);
also; have "... = x + - x"; by (simp! add: negate_eq2);;
also; have "... = x - x"; by (simp! add: diff_eq2);
- also; have "... = <0>"; by (simp!);
+ also; have "... = 00"; by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_mult_zero_right [simp]:
"[| is_vectorspace (V:: 'a::{plus, minus} set) |]
- ==> a <*> <0> = (<0>::'a)";
+ ==> a (*) 00 = (00::'a)";
proof -;
assume "is_vectorspace V";
- have "a <*> <0> = a <*> (<0> - (<0>::'a))"; by (simp!);
- also; have "... = a <*> <0> - a <*> <0>";
+ have "a (*) 00 = a (*) (00 - (00::'a))"; by (simp!);
+ also; have "... = a (*) 00 - a (*) 00";
by (rule vs_diff_mult_distrib1) (simp!)+;
- also; have "... = <0>"; by (simp!);
+ also; have "... = 00"; by (simp!);
finally; show ?thesis; .;
qed;
lemma vs_minus_mult_cancel [simp]:
- "[| is_vectorspace V; x:V |] ==> (- a) <*> - x = a <*> x";
+ "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) x";
by (simp add: negate_eq1);
lemma vs_add_minus_left_eq_diff:
@@ -271,11 +271,11 @@
qed;
lemma vs_add_minus [simp]:
- "[| is_vectorspace V; x:V |] ==> x + - x = <0>";
+ "[| is_vectorspace V; x:V |] ==> x + - x = 00";
by (simp! add: diff_eq2);
lemma vs_add_minus_left [simp]:
- "[| is_vectorspace V; x:V |] ==> - x + x = <0>";
+ "[| is_vectorspace V; x:V |] ==> - x + x = 00";
by (simp! add: diff_eq2);
lemma vs_minus_minus [simp]:
@@ -283,11 +283,11 @@
by (simp add: negate_eq1);
lemma vs_minus_zero [simp]:
- "is_vectorspace (V::'a::{minus, plus} set) ==> - (<0>::'a) = <0>";
+ "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00";
by (simp add: negate_eq1);
lemma vs_minus_zero_iff [simp]:
- "[| is_vectorspace V; x:V |] ==> (- x = <0>) = (x = <0>)"
+ "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)"
(concl is "?L = ?R");
proof -;
assume "is_vectorspace V" "x:V";
@@ -295,7 +295,7 @@
proof;
have "x = - (- x)"; by (rule vs_minus_minus [RS sym]);
also; assume ?L;
- also; have "- ... = <0>"; by (rule vs_minus_zero);
+ also; have "- ... = 00"; by (rule vs_minus_zero);
finally; show ?R; .;
qed (simp!);
qed;
@@ -314,11 +314,11 @@
by (simp add: negate_eq1 vs_add_mult_distrib1);
lemma vs_diff_zero [simp]:
- "[| is_vectorspace V; x:V |] ==> x - <0> = x";
+ "[| is_vectorspace V; x:V |] ==> x - 00 = x";
by (simp add: diff_eq1);
lemma vs_diff_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> <0> - x = - x";
+ "[| is_vectorspace V; x:V |] ==> 00 - x = - x";
by (simp add:diff_eq1);
lemma vs_add_left_cancel:
@@ -327,7 +327,7 @@
(concl is "?L = ?R");
proof;
assume "is_vectorspace V" "x:V" "y:V" "z:V";
- have "y = <0> + y"; by (simp!);
+ have "y = 00 + y"; by (simp!);
also; have "... = - x + x + y"; by (simp!);
also; have "... = - x + (x + y)";
by (simp! only: vs_add_assoc vs_neg_closed);
@@ -350,66 +350,66 @@
lemma vs_mult_left_commute:
"[| is_vectorspace V; x:V; y:V; z:V |]
- ==> x <*> y <*> z = y <*> x <*> z";
+ ==> x (*) y (*) z = y (*) x (*) z";
by (simp add: real_mult_commute);
lemma vs_mult_zero_uniq :
- "[| is_vectorspace V; x:V; a <*> x = <0>; x ~= <0> |] ==> a = 0r";
+ "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = 0r";
proof (rule classical);
- assume "is_vectorspace V" "x:V" "a <*> x = <0>" "x ~= <0>";
+ assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00";
assume "a ~= 0r";
- have "x = (rinv a * a) <*> x"; by (simp!);
- also; have "... = rinv a <*> (a <*> x)"; by (rule vs_mult_assoc);
- also; have "... = rinv a <*> <0>"; by (simp!);
- also; have "... = <0>"; by (simp!);
- finally; have "x = <0>"; .;
+ have "x = (rinv a * a) (*) x"; by (simp!);
+ also; have "... = rinv a (*) (a (*) x)"; by (rule vs_mult_assoc);
+ also; have "... = rinv a (*) 00"; by (simp!);
+ also; have "... = 00"; by (simp!);
+ finally; have "x = 00"; .;
thus "a = 0r"; by contradiction;
qed;
lemma vs_mult_left_cancel:
"[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>
- (a <*> x = a <*> y) = (x = y)"
+ (a (*) x = a (*) y) = (x = y)"
(concl is "?L = ?R");
proof;
assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
- have "x = 1r <*> x"; by (simp!);
- also; have "... = (rinv a * a) <*> x"; by (simp!);
- also; have "... = rinv a <*> (a <*> x)";
+ have "x = 1r (*) x"; by (simp!);
+ also; have "... = (rinv a * a) (*) x"; by (simp!);
+ also; have "... = rinv a (*) (a (*) x)";
by (simp! only: vs_mult_assoc);
also; assume ?L;
- also; have "rinv a <*> ... = y"; by (simp!);
+ also; have "rinv a (*) ... = y"; by (simp!);
finally; show ?R; .;
qed simp;
lemma vs_mult_right_cancel: (*** forward ***)
- "[| is_vectorspace V; x:V; x ~= <0> |]
- ==> (a <*> x = b <*> x) = (a = b)" (concl is "?L = ?R");
+ "[| is_vectorspace V; x:V; x ~= 00 |]
+ ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R");
proof;
- assume "is_vectorspace V" "x:V" "x ~= <0>";
- have "(a - b) <*> x = a <*> x - b <*> x";
+ assume "is_vectorspace V" "x:V" "x ~= 00";
+ have "(a - b) (*) x = a (*) x - b (*) x";
by (simp! add: vs_diff_mult_distrib2);
- also; assume ?L; hence "a <*> x - b <*> x = <0>"; by (simp!);
- finally; have "(a - b) <*> x = <0>"; .;
+ also; assume ?L; hence "a (*) x - b (*) x = 00"; by (simp!);
+ finally; have "(a - b) (*) x = 00"; .;
hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
thus "a = b"; by (rule real_add_minus_eq);
qed simp; (***
backward :
lemma vs_mult_right_cancel:
- "[| is_vectorspace V; x:V; x ~= <0> |] ==>
- (a <*> x = b <*> x) = (a = b)"
+ "[| is_vectorspace V; x:V; x ~= 00 |] ==>
+ (a ( * ) x = b ( * ) x) = (a = b)"
(concl is "?L = ?R");
proof;
- assume "is_vectorspace V" "x:V" "x ~= <0>";
+ assume "is_vectorspace V" "x:V" "x ~= 00";
assume l: ?L;
show "a = b";
proof (rule real_add_minus_eq);
show "a - b = 0r";
proof (rule vs_mult_zero_uniq);
- have "(a - b) <*> x = a <*> x - b <*> x";
+ have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
by (simp! add: vs_diff_mult_distrib2);
- also; from l; have "a <*> x - b <*> x = <0>"; by (simp!);
- finally; show "(a - b) <*> x = <0>"; .;
+ also; from l; have "a ( * ) x - b ( * ) x = 00"; by (simp!);
+ finally; show "(a - b) ( * ) x = 00"; .;
qed;
qed;
next;
@@ -431,7 +431,7 @@
also; have "... = z + - y + y"; by (simp! add: diff_eq1);
also; have "... = z + (- y + y)";
by (rule vs_add_assoc) (simp!)+;
- also; from vs; have "... = z + <0>";
+ also; from vs; have "... = z + 00";
by (simp only: vs_add_minus_left);
also; from vs; have "... = z"; by (simp only: vs_add_zero_right);
finally; show ?R; .;
@@ -448,22 +448,22 @@
qed;
lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x:V; y:V; x + y = <0> |] ==> x = - y";
+ "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y";
proof -;
assume "is_vectorspace V" "x:V" "y:V";
have "x = (- y + y) + x"; by (simp!);
also; have "... = - y + (x + y)"; by (simp!);
- also; assume "x + y = <0>";
- also; have "- y + <0> = - y"; by (simp!);
+ also; assume "x + y = 00";
+ also; have "- y + 00 = - y"; by (simp!);
finally; show "x = - y"; .;
qed;
lemma vs_add_minus_eq:
- "[| is_vectorspace V; x:V; y:V; x - y = <0> |] ==> x = y";
+ "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y";
proof -;
- assume "is_vectorspace V" "x:V" "y:V" "x - y = <0>";
- assume "x - y = <0>";
- hence e: "x + - y = <0>"; by (simp! add: diff_eq1);
+ assume "is_vectorspace V" "x:V" "y:V" "x - y = 00";
+ assume "x - y = 00";
+ hence e: "x + - y = 00"; by (simp! add: diff_eq1);
with _ _ _; have "x = - (- y)";
by (rule vs_add_minus_eq_minus) (simp!)+;
thus "x = y"; by (simp!);
@@ -514,12 +514,12 @@
show "?L = ?R";
proof;
assume l: ?L;
- have "x + z = <0>";
+ have "x + z = 00";
proof (rule vs_add_left_cancel [RS iffD1]);
have "y + (x + z) = x + (y + z)"; by (simp!);
also; note l;
- also; have "y = y + <0>"; by (simp!);
- finally; show "y + (x + z) = y + <0>"; .;
+ also; have "y = y + 00"; by (simp!);
+ finally; show "y + (x + z) = y + 00"; .;
qed (simp!)+;
thus "x = - z"; by (simp! add: vs_add_minus_eq_minus);
next;
@@ -532,4 +532,4 @@
qed;
qed;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Relation.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Relation.ML Thu Apr 13 15:01:50 2000 +0200
@@ -63,7 +63,7 @@
by (Blast_tac 1);
qed "diag_iff";
-Goal "diag(A) <= A Times A";
+Goal "diag(A) <= A <*> A";
by (Blast_tac 1);
qed "diag_subset_Times";
@@ -115,14 +115,14 @@
by (Blast_tac 1);
qed "comp_mono";
-Goal "[| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C";
+Goal "[| s <= A <*> B; r <= B <*> C |] ==> (r O s) <= A <*> C";
by (Blast_tac 1);
qed "comp_subset_Sigma";
(** Natural deduction for refl(r) **)
val prems = Goalw [refl_def]
- "[| r <= A Times A; !! x. x:A ==> (x,x):r |] ==> refl A r";
+ "[| r <= A <*> A; !! x. x:A ==> (x,x):r |] ==> refl A r";
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
qed "reflI";
@@ -371,7 +371,7 @@
by (Blast_tac 1);
qed "Image_Un";
-Goal "r <= A Times 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";
--- a/src/HOL/Relation.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Relation.thy Thu Apr 13 15:01:50 2000 +0200
@@ -29,7 +29,7 @@
"Range(r) == Domain(r^-1)"
refl :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
- "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
+ "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
sym :: "('a*'a) set=>bool" (*symmetry predicate*)
"sym(r) == ALL x y. (x,y): r --> (y,x): r"
--- a/src/HOL/Sexp.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Sexp.ML Thu Apr 13 15:01:50 2000 +0200
@@ -49,7 +49,7 @@
(** Introduction rules for 'pred_sexp' **)
-Goalw [pred_sexp_def] "pred_sexp <= sexp Times sexp";
+Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
by (Blast_tac 1);
qed "pred_sexp_subset_Sigma";
--- a/src/HOL/Subst/Unify.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Subst/Unify.thy Thu Apr 13 15:01:50 2000 +0200
@@ -19,7 +19,7 @@
--either the set of variables decreases
--or the first argument does (in fact, both do)
*)
- unifyRel_def "unifyRel == inv_image (finite_psubset ** measure uterm_size)
+ unifyRel_def "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
(%(M,N). (vars_of M Un vars_of N, M))"
recdef unify "unifyRel"
--- a/src/HOL/Trancl.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Trancl.ML Thu Apr 13 15:01:50 2000 +0200
@@ -342,12 +342,12 @@
by (auto_tac (claset() addIs [r_into_trancl], simpset()));
qed "irrefl_tranclI";
-Goal "[| (a,b) : r^*; r <= A Times A |] ==> a=b | a:A";
+Goal "[| (a,b) : r^*; r <= A <*> A |] ==> a=b | a:A";
by (etac rtrancl_induct 1);
by Auto_tac;
val lemma = result();
-Goalw [trancl_def] "r <= A Times A ==> r^+ <= A Times A";
+Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
by (blast_tac (claset() addSDs [lemma]) 1);
qed "trancl_subset_Sigma";
--- a/src/HOL/UNITY/Extend.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/Extend.thy Thu Apr 13 15:01:50 2000 +0200
@@ -17,7 +17,7 @@
(*Using the locale constant "f", this is f (h (x,y))) = x*)
extend_set :: "['a*'b => 'c, 'a set] => 'c set"
- "extend_set h A == h `` (A Times UNIV)"
+ "extend_set h A == h `` (A <*> UNIV)"
project_set :: "['a*'b => 'c, 'c set] => 'a set"
"project_set h C == {x. EX y. h(x,y) : C}"
--- a/src/HOL/UNITY/LessThan.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/LessThan.thy Thu Apr 13 15:01:50 2000 +0200
@@ -14,7 +14,7 @@
(*MOVE TO RELATION.THY??*)
Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
- "Restrict A r == r Int (A Times UNIV)"
+ "Restrict A r == r Int (A <*> UNIV)"
lessThan :: "nat => nat set"
"lessThan n == {i. i<n}"
--- a/src/HOL/UNITY/Lift_prog.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Thu Apr 13 15:01:50 2000 +0200
@@ -254,20 +254,20 @@
by (Force_tac 1);
qed "delete_map_neq_apply";
-(*A set of the form (A Times UNIV) ignores the second (dummy) state component*)
+(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
-Goal "(f o fst) -`` A = (f-``A) Times UNIV";
+Goal "(f o fst) -`` A = (f-``A) <*> UNIV";
by Auto_tac;
qed "vimage_o_fst_eq";
-Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)";
+Goal "(sub i -``A) <*> UNIV = lift_set i (A <*> UNIV)";
by Auto_tac;
qed "vimage_sub_eq_lift_set";
Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
Goal "[| F : preserves snd; i~=j |] \
-\ ==> lift j F : stable (lift_set i (A Times UNIV))";
+\ ==> lift j F : stable (lift_set i (A <*> UNIV))";
by (auto_tac (claset(),
simpset() addsimps [lift_def, lift_set_def,
stable_def, constrains_def,
@@ -280,9 +280,9 @@
(*If i~=j then lift j F does nothing to lift_set i, and the
premise ensures A<=B.*)
-Goal "[| F i : (A Times UNIV) co (B Times UNIV); \
+Goal "[| F i : (A <*> UNIV) co (B <*> UNIV); \
\ F j : preserves snd |] \
-\ ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))";
+\ ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))";
by (case_tac "i=j" 1);
by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def,
rename_constrains]) 1);
@@ -323,8 +323,8 @@
qed "lift_map_eq_diff";
Goal "F : preserves snd \
-\ ==> (lift i F : transient (lift_set j (A Times UNIV))) = \
-\ (i=j & F : transient (A Times UNIV) | A={})";
+\ ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \
+\ (i=j & F : transient (A <*> UNIV) | A={})";
by (case_tac "i=j" 1);
by (auto_tac (claset(), simpset() addsimps [lift_transient]));
by (auto_tac (claset(),
@@ -349,8 +349,8 @@
qed "lift_transient_eq_disj";
(*USELESS??*)
-Goal "lift_map i `` (A Times UNIV) = \
-\ (UN s:A. UN f. {insert_map i s f}) Times UNIV";
+Goal "lift_map i `` (A <*> UNIV) = \
+\ (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
by (auto_tac (claset() addSIs [bexI, image_eqI],
simpset() addsimps [lift_map_def]));
by (rtac (split RS sym) 1);
--- a/src/HOL/UNITY/PPROD.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/PPROD.ML Thu Apr 13 15:01:50 2000 +0200
@@ -49,9 +49,9 @@
(** Safety & Progress **)
Goal "[| i : I; ALL j. F j : preserves snd |] ==> \
-\ (PLam I F : (lift_set i (A Times UNIV)) co \
-\ (lift_set i (B Times UNIV))) = \
-\ (F i : (A Times UNIV) co (B Times UNIV))";
+\ (PLam I F : (lift_set i (A <*> UNIV)) co \
+\ (lift_set i (B <*> UNIV))) = \
+\ (F i : (A <*> UNIV) co (B <*> UNIV))";
by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
Join_constrains]) 1);
by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
@@ -60,8 +60,8 @@
qed "PLam_constrains";
Goal "[| i : I; ALL j. F j : preserves snd |] \
-\ ==> (PLam I F : stable (lift_set i (A Times UNIV))) = \
-\ (F i : stable (A Times UNIV))";
+\ ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = \
+\ (F i : stable (A <*> UNIV))";
by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
qed "PLam_stable";
@@ -73,9 +73,9 @@
Addsimps [PLam_constrains, PLam_stable, PLam_transient];
(*This holds because the F j cannot change (lift_set i)*)
-Goal "[| i : I; F i : (A Times UNIV) ensures (B Times UNIV); \
+Goal "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV); \
\ ALL j. F j : preserves snd |] ==> \
-\ PLam I F : lift_set i (A Times UNIV) ensures lift_set i (B Times UNIV)";
+\ PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)";
by (auto_tac (claset(),
simpset() addsimps [ensures_def, lift_transient_eq_disj,
lift_set_Un_distrib RS sym,
@@ -85,11 +85,11 @@
qed "PLam_ensures";
Goal "[| i : I; \
-\ F i : ((A Times UNIV) - (B Times UNIV)) co \
-\ ((A Times UNIV) Un (B Times UNIV)); \
-\ F i : transient ((A Times UNIV) - (B Times UNIV)); \
+\ F i : ((A <*> UNIV) - (B <*> UNIV)) co \
+\ ((A <*> UNIV) Un (B <*> UNIV)); \
+\ F i : transient ((A <*> UNIV) - (B <*> UNIV)); \
\ ALL j. F j : preserves snd |] ==> \
-\ PLam I F : lift_set i (A Times UNIV) leadsTo lift_set i (B Times UNIV)";
+\ PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)";
by (rtac (PLam_ensures RS leadsTo_Basis) 1);
by (rtac ensuresI 2);
by (ALLGOALS assume_tac);
@@ -98,9 +98,9 @@
(** invariant **)
-Goal "[| F i : invariant (A Times UNIV); i : I; \
+Goal "[| F i : invariant (A <*> UNIV); i : I; \
\ ALL j. F j : preserves snd |] \
-\ ==> PLam I F : invariant (lift_set i (A Times UNIV))";
+\ ==> PLam I F : invariant (lift_set i (A <*> UNIV))";
by (auto_tac (claset(),
simpset() addsimps [invariant_def]));
qed "invariant_imp_PLam_invariant";
--- a/src/HOL/UNITY/TimerArray.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/TimerArray.ML Thu Apr 13 15:01:50 2000 +0200
@@ -29,7 +29,7 @@
Goal "finite I \
\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
-by (eres_inst_tac [("A'1", "%i. lift_set i ({0} Times UNIV)")]
+by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")]
(finite_stable_completion RS leadsTo_weaken) 1);
by Auto_tac;
(*Safety property, already reduced to the single Timer case*)
@@ -37,7 +37,7 @@
(*Progress property for the array of Timers*)
by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
by (case_tac "m" 1);
-(*Annoying need to massage the conditions to have the form (... Times UNIV)*)
+(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
by (auto_tac (claset() addIs [subset_imp_leadsTo],
simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
lift_set_Un_distrib RS sym,
--- a/src/HOL/UNITY/Token.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/Token.thy Thu Apr 13 15:01:50 2000 +0200
@@ -58,7 +58,7 @@
defines
nodeOrder_def
"nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int
- (lessThan N Times lessThan N)"
+ (lessThan N <*> lessThan N)"
next_def
"next i == (Suc i) mod N"
--- a/src/HOL/UNITY/UNITY.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML Thu Apr 13 15:01:50 2000 +0200
@@ -14,24 +14,6 @@
Delsimps [image_Collect];
-(*** General lemmas ***)
-
-Goal "UNIV Times UNIV = UNIV";
-by Auto_tac;
-qed "UNIV_Times_UNIV";
-Addsimps [UNIV_Times_UNIV];
-
-Goal "- (UNIV Times A) = UNIV Times (-A)";
-by Auto_tac;
-qed "Compl_Times_UNIV1";
-
-Goal "- (A Times UNIV) = (-A) Times UNIV";
-by Auto_tac;
-qed "Compl_Times_UNIV2";
-
-Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
-
-
(*** The abstract type of programs ***)
val rep_ss = simpset() addsimps
--- a/src/HOL/Univ.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Univ.ML Thu Apr 13 15:01:50 2000 +0200
@@ -582,7 +582,7 @@
(*** Bounding theorems ***)
-Goal "(dprod (A Times B) (C Times D)) <= (uprod A C) Times (uprod B D)";
+Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
by (Blast_tac 1);
qed "dprod_Sigma";
@@ -595,7 +595,7 @@
by (Blast_tac 1);
qed "dprod_subset_Sigma2";
-Goal "(dsum (A Times B) (C Times D)) <= (usum A C) Times (usum B D)";
+Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
by (Blast_tac 1);
qed "dsum_Sigma";
--- a/src/HOL/WF.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/WF.ML Thu Apr 13 15:01:50 2000 +0200
@@ -20,7 +20,7 @@
(*Restriction to domain A. If r is well-founded over A then wf(r)*)
val [prem1,prem2] = Goalw [wf_def]
- "[| r <= A Times A; \
+ "[| r <= A <*> A; \
\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \
\ ==> wf(r)";
by (blast_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
--- a/src/HOL/WF_Rel.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/WF_Rel.ML Thu Apr 13 15:01:50 2000 +0200
@@ -73,7 +73,7 @@
*---------------------------------------------------------------------------*)
val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
- "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
+ "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
by (EVERY1 [rtac allI,rtac impI]);
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
by (rtac (wfa RS spec RS mp) 1);
@@ -87,7 +87,7 @@
* Transitivity of WF combinators.
*---------------------------------------------------------------------------*)
Goalw [trans_def, lex_prod_def]
- "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
+ "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
by (Simp_tac 1);
by (Blast_tac 1);
qed "trans_lex_prod";
--- a/src/HOL/WF_Rel.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/WF_Rel.thy Thu Apr 13 15:01:50 2000 +0200
@@ -19,7 +19,8 @@
less_than :: "(nat*nat)set"
inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
measure :: "('a => nat) => ('a * 'a)set"
- "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
+ lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
+ (infixr "<*lex*>" 80)
finite_psubset :: "('a set * 'a set) set"
@@ -30,9 +31,8 @@
measure_def "measure == inv_image less_than"
- lex_prod_def "ra**rb == {p. ? a a' b b'.
- p = ((a,b),(a',b')) &
- ((a,a') : ra | a=a' & (b,b') : rb)}"
+ lex_prod_def "ra <*lex*> rb == {((a,b),(a',b')) | a a' b b'.
+ ((a,a') : ra | a=a' & (b,b') : rb)}"
(* finite proper subset*)
finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
--- a/src/HOL/ex/Primrec.thy Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/ex/Primrec.thy Thu Apr 13 15:01:50 2000 +0200
@@ -19,7 +19,7 @@
Primrec = Main +
consts ack :: "nat * nat => nat"
-recdef ack "less_than ** less_than"
+recdef ack "less_than <*lex*> less_than"
"ack (0,n) = Suc n"
"ack (Suc m,0) = (ack (m, 1))"
"ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
--- a/src/HOL/ex/Tarski.ML Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/ex/Tarski.ML Thu Apr 13 15:01:50 2000 +0200
@@ -540,7 +540,7 @@
qed "T_thm_1_glb";
(* interval *)
-Goal "refl A r ==> r <= A Times A";
+Goal "refl A r ==> r <= A <*> A";
by (afs [refl_def] 1);
qed "reflE1";