heavily revised by Jacques: coercions have alphabetic names;
exponentiation is available, etc.
--- a/src/HOL/Real/PNat.ML Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/PNat.ML Fri Jul 23 17:29:12 1999 +0200
@@ -662,22 +662,23 @@
(** embedding of naturals in positive naturals **)
(* pnat_one_eq! *)
-Goalw [pnat_nat_def,pnat_one_def]"1p = *#0";
+Goalw [pnat_of_nat_def,pnat_one_def]"1p = pnat_of_nat 0";
by (Full_simp_tac 1);
qed "pnat_one_iff";
-Goalw [pnat_nat_def,pnat_one_def,pnat_add_def] "1p + 1p = *#1";
+Goalw [pnat_of_nat_def,pnat_one_def,
+ pnat_add_def] "1p + 1p = pnat_of_nat 1";
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
by (auto_tac (claset() addIs [(gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst)],
simpset()));
qed "pnat_two_eq";
-Goal "inj(pnat_nat)";
+Goal "inj(pnat_of_nat)";
by (rtac injI 1);
-by (rewtac pnat_nat_def);
+by (rewtac pnat_of_nat_def);
by (dtac (inj_on_Abs_pnat RS inj_onD) 1);
by (auto_tac (claset() addSIs [gt_0_mem_pnat],simpset()));
-qed "inj_pnat_nat";
+qed "inj_pnat_of_nat";
Goal "0 < n + 1";
by Auto_tac;
@@ -688,8 +689,9 @@
qed "nat_add_one_less1";
(* this worked with one call to auto_tac before! *)
-Goalw [pnat_add_def,pnat_nat_def,pnat_one_def]
- "*#n1 + *#n2 = *#(n1 + n2) + 1p";
+Goalw [pnat_add_def,pnat_of_nat_def,pnat_one_def]
+ "pnat_of_nat n1 + pnat_of_nat n2 = \
+\ pnat_of_nat (n1 + n2) + 1p";
by (res_inst_tac [("f","Abs_pnat")] arg_cong 1);
by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 1);
by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 2);
@@ -698,12 +700,12 @@
by (auto_tac (claset(),
simpset() addsimps [sum_Rep_pnat_sum,
nat_add_one_less,nat_add_one_less1]));
-qed "pnat_nat_add";
+qed "pnat_of_nat_add";
-Goalw [pnat_nat_def,pnat_less_def] "(n < m) = (*#n < *#m)";
+Goalw [pnat_of_nat_def,pnat_less_def]
+ "(n < m) = (pnat_of_nat n < pnat_of_nat m)";
by (auto_tac (claset(),simpset()
addsimps [Abs_pnat_inverse,Collect_pnat_gt_0]));
-qed "pnat_nat_less_iff";
+qed "pnat_of_nat_less_iff";
+Addsimps [pnat_of_nat_less_iff RS sym];
-Addsimps [pnat_nat_less_iff RS sym];
-
--- a/src/HOL/Real/PNat.thy Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/PNat.thy Fri Jul 23 17:29:12 1999 +0200
@@ -7,10 +7,6 @@
PNat = Arith +
-(** type pnat **)
-
-(* type definition *)
-
typedef
pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def)
@@ -24,14 +20,15 @@
constdefs
- pnat_nat :: nat => pnat ("*# _" [80] 80)
- "*# n == Abs_pnat(n + 1)"
+ pnat_of_nat :: nat => pnat
+ "pnat_of_nat n == Abs_pnat(n + 1)"
defs
- pnat_one_def "1p == Abs_pnat(1)"
- pnat_Suc_def "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
-
+ pnat_one_def
+ "1p == Abs_pnat(1)"
+ pnat_Suc_def
+ "pSuc == (%n. Abs_pnat(Suc(Rep_pnat(n))))"
pnat_add_def
"x + y == Abs_pnat(Rep_pnat(x) + Rep_pnat(y))"
@@ -39,10 +36,10 @@
pnat_mult_def
"x * y == Abs_pnat(Rep_pnat(x) * Rep_pnat(y))"
- pnat_less_def
+ pnat_less_def
"x < (y::pnat) == Rep_pnat(x) < Rep_pnat(y)"
- pnat_le_def
+ pnat_le_def
"x <= (y::pnat) == ~(y < x)"
end
--- a/src/HOL/Real/PRat.ML Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/PRat.ML Fri Jul 23 17:29:12 1999 +0200
@@ -86,10 +86,10 @@
by (rtac Rep_prat_inverse 1);
qed "inj_Rep_prat";
-(** prat_pnat: the injection from pnat to prat **)
-Goal "inj(prat_pnat)";
+(** prat_of_pnat: the injection from pnat to prat **)
+Goal "inj(prat_of_pnat)";
by (rtac injI 1);
-by (rewtac prat_pnat_def);
+by (rewtac prat_of_pnat_def);
by (dtac (inj_on_Abs_prat RS inj_onD) 1);
by (REPEAT (rtac ratrel_in_prat 1));
by (dtac eq_equiv_class 1);
@@ -97,9 +97,8 @@
by (Fast_tac 1);
by Safe_tac;
by (Asm_full_simp_tac 1);
-qed "inj_prat_pnat";
+qed "inj_prat_of_pnat";
-(* lcp's original eq_Abs_Integ *)
val [prem] = goal thy
"(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P";
by (res_inst_tac [("x1","z")]
@@ -139,7 +138,8 @@
by (asm_full_simp_tac (simpset() addsimps [qinv_qinv]) 1);
qed "inj_qinv";
-Goalw [prat_pnat_def] "qinv($# (Abs_pnat 1)) = $#(Abs_pnat 1)";
+Goalw [prat_of_pnat_def]
+ "qinv(prat_of_pnat (Abs_pnat 1)) = prat_of_pnat (Abs_pnat 1)";
by (simp_tac (simpset() addsimps [qinv]) 1);
qed "qinv_1";
@@ -244,49 +244,57 @@
qed "prat_mult_left_commute";
(*Positive Rational multiplication is an AC operator*)
-val prat_mult_ac = [prat_mult_assoc,prat_mult_commute,prat_mult_left_commute];
+val prat_mult_ac = [prat_mult_assoc,
+ prat_mult_commute,prat_mult_left_commute];
-Goalw [prat_pnat_def] "($#Abs_pnat 1) * z = z";
+Goalw [prat_of_pnat_def]
+ "(prat_of_pnat (Abs_pnat 1)) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
-by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [prat_mult] @ pnat_mult_ac) 1);
qed "prat_mult_1";
-Goalw [prat_pnat_def] "z * ($#Abs_pnat 1) = z";
+Goalw [prat_of_pnat_def]
+ "z * (prat_of_pnat (Abs_pnat 1)) = z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
-by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [prat_mult] @ pnat_mult_ac) 1);
qed "prat_mult_1_right";
-Goalw [prat_pnat_def]
- "$#((z1::pnat) + z2) = $#z1 + $#z2";
+Goalw [prat_of_pnat_def]
+ "prat_of_pnat ((z1::pnat) + z2) = \
+\ prat_of_pnat z1 + prat_of_pnat z2";
by (asm_simp_tac (simpset() addsimps [prat_add,
pnat_add_mult_distrib,pnat_mult_1]) 1);
-qed "prat_pnat_add";
+qed "prat_of_pnat_add";
-Goalw [prat_pnat_def]
- "$#((z1::pnat) * z2) = $#z1 * $#z2";
+Goalw [prat_of_pnat_def]
+ "prat_of_pnat ((z1::pnat) * z2) = \
+\ prat_of_pnat z1 * prat_of_pnat z2";
by (asm_simp_tac (simpset() addsimps [prat_mult,
pnat_mult_1]) 1);
-qed "prat_pnat_mult";
+qed "prat_of_pnat_mult";
(*** prat_mult and qinv ***)
-Goalw [prat_def,prat_pnat_def] "qinv (q) * q = $# (Abs_pnat 1)";
+Goalw [prat_def,prat_of_pnat_def]
+ "qinv (q) * q = prat_of_pnat (Abs_pnat 1)";
by (res_inst_tac [("z","q")] eq_Abs_prat 1);
by (asm_full_simp_tac (simpset() addsimps [qinv,
prat_mult,pnat_mult_1,pnat_mult_1_left,
pnat_mult_commute]) 1);
qed "prat_mult_qinv";
-Goal "q * qinv (q) = $# (Abs_pnat 1)";
+Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1)";
by (rtac (prat_mult_commute RS subst) 1);
by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
qed "prat_mult_qinv_right";
-Goal "? y. (x::prat) * y = $# Abs_pnat 1";
+Goal "? y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
qed "prat_qinv_ex";
-Goal "?! y. (x::prat) * y = $# Abs_pnat 1";
+Goal "?! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
@@ -294,7 +302,7 @@
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_ex1";
-Goal "?! y. y * (x::prat) = $# Abs_pnat 1";
+Goal "?! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
@@ -302,7 +310,7 @@
prat_mult_1,prat_mult_1_right]) 1);
qed "prat_qinv_left_ex1";
-Goal "x * y = $# Abs_pnat 1 ==> x = qinv y";
+Goal "x * y = prat_of_pnat (Abs_pnat 1) ==> x = qinv y";
by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
by (Blast_tac 1);
@@ -526,8 +534,9 @@
by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"),
("q2.0","qinv (q2)")] prat_mult_left_less2_mono1 1);
by Auto_tac;
-by (dres_inst_tac [("q2.0","$#Abs_pnat 1")] prat_less_trans 1);
-by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
+by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1)")] prat_less_trans 1);
+by (auto_tac (claset(),simpset() addsimps
+ [prat_less_not_refl]));
qed "lemma2_qinv_prat_less";
Goal
@@ -538,25 +547,31 @@
lemma2_qinv_prat_less],simpset()));
qed "qinv_prat_less";
-Goal "!!(q1::prat). q1 < $#Abs_pnat 1 ==> $#Abs_pnat 1 < qinv(q1)";
+Goal "!!(q1::prat). q1 < prat_of_pnat (Abs_pnat 1) \
+\ ==> prat_of_pnat (Abs_pnat 1) < qinv(q1)";
by (dtac qinv_prat_less 1);
by (full_simp_tac (simpset() addsimps [qinv_1]) 1);
qed "prat_qinv_gt_1";
-Goalw [pnat_one_def] "!!(q1::prat). q1 < $#1p ==> $#1p < qinv(q1)";
+Goalw [pnat_one_def]
+ "!!(q1::prat). q1 < prat_of_pnat 1p \
+\ ==> prat_of_pnat 1p < qinv(q1)";
by (etac prat_qinv_gt_1 1);
qed "prat_qinv_is_gt_1";
-Goalw [prat_less_def] "$#Abs_pnat 1 < $#Abs_pnat 1 + $#Abs_pnat 1";
+Goalw [prat_less_def]
+ "prat_of_pnat (Abs_pnat 1) < prat_of_pnat (Abs_pnat 1) \
+\ + prat_of_pnat (Abs_pnat 1)";
by (Fast_tac 1);
qed "prat_less_1_2";
-Goal "qinv($#Abs_pnat 1 + $#Abs_pnat 1) < $#Abs_pnat 1";
+Goal "qinv(prat_of_pnat (Abs_pnat 1) + \
+\ prat_of_pnat (Abs_pnat 1)) < prat_of_pnat (Abs_pnat 1)";
by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1);
by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1);
qed "prat_less_qinv_2_1";
-Goal "!!(x::prat). x < y ==> x*qinv(y) < $#Abs_pnat 1";
+Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1)";
by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1);
by (Asm_full_simp_tac 1);
qed "prat_mult_qinv_less_1";
@@ -578,7 +593,7 @@
by (simp_tac (simpset() addsimps [prat_self_less_add_right]) 1);
qed "prat_self_less_add_left";
-Goalw [prat_less_def] "$#1p < y ==> (x::prat) < x * y";
+Goalw [prat_less_def] "prat_of_pnat 1p < y ==> (x::prat) < x * y";
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
prat_add_mult_distrib2]));
qed "prat_self_less_mult_right";
@@ -720,7 +735,8 @@
qed "prat_add_left_less_cancel";
(*** lemmas required for lemma_gleason9_34 in PReal : w*y > y/z ***)
-Goalw [prat_pnat_def] "Abs_prat(ratrel^^{(x,y)}) = $#x*qinv($#y)";
+Goalw [prat_of_pnat_def]
+ "Abs_prat(ratrel^^{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)";
by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left,
pnat_mult_1]));
qed "Abs_prat_mult_qinv";
@@ -730,28 +746,29 @@
by (rtac prat_mult_left_le2_mono1 1);
by (rtac qinv_prat_le 1);
by (pnat_ind_tac "y" 1);
-by (dres_inst_tac [("x","$#Abs_pnat 1")] prat_add_le2_mono1 2);
+by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] prat_add_le2_mono1 2);
by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2);
by (auto_tac (claset() addIs [prat_le_trans],
simpset() addsimps [prat_le_refl,
- pSuc_is_plus_one,pnat_one_def,prat_pnat_add]));
+ pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
qed "lemma_Abs_prat_le1";
Goal "Abs_prat(ratrel^^{(x,Abs_pnat 1)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
by (rtac prat_mult_le2_mono1 1);
by (pnat_ind_tac "y" 1);
-by (dres_inst_tac [("x","$#x")] prat_add_le2_mono1 2);
-by (cut_inst_tac [("z","$#x")] (prat_self_less_add_self
+by (dres_inst_tac [("x","prat_of_pnat x")] prat_add_le2_mono1 2);
+by (cut_inst_tac [("z","prat_of_pnat x")] (prat_self_less_add_self
RS prat_less_imp_le) 2);
by (auto_tac (claset() addIs [prat_le_trans],
simpset() addsimps [prat_le_refl,
pSuc_is_plus_one,pnat_one_def,prat_add_mult_distrib2,
- prat_pnat_add,prat_pnat_mult]));
+ prat_of_pnat_add,prat_of_pnat_mult]));
qed "lemma_Abs_prat_le2";
Goal "Abs_prat(ratrel^^{(x,z)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})";
-by (fast_tac (claset() addIs [prat_le_trans,lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
+by (fast_tac (claset() addIs [prat_le_trans,
+ lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
qed "lemma_Abs_prat_le3";
Goal "Abs_prat(ratrel^^{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel^^{(w,x)}) = \
@@ -766,61 +783,62 @@
[pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
qed "pre_lemma_gleason9_34b";
-Goal "($#n < $#m) = (n < m)";
+Goal "(prat_of_pnat n < prat_of_pnat m) = (n < m)";
by (auto_tac (claset(),simpset() addsimps [prat_less_def,
- pnat_less_iff,prat_pnat_add]));
+ pnat_less_iff,prat_of_pnat_add]));
by (res_inst_tac [("z","T")] eq_Abs_prat 1);
by (auto_tac (claset() addDs [pnat_eq_lessI],
simpset() addsimps [prat_add,pnat_mult_1,
- pnat_mult_1_left,prat_pnat_def,pnat_less_iff RS sym]));
-qed "prat_pnat_less_iff";
+ pnat_mult_1_left,prat_of_pnat_def,pnat_less_iff RS sym]));
+qed "prat_of_pnat_less_iff";
-Addsimps [prat_pnat_less_iff];
+Addsimps [prat_of_pnat_less_iff];
-(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)(***)
+(*------------------------------------------------------------------*)
(*** prove witness that will be required to prove non-emptiness ***)
-(*** of preal type as defined using Dedekind Sections in PReal ***)
+(*** of preal type as defined using Dedekind Sections in PReal ***)
(*** Show that exists positive real `one' ***)
-Goal "? q. q: {x::prat. x < $#Abs_pnat 1}";
+Goal "? q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
qed "lemma_prat_less_1_memEx";
-Goal "{x::prat. x < $#Abs_pnat 1} ~= {}";
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {}";
by (rtac notI 1);
by (cut_facts_tac [lemma_prat_less_1_memEx] 1);
by (Asm_full_simp_tac 1);
qed "lemma_prat_less_1_set_non_empty";
-Goalw [psubset_def] "{} < {x::prat. x < $#Abs_pnat 1}";
+Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
by (asm_full_simp_tac (simpset() addsimps
[lemma_prat_less_1_set_non_empty RS not_sym]) 1);
qed "empty_set_psubset_lemma_prat_less_1_set";
-(*** exists rational not in set --- $#Abs_pnat 1 itself ***)
-Goal "? q. q ~: {x::prat. x < $#Abs_pnat 1}";
-by (res_inst_tac [("x","$#Abs_pnat 1")] exI 1);
+(*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
+Goal "? q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
+by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
qed "lemma_prat_less_1_not_memEx";
-Goal "{x::prat. x < $#Abs_pnat 1} ~= {q::prat. True}";
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {q::prat. True}";
by (rtac notI 1);
by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
by (Asm_full_simp_tac 1);
qed "lemma_prat_less_1_set_not_rat_set";
Goalw [psubset_def,subset_def]
- "{x::prat. x < $#Abs_pnat 1} < {q::prat. True}";
+ "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < {q::prat. True}";
by (asm_full_simp_tac (simpset() addsimps
[lemma_prat_less_1_set_not_rat_set,
lemma_prat_less_1_not_memEx]) 1);
qed "lemma_prat_less_1_set_psubset_rat_set";
(*** prove non_emptiness of type ***)
-Goal "{x::prat. x < $#Abs_pnat 1} : {A. {} < A & A < {q::prat. True} & \
-\ (!y: A. ((!z. z < y --> z: A) & \
-\ (? u: A. y < u)))}";
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
+\ A < {q::prat. True} & \
+\ (!y: A. ((!z. z < y --> z: A) & \
+\ (? u: A. y < u)))}";
by (auto_tac (claset() addDs [prat_less_trans],
simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set,
lemma_prat_less_1_set_psubset_rat_set]));
--- a/src/HOL/Real/PRat.thy Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/PRat.thy Fri Jul 23 17:29:12 1999 +0200
@@ -18,11 +18,11 @@
constdefs
- prat_pnat :: pnat => prat ("$#_" [80] 80)
- "$# m == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
+ prat_of_pnat :: pnat => prat
+ "prat_of_pnat m == Abs_prat(ratrel^^{(m,Abs_pnat 1)})"
qinv :: prat => prat
- "qinv(Q) == Abs_prat(UN p:Rep_prat(Q). split (%x y. ratrel^^{(y,x)}) p)"
+ "qinv(Q) == Abs_prat(UN (x,y):Rep_prat(Q). ratrel^^{(y,x)})"
defs
--- a/src/HOL/Real/PReal.ML Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/PReal.ML Fri Jul 23 17:29:12 1999 +0200
@@ -31,7 +31,7 @@
Addsimps [empty_not_mem_preal];
-Goalw [preal_def] "{x::prat. x < $#Abs_pnat 1} : preal";
+Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : preal";
by (rtac preal_1 1);
qed "one_set_mem_preal";
@@ -114,7 +114,7 @@
by (blast_tac (claset() addIs [set_ext] addEs [swap]) 1);
qed "not_mem_Rep_preal_Ex";
-(** prat_pnat: the injection from prat to preal **)
+(** preal_of_prat: the injection from prat to preal **)
(** A few lemmas **)
Goal "{} < {xa::prat. xa < y}";
by (cut_facts_tac [qless_Ex] 1);
@@ -145,14 +145,14 @@
by (auto_tac (claset() addDs [prat_less_not_sym],simpset()));
qed "lemma_prat_set_eq";
-Goal "inj(preal_prat)";
+Goal "inj(preal_of_prat)";
by (rtac injI 1);
-by (rewtac preal_prat_def);
+by (rewtac preal_of_prat_def);
by (dtac (inj_on_Abs_preal RS inj_onD) 1);
by (rtac lemma_prat_less_set_mem_preal 1);
by (rtac lemma_prat_less_set_mem_preal 1);
by (etac lemma_prat_set_eq 1);
-qed "inj_preal_prat";
+qed "inj_preal_of_prat";
(*** theorems for ordering ***)
(* prove introduction and elimination rules for preal_less *)
@@ -249,9 +249,9 @@
\ !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
by Auto_tac;
by (forward_tac [prat_mult_qinv_less_1] 1);
-by (forw_inst_tac [("x","x"),("q2.0","$#Abs_pnat 1")]
+by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")]
prat_mult_less2_mono1 1);
-by (forw_inst_tac [("x","ya"),("q2.0","$#Abs_pnat 1")]
+by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1)")]
prat_mult_less2_mono1 1);
by (Asm_full_simp_tac 1);
by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
@@ -385,7 +385,8 @@
(* Positive Real 1 is the multiplicative identity element *)
(* long *)
-Goalw [preal_prat_def,preal_mult_def] "(@#($#Abs_pnat 1)) * z = z";
+Goalw [preal_of_prat_def,preal_mult_def]
+ "(preal_of_prat (prat_of_pnat (Abs_pnat 1))) * z = z";
by (rtac (Rep_preal_inverse RS subst) 1);
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
@@ -401,7 +402,7 @@
by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
qed "preal_mult_1";
-Goal "z * (@#($#Abs_pnat 1)) = z";
+Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1))) = z";
by (rtac (preal_mult_commute RS subst) 1);
by (rtac preal_mult_1 1);
qed "preal_mult_1_right";
@@ -585,9 +586,10 @@
qed "preal_mem_inv_set";
(*more lemmas for inverse *)
-Goal "x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
+Goal "x: Rep_preal(pinv(A)*A) ==> \
+\ x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
- simpset() addsimps [pinv_def,preal_prat_def] ));
+ simpset() addsimps [pinv_def,preal_of_prat_def] ));
by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
by (auto_tac (claset() addSDs [not_in_preal_ub],simpset()));
by (dtac prat_mult_less_mono 1 THEN Blast_tac 1);
@@ -596,11 +598,12 @@
(*** Gleason's Lemma 9-3.4 p 122 ***)
Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
-\ ? xb : Rep_preal(A). xb + ($#p)*x : Rep_preal(A)";
+\ ? xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
by (cut_facts_tac [mem_Rep_preal_Ex] 1);
by (res_inst_tac [("n","p")] pnat_induct 1);
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
- pSuc_is_plus_one,prat_add_mult_distrib,prat_pnat_add,prat_add_assoc RS sym]));
+ pSuc_is_plus_one,prat_add_mult_distrib,
+ prat_of_pnat_add,prat_add_assoc RS sym]));
qed "lemma1_gleason9_34";
Goal "Abs_prat (ratrel ^^ {(y, z)}) < xb + \
@@ -622,9 +625,9 @@
by (etac bexE 1);
by (cut_inst_tac [("x","y"),("y","xb"),("w","xaa"),
("z","ya"),("xb","xba")] lemma1b_gleason9_34 1);
-by (dres_inst_tac [("x","xba + $#(y * xb) * x")] bspec 1);
+by (dres_inst_tac [("x","xba + prat_of_pnat (y * xb) * x")] bspec 1);
by (auto_tac (claset() addIs [prat_less_asym],
- simpset() addsimps [prat_pnat_def]));
+ simpset() addsimps [prat_of_pnat_def]));
qed "lemma_gleason9_34a";
Goal "? r: Rep_preal(R). r + x ~: Rep_preal(R)";
@@ -648,7 +651,7 @@
(******)
(*** FIXME: long! ***)
-Goal "$#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+Goal "prat_of_pnat 1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
by (Fast_tac 1);
@@ -671,15 +674,17 @@
by Auto_tac;
qed "lemma_gleason9_36";
-Goal "$#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
+\ ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
by (rtac lemma_gleason9_36 1);
by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
qed "lemma_gleason9_36a";
(*** Part 2 of existence of inverse ***)
-Goal "x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
+Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1))) \
+\ ==> x: Rep_preal(pinv(A)*A)";
by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
- simpset() addsimps [pinv_def,preal_prat_def] ));
+ simpset() addsimps [pinv_def,preal_of_prat_def] ));
by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
by (dtac prat_qinv_gt_1 1);
by (dres_inst_tac [("A","A")] lemma_gleason9_36a 1);
@@ -696,13 +701,13 @@
prat_mult_left_commute]));
qed "preal_mem_mult_invI";
-Goal "pinv(A)*A = (@#($#Abs_pnat 1))";
+Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
by (rtac (inj_Rep_preal RS injD) 1);
by (rtac set_ext 1);
by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
qed "preal_mult_inv";
-Goal "A*pinv(A) = (@#($#Abs_pnat 1))";
+Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
by (rtac (preal_mult_commute RS subst) 1);
by (rtac preal_mult_inv 1);
qed "preal_mult_inv_right";
@@ -1240,8 +1245,9 @@
by (etac lemma_preal_rat_less 1);
qed "lemma_preal_rat_less2";
-Goalw [preal_prat_def,preal_add_def]
- "@#((z1::prat) + z2) = @#z1 + @#z2";
+Goalw [preal_of_prat_def,preal_add_def]
+ "preal_of_prat ((z1::prat) + z2) = \
+\ preal_of_prat z1 + preal_of_prat z2";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (auto_tac (claset() addIs [prat_add_less_mono] addSIs [set_ext],simpset() addsimps
[lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
@@ -1251,7 +1257,7 @@
by (etac lemma_preal_rat_less2 1);
by (asm_full_simp_tac (simpset() addsimps [prat_add_mult_distrib RS sym,
prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
-qed "preal_prat_add";
+qed "preal_of_prat_add";
Goal "x < xa ==> x*z1*qinv(xa) < z1";
by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
@@ -1265,8 +1271,9 @@
by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
qed "lemma_preal_rat_less4";
-Goalw [preal_prat_def,preal_mult_def]
- "@#((z1::prat) * z2) = @#z1 * @#z2";
+Goalw [preal_of_prat_def,preal_mult_def]
+ "preal_of_prat ((z1::prat) * z2) = \
+\ preal_of_prat z1 * preal_of_prat z2";
by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
by (auto_tac (claset() addIs [prat_mult_less_mono] addSIs [set_ext],simpset() addsimps
[lemma_prat_less_set_mem_preal RS Abs_preal_inverse]));
@@ -1280,15 +1287,15 @@
addsimps [qinv_mult_eq RS sym] @ prat_mult_ac) 1);
by (asm_full_simp_tac (simpset()
addsimps [prat_mult_assoc RS sym]) 1);
-qed "preal_prat_mult";
+qed "preal_of_prat_mult";
-Goalw [preal_prat_def,preal_less_def]
- "(@#p < @#q) = (p < q)";
+Goalw [preal_of_prat_def,preal_less_def]
+ "(preal_of_prat p < preal_of_prat q) = (p < q)";
by (auto_tac (claset() addSDs [lemma_prat_set_eq] addEs [prat_less_trans],
simpset() addsimps [lemma_prat_less_set_mem_preal,
psubset_def,prat_less_not_refl]));
by (res_inst_tac [("q1.0","p"),("q2.0","q")] prat_linear_less2 1);
by (auto_tac (claset() addIs [prat_less_irrefl],simpset()));
-qed "preal_prat_less_iff";
+qed "preal_of_prat_less_iff";
-Addsimps [preal_prat_less_iff];
+Addsimps [preal_of_prat_less_iff];
--- a/src/HOL/Real/PReal.thy Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/PReal.thy Fri Jul 23 17:29:12 1999 +0200
@@ -15,8 +15,8 @@
preal :: {ord, plus, times}
constdefs
- preal_prat :: prat => preal ("@#_" [80] 80)
- "@# q == Abs_preal({x::prat. x < q})"
+ preal_of_prat :: prat => preal
+ "preal_of_prat q == Abs_preal({x::prat. x < q})"
pinv :: preal => preal
"pinv(R) == Abs_preal({w. ? y. w < y & qinv y ~: Rep_preal(R)})"
--- a/src/HOL/Real/RComplete.ML Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/RComplete.ML Fri Jul 23 17:29:12 1999 +0200
@@ -10,6 +10,75 @@
claset_ref() := claset() delWrapper "bspec";
+(*---------------------------------------------------------
+ Completeness of reals: use supremum property of
+ preal and theorems about real_preal. Theorems
+ previously in Real.ML.
+ ---------------------------------------------------------*)
+ (*a few lemmas*)
+Goal "! x:P. 0r < x ==> \
+\ ((? x:P. y < x) = (? X. real_of_preal X : P & \
+\ y < real_of_preal X))";
+by (blast_tac (claset() addSDs [bspec,
+ real_gt_zero_preal_Ex RS iffD1]) 1);
+qed "real_sup_lemma1";
+
+Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+\ ==> (? X. X: {w. real_of_preal w : P}) & \
+\ (? Y. !X: {w. real_of_preal w : P}. X < Y)";
+by (rtac conjI 1);
+by (blast_tac (claset() addDs [bspec,
+ real_gt_zero_preal_Ex RS iffD1]) 1);
+by Auto_tac;
+by (dtac bspec 1 THEN assume_tac 1);
+by (forward_tac [bspec] 1 THEN assume_tac 1);
+by (dtac real_less_trans 1 THEN assume_tac 1);
+by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1);
+by (res_inst_tac [("x","ya")] exI 1);
+by Auto_tac;
+by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1);
+by (etac real_of_preal_lessD 1);
+qed "real_sup_lemma2";
+
+(*-------------------------------------------------------------
+ Completeness of Positive Reals
+ -------------------------------------------------------------*)
+
+(* Supremum property for the set of positive reals *)
+(* FIXME: long proof - can be improved - need only have
+ one case split *) (* will do for now *)
+Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+\ ==> (? S. !y. (? x: P. y < x) = (y < S))";
+by (res_inst_tac
+ [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
+by Auto_tac;
+by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
+by (case_tac "0r < ya" 1);
+by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
+by (dtac real_less_all_real2 2);
+by Auto_tac;
+by (rtac (preal_complete RS spec RS iffD1) 1);
+by Auto_tac;
+by (forward_tac [real_gt_preal_preal_Ex] 1);
+by Auto_tac;
+(* second part *)
+by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
+by (case_tac "0r < ya" 1);
+by (auto_tac (claset() addSDs [real_less_all_real2,
+ real_gt_zero_preal_Ex RS iffD1],simpset()));
+by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac);
+by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
+by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
+by (Blast_tac 3);
+by (Blast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+qed "posreal_complete";
+
+(*--------------------------------------------------------
+ Completeness properties using isUb, isLub etc.
+ -------------------------------------------------------*)
+
Goal "!!(x::real). [| isLub R S x; isLub R S y |] ==> x = y";
by (forward_tac [isLub_isUb] 1);
by (forw_inst_tac [("x","y")] isLub_isUb 1);
@@ -30,26 +99,26 @@
\ EX x. x: S; \
\ EX u. isUb (UNIV::real set) S u \
\ |] ==> EX t. isLub (UNIV::real set) S t";
-by (res_inst_tac [("x","%#psup({w. %#w : S})")] exI 1);
+by (res_inst_tac [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1);
by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def]));
by (auto_tac (claset() addSIs [setleI,setgeI]
addSDs [real_gt_zero_preal_Ex RS iffD1],simpset()));
by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
-by (auto_tac (claset(), simpset() addsimps [real_preal_le_iff]));
+by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
by (rtac preal_psup_leI2a 1);
-by (forw_inst_tac [("y","%#ya")] setleD 1 THEN assume_tac 1);
+by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1);
by (forward_tac [real_ge_preal_preal_Ex] 1);
by (Step_tac 1);
by (res_inst_tac [("x","y")] exI 1);
-by (blast_tac (claset() addSDs [setleD] addIs [real_preal_le_iff RS iffD1]) 1);
+by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1);
by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
by (forward_tac [isUbD2] 1);
by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
- simpset() addsimps [real_preal_le_iff]));
+ simpset() addsimps [real_of_preal_le_iff]));
by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1]
- addIs [real_preal_le_iff RS iffD1]) 1);
+ addIs [real_of_preal_le_iff RS iffD1]) 1);
qed "posreals_complete";
@@ -142,24 +211,26 @@
qed "reals_complete";
(*----------------------------------------------------------------
- Related property: Archimedean property of reals
+ Related: Archimedean property of reals
----------------------------------------------------------------*)
-Goal "0r < x ==> EX n. rinv(%%#n) < x";
-by (stac real_nat_rinv_Ex_iff 1);
+Goal "0r < x ==> EX n. rinv(real_of_posnat n) < x";
+by (stac real_of_posnat_rinv_Ex_iff 1);
by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
by (fold_tac [real_le_def]);
-by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} 1r" 1);
-by (subgoal_tac "EX X. X : {z. EX n. z = x*%%#n}" 1);
+by (subgoal_tac "isUb (UNIV::real set) \
+\ {z. EX n. z = x*(real_of_posnat n)} 1r" 1);
+by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1);
by (dtac reals_complete 1);
by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
-by (subgoal_tac "ALL m. x*(%%#Suc m) <= t" 1);
+by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1);
by (asm_full_simp_tac (simpset() addsimps
- [real_nat_Suc,real_add_mult_distrib2]) 1);
+ [real_of_posnat_Suc,real_add_mult_distrib2]) 1);
by (blast_tac (claset() addIs [isLubD2]) 2);
by (asm_full_simp_tac
(simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
-by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + -x)" 1);
+by (subgoal_tac "isUb (UNIV::real set) \
+\ {z. EX n. z = x*(real_of_posnat n)} (t + -x)" 1);
by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
by (dres_inst_tac [("y","t+-x")] isLub_le_isUb 1);
by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
@@ -168,20 +239,20 @@
simpset() addsimps [real_less_not_refl,real_add_assoc RS sym]));
qed "reals_Archimedean";
-Goal "EX n. (x::real) < %%#n";
+Goal "EX n. (x::real) < real_of_posnat n";
by (res_inst_tac [("R1.0","x"),("R2.0","0r")] real_linear_less2 1);
by (res_inst_tac [("x","0")] exI 1);
by (res_inst_tac [("x","0")] exI 2);
by (auto_tac (claset() addEs [real_less_trans],
- simpset() addsimps [real_nat_one,real_zero_less_one]));
+ simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1);
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1);
by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
by (dres_inst_tac [("n1","n"),("y","1r")]
- (real_nat_less_zero RS real_mult_less_mono2) 1);
+ (real_of_posnat_less_zero RS real_mult_less_mono2) 1);
by (auto_tac (claset(),
- simpset() addsimps [real_nat_less_zero,
+ simpset() addsimps [real_of_posnat_less_zero,
real_not_refl2 RS not_sym,
real_mult_assoc RS sym]));
qed "reals_Archimedean2";
--- a/src/HOL/Real/Real.ML Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/Real.ML Fri Jul 23 17:29:12 1999 +0200
@@ -1,38 +1,34 @@
-(* Title: HOL/Real/Real.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Type "real" is a linear order
+(* Title: HOL/Real/Real.ML
+ Author: Lawrence C. Paulson
+ Jacques D. Fleuriot
+ Copyright: 1998 University of Cambridge
+ Description: Type "real" is a linear order
*)
-
-
-(** lemma **)
-Goal "(0r < x) = (? y. x = %#y)";
-by (auto_tac (claset(),simpset() addsimps [real_preal_zero_less]));
-by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
+Goal "(0r < x) = (? y. x = real_of_preal y)";
+by (auto_tac (claset(),simpset() addsimps [real_of_preal_zero_less]));
+by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
by (blast_tac (claset() addSEs [real_less_irrefl,
- real_preal_not_minus_gt_zero RS notE]) 1);
+ real_of_preal_not_minus_gt_zero RS notE]) 1);
qed "real_gt_zero_preal_Ex";
-Goal "%#z < x ==> ? y. x = %#y";
-by (blast_tac (claset() addSDs [real_preal_zero_less RS real_less_trans]
+Goal "real_of_preal z < x ==> ? y. x = real_of_preal y";
+by (blast_tac (claset() addSDs [real_of_preal_zero_less RS real_less_trans]
addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
qed "real_gt_preal_preal_Ex";
-Goal "%#z <= x ==> ? y. x = %#y";
+Goal "real_of_preal z <= x ==> ? y. x = real_of_preal y";
by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
real_gt_preal_preal_Ex]) 1);
qed "real_ge_preal_preal_Ex";
-Goal "y <= 0r ==> !x. y < %#x";
+Goal "y <= 0r ==> !x. y < real_of_preal x";
by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
- addIs [real_preal_zero_less RSN(2,real_less_trans)],
- simpset() addsimps [real_preal_zero_less]));
+ addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
+ simpset() addsimps [real_of_preal_zero_less]));
qed "real_less_all_preal";
-Goal "~ 0r < y ==> !x. y < %#x";
+Goal "~ 0r < y ==> !x. y < real_of_preal x";
by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
qed "real_less_all_real2";
@@ -66,7 +62,7 @@
by (blast_tac (claset() addIs [real_less_trans]) 2);
by (auto_tac (claset(),
simpset() addsimps
- [real_gt_zero_preal_Ex,real_preal_minus_less_self]));
+ [real_gt_zero_preal_Ex,real_of_preal_minus_less_self]));
qed "real_gt_zero_iff";
Goal "(x < 0r) = (x < -x)";
@@ -83,17 +79,17 @@
by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym]));
qed "real_le_zero_iff";
-Goal "(%#m1 <= %#m2) = (m1 <= m2)";
+Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)";
by (auto_tac (claset() addSIs [preal_leI],
simpset() addsimps [real_less_le_iff RS sym]));
by (dtac preal_le_less_trans 1 THEN assume_tac 1);
by (etac preal_less_irrefl 1);
-qed "real_preal_le_iff";
+qed "real_of_preal_le_iff";
Goal "!!(x::real). [| 0r < x; 0r < y |] ==> 0r < x * y";
by (auto_tac (claset(),simpset() addsimps [real_gt_zero_preal_Ex]));
by (res_inst_tac [("x","y*ya")] exI 1);
-by (full_simp_tac (simpset() addsimps [real_preal_mult]) 1);
+by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1);
qed "real_mult_order";
Goal "!!(x::real). [| x < 0r; y < 0r |] ==> 0r < x * y";
@@ -108,6 +104,12 @@
simpset()));
qed "real_le_mult_order";
+Goal "!!(x::real). [| 0r < x; 0r <= y |] ==> 0r <= x * y";
+by (dtac real_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [real_mult_order,
+ real_less_imp_le],simpset()));
+qed "real_less_le_mult_order";
+
Goal "!!(x::real). [| x <= 0r; y <= 0r |] ==> 0r <= x * y";
by (rtac real_less_or_eq_imp_le 1);
by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
@@ -135,67 +137,9 @@
Goalw [real_one_def] "0r < 1r";
by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2],
- simpset() addsimps [real_preal_def]));
+ simpset() addsimps [real_of_preal_def]));
qed "real_zero_less_one";
-(*** Completeness of reals ***)
-(** use supremum property of preal and theorems about real_preal **)
- (*** a few lemmas ***)
-Goal "! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
-by (blast_tac (claset() addSDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
-qed "real_sup_lemma1";
-
-Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
-\ ==> (? X. X: {w. %#w : P}) & (? Y. !X: {w. %#w : P}. X < Y)";
-by (rtac conjI 1);
-by (blast_tac (claset() addDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
-by Auto_tac;
-by (dtac bspec 1 THEN assume_tac 1);
-by (forward_tac [bspec] 1 THEN assume_tac 1);
-by (dtac real_less_trans 1 THEN assume_tac 1);
-by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1);
-by (res_inst_tac [("x","ya")] exI 1);
-by Auto_tac;
-by (dres_inst_tac [("x","%#X")] bspec 1 THEN assume_tac 1);
-by (etac real_preal_lessD 1);
-qed "real_sup_lemma2";
-
-(*-------------------------------------------------------------
- Completeness of Positive Reals
- -------------------------------------------------------------*)
-
-(* Supremum property for the set of positive reals *)
-(* FIXME: long proof - can be improved - need only have one case split *)
-(* will do for now *)
-Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
-\ ==> (? S. !y. (? x: P. y < x) = (y < S))";
-by (res_inst_tac [("x","%#psup({w. %#w : P})")] exI 1);
-by Auto_tac;
-by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
-by (case_tac "0r < ya" 1);
-by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
-by (dtac real_less_all_real2 2);
-by Auto_tac;
-by (rtac (preal_complete RS spec RS iffD1) 1);
-by Auto_tac;
-by (forward_tac [real_gt_preal_preal_Ex] 1);
-by Auto_tac;
-(* second part *)
-by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
-by (case_tac "0r < ya" 1);
-by (auto_tac (claset() addSDs [real_less_all_real2,
- real_gt_zero_preal_Ex RS iffD1],simpset()));
-by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac);
-by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
-by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
-by (Blast_tac 3);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed "posreal_complete";
-
-
-
(*** Monotonicity results ***)
Goal "(v+z < w+z) = (v < (w::real))";
@@ -227,8 +171,12 @@
Goal "!!z z'::real. [| w'<w; z'<=z |] ==> w' + z' < w + z";
by (etac (real_add_less_mono1 RS real_less_le_trans) 1);
by (Simp_tac 1);
-qed "real_add_less_mono";
+qed "real_add_less_le_mono";
+Goal "!!z z'::real. [| w'<=w; z'<z |] ==> w' + z' < w + z";
+by (etac (real_add_le_mono1 RS real_le_less_trans) 1);
+by (Simp_tac 1);
+qed "real_add_le_less_mono";
Goal "!!(A::real). A < B ==> C + A < C + B";
by (Simp_tac 1);
@@ -242,6 +190,14 @@
by (Full_simp_tac 1);
qed "real_less_add_left_cancel";
+Goal "!!(A::real). A + C <= B + C ==> A <= B";
+by (Full_simp_tac 1);
+qed "real_le_add_right_cancel";
+
+Goal "!!(A::real). C + A <= C + B ==> A <= B";
+by (Full_simp_tac 1);
+qed "real_le_add_left_cancel";
+
Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
by (etac real_less_trans 1);
by (dtac real_add_less_mono2 1);
@@ -277,80 +233,116 @@
simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
qed "real_less_Ex";
+Goal "!!(u::real). 0r < r ==> u + -r < u";
+by (res_inst_tac [("C","r")] real_less_add_right_cancel 1);
+by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
+qed "real_add_minus_positive_less_self";
+
+Goal "((r::real) <= s) = (-s <= -r)";
+by (Step_tac 1);
+by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1);
+by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2);
+by (Auto_tac);
+by (dres_inst_tac [("z","-r")] real_add_le_mono1 1);
+by (dres_inst_tac [("z","s")] real_add_le_mono1 2);
+by (auto_tac (claset(),simpset() addsimps [real_add_assoc]));
+qed "real_le_minus_iff";
+Addsimps [real_le_minus_iff RS sym];
+
+Goal "0r <= 1r";
+by (rtac (real_zero_less_one RS real_less_imp_le) 1);
+qed "real_zero_le_one";
+Addsimps [real_zero_le_one];
+
+Goal "0r <= x*x";
+by (res_inst_tac [("R2.0","0r"),("R1.0","x")] real_linear_less2 1);
+by (auto_tac (claset() addIs [real_mult_order,
+ real_mult_less_zero1,real_less_imp_le],
+ simpset()));
+qed "real_le_square";
+Addsimps [real_le_square];
+
(*---------------------------------------------------------------------------------
An embedding of the naturals in the reals
---------------------------------------------------------------------------------*)
-Goalw [real_nat_def] "%%#0 = 1r";
-by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_preal_def]) 1);
+Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r";
+by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def]) 1);
by (fold_tac [real_one_def]);
by (rtac refl 1);
-qed "real_nat_one";
+qed "real_of_posnat_one";
-Goalw [real_nat_def] "%%#1 = 1r + 1r";
-by (full_simp_tac (simpset() addsimps [real_preal_def,real_one_def,
- pnat_two_eq,real_add,prat_pnat_add RS sym,preal_prat_add RS sym
+Goalw [real_of_posnat_def] "real_of_posnat 1 = 1r + 1r";
+by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
+ pnat_two_eq,real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym
] @ pnat_add_ac) 1);
-qed "real_nat_two";
+qed "real_of_posnat_two";
-Goalw [real_nat_def]
- "%%#n1 + %%#n2 = %%#(n1 + n2) + 1r";
-by (full_simp_tac (simpset() addsimps [real_nat_one RS sym,
- real_nat_def,real_preal_add RS sym,preal_prat_add RS sym,
- prat_pnat_add RS sym,pnat_nat_add]) 1);
-qed "real_nat_add";
+Goalw [real_of_posnat_def]
+ "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
+by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym,
+ real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym,
+ prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
+qed "real_of_posnat_add";
-Goal "%%#(n + 1) = %%#n + 1r";
+Goal "real_of_posnat (n + 1) = real_of_posnat n + 1r";
by (res_inst_tac [("x1","1r")] (real_add_right_cancel RS iffD1) 1);
-by (rtac (real_nat_add RS subst) 1);
-by (full_simp_tac (simpset() addsimps [real_nat_two,real_add_assoc]) 1);
-qed "real_nat_add_one";
+by (rtac (real_of_posnat_add RS subst) 1);
+by (full_simp_tac (simpset() addsimps [real_of_posnat_two,real_add_assoc]) 1);
+qed "real_of_posnat_add_one";
Goal "Suc n = n + 1";
by Auto_tac;
-qed "lemma";
+qed "lemmaS";
-Goal "%%#Suc n = %%#n + 1r";
-by (stac lemma 1);
-by (rtac real_nat_add_one 1);
-qed "real_nat_Suc";
+Goal "real_of_posnat (Suc n) = real_of_posnat n + 1r";
+by (stac lemmaS 1);
+by (rtac real_of_posnat_add_one 1);
+qed "real_of_posnat_Suc";
-Goal "inj(real_nat)";
+Goal "inj(real_of_posnat)";
by (rtac injI 1);
-by (rewtac real_nat_def);
-by (dtac (inj_real_preal RS injD) 1);
-by (dtac (inj_preal_prat RS injD) 1);
-by (dtac (inj_prat_pnat RS injD) 1);
-by (etac (inj_pnat_nat RS injD) 1);
-qed "inj_real_nat";
+by (rewtac real_of_posnat_def);
+by (dtac (inj_real_of_preal RS injD) 1);
+by (dtac (inj_preal_of_prat RS injD) 1);
+by (dtac (inj_prat_of_pnat RS injD) 1);
+by (etac (inj_pnat_of_nat RS injD) 1);
+qed "inj_real_of_posnat";
-Goalw [real_nat_def] "0r < %%#n";
+Goalw [real_of_posnat_def] "0r < real_of_posnat n";
by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
by (Blast_tac 1);
-qed "real_nat_less_zero";
+qed "real_of_posnat_less_zero";
-Goal "1r <= %%#n";
-by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
+Goal "real_of_posnat n ~= 0r";
+by (rtac (real_of_posnat_less_zero RS real_not_refl2 RS not_sym) 1);
+qed "real_of_posnat_not_eq_zero";
+Addsimps[real_of_posnat_not_eq_zero];
+
+Goal "1r <= real_of_posnat n";
+by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1);
by (induct_tac "n" 1);
by (auto_tac (claset(),
- simpset () addsimps [real_nat_Suc,real_nat_one,
- real_nat_less_zero, real_less_imp_le]));
-qed "real_nat_less_one";
-
-Goal "rinv(%%#n) ~= 0r";
-by (rtac ((real_nat_less_zero RS
- real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
-qed "real_nat_rinv_not_zero";
+ simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
+ real_of_posnat_less_zero, real_less_imp_le]));
+qed "real_of_posnat_less_one";
+Addsimps [real_of_posnat_less_one];
-Goal "rinv(%%#x) = rinv(%%#y) ==> x = y";
-by (rtac (inj_real_nat RS injD) 1);
+Goal "rinv(real_of_posnat n) ~= 0r";
+by (rtac ((real_of_posnat_less_zero RS
+ real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
+qed "real_of_posnat_rinv_not_zero";
+Addsimps [real_of_posnat_rinv_not_zero];
+
+Goal "rinv(real_of_posnat x) = rinv(real_of_posnat y) ==> x = y";
+by (rtac (inj_real_of_posnat RS injD) 1);
by (res_inst_tac [("n2","x")]
- (real_nat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1);
-by (full_simp_tac (simpset() addsimps [(real_nat_less_zero RS
+ (real_of_posnat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1);
+by (full_simp_tac (simpset() addsimps [(real_of_posnat_less_zero RS
real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1);
-by (asm_full_simp_tac (simpset() addsimps [(real_nat_less_zero RS
+by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_less_zero RS
real_not_refl2 RS not_sym)]) 1);
-qed "real_nat_rinv_inj";
+qed "real_of_posnat_rinv_inj";
Goal "0r < x ==> 0r < rinv x";
by (EVERY1[rtac ccontr, dtac real_leI]);
@@ -372,8 +364,14 @@
simpset()));
qed "real_rinv_less_zero";
+Goal "0r < rinv(real_of_posnat n)";
+by (rtac (real_of_posnat_less_zero RS real_rinv_gt_zero) 1);
+qed "real_of_posnat_rinv_gt_zero";
+Addsimps [real_of_posnat_rinv_gt_zero];
+
Goal "x+x=x*(1r+1r)";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
+by (simp_tac (simpset() addsimps
+ [real_add_mult_distrib2]) 1);
qed "real_add_self";
Goal "x < x + 1r";
@@ -454,6 +452,90 @@
by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
qed "real_mult_le_le_mono1";
+Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r < x; x < y|] \
+\ ==> r1 * x < r2 * y";
+by (dres_inst_tac [("x","x")] real_mult_less_mono2 1);
+by (dres_inst_tac [("R1.0","0r")] real_less_trans 2);
+by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
+by (Auto_tac);
+by (blast_tac (claset() addIs [real_less_trans]) 1);
+qed "real_mult_less_mono";
+
+Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r < y|] \
+\ ==> 0r < r2 * y";
+by (dres_inst_tac [("R1.0","0r")] real_less_trans 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [real_mult_order]) 1);
+qed "real_mult_order_trans";
+
+Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r <= x; x < y|] \
+\ ==> r1 * x < r2 * y";
+by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs
+ [real_mult_less_mono,real_mult_order_trans],
+ simpset()));
+qed "real_mult_less_mono3";
+
+Goal "!!(x::real). [| 0r <= r1; r1 <r2; 0r <= x; x < y|] \
+\ ==> r1 * x < r2 * y";
+by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs
+ [real_mult_less_mono,real_mult_order_trans,
+ real_mult_order],simpset()));
+by (dres_inst_tac [("R2.0","x")] real_less_trans 1);
+by (assume_tac 1);
+by (blast_tac (claset() addIs [real_mult_order]) 1);
+qed "real_mult_less_mono4";
+
+Goal "!!(x::real). [| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \
+\ ==> r1 * x <= r2 * y";
+by (rtac real_less_or_eq_imp_le 1);
+by (REPEAT(dtac real_le_imp_less_or_eq 1));
+by (auto_tac (claset() addIs [real_mult_less_mono,
+ real_mult_order_trans,real_mult_order],simpset()));
+qed "real_mult_le_mono";
+
+Goal "!!(x::real). [| 0r < r1; r1 < r2; 0r <= x; x <= y |] \
+\ ==> r1 * x <= r2 * y";
+by (rtac real_less_or_eq_imp_le 1);
+by (REPEAT(dtac real_le_imp_less_or_eq 1));
+by (auto_tac (claset() addIs [real_mult_less_mono,
+ real_mult_order_trans,real_mult_order],simpset()));
+qed "real_mult_le_mono2";
+
+Goal "!!(x::real). [| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \
+\ ==> r1 * x <= r2 * y";
+by (dtac real_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
+by (dtac real_le_trans 1 THEN assume_tac 1);
+by (auto_tac (claset() addIs [real_less_le_mult_order],simpset()));
+qed "real_mult_le_mono3";
+
+Goal "!!(x::real). [| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \
+\ ==> r1 * x <= r2 * y";
+by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [real_mult_le_mono3,
+ real_mult_le_le_mono1],simpset()));
+qed "real_mult_le_mono4";
+
+Goal "!!x. 1r <= x ==> 0r < x";
+by (rtac ccontr 1 THEN dtac real_leI 1);
+by (dtac real_le_trans 1 THEN assume_tac 1);
+by (auto_tac (claset() addDs [real_zero_less_one
+ RSN (2,real_le_less_trans)],simpset() addsimps
+ [real_less_not_refl]));
+qed "real_gt_zero";
+
+Goal "!!r. [| 1r < r; 1r <= x |] ==> x <= r * x";
+by (dtac (real_gt_zero RS real_less_imp_le) 1);
+by (auto_tac (claset() addSDs [real_mult_le_less_mono1],
+ simpset()));
+qed "real_mult_self_le";
+
+Goal "!!r. [| 1r <= r; 1r <= x |] ==> x <= r * x";
+by (dtac real_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [real_mult_self_le],
+ simpset() addsimps [real_le_refl]));
+qed "real_mult_self_le2";
+
Goal "!!(x::real). x < y ==> x < (x + y)*rinv(1r + 1r)";
by (dres_inst_tac [("C","x")] real_add_less_mono2 1);
by (dtac (real_add_self RS subst) 1);
@@ -471,57 +553,276 @@
qed "real_gt_half_sum";
Goal "!!(x::real). x < y ==> EX r. x < r & r < y";
-by (blast_tac (claset() addSIs [real_less_half_sum,real_gt_half_sum]) 1);
+by (blast_tac (claset() addSIs [real_less_half_sum,
+ real_gt_half_sum]) 1);
qed "real_dense";
-Goal "(EX n. rinv(%%#n) < r) = (EX n. 1r < r * %%#n)";
+Goal "(EX n. rinv(real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
by (Step_tac 1);
-by (dres_inst_tac [("n1","n")] (real_nat_less_zero
+by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero
RS real_mult_less_mono1) 1);
-by (dres_inst_tac [("n2","n")] (real_nat_less_zero RS
+by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS
real_rinv_gt_zero RS real_mult_less_mono1) 2);
by (auto_tac (claset(),
- simpset() addsimps [(real_nat_less_zero RS
+ simpset() addsimps [(real_of_posnat_less_zero RS
real_not_refl2 RS not_sym),real_mult_assoc]));
-qed "real_nat_rinv_Ex_iff";
+qed "real_of_posnat_rinv_Ex_iff";
+
+Goal "(rinv(real_of_posnat n) < r) = (1r < r * real_of_posnat n)";
+by (Step_tac 1);
+by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero
+ RS real_mult_less_mono1) 1);
+by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS
+ real_rinv_gt_zero RS real_mult_less_mono1) 2);
+by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]));
+qed "real_of_posnat_rinv_iff";
-Goalw [real_nat_def] "(%%#n < %%#m) = (n < m)";
+Goal "(rinv(real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)";
+by (Step_tac 1);
+by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS
+ real_less_imp_le RS real_mult_le_le_mono1) 1);
+by (dres_inst_tac [("n3","n")] (real_of_posnat_less_zero RS
+ real_rinv_gt_zero RS real_less_imp_le RS
+ real_mult_le_le_mono1) 2);
+by (auto_tac (claset(),simpset() addsimps real_mult_ac));
+qed "real_of_posnat_rinv_le_iff";
+
+Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)";
by Auto_tac;
-qed "real_nat_less_iff";
+qed "real_of_posnat_less_iff";
-Addsimps [real_nat_less_iff];
+Addsimps [real_of_posnat_less_iff];
-Goal "0r < u ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
+Goal "0r < u ==> (u < rinv (real_of_posnat n)) = (real_of_posnat n < rinv(u))";
by (Step_tac 1);
-by (res_inst_tac [("n2","n")] (real_nat_less_zero RS
+by (res_inst_tac [("n2","n")] (real_of_posnat_less_zero RS
real_rinv_gt_zero RS real_mult_less_cancel1) 1);
by (res_inst_tac [("x1","u")] ( real_rinv_gt_zero
RS real_mult_less_cancel1) 2);
by (auto_tac (claset(),
- simpset() addsimps [real_nat_less_zero,
+ simpset() addsimps [real_of_posnat_less_zero,
real_not_refl2 RS not_sym]));
by (res_inst_tac [("z","u")] real_mult_less_cancel2 1);
-by (res_inst_tac [("n1","n")] (real_nat_less_zero RS
+by (res_inst_tac [("n1","n")] (real_of_posnat_less_zero RS
real_mult_less_cancel2) 3);
by (auto_tac (claset(),
- simpset() addsimps [real_nat_less_zero,
+ simpset() addsimps [real_of_posnat_less_zero,
real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
-qed "real_nat_less_rinv_iff";
+qed "real_of_posnat_less_rinv_iff";
-Goal "0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
+Goal "0r < u ==> (u = rinv(real_of_posnat n)) = (real_of_posnat n = rinv u)";
by (auto_tac (claset(),
simpset() addsimps [real_rinv_rinv,
- real_nat_less_zero,real_not_refl2 RS not_sym]));
-qed "real_nat_rinv_eq_iff";
+ real_of_posnat_less_zero,real_not_refl2 RS not_sym]));
+qed "real_of_posnat_rinv_eq_iff";
+
+Goal "!!x. [| 0r < r; r < x |] ==> rinv x < rinv r";
+by (forward_tac [real_less_trans] 1 THEN assume_tac 1);
+by (forward_tac [real_rinv_gt_zero] 1);
+by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1);
+by (forw_inst_tac [("x","r"),("z","rinv r")] real_mult_less_mono1 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS
+ not_sym RS real_mult_inv_right]) 1);
+by (forward_tac [real_rinv_gt_zero] 1);
+by (forw_inst_tac [("x","1r"),("z","rinv x")] real_mult_less_mono2 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS
+ not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
+qed "real_rinv_less_swap";
+
+Goal "!!x. [| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)";
+by (auto_tac (claset() addIs [real_rinv_less_swap],simpset()));
+by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
+by (etac (real_not_refl2 RS not_sym) 1);
+by (res_inst_tac [("t","x")] (real_rinv_rinv RS subst) 1);
+by (etac (real_not_refl2 RS not_sym) 1);
+by (auto_tac (claset() addIs [real_rinv_less_swap],
+ simpset() addsimps [real_rinv_gt_zero]));
+qed "real_rinv_less_iff";
+
+Goal "r < r + rinv(real_of_posnat n)";
+by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
+by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
+qed "real_add_rinv_real_of_posnat_less";
+Addsimps [real_add_rinv_real_of_posnat_less];
+
+Goal "r <= r + rinv(real_of_posnat n)";
+by (rtac real_less_imp_le 1);
+by (Simp_tac 1);
+qed "real_add_rinv_real_of_posnat_le";
+Addsimps [real_add_rinv_real_of_posnat_le];
+
+Goal "r + -rinv(real_of_posnat n) < r";
+by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
+by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
+ real_minus_zero_less_iff2]) 1);
+qed "real_add_minus_rinv_real_of_posnat_less";
+Addsimps [real_add_minus_rinv_real_of_posnat_less];
+
+Goal "r + -rinv(real_of_posnat n) <= r";
+by (rtac real_less_imp_le 1);
+by (Simp_tac 1);
+qed "real_add_minus_rinv_real_of_posnat_le";
+Addsimps [real_add_minus_rinv_real_of_posnat_le];
+
+Goal "!!r. 0r < r ==> r*(1r + -rinv(real_of_posnat n)) < r";
+by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
+by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
+by (auto_tac (claset() addIs [real_mult_order],simpset()
+ addsimps [real_add_assoc RS sym,real_minus_mult_eq2 RS sym,
+ real_minus_zero_less_iff2]));
+qed "real_mult_less_self";
+
+Goal "0r <= 1r + -rinv(real_of_posnat n)";
+by (res_inst_tac [("C","rinv(real_of_posnat n)")] real_le_add_right_cancel 1);
+by (simp_tac (simpset() addsimps [real_add_assoc,
+ real_of_posnat_rinv_le_iff]) 1);
+qed "real_add_one_minus_rinv_ge_zero";
+
+Goal "!!r. 0r < r ==> 0r <= r*(1r + -rinv(real_of_posnat n))";
+by (dtac (real_add_one_minus_rinv_ge_zero RS
+ real_mult_le_less_mono1) 1);
+by (Auto_tac);
+qed "real_mult_add_one_minus_ge_zero";
+
+Goal "!!x. x*y = 0r ==> x = 0r | y = 0r";
+by (auto_tac (claset() addIs [ccontr] addDs
+ [real_mult_not_zero],simpset()));
+qed "real_mult_zero_disj";
+
+Goal "x + x*y = x*(1r + y)";
+by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
+qed "real_add_mult_distrib_one";
+
+Goal "!!x. [| x ~= 1r; y * x = y |] ==> y = 0r";
+by (dtac (sym RS (real_eq_minus_iff RS iffD1)) 1);
+by (dtac sym 1);
+by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2,
+ real_add_mult_distrib_one]) 1);
+by (dtac real_mult_zero_disj 1);
+by (auto_tac (claset(),simpset()
+ addsimps [real_eq_minus_iff2 RS sym]));
+qed "real_mult_eq_self_zero";
+Addsimps [real_mult_eq_self_zero];
+
+Goal "!!x. [| x ~= 1r; y = y * x |] ==> y = 0r";
+by (dtac sym 1);
+by (Asm_full_simp_tac 1);
+qed "real_mult_eq_self_zero2";
+Addsimps [real_mult_eq_self_zero2];
-(*
-(*------------------------------------------------------------------
- lemmas about upper bounds and least upper bound
- ------------------------------------------------------------------*)
-Goalw [real_ub_def] "[| real_ub u S; x : S |] ==> x <= u";
-by Auto_tac;
-qed "real_ubD";
+Goal "!!x. [| 0r <= x*y; 0r < x |] ==> 0r <= y";
+by (forward_tac [real_rinv_gt_zero] 1);
+by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1);
+by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
+by (auto_tac (claset(),simpset() addsimps
+ [real_mult_assoc RS sym]));
+qed "real_mult_ge_zero_cancel";
+
+Goal "!!x. [|x ~= 0r; y ~= 0r |] ==> \
+\ rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
+by (asm_full_simp_tac (simpset() addsimps
+ [real_rinv_distrib,real_add_mult_distrib,
+ real_mult_assoc RS sym]) 1);
+by (rtac (real_mult_assoc RS ssubst) 1);
+by (rtac (real_mult_left_commute RS subst) 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [real_add_commute]) 1);
+qed "real_rinv_add";
+
+(*---------------------------------------------------------------------------------
+ Another embedding of the naturals in the reals (see real_of_posnat)
+ ---------------------------------------------------------------------------------*)
+Goalw [real_of_nat_def] "real_of_nat 0 = 0r";
+by (full_simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
+qed "real_of_nat_zero";
+
+Goalw [real_of_nat_def] "real_of_nat 1 = 1r";
+by (full_simp_tac (simpset() addsimps [real_of_posnat_two,
+ real_add_assoc]) 1);
+qed "real_of_nat_one";
+
+Goalw [real_of_nat_def]
+ "real_of_nat n1 + real_of_nat n2 = real_of_nat (n1 + n2)";
+by (simp_tac (simpset() addsimps
+ [real_of_posnat_add,real_add_assoc RS sym]) 1);
+qed "real_of_nat_add";
+
+Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r";
+by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
+qed "real_of_nat_Suc";
+
+Goalw [real_of_nat_def] "(n < m) = (real_of_nat n < real_of_nat m)";
+by (Auto_tac);
+qed "real_of_nat_less_iff";
+
+Addsimps [real_of_nat_less_iff RS sym];
+
+Goal "inj real_of_nat";
+by (rtac injI 1);
+by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD],
+ simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
+qed "inj_real_of_nat";
-*)
+Goalw [real_of_nat_def] "0r <= real_of_nat n";
+by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [real_add_assoc]) 1);
+qed "real_of_nat_ge_zero";
+Addsimps [real_of_nat_ge_zero];
+
+Goal "real_of_nat n1 * real_of_nat n2 = real_of_nat (n1 * n2)";
+by (induct_tac "n1" 1);
+by (dtac sym 2);
+by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero,
+ real_of_nat_add RS sym,real_of_nat_Suc,real_add_mult_distrib,
+ real_add_commute]));
+qed "real_of_nat_mult";
+
+Goal "(real_of_nat n = real_of_nat m) = (n = m)";
+by (auto_tac (claset() addDs [inj_real_of_nat RS injD],
+ simpset()));
+qed "real_of_nat_eq_cancel";
+
+(*------- lemmas -------*)
+goal NatDef.thy "!!m. [| m < Suc n; n <= m |] ==> m = n";
+by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
+ simpset() addsimps [less_Suc_eq]));
+qed "lemma_nat_not_dense";
+
+goal NatDef.thy "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
+by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
+ simpset() addsimps [le_Suc_eq]));
+qed "lemma_nat_not_dense2";
+
+goal NatDef.thy "!!m. m < Suc n ==> ~ Suc n <= m";
+by (blast_tac (claset() addDs
+ [less_le_trans] addIs [less_asym]) 1);
+qed "lemma_not_leI";
+
+goalw NatDef.thy [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
+by (Auto_tac);
+qed "lemma_not_leI2";
+
+(*------- lemmas -------*)
+val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
+by (rtac (prem RS rev_mp) 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "Suc_diff_n";
+
+(* Goalw [real_of_nat_def]
+ "real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";*)
+
+Goal "n2 < n1 --> real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";
+by (induct_tac "n1" 1);
+by (Step_tac 1 THEN dtac leI 1 THEN dtac sym 2);
+by (dtac lemma_nat_not_dense 1);
+by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
+ real_of_nat_zero] @ real_add_ac));
+by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
+ real_of_nat_add,Suc_diff_n]) 1);
+qed "real_of_nat_minus";
--- a/src/HOL/Real/Real.thy Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/Real.thy Fri Jul 23 17:29:12 1999 +0200
@@ -1,9 +1,8 @@
-(* Title: Real/Real.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Type "real" is a linear order
+(* Title: Real/Real.thy
+ Author: Lawrence C. Paulson
+ Jacques D. Fleuriot
+ Copyright: 1998 University of Cambridge
+ Description: Type "real" is a linear order
*)
Real = RealDef +
--- a/src/HOL/Real/RealAbs.ML Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/RealAbs.ML Fri Jul 23 17:29:12 1999 +0200
@@ -122,6 +122,12 @@
simpset() addsimps [real_ge_zero_iff]));
qed "rabs_minus_cancel";
+Goal "rabs(x + -y) = rabs (y + -x)";
+by (rtac (rabs_minus_cancel RS subst) 1);
+by (simp_tac (simpset() addsimps
+ [real_add_commute]) 1);
+qed "rabs_minus_add_cancel";
+
Goal "rabs(x + -y) <= rabs x + rabs y";
by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1);
by (rtac rabs_triangle_ineq 1);
@@ -134,6 +140,13 @@
by (rtac rabs_triangle_ineq 1);
qed "rabs_sum_triangle_ineq";
+Goal "rabs(x) <= rabs(x + -y) + rabs(y)";
+by (res_inst_tac [("j","rabs(x + -y + y)")] real_le_trans 1);
+by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
+by (simp_tac (simpset() addsimps [real_add_assoc RS sym,
+ rabs_triangle_ineq]) 1);
+qed "rabs_triangle_ineq_minus_cancel";
+
Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s";
by (rtac real_le_less_trans 1);
by (rtac rabs_triangle_ineq 1);
@@ -235,3 +248,67 @@
by (assume_tac 3 THEN Auto_tac);
qed "rabs_interval_iff";
+Goal "(rabs x < r) = (-x < r & x < r)";
+by (auto_tac (claset(),simpset() addsimps [rabs_interval_iff]));
+by (dtac (real_less_swap_iff RS iffD1) 1);
+by (dtac (real_less_swap_iff RS iffD1) 2);
+by (Auto_tac);
+qed "rabs_interval_iff2";
+
+Goal "!!x. rabs x <= r ==> -r<=x & x<=r";
+by (dtac real_le_imp_less_or_eq 1);
+by (auto_tac (claset() addSDs [real_less_imp_le],
+ simpset() addsimps [rabs_interval_iff,rabs_ge_self]));
+by (auto_tac (claset(),simpset() addsimps [real_le_def]));
+by (dtac (real_less_swap_iff RS iffD1) 1);
+by (auto_tac (claset() addSDs [rabs_ge_minus_self
+ RS real_le_less_trans],simpset() addsimps [real_less_not_refl]));
+qed "rabs_leD";
+
+Goal "!!x. [| -r<x; x<=r |] ==> rabs x <= r";
+by (dtac real_le_imp_less_or_eq 1);
+by (Step_tac 1);
+by (blast_tac (claset() addIs
+ [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
+by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps
+ [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl]));
+qed "rabs_leI1";
+
+Goal "!!x. [| -r<=x; x<=r |] ==> rabs x <= r";
+by (REPEAT(dtac real_le_imp_less_or_eq 1));
+by (Step_tac 1);
+by (blast_tac (claset() addIs
+ [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
+by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps
+ [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl,
+ rabs_minus_cancel]));
+by (cut_inst_tac [("x","r")] rabs_disj 1);
+by (rotate_tac 1 1);
+by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
+qed "rabs_leI";
+
+Goal "(rabs x <= r) = (-r<=x & x<=r)";
+by (blast_tac (claset() addSIs [rabs_leD,rabs_leI]) 1);
+qed "rabs_le_interval_iff";
+
+Goal
+ "(rabs (x + -y) < r) = (y + -r < x & x < y + r)";
+by (auto_tac (claset(),simpset() addsimps
+ [rabs_interval_iff]));
+by (ALLGOALS(dtac real_less_sum_gt_zero));
+by (ALLGOALS(dtac real_less_sum_gt_zero));
+by (ALLGOALS(rtac real_sum_gt_zero_less));
+by (auto_tac (claset(),simpset() addsimps
+ [real_minus_add_distrib] addsimps real_add_ac));
+qed "rabs_add_minus_interval_iff";
+
+Goal "!!k. 0r < k ==> 0r < k + rabs(x)";
+by (res_inst_tac [("t","0r")] (real_add_zero_right RS subst) 1);
+by (etac (rabs_ge_zero RSN (2,real_add_less_le_mono)) 1);
+qed "rabs_add_pos_gt_zero";
+
+Goal "0r < 1r + rabs(x)";
+by (rtac (real_zero_less_one RS rabs_add_pos_gt_zero) 1);
+qed "rabs_add_one_gt_zero";
+Addsimps [rabs_add_one_gt_zero];
+
--- a/src/HOL/Real/RealDef.ML Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/RealDef.ML Fri Jul 23 17:29:12 1999 +0200
@@ -80,10 +80,10 @@
by (rtac Rep_real_inverse 1);
qed "inj_Rep_real";
-(** real_preal: the injection from preal to real **)
-Goal "inj(real_preal)";
+(** real_of_preal: the injection from preal to real **)
+Goal "inj(real_of_preal)";
by (rtac injI 1);
-by (rewtac real_preal_def);
+by (rewtac real_of_preal_def);
by (dtac (inj_on_Abs_real RS inj_onD) 1);
by (REPEAT (rtac realrel_in_real 1));
by (dtac eq_equiv_class 1);
@@ -91,7 +91,7 @@
by (Blast_tac 1);
by Safe_tac;
by (Asm_full_simp_tac 1);
-qed "inj_real_preal";
+qed "inj_real_of_preal";
val [prem] = goal thy
"(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
@@ -195,7 +195,7 @@
(* real addition is an AC operator *)
val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute];
-Goalw [real_preal_def,real_zero_def] "0r + z = z";
+Goalw [real_of_preal_def,real_zero_def] "0r + z = z";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
qed "real_add_zero_left";
@@ -253,6 +253,12 @@
by (Blast_tac 1);
qed "real_add_minus_eq_minus";
+Goal "? (y::real). x = -y";
+by (cut_inst_tac [("x","x")] real_minus_ex 1);
+by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
+by (Fast_tac 1);
+qed "real_as_add_inverse_ex";
+
Goal "-(x + y) = -x + -(y::real)";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (res_inst_tac [("z","y")] eq_Abs_real 1);
@@ -271,6 +277,20 @@
by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
qed "real_add_right_cancel";
+Goal "((x::real) = y) = (0r = x + - y)";
+by (Step_tac 1);
+by (res_inst_tac [("x1","-y")]
+ (real_add_right_cancel RS iffD1) 2);
+by (Auto_tac);
+qed "real_eq_minus_iff";
+
+Goal "((x::real) = y) = (x + - y = 0r)";
+by (Step_tac 1);
+by (res_inst_tac [("x1","-y")]
+ (real_add_right_cancel RS iffD1) 2);
+by (Auto_tac);
+qed "real_eq_minus_iff2";
+
Goal "0r - x = -x";
by (simp_tac (simpset() addsimps [real_diff_def]) 1);
qed "real_diff_0";
@@ -458,8 +478,12 @@
by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps [real_zero_iff RS sym]));
-by (res_inst_tac [("x","Abs_real (realrel ^^ {(@#$#1p,pinv(D)+@#$#1p)})")] exI 1);
-by (res_inst_tac [("x","Abs_real (realrel ^^ {(pinv(D)+@#$#1p,@#$#1p)})")] exI 2);
+by (res_inst_tac [("x","Abs_real (realrel ^^ \
+\ {(preal_of_prat(prat_of_pnat 1p),pinv(D)+\
+\ preal_of_prat(prat_of_pnat 1p))})")] exI 1);
+by (res_inst_tac [("x","Abs_real (realrel ^^ \
+\ {(pinv(D)+preal_of_prat(prat_of_pnat 1p),\
+\ preal_of_prat(prat_of_pnat 1p))})")] exI 2);
by (auto_tac (claset(),
simpset() addsimps [real_mult,
pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2,
@@ -496,6 +520,14 @@
by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1);
qed "real_mult_right_cancel";
+Goal "!!a. c*a ~= c*b ==> a ~= b";
+by (Auto_tac);
+qed "real_mult_left_cancel_ccontr";
+
+Goal "!!a. a*c ~= b*c ==> a ~= b";
+by (Auto_tac);
+qed "real_mult_right_cancel_ccontr";
+
Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
by (forward_tac [real_mult_inv_left_ex] 1);
by (etac exE 1);
@@ -507,6 +539,14 @@
Addsimps [real_mult_inv_left,real_mult_inv_right];
+Goal "!!x. [| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
+by (Step_tac 1);
+by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
+qed "real_mult_not_zero";
+
+bind_thm ("real_mult_not_zeroE",real_mult_not_zero RS notE);
+
Goal "x ~= 0r ==> rinv(rinv x) = x";
by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
by (etac rinv_not_zero 1);
@@ -522,16 +562,30 @@
simpset() addsimps
[real_zero_not_eq_one RS not_sym]));
qed "real_rinv_1";
+Addsimps [real_rinv_1];
Goal "x ~= 0r ==> rinv(-x) = -rinv(x)";
by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
by Auto_tac;
qed "real_minus_rinv";
- (*** theorems for ordering ***)
+Goal "!!x y. [| x ~= 0r; y ~= 0r |] \
+\ ==> rinv(x*y) = rinv(x)*rinv(y)";
+by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
+by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
+by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
+by (res_inst_tac [("c1","y")] (real_mult_left_cancel RS iffD1) 1);
+by (auto_tac (claset(),simpset() addsimps [real_mult_left_commute]));
+by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
+qed "real_rinv_distrib";
+
+(*---------------------------------------------------------
+ Theorems for ordering
+ --------------------------------------------------------*)
(* prove introduction and elimination rules for real_less *)
-(* real_less is a strong order i.e nonreflexive and transitive *)
+(* real_less is a strong order i.e. nonreflexive and transitive *)
+
(*** lemmas ***)
Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y";
by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1);
@@ -599,195 +653,209 @@
(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
(****** Map and more real_less ******)
(*** mapping from preal into real ***)
-Goalw [real_preal_def]
- "%#((z1::preal) + z2) = %#z1 + %#z2";
+Goalw [real_of_preal_def]
+ "real_of_preal ((z1::preal) + z2) = \
+\ real_of_preal z1 + real_of_preal z2";
by (asm_simp_tac (simpset() addsimps [real_add,
preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1);
-qed "real_preal_add";
+qed "real_of_preal_add";
-Goalw [real_preal_def]
- "%#((z1::preal) * z2) = %#z1* %#z2";
+Goalw [real_of_preal_def]
+ "real_of_preal ((z1::preal) * z2) = \
+\ real_of_preal z1* real_of_preal z2";
by (full_simp_tac (simpset() addsimps [real_mult,
preal_add_mult_distrib2,preal_mult_1,
preal_mult_1_right,pnat_one_def]
@ preal_add_ac @ preal_mult_ac) 1);
-qed "real_preal_mult";
+qed "real_of_preal_mult";
-Goalw [real_preal_def]
- "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m";
+Goalw [real_of_preal_def]
+ "!!(x::preal). y < x ==> \
+\ ? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps preal_add_ac));
-qed "real_preal_ExI";
+qed "real_of_preal_ExI";
-Goalw [real_preal_def]
- "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#m ==> y < x";
+Goalw [real_of_preal_def]
+ "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = \
+\ real_of_preal m ==> y < x";
by (auto_tac (claset(),
simpset() addsimps
[preal_add_commute,preal_add_assoc]));
by (asm_full_simp_tac (simpset() addsimps
[preal_add_assoc RS sym,preal_self_less_add_left]) 1);
-qed "real_preal_ExD";
+qed "real_of_preal_ExD";
-Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)";
-by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1);
-qed "real_preal_iff";
+Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)";
+by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
+qed "real_of_preal_iff";
(*** Gleason prop 9-4.4 p 127 ***)
-Goalw [real_preal_def,real_zero_def]
- "? m. (x::real) = %#m | x = 0r | x = -(%#m)";
+Goalw [real_of_preal_def,real_zero_def]
+ "? m. (x::real) = real_of_preal m | x = 0r | x = -(real_of_preal m)";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps [preal_add_assoc RS sym]));
by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
-qed "real_preal_trichotomy";
+qed "real_of_preal_trichotomy";
-Goal "!!P. [| !!m. x = %#m ==> P; \
+Goal "!!P. [| !!m. x = real_of_preal m ==> P; \
\ x = 0r ==> P; \
-\ !!m. x = -(%#m) ==> P |] ==> P";
-by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
+\ !!m. x = -(real_of_preal m) ==> P |] ==> P";
+by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
by Auto_tac;
-qed "real_preal_trichotomyE";
+qed "real_of_preal_trichotomyE";
-Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
+Goalw [real_of_preal_def]
+ "real_of_preal m1 < real_of_preal m2 ==> m1 < m2";
by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-qed "real_preal_lessD";
+qed "real_of_preal_lessD";
-Goal "m1 < m2 ==> %#m1 < %#m2";
+Goal "m1 < m2 ==> real_of_preal m1 < real_of_preal m2";
by (dtac preal_less_add_left_Ex 1);
by (auto_tac (claset(),
- simpset() addsimps [real_preal_add,
- real_preal_def,real_less_def]));
+ simpset() addsimps [real_of_preal_add,
+ real_of_preal_def,real_less_def]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (simp_tac (simpset() addsimps [preal_self_less_add_left]
delsimps [preal_add_less_iff2]) 1);
-qed "real_preal_lessI";
+qed "real_of_preal_lessI";
-Goal "(%#m1 < %#m2) = (m1 < m2)";
-by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1);
-qed "real_preal_less_iff1";
+Goal "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)";
+by (blast_tac (claset() addIs [real_of_preal_lessI,real_of_preal_lessD]) 1);
+qed "real_of_preal_less_iff1";
-Addsimps [real_preal_less_iff1];
+Addsimps [real_of_preal_less_iff1];
-Goal "- %#m < %#m";
+Goal "- real_of_preal m < real_of_preal m";
by (auto_tac (claset(),
simpset() addsimps
- [real_preal_def,real_less_def,real_minus]));
+ [real_of_preal_def,real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
preal_add_assoc RS sym]) 1);
-qed "real_preal_minus_less_self";
+qed "real_of_preal_minus_less_self";
-Goalw [real_zero_def] "- %#m < 0r";
+Goalw [real_zero_def] "- real_of_preal m < 0r";
by (auto_tac (claset(),
- simpset() addsimps [real_preal_def,real_less_def,real_minus]));
+ simpset() addsimps [real_of_preal_def,
+ real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (full_simp_tac (simpset() addsimps
[preal_self_less_add_right] @ preal_add_ac) 1);
-qed "real_preal_minus_less_zero";
+qed "real_of_preal_minus_less_zero";
-Goal "~ 0r < - %#m";
-by (cut_facts_tac [real_preal_minus_less_zero] 1);
+Goal "~ 0r < - real_of_preal m";
+by (cut_facts_tac [real_of_preal_minus_less_zero] 1);
by (fast_tac (claset() addDs [real_less_trans]
addEs [real_less_irrefl]) 1);
-qed "real_preal_not_minus_gt_zero";
+qed "real_of_preal_not_minus_gt_zero";
-Goalw [real_zero_def] "0r < %#m";
-by (auto_tac (claset(),
- simpset() addsimps [real_preal_def,real_less_def,real_minus]));
+Goalw [real_zero_def] "0r < real_of_preal m";
+by (auto_tac (claset(),simpset() addsimps
+ [real_of_preal_def,real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (full_simp_tac (simpset() addsimps
[preal_self_less_add_right] @ preal_add_ac) 1);
-qed "real_preal_zero_less";
+qed "real_of_preal_zero_less";
-Goal "~ %#m < 0r";
-by (cut_facts_tac [real_preal_zero_less] 1);
+Goal "~ real_of_preal m < 0r";
+by (cut_facts_tac [real_of_preal_zero_less] 1);
by (blast_tac (claset() addDs [real_less_trans]
addEs [real_less_irrefl]) 1);
-qed "real_preal_not_less_zero";
+qed "real_of_preal_not_less_zero";
-Goal "0r < - - %#m";
+Goal "0r < - - real_of_preal m";
by (simp_tac (simpset() addsimps
- [real_preal_zero_less]) 1);
+ [real_of_preal_zero_less]) 1);
qed "real_minus_minus_zero_less";
(* another lemma *)
-Goalw [real_zero_def] "0r < %#m + %#m1";
+Goalw [real_zero_def]
+ "0r < real_of_preal m + real_of_preal m1";
by (auto_tac (claset(),
- simpset() addsimps [real_preal_def,real_less_def,real_add]));
+ simpset() addsimps [real_of_preal_def,
+ real_less_def,real_add]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
preal_add_assoc RS sym]) 1);
-qed "real_preal_sum_zero_less";
+qed "real_of_preal_sum_zero_less";
-Goal "- %#m < %#m1";
+Goal "- real_of_preal m < real_of_preal m1";
by (auto_tac (claset(),
- simpset() addsimps [real_preal_def,real_less_def,real_minus]));
+ simpset() addsimps [real_of_preal_def,
+ real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
preal_add_assoc RS sym]) 1);
-qed "real_preal_minus_less_all";
+qed "real_of_preal_minus_less_all";
-Goal "~ %#m < - %#m1";
-by (cut_facts_tac [real_preal_minus_less_all] 1);
+Goal "~ real_of_preal m < - real_of_preal m1";
+by (cut_facts_tac [real_of_preal_minus_less_all] 1);
by (blast_tac (claset() addDs [real_less_trans]
addEs [real_less_irrefl]) 1);
-qed "real_preal_not_minus_gt_all";
+qed "real_of_preal_not_minus_gt_all";
-Goal "- %#m1 < - %#m2 ==> %#m2 < %#m1";
+Goal "- real_of_preal m1 < - real_of_preal m2 \
+\ ==> real_of_preal m2 < real_of_preal m1";
by (auto_tac (claset(),
- simpset() addsimps [real_preal_def,real_less_def,real_minus]));
+ simpset() addsimps [real_of_preal_def,
+ real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (auto_tac (claset(),simpset() addsimps preal_add_ac));
by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-qed "real_preal_minus_less_rev1";
+qed "real_of_preal_minus_less_rev1";
-Goal "%#m1 < %#m2 ==> - %#m2 < - %#m1";
+Goal "real_of_preal m1 < real_of_preal m2 \
+\ ==> - real_of_preal m2 < - real_of_preal m1";
by (auto_tac (claset(),
- simpset() addsimps [real_preal_def,real_less_def,real_minus]));
+ simpset() addsimps [real_of_preal_def,
+ real_less_def,real_minus]));
by (REPEAT(rtac exI 1));
by (EVERY[rtac conjI 1, rtac conjI 2]);
by (REPEAT(Blast_tac 2));
by (auto_tac (claset(),simpset() addsimps preal_add_ac));
by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
by (auto_tac (claset(),simpset() addsimps preal_add_ac));
-qed "real_preal_minus_less_rev2";
+qed "real_of_preal_minus_less_rev2";
-Goal "(- %#m1 < - %#m2) = (%#m2 < %#m1)";
-by (blast_tac (claset() addSIs [real_preal_minus_less_rev1,
- real_preal_minus_less_rev2]) 1);
-qed "real_preal_minus_less_rev_iff";
+Goal "(- real_of_preal m1 < - real_of_preal m2) = \
+\ (real_of_preal m2 < real_of_preal m1)";
+by (blast_tac (claset() addSIs [real_of_preal_minus_less_rev1,
+ real_of_preal_minus_less_rev2]) 1);
+qed "real_of_preal_minus_less_rev_iff";
-Addsimps [real_preal_minus_less_rev_iff];
+Addsimps [real_of_preal_minus_less_rev_iff];
(*** linearity ***)
Goal "(R1::real) < R2 | R1 = R2 | R2 < R1";
-by (res_inst_tac [("x","R1")] real_preal_trichotomyE 1);
-by (ALLGOALS(res_inst_tac [("x","R2")] real_preal_trichotomyE));
+by (res_inst_tac [("x","R1")] real_of_preal_trichotomyE 1);
+by (ALLGOALS(res_inst_tac [("x","R2")] real_of_preal_trichotomyE));
by (auto_tac (claset() addSDs [preal_le_anti_sym],
- simpset() addsimps [preal_less_le_iff,real_preal_minus_less_zero,
- real_preal_zero_less,real_preal_minus_less_all]));
+ simpset() addsimps [preal_less_le_iff,real_of_preal_minus_less_zero,
+ real_of_preal_zero_less,real_of_preal_minus_less_all]));
qed "real_linear";
Goal "!!w::real. (w ~= z) = (w<z | z<w)";
@@ -883,46 +951,42 @@
by (blast_tac (claset() addSEs [real_less_asym]) 1);
qed "real_less_le";
-
Goal "(0r < -R) = (R < 0r)";
-by (res_inst_tac [("x","R")] real_preal_trichotomyE 1);
+by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
by (auto_tac (claset(),
- simpset() addsimps [real_preal_not_minus_gt_zero,
- real_preal_not_less_zero,real_preal_zero_less,
- real_preal_minus_less_zero]));
+ simpset() addsimps [real_of_preal_not_minus_gt_zero,
+ real_of_preal_not_less_zero,real_of_preal_zero_less,
+ real_of_preal_minus_less_zero]));
qed "real_minus_zero_less_iff";
Addsimps [real_minus_zero_less_iff];
Goal "(-R < 0r) = (0r < R)";
-by (res_inst_tac [("x","R")] real_preal_trichotomyE 1);
+by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
by (auto_tac (claset(),
- simpset() addsimps [real_preal_not_minus_gt_zero,
- real_preal_not_less_zero,real_preal_zero_less,
- real_preal_minus_less_zero]));
+ simpset() addsimps [real_of_preal_not_minus_gt_zero,
+ real_of_preal_not_less_zero,real_of_preal_zero_less,
+ real_of_preal_minus_less_zero]));
qed "real_minus_zero_less_iff2";
-
(*Alternative definition for real_less*)
Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S";
-by (res_inst_tac [("x","R")] real_preal_trichotomyE 1);
-by (ALLGOALS(res_inst_tac [("x","S")] real_preal_trichotomyE));
+by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
+by (ALLGOALS(res_inst_tac [("x","S")] real_of_preal_trichotomyE));
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
- simpset() addsimps [real_preal_not_minus_gt_all,
- real_preal_add, real_preal_not_less_zero,
+ simpset() addsimps [real_of_preal_not_minus_gt_all,
+ real_of_preal_add, real_of_preal_not_less_zero,
real_less_not_refl,
- real_preal_not_minus_gt_zero]));
-by (res_inst_tac [("x","%#D")] exI 1);
-by (res_inst_tac [("x","%#m+%#ma")] exI 2);
-by (res_inst_tac [("x","%#m")] exI 3);
-by (res_inst_tac [("x","%#D")] exI 4);
+ real_of_preal_not_minus_gt_zero]));
+by (res_inst_tac [("x","real_of_preal D")] exI 1);
+by (res_inst_tac [("x","real_of_preal m+real_of_preal ma")] exI 2);
+by (res_inst_tac [("x","real_of_preal m")] exI 3);
+by (res_inst_tac [("x","real_of_preal D")] exI 4);
by (auto_tac (claset(),
- simpset() addsimps [real_preal_zero_less,
- real_preal_sum_zero_less,real_add_assoc]));
+ simpset() addsimps [real_of_preal_zero_less,
+ real_of_preal_sum_zero_less,real_add_assoc]));
qed "real_less_add_positive_left_Ex";
-
-
(** change naff name(s)! **)
Goal "(W < S) ==> (0r < S + -W)";
by (dtac real_less_add_positive_left_Ex 1);
--- a/src/HOL/Real/RealDef.thy Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/RealDef.thy Fri Jul 23 17:29:12 1999 +0200
@@ -23,24 +23,33 @@
defs
- real_zero_def "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})"
- real_one_def "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})"
+ real_zero_def
+ "0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
+ preal_of_prat(prat_of_pnat 1p))})"
+ real_one_def
+ "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) +
+ preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
real_minus_def
- "- R == Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)"
+ "- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
real_diff_def "x - y == x + -(y::real)"
constdefs
- real_preal :: preal => real ("%#_" [100] 100)
- "%# m == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})"
+ real_of_preal :: preal => real
+ "real_of_preal m ==
+ Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p),
+ preal_of_prat(prat_of_pnat 1p))})"
rinv :: real => real
"rinv(R) == (@S. R ~= 0r & S*R = 1r)"
- real_nat :: nat => real ("%%# _" [100] 100)
- "%%# n == %#(@#($#(*# n)))"
+ real_of_posnat :: nat => real
+ "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
+
+ real_of_nat :: nat => real
+ "real_of_nat n == real_of_posnat n + -1r"
defs
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/RealPow.ML Fri Jul 23 17:29:12 1999 +0200
@@ -0,0 +1,374 @@
+(* Title : RealPow.ML
+ Author : Jacques D. Fleuriot
+ Copyright : 1998 University of Cambridge
+ Description : Natural Powers of reals theory
+
+*)
+
+Goal "0r ^ (Suc n) = 0r";
+by (Auto_tac);
+qed "realpow_zero";
+Addsimps [realpow_zero];
+
+Goal "r ~= 0r --> r ^ n ~= 0r";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addIs [real_mult_not_zeroE],
+ simpset() addsimps [real_zero_not_eq_one RS not_sym]));
+qed_spec_mp "realpow_not_zero";
+
+Goal "!!r. r ^ n = 0r ==> r = 0r";
+by (blast_tac (claset() addIs [ccontr]
+ addDs [realpow_not_zero]) 1);
+qed "realpow_zero_zero";
+
+Goal "r ~= 0r --> rinv(r ^ n) = (rinv r) ^ n";
+by (induct_tac "n" 1);
+by (Auto_tac);
+by (forw_inst_tac [("n","n")] realpow_not_zero 1);
+by (auto_tac (claset() addDs [real_rinv_distrib],
+ simpset()));
+qed_spec_mp "realpow_rinv";
+
+Goal "rabs r ^ n = rabs (r ^ n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(),simpset() addsimps
+ [rabs_mult,rabs_one]));
+qed "realpow_rabs";
+
+Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(),simpset() addsimps real_mult_ac));
+qed "realpow_add";
+
+Goal "(r::real) ^ 1 = r";
+by (Simp_tac 1);
+qed "realpow_one";
+Addsimps [realpow_one];
+
+Goal "(r::real) ^ 2 = r * r";
+by (Simp_tac 1);
+qed "realpow_two";
+
+Goal "0r < r --> 0r <= r ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addDs [real_less_imp_le]
+ addIs [real_le_mult_order],simpset()));
+qed_spec_mp "realpow_ge_zero";
+
+Goal "0r < r --> 0r < r ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addIs [real_mult_order],
+ simpset() addsimps [real_zero_less_one]));
+qed_spec_mp "realpow_gt_zero";
+
+Goal "0r <= r --> 0r <= r ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addIs [real_le_mult_order],
+ simpset()));
+qed_spec_mp "realpow_ge_zero2";
+
+Goal "0r < x & x <= y --> x ^ n <= y ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addSIs [real_mult_le_mono],
+ simpset()));
+by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1);
+qed_spec_mp "realpow_le";
+
+Goal "0r <= x & x <= y --> x ^ n <= y ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addSIs [real_mult_le_mono4],
+ simpset()));
+by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1);
+qed_spec_mp "realpow_le2";
+
+Goal "0r < x & x < y & 0 < n --> x ^ n < y ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addIs [real_mult_less_mono,
+ gr0I] addDs [realpow_gt_zero],simpset()));
+qed_spec_mp "realpow_less";
+
+Goal "1r ^ n = 1r";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed "realpow_eq_one";
+Addsimps [realpow_eq_one];
+
+Goal "rabs(-(1r ^ n)) = 1r";
+by (simp_tac (simpset() addsimps
+ [rabs_minus_cancel,rabs_one]) 1);
+qed "rabs_minus_realpow_one";
+Addsimps [rabs_minus_realpow_one];
+
+Goal "rabs((-1r) ^ n) = 1r";
+by (induct_tac "n" 1);
+by (auto_tac (claset(),simpset() addsimps [rabs_mult,
+ rabs_minus_cancel,rabs_one]));
+qed "rabs_realpow_minus_one";
+Addsimps [rabs_realpow_minus_one];
+
+Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(),simpset() addsimps real_mult_ac));
+qed "realpow_mult";
+
+Goal "0r <= r ^ 2";
+by (simp_tac (simpset() addsimps [realpow_two]) 1);
+qed "realpow_two_le";
+Addsimps [realpow_two_le];
+
+Goal "rabs(x ^ 2) = x ^ 2";
+by (simp_tac (simpset() addsimps [rabs_eqI1]) 1);
+qed "rabs_realpow_two";
+Addsimps [rabs_realpow_two];
+
+Goal "rabs(x) ^ 2 = x ^ 2";
+by (simp_tac (simpset() addsimps
+ [realpow_rabs,rabs_eqI1] delsimps [realpow_Suc]) 1);
+qed "realpow_two_rabs";
+Addsimps [realpow_two_rabs];
+
+Goal "!!r. 1r < r ==> 1r < r ^ 2";
+by (auto_tac (claset(),simpset() addsimps [realpow_two]));
+by (cut_facts_tac [real_zero_less_one] 1);
+by (forw_inst_tac [("R1.0","0r")] real_less_trans 1);
+by (assume_tac 1);
+by (dres_inst_tac [("z","r"),("x","1r")] real_mult_less_mono1 1);
+by (auto_tac (claset() addIs [real_less_trans],simpset()));
+qed "realpow_two_gt_one";
+
+Goal "!!r. 1r <= r ==> 1r <= r ^ 2";
+by (etac (real_le_imp_less_or_eq RS disjE) 1);
+by (etac (realpow_two_gt_one RS real_less_imp_le) 1);
+by (asm_simp_tac (simpset()) 1);
+qed "realpow_two_ge_one";
+
+(* more general result *)
+Goal "1r < r --> 1r <= r ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
+ simpset()));
+by (dtac (real_zero_less_one RS real_mult_less_mono) 1);
+by (dtac sym 4);
+by (auto_tac (claset() addSIs [real_less_imp_le],
+ simpset() addsimps [real_zero_less_one]));
+qed_spec_mp "realpow_ge_one";
+
+Goal "!!r. 1r < r ==> 1r < r ^ (Suc n)";
+by (forw_inst_tac [("n","n")] realpow_ge_one 1);
+by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
+by (dtac sym 2);
+by (forward_tac [real_zero_less_one RS real_less_trans] 1);
+by (dres_inst_tac [("y","r ^ n")] real_mult_less_mono2 1);
+by (auto_tac (claset() addDs [real_less_trans],
+ simpset()));
+qed "realpow_Suc_gt_one";
+
+Goal "!!r. 1r <= r ==> 1r <= r ^ n";
+by (dtac real_le_imp_less_or_eq 1);
+by (auto_tac (claset() addDs [realpow_ge_one],
+ simpset()));
+qed "realpow_ge_one2";
+
+Goal "!!r. 0r < r ==> 0r < r ^ Suc n";
+by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
+by (forw_inst_tac [("n1","n")]
+ ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
+by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
+ addIs [real_mult_order],simpset()));
+qed "realpow_Suc_gt_zero";
+
+Goal "!!r. 0r <= r ==> 0r <= r ^ Suc n";
+by (etac (real_le_imp_less_or_eq RS disjE) 1);
+by (etac (realpow_ge_zero) 1);
+by (asm_simp_tac (simpset()) 1);
+qed "realpow_Suc_ge_zero";
+
+Goal "1r <= (1r +1r) ^ n";
+by (res_inst_tac [("j","1r ^ n")] real_le_trans 1);
+by (rtac realpow_le 2);
+by (auto_tac (claset() addIs [real_less_imp_le],
+ simpset() addsimps [real_zero_less_one,
+ real_one_less_two]));
+qed "two_realpow_ge_one";
+
+Goal "real_of_nat n < (1r + 1r) ^ n";
+by (induct_tac "n" 1);
+by (rtac (lemmaS RS ssubst) 2);
+by (rtac (real_of_nat_add RS subst) 2);
+by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero,
+ real_zero_less_one,real_add_mult_distrib,real_of_nat_one]));
+by (blast_tac (claset() addSIs [real_add_less_le_mono,
+ two_realpow_ge_one]) 1);
+qed "two_realpow_gt";
+Addsimps [two_realpow_gt,two_realpow_ge_one];
+
+Goal "(-1r) ^ (2*n) = 1r";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed "realpow_minus_one";
+Addsimps [realpow_minus_one];
+
+Goal "(-1r) ^ (n + n) = 1r";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed "realpow_minus_one2";
+Addsimps [realpow_minus_one2];
+
+Goal "(-1r) ^ Suc (n + n) = -1r";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed "realpow_minus_one_odd";
+Addsimps [realpow_minus_one_odd];
+
+Goal "(-1r) ^ Suc (Suc (n + n)) = 1r";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed "realpow_minus_one_even";
+Addsimps [realpow_minus_one_even];
+
+Goal "0r < r & r < 1r --> r ^ Suc n < r ^ n";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed_spec_mp "realpow_Suc_less";
+
+Goal "0r <= r & r < 1r --> r ^ Suc n <= r ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addIs [real_less_imp_le] addSDs
+ [real_le_imp_less_or_eq],simpset()));
+qed_spec_mp "realpow_Suc_le";
+
+Goal "0r <= 0r ^ n";
+by (exhaust_tac "n" 1);
+by (Auto_tac);
+qed "realpow_zero_le";
+Addsimps [realpow_zero_le];
+
+Goal "0r < r & r < 1r --> r ^ Suc n <= r ^ n";
+by (blast_tac (claset() addSIs [real_less_imp_le,
+ realpow_Suc_less]) 1);
+qed_spec_mp "realpow_Suc_le2";
+
+Goal "!!r. [| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n";
+by (etac (real_le_imp_less_or_eq RS disjE) 1);
+by (rtac realpow_Suc_le2 1);
+by (Auto_tac);
+qed "realpow_Suc_le3";
+
+Goal "0r <= r & r < 1r & n < N --> r ^ N <= r ^ n";
+by (induct_tac "N" 1);
+by (Auto_tac);
+by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
+by (ALLGOALS(dtac real_mult_le_mono3));
+by (REPEAT(assume_tac 1));
+by (REPEAT(assume_tac 3));
+by (auto_tac (claset(),simpset() addsimps
+ [less_Suc_eq]));
+qed_spec_mp "realpow_less_le";
+
+Goal "!!r. [| 0r <= r; r < 1r; n <= N |] \
+\ ==> r ^ N <= r ^ n";
+by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [realpow_less_le],
+ simpset()));
+qed "realpow_le_le";
+
+Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n <= r";
+by (dres_inst_tac [("n","1"),("N","Suc n")]
+ (real_less_imp_le RS realpow_le_le) 1);
+by (Auto_tac);
+qed "realpow_Suc_le_self";
+
+Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n < 1r";
+by (blast_tac (claset() addIs [realpow_Suc_le_self,
+ real_le_less_trans]) 1);
+qed "realpow_Suc_less_one";
+
+Goal "1r <= r --> r ^ n <= r ^ Suc n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addSIs [real_mult_le_le_mono1],simpset()));
+by (rtac ccontr 1 THEN dtac not_real_leE 1);
+by (dtac real_le_less_trans 1 THEN assume_tac 1);
+by (etac (real_zero_less_one RS real_less_asym) 1);
+qed_spec_mp "realpow_le_Suc";
+
+Goal "1r < r --> r ^ n < r ^ Suc n";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addSIs [real_mult_less_mono2],simpset()));
+by (rtac ccontr 1 THEN dtac real_leI 1);
+by (dtac real_less_le_trans 1 THEN assume_tac 1);
+by (etac (real_zero_less_one RS real_less_asym) 1);
+qed_spec_mp "realpow_less_Suc";
+
+Goal "1r < r --> r ^ n <= r ^ Suc n";
+by (blast_tac (claset() addSIs [real_less_imp_le,
+ realpow_less_Suc]) 1);
+qed_spec_mp "realpow_le_Suc2";
+
+Goal "1r < r & n < N --> r ^ n <= r ^ N";
+by (induct_tac "N" 1);
+by (Auto_tac);
+by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
+by (ALLGOALS(dtac real_mult_self_le));
+by (assume_tac 1);
+by (assume_tac 2);
+by (auto_tac (claset() addIs [real_le_trans],
+ simpset() addsimps [less_Suc_eq]));
+qed_spec_mp "realpow_gt_ge";
+
+Goal "1r <= r & n < N --> r ^ n <= r ^ N";
+by (induct_tac "N" 1);
+by (Auto_tac);
+by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
+by (ALLGOALS(dtac real_mult_self_le2));
+by (assume_tac 1);
+by (assume_tac 2);
+by (auto_tac (claset() addIs [real_le_trans],
+ simpset() addsimps [less_Suc_eq]));
+qed_spec_mp "realpow_gt_ge2";
+
+Goal "!!r. [| 1r < r; n <= N |] ==> r ^ n <= r ^ N";
+by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
+qed "realpow_ge_ge";
+
+Goal "!!r. [| 1r <= r; n <= N |] ==> r ^ n <= r ^ N";
+by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
+qed "realpow_ge_ge2";
+
+Goal "!!r. 1r < r ==> r <= r ^ Suc n";
+by (dres_inst_tac [("n","1"),("N","Suc n")]
+ realpow_ge_ge 1);
+by (Auto_tac);
+qed_spec_mp "realpow_Suc_ge_self";
+
+Goal "!!r. 1r <= r ==> r <= r ^ Suc n";
+by (dres_inst_tac [("n","1"),("N","Suc n")]
+ realpow_ge_ge2 1);
+by (Auto_tac);
+qed_spec_mp "realpow_Suc_ge_self2";
+
+Goal "!!r. [| 1r < r; 0 < n |] ==> r <= r ^ n";
+by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
+by (auto_tac (claset() addSIs
+ [realpow_Suc_ge_self],simpset()));
+qed "realpow_ge_self";
+
+Goal "!!r. [| 1r <= r; 0 < n |] ==> r <= r ^ n";
+by (dtac (less_not_refl2 RS not0_implies_Suc) 1);
+by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset()));
+qed "realpow_ge_self2";
+
+Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n";
+by (induct_tac "n" 1);
+by (auto_tac (claset(),simpset()
+ addsimps [real_mult_commute]));
+qed_spec_mp "realpow_minus_mult";
+Addsimps [realpow_minus_mult];
+
+Goal "!!r. r ~= 0r ==> r * rinv(r) ^ 2 = rinv r";
+by (asm_simp_tac (simpset() addsimps [realpow_two,
+ real_mult_assoc RS sym]) 1);
+qed "realpow_two_mult_rinv";
+Addsimps [realpow_two_mult_rinv];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/RealPow.thy Fri Jul 23 17:29:12 1999 +0200
@@ -0,0 +1,16 @@
+(* Title : RealPow.thy
+ Author : Jacques D. Fleuriot
+ Copyright : 1998 University of Cambridge
+ Description : Natural powers theory
+
+*)
+
+RealPow = WF_Rel + RealAbs +
+
+instance real :: {power}
+
+primrec
+ realpow_0 "r ^ 0 = 1r"
+ realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
+
+end