src/HOL/Extraction/Euclid.thy
changeset 25687 f92c9dfa7681
parent 25422 37e991068d96
child 25976 11c6811f232c
equal deleted inserted replaced
25686:bfa774974b6c 25687:f92c9dfa7681
    95       by (simp only: prime_eq' One_nat_def simp_thms)
    95       by (simp only: prime_eq' One_nat_def simp_thms)
    96     thus ?thesis ..
    96     thus ?thesis ..
    97   qed
    97   qed
    98 qed
    98 qed
    99 
    99 
   100 text {*
       
   101 Unfortunately, the proof in the @{text Factorization} theory using @{text metis}
       
   102 is non-constructive.
       
   103 *}
       
   104 
       
   105 lemma split_primel':
       
   106   "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
       
   107   apply (rule exI)
       
   108   apply safe
       
   109    apply (rule_tac [2] prod_append)
       
   110   apply (simp add: primel_append)
       
   111   done
       
   112 
       
   113 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)"
   100 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)"
   114 proof (induct n rule: nat_wf_ind)
   101 proof (induct n rule: nat_wf_ind)
   115   case (1 n)
   102   case (1 n)
   116   from `Suc 0 < n`
   103   from `Suc 0 < n`
   117   have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
   104   have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
   127     from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1)
   114     from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1)
   128     then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k"
   115     then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k"
   129       by iprover
   116       by iprover
   130     from primel_l1 primel_l2
   117     from primel_l1 primel_l2
   131     have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2"
   118     have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2"
   132       by (rule split_primel')
   119       by (rule split_primel)
   133     with prod_l1_m prod_l2_k nmk show ?thesis by simp
   120     with prod_l1_m prod_l2_k nmk show ?thesis by simp
   134   next
   121   next
   135     assume "prime n"
   122     assume "prime n"
   136     hence "primel [n] \<and> prod [n] = n" by (rule prime_primel)
   123     hence "primel [n] \<and> prod [n] = n" by (rule prime_primel)
   137     thus ?thesis ..
   124     thus ?thesis ..