Eliminated some infixes.
--- a/src/HOL/Univ.ML Wed Aug 18 16:11:14 1999 +0200
+++ b/src/HOL/Univ.ML Wed Aug 18 16:12:20 1999 +0200
@@ -294,13 +294,13 @@
(*** Cartesian Product ***)
-Goalw [uprod_def] "[| M:A; N:B |] ==> Scons M N : A<*>B";
+Goalw [uprod_def] "[| M:A; N:B |] ==> Scons M N : uprod A B";
by (REPEAT (ares_tac [singletonI,UN_I] 1));
qed "uprodI";
(*The general elimination rule*)
val major::prems = Goalw [uprod_def]
- "[| c : A<*>B; \
+ "[| c : uprod A B; \
\ !!x y. [| x:A; y:B; c = Scons x y |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
@@ -310,7 +310,7 @@
(*Elimination of a pair -- introduces no eigenvariables*)
val prems = Goal
- "[| Scons M N : A<*>B; [| M:A; N:B |] ==> P \
+ "[| Scons M N : uprod A B; [| M:A; N:B |] ==> P \
\ |] ==> P";
by (rtac uprodE 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
@@ -319,16 +319,16 @@
(*** Disjoint Sum ***)
-Goalw [usum_def] "M:A ==> In0(M) : A<+>B";
+Goalw [usum_def] "M:A ==> In0(M) : usum A B";
by (Blast_tac 1);
qed "usum_In0I";
-Goalw [usum_def] "N:B ==> In1(N) : A<+>B";
+Goalw [usum_def] "N:B ==> In1(N) : usum A B";
by (Blast_tac 1);
qed "usum_In1I";
val major::prems = Goalw [usum_def]
- "[| u : A<+>B; \
+ "[| u : usum A B; \
\ !!x. [| x:A; u=In0(x) |] ==> P; \
\ !!y. [| y:B; u=In1(y) |] ==> P \
\ |] ==> P";
@@ -465,11 +465,11 @@
(*** Monotonicity ***)
-Goalw [uprod_def] "[| A<=A'; B<=B' |] ==> A<*>B <= A'<*>B'";
+Goalw [uprod_def] "[| A<=A'; B<=B' |] ==> uprod A B <= uprod A' B'";
by (Blast_tac 1);
qed "uprod_mono";
-Goalw [usum_def] "[| A<=A'; B<=B' |] ==> A<+>B <= A'<+>B'";
+Goalw [usum_def] "[| A<=A'; B<=B' |] ==> usum A B <= usum A' B'";
by (Blast_tac 1);
qed "usum_mono";
@@ -529,13 +529,13 @@
(*** Equality for Cartesian Product ***)
Goalw [dprod_def]
- "[| (M,M'):r; (N,N'):s |] ==> (Scons M N, Scons M' N') : r<**>s";
+ "[| (M,M'):r; (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s";
by (Blast_tac 1);
qed "dprodI";
(*The general elimination rule*)
val major::prems = Goalw [dprod_def]
- "[| c : r<**>s; \
+ "[| c : dprod r s; \
\ !!x y x' y'. [| (x,x') : r; (y,y') : s; c = (Scons x y, Scons x' y') |] ==> P \
\ |] ==> P";
by (cut_facts_tac [major] 1);
@@ -546,16 +546,16 @@
(*** Equality for Disjoint Sum ***)
-Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : r<++>s";
+Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : dsum r s";
by (Blast_tac 1);
qed "dsum_In0I";
-Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : r<++>s";
+Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : dsum r s";
by (Blast_tac 1);
qed "dsum_In1I";
val major::prems = Goalw [dsum_def]
- "[| w : r<++>s; \
+ "[| w : dsum r s; \
\ !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; \
\ !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P \
\ |] ==> P";
@@ -571,31 +571,31 @@
(*** Monotonicity ***)
-Goal "[| r<=r'; s<=s' |] ==> r<**>s <= r'<**>s'";
+Goal "[| r<=r'; s<=s' |] ==> dprod r s <= dprod r' s'";
by (Blast_tac 1);
qed "dprod_mono";
-Goal "[| r<=r'; s<=s' |] ==> r<++>s <= r'<++>s'";
+Goal "[| r<=r'; s<=s' |] ==> dsum r s <= dsum r' s'";
by (Blast_tac 1);
qed "dsum_mono";
(*** Bounding theorems ***)
-Goal "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
+Goal "(dprod (A Times B) (C Times D)) <= (uprod A C) Times (uprod B D)";
by (Blast_tac 1);
qed "dprod_Sigma";
val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
(*Dependent version*)
-Goal "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
+Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
by Safe_tac;
by (stac Split 1);
by (Blast_tac 1);
qed "dprod_subset_Sigma2";
-Goal "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
+Goal "(dsum (A Times B) (C Times D)) <= (usum A C) Times (usum B D)";
by (Blast_tac 1);
qed "dsum_Sigma";
@@ -604,11 +604,11 @@
(*** Domain ***)
-Goal "Domain (r<**>s) = (Domain r) <*> (Domain s)";
+Goal "Domain (dprod r s) = uprod (Domain r) (Domain s)";
by Auto_tac;
qed "Domain_dprod";
-Goal "Domain (r<++>s) = (Domain r) <+> (Domain s)";
+Goal "Domain (dsum r s) = usum (Domain r) (Domain s)";
by Auto_tac;
qed "Domain_dsum";
--- a/src/HOL/Univ.thy Wed Aug 18 16:11:14 1999 +0200
+++ b/src/HOL/Univ.thy Wed Aug 18 16:12:20 1999 +0200
@@ -43,16 +43,16 @@
ntrunc :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
- "<*>" :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 80)
- "<+>" :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 70)
+ uprod :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
+ usum :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
- Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
- Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
+ Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
+ Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
- "<**>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
- => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 80)
- "<++>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
- => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 70)
+ dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+ => (('a, 'b) dtree * ('a, 'b) dtree)set"
+ dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+ => (('a, 'b) dtree * ('a, 'b) dtree)set"
local
@@ -88,21 +88,21 @@
ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
(*products and sums for the "universe"*)
- uprod_def "A<*>B == UN x:A. UN y:B. { Scons x y }"
- usum_def "A<+>B == In0``A Un In1``B"
+ uprod_def "uprod A B == UN x:A. UN y:B. { Scons x y }"
+ 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"
Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x))
- | (? y . M = In1(y) & u = d(y))"
+ | (? y . M = In1(y) & u = d(y))"
(** equality for the "universe" **)
- dprod_def "r<**>s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
+ dprod_def "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
- dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
- (UN (y,y'):s. {(In1(y),In1(y'))})"
+ dsum_def "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
+ (UN (y,y'):s. {(In1(y),In1(y'))})"
end