--- a/src/HOL/Real/PReal.thy Thu Jun 07 02:34:37 2007 +0200
+++ b/src/HOL/Real/PReal.thy Thu Jun 07 03:11:31 2007 +0200
@@ -53,7 +53,7 @@
typedef preal = "{A. cut A}"
by (blast intro: cut_of_rat [OF zero_less_one])
-instance preal :: "{ord, plus, minus, times, inverse}" ..
+instance preal :: "{ord, plus, minus, times, inverse, one}" ..
definition
preal_of_rat :: "rat => preal" where
@@ -100,6 +100,9 @@
preal_inverse_def:
"inverse R == Abs_preal (inverse_set (Rep_preal R))"
+ preal_one_def:
+ "1 == preal_of_rat 1"
+
text{*Reduces equality on abstractions to equality on representatives*}
declare Abs_preal_inject [simp]
@@ -334,11 +337,15 @@
apply (force simp add: add_set_def add_ac)
done
+instance preal :: ab_semigroup_add
+proof
+ fix a b c :: preal
+ show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc)
+ show "a + b = b + a" by (rule preal_add_commute)
+qed
+
lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
- apply (rule mk_left_commute [of "op +"])
- apply (rule preal_add_assoc)
- apply (rule preal_add_commute)
- done
+by (rule add_left_commute)
text{* Positive Real addition is an AC operator *}
lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
@@ -465,11 +472,15 @@
apply (force simp add: mult_set_def mult_ac)
done
+instance preal :: ab_semigroup_mult
+proof
+ fix a b c :: preal
+ show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc)
+ show "a * b = b * a" by (rule preal_mult_commute)
+qed
+
lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
- apply (rule mk_left_commute [of "op *"])
- apply (rule preal_mult_assoc)
- apply (rule preal_mult_commute)
- done
+by (rule mult_left_commute)
text{* Positive Real multiplication is an AC operator *}
@@ -479,7 +490,8 @@
text{* Positive real 1 is the multiplicative identity element *}
-lemma preal_mult_1: "(preal_of_rat 1) * z = z"
+lemma preal_mult_1: "(1::preal) * z = z"
+unfolding preal_one_def
proof (induct z)
fix A :: "rat set"
assume A: "A \<in> preal"
@@ -525,11 +537,11 @@
rat_mem_preal A)
qed
+instance preal :: comm_monoid_mult
+by intro_classes (rule preal_mult_1)
-lemma preal_mult_1_right: "z * (preal_of_rat 1) = z"
-apply (rule preal_mult_commute [THEN subst])
-apply (rule preal_mult_1)
-done
+lemma preal_mult_1_right: "z * (1::preal) = z"
+by (rule mult_1_right)
subsection{*Distribution of Multiplication across Addition*}
@@ -596,6 +608,9 @@
lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
by (simp add: preal_mult_commute preal_add_mult_distrib2)
+instance preal :: comm_semiring
+by intro_classes (rule preal_add_mult_distrib)
+
subsection{*Existence of Inverse, a Positive Real*}
@@ -875,12 +890,13 @@
apply (blast intro: inverse_mult_subset_lemma)
done
-lemma preal_mult_inverse: "inverse R * R = (preal_of_rat 1)"
+lemma preal_mult_inverse: "inverse R * R = (1::preal)"
+unfolding preal_one_def
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 = (1::preal)"
apply (rule preal_mult_commute [THEN subst])
apply (rule preal_mult_inverse)
done
@@ -1131,11 +1147,8 @@
instance preal :: ordered_cancel_ab_semigroup_add
proof
fix a b c :: preal
- show "a + b + c = a + (b + c)" by (rule preal_add_assoc)
- show "a + b = b + a" by (rule preal_add_commute)
show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
- show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
- by (simp only: preal_add_le_cancel_left)
+ show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left)
qed
--- a/src/HOL/Real/RealDef.thy Thu Jun 07 02:34:37 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Thu Jun 07 03:11:31 2007 +0200
@@ -37,12 +37,10 @@
defs (overloaded)
real_zero_def:
- "0 == Abs_Real(realrel``{(preal_of_rat 1, preal_of_rat 1)})"
+ "0 == Abs_Real(realrel``{(1, 1)})"
real_one_def:
- "1 == Abs_Real(realrel``
- {(preal_of_rat 1 + preal_of_rat 1,
- preal_of_rat 1)})"
+ "1 == Abs_Real(realrel``{(1 + 1, 1)})"
real_minus_def:
"- r == contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
@@ -61,7 +59,7 @@
{ Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
real_inverse_def:
- "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
+ "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
real_divide_def:
"R / (S::real) == R * inverse S"
@@ -75,21 +73,20 @@
real_abs_def: "abs (r::real) == (if r < 0 then - r else r)"
-
-subsection{*Proving that realrel is an equivalence relation*}
+subsection {* Equivalence relation over positive reals *}
lemma preal_trans_lemma:
assumes "x + y1 = x1 + y"
and "x + y2 = x2 + y"
shows "x1 + y2 = x2 + (y1::preal)"
proof -
- have "(x1 + y2) + x = (x + y2) + x1" by (simp add: preal_add_ac)
+ have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
also have "... = (x2 + y) + x1" by (simp add: prems)
- also have "... = x2 + (x1 + y)" by (simp add: preal_add_ac)
+ also have "... = x2 + (x1 + y)" by (simp add: add_ac)
also have "... = x2 + (x + y1)" by (simp add: prems)
- also have "... = (x2 + y1) + x" by (simp add: preal_add_ac)
+ also have "... = (x2 + y1) + x" by (simp add: add_ac)
finally have "(x1 + y2) + x = (x2 + y1) + x" .
- thus ?thesis by (simp add: preal_add_right_cancel_iff)
+ thus ?thesis by (rule add_right_imp_eq)
qed
@@ -126,15 +123,15 @@
done
-subsection{*Congruence property for addition*}
+subsection {* Addition and Subtraction *}
lemma real_add_congruent2_lemma:
"[|a + ba = aa + b; ab + bc = ac + bb|]
==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))"
-apply (simp add: preal_add_assoc)
-apply (rule preal_add_left_commute [of ab, THEN ssubst])
-apply (simp add: preal_add_assoc [symmetric])
-apply (simp add: preal_add_ac)
+apply (simp add: add_assoc)
+apply (rule add_left_commute [of ab, THEN ssubst])
+apply (simp add: add_assoc [symmetric])
+apply (simp add: add_ac)
done
lemma real_add:
@@ -149,23 +146,6 @@
UN_equiv_class2 [OF equiv_realrel equiv_realrel])
qed
-lemma real_add_commute: "(z::real) + w = w + z"
-by (cases z, cases w, simp add: real_add preal_add_ac)
-
-lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
-by (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc)
-
-lemma real_add_zero_left: "(0::real) + z = z"
-by (cases z, simp add: real_add real_zero_def preal_add_ac)
-
-instance real :: comm_monoid_add
- by (intro_classes,
- (assumption |
- rule real_add_commute real_add_assoc real_add_zero_left)+)
-
-
-subsection{*Additive Inverse on real*}
-
lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
proof -
have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
@@ -174,17 +154,29 @@
by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
qed
-lemma real_add_minus_left: "(-z) + z = (0::real)"
-by (cases z, simp add: real_minus real_add real_zero_def preal_add_commute)
+instance real :: ab_group_add
+proof
+ fix x y z :: real
+ show "(x + y) + z = x + (y + z)"
+ by (cases x, cases y, cases z, simp add: real_add add_assoc)
+ show "x + y = y + x"
+ by (cases x, cases y, simp add: real_add add_commute)
+ show "0 + x = x"
+ by (cases x, simp add: real_add real_zero_def add_ac)
+ show "- x + x = 0"
+ by (cases x, simp add: real_minus real_add real_zero_def add_commute)
+ show "x - y = x + - y"
+ by (simp add: real_diff_def)
+qed
-subsection{*Congruence property for multiplication*}
+subsection {* Multiplication *}
lemma real_mult_congruent2_lemma:
"!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==>
x * x1 + y * y1 + (x * y2 + y * x2) =
x * x2 + y * y2 + (x * y1 + y * x1)"
-apply (simp add: preal_add_left_commute preal_add_assoc [symmetric])
+apply (simp add: add_left_commute add_assoc [symmetric])
apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric])
apply (simp add: preal_add_commute)
done
@@ -228,13 +220,23 @@
text{*one and zero are distinct*}
lemma real_zero_not_eq_one: "0 \<noteq> (1::real)"
proof -
- have "preal_of_rat 1 < preal_of_rat 1 + preal_of_rat 1"
- by (simp add: preal_self_less_add_left)
+ have "(1::preal) < 1 + 1"
+ by (simp add: preal_self_less_add_left)
thus ?thesis
by (simp add: real_zero_def real_one_def preal_add_right_cancel_iff)
qed
-subsection{*existence of inverse*}
+instance real :: comm_ring_1
+proof
+ fix x y z :: real
+ show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
+ show "x * y = y * x" by (rule real_mult_commute)
+ show "1 * x = x" by (rule real_mult_1)
+ show "(x + y) * z = x * z + y * z" by (rule real_add_mult_distrib)
+ show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
+qed
+
+subsection {* Inverse and Division *}
lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0"
by (simp add: real_zero_def preal_add_commute)
@@ -247,12 +249,10 @@
apply (cut_tac x = xa and y = y in linorder_less_linear)
apply (auto dest!: less_add_left_Ex simp add: real_zero_iff)
apply (rule_tac
- x = "Abs_Real (realrel `` { (preal_of_rat 1,
- inverse (D) + preal_of_rat 1)}) "
+ x = "Abs_Real (realrel``{(1, inverse (D) + 1)})"
in exI)
apply (rule_tac [2]
- x = "Abs_Real (realrel `` { (inverse (D) + preal_of_rat 1,
- preal_of_rat 1)})"
+ x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})"
in exI)
apply (auto simp add: real_mult preal_mult_1_right
preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1
@@ -261,8 +261,11 @@
lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
apply (simp add: real_inverse_def)
-apply (frule real_mult_inverse_left_ex, safe)
-apply (rule someI2, auto)
+apply (drule real_mult_inverse_left_ex, safe)
+apply (rule theI, assumption, rename_tac z)
+apply (subgoal_tac "(z * x) * y = z * (x * y)")
+apply (simp add: mult_commute)
+apply (rule mult_assoc)
done
@@ -271,13 +274,6 @@
instance real :: field
proof
fix x y z :: real
- show "- x + x = 0" by (rule real_add_minus_left)
- show "x - y = x + (-y)" by (simp add: real_diff_def)
- show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
- show "x * y = y * x" by (rule real_mult_commute)
- show "1 * x = x" by (rule real_mult_1)
- show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
- show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
show "x / y = x * inverse y" by (simp add: real_divide_def)
qed