--- 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";
--- 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";
--- 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 \<in> 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";
--- 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 \<in> 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";
--- 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 \<in> llist (range Leaf) ==> x \<in> LList"
by (unfold LList_def, simp)
--- 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)} \<in> 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 "\<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]
-
-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 \<le> z ==> int (nat z) = z"
-apply simp
-done
+by simp
lemma nat_le_0 [simp]: "z \<le> 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 \<le> z) = (\<exists>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 \<le> c+b) = (\<exists>n. c+b = a+n+d)"
+ proof
+ assume "a + d \<le> c + b"
+ thus "\<exists>n. c + b = a + n + d"
+ by (auto intro!: exI [where x="c+b - (a+d)"])
+ next
+ assume "\<exists>n. c + b = a + n + d"
+ then obtain n where "c + b = a + n + d" ..
+ thus "a + d \<le> c + b" by arith
+ qed
+qed
lemma abs_int_eq [simp]: "abs (int m) = int m"
by (simp add: abs_if)
--- 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";
--- 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 \<noteq> 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 \<noteq> 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: "(\<forall>x. x = (0::nat)) = False"
by auto
--- 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 \<in> preal ==> \<exists>x\<in>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";