removal of x-symbol syntax <Sigma> for dependent products
authorpaulson
Wed Jun 16 14:56:39 2004 +0200 (2004-06-16)
changeset 1495247455995693d
parent 14951 c98eb0d6615a
child 14953 27decf8d40ff
removal of x-symbol syntax <Sigma> for dependent products
src/HOL/Bali/Decl.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Bali/Decl.thy	Tue Jun 15 13:24:19 2004 +0200
     1.2 +++ b/src/HOL/Bali/Decl.thy	Wed Jun 16 14:56:39 2004 +0200
     1.3 @@ -485,13 +485,14 @@
     1.4  done
     1.5  
     1.6  lemma subint1_def2:  
     1.7 -   "subint1 G = (\<Sigma> I\<in>{I. is_iface G I}. set (isuperIfs (the (iface G I))))"
     1.8 +  "subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))"
     1.9  apply (unfold subint1_def)
    1.10  apply auto
    1.11  done
    1.12  
    1.13  lemma subcls1_def2: 
    1.14 - "subcls1 G = (\<Sigma> C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
    1.15 +  "subcls1 G = 
    1.16 +     (SIGMA C: {C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
    1.17  apply (unfold subcls1_def)
    1.18  apply auto
    1.19  done
     2.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Tue Jun 15 13:24:19 2004 +0200
     2.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Jun 16 14:56:39 2004 +0200
     2.3 @@ -105,21 +105,12 @@
     2.4  lemma comp_is_type: "is_type (comp G) T = is_type G T"
     2.5    by ((cases T),simp,(induct G)) ((simp),(simp only: comp_is_class),(simp add: comp_is_class),(simp only: comp_is_class))
     2.6  
     2.7 -lemma SIGMA_cong: "\<lbrakk> A = B; !!x. x \<in> B \<Longrightarrow> C x = D x \<rbrakk> 
     2.8 -  \<Longrightarrow> (\<Sigma> x \<in> A. C x) = (\<Sigma> x \<in> B. D x)"
     2.9 -by auto
    2.10 -
    2.11  lemma comp_classname: "is_class G C 
    2.12    \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
    2.13  by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
    2.14  
    2.15 -
    2.16  lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
    2.17 -apply (simp add: subcls1_def2 comp_is_class)
    2.18 -apply (rule SIGMA_cong, simp)
    2.19 -apply (simp add: comp_is_class)
    2.20 -apply (simp add: comp_classname)
    2.21 -done
    2.22 +by (auto simp add: subcls1_def2 comp_classname comp_is_class)
    2.23  
    2.24  lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)"
    2.25    apply rule
     3.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jun 15 13:24:19 2004 +0200
     3.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jun 16 14:56:39 2004 +0200
     3.3 @@ -42,7 +42,8 @@
     3.4  done
     3.5  
     3.6  lemma subcls1_def2: 
     3.7 -"subcls1 G = (\<Sigma> C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
     3.8 +  "subcls1 G = 
     3.9 +     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    3.10    by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    3.11  
    3.12  lemma finite_subcls1: "finite (subcls1 G)"
     4.1 --- a/src/HOL/NanoJava/TypeRel.thy	Tue Jun 15 13:24:19 2004 +0200
     4.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Wed Jun 16 14:56:39 2004 +0200
     4.3 @@ -55,7 +55,8 @@
     4.4  done
     4.5  
     4.6  lemma subcls1_def2: 
     4.7 -"subcls1 = (\<Sigma> C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
     4.8 +  "subcls1 = 
     4.9 +    (SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
    4.10  apply (unfold subcls1_def is_class_def)
    4.11  apply auto
    4.12  done
     5.1 --- a/src/HOL/Product_Type.thy	Tue Jun 15 13:24:19 2004 +0200
     5.2 +++ b/src/HOL/Product_Type.thy	Wed Jun 16 14:56:39 2004 +0200
     5.3 @@ -155,12 +155,11 @@
     5.4  end
     5.5  *}
     5.6  
     5.7 +text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
     5.8  syntax (xsymbols)
     5.9 -  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    5.10    "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    5.11  
    5.12  syntax (HTML output)
    5.13 -  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    5.14    "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    5.15  
    5.16  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    5.17 @@ -603,8 +602,7 @@
    5.18  lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
    5.19    by (unfold Sigma_def) blast
    5.20  
    5.21 -
    5.22 -lemma SigmaE:
    5.23 +lemma SigmaE [elim!]:
    5.24      "[| c: Sigma A B;
    5.25          !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P
    5.26       |] ==> P"
    5.27 @@ -617,18 +615,21 @@
    5.28  *}
    5.29  
    5.30  lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
    5.31 -by (erule SigmaE, blast)
    5.32 +by blast
    5.33  
    5.34  lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
    5.35 -by (erule SigmaE, blast)
    5.36 +by blast
    5.37  
    5.38  lemma SigmaE2:
    5.39      "[| (a, b) : Sigma A B;
    5.40          [| a:A;  b:B(a) |] ==> P
    5.41       |] ==> P"
    5.42 -  by (blast dest: SigmaD1 SigmaD2)
    5.43 +  by blast
    5.44  
    5.45 -declare SigmaE [elim!] SigmaE2 [elim!]
    5.46 +lemma Sigma_cong:
    5.47 +     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
    5.48 +      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
    5.49 +by auto
    5.50  
    5.51  lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
    5.52    by blast