# HG changeset patch # User wenzelm # Date 964475948 -7200 # Node ID c8eb573114ded582000edea32cc461fada8254fb # Parent a9c60e65510721ae0140fa717fa5cbc864cf7056 rename_numerals: use implicit theory context; diff -r a9c60e655107 -r c8eb573114de src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Mon Jul 24 23:58:49 2000 +0200 +++ b/src/HOL/Real/RComplete.ML Mon Jul 24 23:59:08 2000 +0200 @@ -1,9 +1,9 @@ -(* Title : RComplete.thy +(* Title : HOL/Real/RComplete.ML ID : $Id$ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge - Description : Completeness theorems for positive - reals and reals + +Completeness theorems for positive reals and reals. *) claset_ref() := claset() delWrapper "bspec"; @@ -18,7 +18,7 @@ \ ((EX x:P. y < x) = (EX X. real_of_preal X : P & \ \ y < real_of_preal X))"; by (blast_tac (claset() addSDs [bspec, - rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1); + rename_numerals real_gt_zero_preal_Ex RS iffD1]) 1); qed "real_sup_lemma1"; Goal "[| ALL x:P. #0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \ @@ -26,12 +26,12 @@ \ (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)"; by (rtac conjI 1); by (blast_tac (claset() addDs [bspec, - rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1); + rename_numerals real_gt_zero_preal_Ex RS iffD1]) 1); by Auto_tac; by (dtac bspec 1 THEN assume_tac 1); by (ftac bspec 1 THEN assume_tac 1); by (dtac real_less_trans 1 THEN assume_tac 1); -by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1 +by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1 THEN etac exE 1); by (res_inst_tac [("x","ya")] exI 1); by Auto_tac; @@ -56,8 +56,8 @@ by Auto_tac; by (ftac real_sup_lemma2 1 THEN Auto_tac); by (case_tac "#0 < ya" 1); -by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); -by (dtac (rename_numerals thy real_less_all_real2) 2); +by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1); +by (dtac (rename_numerals real_less_all_real2) 2); by Auto_tac; by (rtac (preal_complete RS spec RS iffD1) 1); by Auto_tac; @@ -66,7 +66,7 @@ (* second part *) by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1); by (case_tac "#0 < ya" 1); -by (auto_tac (claset() addSDs (map (rename_numerals thy) +by (auto_tac (claset() addSDs (map rename_numerals [real_less_all_real2, real_gt_zero_preal_Ex RS iffD1]), simpset())); @@ -105,10 +105,10 @@ by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def])); by (auto_tac (claset() addSIs [setleI,setgeI] - addSDs [(rename_numerals thy real_gt_zero_preal_Ex) RS iffD1], + addSDs [(rename_numerals real_gt_zero_preal_Ex) RS iffD1], simpset())); by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1); -by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); +by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1); by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff])); by (rtac preal_psup_leI2a 1); by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1); @@ -118,7 +118,7 @@ by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1); by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1); by (ftac isUbD2 1); -by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); +by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1); by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex], simpset() addsimps [real_of_preal_le_iff])); by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] @@ -233,15 +233,15 @@ by (res_inst_tac [("x","0")] exI 2); by (auto_tac (claset() addEs [real_less_trans], simpset() addsimps [real_of_posnat_one,real_zero_less_one])); -by (ftac ((rename_numerals thy real_rinv_gt_zero) RS reals_Archimedean) 1); +by (ftac ((rename_numerals 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")] - (rename_numerals thy real_mult_less_mono1) 1); + (rename_numerals real_mult_less_mono1) 1); by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym])); by (dres_inst_tac [("n1","n"),("y","#1")] (real_of_posnat_less_zero RS real_mult_less_mono2) 1); by (auto_tac (claset(), - simpset() addsimps [rename_numerals thy real_of_posnat_less_zero, + simpset() addsimps [rename_numerals real_of_posnat_less_zero, real_not_refl2 RS not_sym, real_mult_assoc RS sym])); qed "reals_Archimedean2"; diff -r a9c60e655107 -r c8eb573114de src/HOL/Real/RealPow.ML --- a/src/HOL/Real/RealPow.ML Mon Jul 24 23:58:49 2000 +0200 +++ b/src/HOL/Real/RealPow.ML Mon Jul 24 23:59:08 2000 +0200 @@ -24,7 +24,7 @@ by (induct_tac "n" 1); by (Auto_tac); by (forw_inst_tac [("n","n")] realpow_not_zero 1); -by (auto_tac (claset() addDs [rename_numerals thy real_rinv_distrib], +by (auto_tac (claset() addDs [rename_numerals real_rinv_distrib], simpset())); qed_spec_mp "realpow_rinv"; @@ -51,19 +51,19 @@ Goal "(#0::real) < r --> #0 <= r ^ n"; by (induct_tac "n" 1); by (auto_tac (claset() addDs [real_less_imp_le] - addIs [rename_numerals thy real_le_mult_order], + addIs [rename_numerals real_le_mult_order], simpset())); qed_spec_mp "realpow_ge_zero"; Goal "(#0::real) < r --> #0 < r ^ n"; by (induct_tac "n" 1); -by (auto_tac (claset() addIs [rename_numerals thy real_mult_order], +by (auto_tac (claset() addIs [rename_numerals real_mult_order], simpset() addsimps [real_zero_less_one])); qed_spec_mp "realpow_gt_zero"; Goal "(#0::real) <= r --> #0 <= r ^ n"; by (induct_tac "n" 1); -by (auto_tac (claset() addIs [rename_numerals thy real_le_mult_order], +by (auto_tac (claset() addIs [rename_numerals real_le_mult_order], simpset())); qed_spec_mp "realpow_ge_zero2"; @@ -83,7 +83,7 @@ Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n"; by (induct_tac "n" 1); -by (auto_tac (claset() addIs [rename_numerals thy real_mult_less_mono, gr0I] +by (auto_tac (claset() addIs [rename_numerals real_mult_less_mono, gr0I] addDs [realpow_gt_zero], simpset())); qed_spec_mp "realpow_less"; @@ -113,29 +113,29 @@ qed "realpow_mult"; Goal "(#0::real) <= r ^ 2"; -by (simp_tac (simpset() addsimps [rename_numerals thy real_le_square]) 1); +by (simp_tac (simpset() addsimps [rename_numerals real_le_square]) 1); qed "realpow_two_le"; Addsimps [realpow_two_le]; Goal "abs((x::real) ^ 2) = x ^ 2"; by (simp_tac (simpset() addsimps [abs_eqI1, - rename_numerals thy real_le_square]) 1); + rename_numerals real_le_square]) 1); qed "abs_realpow_two"; Addsimps [abs_realpow_two]; Goal "abs(x::real) ^ 2 = x ^ 2"; by (simp_tac (simpset() addsimps - [realpow_abs,abs_eqI1] delsimps [realpow_Suc]) 1); + [realpow_abs,abs_eqI1] delsimps [thm "realpow_Suc"]) 1); qed "realpow_two_abs"; Addsimps [realpow_two_abs]; Goal "(#1::real) < r ==> #1 < r ^ 2"; by Auto_tac; -by (cut_facts_tac [rename_numerals thy real_zero_less_one] 1); +by (cut_facts_tac [rename_numerals real_zero_less_one] 1); by (forw_inst_tac [("R1.0","#0")] real_less_trans 1); by (assume_tac 1); by (dres_inst_tac [("z","r"),("x","#1")] - (rename_numerals thy real_mult_less_mono1) 1); + (rename_numerals real_mult_less_mono1) 1); by (auto_tac (claset() addIs [real_less_trans],simpset())); qed "realpow_two_gt_one"; @@ -143,7 +143,7 @@ by (induct_tac "n" 1); by (auto_tac (claset() addSDs [real_le_imp_less_or_eq], simpset())); -by (dtac (rename_numerals thy (real_zero_less_one RS real_mult_less_mono)) 1); +by (dtac (rename_numerals (real_zero_less_one RS real_mult_less_mono)) 1); by (dtac sym 4); by (auto_tac (claset() addSIs [real_less_imp_le], simpset() addsimps [real_zero_less_one])); @@ -153,9 +153,9 @@ by (forw_inst_tac [("n","n")] realpow_ge_one 1); by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1); by (dtac sym 2); -by (ftac (rename_numerals thy (real_zero_less_one RS real_less_trans)) 1); +by (ftac (rename_numerals (real_zero_less_one RS real_less_trans)) 1); by (dres_inst_tac [("y","r ^ n")] - (rename_numerals thy real_mult_less_mono2) 1); + (rename_numerals real_mult_less_mono2) 1); by (assume_tac 1); by (auto_tac (claset() addDs [real_less_trans], simpset())); @@ -171,7 +171,7 @@ by (forw_inst_tac [("n1","n")] ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1); by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] - addIs [rename_numerals thy real_mult_order], + addIs [rename_numerals real_mult_order], simpset())); qed "realpow_Suc_gt_zero"; @@ -254,7 +254,7 @@ by (induct_tac "N" 1); by (Auto_tac); by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2)); -by (ALLGOALS(dtac (rename_numerals thy real_mult_le_mono3))); +by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3))); by (REPEAT(assume_tac 1)); by (REPEAT(assume_tac 3)); by (auto_tac (claset(),simpset() addsimps @@ -297,7 +297,7 @@ by (induct_tac "N" 1); by (Auto_tac); by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one)); -by (ALLGOALS(dtac (rename_numerals thy real_mult_self_le))); +by (ALLGOALS(dtac (rename_numerals real_mult_self_le))); by (assume_tac 1); by (assume_tac 2); by (auto_tac (claset() addIs [real_le_trans], @@ -308,7 +308,7 @@ by (induct_tac "N" 1); by (Auto_tac); by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2)); -by (ALLGOALS(dtac (rename_numerals thy real_mult_self_le2))); +by (ALLGOALS(dtac (rename_numerals real_mult_self_le2))); by (assume_tac 1); by (assume_tac 2); by (auto_tac (claset() addIs [real_le_trans], @@ -373,18 +373,18 @@ @ real_mult_ac) 1); qed "realpow_two_add_minus"; -goalw RealPow.thy [real_diff_def] +Goalw [real_diff_def] "(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)"; by (simp_tac (simpset() addsimps [realpow_two_add_minus] - delsimps [realpow_Suc]) 1); + delsimps [thm "realpow_Suc"]) 1); qed "realpow_two_diff"; -goalw RealPow.thy [real_diff_def] +Goalw [real_diff_def] "((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)"; -by (auto_tac (claset(),simpset() delsimps [realpow_Suc])); -by (dtac (rename_numerals thy (real_eq_minus_iff RS iffD1 RS sym)) 1); -by (auto_tac (claset() addDs [rename_numerals thy real_add_minus_eq_minus], - simpset() addsimps [realpow_two_add_minus] delsimps [realpow_Suc])); +by (auto_tac (claset(),simpset() delsimps [thm "realpow_Suc"])); +by (dtac (rename_numerals (real_eq_minus_iff RS iffD1 RS sym)) 1); +by (auto_tac (claset() addDs [rename_numerals real_add_minus_eq_minus], + simpset() addsimps [realpow_two_add_minus] delsimps [thm "realpow_Suc"])); qed "realpow_two_disj"; (* used in Transc *)