src/HOL/Algebra/IntRing.thy
 changeset 24131 1099f6c73649 parent 23957 54fab60ddc97 child 25919 8b1c0d434824
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Aug 02 17:31:10 2007 +0200
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Thu Aug 02 18:13:42 2007 +0200
1.3 @@ -195,16 +195,36 @@
1.4    by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
1.5
1.6
1.7 -interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.8 -  where "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
1.9 +text {* Removal of occurrences of @{term UNIV} in interpretation result
1.10 +  --- experimental. *}
1.11 +
1.12 +lemma UNIV:
1.13 +  "x \<in> UNIV = True"
1.14 +  "A \<subseteq> UNIV = True"
1.15 +  "(ALL x : UNIV. P x) = (ALL x. P x)"
1.16 +  "(EX x : UNIV. P x) = (EX x. P x)"
1.17 +  "(True --> Q) = Q"
1.18 +  "(True ==> PROP R) == PROP R"
1.19 +  by simp_all
1.20 +
1.21 +interpretation int [unfolded UNIV]:
1.22 +  partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.23 +  where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
1.24 +    and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
1.25 +    and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
1.26  proof -
1.27    show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
1.28      by unfold_locales simp_all
1.29 +  show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
1.30 +    by simp
1.31 +  show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
1.32 +    by simp
1.33    show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
1.34      by (simp add: lless_def) auto
1.35  qed
1.36
1.37 -interpretation int: lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.38 +interpretation int [unfolded UNIV]:
1.39 +  lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.40    where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
1.41      and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
1.42  proof -
1.43 @@ -229,67 +249,10 @@
1.44      done
1.45  qed
1.46
1.47 -interpretation int: total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.48 +interpretation int [unfolded UNIV]:
1.49 +  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.50    by unfold_locales clarsimp
1.51
1.52 -(*
1.53 -lemma int_le_total_order:
1.54 -  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
1.55 -  apply (rule partial_order.total_orderI)
1.56 -   apply (rule partial_order.intro, simp+)
1.57 -  apply clarsimp
1.58 -  done
1.59 -
1.60 -lemma less_int:
1.61 -  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
1.62 -  by (auto simp add: expand_fun_eq lless_def)
1.63 -
1.64 -lemma join_int:
1.65 -  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
1.66 -  apply (simp add: expand_fun_eq max_def)
1.67 -  apply (rule+)
1.68 -  apply (rule lattice.joinI)
1.69 -  apply (simp add: int_le_total_order total_order.axioms)
1.70 -  apply (simp add: least_def Upper_def)
1.71 -  apply arith
1.72 -  apply simp apply simp
1.73 -  apply (rule lattice.joinI)
1.74 -  apply (simp add: int_le_total_order total_order.axioms)
1.75 -  apply (simp add: least_def Upper_def)
1.76 -  apply arith
1.77 -  apply simp apply simp
1.78 -  done
1.79 -
1.80 -lemma meet_int:
1.81 -  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
1.82 -  apply (simp add: expand_fun_eq min_def)
1.83 -  apply (rule+)
1.84 -  apply (rule lattice.meetI)
1.85 -  apply (simp add: int_le_total_order total_order.axioms)
1.86 -  apply (simp add: greatest_def Lower_def)
1.87 -  apply arith
1.88 -  apply simp apply simp
1.89 -  apply (rule lattice.meetI)
1.90 -  apply (simp add: int_le_total_order total_order.axioms)
1.91 -  apply (simp add: greatest_def Lower_def)
1.92 -  apply arith
1.93 -  apply simp apply simp
1.94 -  done
1.95 -
1.96 -lemma carrier_int:
1.97 -  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
1.98 -  apply simp
1.99 -  done
1.100 -
1.101 -text {* Interpretation unfolding @{text lless}, @{text join} and @{text
1.102 -  meet} since they have natural representations in @{typ int}. *}
1.103 -
1.104 -interpretation
1.105 -  int [unfolded less_int join_int meet_int carrier_int]:
1.106 -  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
1.107 -  by (rule int_le_total_order)
1.108 -*)
1.109 -
1.110
1.111  subsubsection {* Generated Ideals of @{text "\<Z>"} *}
1.112
```