src/HOL/Algebra/IntRing.thy
changeset 55926 3ef14caf5637
parent 55242 413ec965f95d
child 55991 3fa6e6c81788
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Mar 05 20:07:43 2014 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Mar 05 21:51:30 2014 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  abbreviation
     1.6    int_ring :: "int ring" ("\<Z>") where
     1.7 -  "int_ring == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
     1.8 +  "int_ring == \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
     1.9  
    1.10  lemma int_Zcarr [intro!, simp]:
    1.11    "k \<in> carrier \<Z>"
    1.12 @@ -183,27 +183,27 @@
    1.13    by simp_all
    1.14  
    1.15  interpretation int (* FIXME [unfolded UNIV] *) :
    1.16 -  partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.17 -  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    1.18 -    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    1.19 -    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    1.20 +  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.21 +  where "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
    1.22 +    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
    1.23 +    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
    1.24  proof -
    1.25 -  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.26 +  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.27      by default simp_all
    1.28 -  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    1.29 +  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
    1.30      by simp
    1.31 -  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    1.32 +  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
    1.33      by simp
    1.34 -  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    1.35 +  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
    1.36      by (simp add: lless_def) auto
    1.37  qed
    1.38  
    1.39  interpretation int (* FIXME [unfolded UNIV] *) :
    1.40 -  lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.41 -  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
    1.42 -    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
    1.43 +  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.44 +  where "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
    1.45 +    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
    1.46  proof -
    1.47 -  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.48 +  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.49    show "lattice ?Z"
    1.50      apply unfold_locales
    1.51      apply (simp add: least_def Upper_def)
    1.52 @@ -225,7 +225,7 @@
    1.53  qed
    1.54  
    1.55  interpretation int (* [unfolded UNIV] *) :
    1.56 -  total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.57 +  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.58    by default clarsimp
    1.59  
    1.60