src/HOL/Algebra/IntRing.thy
changeset 67396 172a02125bfa
parent 67344 9a0bb8e2be07
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Jan 09 20:15:36 2018 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Jan 10 12:35:03 2018 +0100
     1.3 @@ -172,27 +172,27 @@
     1.4    by simp_all
     1.5  
     1.6  interpretation int (* FIXME [unfolded UNIV] *) :
     1.7 -  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
     1.8 -  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
     1.9 -    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
    1.10 -    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
    1.11 +  partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
    1.12 +  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
    1.13 +    and "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
    1.14 +    and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
    1.15  proof -
    1.16 -  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.17 +  show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
    1.18      by standard simp_all
    1.19 -  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
    1.20 +  show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
    1.21      by simp
    1.22 -  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
    1.23 +  show "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
    1.24      by simp
    1.25 -  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
    1.26 +  show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
    1.27      by (simp add: lless_def) auto
    1.28  qed
    1.29  
    1.30  interpretation int (* FIXME [unfolded UNIV] *) :
    1.31 -  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.32 -  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
    1.33 -    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
    1.34 +  lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
    1.35 +  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = max x y"
    1.36 +    and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = min x y"
    1.37  proof -
    1.38 -  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.39 +  let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
    1.40    show "lattice ?Z"
    1.41      apply unfold_locales
    1.42      apply (simp add: least_def Upper_def)
    1.43 @@ -214,7 +214,7 @@
    1.44  qed
    1.45  
    1.46  interpretation int (* [unfolded UNIV] *) :
    1.47 -  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    1.48 +  total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
    1.49    by standard clarsimp
    1.50  
    1.51