src/HOL/Algebra/IntRing.thy
 changeset 22063 717425609192 parent 21896 9a7949815a84 child 23957 54fab60ddc97
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Jan 12 09:58:31 2007 +0100
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Jan 12 15:37:21 2007 +0100
1.3 @@ -96,54 +96,60 @@
1.4  interpretation "domain" ["\<Z>"] by (rule int_is_domain)
1.5
1.6  lemma int_le_total_order:
1.7 -  "total_order (UNIV::int set) (op \<le>)"
1.8 -apply (rule partial_order.total_orderI)
1.9 - apply (rule partial_order.intro, simp+)
1.10 -apply clarsimp
1.11 -done
1.12 +  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
1.13 +  apply (rule partial_order.total_orderI)
1.14 +   apply (rule partial_order.intro, simp+)
1.15 +  apply clarsimp
1.16 +  done
1.17
1.18  lemma less_int:
1.19 -  "order_syntax.less (op \<le>::[int, int] => bool) = (op <)"
1.20 -  by (auto simp add: expand_fun_eq order_syntax.less_def)
1.21 +  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
1.22 +  by (auto simp add: expand_fun_eq lless_def)
1.23
1.24  lemma join_int:
1.25 -  "order_syntax.join (UNIV::int set) (op \<le>) = max"
1.26 +  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
1.27    apply (simp add: expand_fun_eq max_def)
1.28    apply (rule+)
1.29    apply (rule lattice.joinI)
1.30    apply (simp add: int_le_total_order total_order.axioms)
1.31 -  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
1.32 +  apply (simp add: least_def Upper_def)
1.33    apply arith
1.34    apply simp apply simp
1.35    apply (rule lattice.joinI)
1.36    apply (simp add: int_le_total_order total_order.axioms)
1.37 -  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
1.38 +  apply (simp add: least_def Upper_def)
1.39    apply arith
1.40    apply simp apply simp
1.41    done
1.42
1.43  lemma meet_int:
1.44 -  "order_syntax.meet (UNIV::int set) (op \<le>) = min"
1.45 +  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
1.46    apply (simp add: expand_fun_eq min_def)
1.47    apply (rule+)
1.48    apply (rule lattice.meetI)
1.49    apply (simp add: int_le_total_order total_order.axioms)
1.50 -  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
1.51 +  apply (simp add: greatest_def Lower_def)
1.52    apply arith
1.53    apply simp apply simp
1.54    apply (rule lattice.meetI)
1.55    apply (simp add: int_le_total_order total_order.axioms)
1.56 -  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
1.57 +  apply (simp add: greatest_def Lower_def)
1.58    apply arith
1.59    apply simp apply simp
1.60    done
1.61
1.62 -text {* Interpretation unfolding @{text less}, @{text join} and @{text
1.63 +lemma carrier_int:
1.64 +  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
1.65 +  apply simp
1.66 +  done
1.67 +
1.68 +text {* Interpretation unfolding @{text lless}, @{text join} and @{text
1.69    meet} since they have natural representations in @{typ int}. *}
1.70
1.71  interpretation
1.72 -  int [unfolded less_int join_int meet_int]:
1.73 -  total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
1.74 +  int [unfolded less_int join_int meet_int carrier_int]:
1.75 +  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.76 +  by (rule int_le_total_order)
1.77
1.78
1.79  subsubsection {* Generated Ideals of @{text "\<Z>"} *}
```