Tweaks for 1 -> 1'
authorpaulson
Tue Aug 07 16:36:52 2001 +0200 (2001-08-07)
changeset 1146802cd5d5bc497
parent 11467 1064effe37f6
child 11469 57b072f00626
Tweaks for 1 -> 1'
src/HOL/GroupTheory/Exponent.ML
src/HOL/GroupTheory/Sylow.ML
src/HOL/GroupTheory/Sylow.thy
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/Series.ML
src/HOL/Integ/NatBin.thy
src/HOL/Integ/NatSimprocs.ML
src/HOL/NatArith.ML
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/Factorization.thy
src/HOL/NumberTheory/Fib.thy
     1.1 --- a/src/HOL/GroupTheory/Exponent.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/GroupTheory/Exponent.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -8,11 +8,11 @@
     1.4  
     1.5  val prime_def = thm "prime_def";
     1.6  
     1.7 -Goalw [prime_def] "p\\<in>prime ==> 1 < p";
     1.8 -by (Blast_tac 1); 
     1.9 +Goalw [prime_def] "p\\<in>prime ==> 1' < p";
    1.10 +by (force_tac (claset(), simpset() addsimps []) 1); 
    1.11  qed "prime_imp_one_less";
    1.12  
    1.13 -Goal "(p\\<in>prime) = (1<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
    1.14 +Goal "(p\\<in>prime) = (1'<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
    1.15  by (auto_tac (claset(), simpset() addsimps [prime_imp_one_less]));  
    1.16  by (blast_tac (claset() addSDs [thm "prime_dvd_mult"]) 1);
    1.17  by (auto_tac (claset(), simpset() addsimps [prime_def]));  
    1.18 @@ -23,6 +23,7 @@
    1.19  by (dres_inst_tac [("x","k")] spec 1);
    1.20  by (asm_full_simp_tac
    1.21      (simpset() addsimps [dvd_mult_cancel1, dvd_mult_cancel2]) 1);  
    1.22 +by Auto_tac; 
    1.23  qed "prime_iff";
    1.24  
    1.25  Goal "p\\<in>prime ==> 0 < p^a";
    1.26 @@ -106,9 +107,7 @@
    1.27  by (res_inst_tac [("P","%x. x <= b * c")] subst 1);
    1.28  by (rtac mult_1_right 1);
    1.29  by (rtac mult_le_mono 1);
    1.30 -by (assume_tac 1);
    1.31 -by (stac Suc_le_eq 1);
    1.32 -by (assume_tac 1);
    1.33 +by Auto_tac; 
    1.34  qed "le_extend_mult";
    1.35  
    1.36  
    1.37 @@ -194,15 +193,15 @@
    1.38  qed_spec_mp "prime_power_dvd_cases";
    1.39  
    1.40  (*needed in this form in Sylow.ML*)
    1.41 -Goal "[| p\\<in>prime; ~(p ^ (r+1) dvd n); p ^ (a+r) dvd n * k |] \
    1.42 +Goal "[| p \\<in> prime; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |] \
    1.43  \     ==> p ^ a dvd k";
    1.44 -by (dres_inst_tac [("a","r+1"), ("b","a")] prime_power_dvd_cases 1);
    1.45 +by (dres_inst_tac [("a","Suc r"), ("b","a")] prime_power_dvd_cases 1);
    1.46  by (assume_tac 1);  
    1.47  by Auto_tac;  
    1.48  qed "div_combine";
    1.49  
    1.50  (*Lemma for power_dvd_bound*)
    1.51 -Goal "1 < p ==> Suc n <= p^n";
    1.52 +Goal "1' < p ==> Suc n <= p^n";
    1.53  by (induct_tac "n" 1);
    1.54  by (Asm_simp_tac 1); 
    1.55  by (Asm_full_simp_tac 1); 
    1.56 @@ -219,7 +218,7 @@
    1.57  qed "Suc_le_power";
    1.58  
    1.59  (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
    1.60 -Goal "[|p^n dvd a;  1 < p;  0 < a|] ==> n < a";
    1.61 +Goal "[|p^n dvd a;  1' < p;  0 < a|] ==> n < a";
    1.62  by (dtac dvd_imp_le 1); 
    1.63  by (dres_inst_tac [("n","n")] Suc_le_power 2); 
    1.64  by Auto_tac;  
    1.65 @@ -254,7 +253,7 @@
    1.66  by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
    1.67  by (rtac Greatest_equality 1); 
    1.68  by (Asm_full_simp_tac 1);
    1.69 -by (blast_tac (claset() addIs [prime_imp_one_less, power_dvd_imp_le]) 1); 
    1.70 +by (asm_simp_tac (simpset() addsimps [prime_imp_one_less, power_dvd_imp_le]) 1); 
    1.71  qed "exponent_power_eq";
    1.72  Addsimps [exponent_power_eq];
    1.73  
    1.74 @@ -268,7 +267,7 @@
    1.75  Addsimps [exponent_eq_0];
    1.76  
    1.77  
    1.78 -(* exponent_mult_add, easy inclusion.  Could weaken p\\<in>prime to 1<p *)
    1.79 +(* exponent_mult_add, easy inclusion.  Could weaken p\\<in>prime to 1'<p *)
    1.80  Goal "[| 0 < a; 0 < b |]  \
    1.81  \     ==> (exponent p a) + (exponent p b) <= exponent p (a * b)";
    1.82  by (case_tac "p \\<in> prime" 1);
    1.83 @@ -313,7 +312,7 @@
    1.84  by (auto_tac (claset() addDs [dvd_mult_left], simpset()));  
    1.85  qed "not_divides_exponent_0";
    1.86  
    1.87 -Goal "exponent p 1 = 0";
    1.88 +Goal "exponent p 1' = 0";
    1.89  by (case_tac "p \\<in> prime" 1);
    1.90  by (auto_tac (claset(), 
    1.91                simpset() addsimps [prime_iff, not_divides_exponent_0]));
    1.92 @@ -358,7 +357,7 @@
    1.93  
    1.94  
    1.95  Goal "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a";
    1.96 -by (res_inst_tac [("m","1")] p_fac_forw_lemma 1);
    1.97 +by (res_inst_tac [("m","1'")] p_fac_forw_lemma 1);
    1.98  by Auto_tac;
    1.99  qed "r_le_a_forw";
   1.100  
   1.101 @@ -423,7 +422,7 @@
   1.102  qed "p_not_div_choose";
   1.103  
   1.104  
   1.105 -Goal "0 < m ==> exponent p ((p^a * m - 1) choose (p^a - 1)) = 0";
   1.106 +Goal "0 < m ==> exponent p ((p^a * m - 1') choose (p^a - 1')) = 0";
   1.107  by (case_tac "p \\<in> prime" 1);
   1.108  by (Asm_simp_tac 2);
   1.109  by (forw_inst_tac [("a","a")] zero_less_prime_power 1);
     2.1 --- a/src/HOL/GroupTheory/Sylow.ML	Mon Aug 06 16:43:40 2001 +0200
     2.2 +++ b/src/HOL/GroupTheory/Sylow.ML	Tue Aug 07 16:36:52 2001 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4                                    le_extend_mult, zero_less_m]) 1); 
     2.5  qed "zero_less_card_calM";
     2.6  
     2.7 -Goal "~(p ^ (exponent p m+ 1) dvd card(calM))";
     2.8 +Goal "~ (p ^ Suc(exponent p m) dvd card(calM))";
     2.9  by (subgoal_tac "exponent p m = exponent p (card calM)" 1);
    2.10   by (asm_full_simp_tac (simpset() addsimps [card_calM, 
    2.11                             zero_less_m RS const_p_fac]) 2);
    2.12 @@ -140,7 +140,7 @@
    2.13  by Auto_tac; 
    2.14  qed "finite_calM";
    2.15  
    2.16 -Goal "\\<exists>M \\<in> calM // RelM. ~(p ^ ((exponent p m)+ 1) dvd card(M))";
    2.17 +Goal "\\<exists>M \\<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))";
    2.18  by (rtac (max_p_div_calM RS contrapos_np) 1); 
    2.19  by (asm_full_simp_tac (simpset() addsimps [finite_calM, 
    2.20                            RelM_equiv RSN(2, equiv_imp_dvd_card)]) 1); 
     3.1 --- a/src/HOL/GroupTheory/Sylow.thy	Mon Aug 06 16:43:40 2001 +0200
     3.2 +++ b/src/HOL/GroupTheory/Sylow.thy	Tue Aug 07 16:36:52 2001 +0200
     3.3 @@ -36,7 +36,7 @@
     3.4      M1 :: "'a set"
     3.5    assumes
     3.6      M_in_quot "M \\<in> calM // RelM"
     3.7 -    not_dvd_M "~(p ^ (exponent p m + 1) dvd card(M))"
     3.8 +    not_dvd_M "~(p ^ Suc(exponent p m) dvd card(M))"
     3.9      M1_in_M   "M1 \\<in> M"
    3.10    defines
    3.11     H_def "H == {g. g\\<in>carrier G & M1 #> g = M1}"
     4.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Mon Aug 06 16:43:40 2001 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Tue Aug 07 16:36:52 2001 +0200
     4.3 @@ -682,7 +682,7 @@
     4.4  Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] 
     4.5        "(0::hypnat) < 1hn";
     4.6  by (res_inst_tac [("x","%n. 0")] exI 1);
     4.7 -by (res_inst_tac [("x","%n. 1")] exI 1);
     4.8 +by (res_inst_tac [("x","%n. 1'")] exI 1);
     4.9  by Auto_tac;
    4.10  qed "hypnat_zero_less_one";
    4.11  
    4.12 @@ -806,11 +806,11 @@
    4.13  by Auto_tac;
    4.14  qed "hypnat_of_nat_le_iff";
    4.15  
    4.16 -Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat  1 = 1hn";
    4.17 +Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat 1' = 1hn";
    4.18  by (Simp_tac 1);
    4.19  qed "hypnat_of_nat_one";
    4.20  
    4.21 -Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat  0 = 0";
    4.22 +Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat 0 = 0";
    4.23  by (Simp_tac 1);
    4.24  qed "hypnat_of_nat_zero";
    4.25  
    4.26 @@ -903,7 +903,7 @@
    4.27  qed "SHNat_hypnat_of_nat";
    4.28  Addsimps [SHNat_hypnat_of_nat];
    4.29  
    4.30 -Goal "hypnat_of_nat 1 : Nats";
    4.31 +Goal "hypnat_of_nat 1' : Nats";
    4.32  by (Simp_tac 1);
    4.33  qed "SHNat_hypnat_of_nat_one";
    4.34  
     5.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Mon Aug 06 16:43:40 2001 +0200
     5.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Tue Aug 07 16:36:52 2001 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4  by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
     5.5  qed "hrealpow_add";
     5.6  
     5.7 -Goal "(r::hypreal) ^ 1 = r";
     5.8 +Goal "(r::hypreal) ^ 1' = r";
     5.9  by (Simp_tac 1);
    5.10  qed "hrealpow_one";
    5.11  Addsimps [hrealpow_one];
     6.1 --- a/src/HOL/Hyperreal/Lim.ML	Mon Aug 06 16:43:40 2001 +0200
     6.2 +++ b/src/HOL/Hyperreal/Lim.ML	Tue Aug 07 16:36:52 2001 +0200
     6.3 @@ -1294,7 +1294,7 @@
     6.4  qed "NSDERIV_cmult_Id";
     6.5  Addsimps [NSDERIV_cmult_Id];
     6.6  
     6.7 -Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
     6.8 +Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
     6.9  by (induct_tac "n" 1);
    6.10  by (dtac (DERIV_Id RS DERIV_mult) 2);
    6.11  by (auto_tac (claset(), 
    6.12 @@ -1306,7 +1306,7 @@
    6.13  qed "DERIV_pow";
    6.14  
    6.15  (* NS version *)
    6.16 -Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
    6.17 +Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
    6.18  by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
    6.19  qed "NSDERIV_pow";
    6.20  
     7.1 --- a/src/HOL/Hyperreal/Series.ML	Mon Aug 06 16:43:40 2001 +0200
     7.2 +++ b/src/HOL/Hyperreal/Series.ML	Tue Aug 07 16:36:52 2001 +0200
     7.3 @@ -191,28 +191,17 @@
     7.4  by (Auto_tac);
     7.5  qed "sumr_zero";
     7.6  
     7.7 -Goal "Suc N <= n --> N <= n - 1";
     7.8 -by (induct_tac "n" 1);
     7.9 -by (Auto_tac);
    7.10 -qed_spec_mp "Suc_le_imp_diff_ge";
    7.11 -
    7.12  Goal "ALL n. N <= n --> f (Suc n) = #0 \
    7.13  \     ==> ALL m n. Suc N <= m --> sumr m n f = #0";   
    7.14  by (rtac sumr_zero 1 THEN Step_tac 1);
    7.15 -by (subgoal_tac "0 < n" 1);
    7.16 -by (dtac Suc_le_imp_diff_ge 1);
    7.17 -by (Auto_tac);
    7.18 +by (case_tac "n" 1);
    7.19 +by Auto_tac; 
    7.20  qed "Suc_le_imp_diff_ge2";
    7.21  
    7.22 -(* proved elsewhere? *)
    7.23 -Goal "(0 < n) = (EX m. n = Suc m)";
    7.24 +Goal "sumr 1' n (%n. f(n) * #0 ^ n) = #0";
    7.25  by (induct_tac "n" 1);
    7.26 -by (Auto_tac);
    7.27 -qed "gt_zero_eq_Ex";
    7.28 -
    7.29 -Goal "sumr 1 n (%n. f(n) * #0 ^ n) = #0";
    7.30 -by (induct_tac "n" 1);
    7.31 -by (auto_tac (claset(),simpset() addsimps [gt_zero_eq_Ex]));
    7.32 +by (case_tac "n" 2);
    7.33 +by Auto_tac; 
    7.34  qed "sumr_one_lb_realpow_zero";
    7.35  Addsimps [sumr_one_lb_realpow_zero];
    7.36  
    7.37 @@ -220,7 +209,7 @@
    7.38  by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1);
    7.39  qed "sumr_diff";
    7.40  
    7.41 -Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumr m n f = sumr m n g";
    7.42 +Goal "(ALL p. m <= p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g";
    7.43  by (induct_tac "n" 1);
    7.44  by (Auto_tac);
    7.45  qed_spec_mp "sumr_subst";
    7.46 @@ -564,7 +553,8 @@
    7.47  by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
    7.48  by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
    7.49  by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
    7.50 -by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
    7.51 +by (res_inst_tac [("x","Suc N")] exI 1);
    7.52 +by (Clarify_tac 1); 
    7.53  by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
    7.54  qed "ratio_test_lemma2";
    7.55  
     8.1 --- a/src/HOL/Integ/NatBin.thy	Mon Aug 06 16:43:40 2001 +0200
     8.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Aug 07 16:36:52 2001 +0200
     8.3 @@ -18,10 +18,6 @@
     8.4      "number_of v == nat (number_of v)"
     8.5       (*::bin=>nat        ::bin=>int*)
     8.6  
     8.7 -axioms
     8.8 -neg_number_of_bin_pred_iff_0:
     8.9 -  "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
    8.10 -
    8.11  use "nat_bin.ML"	setup nat_bin_arith_setup
    8.12  
    8.13  end
     9.1 --- a/src/HOL/Integ/NatSimprocs.ML	Mon Aug 06 16:43:40 2001 +0200
     9.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Tue Aug 07 16:36:52 2001 +0200
     9.3 @@ -14,15 +14,12 @@
     9.4  
     9.5  (*Now just instantiating n to (number_of v) does the right simplification,
     9.6    but with some redundant inequality tests.*)
     9.7 -(*
     9.8  Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
     9.9 -by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
    9.10 -by (Asm_simp_tac 1);
    9.11 +by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1')" 1);
    9.12 +by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1); 
    9.13  by (stac less_number_of_Suc 1);
    9.14  by (Simp_tac 1);
    9.15  qed "neg_number_of_bin_pred_iff_0";
    9.16 -*)
    9.17 -val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0";
    9.18  
    9.19  Goal "neg (number_of (bin_minus v)) ==> \
    9.20  \     Suc m - (number_of v) = m - (number_of (bin_pred v))";
    10.1 --- a/src/HOL/NatArith.ML	Mon Aug 06 16:43:40 2001 +0200
    10.2 +++ b/src/HOL/NatArith.ML	Tue Aug 07 16:36:52 2001 +0200
    10.3 @@ -96,17 +96,17 @@
    10.4  
    10.5  (** Lemmas for ex/Factorization **)
    10.6  
    10.7 -Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
    10.8 +Goal "!!m::nat. [| 1' < n; 1' < m |] ==> 1' < m*n";
    10.9  by (case_tac "m" 1);
   10.10  by Auto_tac;
   10.11  qed "one_less_mult"; 
   10.12  
   10.13 -Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
   10.14 +Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<m*n";
   10.15  by (case_tac "m" 1);
   10.16  by Auto_tac;
   10.17  qed "n_less_m_mult_n"; 
   10.18  
   10.19 -Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
   10.20 +Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<n*m";
   10.21  by (case_tac "m" 1);
   10.22  by Auto_tac;
   10.23  qed "n_less_n_mult_m"; 
    11.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Aug 06 16:43:40 2001 +0200
    11.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Tue Aug 07 16:36:52 2001 +0200
    11.3 @@ -56,9 +56,9 @@
    11.4  
    11.5    mhf_def:
    11.6      "mhf mf n i ==
    11.7 -      if i = 0 then funprod mf 1 (n - 1)
    11.8 -      else if i = n then funprod mf 0 (n - 1)
    11.9 -      else funprod mf 0 (i - 1) * funprod mf (i + 1) (n - 1 - i)"
   11.10 +      if i = 0 then funprod mf 1' (n - 1')
   11.11 +      else if i = n then funprod mf 0 (n - 1')
   11.12 +      else funprod mf 0 (i - 1') * funprod mf (Suc i) (n - 1' - i)"
   11.13  
   11.14    xilin_sol_def:
   11.15      "xilin_sol i n kf bf mf ==
    12.1 --- a/src/HOL/NumberTheory/Factorization.thy	Mon Aug 06 16:43:40 2001 +0200
    12.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Tue Aug 07 16:36:52 2001 +0200
    12.3 @@ -26,7 +26,7 @@
    12.4    "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
    12.5  
    12.6  primrec
    12.7 -  "prod [] = 1"
    12.8 +  "prod [] = 1'"
    12.9    "prod (x # xs) = x * prod xs"
   12.10  
   12.11  primrec
   12.12 @@ -40,12 +40,12 @@
   12.13  
   12.14  subsection {* Arithmetic *}
   12.15  
   12.16 -lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1 ==> 1 < m"
   12.17 +lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1' ==> 1' < m"
   12.18    apply (case_tac m)
   12.19     apply auto
   12.20    done
   12.21  
   12.22 -lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1 < m * k ==> 1 < k"
   12.23 +lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1' < m * k ==> 1' < k"
   12.24    apply (case_tac k)
   12.25     apply auto
   12.26    done
   12.27 @@ -54,13 +54,13 @@
   12.28    apply auto
   12.29    done
   12.30  
   12.31 -lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1"
   12.32 +lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1'"
   12.33    apply (case_tac n)
   12.34     apply auto
   12.35    done
   12.36  
   12.37  lemma prod_mn_less_k:
   12.38 -    "(0::nat) < n ==> 0 < k ==> 1 < m ==> m * n = k ==> n < k"
   12.39 +    "(0::nat) < n ==> 0 < k ==> 1' < m ==> m * n = k ==> n < k"
   12.40    apply (induct m)
   12.41     apply auto
   12.42    done
   12.43 @@ -88,7 +88,7 @@
   12.44    apply auto
   12.45    done
   12.46  
   12.47 -lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1"
   12.48 +lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1'"
   12.49    apply (unfold prime_def dvd_def)
   12.50    apply auto
   12.51    done
   12.52 @@ -115,13 +115,13 @@
   12.53    apply auto
   12.54    done
   12.55  
   12.56 -lemma primel_one_empty: "primel xs ==> prod xs = 1 ==> xs = []"
   12.57 +lemma primel_one_empty: "primel xs ==> prod xs = 1' ==> xs = []"
   12.58    apply (unfold primel_def prime_def)
   12.59    apply (case_tac xs)
   12.60     apply simp_all
   12.61    done
   12.62  
   12.63 -lemma prime_g_one: "p \<in> prime ==> 1 < p"
   12.64 +lemma prime_g_one: "p \<in> prime ==> 1' < p"
   12.65    apply (unfold prime_def)
   12.66    apply auto
   12.67    done
   12.68 @@ -132,7 +132,7 @@
   12.69    done
   12.70  
   12.71  lemma primel_nempty_g_one [rule_format]:
   12.72 -    "primel xs --> xs \<noteq> [] --> 1 < prod xs"
   12.73 +    "primel xs --> xs \<noteq> [] --> 1' < prod xs"
   12.74    apply (unfold primel_def prime_def)
   12.75    apply (induct xs)
   12.76     apply (auto elim: one_less_mult)
   12.77 @@ -223,8 +223,8 @@
   12.78    done
   12.79  
   12.80  lemma not_prime_ex_mk:
   12.81 -  "1 < n \<and> n \<notin> prime ==>
   12.82 -    \<exists>m k. 1 < m \<and> 1 < k \<and> m < n \<and> k < n \<and> n = m * k"
   12.83 +  "1' < n \<and> n \<notin> prime ==>
   12.84 +    \<exists>m k. 1' < m \<and> 1' < k \<and> m < n \<and> k < n \<and> n = m * k"
   12.85    apply (unfold prime_def dvd_def)
   12.86    apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
   12.87    done
   12.88 @@ -237,7 +237,7 @@
   12.89    apply (simp add: primel_append)
   12.90    done
   12.91  
   12.92 -lemma factor_exists [rule_format]: "1 < n --> (\<exists>l. primel l \<and> prod l = n)"
   12.93 +lemma factor_exists [rule_format]: "1' < n --> (\<exists>l. primel l \<and> prod l = n)"
   12.94    apply (induct n rule: nat_less_induct)
   12.95    apply (rule impI)
   12.96    apply (case_tac "n \<in> prime")
   12.97 @@ -247,7 +247,7 @@
   12.98     apply (auto intro!: split_primel)
   12.99    done
  12.100  
  12.101 -lemma nondec_factor_exists: "1 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
  12.102 +lemma nondec_factor_exists: "1' < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
  12.103    apply (erule factor_exists [THEN exE])
  12.104    apply (blast intro!: ex_nondec_lemma)
  12.105    done
  12.106 @@ -349,7 +349,7 @@
  12.107    done
  12.108  
  12.109  lemma unique_prime_factorization [rule_format]:
  12.110 -    "\<forall>n. 1 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
  12.111 +    "\<forall>n. 1' < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
  12.112    apply safe
  12.113     apply (erule nondec_factor_exists)
  12.114    apply (rule perm_nondec_unique)
    13.1 --- a/src/HOL/NumberTheory/Fib.thy	Mon Aug 06 16:43:40 2001 +0200
    13.2 +++ b/src/HOL/NumberTheory/Fib.thy	Tue Aug 07 16:36:52 2001 +0200
    13.3 @@ -18,8 +18,8 @@
    13.4  
    13.5  consts fib :: "nat => nat"
    13.6  recdef fib  less_than
    13.7 -  zero: "fib 0 = 0"
    13.8 -  one:  "fib 1 = 1"
    13.9 +  zero: "fib 0  = 0"
   13.10 +  one:  "fib 1' = 1'"
   13.11    Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)"
   13.12  
   13.13  text {*
   13.14 @@ -81,7 +81,7 @@
   13.15  
   13.16  text {* \medskip Towards Law 6.111 of Concrete Mathematics *}
   13.17  
   13.18 -lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1"
   13.19 +lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1'"
   13.20    apply (induct n rule: fib.induct)
   13.21      prefer 3
   13.22      apply (simp add: gcd_commute fib_Suc3)