Extended the notion of letter and digit, such that now one may use greek,
gothic, euler, or calligraphic letters as normal letters.
--- a/NEWS Wed Aug 27 18:22:34 2003 +0200
+++ b/NEWS Thu Aug 28 01:56:40 2003 +0200
@@ -4,6 +4,20 @@
New in this Isabelle release
----------------------------
+*** General ***
+
+* Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
+ (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and
+ euler (\<a>...\<z>), are now considered normal letters, and can
+ therefore be used anywhere where an ASCII letter (a...zA...Z) has
+ until now. Similarily, the symbol digits \<0>...\<9> are now
+ considered normal digits. COMPATIBILITY: This obviously changes the
+ parsing of some terms, especially where a symbol has been used as a
+ binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x
+ will be parsed as an identifier. Fix it by inserting a space around
+ former symbols. Call 'isatool fixgreek' to try to fix parsing
+ errors in existing theory and ML files.
+
*** HOL ***
* 'specification' command added, allowing for definition by
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/fixgreek Thu Aug 28 01:56:40 2003 +0200
@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Sebastian Skalberg, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# DESCRIPTION: fix problems with greek and other foreign letters
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [FILES|DIRS...]"
+ echo
+ echo " Recursively find .thy files, fixing parse problems stemming"
+ echo " from the classification change of greek and other foreign"
+ echo " letters from symbols to letters."
+ echo
+ echo " Renames old versions of FILES by appending \"~~\"."
+ echo
+ exit 1
+}
+
+
+## process command line
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SPECS="$@"; shift "$#"
+
+
+## main
+
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
+find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/fixgreek.pl Thu Aug 28 01:56:40 2003 +0200
@@ -0,0 +1,50 @@
+#
+# $Id$
+# Author: Sebastian Skalberg, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# fixgreek.pl - fix problems with greek and other foreign letters now
+# being classified as letters instead of symbols.
+#
+
+sub fixgreek {
+ my ($file) = @_;
+
+ open (FILE, $file) || die $!;
+ undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
+ close FILE || die $!;
+
+ $_ = $text;
+
+ s/(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)([a-zA-Z0-9])/$1 $3/sg;
+
+ s/([a-zA-Z][a-zA-Z0-9]*)(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)/$1 $2/sg;
+
+ s/(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)([a-zA-Z0-9])/$1 $3/sg;
+
+ s/([a-zA-Z][a-zA-Z0-9]*)(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)/$1 $2/sg;
+
+ s/(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)([a-zA-Z0-9])/$1 $3/sg;
+
+ s/([a-zA-Z][a-zA-Z0-9]*)(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)/$1 $2/sg;
+
+ $result = $_;
+
+ if ($text ne $result) {
+ print STDERR "fixing $file\n";
+ if (! -f "$file~~") {
+ rename $file, "$file~~" || die $!;
+ }
+ open (FILE, "> $file") || die $!;
+ print FILE $result;
+ close FILE || die $!;
+ }
+}
+
+
+## main
+
+foreach $file (@ARGV) {
+ eval { &fixgreek($file); };
+ if ($@) { print STDERR "*** fixgreek $file: ", $@, "\n"; }
+}
--- a/src/HOL/Bali/Decl.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOL/Bali/Decl.thy Thu Aug 28 01:56:40 2003 +0200
@@ -491,7 +491,7 @@
done
lemma subcls1_def2:
- "subcls1 G = (\<Sigma>C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
+ "subcls1 G = (\<Sigma> C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
apply (unfold subcls1_def)
apply auto
done
--- a/src/HOL/Bali/State.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOL/Bali/State.thy Thu Aug 28 01:56:40 2003 +0200
@@ -266,7 +266,7 @@
constdefs
new_Addr :: "heap \<Rightarrow> loc option"
- "new_Addr h \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon>a. h a = None)"
+ "new_Addr h \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon> a. h a = None)"
lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
apply (unfold new_Addr_def)
--- a/src/HOL/Bali/Type.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOL/Bali/Type.thy Thu Aug 28 01:56:40 2003 +0200
@@ -51,7 +51,7 @@
constdefs
the_Class :: "ty \<Rightarrow> qtname"
- "the_Class T \<equiv> \<epsilon>C. T = Class C" (** primrec not possible here **)
+ "the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **)
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
by (auto simp add: the_Class_def)
--- a/src/HOL/MicroJava/J/TypeRel.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Aug 28 01:56:40 2003 +0200
@@ -42,7 +42,7 @@
done
lemma subcls1_def2:
-"subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
+"subcls1 G = (\<Sigma> C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
lemma finite_subcls1: "finite (subcls1 G)"
--- a/src/HOL/NanoJava/TypeRel.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Thu Aug 28 01:56:40 2003 +0200
@@ -55,7 +55,7 @@
done
lemma subcls1_def2:
-"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
+"subcls1 = (\<Sigma> C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
apply (unfold subcls1_def is_class_def)
apply auto
done
--- a/src/HOLCF/FOCUS/Buffer.ML Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOLCF/FOCUS/Buffer.ML Thu Aug 28 01:56:40 2003 +0200
@@ -247,7 +247,7 @@
Goalw [BufSt_def, BufSt_P_def] "BufEq <= BufSt";
by Safe_tac;
by (EVERY'[rename_tac "f", res_inst_tac
- [("x","\\<lambda>s. case s of Sd d => \\<Lambda>x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
+ [("x","\\<lambda>s. case s of Sd d => \\<Lambda> x. f\\<cdot>(Md d\\<leadsto>x)| \\<currency> => f")] bexI] 1);
by ( Simp_tac 1);
by (etac weak_coinduct_image 1);
by (rewtac BufSt_F_def);
--- a/src/HOLCF/FOCUS/Fstream.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Thu Aug 28 01:56:40 2003 +0200
@@ -39,7 +39,7 @@
defs
- fscons_def "fscons a \\<equiv> \\<Lambda>s. Def a && s"
+ fscons_def "fscons a \\<equiv> \\<Lambda> s. Def a && s"
fsfilter_def "fsfilter A \\<equiv> sfilter\\<cdot>(flift2 (\\<lambda>x. x\\<in>A))"
end
--- a/src/HOLCF/ex/Stream.ML Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOLCF/ex/Stream.ML Thu Aug 28 01:56:40 2003 +0200
@@ -358,7 +358,7 @@
section "smap";
bind_thm ("smap_unfold", fix_prover2 thy smap_def
- "smap = (\\<Lambda>f s. case s of x && l => f\\<cdot>x && smap\\<cdot>f\\<cdot>l)");
+ "smap = (\\<Lambda> f s. case s of x && l => f\\<cdot>x && smap\\<cdot>f\\<cdot>l)");
Goal "smap\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>";
by (stac smap_unfold 1);
@@ -570,7 +570,7 @@
section "sfilter";
bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def
- "sfilter = (\\<Lambda>p s. case s of x && xs => \
+ "sfilter = (\\<Lambda> p s. case s of x && xs => \
\ If p\\<cdot>x then x && sfilter\\<cdot>p\\<cdot>xs else sfilter\\<cdot>p\\<cdot>xs fi)");
Goal "sfilter\\<cdot>\\<bottom> = \\<bottom>";
--- a/src/HOLCF/ex/Stream.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/HOLCF/ex/Stream.thy Thu Aug 28 01:56:40 2003 +0200
@@ -18,8 +18,8 @@
defs
- smap_def "smap == fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
- sfilter_def "sfilter == fix\\<cdot>(\\<Lambda>h p s. case s of x && xs =>
+ smap_def "smap == fix\\<cdot>(\\<Lambda> h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
+ sfilter_def "sfilter == fix\\<cdot>(\\<Lambda> h p s. case s of x && xs =>
If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)"
slen_def "#s == if stream_finite s
then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>"
--- a/src/Pure/General/symbol.ML Wed Aug 27 18:22:34 2003 +0200
+++ b/src/Pure/General/symbol.ML Thu Aug 28 01:56:40 2003 +0200
@@ -85,13 +85,57 @@
fun is_ascii s = size s = 1 andalso ord s < 128;
+local
+ fun wrap s = "\\<" ^ s ^ ">"
+ val pre_digits =
+ ["zero","one","two","three","four",
+ "five","six","seven","eight","nine"]
+
+ val cal_letters =
+ ["A","B","C","D","E","F","G","H","I","J","K","L","M",
+ "N","O","P","Q","R","S","T","U","V","W","X","Y","Z"]
+
+ val small_letters =
+ ["a","b","c","d","e","f","g","h","i","j","k","l","m",
+ "n","o","p","q","r","s","t","u","v","w","x","y","z"]
+
+ val goth_letters =
+ ["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM",
+ "NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ",
+ "aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm",
+ "nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"]
+
+ val greek_letters =
+ ["alpha","beta","gamma","delta","epsilon","zeta","eta","theta",
+ "iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau",
+ "upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda",
+ "Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"]
+
+ val bbb_letters = ["bool","complex","nat","rat","real","int"]
+
+ val pre_letters =
+ cal_letters @
+ small_letters @
+ goth_letters @
+ greek_letters
+in
+val ext_digits = map wrap pre_digits
+val ext_letters = map wrap pre_letters
+val ext_letdigs = ext_digits @ ext_letters
+fun is_ext_digit s = String.isPrefix "\\<" s andalso s mem ext_digits
+fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
+fun is_ext_letdig s = String.isPrefix "\\<" s andalso s mem ext_letdigs
+end
+
fun is_letter s =
- size s = 1 andalso
- (ord "A" <= ord s andalso ord s <= ord "Z" orelse
- ord "a" <= ord s andalso ord s <= ord "z");
+ (size s = 1 andalso
+ (ord "A" <= ord s andalso ord s <= ord "Z" orelse
+ ord "a" <= ord s andalso ord s <= ord "z"))
+ orelse is_ext_letter s
fun is_digit s =
- size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9";
+ (size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9")
+ orelse is_ext_digit s
fun is_quasi "_" = true
| is_quasi "'" = true
@@ -107,10 +151,12 @@
fun is_letdig s = is_quasi_letter s orelse is_digit s;
fun is_symbolic s =
- size s > 2 andalso nth_elem_string (2, s) <> "^";
+ size s > 2 andalso nth_elem_string (2, s) <> "^"
+ andalso not (is_ext_letdig s);
fun is_printable s =
size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
+ is_ext_letdig s orelse
is_symbolic s;
fun is_identifier s =
--- a/src/ZF/AC.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC.thy Thu Aug 28 01:56:40 2003 +0200
@@ -26,7 +26,7 @@
apply (erule bspec, assumption)
done
-lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
+lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C)-{0}. X)"
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
apply (erule_tac [2] exI, blast)
done
@@ -52,7 +52,7 @@
apply (erule_tac [2] fun_weaken_type, blast+)
done
-lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"
+lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)"
apply (rule AC_Pi)
apply (simp_all add: non_empty_family)
done
--- a/src/ZF/AC/AC15_WO6.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC/AC15_WO6.thy Thu Aug 28 01:56:40 2003 +0200
@@ -262,7 +262,7 @@
lemma AC13_AC1_lemma:
"\<forall>B \<in> A. f(B)\<noteq>0 & f(B)<=B & f(B) \<lesssim> 1
- ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Pi>X \<in> A. X)"
+ ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Pi> X \<in> A. X)"
apply (rule lam_type)
apply (drule bspec, assumption)
apply (elim conjE)
--- a/src/ZF/AC/AC17_AC1.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC/AC17_AC1.thy Thu Aug 28 01:56:40 2003 +0200
@@ -14,7 +14,7 @@
(** AC0 is equivalent to AC1.
AC0 comes from Suppes, AC1 from Rubin & Rubin **)
-lemma AC0_AC1_lemma: "[| f:(\<Pi>X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi>X \<in> D. X)"
+lemma AC0_AC1_lemma: "[| f:(\<Pi> X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi> X \<in> D. X)"
by (fast intro!: lam_type apply_type)
lemma AC0_AC1: "AC0 ==> AC1"
@@ -28,7 +28,7 @@
(**** The proof of AC1 ==> AC17 ****)
-lemma AC1_AC17_lemma: "f \<in> (\<Pi>X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
+lemma AC1_AC17_lemma: "f \<in> (\<Pi> X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
apply (rule Pi_type, assumption)
apply (drule apply_type, assumption, fast)
done
@@ -143,7 +143,7 @@
(* ********************************************************************** *)
lemma AC1_AC2_aux1:
- "[| f:(\<Pi>X \<in> A. X); B \<in> A; 0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
+ "[| f:(\<Pi> X \<in> A. X); B \<in> A; 0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
by (fast elim!: apply_type)
lemma AC1_AC2_aux2:
@@ -177,7 +177,7 @@
lemma AC2_AC1_aux3:
"\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D Int C = {y}
- ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi>X \<in> A. X)"
+ ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi> X \<in> A. X)"
apply (rule lam_type)
apply (drule bspec, blast)
apply (blast intro: AC2_AC1_aux2 fst_type)
@@ -233,7 +233,7 @@
(* ********************************************************************** *)
lemma AC3_AC1_lemma:
- "b\<notin>A ==> (\<Pi>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi>x \<in> A. x)"
+ "b\<notin>A ==> (\<Pi> x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi> x \<in> A. x)"
apply (simp add: id_def cong add: Pi_cong)
apply (rule_tac b = A in subst_context, fast)
done
@@ -276,7 +276,7 @@
done
lemma AC5_AC4_aux4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]
- ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi>x \<in> C. R``{x})"
+ ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi> x \<in> C. R``{x})"
apply (rule lam_type)
apply (force dest: apply_type)
done
--- a/src/ZF/AC/AC18_AC19.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC/AC18_AC19.thy Thu Aug 28 01:56:40 2003 +0200
@@ -17,14 +17,14 @@
(* ********************************************************************** *)
lemma PROD_subsets:
- "[| f \<in> (\<Pi>b \<in> {P(a). a \<in> A}. b); \<forall>a \<in> A. P(a)<=Q(a) |]
- ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi>a \<in> A. Q(a))"
+ "[| f \<in> (\<Pi> b \<in> {P(a). a \<in> A}. b); \<forall>a \<in> A. P(a)<=Q(a) |]
+ ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi> a \<in> A. Q(a))"
by (rule lam_type, drule apply_type, auto)
lemma lemma_AC18:
- "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi>X \<in> A. X)); A \<noteq> 0 |]
+ "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |]
==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq>
- (\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
+ (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
apply (rule subsetI)
apply (erule_tac x = "{{b \<in> B (a) . x \<in> X (a,b) }. a \<in> A}" in allE)
apply (erule impE, fast)
@@ -67,12 +67,12 @@
done
lemma lemma1_2:
- "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B); a \<in> A |]
+ "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B); a \<in> A |]
==> f`(uu(a))-{0} \<in> a"
apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type)
done
-lemma lemma1: "\<exists>f. f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi>B \<in> A. B)"
+lemma lemma1: "\<exists>f. f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi> B \<in> A. B)"
apply (erule exE)
apply (rule_tac x = "\<lambda>a\<in>A. if (f` (uu(a)) \<in> a, f` (uu(a)), f` (uu(a))-{0})"
in exI)
--- a/src/ZF/AC/AC7_AC9.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC/AC7_AC9.thy Thu Aug 28 01:56:40 2003 +0200
@@ -52,16 +52,16 @@
(* the proof. *)
(* ********************************************************************** *)
-lemma lemma1_1: "y \<in> (\<Pi>B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Pi>B \<in> A. B)"
+lemma lemma1_1: "y \<in> (\<Pi> B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Pi> B \<in> A. B)"
by (fast intro!: lam_type snd_type apply_type)
lemma lemma1_2:
- "y \<in> (\<Pi>B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Pi>B \<in> A. Y*B)"
+ "y \<in> (\<Pi> B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Pi> B \<in> A. Y*B)"
apply (fast intro!: lam_type apply_type)
done
lemma AC7_AC6_lemma1:
- "(\<Pi>B \<in> {(nat->Union(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi>B \<in> A. B) \<noteq> 0"
+ "(\<Pi> B \<in> {(nat->Union(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
by (fast intro!: equals0I lemma1_1 lemma1_2)
lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> Union(A)) * C. C \<in> A}"
@@ -91,7 +91,7 @@
done
lemma AC1_AC8_lemma2:
- "[| f \<in> (\<Pi>X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)"
+ "[| f \<in> (\<Pi> X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)"
apply (simp, fast elim!: apply_type)
done
@@ -151,7 +151,7 @@
"\<forall>B1 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.
\<forall>B2 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.
f`<B1,B2> \<in> bij(B1, B2)
- ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi>X \<in> A. X)"
+ ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi> X \<in> A. X)"
apply (intro lam_type snd_type fst_type)
apply (rule apply_type [OF _ consI1])
apply (fast intro!: fun_weaken_type bij_is_fun)
--- a/src/ZF/AC/AC_Equiv.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Thu Aug 28 01:56:40 2003 +0200
@@ -41,7 +41,7 @@
"WO7 == \<forall>A. Finite(A) <-> (\<forall>R. well_ord(A,R) --> well_ord(A,converse(R)))"
WO8 :: o
- "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi>X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
+ "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
(* Auxiliary concepts needed below *)
@@ -54,28 +54,28 @@
(* Axioms of Choice *)
AC0 :: o
- "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi>X \<in> Pow(A)-{0}. X)"
+ "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
AC1 :: o
- "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi>X \<in> A. X))"
+ "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
AC2 :: o
"AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A)
--> (\<exists>C. \<forall>B \<in> A. \<exists>y. B Int C = {y})"
AC3 :: o
- "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi>x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
+ "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi> x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
AC4 :: o
- "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi>x \<in> domain(R). R``{x})))"
+ "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
AC5 :: o
"AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x"
AC6 :: o
- "AC6 == \<forall>A. 0\<notin>A --> (\<Pi>B \<in> A. B)\<noteq>0"
+ "AC6 == \<forall>A. 0\<notin>A --> (\<Pi> B \<in> A. B)\<noteq>0"
AC7 :: o
- "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi>B \<in> A. B) \<noteq> 0"
+ "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi> B \<in> A. B) \<noteq> 0"
AC8 :: o
"AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2)
@@ -121,13 +121,13 @@
locale AC18 =
assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) -->
((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =
- (\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
+ (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
--"AC18 cannot be expressed within the object-logic"
constdefs
AC19 :: o
"AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A --> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =
- (\<Union>f \<in> (\<Pi>B \<in> A. B). \<Inter>a \<in> A. f`a))"
+ (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))"
@@ -194,10 +194,10 @@
by (blast dest!: well_ord_imp_ex1_first
[THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
-lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi>X \<in> A. X)"
+lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
by (fast elim!: first_in_B intro!: lam_type)
-lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi>X \<in> Pow(A)-{0}. X)"
+lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)"
by (fast elim!: well_ord_subset [THEN ex_choice_fun])
--- a/src/ZF/AC/HH.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC/HH.thy Thu Aug 28 01:56:40 2003 +0200
@@ -208,8 +208,8 @@
done
lemma lam_singI:
- "f \<in> (\<Pi>X \<in> Pow(x)-{0}. F(X))
- ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Pi>X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
+ "f \<in> (\<Pi> X \<in> Pow(x)-{0}. F(X))
+ ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Pi> X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
by (fast del: DiffI DiffE
intro!: lam_type singleton_eq_iff [THEN iffD2] dest: apply_type)
@@ -233,7 +233,7 @@
Perhaps it could be simplified. *)
lemma bijection:
- "f \<in> (\<Pi>X \<in> Pow(x) - {0}. X)
+ "f \<in> (\<Pi> X \<in> Pow(x) - {0}. X)
==> \<exists>g. g \<in> bij(x, LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})"
apply (rule exI)
apply (rule bij_Least_HH_x [THEN bij_converse_bij])
--- a/src/ZF/Coind/Map.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Coind/Map.thy Thu Aug 28 01:56:40 2003 +0200
@@ -23,7 +23,7 @@
"map_emp == 0"
map_owr :: "[i,i,i]=>i"
- "map_owr(m,a,b) == \<Sigma>x \<in> {a} Un domain(m). if x=a then b else m``{x}"
+ "map_owr(m,a,b) == \<Sigma> x \<in> {a} Un domain(m). if x=a then b else m``{x}"
map_app :: "[i,i]=>i"
"map_app(m,a) == m``{a}"
--- a/src/ZF/Constructible/AC_in_L.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy Thu Aug 28 01:56:40 2003 +0200
@@ -244,7 +244,7 @@
DPow_least :: "[i,i,i,i]=>i"
--{*function yielding the smallest index for @{term X}*}
- "DPow_least(f,r,A,X) == \<mu>k. DPow_ord(f,r,A,X,k)"
+ "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
DPow_r :: "[i,i,i]=>i"
--{*a wellordering on @{term "DPow(A)"}*}
--- a/src/ZF/Constructible/Formula.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Constructible/Formula.thy Thu Aug 28 01:56:40 2003 +0200
@@ -820,7 +820,7 @@
text{*The rank function for the constructible universe*}
constdefs
lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
- "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
+ "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
by (simp add: L_def, blast)
--- a/src/ZF/Constructible/L_axioms.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Thu Aug 28 01:56:40 2003 +0200
@@ -189,7 +189,7 @@
text{*instances of locale constants*}
constdefs
L_F0 :: "[i=>o,i] => i"
- "L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
+ "L_F0(P,y) == \<mu> b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
L_FF :: "[i=>o,i] => i"
"L_FF(P) == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)"
--- a/src/ZF/Constructible/Normal.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Constructible/Normal.thy Thu Aug 28 01:56:40 2003 +0200
@@ -84,7 +84,7 @@
assumes closed: "a\<in>A ==> Closed(P(a))"
and unbounded: "a\<in>A ==> Unbounded(P(a))"
and A_non0: "A\<noteq>0"
- defines "next_greater(a,x) == \<mu>y. x<y \<and> P(a,y)"
+ defines "next_greater(a,x) == \<mu> y. x<y \<and> P(a,y)"
and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
--- a/src/ZF/Constructible/Reflection.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Constructible/Reflection.thy Thu Aug 28 01:56:40 2003 +0200
@@ -42,7 +42,7 @@
fixes F0 --{*ordinal for a specific value @{term y}*}
fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
- defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) & P(<y,z>)) -->
+ defines "F0(P,y) == \<mu> b. (\<exists>z. M(z) & P(<y,z>)) -->
(\<exists>z\<in>Mset(b). P(<y,z>))"
and "FF(P) == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a"
@@ -354,8 +354,8 @@
to be relativized.*}
lemma (in reflection)
"Reflects(?Cl,
- \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi>X \<in> A. X)),
- \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
+ \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
+ \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"
by fast
end
--- a/src/ZF/Induct/Brouwer.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Induct/Brouwer.thy Thu Aug 28 01:56:40 2003 +0200
@@ -53,7 +53,7 @@
monos Pi_mono
type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
-lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))"
+lemma Well_unfold: "Well(A, B) = (\<Sigma> x \<in> A. B(x) -> Well(A, B))"
by (fast intro!: Well.intros [unfolded Well.con_defs]
elim: Well.cases [unfolded Well.con_defs])
--- a/src/ZF/OrderArith.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/OrderArith.thy Thu Aug 28 01:56:40 2003 +0200
@@ -556,7 +556,7 @@
text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *}
lemma Pow_Sigma_bij:
"(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})
- \<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
+ \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
apply (blast intro: lam_type)
apply (blast dest: apply_type, simp_all)
--- a/src/ZF/UNITY/State.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/UNITY/State.thy Thu Aug 28 01:56:40 2003 +0200
@@ -23,7 +23,7 @@
constdefs
state :: i
- "state == \<Pi>x \<in> var. cons(default_val(x), type_of(x))"
+ "state == \<Pi> x \<in> var. cons(default_val(x), type_of(x))"
st0 :: i
"st0 == \<lambda>x \<in> var. default_val(x)"
--- a/src/ZF/Zorn.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Zorn.thy Thu Aug 28 01:56:40 2003 +0200
@@ -197,14 +197,14 @@
done
lemma choice_super:
- "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
+ "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
==> ch ` super(S,X) \<in> super(S,X)"
apply (erule apply_type)
apply (unfold super_def maxchain_def, blast)
done
lemma choice_not_equals:
- "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
+ "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
==> ch ` super(S,X) \<noteq> X"
apply (rule notI)
apply (drule choice_super, assumption, assumption)
@@ -213,7 +213,7 @@
text{*This justifies Definition 4.4*}
lemma Hausdorff_next_exists:
- "ch \<in> (\<Pi>X \<in> Pow(chain(S))-{0}. X) ==>
+ "ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==>
\<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
apply (rule_tac x="\<lambda>X\<in>Pow(S).
@@ -237,7 +237,7 @@
text{*Lemma 4*}
lemma TFin_chain_lemma4:
"[| c \<in> TFin(S,next);
- ch \<in> (\<Pi>X \<in> Pow(chain(S))-{0}. X);
+ ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X);
next \<in> increasing(S);
\<forall>X \<in> Pow(S). next`X =
if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
@@ -344,14 +344,14 @@
text{** Defining the "next" operation for Zermelo's Theorem **}
lemma choice_Diff:
- "[| ch \<in> (\<Pi>X \<in> Pow(S) - {0}. X); X \<subseteq> S; X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
+ "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X); X \<subseteq> S; X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
apply (erule apply_type)
apply (blast elim!: equalityE)
done
text{*This justifies Definition 6.1*}
lemma Zermelo_next_exists:
- "ch \<in> (\<Pi>X \<in> Pow(S)-{0}. X) ==>
+ "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
\<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
next`X = (if X=S then S else cons(ch`(S-X), X))"
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
@@ -371,7 +371,7 @@
text{*The construction of the injection*}
lemma choice_imp_injection:
- "[| ch \<in> (\<Pi>X \<in> Pow(S)-{0}. X);
+ "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
next \<in> increasing(S);
\<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
==> (\<lambda> x \<in> S. Union({y \<in> TFin(S,next). x \<notin> y}))
--- a/src/ZF/equalities.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/equalities.thy Thu Aug 28 01:56:40 2003 +0200
@@ -537,19 +537,19 @@
by blast
lemma SUM_UN_distrib1:
- "(\<Sigma>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma>x\<in>C(y). B(x))"
+ "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
by blast
lemma SUM_UN_distrib2:
- "(\<Sigma>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma>i\<in>I. C(i,j))"
+ "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
by blast
lemma SUM_Un_distrib1:
- "(\<Sigma>i\<in>I Un J. C(i)) = (\<Sigma>i\<in>I. C(i)) Un (\<Sigma>j\<in>J. C(j))"
+ "(\<Sigma> i\<in>I Un J. C(i)) = (\<Sigma> i\<in>I. C(i)) Un (\<Sigma> j\<in>J. C(j))"
by blast
lemma SUM_Un_distrib2:
- "(\<Sigma>i\<in>I. A(i) Un B(i)) = (\<Sigma>i\<in>I. A(i)) Un (\<Sigma>i\<in>I. B(i))"
+ "(\<Sigma> i\<in>I. A(i) Un B(i)) = (\<Sigma> i\<in>I. A(i)) Un (\<Sigma> i\<in>I. B(i))"
by blast
(*First-order version of the above, for rewriting*)
@@ -557,11 +557,11 @@
by (rule SUM_Un_distrib2)
lemma SUM_Int_distrib1:
- "(\<Sigma>i\<in>I Int J. C(i)) = (\<Sigma>i\<in>I. C(i)) Int (\<Sigma>j\<in>J. C(j))"
+ "(\<Sigma> i\<in>I Int J. C(i)) = (\<Sigma> i\<in>I. C(i)) Int (\<Sigma> j\<in>J. C(j))"
by blast
lemma SUM_Int_distrib2:
- "(\<Sigma>i\<in>I. A(i) Int B(i)) = (\<Sigma>i\<in>I. A(i)) Int (\<Sigma>i\<in>I. B(i))"
+ "(\<Sigma> i\<in>I. A(i) Int B(i)) = (\<Sigma> i\<in>I. A(i)) Int (\<Sigma> i\<in>I. B(i))"
by blast
(*First-order version of the above, for rewriting*)
@@ -569,7 +569,7 @@
by (rule SUM_Int_distrib2)
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
-lemma SUM_eq_UN: "(\<Sigma>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
+lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
by blast
lemma times_subset_iff:
@@ -577,7 +577,7 @@
by blast
lemma Int_Sigma_eq:
- "(\<Sigma>x \<in> A'. B'(x)) Int (\<Sigma>x \<in> A. B(x)) = (\<Sigma>x \<in> A' Int A. B'(x) Int B(x))"
+ "(\<Sigma> x \<in> A'. B'(x)) Int (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' Int A. B'(x) Int B(x))"
by blast
(** Domain **)
--- a/src/ZF/ex/Limit.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/ex/Limit.thy Thu Aug 28 01:56:40 2003 +0200
@@ -103,8 +103,8 @@
(* Twice, constructions on cpos are more difficult. *)
iprod :: "i=>i"
"iprod(DD) ==
- <(\<Pi>n \<in> nat. set(DD`n)),
- {x:(\<Pi>n \<in> nat. set(DD`n))*(\<Pi>n \<in> nat. set(DD`n)).
+ <(\<Pi> n \<in> nat. set(DD`n)),
+ {x:(\<Pi> n \<in> nat. set(DD`n))*(\<Pi> n \<in> nat. set(DD`n)).
\<forall>n \<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"
mkcpo :: "[i,i=>o]=>i"
@@ -1024,18 +1024,18 @@
(*----------------------------------------------------------------------*)
lemma iprodI:
- "x:(\<Pi>n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
+ "x:(\<Pi> n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
by (simp add: set_def iprod_def)
lemma iprodE:
- "x \<in> set(iprod(DD)) ==> x:(\<Pi>n \<in> nat. set(DD`n))"
+ "x \<in> set(iprod(DD)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
by (simp add: set_def iprod_def)
(* Contains typing conditions in contrast to HOL-ST *)
lemma rel_iprodI:
- "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi>n \<in> nat. set(DD`n));
- g:(\<Pi>n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
+ "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi> n \<in> nat. set(DD`n));
+ g:(\<Pi> n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
by (simp add: iprod_def rel_I)
lemma rel_iprodE:
@@ -1205,14 +1205,14 @@
(*----------------------------------------------------------------------*)
lemma DinfI:
- "[|x:(\<Pi>n \<in> nat. set(DD`n));
+ "[|x:(\<Pi> n \<in> nat. set(DD`n));
!!n. n \<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|]
==> x \<in> set(Dinf(DD,ee))"
apply (simp add: Dinf_def)
apply (blast intro: mkcpoI iprodI)
done
-lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi>n \<in> nat. set(DD`n))"
+lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
apply (simp add: Dinf_def)
apply (erule mkcpoD1 [THEN iprodE])
done
@@ -1226,7 +1226,7 @@
lemma rel_DinfI:
"[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n);
- x:(\<Pi>n \<in> nat. set(DD`n)); y:(\<Pi>n \<in> nat. set(DD`n))|]
+ x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|]
==> rel(Dinf(DD,ee),x,y)"
apply (simp add: Dinf_def)
apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI)