src/HOL/Algebra/IntRing.thy
changeset 27713 95b36bfe7fc4
parent 25919 8b1c0d434824
child 27717 21bbd410ba04
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Jul 30 16:07:00 2008 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Jul 30 19:03:33 2008 +0200
     1.3 @@ -208,27 +208,27 @@
     1.4    by simp_all
     1.5  
     1.6  interpretation int [unfolded UNIV]:
     1.7 -  partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
     1.8 -  where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
     1.9 -    and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
    1.10 -    and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
    1.11 +  partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    1.12 +  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    1.13 +    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    1.14 +    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    1.15  proof -
    1.16 -  show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
    1.17 +  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.18      by unfold_locales simp_all
    1.19 -  show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
    1.20 +  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    1.21      by simp
    1.22 -  show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
    1.23 +  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    1.24      by simp
    1.25 -  show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
    1.26 +  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    1.27      by (simp add: lless_def) auto
    1.28  qed
    1.29  
    1.30  interpretation int [unfolded UNIV]:
    1.31 -  lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
    1.32 -  where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
    1.33 -    and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
    1.34 +  lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    1.35 +  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
    1.36 +    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
    1.37  proof -
    1.38 -  let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
    1.39 +  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    1.40    show "lattice ?Z"
    1.41      apply unfold_locales
    1.42      apply (simp add: least_def Upper_def)
    1.43 @@ -250,7 +250,7 @@
    1.44  qed
    1.45  
    1.46  interpretation int [unfolded UNIV]:
    1.47 -  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
    1.48 +  total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    1.49    by unfold_locales clarsimp
    1.50  
    1.51