1.1 --- a/src/HOL/Extraction/Euclid.thy	Fri Jun 04 16:42:26 2010 +0200
     1.2 +++ b/src/HOL/Extraction/Euclid.thy	Fri Jun 04 17:32:30 2010 +0200
     1.3 @@ -123,18 +123,25 @@
     1.4  lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)"
     1.5    by (simp add: msetprod_Un msetprod_singleton)
     1.6  
     1.7 -abbreviation (input) "primel ps \<equiv> (\<forall>(p::nat)\<in>set ps. prime p)"
     1.8 +definition all_prime :: "nat list \<Rightarrow> bool" where
     1.9 +  "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)"
    1.10  
    1.11 -lemma prime_primel: "prime n \<Longrightarrow> primel [n]"
    1.12 -  by simp
    1.13 +lemma all_prime_simps:
    1.14 +  "all_prime []"
    1.15 +  "all_prime (p # ps) \<longleftrightarrow> prime p \<and> all_prime ps"
    1.16 +  by (simp_all add: all_prime_def)
    1.17  
    1.18 -lemma split_primel:
    1.19 -  assumes "primel ms" and "primel ns"
    1.20 -  shows "\<exists>qs. primel qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
    1.21 +lemma all_prime_append:
    1.22 +  "all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs"
    1.23 +  by (simp add: all_prime_def ball_Un)
    1.24 +
    1.25 +lemma split_all_prime:
    1.26 +  assumes "all_prime ms" and "all_prime ns"
    1.27 +  shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
    1.28      (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
    1.29  proof -
    1.30 -  from assms have "primel (ms @ ns)"
    1.31 -    unfolding set_append ball_Un by iprover
    1.32 +  from assms have "all_prime (ms @ ns)"
    1.33 +    by (simp add: all_prime_append)
    1.34    moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
    1.35      (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
    1.36      by (simp add: msetprod_Un)
    1.37 @@ -142,13 +149,13 @@
    1.38    then show ?thesis ..
    1.39  qed
    1.40  
    1.41 -lemma primel_nempty_g_one:
    1.42 -  assumes "primel ps" and "ps \<noteq> []"
    1.43 +lemma all_prime_nempty_g_one:
    1.44 +  assumes "all_prime ps" and "ps \<noteq> []"
    1.45    shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
    1.46 -  using `ps \<noteq> []` `primel ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
    1.47 -    (simp_all add: msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
    1.48 +  using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
    1.49 +    (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult  del: One_nat_def)
    1.50  
    1.51 -lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = n)"
    1.52 +lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)"
    1.53  proof (induct n rule: nat_wf_ind)
    1.54    case (1 n)
    1.55    from `Suc 0 < n`
    1.56 @@ -159,21 +166,21 @@
    1.57      assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
    1.58      then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
    1.59        and kn: "k < n" and nmk: "n = m * k" by iprover
    1.60 -    from mn and m have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = m" by (rule 1)
    1.61 -    then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "(PROD m\<Colon>nat:#multiset_of l1. m) = m"
    1.62 +    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = m" by (rule 1)
    1.63 +    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#multiset_of ps1. m) = m"
    1.64        by iprover
    1.65 -    from kn and k have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) = k" by (rule 1)
    1.66 -    then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "(PROD m\<Colon>nat:#multiset_of l2. m) = k"
    1.67 +    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = k" by (rule 1)
    1.68 +    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#multiset_of ps2. m) = k"
    1.69        by iprover
    1.70 -    from primel_l1 primel_l2
    1.71 -    have "\<exists>l. primel l \<and> (PROD m\<Colon>nat:#multiset_of l. m) =
    1.72 -      (PROD m\<Colon>nat:#multiset_of l1. m) * (PROD m\<Colon>nat:#multiset_of l2. m)"
    1.73 -      by (rule split_primel)
    1.74 -    with prod_l1_m prod_l2_k nmk show ?thesis by simp
    1.75 +    from `all_prime ps1` `all_prime ps2`
    1.76 +    have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) =
    1.77 +      (PROD m\<Colon>nat:#multiset_of ps1. m) * (PROD m\<Colon>nat:#multiset_of ps2. m)"
    1.78 +      by (rule split_all_prime)
    1.79 +    with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
    1.80    next
    1.81 -    assume "prime n" then have "primel [n]" by (rule prime_primel)
    1.82 +    assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
    1.83      moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
    1.84 -    ultimately have "primel [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
    1.85 +    ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
    1.86      then show ?thesis ..
    1.87    qed
    1.88  qed
    1.89 @@ -182,17 +189,15 @@
    1.90    assumes N: "(1::nat) < n"
    1.91    shows "\<exists>p. prime p \<and> p dvd n"
    1.92  proof -
    1.93 -  from N obtain l where primel_l: "primel l"
    1.94 -    and prod_l: "n = (PROD m\<Colon>nat:#multiset_of l. m)" using factor_exists
    1.95 +  from N obtain ps where "all_prime ps"
    1.96 +    and prod_ps: "n = (PROD m\<Colon>nat:#multiset_of ps. m)" using factor_exists
    1.97      by simp iprover
    1.98 -  with N have "l \<noteq> []"
    1.99 -    by (auto simp add: primel_nempty_g_one msetprod_empty)
   1.100 -  then obtain x xs where l: "l = x # xs"
   1.101 -    by (cases l) simp
   1.102 -  then have "x \<in> set l" by (simp only: insert_def set.simps) (iprover intro: UnI1 CollectI)
   1.103 -  with primel_l have "prime x" ..
   1.104 -  moreover from primel_l l prod_l
   1.105 -  have "x dvd n" by (simp only: dvd_prod)
   1.106 +  with N have "ps \<noteq> []"
   1.107 +    by (auto simp add: all_prime_nempty_g_one msetprod_empty)
   1.108 +  then obtain p qs where ps: "ps = p # qs" by (cases ps) simp
   1.109 +  with `all_prime ps` have "prime p" by (simp add: all_prime_simps)
   1.110 +  moreover from `all_prime ps` ps prod_ps
   1.111 +  have "p dvd n" by (simp only: dvd_prod)
   1.112    ultimately show ?thesis by iprover
   1.113  qed
   1.114