# HG changeset patch # User paulson # Date 907258681 -7200 # Node ID a3ab526bb891f7519550d1c227f65c00c339ea82 # Parent 7fceb6eea475d52caad90ece33590981d1e98cda Revised version with Abelian group simprocs diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/PNat.ML --- a/src/HOL/Real/PNat.ML Tue Sep 29 18:13:05 1998 +0200 +++ b/src/HOL/Real/PNat.ML Thu Oct 01 18:18:01 1998 +0200 @@ -518,7 +518,7 @@ \ |] ==> f(i) <= (f(j)::pnat)"; by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD], simpset() addsimps [pnat_le_iff_Rep_pnat_le, - le_eq_less_or_eq])); + order_le_less])); qed "pnat_less_mono_imp_le_mono"; Goal "!!i j k::pnat. i<=j ==> i + k <= j + k"; diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/PReal.ML --- a/src/HOL/Real/PReal.ML Tue Sep 29 18:13:05 1998 +0200 +++ b/src/HOL/Real/PReal.ML Thu Oct 01 18:18:01 1998 +0200 @@ -157,28 +157,6 @@ (*** theorems for ordering ***) (* prove introduction and elimination rules for preal_less *) -Goalw [preal_less_def] - "R1 < (R2::preal) = (Rep_preal(R1) < Rep_preal(R2))"; -by (Fast_tac 1); -qed "preal_less_iff"; - -Goalw [preal_less_def] - "!! (R1::preal). R1 < R2 ==> (Rep_preal(R1) < Rep_preal(R2))"; -by (Fast_tac 1); -qed "preal_lessI"; - -Goalw [preal_less_def] - "R1 < (R2::preal) --> (Rep_preal(R1) < Rep_preal(R2))"; -by (Fast_tac 1); -qed "preal_lessE_lemma"; - -Goal "!!P. [| R1 < (R2::preal); \ -\ (Rep_preal(R1) < Rep_preal(R2)) ==> P |] \ -\ ==> P"; -by (dtac (preal_lessE_lemma RS mp) 1); -by Auto_tac; -qed "preal_lessE"; - (* A positive fraction not in a positive real is an upper bound *) (* Gleason p. 122 - Remark (1) *) @@ -806,10 +784,6 @@ by Auto_tac; qed "preal_less_or_eq_imp_le"; -Goal "(x <= (y::preal)) = (x < y | x=y)"; -by (REPEAT(ares_tac [iffI, preal_less_or_eq_imp_le, preal_le_imp_less_or_eq] 1)); -qed "preal_le_eq_less_or_eq"; - Goalw [preal_le_def] "w <= (w::preal)"; by (Simp_tac 1); qed "preal_le_refl"; @@ -1037,13 +1011,6 @@ simpset() addsimps [preal_add_commute])); qed "preal_add_le_mono1"; -Goal "!!k l::preal. [|i<=j; k<=l |] ==> i + k <= j + l"; -by (etac (preal_add_le_mono1 RS preal_le_trans) 1); -by (simp_tac (simpset() addsimps [preal_add_commute]) 1); -(*j moves to the end because it is free while k, l are bound*) -by (etac preal_add_le_mono1 1); -qed "preal_add_le_mono"; - Goal "!!(A::preal). A + C < B + C ==> A < B"; by (cut_facts_tac [preal_linear] 1); by (auto_tac (claset() addEs [preal_less_irrefl],simpset())); diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Tue Sep 29 18:13:05 1998 +0200 +++ b/src/HOL/Real/RComplete.ML Thu Oct 01 18:18:01 1998 +0200 @@ -31,12 +31,12 @@ \ 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 (auto_tac (claset(),simpset() addsimps [isLub_def,leastP_def,isUb_def])); +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())); + 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_preal_le_iff])); by (rtac preal_psup_leI2a 1); by (forw_inst_tac [("y","%#ya")] setleD 1 THEN assume_tac 1); by (forward_tac [real_ge_preal_preal_Ex] 1); @@ -46,73 +46,48 @@ 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])); -by (blast_tac (claset() addSDs [setleD] addSIs - [psup_le_ub1] addIs [real_preal_le_iff RS iffD1]) 1); +by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex], + simpset() addsimps [real_preal_le_iff])); +by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] + addIs [real_preal_le_iff RS iffD1]) 1); qed "posreals_complete"; (*------------------------------- Lemmas -------------------------------*) -Goal "! y : {z. ? x: P. z = x + %~xa + 1r} Int {x. 0r < x}. 0r < y"; +Goal "! y : {z. ? x: P. z = x + -xa + 1r} Int {x. 0r < x}. 0r < y"; by Auto_tac; qed "real_sup_lemma3"; -(* lemmas re-arranging the terms *) -Goal "(S <= Y + %~X + Z) = (S + X + %~Z <= Y)"; -by (Step_tac 1); -by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 1); -by (dres_inst_tac [("x","Z")] real_add_le_mono1 2); -by (auto_tac (claset(),simpset() addsimps [real_add_assoc, - real_add_minus,real_add_zero_right,real_add_minus_left])); -by (dres_inst_tac [("x","X")] real_add_le_mono1 1); -by (dres_inst_tac [("x","%~X")] real_add_le_mono1 2); -by (auto_tac (claset(),simpset() addsimps [real_add_assoc, - real_add_minus,real_add_zero_right,real_add_minus_left])); -by (auto_tac (claset(),simpset() addsimps [real_add_commute])); -qed "lemma_le_swap"; - -Goal "(xa <= S + X + %~Z) = (xa + %~X + Z <= S)"; -by (Step_tac 1); -by (dres_inst_tac [("x","Z")] real_add_le_mono1 1); -by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 2); -by (auto_tac (claset(),simpset() addsimps [real_add_assoc, - real_add_minus,real_add_zero_right,real_add_minus_left])); -by (dres_inst_tac [("x","%~X")] real_add_le_mono1 1); -by (dres_inst_tac [("x","X")] real_add_le_mono1 2); -by (auto_tac (claset(),simpset() addsimps [real_add_assoc, - real_add_minus,real_add_zero_right,real_add_minus_left])); -by (auto_tac (claset(),simpset() addsimps [real_add_commute])); +Goal "(xa <= S + X + -Z) = (xa + -X + Z <= (S::real))"; +by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ + real_add_ac) 1); qed "lemma_le_swap2"; -Goal "[| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r"; +Goal "[| 0r < x + -X + 1r; x < xa |] ==> 0r < xa + -X + 1r"; by (dtac real_add_less_mono 1); by (assume_tac 1); -by (dres_inst_tac [("C","%~x"),("A","0r + x")] real_add_less_mono2 1); +by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1); by (asm_full_simp_tac (simpset() addsimps [real_add_zero_right, real_add_assoc RS sym,real_add_minus_left,real_add_zero_left]) 1); by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); qed "lemma_real_complete1"; -Goal "!!x. [| x + %~X + 1r <= S; xa < x |] ==> xa + %~X + 1r <= S"; +Goal "!!x. [| x + -X + 1r <= S; xa < x |] ==> xa + -X + 1r <= S"; by (dtac real_less_imp_le 1); by (dtac real_add_le_mono 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); -by (dres_inst_tac [("x","%~x"),("q2.0","x + S")] real_add_left_le_mono1 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym, - real_add_minus_left,real_add_zero_left]) 1); qed "lemma_real_complete2"; -Goal "[| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**) +Goal "[| x + -X + 1r <= S; xa < x |] ==> xa <= S + X + -1r"; (**) by (rtac (lemma_le_swap2 RS iffD2) 1); by (etac lemma_real_complete2 1); by (assume_tac 1); qed "lemma_real_complete2a"; -Goal "[| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r"; +Goal "[| x + -X + 1r <= S; xa <= x |] ==> xa <= S + X + -1r"; by (rotate_tac 1 1); by (etac (real_le_imp_less_or_eq RS disjE) 1); by (blast_tac (claset() addIs [lemma_real_complete2a]) 1); @@ -126,20 +101,22 @@ \ EX Y. isUb (UNIV::real set) S Y \ \ |] ==> EX t. isLub (UNIV :: real set) S t"; by (Step_tac 1); -by (subgoal_tac "? u. u: {z. ? x: S. z = x + %~X + 1r} \ +by (subgoal_tac "? u. u: {z. ? x: S. z = x + -X + 1r} \ \ Int {x. 0r < x}" 1); -by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + %~X + 1r} \ -\ Int {x. 0r < x}) (Y + %~X + 1r)" 1); +by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + -X + 1r} \ +\ Int {x. 0r < x}) (Y + -X + 1r)" 1); by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1); by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, Step_tac]); -by (res_inst_tac [("x","t + X + %~1r")] exI 1); +by (res_inst_tac [("x","t + X + -1r")] exI 1); by (rtac isLubI2 1); by (rtac setgeI 2 THEN Step_tac 2); -by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + %~X + 1r} \ -\ Int {x. 0r < x}) (y + %~X + 1r)" 2); -by (dres_inst_tac [("y","(y + %~ X + 1r)")] isLub_le_isUb 2 +by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + -X + 1r} \ +\ Int {x. 0r < x}) (y + -X + 1r)" 2); +by (dres_inst_tac [("y","(y + - X + 1r)")] isLub_le_isUb 2 THEN assume_tac 2); -by (etac (lemma_le_swap RS subst) 2); +by (full_simp_tac + (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ + real_add_ac) 2); by (rtac (setleI RS isUbI) 1); by (Step_tac 1); by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1); @@ -154,27 +131,20 @@ by (rtac lemma_real_complete2b 1); by (etac real_less_imp_le 2); by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1); -by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)] - addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1); -by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)] - addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1); -by (auto_tac (claset(),simpset() addsimps [real_add_assoc RS sym, - real_add_minus,real_add_zero_left,real_zero_less_one])); +by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); +by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] + addIs [real_add_le_mono1]) 1); +by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] + addIs [real_add_le_mono1]) 1); +by (auto_tac (claset(), + simpset() addsimps [real_add_assoc RS sym, + real_zero_less_one])); qed "reals_complete"; (*---------------------------------------------------------------- Related property: Archimedean property of reals ----------------------------------------------------------------*) -Goal "(ALL m. x*%%#m + x <= t) = (ALL m. x*%%#m <= t + %~x)"; -by Auto_tac; -by (ALLGOALS(dres_inst_tac [("x","m")] spec)); -by (dres_inst_tac [("x","%~x")] real_add_le_mono1 1); -by (dres_inst_tac [("x","x")] real_add_le_mono1 2); -by (auto_tac (claset(),simpset() addsimps [real_add_assoc, - real_add_minus,real_add_minus_left,real_add_zero_right])); -qed "lemma_arch"; - Goal "0r < x ==> EX n. rinv(%%#n) < x"; by (stac real_nat_rinv_Ex_iff 1); by (EVERY1[rtac ccontr, Asm_full_simp_tac]); @@ -187,15 +157,15 @@ by (asm_full_simp_tac (simpset() addsimps [real_nat_Suc,real_add_mult_distrib2]) 1); by (blast_tac (claset() addIs [isLubD2]) 2); -by (asm_full_simp_tac (simpset() addsimps [lemma_arch]) 1); -by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + %~x)" 1); +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 (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); +by (dres_inst_tac [("y","t+-x")] isLub_le_isUb 1); +by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2); by (auto_tac (claset() addDs [real_le_less_trans, - (real_minus_zero_less_iff2 RS iffD2)], simpset() - addsimps [real_less_not_refl,real_add_assoc RS sym, - real_add_minus_left,real_add_zero_left])); + (real_minus_zero_less_iff2 RS iffD2)], + simpset() addsimps [real_less_not_refl,real_add_assoc RS sym])); qed "reals_Archimedean"; Goal "EX n. (x::real) < %%#n"; @@ -203,15 +173,17 @@ 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_nat_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); -by (auto_tac (claset(),simpset() addsimps [real_nat_less_zero, - real_not_refl2 RS not_sym,real_mult_assoc RS sym])); +by (auto_tac (claset(), + simpset() addsimps [real_nat_less_zero, + real_not_refl2 RS not_sym, + real_mult_assoc RS sym])); qed "reals_Archimedean2"; diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/ROOT.ML --- a/src/HOL/Real/ROOT.ML Tue Sep 29 18:13:05 1998 +0200 +++ b/src/HOL/Real/ROOT.ML Thu Oct 01 18:18:01 1998 +0200 @@ -11,5 +11,7 @@ writeln"Root file for HOL/Real"; set proof_timing; +time_use_thy "RealDef"; +use "simproc"; time_use_thy "RealAbs"; time_use_thy "RComplete"; diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/Real.ML --- a/src/HOL/Real/Real.ML Tue Sep 29 18:13:05 1998 +0200 +++ b/src/HOL/Real/Real.ML Thu Oct 01 18:18:01 1998 +0200 @@ -1,872 +1,12 @@ -(* Title : Real.ML - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : The reals +(* 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 *) -(*** Proving that realrel is an equivalence relation ***) -Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \ -\ ==> x1 + y3 = x3 + y1"; -by (res_inst_tac [("C","y2")] preal_add_right_cancel 1); -by (rotate_tac 1 1 THEN dtac sym 1); -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); -by (rtac (preal_add_left_commute RS subst) 1); -by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1); -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); -qed "preal_trans_lemma"; - -(** Natural deduction for realrel **) - -Goalw [realrel_def] - "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)"; -by (Blast_tac 1); -qed "realrel_iff"; - -Goalw [realrel_def] - "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel"; -by (Blast_tac 1); -qed "realrelI"; - -Goalw [realrel_def] - "p: realrel --> (EX x1 y1 x2 y2. \ -\ p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)"; -by (Blast_tac 1); -qed "realrelE_lemma"; - -val [major,minor] = goal thy - "[| p: realrel; \ -\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1 \ -\ |] ==> Q |] ==> Q"; -by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1); -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); -qed "realrelE"; - -AddSIs [realrelI]; -AddSEs [realrelE]; - -Goal "(x,x): realrel"; -by (stac surjective_pairing 1 THEN rtac (refl RS realrelI) 1); -qed "realrel_refl"; - -Goalw [equiv_def, refl_def, sym_def, trans_def] - "equiv {x::(preal*preal).True} realrel"; -by (fast_tac (claset() addSIs [realrel_refl] - addSEs [sym,preal_trans_lemma]) 1); -qed "equiv_realrel"; - -val equiv_realrel_iff = - [TrueI, TrueI] MRS - ([CollectI, CollectI] MRS - (equiv_realrel RS eq_equiv_class_iff)); - -Goalw [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real"; -by (Blast_tac 1); -qed "realrel_in_real"; - -Goal "inj_on Abs_real real"; -by (rtac inj_on_inverseI 1); -by (etac Abs_real_inverse 1); -qed "inj_on_Abs_real"; - -Addsimps [equiv_realrel_iff,inj_on_Abs_real RS inj_on_iff, - realrel_iff, realrel_in_real, Abs_real_inverse]; - -Addsimps [equiv_realrel RS eq_equiv_class_iff]; -val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class); - -Goal "inj(Rep_real)"; -by (rtac inj_inverseI 1); -by (rtac Rep_real_inverse 1); -qed "inj_Rep_real"; - -(** real_preal: the injection from preal to real **) -Goal "inj(real_preal)"; -by (rtac injI 1); -by (rewtac real_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); -by (rtac equiv_realrel 1); -by (Blast_tac 1); -by Safe_tac; -by (Asm_full_simp_tac 1); -qed "inj_real_preal"; - -val [prem] = goal thy - "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P"; -by (res_inst_tac [("x1","z")] - (rewrite_rule [real_def] Rep_real RS quotientE) 1); -by (dres_inst_tac [("f","Abs_real")] arg_cong 1); -by (res_inst_tac [("p","x")] PairE 1); -by (rtac prem 1); -by (asm_full_simp_tac (simpset() addsimps [Rep_real_inverse]) 1); -qed "eq_Abs_real"; - -(**** real_minus: additive inverse on real ****) - -Goalw [congruent_def] - "congruent realrel (%p. split (%x y. realrel^^{(y,x)}) p)"; -by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1); -qed "real_minus_congruent"; - -(*Resolve th against the corresponding facts for real_minus*) -val real_minus_ize = RSLIST [equiv_realrel, real_minus_congruent]; - -Goalw [real_minus_def] - "%~ (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})"; -by (res_inst_tac [("f","Abs_real")] arg_cong 1); -by (simp_tac (simpset() addsimps - [realrel_in_real RS Abs_real_inverse,real_minus_ize UN_equiv_class]) 1); -qed "real_minus"; - -Goal "%~ (%~ z) = z"; -by (res_inst_tac [("z","z")] eq_Abs_real 1); -by (asm_simp_tac (simpset() addsimps [real_minus]) 1); -qed "real_minus_minus"; - -Addsimps [real_minus_minus]; - -Goal "inj(real_minus)"; -by (rtac injI 1); -by (dres_inst_tac [("f","real_minus")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1); -qed "inj_real_minus"; - -Goalw [real_zero_def] "%~0r = 0r"; -by (simp_tac (simpset() addsimps [real_minus]) 1); -qed "real_minus_zero"; - -Addsimps [real_minus_zero]; - -Goal "(%~x = 0r) = (x = 0r)"; -by (res_inst_tac [("z","x")] eq_Abs_real 1); -by (auto_tac (claset(),simpset() addsimps [real_zero_def, - real_minus] @ preal_add_ac)); -qed "real_minus_zero_iff"; - -Addsimps [real_minus_zero_iff]; - -Goal "(%~x ~= 0r) = (x ~= 0r)"; -by Auto_tac; -qed "real_minus_not_zero_iff"; - -(*** Congruence property for addition ***) -Goalw [congruent2_def] - "congruent2 realrel (%p1 p2. \ -\ split (%x1 y1. split (%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"; -by Safe_tac; -by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1); -by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1); -by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); -by (asm_simp_tac (simpset() addsimps preal_add_ac) 1); -qed "real_add_congruent2"; - -(*Resolve th against the corresponding facts for real_add*) -val real_add_ize = RSLIST [equiv_realrel, real_add_congruent2]; - -Goalw [real_add_def] - "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \ -\ Abs_real(realrel^^{(x1+x2, y1+y2)})"; -by (asm_simp_tac - (simpset() addsimps [real_add_ize UN_equiv_class2]) 1); -qed "real_add"; - -Goal "(z::real) + w = w + z"; -by (res_inst_tac [("z","z")] eq_Abs_real 1); -by (res_inst_tac [("z","w")] eq_Abs_real 1); -by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1); -qed "real_add_commute"; - -Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)"; -by (res_inst_tac [("z","z1")] eq_Abs_real 1); -by (res_inst_tac [("z","z2")] eq_Abs_real 1); -by (res_inst_tac [("z","z3")] eq_Abs_real 1); -by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1); -qed "real_add_assoc"; - -(*For AC rewriting*) -Goal "(x::real)+(y+z)=y+(x+z)"; -by (rtac (real_add_commute RS trans) 1); -by (rtac (real_add_assoc RS trans) 1); -by (rtac (real_add_commute RS arg_cong) 1); -qed "real_add_left_commute"; - -(* 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"; -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"; - -Goal "z + 0r = z"; -by (simp_tac (simpset() addsimps [real_add_zero_left,real_add_commute]) 1); -qed "real_add_zero_right"; - -Goalw [real_zero_def] "z + %~z = 0r"; -by (res_inst_tac [("z","z")] eq_Abs_real 1); -by (asm_full_simp_tac (simpset() addsimps [real_minus, - real_add, preal_add_commute]) 1); -qed "real_add_minus"; - -Goal "%~z + z = 0r"; -by (simp_tac (simpset() addsimps - [real_add_commute,real_add_minus]) 1); -qed "real_add_minus_left"; - -Goal "? y. (x::real) + y = 0r"; -by (blast_tac (claset() addIs [real_add_minus]) 1); -qed "real_minus_ex"; - -Goal "?! y. (x::real) + y = 0r"; -by (auto_tac (claset() addIs [real_add_minus],simpset())); -by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_commute, - real_add_zero_right,real_add_zero_left]) 1); -qed "real_minus_ex1"; - -Goal "?! y. y + (x::real) = 0r"; -by (auto_tac (claset() addIs [real_add_minus_left],simpset())); -by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_commute, - real_add_zero_right,real_add_zero_left]) 1); -qed "real_minus_left_ex1"; - -Goal "x + y = 0r ==> x = %~y"; -by (cut_inst_tac [("z","y")] real_add_minus_left 1); -by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1); -by (Blast_tac 1); -qed "real_add_minus_eq_minus"; - -Goal "? y. 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 (Blast_tac 1); -qed "real_as_add_inverse_ex"; - -(* real_minus_add_distrib *) -Goal "%~(x + y) = %~x + %~y"; -by (res_inst_tac [("z","x")] eq_Abs_real 1); -by (res_inst_tac [("z","y")] eq_Abs_real 1); -by (auto_tac (claset(),simpset() addsimps [real_minus,real_add])); -qed "real_minus_add_eq"; - -val real_minus_add_distrib = real_minus_add_eq; - -Goal "((x::real) + y = x + z) = (y = z)"; -by (Step_tac 1); -by (dres_inst_tac [("f","%t.%~x + t")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_minus_left, - real_add_assoc RS sym,real_add_zero_left]) 1); -qed "real_add_left_cancel"; - -Goal "(y + (x::real)= z + x) = (y = z)"; -by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1); -qed "real_add_right_cancel"; - -(*** Congruence property for multiplication ***) -Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \ -\ x * x1 + y * y1 + (x * y2 + x2 * y) = \ -\ x * x2 + y * y2 + (x * y1 + x1 * y)"; -by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute, - preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1); -by (rtac (preal_mult_commute RS subst) 1); -by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1); -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc, - preal_add_mult_distrib2 RS sym]) 1); -by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1); -qed "real_mult_congruent2_lemma"; - -Goal - "congruent2 realrel (%p1 p2. \ -\ split (%x1 y1. split (%x2 y2. realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"; -by (rtac (equiv_realrel RS congruent2_commuteI) 1); -by Safe_tac; -by (rewtac split_def); -by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1); -by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma])); -qed "real_mult_congruent2"; - -(*Resolve th against the corresponding facts for real_mult*) -val real_mult_ize = RSLIST [equiv_realrel, real_mult_congruent2]; - -Goalw [real_mult_def] - "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) = \ -\ Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})"; -by (simp_tac (simpset() addsimps [real_mult_ize UN_equiv_class2]) 1); -qed "real_mult"; - -Goal "(z::real) * w = w * z"; -by (res_inst_tac [("z","z")] eq_Abs_real 1); -by (res_inst_tac [("z","w")] eq_Abs_real 1); -by (asm_simp_tac - (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1); -qed "real_mult_commute"; - -Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)"; -by (res_inst_tac [("z","z1")] eq_Abs_real 1); -by (res_inst_tac [("z","z2")] eq_Abs_real 1); -by (res_inst_tac [("z","z3")] eq_Abs_real 1); -by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @ - preal_add_ac @ preal_mult_ac) 1); -qed "real_mult_assoc"; - -qed_goal "real_mult_left_commute" thy - "(z1::real) * (z2 * z3) = z2 * (z1 * z3)" - (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1, - rtac (real_mult_commute RS arg_cong) 1]); - -(* real multiplication is an AC operator *) -val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute]; - -Goalw [real_one_def,pnat_one_def] "1r * z = z"; -by (res_inst_tac [("z","z")] eq_Abs_real 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult, - preal_add_mult_distrib2,preal_mult_1_right] - @ preal_mult_ac @ preal_add_ac) 1); -qed "real_mult_1"; - -Goal "z * 1r = z"; -by (simp_tac (simpset() addsimps [real_mult_commute, - real_mult_1]) 1); -qed "real_mult_1_right"; - -Goalw [real_zero_def,pnat_one_def] "0r * z = 0r"; -by (res_inst_tac [("z","z")] eq_Abs_real 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult, - preal_add_mult_distrib2,preal_mult_1_right] - @ preal_mult_ac @ preal_add_ac) 1); -qed "real_mult_0"; - -Goal "z * 0r = 0r"; -by (simp_tac (simpset() addsimps [real_mult_commute, - real_mult_0]) 1); -qed "real_mult_0_right"; - -Addsimps [real_mult_0_right,real_mult_0]; - -Goal "%~(x * y) = %~x * y"; -by (res_inst_tac [("z","x")] eq_Abs_real 1); -by (res_inst_tac [("z","y")] eq_Abs_real 1); -by (auto_tac (claset(),simpset() addsimps [real_minus,real_mult] - @ preal_mult_ac @ preal_add_ac)); -qed "real_minus_mult_eq1"; - -Goal "%~(x * y) = x * %~y"; -by (res_inst_tac [("z","x")] eq_Abs_real 1); -by (res_inst_tac [("z","y")] eq_Abs_real 1); -by (auto_tac (claset(),simpset() addsimps [real_minus,real_mult] - @ preal_mult_ac @ preal_add_ac)); -qed "real_minus_mult_eq2"; - -Goal "%~x*%~y = x*y"; -by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, - real_minus_mult_eq1 RS sym]) 1); -qed "real_minus_mult_cancel"; - -Addsimps [real_minus_mult_cancel]; - -Goal "%~x*y = x*%~y"; -by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, - real_minus_mult_eq1 RS sym]) 1); -qed "real_minus_mult_commute"; - -(*----------------------------------------------------------------------------- - - -----------------------------------------------------------------------------*) - -(** Lemmas **) - -qed_goal "real_add_assoc_cong" thy - "!!z. (z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" - (fn _ => [(asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1)]); - -qed_goal "real_add_assoc_swap" thy "(z::real) + (v + w) = v + (z + w)" - (fn _ => [(REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1))]); - -Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"; -by (res_inst_tac [("z","z1")] eq_Abs_real 1); -by (res_inst_tac [("z","z2")] eq_Abs_real 1); -by (res_inst_tac [("z","w")] eq_Abs_real 1); -by (asm_simp_tac - (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @ - preal_add_ac @ preal_mult_ac) 1); -qed "real_add_mult_distrib"; - -val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute; - -Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)"; -by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1); -qed "real_add_mult_distrib2"; - -val real_mult_simps = [real_mult_1, real_mult_1_right]; -Addsimps real_mult_simps; - -(*** one and zero are distinct ***) -Goalw [real_zero_def,real_one_def] "0r ~= 1r"; -by (auto_tac (claset(),simpset() addsimps - [preal_self_less_add_left RS preal_not_refl2])); -qed "real_zero_not_eq_one"; - -(*** existence of inverse ***) -(** lemma -- alternative definition for 0r **) -Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})"; -by (auto_tac (claset(),simpset() addsimps [preal_add_commute])); -qed "real_zero_iff"; - -Goalw [real_zero_def,real_one_def] - "!!(x::real). x ~= 0r ==> ? y. x*y = 1r"; -by (res_inst_tac [("z","x")] eq_Abs_real 1); -by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1); -by (auto_tac (claset() addSDs [preal_less_add_left_Ex], - 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 (auto_tac (claset(),simpset() addsimps [real_mult, - pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2, - preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right] - @ preal_add_ac @ preal_mult_ac)); -qed "real_mult_inv_right_ex"; - -Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r"; -by (asm_simp_tac (simpset() addsimps [real_mult_commute, - real_mult_inv_right_ex]) 1); -qed "real_mult_inv_left_ex"; - -Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r"; -by (forward_tac [real_mult_inv_left_ex] 1); -by (Step_tac 1); -by (rtac selectI2 1); -by Auto_tac; -qed "real_mult_inv_left"; - -Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r"; -by (auto_tac (claset() addIs [real_mult_commute RS subst], - simpset() addsimps [real_mult_inv_left])); -qed "real_mult_inv_right"; - -Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)"; -by Auto_tac; -by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); -qed "real_mult_left_cancel"; - -Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)"; -by (Step_tac 1); -by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); -qed "real_mult_right_cancel"; - -Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r"; -by (forward_tac [real_mult_inv_left_ex] 1); -by (etac exE 1); -by (rtac selectI2 1); -by (auto_tac (claset(),simpset() addsimps [real_mult_0, - real_zero_not_eq_one])); -qed "rinv_not_zero"; - -Addsimps [real_mult_inv_left,real_mult_inv_right]; - -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); -by (auto_tac (claset() addDs [rinv_not_zero],simpset())); -qed "real_rinv_rinv"; - -Goalw [rinv_def] "rinv(1r) = 1r"; -by (cut_facts_tac [real_zero_not_eq_one RS - not_sym RS real_mult_inv_left_ex] 1); -by (etac exE 1); -by (rtac selectI2 1); -by (auto_tac (claset(),simpset() addsimps - [real_zero_not_eq_one RS not_sym])); -qed "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 ***) -(* prove introduction and elimination rules for real_less *) - -Goalw [real_less_def] - "P < (Q::real) = (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \ -\ (x1,y1::preal):Rep_real(P) & \ -\ (x2,y2):Rep_real(Q))"; -by (Blast_tac 1); -qed "real_less_iff"; - -Goalw [real_less_def] - "[| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \ -\ (x2,y2):Rep_real(Q) |] ==> P < (Q::real)"; -by (Blast_tac 1); -qed "real_lessI"; - -Goalw [real_less_def] - "!!P. [| R1 < (R2::real); \ -\ !!x1 x2 y1 y2. x1 + y2 < x2 + y1 ==> P; \ -\ !!x1 y1. (x1,y1::preal):Rep_real(R1) ==> P; \ -\ !!x2 y2. (x2,y2::preal):Rep_real(R2) ==> P |] \ -\ ==> P"; -by Auto_tac; -qed "real_lessE"; - -Goalw [real_less_def] - "R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \ -\ (x1,y1::preal):Rep_real(R1) & \ -\ (x2,y2):Rep_real(R2))"; -by (Blast_tac 1); -qed "real_lessD"; - -(* 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); -qed "preal_lemma_eq_rev_sum"; - -Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1"; -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); -qed "preal_add_left_commute_cancel"; - -Goal - "!!(x::preal). [| x + y2a = x2a + y; \ -\ x + y2b = x2b + y |] \ -\ ==> x2a + y2b = x2b + y2a"; -by (dtac preal_lemma_eq_rev_sum 1); -by (assume_tac 1); -by (thin_tac "x + y2b = x2b + y" 1); -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); -by (dtac preal_add_left_commute_cancel 1); -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); -qed "preal_lemma_for_not_refl"; - -Goal "~ (R::real) < R"; -by (res_inst_tac [("z","R")] eq_Abs_real 1); -by (auto_tac (claset(),simpset() addsimps [real_less_def])); -by (dtac preal_lemma_for_not_refl 1); -by (assume_tac 1 THEN rotate_tac 2 1); -by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl])); -qed "real_less_not_refl"; - -(*** y < y ==> P ***) -bind_thm("real_less_irrefl",real_less_not_refl RS notE); - -Goal "!!(x::real). x < y ==> x ~= y"; -by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); -qed "real_not_refl2"; - -(* lemma re-arranging and eliminating terms *) -Goal "!! (a::preal). [| a + b = c + d; \ -\ x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \ -\ ==> x2b + y2e < x2e + y2b"; -by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); -by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1); -by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); -qed "preal_lemma_trans"; - -(** heavy re-writing involved*) -Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3"; -by (res_inst_tac [("z","R1")] eq_Abs_real 1); -by (res_inst_tac [("z","R2")] eq_Abs_real 1); -by (res_inst_tac [("z","R3")] eq_Abs_real 1); -by (auto_tac (claset(),simpset() addsimps [real_less_def])); -by (REPEAT(rtac exI 1)); -by (EVERY[rtac conjI 1, rtac conjI 2]); -by (REPEAT(Blast_tac 2)); -by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1); -by (blast_tac (claset() addDs [preal_add_less_mono] - addIs [preal_lemma_trans]) 1); -qed "real_less_trans"; - -Goal "!! (R1::real). [| R1 < R2; R2 < R1 |] ==> P"; -by (dtac real_less_trans 1 THEN assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1); -qed "real_less_asym"; - -(****)(****)(****)(****)(****)(****)(****)(****)(****)(****) - (****** Map and more real_less ******) -(*** mapping from preal into real ***) -Goalw [real_preal_def] - "%#((z1::preal) + z2) = %#z1 + %#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"; - -Goalw [real_preal_def] - "%#((z1::preal) * z2) = %#z1* %#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"; - -Goalw [real_preal_def] - "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m"; -by (auto_tac (claset() addSDs [preal_less_add_left_Ex], - simpset() addsimps preal_add_ac)); -qed "real_preal_ExI"; - -Goalw [real_preal_def] - "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#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"; - -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"; - -(*** Gleason prop 9-4.4 p 127 ***) -Goalw [real_preal_def,real_zero_def] - "? m. (x::real) = %#m | x = 0r | x = %~(%#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"; - -Goal "!!P. [| !!m. x = %#m ==> P; \ -\ x = 0r ==> P; \ -\ !!m. x = %~(%#m) ==> P |] ==> P"; -by (cut_inst_tac [("x","x")] real_preal_trichotomy 1); -by Auto_tac; -qed "real_preal_trichotomyE"; - -Goalw [real_preal_def] "%#m1 < %#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"; - -Goal "m1 < m2 ==> %#m1 < %#m2"; -by (dtac preal_less_add_left_Ex 1); -by (auto_tac (claset(),simpset() addsimps [real_preal_add, - real_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"; - -Goal "(%#m1 < %#m2) = (m1 < m2)"; -by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1); -qed "real_preal_less_iff1"; - -Addsimps [real_preal_less_iff1]; - -Goal "%~ %#m < %#m"; -by (auto_tac (claset(),simpset() addsimps - [real_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"; - -Goalw [real_zero_def] "%~ %#m < 0r"; -by (auto_tac (claset(),simpset() addsimps - [real_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"; - -Goal "~ 0r < %~ %#m"; -by (cut_facts_tac [real_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"; - -Goalw [real_zero_def] " 0r < %#m"; -by (auto_tac (claset(),simpset() addsimps - [real_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"; - -Goal "~ %#m < 0r"; -by (cut_facts_tac [real_preal_zero_less] 1); -by (blast_tac (claset() addDs [real_less_trans] - addEs [real_less_irrefl]) 1); -qed "real_preal_not_less_zero"; - -Goal "0r < %~ %~ %#m"; -by (simp_tac (simpset() addsimps - [real_preal_zero_less]) 1); -qed "real_minus_minus_zero_less"; - -(* another lemma *) -Goalw [real_zero_def] " 0r < %#m + %#m1"; -by (auto_tac (claset(),simpset() addsimps - [real_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"; - -Goal "%~ %#m < %#m1"; -by (auto_tac (claset(),simpset() addsimps - [real_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"; - -Goal "~ %#m < %~ %#m1"; -by (cut_facts_tac [real_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"; - -Goal "%~ %#m1 < %~ %#m2 ==> %#m2 < %#m1"; -by (auto_tac (claset(),simpset() addsimps - [real_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"; - -Goal "%#m1 < %#m2 ==> %~ %#m2 < %~ %#m1"; -by (auto_tac (claset(),simpset() addsimps - [real_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"; - -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"; - -Addsimps [real_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 (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])); -qed "real_linear"; - -Goal "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; \ -\ R2 < R1 ==> P |] ==> P"; -by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1); -by Auto_tac; -qed "real_linear_less2"; - -(*** Properties of <= ***) - -Goalw [real_le_def] "~(w < z) ==> z <= (w::real)"; -by (assume_tac 1); -qed "real_leI"; - -Goalw [real_le_def] "z<=w ==> ~(w<(z::real))"; -by (assume_tac 1); -qed "real_leD"; - -val real_leE = make_elim real_leD; - -Goal "(~(w < z)) = (z <= (w::real))"; -by (blast_tac (claset() addSIs [real_leI,real_leD]) 1); -qed "real_less_le_iff"; - -Goalw [real_le_def] "~ z <= w ==> w<(z::real)"; -by (Blast_tac 1); -qed "not_real_leE"; - -Goalw [real_le_def] "z < w ==> z <= (w::real)"; -by (blast_tac (claset() addEs [real_less_asym]) 1); -qed "real_less_imp_le"; - -Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y"; -by (cut_facts_tac [real_linear] 1); -by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); -qed "real_le_imp_less_or_eq"; - -Goalw [real_le_def] "z z <=(w::real)"; -by (cut_facts_tac [real_linear] 1); -by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); -qed "real_less_or_eq_imp_le"; - -Goal "(x <= (y::real)) = (x < y | x=y)"; -by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1)); -qed "real_le_eq_less_or_eq"; - -Goal "w <= (w::real)"; -by (simp_tac (simpset() addsimps [real_le_eq_less_or_eq]) 1); -qed "real_le_refl"; - -val prems = goal Real.thy "!!i. [| i <= j; j < k |] ==> i < (k::real)"; -by (dtac real_le_imp_less_or_eq 1); -by (blast_tac (claset() addIs [real_less_trans]) 1); -qed "real_le_less_trans"; - -Goal "!! (i::real). [| i < j; j <= k |] ==> i < k"; -by (dtac real_le_imp_less_or_eq 1); -by (blast_tac (claset() addIs [real_less_trans]) 1); -qed "real_less_le_trans"; - -Goal "[| i <= j; j <= k |] ==> i <= (k::real)"; -by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, - rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]); -qed "real_le_trans"; - -Goal "[| z <= w; w <= z |] ==> z = (w::real)"; -by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, - fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]); -qed "real_le_anti_sym"; - -Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)"; -by (rtac not_real_leE 1); -by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1); -qed "not_less_not_eq_real_less"; - -Goal "(0r < %~R) = (R < 0r)"; -by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); -by (auto_tac (claset(),simpset() addsimps [real_preal_not_minus_gt_zero, - real_preal_not_less_zero,real_preal_zero_less, - real_preal_minus_less_zero])); -qed "real_minus_zero_less_iff"; - -Addsimps [real_minus_zero_less_iff]; - -Goal "(%~R < 0r) = (0r < R)"; -by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); -by (auto_tac (claset(),simpset() addsimps [real_preal_not_minus_gt_zero, - real_preal_not_less_zero,real_preal_zero_less, - real_preal_minus_less_zero])); -qed "real_minus_zero_less_iff2"; (** lemma **) Goal "(0r < x) = (? y. x = %#y)"; @@ -896,78 +36,7 @@ by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1); qed "real_less_all_real2"; -(**** Derive alternative definition for real_less ****) -(** lemma **) -Goal "!!(R::real). ? A. S + A = R"; -by (res_inst_tac [("x","%~S + R")] exI 1); -by (simp_tac (simpset() addsimps [real_add_minus, - real_add_zero_right] @ real_add_ac) 1); -qed "real_lemma_add_left_ex"; - -Goal "!!(R::real). R < S ==> ? 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 (auto_tac (claset() addSDs [preal_le_anti_sym] addSDs [preal_less_add_left_Ex], - simpset() addsimps [preal_less_le_iff,real_preal_add,real_minus_add_eq, - real_preal_minus_less_zero,real_less_not_refl,real_minus_ex,real_add_assoc, - real_preal_zero_less,real_preal_minus_less_all,real_add_minus_left, - real_preal_not_less_zero,real_add_zero_left,real_lemma_add_left_ex])); -qed "real_less_add_left_Ex"; - -Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S"; -by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); -by (ALLGOALS(res_inst_tac [("x","S")] real_preal_trichotomyE)); -by (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,real_less_not_refl, - real_preal_not_minus_gt_zero,real_add_zero_left,real_minus_add_eq])); -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); -by (auto_tac (claset(),simpset() addsimps [real_preal_zero_less, - real_preal_sum_zero_less,real_add_minus_left,real_add_assoc, - real_add_minus,real_add_zero_right])); -by (simp_tac (simpset() addsimps [real_add_assoc RS sym, - real_add_minus_left,real_add_zero_left]) 1); -qed "real_less_add_positive_left_Ex"; - -(* lemmas *) -(** change naff name(s)! **) -Goal "(W < S) ==> (0r < S + %~W)"; -by (dtac real_less_add_positive_left_Ex 1); -by (auto_tac (claset(),simpset() addsimps [real_add_minus, - real_add_zero_right] @ real_add_ac)); -qed "real_less_sum_gt_zero"; - -Goal "!!S. T = S + W ==> S = T + %~W"; -by (asm_simp_tac (simpset() addsimps [real_add_minus, real_add_zero_right] - @ real_add_ac) 1); -qed "real_lemma_change_eq_subj"; - -(* FIXME: long! *) -Goal "(0r < S + %~W) ==> (W < S)"; -by (rtac ccontr 1); -by (dtac (real_leI RS real_le_imp_less_or_eq) 1); -by (auto_tac (claset(), - simpset() addsimps [real_less_not_refl,real_add_minus])); -by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]); -by (asm_full_simp_tac (simpset() addsimps [real_add_zero_left]) 1); -by (dtac real_lemma_change_eq_subj 1); -by (auto_tac (claset(),simpset() addsimps [real_minus_minus])); -by (dtac real_less_sum_gt_zero 1); -by (asm_full_simp_tac (simpset() addsimps [real_minus_add_eq] @ real_add_ac) 1); -by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]); -by (auto_tac (claset() addEs [real_less_asym], - simpset() addsimps [real_add_minus,real_add_zero_right])); -qed "real_sum_gt_zero_less"; - -Goal "(0r < S + %~W) = (W < S)"; -by (blast_tac (claset() addIs [real_less_sum_gt_zero, - real_sum_gt_zero_less]) 1); -qed "real_less_sum_gt_0_iff"; - -Goal "((x::real) < y) = (%~y < %~x)"; +Goal "((x::real) < y) = (-y < -x)"; by (rtac (real_less_sum_gt_0_iff RS subst) 1); by (res_inst_tac [("W1","x")] (real_less_sum_gt_0_iff RS subst) 1); by (simp_tac (simpset() addsimps [real_add_commute]) 1); @@ -975,42 +44,42 @@ Goal "[| R + L = S; 0r < L |] ==> R < S"; by (rtac (real_less_sum_gt_0_iff RS iffD1) 1); -by (auto_tac (claset(),simpset() addsimps [ - real_add_minus,real_add_zero_right] @ real_add_ac)); +by (auto_tac (claset(), simpset() addsimps real_add_ac)); qed "real_lemma_add_positive_imp_less"; Goal "!!(R::real). ? T. 0r < T & R + T = S ==> R < S"; by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1); qed "real_ex_add_positive_left_less"; -(*** alternative definition for real_less ***) -Goal "!!(R::real). (? T. 0r < T & R + T = S) = (R < S)"; +(*Alternative definition for real_less. NOT for rewriting*) +Goal "!!(R::real). (R < S) = (? T. 0r < T & R + T = S)"; by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex, - real_ex_add_positive_left_less]) 1); -qed "real_less_iffdef"; + real_ex_add_positive_left_less]) 1); +qed "real_less_iff_add"; -Goal "(0r < x) = (%~x < x)"; +Goal "(0r < x) = (-x < x)"; by Safe_tac; by (rtac ccontr 2 THEN forward_tac [real_leI RS real_le_imp_less_or_eq] 2); by (Step_tac 2); by (dtac (real_minus_zero_less_iff RS iffD2) 2); 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])); +by (auto_tac (claset(), + simpset() addsimps + [real_gt_zero_preal_Ex,real_preal_minus_less_self])); qed "real_gt_zero_iff"; -Goal "(x < 0r) = (x < %~x)"; +Goal "(x < 0r) = (x < -x)"; by (rtac (real_minus_zero_less_iff RS subst) 1); by (stac real_gt_zero_iff 1); by (Full_simp_tac 1); qed "real_lt_zero_iff"; -Goalw [real_le_def] "(0r <= x) = (%~x <= x)"; +Goalw [real_le_def] "(0r <= x) = (-x <= x)"; by (auto_tac (claset(),simpset() addsimps [real_lt_zero_iff RS sym])); qed "real_ge_zero_iff"; -Goalw [real_le_def] "(x <= 0r) = (x <= %~x)"; +Goalw [real_le_def] "(x <= 0r) = (x <= -x)"; by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym])); qed "real_le_zero_iff"; @@ -1035,8 +104,8 @@ Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x * y"; by (REPEAT(dtac real_le_imp_less_or_eq 1)); -by (auto_tac (claset() addIs [real_mult_order, - real_less_imp_le],simpset() addsimps [real_le_refl])); +by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le], + simpset())); qed "real_le_mult_order"; Goal "!!(x::real). [| x <= 0r; y <= 0r |] ==> 0r <= x * y"; @@ -1125,93 +194,89 @@ by (Blast_tac 1); qed "posreal_complete"; -(*------------------------------------------------------------------ + + +(*** Monotonicity results ***) + +Goal "(v+z < w+z) = (v < (w::real))"; +by (Simp_tac 1); +qed "real_add_right_cancel_less"; - ------------------------------------------------------------------*) +Goal "(z+v < z+w) = (v < (w::real))"; +by (Simp_tac 1); +qed "real_add_left_cancel_less"; + +Addsimps [real_add_right_cancel_less, real_add_left_cancel_less]; + +Goal "(v+z <= w+z) = (v <= (w::real))"; +by (Simp_tac 1); +qed "real_add_right_cancel_le"; -Goal "!!(A::real). A < B ==> A + C < B + C"; -by (dtac (real_less_iffdef RS iffD2) 1); -by (rtac (real_less_iffdef RS iffD1) 1); -by (REPEAT(Step_tac 1)); -by (full_simp_tac (simpset() addsimps real_add_ac) 1); -qed "real_add_less_mono1"; +Goal "(z+v <= z+w) = (v <= (w::real))"; +by (Simp_tac 1); +qed "real_add_left_cancel_le"; + +Addsimps [real_add_right_cancel_le, real_add_left_cancel_le]; + +(*"v<=w ==> v+z <= w+z"*) +bind_thm ("real_add_less_mono1", real_add_right_cancel_less RS iffD2); + +(*"v<=w ==> v+z <= w+z"*) +bind_thm ("real_add_le_mono1", real_add_right_cancel_le RS iffD2); + +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"; + Goal "!!(A::real). A < B ==> C + A < C + B"; -by (auto_tac (claset() addIs [real_add_less_mono1], - simpset() addsimps [real_add_commute])); +by (Simp_tac 1); qed "real_add_less_mono2"; Goal "!!(A::real). A + C < B + C ==> A < B"; -by (dres_inst_tac [("C","%~C")] real_add_less_mono1 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc, - real_add_minus,real_add_zero_right]) 1); +by (Full_simp_tac 1); qed "real_less_add_right_cancel"; Goal "!!(A::real). C + A < C + B ==> A < B"; -by (dres_inst_tac [("C","%~C")] real_add_less_mono2 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym, - real_add_minus_left,real_add_zero_left]) 1); +by (Full_simp_tac 1); qed "real_less_add_left_cancel"; Goal "[| 0r < x; 0r < y |] ==> 0r < x + y"; -by (REPEAT(dtac (real_gt_zero_preal_Ex RS iffD1) 1)); -by (rtac (real_gt_zero_preal_Ex RS iffD2) 1); -by (Step_tac 1); -by (res_inst_tac [("x","y + ya")] exI 1); -by (full_simp_tac (simpset() addsimps [real_preal_add]) 1); +be real_less_trans 1; +bd real_add_less_mono2 1; +by (Full_simp_tac 1); qed "real_add_order"; Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x + y"; by (REPEAT(dtac real_le_imp_less_or_eq 1)); -by (auto_tac (claset() addIs [real_add_order, - real_less_imp_le],simpset() addsimps [real_add_zero_left, - real_add_zero_right,real_le_refl])); +by (auto_tac (claset() addIs [real_add_order, real_less_imp_le], + simpset())); qed "real_le_add_order"; -Goal - "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)"; -by (dtac (real_less_iffdef RS iffD2) 1); -by (dtac (real_less_iffdef RS iffD2) 1); -by (rtac (real_less_iffdef RS iffD1) 1); -by Auto_tac; -by (res_inst_tac [("x","T + Ta")] exI 1); -by (auto_tac (claset(),simpset() addsimps [real_add_order] @ real_add_ac)); +Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)"; +bd real_add_less_mono1 1; +be real_less_trans 1; +be real_add_less_mono2 1; qed "real_add_less_mono"; -Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x + y"; -by (REPEAT(dtac real_le_imp_less_or_eq 1)); -by (auto_tac (claset() addIs [real_add_order, - real_less_imp_le],simpset() addsimps [real_add_zero_left, - real_add_zero_right,real_le_refl])); -qed "real_le_add_order"; - Goal "!!(q1::real). q1 <= q2 ==> x + q1 <= x + q2"; -by (dtac real_le_imp_less_or_eq 1); -by (Step_tac 1); -by (auto_tac (claset() addSIs [real_le_refl, - real_less_imp_le,real_add_less_mono1], - simpset() addsimps [real_add_commute])); +by (Simp_tac 1); qed "real_add_left_le_mono1"; -Goal "!!(q1::real). q1 <= q2 ==> q1 + x <= q2 + x"; -by (auto_tac (claset() addDs [real_add_left_le_mono1], - simpset() addsimps [real_add_commute])); -qed "real_add_le_mono1"; - -Goal "!!k l::real. [|i<=j; k<=l |] ==> i + k <= j + l"; -by (etac (real_add_le_mono1 RS real_le_trans) 1); -by (simp_tac (simpset() addsimps [real_add_commute]) 1); -(*j moves to the end because it is free while k, l are bound*) -by (etac real_add_le_mono1 1); +Goal "[|i<=j; k<=l |] ==> i + k <= j + (l::real)"; +bd real_add_le_mono1 1; +be real_le_trans 1; +by (Simp_tac 1); qed "real_add_le_mono"; Goal "EX (x::real). x < y"; by (rtac (real_add_zero_right RS subst) 1); -by (res_inst_tac [("x","y + %~1r")] exI 1); +by (res_inst_tac [("x","y + -1r")] exI 1); by (auto_tac (claset() addSIs [real_add_less_mono2], - simpset() addsimps [real_minus_zero_less_iff2, - real_zero_less_one])); + simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one])); qed "real_less_Ex"; + (*--------------------------------------------------------------------------------- An embedding of the naturals in the reals ---------------------------------------------------------------------------------*) @@ -1267,13 +332,9 @@ Goal "1r <= %%#n"; by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1); by (induct_tac "n" 1); -by (auto_tac (claset(),simpset () - addsimps [real_nat_Suc,real_le_refl,real_nat_one])); -by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1); -by (rtac real_add_le_mono 1); -by (auto_tac (claset(),simpset () - addsimps [real_le_refl,real_nat_less_zero, - real_less_imp_le,real_add_zero_left])); +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"; @@ -1318,8 +379,7 @@ Goal "x < x + 1r"; by (rtac (real_less_sum_gt_0_iff RS iffD1) 1); by (full_simp_tac (simpset() addsimps [real_zero_less_one, - real_add_assoc,real_add_minus,real_add_zero_right, - real_add_left_commute]) 1); + real_add_assoc, real_add_left_commute]) 1); qed "real_self_less_add_one"; Goal "1r < 1r + 1r"; @@ -1328,7 +388,7 @@ Goal "0r < 1r + 1r"; by (rtac ([real_zero_less_one, - real_one_less_two] MRS real_less_trans) 1); + real_one_less_two] MRS real_less_trans) 1); qed "real_zero_less_two"; Goal "1r + 1r ~= 0r"; @@ -1358,7 +418,8 @@ Goal "!!(x::real). [| 0r x z*x<=z*y"; by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1); -by (auto_tac (claset() addIs [real_mult_le_less_mono2,real_le_refl],simpset())); +by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset())); qed "real_mult_le_le_mono1"; Goal "!!(x::real). x < y ==> x < (x + y)*rinv(1r + 1r)"; @@ -1402,7 +463,7 @@ qed "real_less_half_sum"; Goal "!!(x::real). x < y ==> (x + y)*rinv(1r + 1r) < y"; -by (dres_inst_tac [("C","y")] real_add_less_mono1 1); +by (dtac real_add_less_mono1 1); by (dtac (real_add_self RS subst) 1); by (dtac (real_zero_less_two RS real_rinv_gt_zero RS real_mult_less_mono1) 1); @@ -1419,7 +480,8 @@ RS real_mult_less_mono1) 1); by (dres_inst_tac [("n2","n")] (real_nat_less_zero RS real_rinv_gt_zero RS real_mult_less_mono1) 2); -by (auto_tac (claset(),simpset() addsimps [(real_nat_less_zero RS +by (auto_tac (claset(), + simpset() addsimps [(real_nat_less_zero RS real_not_refl2 RS not_sym),real_mult_assoc])); qed "real_nat_rinv_Ex_iff"; @@ -1435,17 +497,20 @@ 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, +by (auto_tac (claset(), + simpset() addsimps [real_nat_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 real_mult_less_cancel2) 3); -by (auto_tac (claset(),simpset() addsimps [real_nat_less_zero, +by (auto_tac (claset(), + simpset() addsimps [real_nat_less_zero, real_not_refl2 RS not_sym,real_mult_assoc RS sym])); qed "real_nat_less_rinv_iff"; Goal "0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)"; -by (auto_tac (claset(),simpset() addsimps [real_rinv_rinv, +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"; @@ -1458,3 +523,5 @@ qed "real_ubD"; *) + + diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/Real.thy --- a/src/HOL/Real/Real.thy Tue Sep 29 18:13:05 1998 +0200 +++ b/src/HOL/Real/Real.thy Thu Oct 01 18:18:01 1998 +0200 @@ -1,61 +1,14 @@ -(* Title : Real.thy - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : The reals -*) - -Real = PReal + - -constdefs - realrel :: "((preal * preal) * (preal * preal)) set" - "realrel == {p. ? x1 y1 x2 y2. p=((x1::preal,y1),(x2,y2)) & x1+y2 = x2+y1}" - -typedef real = "{x::(preal*preal).True}/realrel" (Equiv.quotient_def) - - -instance - real :: {ord,plus,times} - -consts - - "0r" :: real ("0r") - "1r" :: real ("1r") - -defs - - real_zero_def "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})" - real_one_def "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})" - -constdefs +(* Title: Real/Real.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge - real_preal :: preal => real ("%#_" [80] 80) - "%# m == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})" - - real_minus :: real => real ("%~ _" [80] 80) - "%~ R == Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)" - - rinv :: real => real - "rinv(R) == (@S. R ~= 0r & S*R = 1r)" - - real_nat :: nat => real ("%%# _" [80] 80) - "%%# n == %#(@#($#(*# n)))" - -defs +Type "real" is a linear order +*) - real_add_def - "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). - split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)" - - real_mult_def - "P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). - split(%x1 y1. split(%x2 y2. realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)" +Real = RealDef + - real_less_def - "P < (Q::real) == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & - (x1,y1::preal):Rep_real(P) & - (x2,y2):Rep_real(Q)" - - real_le_def - "P <= (Q::real) == ~(Q < P)" +instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le) +instance real :: linorder (real_le_linear) end diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/RealAbs.ML --- a/src/HOL/Real/RealAbs.ML Tue Sep 29 18:13:05 1998 +0200 +++ b/src/HOL/Real/RealAbs.ML Thu Oct 01 18:18:01 1998 +0200 @@ -4,13 +4,11 @@ Description : Absolute value function for the reals *) -open RealAbs; - (*---------------------------------------------------------------------------- Properties of the absolute value function over the reals (adapted version of previously proved theorems about abs) ----------------------------------------------------------------------------*) -Goalw [rabs_def] "rabs r = (if 0r<=r then r else %~r)"; +Goalw [rabs_def] "rabs r = (if 0r<=r then r else -r)"; by Auto_tac; qed "rabs_iff"; @@ -20,7 +18,7 @@ Addsimps [rabs_zero]; -Goalw [rabs_def] "rabs 0r = %~0r"; +Goalw [rabs_def] "rabs 0r = -0r"; by (stac real_minus_zero 1); by (rtac if_cancel 1); qed "rabs_minus_zero"; @@ -33,19 +31,19 @@ by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1); qed "rabs_eqI2"; -val [prem] = goalw thy [rabs_def,real_le_def] "x<0r ==> rabs x = %~x"; +val [prem] = goalw thy [rabs_def,real_le_def] "x<0r ==> rabs x = -x"; by (simp_tac (simpset() addsimps [prem,if_not_P]) 1); qed "rabs_minus_eqI2"; -Goal "x<=0r ==> rabs x = %~x"; +Goal "x<=0r ==> rabs x = -x"; by (dtac real_le_imp_less_or_eq 1); by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1); qed "rabs_minus_eqI1"; Goalw [rabs_def,real_le_def] "0r<= rabs x"; -by (full_simp_tac (simpset() setloop (split_tac [expand_if])) 1); +by (Full_simp_tac 1); by (blast_tac (claset() addDs [real_minus_zero_less_iff RS iffD2, - real_less_asym]) 1); + real_less_asym]) 1); qed "rabs_ge_zero"; Goal "rabs(rabs x)=rabs x"; @@ -54,29 +52,27 @@ qed "rabs_idempotent"; Goalw [rabs_def] "(x=0r) = (rabs x = 0r)"; -by (full_simp_tac (simpset() setloop (split_tac [expand_if])) 1); +by (Full_simp_tac 1); qed "rabs_zero_iff"; Goal "(x ~= 0r) = (rabs x ~= 0r)"; -by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym] - setloop (split_tac [expand_if])) 1); +by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym]) 1); qed "rabs_not_zero_iff"; Goalw [rabs_def] "x<=rabs x"; -by (full_simp_tac (simpset() addsimps [real_le_refl] setloop (split_tac [expand_if])) 1); +by (Full_simp_tac 1); by (auto_tac (claset() addDs [not_real_leE RS real_less_imp_le], - simpset() addsimps [real_le_zero_iff])); + simpset() addsimps [real_le_zero_iff])); qed "rabs_ge_self"; -Goalw [rabs_def] "%~x<=rabs x"; -by (full_simp_tac (simpset() addsimps [real_le_refl, - real_ge_zero_iff] setloop (split_tac [expand_if])) 1); +Goalw [rabs_def] "-x<=rabs x"; +by (full_simp_tac (simpset() addsimps [real_ge_zero_iff]) 1); qed "rabs_ge_minus_self"; (* case splits nightmare *) Goalw [rabs_def] "rabs(x*y) = (rabs x)*(rabs y)"; by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1, - real_minus_mult_commute,real_minus_mult_eq2] setloop (split_tac [expand_if]))); + real_minus_mult_commute,real_minus_mult_eq2])); by (blast_tac (claset() addDs [real_le_mult_order]) 1); by (auto_tac (claset() addSDs [not_real_leE],simpset())); by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]); @@ -88,7 +84,7 @@ Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))"; by (auto_tac (claset(),simpset() addsimps [real_minus_rinv] - setloop (split_tac [expand_if]))); + )); by (ALLGOALS(dtac not_real_leE)); by (etac real_less_asym 1); by (blast_tac (claset() addDs [real_le_imp_less_or_eq, @@ -108,28 +104,30 @@ Goal "rabs(x+y) <= rabs x + rabs y"; by (EVERY1 [res_inst_tac [("Q1","0r<=x+y")] (expand_if RS ssubst), rtac conjI]); -by (asm_simp_tac (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1); -by (asm_simp_tac (simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono, - rabs_ge_minus_self,real_minus_add_eq]) 1); +by (asm_simp_tac + (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1); +by (asm_simp_tac + (simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono, + rabs_ge_minus_self]) 1); qed "rabs_triangle_ineq"; Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)"; by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); by (blast_tac (claset() addSIs [(rabs_triangle_ineq RS real_le_trans), - real_add_left_le_mono1,real_le_refl]) 1); + real_add_left_le_mono1]) 1); qed "rabs_triangle_ineq_four"; -Goalw [rabs_def] "rabs(%~x)=rabs(x)"; +Goalw [rabs_def] "rabs(-x)=rabs(x)"; by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] addIs [real_le_anti_sym], - simpset() addsimps [real_ge_zero_iff] setloop (split_tac [expand_if]))); + simpset() addsimps [real_ge_zero_iff])); qed "rabs_minus_cancel"; -Goal "rabs(x + %~y) <= rabs x + rabs y"; +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); qed "rabs_triangle_minus_ineq"; -Goal "rabs (x + y + (%~l + %~m)) <= rabs(x + %~l) + rabs(y + %~m)"; +Goal "rabs (x + y + (-l + -m)) <= rabs(x + -l) + rabs(y + -m)"; by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1); by (rtac (real_add_assoc RS subst) 1); @@ -142,7 +140,7 @@ by (REPEAT (ares_tac [real_add_less_mono] 1)); qed "rabs_add_less"; -Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s"; +Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ -y) < r+s"; by (rotate_tac 1 1); by (dtac (rabs_minus_cancel RS ssubst) 1); by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1); @@ -176,8 +174,7 @@ real_le_less_trans]) 1); qed "rabs_mult_less"; -Goal "[| rabs x < r; rabs y < s |] \ -\ ==> rabs(x)*rabs(y) rabs(x)*rabs(y) r < rabs(x*y)"; @@ -205,27 +202,27 @@ Goalw [rabs_def] "rabs 1r = 1r"; by (auto_tac (claset() addSDs [not_real_leE RS real_less_asym], - simpset() addsimps [real_zero_less_one] setloop (split_tac [expand_if]))); + simpset() addsimps [real_zero_less_one])); qed "rabs_one"; Goal "[| 0r < x ; x < r |] ==> rabs x < r"; by (asm_simp_tac (simpset() addsimps [rabs_eqI2]) 1); qed "rabs_lessI"; -Goal "rabs x =x | rabs x = %~x"; +Goal "rabs x =x | rabs x = -x"; by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1); by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2, rabs_zero,rabs_minus_zero]) 1); qed "rabs_disj"; -Goal "rabs x = y ==> x = y | %~x = y"; +Goal "rabs x = y ==> x = y | -x = y"; by (dtac sym 1); by (hyp_subst_tac 1); by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1); by (REPEAT(Asm_simp_tac 1)); qed "rabs_eq_disj"; -Goal "(rabs x < r) = (%~r real - "rabs r == if 0r<=r then r else %~r" + "rabs r == if 0r<=r then r else -r" end \ No newline at end of file diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/RealDef.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealDef.ML Thu Oct 01 18:18:01 1998 +0200 @@ -0,0 +1,1042 @@ +(* Title : Real/RealDef.ML + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : The reals +*) + +(*** Proving that realrel is an equivalence relation ***) + +Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \ +\ ==> x1 + y3 = x3 + y1"; +by (res_inst_tac [("C","y2")] preal_add_right_cancel 1); +by (rotate_tac 1 1 THEN dtac sym 1); +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); +by (rtac (preal_add_left_commute RS subst) 1); +by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1); +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); +qed "preal_trans_lemma"; + +(** Natural deduction for realrel **) + +Goalw [realrel_def] + "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)"; +by (Blast_tac 1); +qed "realrel_iff"; + +Goalw [realrel_def] + "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel"; +by (Blast_tac 1); +qed "realrelI"; + +Goalw [realrel_def] + "p: realrel --> (EX x1 y1 x2 y2. \ +\ p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)"; +by (Blast_tac 1); +qed "realrelE_lemma"; + +val [major,minor] = goal thy + "[| p: realrel; \ +\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1 \ +\ |] ==> Q |] ==> Q"; +by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1); +by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); +qed "realrelE"; + +AddSIs [realrelI]; +AddSEs [realrelE]; + +Goal "(x,x): realrel"; +by (stac surjective_pairing 1 THEN rtac (refl RS realrelI) 1); +qed "realrel_refl"; + +Goalw [equiv_def, refl_def, sym_def, trans_def] + "equiv {x::(preal*preal).True} realrel"; +by (fast_tac (claset() addSIs [realrel_refl] + addSEs [sym,preal_trans_lemma]) 1); +qed "equiv_realrel"; + +val equiv_realrel_iff = + [TrueI, TrueI] MRS + ([CollectI, CollectI] MRS + (equiv_realrel RS eq_equiv_class_iff)); + +Goalw [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real"; +by (Blast_tac 1); +qed "realrel_in_real"; + +Goal "inj_on Abs_real real"; +by (rtac inj_on_inverseI 1); +by (etac Abs_real_inverse 1); +qed "inj_on_Abs_real"; + +Addsimps [equiv_realrel_iff,inj_on_Abs_real RS inj_on_iff, + realrel_iff, realrel_in_real, Abs_real_inverse]; + +Addsimps [equiv_realrel RS eq_equiv_class_iff]; +val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class); + +Goal "inj(Rep_real)"; +by (rtac inj_inverseI 1); +by (rtac Rep_real_inverse 1); +qed "inj_Rep_real"; + +(** real_preal: the injection from preal to real **) +Goal "inj(real_preal)"; +by (rtac injI 1); +by (rewtac real_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); +by (rtac equiv_realrel 1); +by (Blast_tac 1); +by Safe_tac; +by (Asm_full_simp_tac 1); +qed "inj_real_preal"; + +val [prem] = goal thy + "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P"; +by (res_inst_tac [("x1","z")] + (rewrite_rule [real_def] Rep_real RS quotientE) 1); +by (dres_inst_tac [("f","Abs_real")] arg_cong 1); +by (res_inst_tac [("p","x")] PairE 1); +by (rtac prem 1); +by (asm_full_simp_tac (simpset() addsimps [Rep_real_inverse]) 1); +qed "eq_Abs_real"; + +(**** real_minus: additive inverse on real ****) + +Goalw [congruent_def] + "congruent realrel (%p. split (%x y. realrel^^{(y,x)}) p)"; +by Safe_tac; +by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1); +qed "real_minus_congruent"; + +(*Resolve th against the corresponding facts for real_minus*) +val real_minus_ize = RSLIST [equiv_realrel, real_minus_congruent]; + +Goalw [real_minus_def] + "- (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})"; +by (res_inst_tac [("f","Abs_real")] arg_cong 1); +by (simp_tac (simpset() addsimps + [realrel_in_real RS Abs_real_inverse,real_minus_ize UN_equiv_class]) 1); +qed "real_minus"; + +Goal "- (- z) = (z::real)"; +by (res_inst_tac [("z","z")] eq_Abs_real 1); +by (asm_simp_tac (simpset() addsimps [real_minus]) 1); +qed "real_minus_minus"; + +Addsimps [real_minus_minus]; + +Goal "inj(%r::real. -r)"; +by (rtac injI 1); +by (dres_inst_tac [("f","uminus")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1); +qed "inj_real_minus"; + +Goalw [real_zero_def] "-0r = 0r"; +by (simp_tac (simpset() addsimps [real_minus]) 1); +qed "real_minus_zero"; + +Addsimps [real_minus_zero]; + +Goal "(-x = 0r) = (x = 0r)"; +by (res_inst_tac [("z","x")] eq_Abs_real 1); +by (auto_tac (claset(), + simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac)); +qed "real_minus_zero_iff"; + +Addsimps [real_minus_zero_iff]; + +Goal "(-x ~= 0r) = (x ~= 0r)"; +by Auto_tac; +qed "real_minus_not_zero_iff"; + +(*** Congruence property for addition ***) +Goalw [congruent2_def] + "congruent2 realrel (%p1 p2. \ +\ split (%x1 y1. split (%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"; +by Safe_tac; +by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1); +by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1); +by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); +by (asm_simp_tac (simpset() addsimps preal_add_ac) 1); +qed "real_add_congruent2"; + +(*Resolve th against the corresponding facts for real_add*) +val real_add_ize = RSLIST [equiv_realrel, real_add_congruent2]; + +Goalw [real_add_def] + "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \ +\ Abs_real(realrel^^{(x1+x2, y1+y2)})"; +by (asm_simp_tac (simpset() addsimps [real_add_ize UN_equiv_class2]) 1); +qed "real_add"; + +Goal "(z::real) + w = w + z"; +by (res_inst_tac [("z","z")] eq_Abs_real 1); +by (res_inst_tac [("z","w")] eq_Abs_real 1); +by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1); +qed "real_add_commute"; + +Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)"; +by (res_inst_tac [("z","z1")] eq_Abs_real 1); +by (res_inst_tac [("z","z2")] eq_Abs_real 1); +by (res_inst_tac [("z","z3")] eq_Abs_real 1); +by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1); +qed "real_add_assoc"; + +(*For AC rewriting*) +Goal "(x::real)+(y+z)=y+(x+z)"; +by (rtac (real_add_commute RS trans) 1); +by (rtac (real_add_assoc RS trans) 1); +by (rtac (real_add_commute RS arg_cong) 1); +qed "real_add_left_commute"; + +(* 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"; +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"; +Addsimps [real_add_zero_left]; + +Goal "z + 0r = z"; +by (simp_tac (simpset() addsimps [real_add_commute]) 1); +qed "real_add_zero_right"; +Addsimps [real_add_zero_right]; + +Goalw [real_zero_def] "z + -z = 0r"; +by (res_inst_tac [("z","z")] eq_Abs_real 1); +by (asm_full_simp_tac (simpset() addsimps [real_minus, + real_add, preal_add_commute]) 1); +qed "real_add_minus"; +Addsimps [real_add_minus]; + +Goal "-z + z = 0r"; +by (simp_tac (simpset() addsimps [real_add_commute]) 1); +qed "real_add_minus_left"; +Addsimps [real_add_minus_left]; + + +Goal "z + (- z + w) = (w::real)"; +by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); +qed "real_add_minus_cancel"; + +Goal "(-z) + (z + w) = (w::real)"; +by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); +qed "real_minus_add_cancel"; + +Addsimps [real_add_minus_cancel, real_minus_add_cancel]; + +Goal "? y. (x::real) + y = 0r"; +by (blast_tac (claset() addIs [real_add_minus]) 1); +qed "real_minus_ex"; + +Goal "?! y. (x::real) + y = 0r"; +by (auto_tac (claset() addIs [real_add_minus],simpset())); +by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); +by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); +qed "real_minus_ex1"; + +Goal "?! y. y + (x::real) = 0r"; +by (auto_tac (claset() addIs [real_add_minus_left],simpset())); +by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1); +by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); +qed "real_minus_left_ex1"; + +Goal "x + y = 0r ==> x = -y"; +by (cut_inst_tac [("z","y")] real_add_minus_left 1); +by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1); +by (Blast_tac 1); +qed "real_add_minus_eq_minus"; + +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); +by (auto_tac (claset(),simpset() addsimps [real_minus,real_add])); +qed "real_minus_add_distrib"; + +Addsimps [real_minus_add_distrib]; + +Goal "((x::real) + y = x + z) = (y = z)"; +by (Step_tac 1); +by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); +qed "real_add_left_cancel"; + +Goal "(y + (x::real)= z + x) = (y = z)"; +by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1); +qed "real_add_right_cancel"; + +Goal "0r - x = -x"; +by (simp_tac (simpset() addsimps [real_diff_def]) 1); +qed "real_diff_0"; + +Goal "x - 0r = x"; +by (simp_tac (simpset() addsimps [real_diff_def]) 1); +qed "real_diff_0_right"; + +Goal "x - x = 0r"; +by (simp_tac (simpset() addsimps [real_diff_def]) 1); +qed "real_diff_self"; + +Addsimps [real_diff_0, real_diff_0_right, real_diff_self]; + + +(*** Congruence property for multiplication ***) + +Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \ +\ x * x1 + y * y1 + (x * y2 + x2 * y) = \ +\ x * x2 + y * y2 + (x * y1 + x1 * y)"; +by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute, + preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1); +by (rtac (preal_mult_commute RS subst) 1); +by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1); +by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc, + preal_add_mult_distrib2 RS sym]) 1); +by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1); +qed "real_mult_congruent2_lemma"; + +Goal + "congruent2 realrel (%p1 p2. \ +\ split (%x1 y1. split (%x2 y2. realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"; +by (rtac (equiv_realrel RS congruent2_commuteI) 1); +by Safe_tac; +by (rewtac split_def); +by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1); +by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma])); +qed "real_mult_congruent2"; + +(*Resolve th against the corresponding facts for real_mult*) +val real_mult_ize = RSLIST [equiv_realrel, real_mult_congruent2]; + +Goalw [real_mult_def] + "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) = \ +\ Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})"; +by (simp_tac (simpset() addsimps [real_mult_ize UN_equiv_class2]) 1); +qed "real_mult"; + +Goal "(z::real) * w = w * z"; +by (res_inst_tac [("z","z")] eq_Abs_real 1); +by (res_inst_tac [("z","w")] eq_Abs_real 1); +by (asm_simp_tac + (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1); +qed "real_mult_commute"; + +Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)"; +by (res_inst_tac [("z","z1")] eq_Abs_real 1); +by (res_inst_tac [("z","z2")] eq_Abs_real 1); +by (res_inst_tac [("z","z3")] eq_Abs_real 1); +by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @ + preal_add_ac @ preal_mult_ac) 1); +qed "real_mult_assoc"; + +qed_goal "real_mult_left_commute" thy + "(z1::real) * (z2 * z3) = z2 * (z1 * z3)" + (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1, + rtac (real_mult_commute RS arg_cong) 1]); + +(* real multiplication is an AC operator *) +val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute]; + +Goalw [real_one_def,pnat_one_def] "1r * z = z"; +by (res_inst_tac [("z","z")] eq_Abs_real 1); +by (asm_full_simp_tac + (simpset() addsimps [real_mult, + preal_add_mult_distrib2,preal_mult_1_right] + @ preal_mult_ac @ preal_add_ac) 1); +qed "real_mult_1"; + +Addsimps [real_mult_1]; + +Goal "z * 1r = z"; +by (simp_tac (simpset() addsimps [real_mult_commute]) 1); +qed "real_mult_1_right"; + +Addsimps [real_mult_1_right]; + +Goalw [real_zero_def,pnat_one_def] "0r * z = 0r"; +by (res_inst_tac [("z","z")] eq_Abs_real 1); +by (asm_full_simp_tac (simpset() addsimps [real_mult, + preal_add_mult_distrib2,preal_mult_1_right] + @ preal_mult_ac @ preal_add_ac) 1); +qed "real_mult_0"; + +Goal "z * 0r = 0r"; +by (simp_tac (simpset() addsimps [real_mult_commute, real_mult_0]) 1); +qed "real_mult_0_right"; + +Addsimps [real_mult_0_right, real_mult_0]; + +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); +by (auto_tac (claset(), + simpset() addsimps [real_minus,real_mult] + @ preal_mult_ac @ preal_add_ac)); +qed "real_minus_mult_eq1"; + +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); +by (auto_tac (claset(), + simpset() addsimps [real_minus,real_mult] + @ preal_mult_ac @ preal_add_ac)); +qed "real_minus_mult_eq2"; + +Goal "- 1r * z = -z"; +by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1); +qed "real_mult_minus_1"; + +Addsimps [real_mult_minus_1]; + +Goal "z * - 1r = -z"; +by (stac real_mult_commute 1); +by (Simp_tac 1); +qed "real_mult_minus_1_right"; + +Addsimps [real_mult_minus_1_right]; + +Goal "-x * -y = x * (y::real)"; +by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, + real_minus_mult_eq1 RS sym]) 1); +qed "real_minus_mult_cancel"; + +Addsimps [real_minus_mult_cancel]; + +Goal "-x * y = x * -(y::real)"; +by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym, + real_minus_mult_eq1 RS sym]) 1); +qed "real_minus_mult_commute"; + +(*----------------------------------------------------------------------------- + + -----------------------------------------------------------------------------*) + +(** Lemmas **) + +qed_goal "real_add_assoc_cong" thy + "!!z. (z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" + (fn _ => [(asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1)]); + +qed_goal "real_add_assoc_swap" thy "(z::real) + (v + w) = v + (z + w)" + (fn _ => [(REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1))]); + +Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"; +by (res_inst_tac [("z","z1")] eq_Abs_real 1); +by (res_inst_tac [("z","z2")] eq_Abs_real 1); +by (res_inst_tac [("z","w")] eq_Abs_real 1); +by (asm_simp_tac + (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @ + preal_add_ac @ preal_mult_ac) 1); +qed "real_add_mult_distrib"; + +val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute; + +Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)"; +by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1); +qed "real_add_mult_distrib2"; + +(*** one and zero are distinct ***) +Goalw [real_zero_def,real_one_def] "0r ~= 1r"; +by (auto_tac (claset(), + simpset() addsimps [preal_self_less_add_left RS preal_not_refl2])); +qed "real_zero_not_eq_one"; + +(*** existence of inverse ***) +(** lemma -- alternative definition for 0r **) +Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})"; +by (auto_tac (claset(),simpset() addsimps [preal_add_commute])); +qed "real_zero_iff"; + +Goalw [real_zero_def,real_one_def] + "!!(x::real). x ~= 0r ==> ? y. x*y = 1r"; +by (res_inst_tac [("z","x")] eq_Abs_real 1); +by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1); +by (auto_tac (claset() addSDs [preal_less_add_left_Ex], + 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 (auto_tac (claset(), + simpset() addsimps [real_mult, + pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2, + preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right] + @ preal_add_ac @ preal_mult_ac)); +qed "real_mult_inv_right_ex"; + +Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r"; +by (asm_simp_tac (simpset() addsimps [real_mult_commute, + real_mult_inv_right_ex]) 1); +qed "real_mult_inv_left_ex"; + +Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r"; +by (forward_tac [real_mult_inv_left_ex] 1); +by (Step_tac 1); +by (rtac selectI2 1); +by Auto_tac; +qed "real_mult_inv_left"; + +Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r"; +by (auto_tac (claset() addIs [real_mult_commute RS subst], + simpset() addsimps [real_mult_inv_left])); +qed "real_mult_inv_right"; + +Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)"; +by Auto_tac; +by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); +qed "real_mult_left_cancel"; + +Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)"; +by (Step_tac 1); +by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1); +qed "real_mult_right_cancel"; + +Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r"; +by (forward_tac [real_mult_inv_left_ex] 1); +by (etac exE 1); +by (rtac selectI2 1); +by (auto_tac (claset(), + simpset() addsimps [real_mult_0, + real_zero_not_eq_one])); +qed "rinv_not_zero"; + +Addsimps [real_mult_inv_left,real_mult_inv_right]; + +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); +by (auto_tac (claset() addDs [rinv_not_zero],simpset())); +qed "real_rinv_rinv"; + +Goalw [rinv_def] "rinv(1r) = 1r"; +by (cut_facts_tac [real_zero_not_eq_one RS + not_sym RS real_mult_inv_left_ex] 1); +by (etac exE 1); +by (rtac selectI2 1); +by (auto_tac (claset(), + simpset() addsimps + [real_zero_not_eq_one RS not_sym])); +qed "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 ***) +(* prove introduction and elimination rules for real_less *) + +(* 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); +qed "preal_lemma_eq_rev_sum"; + +Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1"; +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); +qed "preal_add_left_commute_cancel"; + +Goal "!!(x::preal). [| x + y2a = x2a + y; \ +\ x + y2b = x2b + y |] \ +\ ==> x2a + y2b = x2b + y2a"; +by (dtac preal_lemma_eq_rev_sum 1); +by (assume_tac 1); +by (thin_tac "x + y2b = x2b + y" 1); +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); +by (dtac preal_add_left_commute_cancel 1); +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); +qed "preal_lemma_for_not_refl"; + +Goal "~ (R::real) < R"; +by (res_inst_tac [("z","R")] eq_Abs_real 1); +by (auto_tac (claset(),simpset() addsimps [real_less_def])); +by (dtac preal_lemma_for_not_refl 1); +by (assume_tac 1 THEN rotate_tac 2 1); +by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl])); +qed "real_less_not_refl"; + +(*** y < y ==> P ***) +bind_thm("real_less_irrefl", real_less_not_refl RS notE); +AddSEs [real_less_irrefl]; + +Goal "!!(x::real). x < y ==> x ~= y"; +by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); +qed "real_not_refl2"; + +(* lemma re-arranging and eliminating terms *) +Goal "!! (a::preal). [| a + b = c + d; \ +\ x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \ +\ ==> x2b + y2e < x2e + y2b"; +by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1); +by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1); +by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1); +qed "preal_lemma_trans"; + +(** heavy re-writing involved*) +Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3"; +by (res_inst_tac [("z","R1")] eq_Abs_real 1); +by (res_inst_tac [("z","R2")] eq_Abs_real 1); +by (res_inst_tac [("z","R3")] eq_Abs_real 1); +by (auto_tac (claset(),simpset() addsimps [real_less_def])); +by (REPEAT(rtac exI 1)); +by (EVERY[rtac conjI 1, rtac conjI 2]); +by (REPEAT(Blast_tac 2)); +by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1); +by (blast_tac (claset() addDs [preal_add_less_mono] + addIs [preal_lemma_trans]) 1); +qed "real_less_trans"; + +Goal "!! (R1::real). [| R1 < R2; R2 < R1 |] ==> P"; +by (dtac real_less_trans 1 THEN assume_tac 1); +by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1); +qed "real_less_asym"; + +(****)(****)(****)(****)(****)(****)(****)(****)(****)(****) + (****** Map and more real_less ******) +(*** mapping from preal into real ***) +Goalw [real_preal_def] + "%#((z1::preal) + z2) = %#z1 + %#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"; + +Goalw [real_preal_def] + "%#((z1::preal) * z2) = %#z1* %#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"; + +Goalw [real_preal_def] + "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m"; +by (auto_tac (claset() addSDs [preal_less_add_left_Ex], + simpset() addsimps preal_add_ac)); +qed "real_preal_ExI"; + +Goalw [real_preal_def] + "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#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"; + +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"; + +(*** Gleason prop 9-4.4 p 127 ***) +Goalw [real_preal_def,real_zero_def] + "? m. (x::real) = %#m | x = 0r | x = -(%#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"; + +Goal "!!P. [| !!m. x = %#m ==> P; \ +\ x = 0r ==> P; \ +\ !!m. x = -(%#m) ==> P |] ==> P"; +by (cut_inst_tac [("x","x")] real_preal_trichotomy 1); +by Auto_tac; +qed "real_preal_trichotomyE"; + +Goalw [real_preal_def] "%#m1 < %#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"; + +Goal "m1 < m2 ==> %#m1 < %#m2"; +by (dtac preal_less_add_left_Ex 1); +by (auto_tac (claset(), + simpset() addsimps [real_preal_add, + real_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"; + +Goal "(%#m1 < %#m2) = (m1 < m2)"; +by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1); +qed "real_preal_less_iff1"; + +Addsimps [real_preal_less_iff1]; + +Goal "- %#m < %#m"; +by (auto_tac (claset(), + simpset() addsimps + [real_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"; + +Goalw [real_zero_def] "- %#m < 0r"; +by (auto_tac (claset(), + simpset() addsimps [real_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"; + +Goal "~ 0r < - %#m"; +by (cut_facts_tac [real_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"; + +Goalw [real_zero_def] "0r < %#m"; +by (auto_tac (claset(), + simpset() addsimps [real_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"; + +Goal "~ %#m < 0r"; +by (cut_facts_tac [real_preal_zero_less] 1); +by (blast_tac (claset() addDs [real_less_trans] + addEs [real_less_irrefl]) 1); +qed "real_preal_not_less_zero"; + +Goal "0r < - - %#m"; +by (simp_tac (simpset() addsimps + [real_preal_zero_less]) 1); +qed "real_minus_minus_zero_less"; + +(* another lemma *) +Goalw [real_zero_def] "0r < %#m + %#m1"; +by (auto_tac (claset(), + simpset() addsimps [real_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"; + +Goal "- %#m < %#m1"; +by (auto_tac (claset(), + simpset() addsimps [real_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"; + +Goal "~ %#m < - %#m1"; +by (cut_facts_tac [real_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"; + +Goal "- %#m1 < - %#m2 ==> %#m2 < %#m1"; +by (auto_tac (claset(), + simpset() addsimps [real_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"; + +Goal "%#m1 < %#m2 ==> - %#m2 < - %#m1"; +by (auto_tac (claset(), + simpset() addsimps [real_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"; + +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"; + +Addsimps [real_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 (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])); +qed "real_linear"; + +Goal "!!w::real. (w ~= z) = (w P; R1 = R2 ==> P; \ +\ R2 < R1 ==> P |] ==> P"; +by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1); +by Auto_tac; +qed "real_linear_less2"; + +(*** Properties of <= ***) + +Goalw [real_le_def] "~(w < z) ==> z <= (w::real)"; +by (assume_tac 1); +qed "real_leI"; + +Goalw [real_le_def] "z<=w ==> ~(w<(z::real))"; +by (assume_tac 1); +qed "real_leD"; + +val real_leE = make_elim real_leD; + +Goal "(~(w < z)) = (z <= (w::real))"; +by (blast_tac (claset() addSIs [real_leI,real_leD]) 1); +qed "real_less_le_iff"; + +Goalw [real_le_def] "~ z <= w ==> w<(z::real)"; +by (Blast_tac 1); +qed "not_real_leE"; + +Goalw [real_le_def] "z < w ==> z <= (w::real)"; +by (blast_tac (claset() addEs [real_less_asym]) 1); +qed "real_less_imp_le"; + +Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y"; +by (cut_facts_tac [real_linear] 1); +by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); +qed "real_le_imp_less_or_eq"; + +Goalw [real_le_def] "z z <=(w::real)"; +by (cut_facts_tac [real_linear] 1); +by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1); +qed "real_less_or_eq_imp_le"; + +Goal "(x <= (y::real)) = (x < y | x=y)"; +by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1)); +qed "real_le_less"; + +Goal "w <= (w::real)"; +by (simp_tac (simpset() addsimps [real_le_less]) 1); +qed "real_le_refl"; + +AddIffs [real_le_refl]; + +(* Axiom 'linorder_linear' of class 'linorder': *) +Goal "(z::real) <= w | w <= z"; +by (simp_tac (simpset() addsimps [real_le_less]) 1); +by (cut_facts_tac [real_linear] 1); +by (Blast_tac 1); +qed "real_le_linear"; + +Goal "[| i <= j; j < k |] ==> i < (k::real)"; +by (dtac real_le_imp_less_or_eq 1); +by (blast_tac (claset() addIs [real_less_trans]) 1); +qed "real_le_less_trans"; + +Goal "!! (i::real). [| i < j; j <= k |] ==> i < k"; +by (dtac real_le_imp_less_or_eq 1); +by (blast_tac (claset() addIs [real_less_trans]) 1); +qed "real_less_le_trans"; + +Goal "[| i <= j; j <= k |] ==> i <= (k::real)"; +by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, + rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]); +qed "real_le_trans"; + +Goal "[| z <= w; w <= z |] ==> z = (w::real)"; +by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq, + fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]); +qed "real_le_anti_sym"; + +Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)"; +by (rtac not_real_leE 1); +by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1); +qed "not_less_not_eq_real_less"; + +(* Axiom 'order_less_le' of class 'order': *) +Goal "(w::real) < z = (w <= z & w ~= z)"; +by (simp_tac (simpset() addsimps [real_le_def, real_neq_iff]) 1); +by (blast_tac (claset() addSEs [real_less_asym]) 1); +qed "real_less_le"; + + +Goal "(0r < -R) = (R < 0r)"; +by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); +by (auto_tac (claset(), + simpset() addsimps [real_preal_not_minus_gt_zero, + real_preal_not_less_zero,real_preal_zero_less, + real_preal_minus_less_zero])); +qed "real_minus_zero_less_iff"; + +Addsimps [real_minus_zero_less_iff]; + +Goal "(-R < 0r) = (0r < R)"; +by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); +by (auto_tac (claset(), + simpset() addsimps [real_preal_not_minus_gt_zero, + real_preal_not_less_zero,real_preal_zero_less, + real_preal_minus_less_zero])); +qed "real_minus_zero_less_iff2"; + + +(*Alternative definition for real_less*) +Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S"; +by (res_inst_tac [("x","R")] real_preal_trichotomyE 1); +by (ALLGOALS(res_inst_tac [("x","S")] real_preal_trichotomyE)); +by (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, + 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); +by (auto_tac (claset(), + simpset() addsimps [real_preal_zero_less, + real_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); +by (auto_tac (claset(), + simpset() addsimps [real_add_minus, + real_add_zero_right] @ real_add_ac)); +qed "real_less_sum_gt_zero"; + +Goal "!!S::real. T = S + W ==> S = T + -W"; +by (asm_simp_tac (simpset() addsimps real_add_ac) 1); +qed "real_lemma_change_eq_subj"; + +(* FIXME: long! *) +Goal "(0r < S + -W) ==> (W < S)"; +by (rtac ccontr 1); +by (dtac (real_leI RS real_le_imp_less_or_eq) 1); +by (auto_tac (claset(), + simpset() addsimps [real_less_not_refl])); +by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]); +by (Asm_full_simp_tac 1); +by (dtac real_lemma_change_eq_subj 1); +by Auto_tac; +by (dtac real_less_sum_gt_zero 1); +by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1); +by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]); +by (auto_tac (claset() addEs [real_less_asym], simpset())); +qed "real_sum_gt_zero_less"; + +Goal "(0r < S + -W) = (W < S)"; +by (blast_tac (claset() addIs [real_less_sum_gt_zero, + real_sum_gt_zero_less]) 1); +qed "real_less_sum_gt_0_iff"; + + +Goalw [real_diff_def] "(x (x (y<=x) = (y'<=x')"; +by (dtac real_less_eqI 1); +by (asm_simp_tac (simpset() addsimps [real_le_def]) 1); +qed "real_le_eqI"; + +Goal "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"; +by Safe_tac; +by (ALLGOALS + (asm_full_simp_tac + (simpset() addsimps [real_eq_diff_eq, real_diff_eq_eq]))); +qed "real_eq_eqI"; diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/RealDef.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealDef.thy Thu Oct 01 18:18:01 1998 +0200 @@ -0,0 +1,62 @@ +(* Title : Real/RealDef.thy + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : The reals +*) + +RealDef = PReal + + +constdefs + realrel :: "((preal * preal) * (preal * preal)) set" + "realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" + +typedef real = "{x::(preal*preal).True}/realrel" (Equiv.quotient_def) + + +instance + real :: {ord, plus, times, minus} + +consts + + "0r" :: real ("0r") + "1r" :: real ("1r") + +defs + + real_zero_def "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})" + real_one_def "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})" + + real_minus_def + "- R == Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)" + + real_diff_def "x - y == x + -(y::real)" + +constdefs + + real_preal :: preal => real ("%#_" [80] 80) + "%# m == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})" + + rinv :: real => real + "rinv(R) == (@S. R ~= 0r & S*R = 1r)" + + real_nat :: nat => real ("%%# _" [80] 80) + "%%# n == %#(@#($#(*# n)))" + +defs + + real_add_def + "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). + split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)" + + real_mult_def + "P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). + split(%x1 y1. split(%x2 y2. realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)" + + real_less_def + "P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & + (x1,y1):Rep_real(P) & + (x2,y2):Rep_real(Q)" + real_le_def + "P <= (Q::real) == ~(Q < P)" + +end diff -r 7fceb6eea475 -r a3ab526bb891 src/HOL/Real/simproc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/simproc.ML Thu Oct 01 18:18:01 1998 +0200 @@ -0,0 +1,62 @@ +(* Title: HOL/Real/simproc.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +Apply Abel_Cancel to the reals +*) + +(*** Two lemmas needed for the simprocs ***) + +(*Deletion of other terms in the formula, seeking the -x at the front of z*) +val real_add_cancel_21 = prove_goal RealDef.thy + "((x::real) + (y + z) = y + u) = ((x + z) = u)" + (fn _ => [stac real_add_left_commute 1, + rtac real_add_left_cancel 1]); + +(*A further rule to deal with the case that + everything gets cancelled on the right.*) +val real_add_cancel_end = prove_goal RealDef.thy + "((x::real) + (y + z) = y) = (x = -z)" + (fn _ => [stac real_add_left_commute 1, + res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1, + stac real_add_left_cancel 1, + simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1]); + + +structure Real_Cancel_Data = +struct + val ss = HOL_ss + val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq + fun mk_meta_eq r = r RS eq_reflection + + val thy = RealDef.thy + val T = Type ("RealDef.real", []) + val zero = Const ("RealDef.0r", T) + val add_cancel_21 = real_add_cancel_21 + val add_cancel_end = real_add_cancel_end + val add_left_cancel = real_add_left_cancel + val add_assoc = real_add_assoc + val add_commute = real_add_commute + val add_left_commute = real_add_left_commute + val add_0 = real_add_zero_left + val add_0_right = real_add_zero_right + + val eq_diff_eq = real_eq_diff_eq + val eqI_rules = [real_less_eqI, real_eq_eqI, real_le_eqI] + fun dest_eqI th = + #1 (HOLogic.dest_bin "op =" HOLogic.boolT + (HOLogic.dest_Trueprop (concl_of th))) + + val diff_def = real_diff_def + val minus_add_distrib = real_minus_add_distrib + val minus_minus = real_minus_minus + val minus_0 = real_minus_zero + val add_inverses = [real_add_minus, real_add_minus_left]; + val cancel_simps = [real_add_minus_cancel, real_minus_add_cancel] +end; + +structure Real_Cancel = Abel_Cancel (Real_Cancel_Data); + +Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv]; +