--- a/src/HOL/Hyperreal/HRealAbs.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HRealAbs.ML Mon Oct 08 15:23:20 2001 +0200
@@ -241,7 +241,7 @@
qed "inj_hypreal_of_nat";
Goalw [hypreal_of_nat_def]
- "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr";
+ "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)";
by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1);
qed "hypreal_of_nat_Suc";
--- a/src/HOL/Hyperreal/HSeries.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HSeries.ML Mon Oct 08 15:23:20 2001 +0200
@@ -44,7 +44,7 @@
(* Theorem corresponding to recursive case in def of sumr *)
Goalw [hypnat_one_def]
- "sumhr(m,n+1hn,f) = (if n + 1hn <= m then Numeral0 \
+ "sumhr(m,n+(1::hypnat),f) = (if n + (1::hypnat) <= m then Numeral0 \
\ else sumhr(m,n,f) + (*fNat* f) n)";
by (simp_tac (HOL_ss addsimps
[zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
@@ -55,7 +55,7 @@
by (ALLGOALS(Ultra_tac));
qed "sumhr_if";
-Goalw [hypnat_one_def] "sumhr (n + 1hn, n, f) = Numeral0";
+Goalw [hypnat_one_def] "sumhr (n + (1::hypnat), n, f) = Numeral0";
by (simp_tac (HOL_ss addsimps
[zero_eq_numeral_0 RS sym, hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
@@ -73,7 +73,7 @@
Addsimps [sumhr_eq_bounds];
Goalw [hypnat_one_def]
- "sumhr (m,m + 1hn,f) = (*fNat* f) m";
+ "sumhr (m,m + (1::hypnat),f) = (*fNat* f) m";
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
simpset() addsimps [sumhr, hypnat_add,starfunNat]));
@@ -290,7 +290,7 @@
Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> Numeral0";
by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy]));
by (dtac bspec 1 THEN Auto_tac);
-by (dres_inst_tac [("x","N + 1hn")] bspec 1);
+by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1);
by (auto_tac (claset() addIs [HNatInfinite_add_one,
approx_hrabs_zero_cancel],
simpset() addsimps [rename_numerals hypreal_of_real_zero]));
--- a/src/HOL/Hyperreal/HyperBin.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML Mon Oct 08 15:23:20 2001 +0200
@@ -17,7 +17,7 @@
by (simp_tac (simpset() addsimps [hypreal_of_real_zero RS sym]) 1);
qed "zero_eq_numeral_0";
-Goalw [hypreal_number_of_def] "1hr = Numeral1";
+Goalw [hypreal_number_of_def] "(1::hypreal) = Numeral1";
by (simp_tac (simpset() addsimps [hypreal_of_real_one RS sym]) 1);
qed "one_eq_numeral_1";
@@ -105,13 +105,13 @@
qed "le_hypreal_number_of_eq_not_less";
Addsimps [le_hypreal_number_of_eq_not_less];
-(*** New versions of existing theorems involving 0, 1hr ***)
+(*** New versions of existing theorems involving 0, 1 ***)
Goal "- Numeral1 = (-1::hypreal)";
by (Simp_tac 1);
qed "minus_numeral_one";
-(*Maps 0 to Numeral0 and 1hr to Numeral1 and -1hr to -1*)
+(*Maps 0 to Numeral0 and (1::hypreal) to Numeral1 and -(Numeral1) to -1*)
val hypreal_numeral_ss =
real_numeral_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1,
minus_numeral_one];
@@ -120,7 +120,7 @@
asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th);
-(*Now insert some identities previously stated for 0 and 1hr*)
+(*Now insert some identities previously stated for 0 and 1*)
(** HyperDef **)
--- a/src/HOL/Hyperreal/HyperDef.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperDef.ML Mon Oct 08 15:23:20 2001 +0200
@@ -531,12 +531,12 @@
bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute,
hypreal_mult_left_commute]);
-Goalw [hypreal_one_def] "1hr * z = z";
+Goalw [hypreal_one_def] "(1::hypreal) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
qed "hypreal_mult_1";
-Goal "z * 1hr = z";
+Goal "z * (1::hypreal) = z";
by (simp_tac (simpset() addsimps [hypreal_mult_commute,
hypreal_mult_1]) 1);
qed "hypreal_mult_1_right";
@@ -614,7 +614,7 @@
qed "hypreal_diff_mult_distrib2";
(*** one and zero are distinct ***)
-Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
+Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= (1::hypreal)";
by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one]));
qed "hypreal_zero_not_eq_one";
@@ -657,7 +657,7 @@
qed "hypreal_inverse_inverse";
Addsimps [hypreal_inverse_inverse];
-Goalw [hypreal_one_def] "inverse(1hr) = 1hr";
+Goalw [hypreal_one_def] "inverse((1::hypreal)) = (1::hypreal)";
by (full_simp_tac (simpset() addsimps [hypreal_inverse,
real_zero_not_eq_one RS not_sym]) 1);
qed "hypreal_inverse_1";
@@ -667,7 +667,7 @@
(*** existence of inverse ***)
Goalw [hypreal_one_def,hypreal_zero_def]
- "x ~= 0 ==> x*inverse(x) = 1hr";
+ "x ~= 0 ==> x*inverse(x) = (1::hypreal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (rotate_tac 1 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
@@ -676,7 +676,7 @@
FreeUltrafilterNat_subset]) 1);
qed "hypreal_mult_inverse";
-Goal "x ~= 0 ==> inverse(x)*x = 1hr";
+Goal "x ~= 0 ==> inverse(x)*x = (1::hypreal)";
by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse,
hypreal_mult_commute]) 1);
qed "hypreal_mult_inverse_left";
@@ -844,12 +844,12 @@
by (res_inst_tac [("x","%n. Numeral0")] exI 1);
by (Step_tac 1);
by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
-qed "lemma_hyprel_0r_mem";
+qed "lemma_hyprel_0_mem";
Goalw [hypreal_zero_def]"0 < x | x = 0 | x < (0::hypreal)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
-by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1);
+by (cut_facts_tac [lemma_hyprel_0_mem] 1 THEN etac exE 1);
by (dres_inst_tac [("x","xa")] spec 1);
by (dres_inst_tac [("x","x")] spec 1);
by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1);
@@ -1101,7 +1101,7 @@
(*DON'T insert this or the next one as default simprules.
They are used in both orientations and anyway aren't the ones we finally
need, which would use binary literals.*)
-Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real Numeral1 = 1hr";
+Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real Numeral1 = (1::hypreal)";
by (Step_tac 1);
qed "hypreal_of_real_one";
@@ -1139,7 +1139,7 @@
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
qed "hypreal_zero_divide";
-Goal "x/1hr = x";
+Goal "x/(1::hypreal) = x";
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
qed "hypreal_divide_one";
Addsimps [hypreal_zero_divide, hypreal_divide_one];
--- a/src/HOL/Hyperreal/HyperDef.thy Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Mon Oct 08 15:23:20 2001 +0200
@@ -25,12 +25,7 @@
typedef hypreal = "UNIV//hyprel" (Equiv.quotient_def)
instance
- hypreal :: {ord, zero, plus, times, minus, inverse}
-
-consts
-
- "1hr" :: hypreal ("1hr")
-
+ hypreal :: {ord, zero, one, plus, times, minus, inverse}
defs
@@ -38,7 +33,7 @@
"0 == Abs_hypreal(hyprel``{%n::nat. (Numeral0::real)})"
hypreal_one_def
- "1hr == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})"
+ "1 == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})"
hypreal_minus_def
"- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
--- a/src/HOL/Hyperreal/HyperNat.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperNat.ML Mon Oct 08 15:23:20 2001 +0200
@@ -310,13 +310,13 @@
val hypnat_mult_ac = [hypnat_mult_assoc, hypnat_mult_commute,
hypnat_mult_left_commute];
-Goalw [hypnat_one_def] "1hn * z = z";
+Goalw [hypnat_one_def] "(1::hypnat) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
by (asm_full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
qed "hypnat_mult_1";
Addsimps [hypnat_mult_1];
-Goal "z * 1hn = z";
+Goal "z * (1::hypnat) = z";
by (simp_tac (simpset() addsimps [hypnat_mult_commute]) 1);
qed "hypnat_mult_1_right";
Addsimps [hypnat_mult_1_right];
@@ -375,7 +375,7 @@
Addsimps [hypnat_add_mult_distrib2];
(*** (hypnat) one and zero are distinct ***)
-Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= 1hn";
+Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= (1::hypnat)";
by Auto_tac;
qed "hypnat_zero_not_eq_one";
Addsimps [hypnat_zero_not_eq_one];
@@ -446,7 +446,7 @@
bind_thm ("hypnat_less_zeroE", hypnat_not_less0 RS notE);
Goalw [hypnat_less_def,hypnat_zero_def,hypnat_one_def]
- "(n<1hn) = (n=0)";
+ "(n<(1::hypnat)) = (n=0)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset() addSIs [exI] addEs
[FreeUltrafilterNat_subset],simpset()));
@@ -680,7 +680,7 @@
qed "hypnat_le_mult_order";
Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def]
- "(0::hypnat) < 1hn";
+ "(0::hypnat) < (1::hypnat)";
by (res_inst_tac [("x","%n. 0")] exI 1);
by (res_inst_tac [("x","%n. Suc 0")] exI 1);
by Auto_tac;
@@ -736,19 +736,19 @@
qed "hypnat_add_self_le";
Addsimps [hypnat_add_self_le];
-Goal "(x::hypnat) < x + 1hn";
+Goal "(x::hypnat) < x + (1::hypnat)";
by (cut_facts_tac [hypnat_zero_less_one
RS hypnat_add_less_mono2] 1);
by Auto_tac;
qed "hypnat_add_one_self_less";
Addsimps [hypnat_add_one_self_less];
-Goalw [hypnat_le_def] "~ x + 1hn <= x";
+Goalw [hypnat_le_def] "~ x + (1::hypnat) <= x";
by (Simp_tac 1);
qed "not_hypnat_add_one_le_self";
Addsimps [not_hypnat_add_one_le_self];
-Goal "((0::hypnat) < n) = (1hn <= n)";
+Goal "((0::hypnat) < n) = ((1::hypnat) <= n)";
by (res_inst_tac [("x","n")] hypnat_trichotomyE 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_le_def]));
qed "hypnat_gt_zero_iff";
@@ -756,11 +756,11 @@
Addsimps [hypnat_le_add_diff_inverse, hypnat_le_add_diff_inverse2,
hypnat_less_imp_le RS hypnat_le_add_diff_inverse2];
-Goal "(0 < n) = (EX m. n = m + 1hn)";
+Goal "(0 < n) = (EX m. n = m + (1::hypnat))";
by (Step_tac 1);
by (res_inst_tac [("x","m")] hypnat_trichotomyE 2);
by (rtac hypnat_less_trans 2);
-by (res_inst_tac [("x","n - 1hn")] exI 1);
+by (res_inst_tac [("x","n - (1::hypnat)")] exI 1);
by (auto_tac (claset(),simpset() addsimps
[hypnat_gt_zero_iff,hypnat_add_commute]));
qed "hypnat_gt_zero_iff2";
@@ -806,7 +806,7 @@
by Auto_tac;
qed "hypnat_of_nat_le_iff";
-Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat (Suc 0) = 1hn";
+Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat (Suc 0) = (1::hypnat)";
by (Simp_tac 1);
qed "hypnat_of_nat_one";
@@ -825,7 +825,7 @@
qed "hypnat_of_nat_not_zero_iff";
Goalw [hypnat_of_nat_def,hypnat_one_def]
- "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn";
+ "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)";
by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
qed "hypnat_of_nat_Suc";
@@ -911,7 +911,7 @@
by (Simp_tac 1);
qed "SHNat_hypnat_of_nat_zero";
-Goal "1hn : Nats";
+Goal "(1::hypnat) : Nats";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one,
hypnat_of_nat_one RS sym]) 1);
qed "SHNat_one";
@@ -924,7 +924,7 @@
Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero,
SHNat_one,SHNat_zero];
-Goal "1hn + 1hn : Nats";
+Goal "(1::hypnat) + (1::hypnat) : Nats";
by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1);
qed "SHNat_two";
@@ -1000,7 +1000,7 @@
qed "hypnat_zero_less_hypnat_omega";
Addsimps [hypnat_zero_less_hypnat_omega];
-Goal "1hn < whn";
+Goal "(1::hypnat) < whn";
by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
by Auto_tac;
qed "hypnat_one_less_hypnat_omega";
@@ -1104,7 +1104,7 @@
FreeUltrafilterNat_HNatInfinite]) 1);
qed "HNatInfinite_FreeUltrafilterNat_iff";
-Goal "x : HNatInfinite ==> 1hn < x";
+Goal "x : HNatInfinite ==> (1::hypnat) < x";
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
qed "HNatInfinite_gt_one";
Addsimps [HNatInfinite_gt_one];
@@ -1112,7 +1112,7 @@
Goal "0 ~: HNatInfinite";
by (auto_tac (claset(),simpset()
addsimps [HNatInfinite_iff]));
-by (dres_inst_tac [("a","1hn")] equals0D 1);
+by (dres_inst_tac [("a","(1::hypnat)")] equals0D 1);
by (Asm_full_simp_tac 1);
qed "zero_not_mem_HNatInfinite";
Addsimps [zero_not_mem_HNatInfinite];
@@ -1121,7 +1121,7 @@
by Auto_tac;
qed "HNatInfinite_not_eq_zero";
-Goal "x : HNatInfinite ==> 1hn <= x";
+Goal "x : HNatInfinite ==> (1::hypnat) <= x";
by (blast_tac (claset() addIs [hypnat_less_imp_le,
HNatInfinite_gt_one]) 1);
qed "HNatInfinite_ge_one";
@@ -1156,20 +1156,20 @@
simpset() addsimps [not_SHNat_HNatInfinite_iff,HNatInfinite_iff]));
qed "HNatInfinite_SHNat_diff";
-Goal "x: HNatInfinite ==> x + 1hn: HNatInfinite";
+Goal "x: HNatInfinite ==> x + (1::hypnat): HNatInfinite";
by (auto_tac (claset() addIs [HNatInfinite_SHNat_add],
simpset()));
qed "HNatInfinite_add_one";
-Goal "x: HNatInfinite ==> x - 1hn: HNatInfinite";
+Goal "x: HNatInfinite ==> x - (1::hypnat): HNatInfinite";
by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
-by (dres_inst_tac [("x","x - 1hn"),("y","1hn")] SHNat_add 1);
+by (dres_inst_tac [("x","x - (1::hypnat)"),("y","(1::hypnat)")] SHNat_add 1);
by (auto_tac (claset(),simpset() addsimps
[not_SHNat_HNatInfinite_iff RS sym]));
qed "HNatInfinite_minus_one";
-Goal "x : HNatInfinite ==> EX y. x = y + 1hn";
-by (res_inst_tac [("x","x - 1hn")] exI 1);
+Goal "x : HNatInfinite ==> EX y. x = y + (1::hypnat)";
+by (res_inst_tac [("x","x - (1::hypnat)")] exI 1);
by Auto_tac;
qed "HNatInfinite_is_Suc";
@@ -1253,7 +1253,7 @@
qed "hypreal_of_hypnat_zero";
Goalw [hypnat_one_def]
- "hypreal_of_hypnat 1hn = Numeral1";
+ "hypreal_of_hypnat (1::hypnat) = Numeral1";
by (simp_tac (HOL_ss addsimps
[one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
by (simp_tac (simpset() addsimps [hypreal_of_hypnat, real_of_nat_one]) 1);
@@ -1297,12 +1297,12 @@
Goal "~ (ALL n. n = (0::hypnat))";
by Auto_tac;
-by (res_inst_tac [("x","1hn")] exI 1);
+by (res_inst_tac [("x","(1::hypnat)")] exI 1);
by (Simp_tac 1);
qed "hypnat_not_all_eq_zero";
Addsimps [hypnat_not_all_eq_zero];
-Goal "n ~= 0 ==> (n <= 1hn) = (n = 1hn)";
+Goal "n ~= 0 ==> (n <= (1::hypnat)) = (n = (1::hypnat))";
by (auto_tac (claset(), simpset() addsimps [hypnat_le_less]));
qed "hypnat_le_one_eq_one";
Addsimps [hypnat_le_one_eq_one];
--- a/src/HOL/Hyperreal/HyperNat.thy Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Mon Oct 08 15:23:20 2001 +0200
@@ -15,10 +15,9 @@
typedef hypnat = "UNIV//hypnatrel" (Equiv.quotient_def)
instance
- hypnat :: {ord,zero,plus,times,minus}
+ hypnat :: {ord, zero, one, plus, times, minus}
consts
- "1hn" :: hypnat ("1hn")
"whn" :: hypnat ("whn")
constdefs
@@ -54,7 +53,7 @@
(** hypernatural arithmetic **)
hypnat_zero_def "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
- hypnat_one_def "1hn == Abs_hypnat(hypnatrel``{%n::nat. 1})"
+ hypnat_one_def "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
(* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
hypnat_omega_def "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
--- a/src/HOL/Hyperreal/HyperOrd.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperOrd.ML Mon Oct 08 15:23:20 2001 +0200
@@ -149,7 +149,7 @@
by (Asm_full_simp_tac 1);
qed "hypreal_mult_less_zero";
-Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
+Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < (1::hypreal)";
by (res_inst_tac [("x","%n. Numeral0")] exI 1);
by (res_inst_tac [("x","%n. Numeral1")] exI 1);
by (auto_tac (claset(),
--- a/src/HOL/Hyperreal/HyperPow.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperPow.ML Mon Oct 08 15:23:20 2001 +0200
@@ -241,7 +241,7 @@
by (Fuf_tac 1);
qed "hyperpow";
-Goalw [hypnat_one_def] "(Numeral0::hypreal) pow (n + 1hn) = Numeral0";
+Goalw [hypnat_one_def] "(Numeral0::hypreal) pow (n + (1::hypnat)) = Numeral0";
by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
@@ -285,14 +285,14 @@
simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add]));
qed "hyperpow_add";
-Goalw [hypnat_one_def] "r pow 1hn = r";
+Goalw [hypnat_one_def] "r pow (1::hypnat) = r";
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
qed "hyperpow_one";
Addsimps [hyperpow_one];
Goalw [hypnat_one_def]
- "r pow (1hn + 1hn) = r * r";
+ "r pow ((1::hypnat) + (1::hypnat)) = r * r";
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
by (auto_tac (claset(),
simpset() addsimps [hyperpow,hypnat_add, hypreal_mult]));
@@ -341,7 +341,7 @@
Addsimps [hrabs_minus_hyperpow_one];
Goal "abs(-1 pow n) = (Numeral1::hypreal)";
-by (subgoal_tac "abs((- 1hr) pow n) = 1hr" 1);
+by (subgoal_tac "abs((- (1::hypreal)) pow n) = (1::hypreal)" 1);
by (Asm_full_simp_tac 1);
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
@@ -358,31 +358,31 @@
simpset() addsimps [hyperpow, hypreal_mult,realpow_mult]));
qed "hyperpow_mult";
-Goal "(Numeral0::hypreal) <= r pow (1hn + 1hn)";
+Goal "(Numeral0::hypreal) <= r pow ((1::hypnat) + (1::hypnat))";
by (auto_tac (claset(),
simpset() addsimps [hyperpow_two, hypreal_0_le_mult_iff]));
qed "hyperpow_two_le";
Addsimps [hyperpow_two_le];
-Goal "abs(x pow (1hn + 1hn)) = x pow (1hn + 1hn)";
+Goal "abs(x pow ((1::hypnat) + (1::hypnat))) = x pow ((1::hypnat) + (1::hypnat))";
by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1);
qed "hrabs_hyperpow_two";
Addsimps [hrabs_hyperpow_two];
-Goal "abs(x) pow (1hn + 1hn) = x pow (1hn + 1hn)";
+Goal "abs(x) pow ((1::hypnat) + (1::hypnat)) = x pow ((1::hypnat) + (1::hypnat))";
by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1);
qed "hyperpow_two_hrabs";
Addsimps [hyperpow_two_hrabs];
(*? very similar to hrealpow_two_gt_one *)
-Goal "(Numeral1::hypreal) < r ==> Numeral1 < r pow (1hn + 1hn)";
+Goal "(Numeral1::hypreal) < r ==> Numeral1 < r pow ((1::hypnat) + (1::hypnat))";
by (auto_tac (claset(), simpset() addsimps [hyperpow_two]));
by (res_inst_tac [("y","Numeral1*Numeral1")] order_le_less_trans 1);
by (rtac hypreal_mult_less_mono 2);
by Auto_tac;
qed "hyperpow_two_gt_one";
-Goal "(Numeral1::hypreal) <= r ==> Numeral1 <= r pow (1hn + 1hn)";
+Goal "(Numeral1::hypreal) <= r ==> Numeral1 <= r pow ((1::hypnat) + (1::hypnat))";
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq]
addIs [hyperpow_two_gt_one,order_less_imp_le],
simpset()));
@@ -397,8 +397,8 @@
Addsimps [simplify (simpset()) realpow_minus_one];
-Goal "-1 pow ((1hn + 1hn)*n) = (Numeral1::hypreal)";
-by (subgoal_tac "(-(1hr)) pow ((1hn + 1hn)*n) = 1hr" 1);
+Goal "-1 pow (((1::hypnat) + (1::hypnat))*n) = (Numeral1::hypreal)";
+by (subgoal_tac "(-((1::hypreal))) pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)" 1);
by (Asm_full_simp_tac 1);
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
@@ -409,7 +409,7 @@
Addsimps [hyperpow_minus_one2];
Goalw [hypnat_one_def]
- "(Numeral0::hypreal) < r & r < Numeral1 --> r pow (n + 1hn) < r pow n";
+ "(Numeral0::hypreal) < r & r < Numeral1 --> r pow (n + (1::hypnat)) < r pow n";
by (full_simp_tac
(HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
@@ -421,7 +421,7 @@
qed_spec_mp "hyperpow_Suc_less";
Goalw [hypnat_one_def]
- "Numeral0 <= r & r < (Numeral1::hypreal) --> r pow (n + 1hn) <= r pow n";
+ "Numeral0 <= r & r < (Numeral1::hypreal) --> r pow (n + (1::hypnat)) <= r pow n";
by (full_simp_tac
(HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
@@ -482,13 +482,13 @@
by (auto_tac (claset() addIs [hyperpow_less_le], simpset()));
qed "hyperpow_le_le";
-Goal "[| (Numeral0::hypreal) < r; r < Numeral1 |] ==> r pow (n + 1hn) <= r";
-by (dres_inst_tac [("n","1hn")] (order_less_imp_le RS hyperpow_le_le) 1);
+Goal "[| (Numeral0::hypreal) < r; r < Numeral1 |] ==> r pow (n + (1::hypnat)) <= r";
+by (dres_inst_tac [("n","(1::hypnat)")] (order_less_imp_le RS hyperpow_le_le) 1);
by (Auto_tac);
qed "hyperpow_Suc_le_self";
-Goal "[| (Numeral0::hypreal) <= r; r < Numeral1 |] ==> r pow (n + 1hn) <= r";
-by (dres_inst_tac [("n","1hn")] hyperpow_le_le 1);
+Goal "[| (Numeral0::hypreal) <= r; r < Numeral1 |] ==> r pow (n + (1::hypnat)) <= r";
+by (dres_inst_tac [("n","(1::hypnat)")] hyperpow_le_le 1);
by (Auto_tac);
qed "hyperpow_Suc_le_self2";
--- a/src/HOL/Hyperreal/HyperPow.thy Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Mon Oct 08 15:23:20 2001 +0200
@@ -20,7 +20,7 @@
consts hpowr :: "[hypreal,nat] => hypreal"
primrec
- hpowr_0 "r ^ 0 = 1hr"
+ hpowr_0 "r ^ 0 = (1::hypreal)"
hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
consts
--- a/src/HOL/Hyperreal/Lim.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML Mon Oct 08 15:23:20 2001 +0200
@@ -1712,7 +1712,7 @@
qed "abs_real_of_nat_cancel";
Addsimps [abs_real_of_nat_cancel];
-Goal "~ abs(x) + 1r < x";
+Goal "~ abs(x) + (1::real) < x";
by (rtac real_leD 1);
by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset()));
qed "abs_add_one_not_less_self";
--- a/src/HOL/Hyperreal/NatStar.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/NatStar.ML Mon Oct 08 15:23:20 2001 +0200
@@ -358,7 +358,7 @@
(*----------------------------------------------------------------
NS extension when we displace argument by one
---------------------------------------------------------------*)
-Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + 1hn)";
+Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + (1::hypnat))";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),
simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
--- a/src/HOL/Hyperreal/SEQ.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/SEQ.ML Mon Oct 08 15:23:20 2001 +0200
@@ -1248,7 +1248,7 @@
by (forward_tac [HNatInfinite_add_one] 1);
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","N + 1hn")] bspec 1 THEN assume_tac 1);
+by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
by (dtac approx_mult_subst_SReal 1 THEN assume_tac 1);
by (dtac approx_trans3 1 THEN assume_tac 1);
--- a/src/HOL/Integ/Bin.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Integ/Bin.ML Mon Oct 08 15:23:20 2001 +0200
@@ -182,8 +182,14 @@
(** Converting simple cases of (int n) to numerals **)
-(*int 0 = Numeral0 *)
-bind_thm ("int_0", number_of_Pls RS sym);
+Goal "int 0 = Numeral0";
+by (rtac sym 1);
+by (rtac number_of_Pls 1);
+qed "int_0";
+
+Goal "int 1 = Numeral1";
+by (Simp_tac 1);
+qed "int_1";
Goal "int (Suc n) = Numeral1 + int n";
by (simp_tac (simpset() addsimps [zadd_int]) 1);
--- a/src/HOL/Integ/IntDef.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Integ/IntDef.ML Mon Oct 08 15:23:20 2001 +0200
@@ -7,8 +7,8 @@
*)
-(*Rewrite the overloaded 0::int to (int 0)*) (* FIXME !? *)
-Addsimps [Zero_int_def];
+(*Rewrite the overloaded 0::int and 1::int*) (* FIXME *)
+Addsimps [Zero_int_def, One_int_def];
Goalw [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
by (Blast_tac 1);
--- a/src/HOL/Integ/IntDef.thy Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Integ/IntDef.thy Mon Oct 08 15:23:20 2001 +0200
@@ -15,7 +15,7 @@
int = "UNIV//intrel" (Equiv.quotient_def)
instance
- int :: {ord, zero, plus, times, minus}
+ int :: {ord, zero, one, plus, times, minus}
defs
zminus_def
@@ -35,7 +35,8 @@
defs (*of overloaded constants*)
- Zero_int_def "0 == int 0"
+ Zero_int_def "0 == int 0"
+ One_int_def "1 == int 1"
zadd_def
"z + w ==
--- a/src/HOL/Integ/int_arith1.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Integ/int_arith1.ML Mon Oct 08 15:23:20 2001 +0200
@@ -410,7 +410,7 @@
zmult_1, zmult_1_right,
zmult_minus1, zmult_minus1_right,
zminus_zadd_distrib, zminus_zminus, zmult_assoc,
- Zero_int_def, int_0, zadd_int RS sym, int_Suc];
+ Zero_int_def, One_int_def, int_0, int_1, zadd_int RS sym, int_Suc];
val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
Int_Numeral_Simprocs.cancel_numerals;
--- a/src/HOL/Real/RealBin.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Real/RealBin.ML Mon Oct 08 15:23:20 2001 +0200
@@ -17,7 +17,7 @@
by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1);
qed "zero_eq_numeral_0";
-Goalw [real_number_of_def] "1r = Numeral1";
+Goalw [real_number_of_def] "(1::real) = Numeral1";
by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1);
qed "one_eq_numeral_1";
@@ -109,14 +109,14 @@
Addsimps [le_real_number_of_eq_not_less];
-(*** New versions of existing theorems involving 0, 1r ***)
+(*** New versions of existing theorems involving 0, 1 ***)
Goal "- Numeral1 = (-1::real)";
by (Simp_tac 1);
qed "minus_numeral_one";
-(*Maps 0 to Numeral0 and 1r to Numeral1 and -1r to -1*)
+(*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*)
val real_numeral_ss =
HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1,
minus_numeral_one];
@@ -125,7 +125,7 @@
asm_full_simplify real_numeral_ss (Thm.transfer (the_context ()) th);
-(*Now insert some identities previously stated for 0 and 1r*)
+(*Now insert some identities previously stated for 0 and 1*)
(** RealDef & Real **)
--- a/src/HOL/Real/RealDef.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Real/RealDef.ML Mon Oct 08 15:23:20 2001 +0200
@@ -338,7 +338,7 @@
bind_thms ("real_mult_ac",
[real_mult_assoc, real_mult_commute, real_mult_left_commute]);
-Goalw [real_one_def,pnat_one_def] "1r * z = z";
+Goalw [real_one_def,pnat_one_def] "(1::real) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_REAL 1);
by (asm_full_simp_tac
(simpset() addsimps [real_mult,
@@ -348,7 +348,7 @@
Addsimps [real_mult_1];
-Goal "z * 1r = z";
+Goal "z * (1::real) = z";
by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
qed "real_mult_1_right";
@@ -382,11 +382,11 @@
Addsimps [real_minus_mult_eq1 RS sym, real_minus_mult_eq2 RS sym];
-Goal "(- 1r) * z = -z";
+Goal "(- (1::real)) * z = -z";
by (Simp_tac 1);
qed "real_mult_minus_1";
-Goal "z * (- 1r) = -z";
+Goal "z * (- (1::real)) = -z";
by (stac real_mult_commute 1);
by (Simp_tac 1);
qed "real_mult_minus_1_right";
@@ -441,7 +441,7 @@
qed "real_diff_mult_distrib2";
(*** one and zero are distinct ***)
-Goalw [real_zero_def,real_one_def] "0 ~= 1r";
+Goalw [real_zero_def,real_one_def] "0 ~= (1::real)";
by (auto_tac (claset(),
simpset() addsimps [preal_self_less_add_left RS preal_not_refl2]));
qed "real_zero_not_eq_one";
@@ -453,7 +453,7 @@
qed "real_zero_iff";
Goalw [real_zero_def,real_one_def]
- "!!(x::real). x ~= 0 ==> EX y. x*y = 1r";
+ "!!(x::real). x ~= 0 ==> EX y. x*y = (1::real)";
by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
@@ -471,12 +471,12 @@
@ preal_add_ac @ preal_mult_ac));
qed "real_mult_inv_right_ex";
-Goal "x ~= 0 ==> EX y. y*x = 1r";
+Goal "x ~= 0 ==> EX y. y*x = (1::real)";
by (dtac real_mult_inv_right_ex 1);
by (auto_tac (claset(), simpset() addsimps [real_mult_commute]));
qed "real_mult_inv_left_ex";
-Goalw [real_inverse_def] "x ~= 0 ==> inverse(x)*x = 1r";
+Goalw [real_inverse_def] "x ~= 0 ==> inverse(x)*x = (1::real)";
by (ftac real_mult_inv_left_ex 1);
by (Step_tac 1);
by (rtac someI2 1);
@@ -484,7 +484,7 @@
qed "real_mult_inv_left";
Addsimps [real_mult_inv_left];
-Goal "x ~= 0 ==> x*inverse(x) = 1r";
+Goal "x ~= 0 ==> x*inverse(x) = (1::real)";
by (stac real_mult_commute 1);
by (auto_tac (claset(), simpset() addsimps [real_mult_inv_left]));
qed "real_mult_inv_right";
@@ -548,7 +548,7 @@
qed "real_inverse_inverse";
Addsimps [real_inverse_inverse];
-Goalw [real_inverse_def] "inverse(1r) = 1r";
+Goalw [real_inverse_def] "inverse((1::real)) = (1::real)";
by (cut_facts_tac [real_zero_not_eq_one RS
not_sym RS real_mult_inv_left_ex] 1);
by (auto_tac (claset(),
--- a/src/HOL/Real/RealDef.thy Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Real/RealDef.thy Mon Oct 08 15:23:20 2001 +0200
@@ -19,11 +19,9 @@
instance
- real :: {ord, zero, plus, times, minus, inverse}
+ real :: {ord, zero, one, plus, times, minus, inverse}
consts
- "1r" :: real ("1r")
-
(*Overloaded constants denoting the Nat and Real subsets of enclosing
types such as hypreal and complex*)
Nats, Reals :: "'a set"
@@ -38,7 +36,7 @@
"0 == 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) +
+ "1 == 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
@@ -48,7 +46,7 @@
"R - (S::real) == R + - S"
real_inverse_def
- "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1r)"
+ "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
real_divide_def
"R / (S::real) == R * inverse S"
@@ -69,7 +67,7 @@
defs
(*overloaded*)
- real_of_nat_def "real n == real_of_posnat n + (- 1r)"
+ real_of_nat_def "real n == real_of_posnat n + (- 1)"
real_add_def
"P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
--- a/src/HOL/Real/RealInt.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Real/RealInt.ML Mon Oct 08 15:23:20 2001 +0200
@@ -39,7 +39,7 @@
by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
qed "real_of_int_zero";
-Goalw [int_def,real_one_def] "real (int 1) = 1r";
+Goalw [int_def,real_one_def] "real (int 1) = (1::real)";
by (auto_tac (claset(),
simpset() addsimps [real_of_int,
preal_of_prat_add RS sym,pnat_two_eq,
@@ -80,7 +80,7 @@
qed "real_of_int_mult";
Addsimps [real_of_int_mult RS sym];
-Goal "real (int (Suc n)) = real (int n) + 1r";
+Goal "real (int (Suc n)) = real (int n) + (1::real)";
by (simp_tac (simpset() addsimps [real_of_int_one RS sym, zadd_int] @
zadd_ac) 1);
qed "real_of_int_Suc";
--- a/src/HOL/Real/RealOrd.ML Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Real/RealOrd.ML Mon Oct 08 15:23:20 2001 +0200
@@ -137,7 +137,7 @@
by (Asm_full_simp_tac 1);
qed "real_mult_less_zero";
-Goalw [real_one_def] "0 < 1r";
+Goalw [real_one_def] "0 < (1::real)";
by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2],
simpset() addsimps [real_of_preal_def]));
qed "real_zero_less_one";
@@ -230,7 +230,7 @@
Goal "EX (x::real). x < y";
by (rtac (real_add_zero_right RS subst) 1);
-by (res_inst_tac [("x","y + (- 1r)")] exI 1);
+by (res_inst_tac [("x","y + (- (1::real))")] exI 1);
by (auto_tac (claset() addSIs [real_add_less_mono2],
simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
qed "real_less_Ex";
@@ -264,31 +264,31 @@
An embedding of the naturals in the reals
----------------------------------------------------------------------------*)
-Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r";
+Goalw [real_of_posnat_def] "real_of_posnat 0 = (1::real)";
by (simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def,
symmetric real_one_def]) 1);
qed "real_of_posnat_one";
-Goalw [real_of_posnat_def] "real_of_posnat (Suc 0) = 1r + 1r";
+Goalw [real_of_posnat_def] "real_of_posnat (Suc 0) = (1::real) + (1::real)";
by (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_of_posnat_two";
Goalw [real_of_posnat_def]
- "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r";
+ "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)";
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 "real_of_posnat (n + 1) = real_of_posnat n + 1r";
-by (res_inst_tac [("x1","1r")] (real_add_right_cancel RS iffD1) 1);
+Goal "real_of_posnat (n + 1) = real_of_posnat n + (1::real)";
+by (res_inst_tac [("x1","(1::real)")] (real_add_right_cancel RS iffD1) 1);
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 "real_of_posnat (Suc n) = real_of_posnat n + 1r";
+Goal "real_of_posnat (Suc n) = real_of_posnat n + (1::real)";
by (stac (real_of_posnat_add_one RS sym) 1);
by (Simp_tac 1);
qed "real_of_posnat_Suc";
@@ -306,7 +306,7 @@
by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
qed "real_of_nat_zero";
-Goalw [real_of_nat_def] "real (Suc 0) = 1r";
+Goalw [real_of_nat_def] "real (Suc 0) = (1::real)";
by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
qed "real_of_nat_one";
Addsimps [real_of_nat_zero, real_of_nat_one];
@@ -319,7 +319,7 @@
Addsimps [real_of_nat_add];
(*Not for addsimps: often the LHS is used to represent a positive natural*)
-Goalw [real_of_nat_def] "real (Suc n) = real n + 1r";
+Goalw [real_of_nat_def] "real (Suc n) = real n + (1::real)";
by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1);
qed "real_of_nat_Suc";
@@ -475,20 +475,20 @@
simpset()));
qed "real_mult_less_mono'";
-Goal "1r <= x ==> 0 < x";
+Goal "(1::real) <= x ==> 0 < x";
by (rtac ccontr 1 THEN dtac real_leI 1);
by (dtac order_trans 1 THEN assume_tac 1);
by (auto_tac (claset() addDs [real_zero_less_one RSN (2,order_le_less_trans)],
simpset()));
qed "real_gt_zero";
-Goal "[| 1r < r; 1r <= x |] ==> x <= r * x";
+Goal "[| (1::real) < r; (1::real) <= x |] ==> x <= r * x";
by (dtac (real_gt_zero RS order_less_imp_le) 1);
by (auto_tac (claset() addSDs [real_mult_le_less_mono1],
simpset()));
qed "real_mult_self_le";
-Goal "[| 1r <= r; 1r <= x |] ==> x <= r * x";
+Goal "[| (1::real) <= r; (1::real) <= x |] ==> x <= r * x";
by (dtac order_le_imp_less_or_eq 1);
by (auto_tac (claset() addIs [real_mult_self_le], simpset()));
qed "real_mult_self_le2";
@@ -502,7 +502,7 @@
by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS
not_sym RS real_mult_inv_right]) 1);
by (ftac real_inverse_gt_zero 1);
-by (forw_inst_tac [("x","1r"),("z","inverse x")] real_mult_less_mono2 1);
+by (forw_inst_tac [("x","(1::real)"),("z","inverse 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);