src/HOL/Algebra/IntRing.thy
 changeset 27713 95b36bfe7fc4 parent 25919 8b1c0d434824 child 27717 21bbd410ba04
equal 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 `