Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/UF.thy
changeset 238 6ea1062da89a
parent 237 06a6db387cd2
child 239 ac3309722536
equal deleted inserted replaced
237:06a6db387cd2 238:6ea1062da89a 
     3 *)
 
     3 *)
 
     4 
     4 
     5 header {* Construction of a Universal Function *}
 
     5 header {* Construction of a Universal Function *}
 
     6 
     6 
     7 theory UF
 
     7 theory UF
 
     8 imports Rec_Def GCD Abacus
 
     8 imports Rec_Def GCD Abacus "~~/src/HOL/Number_Theory/Primes"
 
     9 begin
 
     9 begin
 
    10 
    10 
    11 text {*
 
    11 text {*
 
    12   This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined
 
    12   This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined
 
    13   in terms of recursive functions. This @{text "rec_F"} is essentially an 
    13   in terms of recursive functions. This @{text "rec_F"} is essentially an 
   818 apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)
 
   818 apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)
 
   819 apply(case_tac "ys = []", simp_all)
 
   819 apply(case_tac "ys = []", simp_all)
 
   820 done
 
   820 done
 
   821 
   821 
   822 lemma Maxr_Suc_simp: 
   822 lemma Maxr_Suc_simp: 
   823   "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w
 
   823   "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w else Maxr Rr xs w)"
 
   824      else Maxr Rr xs w)"
 
       
   825 apply(auto simp: Maxr.simps Max.insert)
 
   824 apply(auto simp: Maxr.simps Max.insert)
 
   826 apply(rule_tac Max_eqI, auto)
 
   825 apply(rule_tac Max_eqI, auto)
 
   827 done
 
   826 done
 
   828 
   827 
   829 lemma [simp]: "min (Suc n) n = n" by simp
 
   828 lemma [simp]: "min (Suc n) n = n" by simp
 
   830 
   829 
   831 lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> 
   830 lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> Sigma f (xs @ [n]) = 0"
 
   832                               Sigma f (xs @ [n]) = 0"
 
       
   833 apply(induct n, simp add: Sigma.simps)
 
   831 apply(induct n, simp add: Sigma.simps)
 
   834 apply(simp add: Sigma_Suc_simp_rewrite)
 
   832 apply(simp add: Sigma_Suc_simp_rewrite)
 
   835 done
 
   833 done
 
   836   
   834   
   837 lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0
 
   835 lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0 \<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
 
   838         \<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
 
       
   839 apply(induct w)
 
   836 apply(induct w)
 
   840 apply(simp add: Sigma.simps, simp)
 
   837 apply(simp add: Sigma.simps, simp)
 
   841 apply(simp add: Sigma.simps)
 
   838 apply(simp add: Sigma.simps)
 
   842 done
 
   839 done
 
   843 
   840 
  1000 text {* 
   997 text {* 
  1001   @{text "quo"} is the formal specification of division.
 
   998   @{text "quo"} is the formal specification of division.
 
  1002  *}
 
   999  *}
 
  1003 fun quo :: "nat list \<Rightarrow> nat"
 
  1000 fun quo :: "nat list \<Rightarrow> nat"
 
  1004   where
 
  1001   where
 
  1005   "quo [x, y] = (let Rr = 
  1002   "quo [x, y] = 
  1006                          (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0))
 
  1003     (let Rr = (\<lambda> zs. ((zs ! (Suc 0) * zs ! (Suc (Suc 0)) \<le> zs ! 0) \<and> zs ! Suc 0 \<noteq> 0))
 
  1007                                  \<le> zs ! 0) \<and> zs ! Suc 0 \<noteq> (0::nat)))
 
  1004      in Maxr Rr [x, y] x)"
 
  1008                  in Maxr Rr [x, y] x)"
 
       
  1009  
  1005  
  1010 declare quo.simps[simp del]
 
  1006 declare quo.simps[simp del]
 
  1011 
  1007 
  1012 text {*
 
  1008 text {*
 
  1013   The following lemmas shows more directly the menaing of @{text "quo"}:
 
  1009   The following lemmas shows more directly the menaing of @{text "quo"}:
 
  1040   two arguments are not equal.
 
  1036   two arguments are not equal.
 
  1041   *}
 
  1037   *}
 
  1042 definition rec_noteq:: "recf"
 
  1038 definition rec_noteq:: "recf"
 
  1043   where
 
  1039   where
 
  1044   "rec_noteq = Cn (Suc (Suc 0)) rec_not [Cn (Suc (Suc 0)) 
  1040   "rec_noteq = Cn (Suc (Suc 0)) rec_not [Cn (Suc (Suc 0)) 
  1045               rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0)) 
  1041               rec_eq [id (Suc (Suc 0)) (0), id (Suc (Suc 0)) ((Suc 0))]]"
 
  1046                                         ((Suc 0))]]"
 
       
  1047 
  1042 
  1048 text {*
 
  1043 text {*
 
  1049   The correctness of @{text "rec_noteq"}.
 
  1044   The correctness of @{text "rec_noteq"}.
 
  1050   *}
 
  1045   *}
 
  1051 lemma noteq_lemma: 
  1046 lemma noteq_lemma: 
  1052   "\<And> x y. rec_exec rec_noteq [x, y] = 
  1047   "rec_exec rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
 
  1053                (if x \<noteq> y then 1 else 0)"
 
       
  1054 by(simp add: rec_exec.simps rec_noteq_def)
 
  1048 by(simp add: rec_exec.simps rec_noteq_def)
 
  1055 
  1049 
  1056 declare noteq_lemma[simp]
 
  1050 declare noteq_lemma[simp]
 
  1057 
  1051 
  1058 text {*
 
  1052 text {*
 
  1140                                                      (Suc (0))]]"
 
  1134                                                      (Suc (0))]]"
 
  1141 
  1135 
  1142 text {*
 
  1136 text {*
 
  1143   The correctness of @{text "rec_mod"}:
 
  1137   The correctness of @{text "rec_mod"}:
 
  1144   *}
 
  1138   *}
 
  1145 lemma mod_lemma: "\<And> x y. rec_exec rec_mod [x, y] = (x mod y)"
 
  1139 lemma mod_lemma: "rec_exec rec_mod [x, y] = (x mod y)"
 
  1146 proof(simp add: rec_exec.simps rec_mod_def quo_lemma2)
 
  1140 proof(simp add: rec_exec.simps rec_mod_def quo_lemma2)
 
  1147   fix x y
 
  1141   fix x y
 
  1148   show "x - x div y * y = x mod (y::nat)"
 
  1142   show "x - x div y * y = x mod (y::nat)"
 
  1149     using mod_div_equality2[of y x]
 
  1143     using mod_div_equality2[of y x]
 
  1150     apply(subgoal_tac "y * (x div y) = (x div y ) * y", arith, simp)
 
  1144     apply(subgoal_tac "y * (x div y) = (x div y ) * y", arith, simp)
 
  1151     done
 
  1145     done
 
  1152 qed
 
  1146 qed
 
  1153 
  1147 
  1154 text{* lemmas for embranch function*}
 
  1148 section {* Embranch Function *}
 
       
  1149 
  1155 type_synonym ftype = "nat list \<Rightarrow> nat"
 
  1150 type_synonym ftype = "nat list \<Rightarrow> nat"
 
  1156 type_synonym rtype = "nat list \<Rightarrow> bool"
 
  1151 type_synonym rtype = "nat list \<Rightarrow> bool"
 
  1157 
  1152 
  1158 text {*
 
  1153 text {*
 
  1159   The specifation of the mutli-way branching statement on
 
  1154   The specifation of the mutli-way branching statement on
 
  1424       apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps)
 
  1419       apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps)
 
  1425       done
 
  1420       done
 
  1426   qed
 
  1421   qed
 
  1427 qed
 
  1422 qed
 
  1428 
  1423 
  1429 text{* 
       
  1430   @{text "prime n"} means @{text "n"} is a prime number.
 
       
  1431 *}
 
       
  1432 fun Prime :: "nat \<Rightarrow> bool"
 
       
  1433   where
 
       
  1434   "Prime x = (1 < x \<and> (\<forall> u < x. (\<forall> v < x. u * v \<noteq> x)))"
 
       
  1435 
       
  1436 declare Prime.simps [simp del]
 
       
  1437 
  1424 
  1438 lemma primerec_all1: 
  1425 lemma primerec_all1: 
  1439   "primerec (rec_all rt rf) n \<Longrightarrow> primerec rt n"
 
  1426   "primerec (rec_all rt rf) n \<Longrightarrow> primerec rt n"
 
  1440   by (simp add: primerec_all)
 
  1427   by (simp add: primerec_all)
 
  1441 
  1428 
  1471 done
 
  1458 done
 
  1472 
  1459 
  1473 text {*
 
  1460 text {*
 
  1474   The correctness of @{text "Prime"}.
 
  1461   The correctness of @{text "Prime"}.
 
  1475   *}
 
  1462   *}
 
  1476 lemma prime_lemma: "rec_exec rec_prime [x] = (if Prime x then 1 else 0)"
 
  1463 lemma prime_lemma: "rec_exec rec_prime [x] = (if prime x then 1 else 0)"
 
  1477 proof(simp add: rec_exec.simps rec_prime_def)
 
  1464 proof(simp add: rec_exec.simps rec_prime_def)
 
  1478   let ?rt1 = "(Cn 2 rec_minus [recf.id 2 0, 
  1465   let ?rt1 = "(Cn 2 rec_minus [recf.id 2 0, 
  1479     Cn 2 (constn (Suc 0)) [recf.id 2 0]])"
 
  1466     Cn 2 (constn (Suc 0)) [recf.id 2 0]])"
 
  1480   let ?rf1 = "(Cn 3 rec_noteq [Cn 3 rec_mult 
  1467   let ?rf1 = "(Cn 3 rec_noteq [Cn 3 rec_mult 
  1481     [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 (0)])"
 
  1468     [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 (0)])"
 
  1498       apply(case_tac i, auto)
 
  1485       apply(case_tac i, auto)
 
  1499       done
 
  1486       done
 
  1500   qed
 
  1487   qed
 
  1501   from h1 show 
  1488   from h1 show 
  1502    "(Suc 0 < x \<longrightarrow>  (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow> 
  1489    "(Suc 0 < x \<longrightarrow>  (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow> 
  1503     \<not> Prime x) \<and>
 
  1490     \<not> prime x) \<and>
 
  1504      (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \<longrightarrow> Prime x)) \<and>
 
  1491      (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \<longrightarrow> prime x)) \<and>
 
  1505     (\<not> Suc 0 < x \<longrightarrow> \<not> Prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
 
  1492     (\<not> Suc 0 < x \<longrightarrow> \<not> prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
 
  1506     \<longrightarrow> \<not> Prime x))"
 
  1493     \<longrightarrow> \<not> prime x))"
 
  1507     apply(auto simp:rec_exec.simps)
 
  1494     apply(auto simp:rec_exec.simps)
 
  1508     apply(simp add: exec_tmp rec_exec.simps)
 
  1495     apply(simp add: exec_tmp rec_exec.simps)
 
  1509   proof -
 
  1496   proof -
 
  1510     assume "\<forall>k\<le>x - Suc 0. (0::nat) < (if \<forall>w\<le>x - Suc 0. 
  1497     assume "\<forall>k\<le>x - Suc 0. (0::nat) < (if \<forall>w\<le>x - Suc 0. 
  1511            0 < (if k * w \<noteq> x then 1 else (0 :: nat)) then 1 else 0)" "Suc 0 < x"
 
  1498            0 < (if k * w \<noteq> x then 1 else (0 :: nat)) then 1 else 0)" "Suc 0 < x"
 
  1512     thus "Prime x"
 
  1499     thus "prime x"
 
  1513       apply(simp add: rec_exec.simps split: if_splits)
 
  1500       apply(simp add: rec_exec.simps split: if_splits)
 
  1514       apply(simp add: Prime.simps, auto)
 
  1501       apply(simp add: prime_nat_def dvd_def, auto)
 
  1515       apply(erule_tac x = u in allE, auto)
 
  1502       apply(erule_tac x = m in allE, auto)
 
  1516       apply(case_tac u, simp, case_tac nat, simp, simp)
 
  1503       apply(case_tac m, simp, case_tac nat, simp, simp)
 
  1517       apply(case_tac v, simp, case_tac nat, simp, simp)
 
  1504       apply(case_tac k, simp, case_tac nat, simp, simp)
 
  1518       done
 
  1505       done
 
  1519   next
 
  1506   next
 
  1520     assume "\<not> Suc 0 < x" "Prime x"
 
  1507     assume "\<not> Suc 0 < x" "prime x"
 
  1521     thus "False"
 
  1508     thus "False"
 
  1522       apply(simp add: Prime.simps)
 
  1509       by (simp add: prime_nat_def)
 
  1523       done
 
       
  1524   next
 
  1510   next
 
  1525     fix k
 
  1511     fix k
 
  1526     assume "rec_exec (rec_all ?rt1 ?rf1)
 
  1512     assume "rec_exec (rec_all ?rt1 ?rf1)
 
  1527       [x, k] = 0" "k \<le> x - Suc 0" "Prime x"
 
  1513       [x, k] = 0" "k \<le> x - Suc 0" "prime x"
 
  1528     thus "False"
 
  1514     thus "False"
 
  1529       apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits)
 
  1515       by (auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
 
  1530       done
 
       
  1531   next
 
  1516   next
 
  1532     fix k
 
  1517     fix k
 
  1533     assume "rec_exec (rec_all ?rt1 ?rf1)
 
  1518     assume "rec_exec (rec_all ?rt1 ?rf1)
 
  1534       [x, k] = 0" "k \<le> x - Suc 0" "Prime x"
 
  1519       [x, k] = 0" "k \<le> x - Suc 0" "prime x"
 
  1535     thus "False"
 
  1520     thus "False"
 
  1536       apply(simp add: exec_tmp rec_exec.simps Prime.simps split: if_splits)
 
  1521       by(auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
 
  1537       done
 
       
  1538   qed
 
  1522   qed
 
  1539 qed
 
  1523 qed
 
  1540 
  1524 
  1541 definition rec_dummyfac :: "recf"
 
  1525 definition rec_dummyfac :: "recf"
 
  1542   where
 
  1526   where
 
  1543   "rec_dummyfac = Pr 1 (constn 1) 
  1527   "rec_dummyfac = Pr 1 (constn 1) (Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])"
 
  1544   (Cn 3 rec_mult [id 3 2, Cn 3 s [id 3 1]])"
 
       
  1545 
  1528 
  1546 text {*
 
  1529 text {*
 
  1547   The recursive function used to implment factorization.
 
  1530   The recursive function used to implment factorization.
 
  1548   *}
 
  1531   *}
 
  1549 definition rec_fac :: "recf"
 
  1532 definition rec_fac :: "recf"
 
  1559   "fac (Suc x) = (Suc x) * fac x"
 
  1542   "fac (Suc x) = (Suc x) * fac x"
 
  1560 
  1543 
  1561 lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
 
  1544 lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
 
  1562 by(simp add: rec_dummyfac_def rec_exec.simps)
 
  1545 by(simp add: rec_dummyfac_def rec_exec.simps)
 
  1563 
  1546 
  1564 lemma rec_cn_simp: "rec_exec (Cn n f gs) xs = 
  1547 lemma rec_cn_simp: 
  1565                 (let rgs = map (\<lambda> g. rec_exec g xs) gs in
 
  1548   "rec_exec (Cn n f gs) xs = (let rgs = map (\<lambda> g. rec_exec g xs) gs in rec_exec f rgs)"
 
  1566                  rec_exec f rgs)"
 
       
  1567 by(simp add: rec_exec.simps)
 
  1549 by(simp add: rec_exec.simps)
 
  1568 
  1550 
  1569 lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n" 
  1551 lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n" 
  1570   by(simp add: rec_exec.simps)
 
  1552   by(simp add: rec_exec.simps)
 
  1571 
  1553 
  1586 text {*
 
  1568 text {*
 
  1587   @{text "Np x"} returns the first prime number after @{text "x"}.
 
  1569   @{text "Np x"} returns the first prime number after @{text "x"}.
 
  1588   *}
 
  1570   *}
 
  1589 fun Np ::"nat \<Rightarrow> nat"
 
  1571 fun Np ::"nat \<Rightarrow> nat"
 
  1590   where
 
  1572   where
 
  1591   "Np x = Min {y. y \<le> Suc (x!) \<and> x < y \<and> Prime y}"
 
  1573   "Np x = Min {y. y \<le> Suc (x!) \<and> x < y \<and> prime y}"
 
  1592 
  1574 
  1593 declare Np.simps[simp del] rec_Minr.simps[simp del]
 
  1575 declare Np.simps[simp del] rec_Minr.simps[simp del]
 
  1594 
  1576 
  1595 text {*
 
  1577 text {*
 
  1596   @{text "rec_np"} is the recursive function used to implement
 
  1578   @{text "rec_np"} is the recursive function used to implement
 
  1607 apply(simp add: fac.simps)
 
  1589 apply(simp add: fac.simps)
 
  1608 apply(case_tac n, auto simp: fac.simps)
 
  1590 apply(case_tac n, auto simp: fac.simps)
 
  1609 done
 
  1591 done
 
  1610 
  1592 
  1611 lemma divsor_ex: 
  1593 lemma divsor_ex: 
  1612 "\<lbrakk>\<not> Prime x; x > Suc 0\<rbrakk> \<Longrightarrow> (\<exists> u > Suc 0. (\<exists> v > Suc 0. u * v = x))"
 
  1594 "\<lbrakk>\<not> prime x; x > Suc 0\<rbrakk> \<Longrightarrow> (\<exists> u > Suc 0. (\<exists> v > Suc 0. u * v = x))"
 
  1613  by(auto simp: Prime.simps)
 
  1595  apply(auto simp: prime_nat_def dvd_def)
 
  1614 
  1596 by (metis Suc_lessI mult_0 nat_mult_commute neq0_conv)
 
  1615 lemma divsor_prime_ex: "\<lbrakk>\<not> Prime x; x > Suc 0\<rbrakk> \<Longrightarrow> 
  1597 
  1616   \<exists> p. Prime p \<and> p dvd x"
 
  1598 
       
  1599 lemma divsor_prime_ex: "\<lbrakk>\<not> prime x; x > Suc 0\<rbrakk> \<Longrightarrow> 
       
  1600   \<exists> p. prime p \<and> p dvd x"
 
  1617 apply(induct x rule: wf_induct[where r = "measure (\<lambda> y. y)"], simp)
 
  1601 apply(induct x rule: wf_induct[where r = "measure (\<lambda> y. y)"], simp)
 
  1618 apply(drule_tac divsor_ex, simp, auto)
 
  1602 apply(drule_tac divsor_ex, simp, auto)
 
  1619 apply(erule_tac x = u in allE, simp)
 
  1603 apply(erule_tac x = u in allE, simp)
 
  1620 apply(case_tac "Prime u", simp)
 
  1604 apply(case_tac "prime u", simp)
 
  1621 apply(rule_tac x = u in exI, simp, auto)
 
  1605 apply(rule_tac x = u in exI, simp, auto)
 
  1622 done
 
  1606 done
 
  1623 
  1607 
  1624 lemma [intro]: "0 < n!"
 
  1608 lemma [intro]: "0 < n!"
 
  1625 apply(induct n)
 
  1609 apply(induct n)
 
  1653   from this obtain d where "d > 0 \<and> ka = d + k" ..
 
  1637   from this obtain d where "d > 0 \<and> ka = d + k" ..
 
  1654   from h2 and this and h1 show "False"
 
  1638   from h2 and this and h1 show "False"
 
  1655     by(simp add: add_mult_distrib2)
 
  1639     by(simp add: add_mult_distrib2)
 
  1656 qed
 
  1640 qed
 
  1657     
  1641     
  1658 lemma prime_ex: "\<exists> p. n < p \<and> p \<le> Suc (n!) \<and> Prime p"
 
  1642 lemma prime_ex: "\<exists> p. n < p \<and> p \<le> Suc (n!) \<and> prime p"
 
  1659 proof(cases "Prime (n! + 1)")
 
  1643 proof(cases "prime (n! + 1)")
 
  1660   case True thus "?thesis" 
  1644   case True thus "?thesis" 
  1661     by(rule_tac x = "Suc (n!)" in exI, simp)
 
  1645     by(rule_tac x = "Suc (n!)" in exI, simp)
 
  1662 next
 
  1646 next
 
  1663   assume h: "\<not> Prime (n! + 1)"  
  1647   assume h: "\<not> prime (n! + 1)"  
  1664   hence "\<exists> p. Prime p \<and> p dvd (n! + 1)"
 
  1648   hence "\<exists> p. prime p \<and> p dvd (n! + 1)"
 
  1665     by(erule_tac divsor_prime_ex, auto)
 
  1649     by(erule_tac divsor_prime_ex, auto)
 
  1666   from this obtain q where k: "Prime q \<and> q dvd (n! + 1)" ..
 
  1650   from this obtain q where k: "prime q \<and> q dvd (n! + 1)" ..
 
  1667   thus "?thesis"
 
  1651   thus "?thesis"
 
  1668   proof(cases "q > n")
 
  1652   proof(cases "q > n")
 
  1669     case True thus "?thesis"
 
  1653     case True thus "?thesis"
 
  1670       using k
 
  1654       using k
 
  1671       apply(rule_tac x = q in exI, auto)
 
  1655       apply(rule_tac x = q in exI, auto)
 
  1674   next
 
  1658   next
 
  1675     case False thus "?thesis"
 
  1659     case False thus "?thesis"
 
  1676     proof -
 
  1660     proof -
 
  1677       assume g: "\<not> n < q"
 
  1661       assume g: "\<not> n < q"
 
  1678       have j: "q > Suc 0"
 
  1662       have j: "q > Suc 0"
 
  1679         using k by(case_tac q, auto simp: Prime.simps)
 
  1663         using k by(case_tac q, auto simp: prime_nat_def dvd_def)
 
  1680       hence "q dvd n!"
 
  1664       hence "q dvd n!"
 
  1681         using g 
  1665         using g 
  1682         apply(rule_tac fac_dvd, auto)
 
  1666         apply(rule_tac fac_dvd, auto)
 
  1683         done
 
  1667         done
 
  1684       hence "\<not> q dvd Suc (n!)"
 
  1668       hence "\<not> q dvd Suc (n!)"
 
  1706   *}
 
  1690   *}
 
  1707 lemma np_lemma: "rec_exec rec_np [x] = Np x"
 
  1691 lemma np_lemma: "rec_exec rec_np [x] = Np x"
 
  1708 proof(auto simp: rec_np_def rec_exec.simps Let_def fac_lemma)
 
  1692 proof(auto simp: rec_np_def rec_exec.simps Let_def fac_lemma)
 
  1709   let ?rr = "(Cn 2 rec_conj [Cn 2 rec_less [recf.id 2 0,
 
  1693   let ?rr = "(Cn 2 rec_conj [Cn 2 rec_less [recf.id 2 0,
 
  1710     recf.id 2 (Suc 0)], Cn 2 rec_prime [recf.id 2 (Suc 0)]])"
 
  1694     recf.id 2 (Suc 0)], Cn 2 rec_prime [recf.id 2 (Suc 0)]])"
 
  1711   let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> Prime (zs ! 1)"
 
  1695   let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> prime (zs ! 1)"
 
  1712   have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) = 
  1696   have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) = 
  1713     Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!))"
 
  1697     Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!))"
 
  1714     by(rule_tac Minr_lemma, auto simp: rec_exec.simps
 
  1698     by(rule_tac Minr_lemma, auto simp: rec_exec.simps
 
  1715       prime_lemma, auto simp:  numeral_2_eq_2 numeral_3_eq_3)
 
  1699       prime_lemma, auto simp:  numeral_2_eq_2 numeral_3_eq_3)
 
  1716   have g2: "Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!)) = Np x"
 
  1700   have g2: "Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!)) = Np x"
 
  1717     using prime_ex[of x]
 
  1701     using prime_ex[of x]
 
  1718     apply(auto simp: Minr.simps Np.simps rec_exec.simps)
 
  1702     apply(auto simp: Minr.simps Np.simps rec_exec.simps)
 
  1719     apply(erule_tac x = p in allE, simp add: prime_lemma)
 
  1703     apply(erule_tac x = p in allE, simp add: prime_lemma)
 
  1720     apply(simp add: prime_lemma split: if_splits)
 
  1704     apply(simp add: prime_lemma split: if_splits)
 
  1721     apply(subgoal_tac
 
  1705     apply(subgoal_tac
 
  1722    "{uu. (Prime uu \<longrightarrow> (x < uu \<longrightarrow> uu \<le> Suc (x!)) \<and> x < uu) \<and> Prime uu}
 
  1706    "{uu. (prime uu \<longrightarrow> (x < uu \<longrightarrow> uu \<le> Suc (x!)) \<and> x < uu) \<and> prime uu}
 
  1723     = {y. y \<le> Suc (x!) \<and> x < y \<and> Prime y}", auto)
 
  1707     = {y. y \<le> Suc (x!) \<and> x < y \<and> prime y}", auto)
 
  1724     done
 
  1708     done
 
  1725   from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
 
  1709   from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
 
  1726     by simp
 
  1710     by simp
 
  1727 qed
 
  1711 qed
 
  1728 
  1712 
  1960 text {*
 
  1944 text {*
 
  1961   @{text "rec_lg"} is the recursive function used to implement @{text "lg"}.
 
  1945   @{text "rec_lg"} is the recursive function used to implement @{text "lg"}.
 
  1962   *}
 
  1946   *}
 
  1963 definition rec_lg :: "recf"
 
  1947 definition rec_lg :: "recf"
 
  1964   where
 
  1948   where
 
  1965   "rec_lg = (let rec_lgR = Cn 3 rec_le
 
  1949   "rec_lg = 
  1966   [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
 
  1950   (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
 
  1967   let conR1 = Cn 2 rec_conj [Cn 2 rec_less 
  1951    let conR1 = Cn 2 rec_conj [Cn 2 rec_less 
  1968                      [Cn 2 (constn 1) [id 2 0], id 2 0], 
  1952                      [Cn 2 (constn 1) [id 2 0], id 2 0], 
  1969                             Cn 2 rec_less [Cn 2 (constn 1) 
  1953                             Cn 2 rec_less [Cn 2 (constn 1) 
  1970                                  [id 2 0], id 2 1]] in 
  1954                                  [id 2 0], id 2 1]] in 
  1971   let conR2 = Cn 2 rec_not [conR1] in 
  1955    let conR2 = Cn 2 rec_not [conR1] in 
  1972         Cn 2 rec_add [Cn 2 rec_mult 
  1956       Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR)
 
  1973               [conR1, Cn 2 (rec_maxr rec_lgR)
 
  1957                                                [id 2 0, id 2 1, id 2 0]], 
  1974                        [id 2 0, id 2 1, id 2 0]], 
  1958                     Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])"
 
  1975                        Cn 2 rec_mult [conR2, Cn 2 (constn 0) 
       
  1976                                 [id 2 0]]])"
 
       
  1977 
  1959 
  1978 lemma lg_maxr: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> 
  1960 lemma lg_maxr: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> 
  1979                       rec_exec rec_lg [x, y] = Maxr lgR [x, y] x"
 
  1961                       rec_exec rec_lg [x, y] = Maxr lgR [x, y] x"
 
  1980 proof(simp add: rec_exec.simps rec_lg_def Let_def)
 
  1962 proof(simp add: rec_exec.simps rec_lg_def Let_def)
 
  1981   assume h: "Suc 0 < x" "Suc 0 < y"
 
  1963   assume h: "Suc 0 < x" "Suc 0 < y"
 
  3057 qed
 
  3039 qed
 
  3058 
  3040 
  3059 text {*
 
  3041 text {*
 
  3060   The following lemma gives the correctness of @{text "rec_halt"}.
 
  3042   The following lemma gives the correctness of @{text "rec_halt"}.
 
  3061   It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"}
 
  3043   It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"}
 
  3062   will reach a standard final configuration after @{text "t"} steps of execution, then it is indeed so.
 
  3044   will reach a standard final configuration after @{text "t"} steps of execution, 
       
  3045   then it is indeed so.
 
  3063   *}
 
  3046   *}
 
  3064  
  3047  
       
  3048 
  3065 text {*F: universal machine*}
 
  3049 text {*F: universal machine*}
 
  3066 
  3050 
  3067 text {*
 
  3051 text {*
 
  3068   @{text "valu r"} extracts computing result out of the right number @{text "r"}.
 
  3052   @{text "valu r"} extracts computing result out of the right number @{text "r"}.
 
  3069   *}
 
  3053   *}
 
  3103   The definition of the universal function @{text "rec_F"}.
 
  3087   The definition of the universal function @{text "rec_F"}.
 
  3104   *}
 
  3088   *}
 
  3105 definition rec_F :: "recf"
 
  3089 definition rec_F :: "recf"
 
  3106   where
 
  3090   where
 
  3107   "rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
 
  3091   "rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
 
  3108  rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]"
 
  3092    rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]"
 
  3109 
  3093 
  3110 lemma get_fstn_args_nth: 
  3094 lemma get_fstn_args_nth: 
  3111   "k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)"
 
  3095   "k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)"
 
  3112 apply(induct n, simp)
 
  3096 apply(induct n, simp)
 
  3113 apply(case_tac "k = n", simp_all add: get_fstn_args.simps 
  3097 apply(case_tac "k = n", simp_all add: get_fstn_args.simps 
  3229 done
 
  3213 done
 
  3230 
  3214 
  3231 lemma Pi_gr_1[simp]: "Pi n > Suc 0"
 
  3215 lemma Pi_gr_1[simp]: "Pi n > Suc 0"
 
  3232 proof(induct n, auto simp: Pi.simps Np.simps)
 
  3216 proof(induct n, auto simp: Pi.simps Np.simps)
 
  3233   fix n
 
  3217   fix n
 
  3234   let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> Prime y}"
 
  3218   let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> prime y}"
 
  3235   have "finite ?setx" by auto
 
  3219   have "finite ?setx" by auto
 
  3236   moreover have "?setx \<noteq> {}"
 
  3220   moreover have "?setx \<noteq> {}"
 
  3237     using prime_ex[of "Pi n"]
 
  3221     using prime_ex[of "Pi n"]
 
  3238     apply(auto)
 
  3222     apply(auto)
 
  3239     done
 
  3223     done
 
  3240   ultimately show "Suc 0 < Min ?setx"
 
  3224   ultimately show "Suc 0 < Min ?setx"
 
  3241     apply(simp add: Min_gr_iff)
 
  3225     apply(simp add: Min_gr_iff)
 
  3242     apply(auto simp: Prime.simps)
 
  3226     apply(auto simp: prime_nat_def dvd_def)
 
  3243     done
 
  3227     done
 
  3244 qed
 
  3228 qed
 
  3245 
  3229 
  3246 lemma Pi_not_0[simp]: "Pi n > 0"
 
  3230 lemma Pi_not_0[simp]: "Pi n > 0"
 
  3247 using Pi_gr_1[of n]
 
  3231 using Pi_gr_1[of n]
 
  3266   "\<lbrakk>i < length nl; \<not> Suc 0 < godel_code nl\<rbrakk> \<Longrightarrow> nl ! i = 0"
 
  3250   "\<lbrakk>i < length nl; \<not> Suc 0 < godel_code nl\<rbrakk> \<Longrightarrow> nl ! i = 0"
 
  3267 using godel_code_great[of nl] godel_code_eq_1[of nl]
 
  3251 using godel_code_great[of nl] godel_code_eq_1[of nl]
 
  3268 apply(simp)
 
  3252 apply(simp)
 
  3269 done
 
  3253 done
 
  3270 
  3254 
  3271 lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
 
       
  3272 proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
 
       
  3273       rule_tac classical, simp)
 
       
  3274   fix d k ka
 
       
  3275   assume case_ka: "\<forall>u<d * ka. \<forall>v<d * ka. u * v \<noteq> d * ka" 
       
  3276     and case_k: "\<forall>u<d * k. \<forall>v<d * k. u * v \<noteq> d * k"
 
       
  3277     and h: "(0::nat) < d" "d \<noteq> Suc 0" "Suc 0 < d * ka" 
       
  3278            "ka \<noteq> k" "Suc 0 < d * k"
 
       
  3279   from h have "k > Suc 0 \<or> ka >Suc 0"
 
       
  3280     apply(auto)
 
       
  3281     apply(case_tac ka, simp, simp)
 
       
  3282     apply(case_tac k, simp, simp)
 
       
  3283     done
 
       
  3284   from this show "False"
 
       
  3285   proof(erule_tac disjE)
 
       
  3286     assume  "(Suc 0::nat) < k"
 
       
  3287     hence "k < d*k \<and> d < d*k"
 
       
  3288       using h
 
       
  3289       by(auto)
 
       
  3290     thus "?thesis"
 
       
  3291       using case_k
 
       
  3292       apply(erule_tac x = d in allE)
 
       
  3293       apply(simp)
 
       
  3294       apply(erule_tac x = k in allE)
 
       
  3295       apply(simp)
 
       
  3296       done
 
       
  3297   next
 
       
  3298     assume "(Suc 0::nat) < ka"
 
       
  3299     hence "ka < d * ka \<and> d < d*ka"
 
       
  3300       using h by auto
 
       
  3301     thus "?thesis"
 
       
  3302       using case_ka
 
       
  3303       apply(erule_tac x = d in allE)
 
       
  3304       apply(simp)
 
       
  3305       apply(erule_tac x = ka in allE)
 
       
  3306       apply(simp)
 
       
  3307       done
 
       
  3308   qed
 
       
  3309 qed
 
       
  3310 
       
  3311 lemma Pi_inc: "Pi (Suc i) > Pi i"
 
  3255 lemma Pi_inc: "Pi (Suc i) > Pi i"
 
  3312 proof(simp add: Pi.simps Np.simps)
 
  3256 proof(simp add: Pi.simps Np.simps)
 
  3313   let ?setx = "{y. y \<le> Suc (Pi i!) \<and> Pi i < y \<and> Prime y}"
 
  3257   let ?setx = "{y. y \<le> Suc (Pi i!) \<and> Pi i < y \<and> prime y}"
 
  3314   have "finite ?setx" by simp
 
  3258   have "finite ?setx" by simp
 
  3315   moreover have "?setx \<noteq> {}"
 
  3259   moreover have "?setx \<noteq> {}"
 
  3316     using prime_ex[of "Pi i"]
 
  3260     using prime_ex[of "Pi i"]
 
  3317     apply(auto)
 
  3261     apply(auto)
 
  3318     done
 
  3262     done
 
  3354 apply(simp)
 
  3298 apply(simp)
 
  3355 using Pi_inc_gr[of j i]
 
  3299 using Pi_inc_gr[of j i]
 
  3356 apply(simp)
 
  3300 apply(simp)
 
  3357 done
 
  3301 done
 
  3358 
  3302 
  3359 lemma [intro]: "Prime (Suc (Suc 0))"
 
  3303 lemma [intro]: "prime (Suc (Suc 0))"
 
  3360 apply(auto simp: Prime.simps)
 
  3304 apply(auto simp: prime_nat_def dvd_def)
 
  3361 apply(case_tac u, simp, case_tac nat, simp, simp)
 
  3305 apply(case_tac m, simp, case_tac k, simp, simp)
 
  3362 done
 
  3306 done
 
  3363 
  3307 
  3364 lemma Prime_Pi[intro]: "Prime (Pi n)"
 
  3308 lemma Prime_Pi[intro]: "prime (Pi n)"
 
  3365 proof(induct n, auto simp: Pi.simps Np.simps)
 
  3309 proof(induct n, auto simp: Pi.simps Np.simps)
 
  3366   fix n
 
  3310   fix n
 
  3367   let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> Prime y}"
 
  3311   let ?setx = "{y. y \<le> Suc (Pi n!) \<and> Pi n < y \<and> prime y}"
 
  3368   show "Prime (Min ?setx)"
 
  3312   show "prime (Min ?setx)"
 
  3369   proof -
 
  3313   proof -
 
  3370     have "finite ?setx" by simp
 
  3314     have "finite ?setx" by simp
 
  3371     moreover have "?setx \<noteq> {}" 
  3315     moreover have "?setx \<noteq> {}" 
  3372       using prime_ex[of "Pi n"]
 
  3316       using prime_ex[of "Pi n"]
 
  3373       apply(simp)
 
  3317       apply(simp)
 
  3379 qed
 
  3323 qed
 
  3380     
  3324     
  3381 lemma Pi_coprime: "i \<noteq> j \<Longrightarrow> coprime (Pi i) (Pi j)"
 
  3325 lemma Pi_coprime: "i \<noteq> j \<Longrightarrow> coprime (Pi i) (Pi j)"
 
  3382 using Prime_Pi[of i]
 
  3326 using Prime_Pi[of i]
 
  3383 using Prime_Pi[of j]
 
  3327 using Prime_Pi[of j]
 
  3384 apply(rule_tac prime_coprime, simp_all add: Pi_notEq)
 
  3328 apply(rule_tac primes_coprime_nat, simp_all add: Pi_notEq)
 
  3385 done
 
  3329 done
 
  3386 
  3330 
  3387 lemma Pi_power_coprime: "i \<noteq> j \<Longrightarrow> coprime ((Pi i)^m) ((Pi j)^n)"
 
  3331 lemma Pi_power_coprime: "i \<noteq> j \<Longrightarrow> coprime ((Pi i)^m) ((Pi j)^n)"
 
  3388 by(rule_tac coprime_exp2_nat, erule_tac Pi_coprime)
 
  3332 by(rule_tac coprime_exp2_nat, erule_tac Pi_coprime)
 
  3389 
  3333 
  3475   from g have 
  3419   from g have 
  3476     "coprime (Pi (Suc i)) (godel_code' (butlast ps) (Suc 0) *
 
  3420     "coprime (Pi (Suc i)) (godel_code' (butlast ps) (Suc 0) *
 
  3477                                         Pi (length ps)^(last ps)) "
 
  3421                                         Pi (length ps)^(last ps)) "
 
  3478   proof(rule_tac coprime_mult_nat, simp)
 
  3422   proof(rule_tac coprime_mult_nat, simp)
 
  3479     show "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
 
  3423     show "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
 
  3480       apply(rule_tac coprime_exp_nat, rule prime_coprime, auto)
 
  3424       apply(rule_tac coprime_exp_nat, rule primes_coprime_nat, auto)
 
  3481       using Pi_notEq[of "Suc i" "length ps"] h by simp
 
  3425       using Pi_notEq[of "Suc i" "length ps"] h by simp
 
  3482   qed
 
  3426   qed
 
  3483   from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
 
  3427   from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
 
  3484     by simp
 
  3428     by simp
 
  3485 qed
 
  3429 qed
tm