# HG changeset patch # User paulson # Date 1103128360 -3600 # Node ID 901d1bfedf09bb2c2a84dee118b57dee9fc06121 # Parent 7f373e478a5ad216840678d81a532f03434c9df7 removal of archaic Abs/Rep proofs diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Complex/NSComplex.thy Wed Dec 15 17:32:40 2004 +0100 @@ -152,22 +152,9 @@ lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex" by (simp add: hcomplex_def hcomplexrel_def quotient_def, blast) -lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex" -apply (rule inj_on_inverseI) -apply (erule Abs_hcomplex_inverse) -done - -declare inj_on_Abs_hcomplex [THEN inj_on_iff, simp] - Abs_hcomplex_inverse [simp] - +declare Abs_hcomplex_inject [simp] Abs_hcomplex_inverse [simp] declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp] - -lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)" -apply (rule inj_on_inverseI) -apply (rule Rep_hcomplex_inverse) -done - lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}" by (simp add: hcomplexrel_def) @@ -1552,8 +1539,6 @@ val equiv_hcomplexrel = thm"equiv_hcomplexrel"; val equiv_hcomplexrel_iff = thm"equiv_hcomplexrel_iff"; val hcomplexrel_in_hcomplex = thm"hcomplexrel_in_hcomplex"; -val inj_on_Abs_hcomplex = thm"inj_on_Abs_hcomplex"; -val inj_Rep_hcomplex = thm"inj_Rep_hcomplex"; val lemma_hcomplexrel_refl = thm"lemma_hcomplexrel_refl"; val hcomplex_empty_not_mem = thm"hcomplex_empty_not_mem"; val Rep_hcomplex_nonempty = thm"Rep_hcomplex_nonempty"; diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Datatype_Universe.thy --- a/src/HOL/Datatype_Universe.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Datatype_Universe.thy Wed Dec 15 17:32:40 2004 +0100 @@ -131,19 +131,7 @@ lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P" by (auto simp add: Push_def expand_fun_eq split: nat.split_asm) -(*** Isomorphisms ***) - -lemma inj_Rep_Node: "inj(Rep_Node)" -apply (rule inj_on_inverseI) -apply (rule Rep_Node_inverse) -done - -lemma inj_on_Abs_Node: "inj_on Abs_Node Node" -apply (rule inj_on_inverseI) -apply (erule Abs_Node_inverse) -done - -lemmas Abs_Node_inj = inj_on_Abs_Node [THEN inj_onD, standard] +lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard] (*** Introduction rules for Node ***) @@ -151,8 +139,7 @@ lemma Node_K0_I: "(%k. Inr 0, a) : Node" by (simp add: Node_def) -lemma Node_Push_I: - "p: Node ==> apfst (Push i) p : Node" +lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node" apply (simp add: Node_def Push_def) apply (fast intro!: apfst_conv nat_case_Suc [THEN trans]) done @@ -211,7 +198,7 @@ apply (erule Abs_Node_inj [THEN apfst_convE]) apply (rule Rep_Node [THEN Node_Push_I])+ apply (erule sym [THEN apfst_convE]) -apply (blast intro: inj_Rep_Node [THEN injD] trans sym elim!: Push_inject) +apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject) done @@ -551,8 +538,6 @@ val Push_inject2 = thm "Push_inject2"; val Push_inject = thm "Push_inject"; val Push_neq_K0 = thm "Push_neq_K0"; -val inj_Rep_Node = thm "inj_Rep_Node"; -val inj_on_Abs_Node = thm "inj_on_Abs_Node"; val Abs_Node_inj = thm "Abs_Node_inj"; val Node_K0_I = thm "Node_K0_I"; val Node_Push_I = thm "Node_Push_I"; diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Wed Dec 15 17:32:40 2004 +0100 @@ -255,25 +255,13 @@ lemma hyprel_in_hypreal [simp]: "hyprel``{x}:hypreal" by (simp add: hypreal_def hyprel_def quotient_def, blast) -lemma inj_on_Abs_hypreal: "inj_on Abs_hypreal hypreal" -apply (rule inj_on_inverseI) -apply (erule Abs_hypreal_inverse) -done -declare inj_on_Abs_hypreal [THEN inj_on_iff, simp] - Abs_hypreal_inverse [simp] - +declare Abs_hypreal_inject [simp] Abs_hypreal_inverse [simp] declare equiv_hyprel [THEN eq_equiv_class_iff, simp] - declare hyprel_iff [iff] lemmas eq_hyprelD = eq_equiv_class [OF _ equiv_hyprel] -lemma inj_Rep_hypreal: "inj(Rep_hypreal)" -apply (rule inj_on_inverseI) -apply (rule Rep_hypreal_inverse) -done - lemma lemma_hyprel_refl [simp]: "x \ hyprel `` {x}" by (simp add: hyprel_def) @@ -723,8 +711,6 @@ val hyprel_iff = thm "hyprel_iff"; val hyprel_in_hypreal = thm "hyprel_in_hypreal"; val Abs_hypreal_inverse = thm "Abs_hypreal_inverse"; -val inj_on_Abs_hypreal = thm "inj_on_Abs_hypreal"; -val inj_Rep_hypreal = thm "inj_Rep_hypreal"; val lemma_hyprel_refl = thm "lemma_hyprel_refl"; val hypreal_empty_not_mem = thm "hypreal_empty_not_mem"; val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty"; diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Hyperreal/HyperNat.thy --- a/src/HOL/Hyperreal/HyperNat.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Hyperreal/HyperNat.thy Wed Dec 15 17:32:40 2004 +0100 @@ -86,24 +86,10 @@ lemma hypnatrel_in_hypnat [simp]: "hypnatrel``{x}:hypnat" by (simp add: hypnat_def hypnatrel_def quotient_def, blast) -lemma inj_on_Abs_hypnat: "inj_on Abs_hypnat hypnat" -apply (rule inj_on_inverseI) -apply (erule Abs_hypnat_inverse) -done - -declare inj_on_Abs_hypnat [THEN inj_on_iff, simp] - Abs_hypnat_inverse [simp] - +declare Abs_hypnat_inject [simp] Abs_hypnat_inverse [simp] declare equiv_hypnatrel [THEN eq_equiv_class_iff, simp] - declare hypnatrel_iff [iff] - -lemma inj_Rep_hypnat: "inj(Rep_hypnat)" -apply (rule inj_on_inverseI) -apply (rule Rep_hypnat_inverse) -done - lemma lemma_hypnatrel_refl: "x \ hypnatrel `` {x}" by (simp add: hypnatrel_def) @@ -792,8 +778,6 @@ val hypnatrel_iff = thm "hypnatrel_iff"; val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat"; -val inj_on_Abs_hypnat = thm "inj_on_Abs_hypnat"; -val inj_Rep_hypnat = thm "inj_Rep_hypnat"; val lemma_hypnatrel_refl = thm "lemma_hypnatrel_refl"; val hypnat_empty_not_mem = thm "hypnat_empty_not_mem"; val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty"; diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Induct/LList.thy --- a/src/HOL/Induct/LList.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Induct/LList.thy Wed Dec 15 17:32:40 2004 +0100 @@ -443,12 +443,6 @@ subsection{* Isomorphisms *} -lemma inj_Rep_LList: "inj Rep_LList" -apply (rule inj_on_inverseI) -apply (rule Rep_LList_inverse) -done - - lemma LListI: "x \ llist (range Leaf) ==> x \ LList" by (unfold LList_def, simp) diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Integ/IntDef.thy Wed Dec 15 17:32:40 2004 +0100 @@ -75,25 +75,16 @@ lemma [simp]: "intrel``{(x,y)} \ Integ" 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: +text{*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] - -declare Abs_Integ_inverse [simp] +declare Abs_Integ_inject [simp] Abs_Integ_inverse [simp] text{*Case analysis on the representation of an integer as an equivalence class of pairs of naturals.*} lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P" -apply (rule Rep_Integ [of z, unfolded Integ_def, THEN quotientE]) -apply (drule arg_cong [where f=Abs_Integ]) -apply (auto simp add: Rep_Integ_inverse) +apply (rule Abs_Integ_cases [of z]) +apply (auto simp add: Integ_def quotient_def) done @@ -408,8 +399,7 @@ by (cases z, simp add: nat le int_def Zero_int_def) corollary nat_0_le: "0 \ z ==> int (nat z) = z" -apply simp -done +by simp lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" by (cases z, simp add: nat le int_def Zero_int_def) @@ -496,12 +486,20 @@ by (force simp add: order_eq_iff [of "- int n"] int_zle_neg) lemma zle_iff_zadd: "(w \ z) = (\n. z = w + int n)" -apply (cases w, cases z) -apply (auto simp add: le add int_def) -apply (rename_tac a b c d) -apply (rule_tac x="c+b - (a+d)" in exI) -apply arith -done +proof (cases w, cases z, simp add: le add int_def) + fix a b c d + assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})" + show "(a+d \ c+b) = (\n. c+b = a+n+d)" + proof + assume "a + d \ c + b" + thus "\n. c + b = a + n + d" + by (auto intro!: exI [where x="c+b - (a+d)"]) + next + assume "\n. c + b = a + n + d" + then obtain n where "c + b = a + n + d" .. + thus "a + d \ c + b" by arith + qed +qed lemma abs_int_eq [simp]: "abs (int m) = int m" by (simp add: abs_if) diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Nat.ML Wed Dec 15 17:32:40 2004 +0100 @@ -110,9 +110,7 @@ val gr0I = thm "gr0I"; val gr0_conv_Suc = thm "gr0_conv_Suc"; val gr_implies_not0 = thm "gr_implies_not0"; -val inj_Rep_Nat = thm "inj_Rep_Nat"; val inj_Suc = thm "inj_Suc"; -val inj_on_Abs_Nat = thm "inj_on_Abs_Nat"; val le0 = thm "le0"; val leD = thm "leD"; val leE = thm "leE"; diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Nat.thy Wed Dec 15 17:32:40 2004 +0100 @@ -76,27 +76,11 @@ apply (rules elim: Abs_Nat_inverse [THEN subst]) done - -text {* Isomorphisms: @{text Abs_Nat} and @{text Rep_Nat} *} - -lemma inj_Rep_Nat: "inj Rep_Nat" - apply (rule inj_on_inverseI) - apply (rule Rep_Nat_inverse) - done - -lemma inj_on_Abs_Nat: "inj_on Abs_Nat Nat" - apply (rule inj_on_inverseI) - apply (erule Abs_Nat_inverse) - done - text {* Distinctness of constructors *} lemma Suc_not_Zero [iff]: "Suc m \ 0" - apply (unfold Zero_nat_def Suc_def) - apply (rule inj_on_Abs_Nat [THEN inj_on_contraD]) - apply (rule Suc_Rep_not_Zero_Rep) - apply (rule Rep_Nat Nat.Suc_RepI Nat.Zero_RepI)+ - done + by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI + Suc_Rep_not_Zero_Rep) lemma Zero_not_Suc [iff]: "0 \ Suc m" by (rule not_sym, rule Suc_not_Zero not_sym) @@ -110,22 +94,14 @@ text {* Injectiveness of @{term Suc} *} lemma inj_Suc: "inj_on Suc N" - apply (unfold Suc_def) - apply (rule inj_onI) - apply (drule inj_on_Abs_Nat [THEN inj_onD]) - apply (rule Rep_Nat Nat.Suc_RepI)+ - apply (drule inj_Suc_Rep [THEN injD]) - apply (erule inj_Rep_Nat [THEN injD]) - done + by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI + inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) lemma Suc_inject: "Suc x = Suc y ==> x = y" by (rule inj_Suc [THEN injD]) lemma Suc_Suc_eq [iff]: "(Suc m = Suc n) = (m = n)" - apply (rule iffI) - apply (erule Suc_inject) - apply (erule arg_cong) - done + by (rule inj_Suc [THEN inj_eq]) lemma nat_not_singleton: "(\x. x = (0::nat)) = False" by auto diff -r 7f373e478a5a -r 901d1bfedf09 src/HOL/Real/PReal.thy --- a/src/HOL/Real/PReal.thy Wed Dec 15 10:19:19 2004 +0100 +++ b/src/HOL/Real/PReal.thy Wed Dec 15 17:32:40 2004 +0100 @@ -95,17 +95,8 @@ "inverse R == Abs_preal(inverse_set (Rep_preal R))" -lemma inj_on_Abs_preal: "inj_on Abs_preal preal" -apply (rule inj_on_inverseI) -apply (erule Abs_preal_inverse) -done - -declare inj_on_Abs_preal [THEN inj_on_iff, simp] - -lemma inj_Rep_preal: "inj(Rep_preal)" -apply (rule inj_on_inverseI) -apply (rule Rep_preal_inverse) -done +text{*Reduces equality on abstractions to equality on representatives*} +declare Abs_preal_inject [simp] lemma preal_nonempty: "A \ preal ==> \x\A. 0 < x" by (unfold preal_def cut_def, blast) @@ -601,7 +592,7 @@ done lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)" -apply (rule inj_Rep_preal [THEN injD]) +apply (rule Rep_preal_inject [THEN iffD1]) apply (rule equalityI [OF distrib_subset1 distrib_subset2]) done @@ -887,14 +878,12 @@ apply (blast intro: inverse_mult_subset_lemma) done -lemma preal_mult_inverse: - "inverse R * R = (preal_of_rat 1)" -apply (rule inj_Rep_preal [THEN injD]) +lemma preal_mult_inverse: "inverse R * R = (preal_of_rat 1)" +apply (rule Rep_preal_inject [THEN iffD1]) apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) done -lemma preal_mult_inverse_right: - "R * inverse R = (preal_of_rat 1)" +lemma preal_mult_inverse_right: "R * inverse R = (preal_of_rat 1)" apply (rule preal_mult_commute [THEN subst]) apply (rule preal_mult_inverse) done @@ -1328,8 +1317,6 @@ ML {* -val inj_on_Abs_preal = thm"inj_on_Abs_preal"; -val inj_Rep_preal = thm"inj_Rep_preal"; val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex"; val preal_add_commute = thm"preal_add_commute"; val preal_add_assoc = thm"preal_add_assoc";