# HG changeset patch
# User wenzelm
# Date 1197933420 -3600
# Node ID f92c9dfa768159b4c0510f5b2d1630895500426a
# Parent  bfa774974b6c753a9ac3aa29776aaeca2455a91d
split_primel: salvaged original proof after blow with sledghammer
  (this constructive version is required in HOL/Extraction);

diff -r bfa774974b6c -r f92c9dfa7681 src/HOL/Extraction/Euclid.thy
--- a/src/HOL/Extraction/Euclid.thy	Mon Dec 17 23:33:00 2007 +0100
+++ b/src/HOL/Extraction/Euclid.thy	Tue Dec 18 00:17:00 2007 +0100
@@ -97,19 +97,6 @@
   qed
 qed
 
-text {*
-Unfortunately, the proof in the @{text Factorization} theory using @{text metis}
-is non-constructive.
-*}
-
-lemma split_primel':
-  "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
-  apply (rule exI)
-  apply safe
-   apply (rule_tac [2] prod_append)
-  apply (simp add: primel_append)
-  done
-
 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)"
 proof (induct n rule: nat_wf_ind)
   case (1 n)
@@ -129,7 +116,7 @@
       by iprover
     from primel_l1 primel_l2
     have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2"
-      by (rule split_primel')
+      by (rule split_primel)
     with prod_l1_m prod_l2_k nmk show ?thesis by simp
   next
     assume "prime n"
diff -r bfa774974b6c -r f92c9dfa7681 src/HOL/NumberTheory/Factorization.thy
--- a/src/HOL/NumberTheory/Factorization.thy	Mon Dec 17 23:33:00 2007 +0100
+++ b/src/HOL/NumberTheory/Factorization.thy	Tue Dec 18 00:17:00 2007 +0100
@@ -229,8 +229,12 @@
   done
 
 lemma split_primel:
-    "primel xs ==> primel ys ==> \<exists>l. primel l \<and> prod l = prod xs * prod ys" 
-  by (metis primel_append prod.simps(2) prod_append)
+  "primel xs \<Longrightarrow> primel ys \<Longrightarrow> \<exists>l. primel l \<and> prod l = prod xs * prod ys"
+  apply (rule exI)
+  apply safe
+   apply (rule_tac [2] prod_append)
+  apply (simp add: primel_append)
+  done
 
 lemma factor_exists [rule_format]: "Suc 0 < n --> (\<exists>l. primel l \<and> prod l = n)"
   apply (induct n rule: nat_less_induct)