src/HOL/Algebra/IntRing.thy
changeset 21896 9a7949815a84
parent 21041 60e418260b4d
child 22063 717425609192
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Dec 21 13:55:15 2006 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Dec 22 14:03:30 2006 +0100
     1.3 @@ -102,7 +102,48 @@
     1.4  apply clarsimp
     1.5  done
     1.6  
     1.7 -interpretation total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
     1.8 +lemma less_int:
     1.9 +  "order_syntax.less (op \<le>::[int, int] => bool) = (op <)"
    1.10 +  by (auto simp add: expand_fun_eq order_syntax.less_def)
    1.11 +
    1.12 +lemma join_int:
    1.13 +  "order_syntax.join (UNIV::int set) (op \<le>) = max"
    1.14 +  apply (simp add: expand_fun_eq max_def)
    1.15 +  apply (rule+)
    1.16 +  apply (rule lattice.joinI)
    1.17 +  apply (simp add: int_le_total_order total_order.axioms)
    1.18 +  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
    1.19 +  apply arith
    1.20 +  apply simp apply simp
    1.21 +  apply (rule lattice.joinI)
    1.22 +  apply (simp add: int_le_total_order total_order.axioms)
    1.23 +  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
    1.24 +  apply arith
    1.25 +  apply simp apply simp
    1.26 +  done
    1.27 +
    1.28 +lemma meet_int:
    1.29 +  "order_syntax.meet (UNIV::int set) (op \<le>) = min"
    1.30 +  apply (simp add: expand_fun_eq min_def)
    1.31 +  apply (rule+)
    1.32 +  apply (rule lattice.meetI)
    1.33 +  apply (simp add: int_le_total_order total_order.axioms)
    1.34 +  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
    1.35 +  apply arith
    1.36 +  apply simp apply simp
    1.37 +  apply (rule lattice.meetI)
    1.38 +  apply (simp add: int_le_total_order total_order.axioms)
    1.39 +  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
    1.40 +  apply arith
    1.41 +  apply simp apply simp
    1.42 +  done
    1.43 +
    1.44 +text {* Interpretation unfolding @{text less}, @{text join} and @{text
    1.45 +  meet} since they have natural representations in @{typ int}. *}
    1.46 +
    1.47 +interpretation 
    1.48 +  int [unfolded less_int join_int meet_int]:
    1.49 +  total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
    1.50  
    1.51  
    1.52  subsubsection {* Generated Ideals of @{text "\<Z>"} *}