author paulson Tue, 30 Mar 2004 11:18:12 +0200 changeset 14496 aba569f1b1e0 parent 14495 e2a1c31cf6d3 child 14497 76cdbeb0c9de
tidied
 src/HOL/Integ/Equiv.thy file | annotate | diff | comparison | revisions src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integ/Equiv.thy	Tue Mar 30 08:45:39 2004 +0200
+++ b/src/HOL/Integ/Equiv.thy	Tue Mar 30 11:18:12 2004 +0200
@@ -58,7 +58,7 @@
-- {* lemma for the next result *}
by (unfold equiv_def trans_def sym_def) blast

-lemma equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}"
+theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}"
apply (assumption | rule equalityI equiv_class_subset)+
apply (unfold equiv_def sym_def)
apply blast
@@ -83,11 +83,11 @@
lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A"
by (unfold equiv_def refl_def) blast

-lemma equiv_class_eq_iff:
+theorem equiv_class_eq_iff:
"equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)"
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

-lemma eq_equiv_class_iff:
+corollary eq_equiv_class_iff:
"equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

@@ -311,7 +311,6 @@
val equiv_class_eq_iff = thm "equiv_class_eq_iff";
val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
val equiv_class_self = thm "equiv_class_self";
-val equiv_class_subset = thm "equiv_class_subset";
val equiv_comp_eq = thm "equiv_comp_eq";
val equiv_def = thm "equiv_def";
val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";```
```--- a/src/HOL/Integ/IntDef.thy	Tue Mar 30 08:45:39 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue Mar 30 11:18:12 2004 +0200
@@ -12,7 +12,7 @@
constdefs
intrel :: "((nat * nat) * (nat * nat)) set"
--{*the equivalence relation underlying the integers*}
-    "intrel == {p. \<exists>x y u v. p = ((x,y),(u,v)) & x+v = u+y}"
+    "intrel == {((x,y),(u,v)) | x y u v. x+v = u+y}"

typedef (Integ)
int = "UNIV//intrel"
@@ -62,25 +62,34 @@

subsubsection{*Preliminary Lemmas about the Equivalence Relation*}

-lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in>  intrel) = (x+v = u+y)"
+lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"

lemma equiv_intrel: "equiv UNIV intrel"
by (simp add: intrel_def equiv_def refl_def sym_def trans_def)

-lemmas equiv_intrel_iff =
-       eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I, simp]
+text{*Reduces equality of equivalence classes to the @{term intrel} relation:
+  @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
+lemmas equiv_intrel_iff = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]

+declare equiv_intrel_iff [simp]
+
+
+text{*All equivalence classes belong to set of representatives*}
lemma intrel_in_integ [simp]: "intrel``{(x,y)} \<in> Integ"
-by (simp add: Integ_def intrel_def quotient_def, fast)
+by (auto simp add: Integ_def intrel_def quotient_def)

lemma inj_on_Abs_Integ: "inj_on Abs_Integ Integ"
apply (rule inj_on_inverseI)
apply (erule Abs_Integ_inverse)
done

+text{*This theorem reduces equality on abstractions to equality on
+      representatives:
+  @{term "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
declare inj_on_Abs_Integ [THEN inj_on_iff, simp]
-        Abs_Integ_inverse [simp]
+
+declare Abs_Integ_inverse [simp]

text{*Case analysis on the representation of an integer as an equivalence
class of pairs of naturals.*}
@@ -211,10 +220,7 @@

lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"
-done

lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"
by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
@@ -672,21 +678,28 @@
show "int n = of_nat n"  by (induct n, simp_all add: int_Suc add_ac)
qed

+lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
+proof
+  fix n
+  show "of_nat n = id n"  by (induct n, simp_all)
+qed
+

subsection{*Embedding of the Integers into any Ring: @{term of_int}*}

constdefs
of_int :: "int => 'a::ring"
-   "of_int z ==
-      (THE a. \<exists>i j. (i,j) \<in> Rep_Integ z & a = (of_nat i) - (of_nat j))"
+   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ(z). { of_nat i - of_nat j })"

lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
-apply (rule the_equality, auto)
-done
+proof -
+  have "congruent intrel (\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) })"
+  thus ?thesis
+    by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
+qed

lemma of_int_0 [simp]: "of_int 0 = 0"
by (simp add: of_int Zero_int_def int_def)
@@ -738,6 +751,14 @@
declare of_int_eq_iff [of 0, simplified, simp]
declare of_int_eq_iff [of _ 0, simplified, simp]

+lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
+proof
+ fix z
+ show "of_int z = id z"
+  by (cases z,
+qed
+

subsection{*The Set of Integers*}

@@ -886,8 +907,7 @@
lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
apply (cases x)
apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x="y - Suc x" in exI)
-apply arith
+apply (rule_tac x="y - Suc x" in exI, arith)
done

theorem int_cases [cases type: int, case_names nonneg neg]:
@@ -942,11 +962,6 @@
val One_int_def = thm "One_int_def";
val diff_int_def = thm "diff_int_def";

-val intrel_iff = thm "intrel_iff";
-val equiv_intrel = thm "equiv_intrel";
-val equiv_intrel_iff = thm "equiv_intrel_iff";
-val intrel_in_integ = thm "intrel_in_integ";
-val inj_on_Abs_Integ = thm "inj_on_Abs_Integ";
val inj_int = thm "inj_int";
val zminus_zminus = thm "zminus_zminus";
val zminus_0 = thm "zminus_0";```