--- a/scala/recs.scala Mon Apr 22 08:26:16 2013 +0100
+++ b/scala/recs.scala Mon Apr 22 10:33:40 2013 +0100
@@ -205,4 +205,14 @@
Branch_aux(rs, rs.head._1.arity)
}
+val Lg = {
+ val rec_lgR = Less o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
+ val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0)),
+ Less o (Const(1) o (Id(2, 0)), Id(2, 1))))
+ val conR2 = Not o ConR1
+ Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))),
+ Mult o (conR2, Constn(0) o (Id(2, 0))))
}
+
+
+}
--- 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))"