src/HOL/Real/PNat.ML
changeset 11464 ddea204de5bc
parent 10834 a7897aebbffc
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Real/PNat.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Real/PNat.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -6,13 +6,13 @@
     1.4  The positive naturals -- proofs mainly as in theory Nat.
     1.5  *)
     1.6  
     1.7 -Goal "mono(%X. {1} Un Suc`X)";
     1.8 +Goal "mono(%X. {1'} Un Suc`X)";
     1.9  by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    1.10  qed "pnat_fun_mono";
    1.11  
    1.12  bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_unfold));
    1.13  
    1.14 -Goal "1 : pnat";
    1.15 +Goal "1' : pnat";
    1.16  by (stac pnat_unfold 1);
    1.17  by (rtac (singletonI RS UnI1) 1);
    1.18  qed "one_RepI";
    1.19 @@ -31,7 +31,7 @@
    1.20  (*** Induction ***)
    1.21  
    1.22  val major::prems = Goal
    1.23 -    "[| i: pnat;  P(1);   \
    1.24 +    "[| i: pnat;  P(1');   \
    1.25  \       !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |]  ==> P(i)";
    1.26  by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_lfp_induct) 1);
    1.27  by (blast_tac (claset() addIs prems) 1);
    1.28 @@ -250,7 +250,7 @@
    1.29  (*** Rep_pnat < 0 ==> P ***)
    1.30  bind_thm ("Rep_pnat_less_zeroE",Rep_pnat_not_less0 RS notE);
    1.31  
    1.32 -Goal "~ Rep_pnat y < 1";
    1.33 +Goal "~ Rep_pnat y < 1'";
    1.34  by (auto_tac (claset(),simpset() addsimps [less_Suc_eq,
    1.35                    Rep_pnat_gt_zero,less_not_refl2]));
    1.36  qed "Rep_pnat_not_less_one";
    1.37 @@ -259,7 +259,7 @@
    1.38  bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
    1.39  
    1.40  Goalw [pnat_less_def] 
    1.41 -     "x < (y::pnat) ==> Rep_pnat y ~= 1";
    1.42 +     "x < (y::pnat) ==> Rep_pnat y ~= 1'";
    1.43  by (auto_tac (claset(),simpset() 
    1.44      addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
    1.45  qed "Rep_pnat_gt_implies_not0";
    1.46 @@ -270,7 +270,7 @@
    1.47  by (fast_tac (claset() addIs [inj_Rep_pnat RS injD]) 1);
    1.48  qed "pnat_less_linear";
    1.49  
    1.50 -Goalw [le_def] "1 <= Rep_pnat x";
    1.51 +Goalw [le_def] "1' <= Rep_pnat x";
    1.52  by (rtac Rep_pnat_not_less_one 1);
    1.53  qed "Rep_pnat_le_one";
    1.54  
    1.55 @@ -416,12 +416,12 @@
    1.56            Abs_pnat_inverse,mult_left_commute]) 1);
    1.57  qed "pnat_mult_left_commute";
    1.58  
    1.59 -Goalw [pnat_mult_def] "x * (Abs_pnat 1) = x";
    1.60 +Goalw [pnat_mult_def] "x * (Abs_pnat 1') = x";
    1.61  by (full_simp_tac (simpset() addsimps [one_RepI RS Abs_pnat_inverse,
    1.62                     Rep_pnat_inverse]) 1);
    1.63  qed "pnat_mult_1";
    1.64  
    1.65 -Goal "Abs_pnat 1 * x = x";
    1.66 +Goal "Abs_pnat 1' * x = x";
    1.67  by (full_simp_tac (simpset() addsimps [pnat_mult_1,
    1.68                     pnat_mult_commute]) 1);
    1.69  qed "pnat_mult_1_left";