diff -r 06a6db387cd2 -r 6ea1062da89a thys/UF.thy
--- a/thys/UF.thy	Mon Apr 22 08:26:16 2013 +0100
+++ b/thys/UF.thy	Mon Apr 22 10:33:40 2013 +0100
@@ -5,7 +5,7 @@
 header {* Construction of a Universal Function *}
 
 theory UF
-imports Rec_Def GCD Abacus
+imports Rec_Def GCD Abacus "~~/src/HOL/Number_Theory/Primes"
 begin
 
 text {*
@@ -820,22 +820,19 @@
 done
 
 lemma Maxr_Suc_simp: 
-  "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w
-     else Maxr Rr xs w)"
+  "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w else Maxr Rr xs w)"
 apply(auto simp: Maxr.simps Max.insert)
 apply(rule_tac Max_eqI, auto)
 done
 
 lemma [simp]: "min (Suc n) n = n" by simp
 
-lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> 
-                              Sigma f (xs @ [n]) = 0"
+lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> Sigma f (xs @ [n]) = 0"
 apply(induct n, simp add: Sigma.simps)
 apply(simp add: Sigma_Suc_simp_rewrite)
 done
   
-lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0
-        \<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
+lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0 \<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
 apply(induct w)
 apply(simp add: Sigma.simps, simp)
 apply(simp add: Sigma.simps)
@@ -1002,10 +999,9 @@
  *}
 fun quo :: "nat list \<Rightarrow> nat"
   where
-  "quo [x, y] = (let Rr = 
-                         (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0))
-                                 \<le> zs ! 0) \<and> zs ! Suc 0 \<noteq> (0::nat)))
-                 in Maxr Rr [x, y] x)"
+  "quo [x, y] = 
+    (let Rr = (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0)) \<le> zs ! 0) \<and> zs ! Suc 0 \<noteq> 0))
+     in Maxr Rr [x, y] x)"
  
 declare quo.simps[simp del]
 
@@ -1042,15 +1038,13 @@
 definition rec_noteq:: "recf"
   where
   "rec_noteq = Cn (Suc (Suc 0)) rec_not [Cn (Suc (Suc 0)) 
-              rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0)) 
-                                        ((Suc 0))]]"
+              rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0)) ((Suc 0))]]"
 
 text {*
   The correctness of @{text "rec_noteq"}.
   *}
 lemma noteq_lemma: 
-  "\<And> x y. rec_exec rec_noteq [x, y] = 
-               (if x \<noteq> y then 1 else 0)"
+  "rec_exec rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
 by(simp add: rec_exec.simps rec_noteq_def)
 
 declare noteq_lemma[simp]
@@ -1142,7 +1136,7 @@
 text {*
   The correctness of @{text "rec_mod"}:
   *}
-lemma mod_lemma: "\<And> x y. rec_exec rec_mod [x, y] = (x mod y)"
+lemma mod_lemma: "rec_exec rec_mod [x, y] = (x mod y)"
 proof(simp add: rec_exec.simps rec_mod_def quo_lemma2)
   fix x y
   show "x - x div y * y = x mod (y::nat)"
@@ -1151,7 +1145,8 @@
     done
 qed
 
-text{* lemmas for embranch function*}
+section {* Embranch Function *}
+
 type_synonym ftype = "nat list \<Rightarrow> nat"
 type_synonym rtype = "nat list \<Rightarrow> bool"
 
@@ -1426,14 +1421,6 @@
   qed
 qed
 
-text{* 
-  @{text "prime n"} means @{text "n"} is a prime number.
-*}
-fun Prime :: "nat \<Rightarrow> bool"
-  where
-  "Prime x = (1 < x \<and> (\<forall> u < x. (\<forall> v < x. u * v \<noteq> x)))"
-
-declare Prime.simps [simp del]
 
 lemma primerec_all1: 
   "primerec (rec_all rt rf) n \<Longrightarrow> primerec rt n"
@@ -1473,7 +1460,7 @@
 text {*
   The correctness of @{text "Prime"}.
   *}
-lemma prime_lemma: "rec_exec rec_prime [x] = (if Prime x then 1 else 0)"
+lemma prime_lemma: "rec_exec rec_prime [x] = (if prime x then 1 else 0)"
 proof(simp add: rec_exec.simps rec_prime_def)
   let ?rt1 = "(Cn 2 rec_minus [recf.id 2 0, 
     Cn 2 (constn (Suc 0)) [recf.id 2 0]])"
@@ -1500,48 +1487,44 @@
   qed
   from h1 show 
    "(Suc 0 < x \<longrightarrow>  (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow> 
-    \<not> Prime x) \<and>
-     (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \<longrightarrow> Prime x)) \<and>
-    (\<not> Suc 0 < x \<longrightarrow> \<not> Prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
-    \<longrightarrow> \<not> Prime x))"
+    \<not> prime x) \<and>
+     (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \<longrightarrow> prime x)) \<and>
+    (\<not> Suc 0 < x \<longrightarrow> \<not> prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
+    \<longrightarrow> \<not> prime x))"
     apply(auto simp:rec_exec.simps)
     apply(simp add: exec_tmp rec_exec.simps)
   proof -
     assume "\<forall>k\<le>x - Suc 0. (0::nat) < (if \<forall>w\<le>x - Suc 0. 
            0 < (if k * w \<noteq> x then 1 else (0 :: nat)) then 1 else 0)" "Suc 0 < x"
-    thus "Prime x"
+    thus "prime x"
       apply(simp add: rec_exec.simps split: if_splits)
-      apply(simp add: Prime.simps, auto)
-      apply(erule_tac x = u in allE, auto)
-      apply(case_tac u, simp, case_tac nat, simp, simp)
-      apply(case_tac v, simp, case_tac nat, simp, simp)
+      apply(simp add: prime_nat_def dvd_def, auto)
+      apply(erule_tac x = m in allE, auto)
+      apply(case_tac m, simp, case_tac nat, simp, simp)
+      apply(case_tac k, simp, case_tac nat, simp, simp)
       done
   next
-    assume "\<not> Suc 0 < x" "Prime x"
+    assume "\<not> Suc 0 < x" "prime x"
     thus "False"
-      apply(simp add: Prime.simps)
-      done
+      by (simp add: prime_nat_def)
   next
     fix k
     assume "rec_exec (rec_all ?rt1 ?rf1)
-      [x, k] = 0" "k \<le> x - Suc 0" "Prime x"
+      [x, k] = 0" "k \<le> x - Suc 0" "prime x"
     thus "False"
-      apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits)
-      done
+      by (auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
   next
     fix k
     assume "rec_exec (rec_all ?rt1 ?rf1)
-      [x, k] = 0" "k \<le> x - Suc 0" "Prime x"
+      [x, k] = 0" "k \<le> x - Suc 0" "prime x"
     thus "False"
-      apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits)
-      done
+      by(auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
   qed
 qed
 
 definition rec_dummyfac :: "recf"
   where
-  "rec_dummyfac = Pr 1 (constn 1) 
-  (Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])"
+  "rec_dummyfac = Pr 1 (constn 1) (Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])"
 
 text {*
   The recursive function used to implment factorization.
@@ -1561,9 +1544,8 @@
 lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
 by(simp add: rec_dummyfac_def rec_exec.simps)
 
-lemma rec_cn_simp: "rec_exec (Cn n f gs) xs = 
-                (let rgs = map (\<lambda> g. rec_exec g xs) gs in
-                 rec_exec f rgs)"
+lemma rec_cn_simp: 
+  "rec_exec (Cn n f gs) xs = (let rgs = map (\<lambda> g. rec_exec g xs) gs in rec_exec f rgs)"
 by(simp add: rec_exec.simps)
 
 lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n" 
@@ -1588,7 +1570,7 @@
   *}
 fun Np ::"nat \<Rightarrow> nat"
   where
-  "Np x = Min {y. y \<le> Suc (x!) \<and> x < y \<and> Prime y}"
+  "Np x = Min {y. y \<le> Suc (x!) \<and> x < y \<and> prime y}"
 
 declare Np.simps[simp del] rec_Minr.simps[simp del]
 
@@ -1609,15 +1591,17 @@
 done
 
 lemma divsor_ex: 
-"\<lbrakk>\<not> Prime x; x > Suc 0\<rbrakk> \<Longrightarrow> (\<exists> u > Suc 0. (\<exists> v > Suc 0. u * v = x))"
- by(auto simp: Prime.simps)
-
-lemma divsor_prime_ex: "\<lbrakk>\<not> Prime x; x > Suc 0\<rbrakk> \<Longrightarrow> 
-  \<exists> p. Prime p \<and> p dvd x"
+"\<lbrakk>\<not> prime x; x > Suc 0\<rbrakk> \<Longrightarrow> (\<exists> u > Suc 0. (\<exists> v > Suc 0. u * v = x))"
+ apply(auto simp: prime_nat_def dvd_def)
+by (metis Suc_lessI mult_0 nat_mult_commute neq0_conv)
+
+
+lemma divsor_prime_ex: "\<lbrakk>\<not> prime x; x > Suc 0\<rbrakk> \<Longrightarrow> 
+  \<exists> p. prime p \<and> p dvd x"
 apply(induct x rule: wf_induct[where r = "measure (\<lambda> y. y)"], simp)
 apply(drule_tac divsor_ex, simp, auto)
 apply(erule_tac x = u in allE, simp)
-apply(case_tac "Prime u", simp)
+apply(case_tac "prime u", simp)
 apply(rule_tac x = u in exI, simp, auto)
 done
 
@@ -1655,15 +1639,15 @@
     by(simp add: add_mult_distrib2)
 qed
     
-lemma prime_ex: "\<exists> p. n < p \<and> p \<le> Suc (n!) \<and> Prime p"
-proof(cases "Prime (n! + 1)")
+lemma prime_ex: "\<exists> p. n < p \<and> p \<le> Suc (n!) \<and> prime p"
+proof(cases "prime (n! + 1)")
   case True thus "?thesis" 
     by(rule_tac x = "Suc (n!)" in exI, simp)
 next
-  assume h: "\<not> Prime (n! + 1)"  
-  hence "\<exists> p. Prime p \<and> p dvd (n! + 1)"
+  assume h: "\<not> prime (n! + 1)"  
+  hence "\<exists> p. prime p \<and> p dvd (n! + 1)"
     by(erule_tac divsor_prime_ex, auto)
-  from this obtain q where k: "Prime q \<and> q dvd (n! + 1)" ..
+  from this obtain q where k: "prime q \<and> q dvd (n! + 1)" ..
   thus "?thesis"
   proof(cases "q > n")
     case True thus "?thesis"
@@ -1676,7 +1660,7 @@
     proof -
       assume g: "\<not> n < q"
       have j: "q > Suc 0"
-        using k by(case_tac q, auto simp: Prime.simps)
+        using k by(case_tac q, auto simp: prime_nat_def dvd_def)
       hence "q dvd n!"
         using g 
         apply(rule_tac fac_dvd, auto)
@@ -1708,7 +1692,7 @@
 proof(auto simp: rec_np_def rec_exec.simps Let_def fac_lemma)
   let ?rr = "(Cn 2 rec_conj [Cn 2 rec_less [recf.id 2 0,
     recf.id 2 (Suc 0)], Cn 2 rec_prime [recf.id 2 (Suc 0)]])"
-  let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> Prime (zs ! 1)"
+  let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> prime (zs ! 1)"
   have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) = 
     Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!))"
     by(rule_tac Minr_lemma, auto simp: rec_exec.simps
@@ -1719,8 +1703,8 @@
     apply(erule_tac x = p in allE, simp add: prime_lemma)
     apply(simp add: prime_lemma split: if_splits)
     apply(subgoal_tac
-   "{uu. (Prime uu \<longrightarrow> (x < uu \<longrightarrow> uu \<le> Suc (x!)) \<and> x < uu) \<and> Prime uu}
-    = {y. y \<le> Suc (x!) \<and> x < y \<and> Prime y}", auto)
+   "{uu. (prime uu \<longrightarrow> (x < uu \<longrightarrow> uu \<le> Suc (x!)) \<and> x < uu) \<and> prime uu}
+    = {y. y \<le> Suc (x!) \<and> x < y \<and> prime y}", auto)
     done
   from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
     by simp
@@ -1962,18 +1946,16 @@
   *}
 definition rec_lg :: "recf"
   where
-  "rec_lg = (let rec_lgR = Cn 3 rec_le
-  [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
-  let conR1 = Cn 2 rec_conj [Cn 2 rec_less 
+  "rec_lg = 
+  (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
+   let conR1 = Cn 2 rec_conj [Cn 2 rec_less 
                      [Cn 2 (constn 1) [id 2 0], id 2 0], 
                             Cn 2 rec_less [Cn 2 (constn 1) 
                                  [id 2 0], id 2 1]] in 
-  let conR2 = Cn 2 rec_not [conR1] in 
-        Cn 2 rec_add [Cn 2 rec_mult 
-              [conR1, Cn 2 (rec_maxr rec_lgR)
-                       [id 2 0, id 2 1, id 2 0]], 
-                       Cn 2 rec_mult [conR2, Cn 2 (constn 0) 
-                                [id 2 0]]])"
+   let conR2 = Cn 2 rec_not [conR1] in 
+      Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR)
+                                               [id 2 0, id 2 1, id 2 0]], 
+                    Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])"
 
 lemma lg_maxr: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> 
                       rec_exec rec_lg [x, y] = Maxr lgR [x, y] x"
@@ -3059,9 +3041,11 @@
 text {*
   The following lemma gives the correctness of @{text "rec_halt"}.
   It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"}
-  will reach a standard final configuration after @{text "t"} steps of execution, then it is indeed so.
+  will reach a standard final configuration after @{text "t"} steps of execution, 
+  then it is indeed so.
   *}
  
+
 text {*F: universal machine*}
 
 text {*
@@ -3105,7 +3089,7 @@
 definition rec_F :: "recf"
   where
   "rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
- rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]"
+   rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]"
 
 lemma get_fstn_args_nth: 
   "k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)"
@@ -3231,7 +3215,7 @@
 lemma Pi_gr_1[simp]: "Pi n > Suc 0"
 proof(induct n, auto simp: Pi.simps Np.simps)
   fix n
-  let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> Prime y}"
+  let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> prime y}"
   have "finite ?setx" by auto
   moreover have "?setx \<noteq> {}"
     using prime_ex[of "Pi n"]
@@ -3239,7 +3223,7 @@
     done
   ultimately show "Suc 0 < Min ?setx"
     apply(simp add: Min_gr_iff)
-    apply(auto simp: Prime.simps)
+    apply(auto simp: prime_nat_def dvd_def)
     done
 qed
 
@@ -3268,49 +3252,9 @@
 apply(simp)
 done
 
-lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
-proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
-      rule_tac classical, simp)
-  fix d k ka
-  assume case_ka: "\<forall>u<d * ka. \<forall>v<d * ka. u * v \<noteq> d * ka" 
-    and case_k: "\<forall>u<d * k. \<forall>v<d * k. u * v \<noteq> d * k"
-    and h: "(0::nat) < d" "d \<noteq> Suc 0" "Suc 0 < d * ka" 
-           "ka \<noteq> k" "Suc 0 < d * k"
-  from h have "k > Suc 0 \<or> ka >Suc 0"
-    apply(auto)
-    apply(case_tac ka, simp, simp)
-    apply(case_tac k, simp, simp)
-    done
-  from this show "False"
-  proof(erule_tac disjE)
-    assume  "(Suc 0::nat) < k"
-    hence "k < d*k \<and> d < d*k"
-      using h
-      by(auto)
-    thus "?thesis"
-      using case_k
-      apply(erule_tac x = d in allE)
-      apply(simp)
-      apply(erule_tac x = k in allE)
-      apply(simp)
-      done
-  next
-    assume "(Suc 0::nat) < ka"
-    hence "ka < d * ka \<and> d < d*ka"
-      using h by auto
-    thus "?thesis"
-      using case_ka
-      apply(erule_tac x = d in allE)
-      apply(simp)
-      apply(erule_tac x = ka in allE)
-      apply(simp)
-      done
-  qed
-qed
-
 lemma Pi_inc: "Pi (Suc i) > Pi i"
 proof(simp add: Pi.simps Np.simps)
-  let ?setx = "{y. y \<le> Suc (Pi i!) \<and> Pi i < y \<and> Prime y}"
+  let ?setx = "{y. y \<le> Suc (Pi i!) \<and> Pi i < y \<and> prime y}"
   have "finite ?setx" by simp
   moreover have "?setx \<noteq> {}"
     using prime_ex[of "Pi i"]
@@ -3356,16 +3300,16 @@
 apply(simp)
 done
 
-lemma [intro]: "Prime (Suc (Suc 0))"
-apply(auto simp: Prime.simps)
-apply(case_tac u, simp, case_tac nat, simp, simp)
+lemma [intro]: "prime (Suc (Suc 0))"
+apply(auto simp: prime_nat_def dvd_def)
+apply(case_tac m, simp, case_tac k, simp, simp)
 done
 
-lemma Prime_Pi[intro]: "Prime (Pi n)"
+lemma Prime_Pi[intro]: "prime (Pi n)"
 proof(induct n, auto simp: Pi.simps Np.simps)
   fix n
-  let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> Prime y}"
-  show "Prime (Min ?setx)"
+  let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> prime y}"
+  show "prime (Min ?setx)"
   proof -
     have "finite ?setx" by simp
     moreover have "?setx \<noteq> {}" 
@@ -3381,7 +3325,7 @@
 lemma Pi_coprime: "i \<noteq> j \<Longrightarrow> coprime (Pi i) (Pi j)"
 using Prime_Pi[of i]
 using Prime_Pi[of j]
-apply(rule_tac prime_coprime, simp_all add: Pi_notEq)
+apply(rule_tac primes_coprime_nat, simp_all add: Pi_notEq)
 done
 
 lemma Pi_power_coprime: "i \<noteq> j \<Longrightarrow> coprime ((Pi i)^m) ((Pi j)^n)"
@@ -3477,7 +3421,7 @@
                                         Pi (length ps)^(last ps)) "
   proof(rule_tac coprime_mult_nat, simp)
     show "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
-      apply(rule_tac coprime_exp_nat, rule prime_coprime, auto)
+      apply(rule_tac coprime_exp_nat, rule primes_coprime_nat, auto)
       using Pi_notEq[of "Suc i" "length ps"] h by simp
   qed
   from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"