more symbols;
authorwenzelm
Wed Mar 05 21:51:30 2014 +0100 (2014-03-05)
changeset 559263ef14caf5637
parent 55925 56165322c98b
child 55927 30c41a8eca0e
more symbols;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/UnivPoly.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 20:07:43 2014 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 21:51:30 2014 +0100
     1.3 @@ -54,8 +54,8 @@
     1.4  locale abelian_group_hom = G: abelian_group G + H: abelian_group H
     1.5      for G (structure) and H (structure) +
     1.6    fixes h
     1.7 -  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
     1.8 -                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
     1.9 +  assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
    1.10 +                                  \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
    1.11  
    1.12  lemmas a_r_coset_defs =
    1.13    a_r_coset_def r_coset_def
    1.14 @@ -129,12 +129,12 @@
    1.15      folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
    1.16  
    1.17  lemma (in abelian_group) a_coset_join1:
    1.18 -     "[| H +> x = H;  x \<in> carrier G;  subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \<in> H"
    1.19 +     "[| H +> x = H;  x \<in> carrier G;  subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H"
    1.20  by (rule group.coset_join1 [OF a_group,
    1.21      folded a_r_coset_def, simplified monoid_record_simps])
    1.22  
    1.23  lemma (in abelian_group) a_solve_equation:
    1.24 -    "\<lbrakk>subgroup H (|carrier = carrier G, mult = add G, one = zero G|); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
    1.25 +    "\<lbrakk>subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
    1.26  by (rule group.solve_equation [OF a_group,
    1.27      folded a_r_coset_def, simplified monoid_record_simps])
    1.28  
    1.29 @@ -535,8 +535,8 @@
    1.30  lemma abelian_group_homI:
    1.31    assumes "abelian_group G"
    1.32    assumes "abelian_group H"
    1.33 -  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
    1.34 -                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
    1.35 +  assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
    1.36 +                                  \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
    1.37    shows "abelian_group_hom G H h"
    1.38  proof -
    1.39    interpret G: abelian_group G by fact
    1.40 @@ -636,7 +636,7 @@
    1.41  theorem (in abelian_group_hom) A_FactGroup_iso:
    1.42    "h ` carrier G = carrier H
    1.43     \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
    1.44 -          (| carrier = carrier H, mult = add H, one = zero H |)"
    1.45 +          \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
    1.46  by (rule group_hom.FactGroup_iso[OF a_group_hom,
    1.47      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
    1.48  
     2.1 --- a/src/HOL/Algebra/Group.thy	Wed Mar 05 20:07:43 2014 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Wed Mar 05 21:51:30 2014 +0100
     2.3 @@ -721,7 +721,7 @@
     2.4  text_raw {* \label{sec:subgroup-lattice} *}
     2.5  
     2.6  theorem (in group) subgroups_partial_order:
     2.7 -  "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
     2.8 +  "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
     2.9    by default simp_all
    2.10  
    2.11  lemma (in group) subgroup_self:
    2.12 @@ -729,7 +729,7 @@
    2.13    by (rule subgroupI) auto
    2.14  
    2.15  lemma (in group) subgroup_imp_group:
    2.16 -  "subgroup H G ==> group (G(| carrier := H |))"
    2.17 +  "subgroup H G ==> group (G\<lparr>carrier := H\<rparr>)"
    2.18    by (erule subgroup.subgroup_is_group) (rule group_axioms)
    2.19  
    2.20  lemma (in group) is_monoid [intro, simp]:
    2.21 @@ -737,7 +737,7 @@
    2.22    by (auto intro: monoid.intro m_assoc) 
    2.23  
    2.24  lemma (in group) subgroup_inv_equality:
    2.25 -  "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
    2.26 +  "[| subgroup H G; x \<in> H |] ==> m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
    2.27  apply (rule_tac inv_equality [THEN sym])
    2.28    apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
    2.29   apply (rule subsetD [OF subgroup.subset], assumption+)
    2.30 @@ -766,7 +766,7 @@
    2.31  qed
    2.32  
    2.33  theorem (in group) subgroups_complete_lattice:
    2.34 -  "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
    2.35 +  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
    2.36      (is "complete_lattice ?L")
    2.37  proof (rule partial_order.complete_lattice_criterion1)
    2.38    show "partial_order ?L" by (rule subgroups_partial_order)
    2.39 @@ -784,7 +784,7 @@
    2.40      fix H
    2.41      assume H: "H \<in> A"
    2.42      with L have subgroupH: "subgroup H G" by auto
    2.43 -    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
    2.44 +    from subgroupH have groupH: "group (G \<lparr>carrier := H\<rparr>)" (is "group ?H")
    2.45        by (rule subgroup_imp_group)
    2.46      from groupH have monoidH: "monoid ?H"
    2.47        by (rule group.is_monoid)
     3.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Mar 05 20:07:43 2014 +0100
     3.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Mar 05 21:51:30 2014 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  
     3.5  abbreviation
     3.6    int_ring :: "int ring" ("\<Z>") where
     3.7 -  "int_ring == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
     3.8 +  "int_ring == \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
     3.9  
    3.10  lemma int_Zcarr [intro!, simp]:
    3.11    "k \<in> carrier \<Z>"
    3.12 @@ -183,27 +183,27 @@
    3.13    by simp_all
    3.14  
    3.15  interpretation int (* FIXME [unfolded UNIV] *) :
    3.16 -  partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    3.17 -  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    3.18 -    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    3.19 -    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    3.20 +  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    3.21 +  where "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
    3.22 +    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
    3.23 +    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
    3.24  proof -
    3.25 -  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    3.26 +  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    3.27      by default simp_all
    3.28 -  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    3.29 +  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
    3.30      by simp
    3.31 -  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    3.32 +  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
    3.33      by simp
    3.34 -  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    3.35 +  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
    3.36      by (simp add: lless_def) auto
    3.37  qed
    3.38  
    3.39  interpretation int (* FIXME [unfolded UNIV] *) :
    3.40 -  lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    3.41 -  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
    3.42 -    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
    3.43 +  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    3.44 +  where "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
    3.45 +    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
    3.46  proof -
    3.47 -  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    3.48 +  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    3.49    show "lattice ?Z"
    3.50      apply unfold_locales
    3.51      apply (simp add: least_def Upper_def)
    3.52 @@ -225,7 +225,7 @@
    3.53  qed
    3.54  
    3.55  interpretation int (* [unfolded UNIV] *) :
    3.56 -  total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    3.57 +  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    3.58    by default clarsimp
    3.59  
    3.60  
     4.1 --- a/src/HOL/Algebra/Lattice.thy	Wed Mar 05 20:07:43 2014 +0100
     4.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Mar 05 21:51:30 2014 +0100
     4.3 @@ -1278,7 +1278,7 @@
     4.4  subsubsection {* The Powerset of a Set is a Complete Lattice *}
     4.5  
     4.6  theorem powerset_is_complete_lattice:
     4.7 -  "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
     4.8 +  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
     4.9    (is "complete_lattice ?L")
    4.10  proof (rule partial_order.complete_latticeI)
    4.11    show "partial_order ?L"
     5.1 --- a/src/HOL/Algebra/Ring.thy	Wed Mar 05 20:07:43 2014 +0100
     5.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Mar 05 21:51:30 2014 +0100
     5.3 @@ -19,7 +19,7 @@
     5.4  
     5.5  definition
     5.6    a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
     5.7 -  where "a_inv R = m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
     5.8 +  where "a_inv R = m_inv \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
     5.9  
    5.10  definition
    5.11    a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
    5.12 @@ -28,11 +28,11 @@
    5.13  locale abelian_monoid =
    5.14    fixes G (structure)
    5.15    assumes a_comm_monoid:
    5.16 -     "comm_monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    5.17 +     "comm_monoid \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.18  
    5.19  definition
    5.20    finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
    5.21 -  "finsum G = finprod (| carrier = carrier G, mult = add G, one = zero G |)"
    5.22 +  "finsum G = finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.23  
    5.24  syntax
    5.25    "_finsum" :: "index => idt => 'a set => 'b => 'b"
    5.26 @@ -50,7 +50,7 @@
    5.27  
    5.28  locale abelian_group = abelian_monoid +
    5.29    assumes a_comm_group:
    5.30 -     "comm_group (| carrier = carrier G, mult = add G, one = zero G |)"
    5.31 +     "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.32  
    5.33  
    5.34  subsection {* Basic Properties *}
    5.35 @@ -87,11 +87,11 @@
    5.36      intro: assms)
    5.37  
    5.38  lemma (in abelian_monoid) a_monoid:
    5.39 -  "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    5.40 +  "monoid \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.41  by (rule comm_monoid.axioms, rule a_comm_monoid) 
    5.42  
    5.43  lemma (in abelian_group) a_group:
    5.44 -  "group (| carrier = carrier G, mult = add G, one = zero G |)"
    5.45 +  "group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.46    by (simp add: group_def a_monoid)
    5.47      (simp add: comm_group.axioms group.axioms a_comm_group)
    5.48  
    5.49 @@ -100,10 +100,10 @@
    5.50  text {* Transfer facts from multiplicative structures via interpretation. *}
    5.51  
    5.52  sublocale abelian_monoid <
    5.53 -  add!: monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
    5.54 -  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
    5.55 -    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
    5.56 -    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
    5.57 +  add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.58 +  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
    5.59 +    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
    5.60 +    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
    5.61    by (rule a_monoid) auto
    5.62  
    5.63  context abelian_monoid begin
    5.64 @@ -118,11 +118,11 @@
    5.65  end
    5.66  
    5.67  sublocale abelian_monoid <
    5.68 -  add!: comm_monoid "(| carrier = carrier G, mult = add G, one = zero G |)"
    5.69 -  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
    5.70 -    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
    5.71 -    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
    5.72 -    and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
    5.73 +  add!: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.74 +  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
    5.75 +    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
    5.76 +    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
    5.77 +    and "finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = finsum G"
    5.78    by (rule a_comm_monoid) (auto simp: finsum_def)
    5.79  
    5.80  context abelian_monoid begin
    5.81 @@ -173,14 +173,15 @@
    5.82  end
    5.83  
    5.84  sublocale abelian_group <
    5.85 -  add!: group "(| carrier = carrier G, mult = add G, one = zero G |)"
    5.86 -  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
    5.87 -    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
    5.88 -    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
    5.89 -    and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
    5.90 +  add!: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    5.91 +  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
    5.92 +    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
    5.93 +    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
    5.94 +    and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
    5.95    by (rule a_group) (auto simp: m_inv_def a_inv_def)
    5.96  
    5.97 -context abelian_group begin
    5.98 +context abelian_group
    5.99 +begin
   5.100  
   5.101  lemmas a_inv_closed = add.inv_closed
   5.102  
   5.103 @@ -200,12 +201,12 @@
   5.104  end
   5.105  
   5.106  sublocale abelian_group <
   5.107 -  add!: comm_group "(| carrier = carrier G, mult = add G, one = zero G |)"
   5.108 -  where "carrier (| carrier = carrier G, mult = add G, one = zero G |) = carrier G"
   5.109 -    and "mult (| carrier = carrier G, mult = add G, one = zero G |) = add G"
   5.110 -    and "one (| carrier = carrier G, mult = add G, one = zero G |) = zero G"
   5.111 -    and "m_inv (| carrier = carrier G, mult = add G, one = zero G |) = a_inv G"
   5.112 -    and "finprod (| carrier = carrier G, mult = add G, one = zero G |) = finsum G"
   5.113 +  add!: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   5.114 +  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
   5.115 +    and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
   5.116 +    and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
   5.117 +    and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
   5.118 +    and "finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = finsum G"
   5.119    by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def)
   5.120  
   5.121  lemmas (in abelian_group) minus_add = add.inv_mult
     6.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 20:07:43 2014 +0100
     6.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 21:51:30 2014 +0100
     6.3 @@ -57,7 +57,7 @@
     6.4    where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
     6.5  
     6.6  definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
     6.7 -  where "UP R = (|
     6.8 +  where "UP R = \<lparr>
     6.9     carrier = up R,
    6.10     mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
    6.11     one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
    6.12 @@ -65,7 +65,7 @@
    6.13     add = (%p:up R. %q:up R. %i. p i \<oplus>\<^bsub>R\<^esub> q i),
    6.14     smult = (%a:carrier R. %p:up R. %i. a \<otimes>\<^bsub>R\<^esub> p i),
    6.15     monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
    6.16 -   coeff = (%p:up R. %n. p n) |)"
    6.17 +   coeff = (%p:up R. %n. p n)\<rparr>"
    6.18  
    6.19  text {*
    6.20    Properties of the set of polynomials @{term up}.
    6.21 @@ -1814,7 +1814,7 @@
    6.22  
    6.23  definition
    6.24    INTEG :: "int ring"
    6.25 -  where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
    6.26 +  where "INTEG = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
    6.27  
    6.28  lemma INTEG_cring: "cring INTEG"
    6.29    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI