src/HOL/Real/PRat.ML
changeset 11464 ddea204de5bc
parent 10834 a7897aebbffc
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Real/PRat.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Real/PRat.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  qed "inj_qinv";
     1.5  
     1.6  Goalw [prat_of_pnat_def] 
     1.7 -      "qinv(prat_of_pnat  (Abs_pnat 1)) = prat_of_pnat (Abs_pnat 1)";
     1.8 +      "qinv(prat_of_pnat  (Abs_pnat 1')) = prat_of_pnat (Abs_pnat 1')";
     1.9  by (simp_tac (simpset() addsimps [qinv]) 1);
    1.10  qed "qinv_1";
    1.11  
    1.12 @@ -232,13 +232,13 @@
    1.13                      prat_mult_commute,prat_mult_left_commute]);
    1.14  
    1.15  Goalw [prat_of_pnat_def] 
    1.16 -      "(prat_of_pnat (Abs_pnat 1)) * z = z";
    1.17 +      "(prat_of_pnat (Abs_pnat 1')) * z = z";
    1.18  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
    1.19  by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
    1.20  qed "prat_mult_1";
    1.21  
    1.22  Goalw [prat_of_pnat_def] 
    1.23 -      "z * (prat_of_pnat (Abs_pnat 1)) = z";
    1.24 +      "z * (prat_of_pnat (Abs_pnat 1')) = z";
    1.25  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
    1.26  by (asm_full_simp_tac (simpset() addsimps [prat_mult] @ pnat_mult_ac) 1);
    1.27  qed "prat_mult_1_right";
    1.28 @@ -259,22 +259,22 @@
    1.29  (*** prat_mult and qinv ***)
    1.30  
    1.31  Goalw [prat_def,prat_of_pnat_def] 
    1.32 -      "qinv (q) * q = prat_of_pnat (Abs_pnat 1)";
    1.33 +      "qinv (q) * q = prat_of_pnat (Abs_pnat 1')";
    1.34  by (res_inst_tac [("z","q")] eq_Abs_prat 1);
    1.35  by (asm_full_simp_tac (simpset() addsimps [qinv,
    1.36          prat_mult,pnat_mult_1,pnat_mult_1_left, pnat_mult_commute]) 1);
    1.37  qed "prat_mult_qinv";
    1.38  
    1.39 -Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1)";
    1.40 +Goal "q * qinv (q) = prat_of_pnat (Abs_pnat 1')";
    1.41  by (rtac (prat_mult_commute RS subst) 1);
    1.42  by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
    1.43  qed "prat_mult_qinv_right";
    1.44  
    1.45 -Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
    1.46 +Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
    1.47  by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
    1.48  qed "prat_qinv_ex";
    1.49  
    1.50 -Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
    1.51 +Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1')";
    1.52  by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
    1.53  by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
    1.54  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
    1.55 @@ -282,7 +282,7 @@
    1.56      prat_mult_1,prat_mult_1_right]) 1);
    1.57  qed "prat_qinv_ex1";
    1.58  
    1.59 -Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
    1.60 +Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1')";
    1.61  by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
    1.62  by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
    1.63  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
    1.64 @@ -290,7 +290,7 @@
    1.65      prat_mult_1,prat_mult_1_right]) 1);
    1.66  qed "prat_qinv_left_ex1";
    1.67  
    1.68 -Goal "x * y = prat_of_pnat (Abs_pnat 1) ==> x = qinv y";
    1.69 +Goal "x * y = prat_of_pnat (Abs_pnat 1') ==> x = qinv y";
    1.70  by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
    1.71  by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
    1.72  by (Blast_tac 1);
    1.73 @@ -506,7 +506,7 @@
    1.74  by (cut_inst_tac [("x","q1"),("q1.0","qinv (q1)"), ("q2.0","qinv (q2)")] 
    1.75      prat_mult_left_less2_mono1 1);
    1.76  by Auto_tac;
    1.77 -by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1)")] prat_less_trans 1);
    1.78 +by (dres_inst_tac [("q2.0","prat_of_pnat (Abs_pnat 1')")] prat_less_trans 1);
    1.79  by (auto_tac (claset(),simpset() addsimps 
    1.80      [prat_less_not_refl]));
    1.81  qed "lemma2_qinv_prat_less";
    1.82 @@ -517,8 +517,8 @@
    1.83                   lemma2_qinv_prat_less],simpset()));
    1.84  qed "qinv_prat_less";
    1.85  
    1.86 -Goal "q1 < prat_of_pnat (Abs_pnat 1) \
    1.87 -\     ==> prat_of_pnat (Abs_pnat 1) < qinv(q1)";
    1.88 +Goal "q1 < prat_of_pnat (Abs_pnat 1') \
    1.89 +\     ==> prat_of_pnat (Abs_pnat 1') < qinv(q1)";
    1.90  by (dtac qinv_prat_less 1);
    1.91  by (full_simp_tac (simpset() addsimps [qinv_1]) 1);
    1.92  qed "prat_qinv_gt_1";
    1.93 @@ -529,18 +529,18 @@
    1.94  qed "prat_qinv_is_gt_1";
    1.95  
    1.96  Goalw [prat_less_def] 
    1.97 -      "prat_of_pnat (Abs_pnat 1) < prat_of_pnat (Abs_pnat 1) \
    1.98 -\                   + prat_of_pnat (Abs_pnat 1)";
    1.99 +      "prat_of_pnat (Abs_pnat 1') < prat_of_pnat (Abs_pnat 1') \
   1.100 +\                   + prat_of_pnat (Abs_pnat 1')";
   1.101  by (Fast_tac 1); 
   1.102  qed "prat_less_1_2";
   1.103  
   1.104 -Goal "qinv(prat_of_pnat (Abs_pnat 1) + \
   1.105 -\     prat_of_pnat (Abs_pnat 1)) < prat_of_pnat (Abs_pnat 1)";
   1.106 +Goal "qinv(prat_of_pnat (Abs_pnat 1') + \
   1.107 +\     prat_of_pnat (Abs_pnat 1')) < prat_of_pnat (Abs_pnat 1')";
   1.108  by (cut_facts_tac [prat_less_1_2 RS qinv_prat_less] 1);
   1.109  by (asm_full_simp_tac (simpset() addsimps [qinv_1]) 1);
   1.110  qed "prat_less_qinv_2_1";
   1.111  
   1.112 -Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1)";
   1.113 +Goal "!!(x::prat). x < y ==> x*qinv(y) < prat_of_pnat (Abs_pnat 1')";
   1.114  by (dres_inst_tac [("x","qinv(y)")] prat_mult_less2_mono1 1);
   1.115  by (Asm_full_simp_tac 1);
   1.116  qed "prat_mult_qinv_less_1";
   1.117 @@ -701,19 +701,19 @@
   1.118      pnat_mult_1]));
   1.119  qed "Abs_prat_mult_qinv";
   1.120  
   1.121 -Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1)})";
   1.122 +Goal "Abs_prat(ratrel``{(x,y)}) <= Abs_prat(ratrel``{(x,Abs_pnat 1')})";
   1.123  by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
   1.124  by (rtac prat_mult_left_le2_mono1 1);
   1.125  by (rtac qinv_prat_le 1);
   1.126  by (pnat_ind_tac "y" 1);
   1.127 -by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] prat_add_le2_mono1 2);
   1.128 +by (dres_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] prat_add_le2_mono1 2);
   1.129  by (cut_facts_tac [prat_less_1_2 RS prat_less_imp_le] 2);
   1.130  by (auto_tac (claset() addIs [prat_le_trans],
   1.131      simpset() addsimps [prat_le_refl,
   1.132      pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add]));
   1.133  qed "lemma_Abs_prat_le1";
   1.134  
   1.135 -Goal "Abs_prat(ratrel``{(x,Abs_pnat 1)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
   1.136 +Goal "Abs_prat(ratrel``{(x,Abs_pnat 1')}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
   1.137  by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1);
   1.138  by (rtac prat_mult_le2_mono1 1);
   1.139  by (pnat_ind_tac "y" 1);
   1.140 @@ -726,19 +726,19 @@
   1.141  			prat_of_pnat_add,prat_of_pnat_mult]));
   1.142  qed "lemma_Abs_prat_le2";
   1.143  
   1.144 -Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1)})";
   1.145 +Goal "Abs_prat(ratrel``{(x,z)}) <= Abs_prat(ratrel``{(x*y,Abs_pnat 1')})";
   1.146  by (fast_tac (claset() addIs [prat_le_trans,
   1.147  			      lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1);
   1.148  qed "lemma_Abs_prat_le3";
   1.149  
   1.150 -Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel``{(w,x)}) = \
   1.151 -\         Abs_prat(ratrel``{(w*y,Abs_pnat 1)})";
   1.152 +Goal "Abs_prat(ratrel``{(x*y,Abs_pnat 1')}) * Abs_prat(ratrel``{(w,x)}) = \
   1.153 +\         Abs_prat(ratrel``{(w*y,Abs_pnat 1')})";
   1.154  by (full_simp_tac (simpset() addsimps [prat_mult,
   1.155      pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1);
   1.156  qed "pre_lemma_gleason9_34";
   1.157  
   1.158 -Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1*y)}) = \
   1.159 -\         Abs_prat(ratrel``{(x,Abs_pnat 1)})";
   1.160 +Goal "Abs_prat(ratrel``{(y*x,Abs_pnat 1'*y)}) = \
   1.161 +\         Abs_prat(ratrel``{(x,Abs_pnat 1')})";
   1.162  by (auto_tac (claset(),
   1.163  	      simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac));
   1.164  qed "pre_lemma_gleason9_34b";
   1.165 @@ -760,42 +760,42 @@
   1.166  (*** of preal type as defined using Dedekind Sections in PReal  ***)
   1.167  (*** Show that exists positive real `one' ***)
   1.168  
   1.169 -Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
   1.170 +Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
   1.171  by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
   1.172  qed "lemma_prat_less_1_memEx";
   1.173  
   1.174 -Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {}";
   1.175 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= {}";
   1.176  by (rtac notI 1);
   1.177  by (cut_facts_tac [lemma_prat_less_1_memEx] 1);
   1.178  by (Asm_full_simp_tac 1);
   1.179  qed "lemma_prat_less_1_set_non_empty";
   1.180  
   1.181 -Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
   1.182 +Goalw [psubset_def] "{} < {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
   1.183  by (asm_full_simp_tac (simpset() addsimps 
   1.184           [lemma_prat_less_1_set_non_empty RS not_sym]) 1);
   1.185  qed "empty_set_psubset_lemma_prat_less_1_set";
   1.186  
   1.187  (*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
   1.188 -Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
   1.189 -by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
   1.190 +Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1')}";
   1.191 +by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1')")] exI 1);
   1.192  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   1.193  qed "lemma_prat_less_1_not_memEx";
   1.194  
   1.195 -Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= UNIV";
   1.196 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} ~= UNIV";
   1.197  by (rtac notI 1);
   1.198  by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
   1.199  by (Asm_full_simp_tac 1);
   1.200  qed "lemma_prat_less_1_set_not_rat_set";
   1.201  
   1.202  Goalw [psubset_def,subset_def] 
   1.203 -      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < UNIV";
   1.204 +      "{x::prat. x < prat_of_pnat (Abs_pnat 1')} < UNIV";
   1.205  by (asm_full_simp_tac
   1.206      (simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
   1.207  			 lemma_prat_less_1_not_memEx]) 1);
   1.208  qed "lemma_prat_less_1_set_psubset_rat_set";
   1.209  
   1.210  (*** prove non_emptiness of type ***)
   1.211 -Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
   1.212 +Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : {A. {} < A & \
   1.213  \               A < UNIV & \
   1.214  \               (!y: A. ((!z. z < y --> z: A) & \
   1.215  \               (EX u: A. y < u)))}";