# HG changeset patch # User paulson # Date 932743752 -7200 # Node ID 60b098bb8b8aab36b89bffd140e6f0f717114db8 # Parent a30e024791c60127926a53bad1d85f66e499c091 heavily revised by Jacques: coercions have alphabetic names; exponentiation is available, etc. diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/PNat.ML --- 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]; - diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/PNat.thy --- 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 diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/PRat.ML --- 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])); diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/PRat.thy --- 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 diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/PReal.ML --- 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]; diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/PReal.thy --- 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)})" diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/RComplete.ML --- 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"; diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/Real.ML --- 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' < 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' 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 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 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 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 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"; diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/Real.thy --- 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 + diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/RealAbs.ML --- 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 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]; + diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/RealDef.ML --- 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 ? 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); diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/RealDef.thy --- 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 diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/RealPow.ML --- /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]; + diff -r a30e024791c6 -r 60b098bb8b8a src/HOL/Real/RealPow.thy --- /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