src/HOL/Real/PReal.ML
changeset 11464 ddea204de5bc
parent 10834 a7897aebbffc
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Real/PReal.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Real/PReal.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  
     1.5  Addsimps [empty_not_mem_preal];
     1.6  
     1.7 -Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : preal";
     1.8 +Goalw [preal_def] "{x::prat. x < prat_of_pnat (Abs_pnat 1')} : preal";
     1.9  by (rtac preal_1 1);
    1.10  qed "one_set_mem_preal";
    1.11  
    1.12 @@ -234,9 +234,9 @@
    1.13  \         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
    1.14  by Auto_tac;
    1.15  by (ftac prat_mult_qinv_less_1 1);
    1.16 -by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
    1.17 +by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1')")] 
    1.18      prat_mult_less2_mono1 1);
    1.19 -by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
    1.20 +by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1')")] 
    1.21      prat_mult_less2_mono1 1);
    1.22  by (Asm_full_simp_tac 1);
    1.23  by (REPEAT(dtac (Rep_preal RS prealE_lemma3a) 1));
    1.24 @@ -367,7 +367,7 @@
    1.25  (* Positive Real 1 is the multiplicative identity element *) 
    1.26  (* long *)
    1.27  Goalw [preal_of_prat_def,preal_mult_def] 
    1.28 -      "(preal_of_prat (prat_of_pnat (Abs_pnat 1))) * z = z";
    1.29 +      "(preal_of_prat (prat_of_pnat (Abs_pnat 1'))) * z = z";
    1.30  by (rtac (Rep_preal_inverse RS subst) 1);
    1.31  by (res_inst_tac [("f","Abs_preal")] arg_cong 1);
    1.32  by (rtac (one_set_mem_preal RS Abs_preal_inverse RS ssubst) 1);
    1.33 @@ -382,7 +382,7 @@
    1.34  by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
    1.35  qed "preal_mult_1";
    1.36  
    1.37 -Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1))) = z";
    1.38 +Goal "z * (preal_of_prat (prat_of_pnat (Abs_pnat 1'))) = z";
    1.39  by (rtac (preal_mult_commute RS subst) 1);
    1.40  by (rtac preal_mult_1 1);
    1.41  qed "preal_mult_1_right";
    1.42 @@ -563,7 +563,7 @@
    1.43  
    1.44  (*more lemmas for inverse *)
    1.45  Goal "x: Rep_preal(pinv(A)*A) ==> \
    1.46 -\     x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
    1.47 +\     x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
    1.48  by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
    1.49                simpset() addsimps [pinv_def,preal_of_prat_def] ));
    1.50  by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
    1.51 @@ -583,8 +583,8 @@
    1.52  qed "lemma1_gleason9_34";
    1.53  
    1.54  Goal "Abs_prat (ratrel `` {(y, z)}) < xb + \
    1.55 -\         Abs_prat (ratrel `` {(x*y, Abs_pnat 1)})*Abs_prat (ratrel `` {(w, x)})";
    1.56 -by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat 1)}) *\
    1.57 +\         Abs_prat (ratrel `` {(x*y, Abs_pnat 1')})*Abs_prat (ratrel `` {(w, x)})";
    1.58 +by (res_inst_tac [("j","Abs_prat (ratrel `` {(x * y, Abs_pnat 1')}) *\
    1.59  \                   Abs_prat (ratrel `` {(w, x)})")] prat_le_less_trans 1);
    1.60  by (rtac prat_self_less_add_right 2);
    1.61  by (auto_tac (claset() addIs [lemma_Abs_prat_le3],
    1.62 @@ -650,14 +650,14 @@
    1.63  by Auto_tac;
    1.64  qed "lemma_gleason9_36";
    1.65  
    1.66 -Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
    1.67 +Goal "prat_of_pnat (Abs_pnat 1') < x ==> \
    1.68  \     EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
    1.69  by (rtac lemma_gleason9_36 1);
    1.70  by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
    1.71  qed "lemma_gleason9_36a";
    1.72  
    1.73  (*** Part 2 of existence of inverse ***)
    1.74 -Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1))) \
    1.75 +Goal "x: Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat 1'))) \
    1.76  \     ==> x: Rep_preal(pinv(A)*A)";
    1.77  by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
    1.78                simpset() addsimps [pinv_def,preal_of_prat_def] ));
    1.79 @@ -677,12 +677,12 @@
    1.80      prat_mult_left_commute]));
    1.81  qed "preal_mem_mult_invI";
    1.82  
    1.83 -Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
    1.84 +Goal "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
    1.85  by (rtac (inj_Rep_preal RS injD) 1);
    1.86  by (fast_tac (claset() addDs [preal_mem_mult_invD,preal_mem_mult_invI]) 1);
    1.87  qed "preal_mult_inv";
    1.88  
    1.89 -Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
    1.90 +Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1')))";
    1.91  by (rtac (preal_mult_commute RS subst) 1);
    1.92  by (rtac preal_mult_inv 1);
    1.93  qed "preal_mult_inv_right";