# HG changeset patch # User wenzelm # Date 1002547400 -7200 # Node ID 883d559b0b8c2ecb881bd78392e5807c33f9bf5c # Parent deb8cac87063fed4acfb910e0e01f8f95544c4a2 sane numerals (stage 3): provide generic "1" on all number types; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HRealAbs.ML --- 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"; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HSeries.ML --- 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])); diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperBin.ML --- 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 **) diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperDef.ML --- 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]; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperDef.thy --- 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)})" diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperNat.ML --- 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]; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperNat.thy --- 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})" diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperOrd.ML --- 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(), diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperPow.ML --- 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"; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperPow.thy --- 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 diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/Lim.ML --- 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"; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/NatStar.ML --- 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])); diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/SEQ.ML --- 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); diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Integ/Bin.ML --- 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); diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Integ/IntDef.ML --- 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); diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Integ/IntDef.thy --- 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 == diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Integ/int_arith1.ML --- 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; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Real/RealBin.ML --- 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 **) diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Real/RealDef.ML --- 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(), diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Real/RealDef.thy --- 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). diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Real/RealInt.ML --- 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"; diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Real/RealOrd.ML --- 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);