# HG changeset patch
# User paulson
# Date 1087390599 -7200
# Node ID 47455995693d67ba035cae2ae14522bca98754b1
# Parent  c98eb0d6615ae7c5f989384d4f2537da0b6a020f
removal of x-symbol syntax <Sigma> for dependent products

diff -r c98eb0d6615a -r 47455995693d src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Tue Jun 15 13:24:19 2004 +0200
+++ b/src/HOL/Bali/Decl.thy	Wed Jun 16 14:56:39 2004 +0200
@@ -485,13 +485,14 @@
 done
 
 lemma subint1_def2:  
-   "subint1 G = (\<Sigma> I\<in>{I. is_iface G I}. set (isuperIfs (the (iface G I))))"
+  "subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))"
 apply (unfold subint1_def)
 apply auto
 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: {C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
 apply (unfold subcls1_def)
 apply auto
 done
diff -r c98eb0d6615a -r 47455995693d src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Tue Jun 15 13:24:19 2004 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Jun 16 14:56:39 2004 +0200
@@ -105,21 +105,12 @@
 lemma comp_is_type: "is_type (comp G) T = is_type G T"
   by ((cases T),simp,(induct G)) ((simp),(simp only: comp_is_class),(simp add: comp_is_class),(simp only: comp_is_class))
 
-lemma SIGMA_cong: "\<lbrakk> A = B; !!x. x \<in> B \<Longrightarrow> C x = D x \<rbrakk> 
-  \<Longrightarrow> (\<Sigma> x \<in> A. C x) = (\<Sigma> x \<in> B. D x)"
-by auto
-
 lemma comp_classname: "is_class G C 
   \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
 by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
 
-
 lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
-apply (simp add: subcls1_def2 comp_is_class)
-apply (rule SIGMA_cong, simp)
-apply (simp add: comp_is_class)
-apply (simp add: comp_classname)
-done
+by (auto simp add: subcls1_def2 comp_classname comp_is_class)
 
 lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)"
   apply rule
diff -r c98eb0d6615a -r 47455995693d src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jun 15 13:24:19 2004 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jun 16 14:56:39 2004 +0200
@@ -42,7 +42,8 @@
 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: {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)"
diff -r c98eb0d6615a -r 47455995693d src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Tue Jun 15 13:24:19 2004 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy	Wed Jun 16 14:56:39 2004 +0200
@@ -55,7 +55,8 @@
 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: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
 apply (unfold subcls1_def is_class_def)
 apply auto
 done
diff -r c98eb0d6615a -r 47455995693d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Jun 15 13:24:19 2004 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jun 16 14:56:39 2004 +0200
@@ -155,12 +155,11 @@
 end
 *}
 
+text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
 syntax (xsymbols)
-  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
 
 syntax (HTML output)
-  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
 
 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
@@ -603,8 +602,7 @@
 lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   by (unfold Sigma_def) blast
 
-
-lemma SigmaE:
+lemma SigmaE [elim!]:
     "[| c: Sigma A B;
         !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P
      |] ==> P"
@@ -617,18 +615,21 @@
 *}
 
 lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
-by (erule SigmaE, blast)
+by blast
 
 lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
-by (erule SigmaE, blast)
+by blast
 
 lemma SigmaE2:
     "[| (a, b) : Sigma A B;
         [| a:A;  b:B(a) |] ==> P
      |] ==> P"
-  by (blast dest: SigmaD1 SigmaD2)
+  by blast
 
-declare SigmaE [elim!] SigmaE2 [elim!]
+lemma Sigma_cong:
+     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
+      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
+by auto
 
 lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   by blast