src/HOL/Old_Number_Theory/Factorization.thy

 (*  Title:      HOL/Old_Number_Theory/Factorization.thy
     Author:     Thomas Marthedal Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
-section {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
+section \<open>Fundamental Theorem of Arithmetic (unique factorization into primes)\<close>
 
 theory Factorization
 imports Primes "~~/src/HOL/Library/Permutation"
 begin
 
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 definition primel :: "nat list => bool"
   where "primel xs = (\<forall>p \<in> set xs. prime p)"
 
 primrec nondec :: "nat list => bool"

 where
   "sort [] = []"
 | "sort (x # xs) = oinsert x (sort xs)"
 
 
-subsection {* Arithmetic *}
+subsection \<open>Arithmetic\<close>
 
 lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
   apply (cases m)
    apply auto
   done

   apply (induct m)
    apply auto
   done
 
 
-subsection {* Prime list and product *}
+subsection \<open>Prime list and product\<close>
 
 lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
   apply (induct xs)
    apply (simp_all add: mult.assoc)
   done

   apply (induct xs)
    apply (auto simp: primel_def prime_def)
   done
 
 
-subsection {* Sorting *}
+subsection \<open>Sorting\<close>
 
 lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
   apply (induct xs)
    apply simp
    apply (case_tac xs)

   apply (induct l)
   apply auto
   done
 
 
-subsection {* Permutation *}
+subsection \<open>Permutation\<close>
 
 lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   apply (unfold primel_def)
   apply (induct set: perm)
      apply simp

   apply (induct set: perm)
      apply (simp_all add: oinsert_x_y)
   done
 
 
-subsection {* Existence *}
+subsection \<open>Existence\<close>
 
 lemma ex_nondec_lemma:
     "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
   apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym)
   done

   apply (erule factor_exists [THEN exE])
   apply (blast intro!: ex_nondec_lemma)
   done
 
 
-subsection {* Uniqueness *}
+subsection \<open>Uniqueness\<close>
 
 lemma prime_dvd_mult_list [rule_format]:
     "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
   apply (induct xs)
    apply (force simp add: prime_def)