src/HOL/Real/Hyperreal/HyperDef.ML
changeset 9013 9dd0274f76af
parent 8856 435187ffc64e
child 9043 ca761fe227d8
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed May 31 18:06:02 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Jun 01 11:22:27 2000 +0200
     1.3 @@ -327,7 +327,7 @@
     1.4  (**** hrinv: multiplicative inverse on hypreal ****)
     1.5  
     1.6  Goalw [congruent_def]
     1.7 -  "congruent hyprel (%X. hyprel^^{%n. if X n = 0r then 0r else rinv(X n)})";
     1.8 +  "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else rinv(X n)})";
     1.9  by (Auto_tac THEN Ultra_tac 1);
    1.10  qed "hypreal_hrinv_congruent";
    1.11  
    1.12 @@ -336,7 +336,7 @@
    1.13  
    1.14  Goalw [hrinv_def]
    1.15        "hrinv (Abs_hypreal(hyprel^^{%n. X n})) = \
    1.16 -\      Abs_hypreal(hyprel ^^ {%n. if X n = 0r then 0r else rinv(X n)})";
    1.17 +\      Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else rinv(X n)})";
    1.18  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    1.19  by (simp_tac (simpset() addsimps 
    1.20     [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
    1.21 @@ -347,7 +347,8 @@
    1.22  by (rotate_tac 1 1);
    1.23  by (asm_full_simp_tac (simpset() addsimps 
    1.24      [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
    1.25 -by (ultra_tac (claset() addDs [rinv_not_zero,real_rinv_rinv],simpset()) 1);
    1.26 +by (ultra_tac (claset() addDs (map (full_rename_numerals thy)
    1.27 +    [rinv_not_zero,real_rinv_rinv]),simpset()) 1);
    1.28  qed "hypreal_hrinv_hrinv";
    1.29  
    1.30  Addsimps [hypreal_hrinv_hrinv];
    1.31 @@ -718,7 +719,7 @@
    1.32      hypreal_mult] setloop (split_tac [expand_if])) 1);
    1.33  by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
    1.34  by (ultra_tac (claset() addIs [ccontr] addDs 
    1.35 -    [rinv_not_zero],simpset()) 1);
    1.36 +    [full_rename_numerals thy rinv_not_zero],simpset()) 1);
    1.37  qed "hrinv_not_zero";
    1.38  
    1.39  Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
    1.40 @@ -861,15 +862,16 @@
    1.41  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    1.42  by (auto_tac (claset() addSIs [exI],simpset() addsimps
    1.43      [hypreal_less_def,hypreal_mult]));
    1.44 -by (ultra_tac (claset() addIs [real_mult_order],simpset()) 1);
    1.45 +by (ultra_tac (claset() addIs [rename_numerals thy 
    1.46 +    real_mult_order],simpset()) 1);
    1.47  qed "hypreal_mult_order";
    1.48  
    1.49  (*---------------------------------------------------------------------------------
    1.50                           Trichotomy of the hyperreals
    1.51    --------------------------------------------------------------------------------*)
    1.52  
    1.53 -Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. 0r}";
    1.54 -by (res_inst_tac [("x","%n. 0r")] exI 1);
    1.55 +Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. #0}";
    1.56 +by (res_inst_tac [("x","%n. #0")] exI 1);
    1.57  by (Step_tac 1);
    1.58  by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
    1.59  qed "lemma_hyprel_0r_mem";
    1.60 @@ -1153,8 +1155,8 @@
    1.61  qed "hypreal_mult_less_zero";
    1.62  
    1.63  Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
    1.64 -by (res_inst_tac [("x","%n. 0r")] exI 1);
    1.65 -by (res_inst_tac [("x","%n. 1r")] exI 1);
    1.66 +by (res_inst_tac [("x","%n. #0")] exI 1);
    1.67 +by (res_inst_tac [("x","%n. #1")] exI 1);
    1.68  by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
    1.69      FreeUltrafilterNat_Nat_set]));
    1.70  qed "hypreal_zero_less_one";
    1.71 @@ -1326,25 +1328,25 @@
    1.72      simpset()));
    1.73  qed "hypreal_hrinv_less_zero";
    1.74  
    1.75 -Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  1r = 1hr";
    1.76 +Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  #1 = 1hr";
    1.77  by (Step_tac 1);
    1.78  qed "hypreal_of_real_one";
    1.79  
    1.80 -Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  0r = 0hr";
    1.81 +Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  #0 = 0hr";
    1.82  by (Step_tac 1);
    1.83  qed "hypreal_of_real_zero";
    1.84  
    1.85 -Goal "(hypreal_of_real  r = 0hr) = (r = 0r)";
    1.86 +Goal "(hypreal_of_real  r = 0hr) = (r = #0)";
    1.87  by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
    1.88      simpset() addsimps [hypreal_of_real_def,
    1.89      hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
    1.90  qed "hypreal_of_real_zero_iff";
    1.91  
    1.92 -Goal "(hypreal_of_real  r ~= 0hr) = (r ~= 0r)";
    1.93 +Goal "(hypreal_of_real  r ~= 0hr) = (r ~= #0)";
    1.94  by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
    1.95  qed "hypreal_of_real_not_zero_iff";
    1.96  
    1.97 -Goal "r ~= 0r ==> hrinv (hypreal_of_real r) = \
    1.98 +Goal "r ~= #0 ==> hrinv (hypreal_of_real r) = \
    1.99  \          hypreal_of_real (rinv r)";
   1.100  by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
   1.101  by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
   1.102 @@ -1665,6 +1667,7 @@
   1.103  qed "hypreal_three_squares_add_zero_iff";
   1.104  Addsimps [hypreal_three_squares_add_zero_iff];
   1.105  
   1.106 +Addsimps [rename_numerals thy real_le_square];
   1.107  Goal "(x::hypreal)*x <= x*x + y*y";
   1.108  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.109  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.110 @@ -1679,7 +1682,7 @@
   1.111  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   1.112  by (auto_tac (claset(),simpset() addsimps 
   1.113      [hypreal_mult,hypreal_add,hypreal_le,
   1.114 -    real_le_add_order]));
   1.115 +    rename_numerals thy real_le_add_order]));
   1.116  qed "hypreal_self_le_add_pos2";
   1.117  Addsimps [hypreal_self_le_add_pos2];
   1.118  
   1.119 @@ -1690,13 +1693,15 @@
   1.120  by (full_simp_tac (simpset() addsimps 
   1.121      [pnat_one_iff RS sym,real_of_preal_def]) 1);
   1.122  by (fold_tac [real_one_def]);
   1.123 -by (rtac hypreal_of_real_one 1);
   1.124 +by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
   1.125  qed "hypreal_of_posnat_one";
   1.126  
   1.127  Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
   1.128 -by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
   1.129 -    hypreal_one_def,hypreal_add,hypreal_of_real_def,pnat_two_eq,
   1.130 -    real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ pnat_add_ac) 1);
   1.131 +by (full_simp_tac (simpset() addsimps [real_of_preal_def,
   1.132 +    rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
   1.133 +     hypreal_add,hypreal_of_real_def,pnat_two_eq,hypreal_one_def,
   1.134 +    real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ 
   1.135 +    pnat_add_ac) 1);
   1.136  qed "hypreal_of_posnat_two";
   1.137  
   1.138  Goalw [hypreal_of_posnat_def]
   1.139 @@ -1788,9 +1793,10 @@
   1.140  
   1.141  Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
   1.142  by (auto_tac (claset(),simpset() addsimps 
   1.143 -    [real_of_posnat_rinv_not_zero]));
   1.144 +    [rename_numerals thy real_of_posnat_rinv_not_zero]));
   1.145  qed "hypreal_epsilon_not_zero";
   1.146  
   1.147 +Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];
   1.148  Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
   1.149  by (Simp_tac 1);
   1.150  qed "hypreal_omega_not_zero";