src/HOL/Algebra/IntRing.thy
changeset 27713 95b36bfe7fc4
parent 25919 8b1c0d434824
child 27717 21bbd410ba04
equal deleted inserted replaced
27712:007a339b9e7d 27713:95b36bfe7fc4
   206   "(True --> Q) = Q"
   206   "(True --> Q) = Q"
   207   "(True ==> PROP R) == PROP R"
   207   "(True ==> PROP R) == PROP R"
   208   by simp_all
   208   by simp_all
   209 
   209 
   210 interpretation int [unfolded UNIV]:
   210 interpretation int [unfolded UNIV]:
   211   partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   211   partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   212   where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
   212   where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
   213     and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
   213     and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
   214     and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
   214     and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
   215 proof -
   215 proof -
   216   show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
   216   show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   217     by unfold_locales simp_all
   217     by unfold_locales simp_all
   218   show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
   218   show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
   219     by simp
   219     by simp
   220   show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
   220   show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
   221     by simp
   221     by simp
   222   show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
   222   show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
   223     by (simp add: lless_def) auto
   223     by (simp add: lless_def) auto
   224 qed
   224 qed
   225 
   225 
   226 interpretation int [unfolded UNIV]:
   226 interpretation int [unfolded UNIV]:
   227   lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
   227   lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   228   where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
   228   where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
   229     and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
   229     and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
   230 proof -
   230 proof -
   231   let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
   231   let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   232   show "lattice ?Z"
   232   show "lattice ?Z"
   233     apply unfold_locales
   233     apply unfold_locales
   234     apply (simp add: least_def Upper_def)
   234     apply (simp add: least_def Upper_def)
   235     apply arith
   235     apply arith
   236     apply (simp add: greatest_def Lower_def)
   236     apply (simp add: greatest_def Lower_def)
   248     apply arith
   248     apply arith
   249     done
   249     done
   250 qed
   250 qed
   251 
   251 
   252 interpretation int [unfolded UNIV]:
   252 interpretation int [unfolded UNIV]:
   253   total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   253   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   254   by unfold_locales clarsimp
   254   by unfold_locales clarsimp
   255 
   255 
   256 
   256 
   257 subsubsection {* Generated Ideals of @{text "\<Z>"} *}
   257 subsubsection {* Generated Ideals of @{text "\<Z>"} *}
   258 
   258