# HG changeset patch # User paulson # Date 1080638292 -7200 # Node ID aba569f1b1e0ef369ba17fab90d8477f94911132 # Parent e2a1c31cf6d33af478db86d08c1bce5fb03dfb01 tidied diff -r e2a1c31cf6d3 -r aba569f1b1e0 src/HOL/Integ/Equiv.thy --- 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) \ r ==> r``{a} = r``{b}" +theorem equiv_class_eq: "equiv A r ==> (a, b) \ 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 \ A \ A" by (unfold equiv_def refl_def) blast -lemma equiv_class_eq_iff: +theorem equiv_class_eq_iff: "equiv A r ==> ((x, y) \ r) = (r``{x} = r``{y} & x \ A & y \ 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 \ A ==> y \ A ==> (r``{x} = r``{y}) = ((x, y) \ 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"; diff -r e2a1c31cf6d3 -r aba569f1b1e0 src/HOL/Integ/IntDef.thy --- 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. \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)) \ intrel) = (x+v = u+y)" +lemma intrel_iff [simp]: "(((x,y),(u,v)) \ intrel) = (x+v = u+y)" by (simp add: intrel_def) 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) \ 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)} \ 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 "\x \ Integ; y \ Integ\ \ (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 @@ by (simp add: zmult_commute [of w] zadd_zmult_distrib) lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)" -apply (simp add: diff_int_def) -apply (subst zadd_zmult_distrib) -apply (simp add: zmult_zminus) -done +by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus) 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. \i j. (i,j) \ Rep_Integ z & a = (of_nat i) - (of_nat j))" + "of_int z == contents (\(i,j) \ 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 (simp add: of_int_def) -apply (rule the_equality, auto) -apply (simp add: compare_rls add_ac of_nat_add [symmetric] - del: of_nat_add) -done +proof - + have "congruent intrel (\(i,j). { of_nat i - (of_nat j :: 'a) })" + by (simp add: congruent_def compare_rls of_nat_add [symmetric] + del: of_nat_add) + 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, + simp add: of_int add minus int_eq_of_nat [symmetric] int_def diff_minus) +qed + subsection{*The Set of Integers*} @@ -886,8 +907,7 @@ lemma negD: "x<0 ==> \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";