undid UN/INT syntax
authornipkow
Fri Aug 06 16:55:14 2004 +0200 (2004-08-06)
changeset 15120f0359f75682e
parent 15119 e5f167042c1d
child 15121 1198032bad25
undid UN/INT syntax
src/HOL/Algebra/Coset.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Fri Aug 06 16:54:26 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Aug 06 16:55:14 2004 +0200
     1.3 @@ -153,13 +153,13 @@
     1.4    proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
     1.5      fix x
     1.6      assume x: "x \<in> carrier G"
     1.7 -    show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) = (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
     1.8 +    show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
     1.9      proof
    1.10 -      show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
    1.11 +      show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
    1.12        proof clarify
    1.13          fix n
    1.14          assume n: "n \<in> N" 
    1.15 -        show "n \<otimes> x \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
    1.16 +        show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
    1.17          proof 
    1.18            from closed [of "inv x"]
    1.19            show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
    1.20 @@ -168,11 +168,11 @@
    1.21          qed
    1.22        qed
    1.23      next
    1.24 -      show "(\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
    1.25 +      show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
    1.26        proof clarify
    1.27          fix n
    1.28          assume n: "n \<in> N" 
    1.29 -        show "x \<otimes> n \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
    1.30 +        show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
    1.31          proof 
    1.32            show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
    1.33            show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
    1.34 @@ -261,7 +261,7 @@
    1.35  proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
    1.36    fix h
    1.37    assume "h \<in> H"
    1.38 -  show "inv x \<otimes> inv h \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {j \<otimes> inv x})"
    1.39 +  show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
    1.40    proof
    1.41      show "inv x \<otimes> inv h \<otimes> x \<in> H"
    1.42        by (simp add: inv_op_closed1 prems)
    1.43 @@ -271,7 +271,7 @@
    1.44  next
    1.45    fix h
    1.46    assume "h \<in> H"
    1.47 -  show "h \<otimes> inv x \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {inv x \<otimes> inv j})"
    1.48 +  show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
    1.49    proof
    1.50      show "x \<otimes> inv h \<otimes> inv x \<in> H"
    1.51        by (simp add: inv_op_closed2 prems)
    1.52 @@ -651,7 +651,7 @@
    1.53      assume y: "y \<in> carrier H"
    1.54      with h obtain g where g: "g \<in> carrier G" "h g = y"
    1.55        by (blast elim: equalityE); 
    1.56 -    hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}" 
    1.57 +    hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
    1.58        by (auto simp add: y kernel_def r_coset_def) 
    1.59      with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
    1.60        by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
     2.1 --- a/src/HOL/Induct/QuoDataType.thy	Fri Aug 06 16:54:26 2004 +0200
     2.2 +++ b/src/HOL/Induct/QuoDataType.thy	Fri Aug 06 16:55:14 2004 +0200
     2.3 @@ -147,15 +147,15 @@
     2.4  
     2.5    MPair :: "[msg,msg] \<Rightarrow> msg"
     2.6     "MPair X Y ==
     2.7 -       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> \<Union>\<^bsub>V \<in> Rep_Msg Y\<^esub> msgrel``{MPAIR U V})"
     2.8 +       Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
     2.9  
    2.10    Crypt :: "[nat,msg] \<Rightarrow> msg"
    2.11     "Crypt K X ==
    2.12 -       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{CRYPT K U})"
    2.13 +       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
    2.14  
    2.15    Decrypt :: "[nat,msg] \<Rightarrow> msg"
    2.16     "Decrypt K X ==
    2.17 -       Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{DECRYPT K U})"
    2.18 +       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
    2.19  
    2.20  
    2.21  text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
    2.22 @@ -228,7 +228,7 @@
    2.23  
    2.24  constdefs
    2.25    nonces :: "msg \<Rightarrow> nat set"
    2.26 -   "nonces X == \<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> freenonces U"
    2.27 +   "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
    2.28  
    2.29  lemma nonces_congruent: "congruent msgrel freenonces"
    2.30  by (simp add: congruent_def msgrel_imp_eq_freenonces) 
    2.31 @@ -263,7 +263,7 @@
    2.32  
    2.33  constdefs
    2.34    left :: "msg \<Rightarrow> msg"
    2.35 -   "left X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeleft U})"
    2.36 +   "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
    2.37  
    2.38  lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeleft U})"
    2.39  by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
    2.40 @@ -297,7 +297,7 @@
    2.41  
    2.42  constdefs
    2.43    right :: "msg \<Rightarrow> msg"
    2.44 -   "right X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeright U})"
    2.45 +   "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
    2.46  
    2.47  lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeright U})"
    2.48  by (simp add: congruent_def msgrel_imp_eqv_freeright) 
     3.1 --- a/src/HOL/Set.thy	Fri Aug 06 16:54:26 2004 +0200
     3.2 +++ b/src/HOL/Set.thy	Fri Aug 06 16:55:14 2004 +0200
     3.3 @@ -120,17 +120,30 @@
     3.4    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
     3.5    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
     3.6  
     3.7 -syntax (input)
     3.8 +syntax (xsymbols)
     3.9    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
    3.10    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
    3.11    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
    3.12    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
    3.13 -
    3.14 +(*
    3.15  syntax (xsymbols)
    3.16    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
    3.17    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
    3.18    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    3.19    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    3.20 +*)
    3.21 +syntax (latex output)
    3.22 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
    3.23 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
    3.24 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    3.25 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    3.26 +
    3.27 +text{* Note the difference between ordinary xsymbol syntax of indexed
    3.28 +unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
    3.29 +and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
    3.30 +former does not make the index expression a subscript of the
    3.31 +union/intersection symbol because this leads to problems with nested
    3.32 +subscripts in Proof General.  *}
    3.33  
    3.34  
    3.35  translations