src/HOL/NumberTheory/Factorization.thy
changeset 11701 3d51fbf81c17
parent 11468 02cd5d5bc497
child 15236 f289e8ba2bb3
     1.1 --- a/src/HOL/NumberTheory/Factorization.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
     1.5  
     1.6  primrec
     1.7 -  "prod [] = 1'"
     1.8 +  "prod [] = Suc 0"
     1.9    "prod (x # xs) = x * prod xs"
    1.10  
    1.11  primrec
    1.12 @@ -40,12 +40,12 @@
    1.13  
    1.14  subsection {* Arithmetic *}
    1.15  
    1.16 -lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1' ==> 1' < m"
    1.17 +lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
    1.18    apply (case_tac m)
    1.19     apply auto
    1.20    done
    1.21  
    1.22 -lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1' < m * k ==> 1' < k"
    1.23 +lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k"
    1.24    apply (case_tac k)
    1.25     apply auto
    1.26    done
    1.27 @@ -54,13 +54,13 @@
    1.28    apply auto
    1.29    done
    1.30  
    1.31 -lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1'"
    1.32 +lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
    1.33    apply (case_tac n)
    1.34     apply auto
    1.35    done
    1.36  
    1.37  lemma prod_mn_less_k:
    1.38 -    "(0::nat) < n ==> 0 < k ==> 1' < m ==> m * n = k ==> n < k"
    1.39 +    "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
    1.40    apply (induct m)
    1.41     apply auto
    1.42    done
    1.43 @@ -88,7 +88,7 @@
    1.44    apply auto
    1.45    done
    1.46  
    1.47 -lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1'"
    1.48 +lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd Suc 0"
    1.49    apply (unfold prime_def dvd_def)
    1.50    apply auto
    1.51    done
    1.52 @@ -115,13 +115,13 @@
    1.53    apply auto
    1.54    done
    1.55  
    1.56 -lemma primel_one_empty: "primel xs ==> prod xs = 1' ==> xs = []"
    1.57 +lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
    1.58    apply (unfold primel_def prime_def)
    1.59    apply (case_tac xs)
    1.60     apply simp_all
    1.61    done
    1.62  
    1.63 -lemma prime_g_one: "p \<in> prime ==> 1' < p"
    1.64 +lemma prime_g_one: "p \<in> prime ==> Suc 0 < p"
    1.65    apply (unfold prime_def)
    1.66    apply auto
    1.67    done
    1.68 @@ -132,7 +132,7 @@
    1.69    done
    1.70  
    1.71  lemma primel_nempty_g_one [rule_format]:
    1.72 -    "primel xs --> xs \<noteq> [] --> 1' < prod xs"
    1.73 +    "primel xs --> xs \<noteq> [] --> Suc 0 < prod xs"
    1.74    apply (unfold primel_def prime_def)
    1.75    apply (induct xs)
    1.76     apply (auto elim: one_less_mult)
    1.77 @@ -223,8 +223,8 @@
    1.78    done
    1.79  
    1.80  lemma not_prime_ex_mk:
    1.81 -  "1' < n \<and> n \<notin> prime ==>
    1.82 -    \<exists>m k. 1' < m \<and> 1' < k \<and> m < n \<and> k < n \<and> n = m * k"
    1.83 +  "Suc 0 < n \<and> n \<notin> prime ==>
    1.84 +    \<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
    1.85    apply (unfold prime_def dvd_def)
    1.86    apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
    1.87    done
    1.88 @@ -237,7 +237,7 @@
    1.89    apply (simp add: primel_append)
    1.90    done
    1.91  
    1.92 -lemma factor_exists [rule_format]: "1' < n --> (\<exists>l. primel l \<and> prod l = n)"
    1.93 +lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)"
    1.94    apply (induct n rule: nat_less_induct)
    1.95    apply (rule impI)
    1.96    apply (case_tac "n \<in> prime")
    1.97 @@ -247,7 +247,7 @@
    1.98     apply (auto intro!: split_primel)
    1.99    done
   1.100  
   1.101 -lemma nondec_factor_exists: "1' < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
   1.102 +lemma nondec_factor_exists: "Suc 0 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
   1.103    apply (erule factor_exists [THEN exE])
   1.104    apply (blast intro!: ex_nondec_lemma)
   1.105    done
   1.106 @@ -349,7 +349,7 @@
   1.107    done
   1.108  
   1.109  lemma unique_prime_factorization [rule_format]:
   1.110 -    "\<forall>n. 1' < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
   1.111 +    "\<forall>n. Suc 0 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
   1.112    apply safe
   1.113     apply (erule nondec_factor_exists)
   1.114    apply (rule perm_nondec_unique)