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>"} *}