author ballarin Thu, 02 Aug 2007 18:13:42 +0200 changeset 24131 1099f6c73649 parent 24130 5ab8044b6d46 child 24132 dc95373bd69f
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
```--- a/src/HOL/Algebra/IntRing.thy	Thu Aug 02 17:31:10 2007 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Thu Aug 02 18:13:42 2007 +0200
@@ -195,16 +195,36 @@
by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)

-interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
-  where "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
+text {* Removal of occurrences of @{term UNIV} in interpretation result
+  --- experimental. *}
+
+lemma UNIV:
+  "x \<in> UNIV = True"
+  "A \<subseteq> UNIV = True"
+  "(ALL x : UNIV. P x) = (ALL x. P x)"
+  "(EX x : UNIV. P x) = (EX x. P x)"
+  "(True --> Q) = Q"
+  "(True ==> PROP R) == PROP R"
+  by simp_all
+
+interpretation int [unfolded UNIV]:
+  partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
+  where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
+    and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
+    and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
proof -
show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
by unfold_locales simp_all
+  show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
+    by simp
+  show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
+    by simp
show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
qed

-interpretation int: lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
+interpretation int [unfolded UNIV]:
+  lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
proof -
@@ -229,67 +249,10 @@
done
qed

-interpretation int: total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
+interpretation int [unfolded UNIV]:
+  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
by unfold_locales clarsimp

-(*
-lemma int_le_total_order:
-  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
-  apply (rule partial_order.total_orderI)
-   apply (rule partial_order.intro, simp+)
-  apply clarsimp
-  done
-
-lemma less_int:
-  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
-  by (auto simp add: expand_fun_eq lless_def)
-
-lemma join_int:
-  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
-  apply (simp add: expand_fun_eq max_def)
-  apply (rule+)
-  apply (rule lattice.joinI)
-  apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: least_def Upper_def)
-  apply arith
-  apply simp apply simp
-  apply (rule lattice.joinI)
-  apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: least_def Upper_def)
-  apply arith
-  apply simp apply simp
-  done
-
-lemma meet_int:
-  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
-  apply (simp add: expand_fun_eq min_def)
-  apply (rule+)
-  apply (rule lattice.meetI)
-  apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: greatest_def Lower_def)
-  apply arith
-  apply simp apply simp
-  apply (rule lattice.meetI)
-  apply (simp add: int_le_total_order total_order.axioms)
-  apply (simp add: greatest_def Lower_def)
-  apply arith
-  apply simp apply simp
-  done
-
-lemma carrier_int:
-  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
-  apply simp
-  done
-
-text {* Interpretation unfolding @{text lless}, @{text join} and @{text
-  meet} since they have natural representations in @{typ int}. *}
-
-interpretation
-  int [unfolded less_int join_int meet_int carrier_int]:
-  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
-  by (rule int_le_total_order)
-*)
-

subsubsection {* Generated Ideals of @{text "\<Z>"} *}
```