Binary file paper.pdf has changed
--- a/thys/Recs.thy Thu May 02 12:49:33 2013 +0100
+++ b/thys/Recs.thy Thu May 02 13:19:50 2013 +0100
@@ -242,7 +242,9 @@
"rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
-text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
+text {*
+ The @{text "sign"} function returns 1 when the input argument
+ is greater than @{text "0"}. *}
definition
"rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]"
@@ -269,20 +271,19 @@
"rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
- y otherwise *}
+ y otherwise; @{term "rec_if [z, x, y]"} returns x if z is *not*
+ zero, y otherwise *}
definition
"rec_ifz = PR (Id 2 0) (Id 4 3)"
-text {* @{term "rec_if [z, x, y]"} returns x if z is *not* zero,
- y otherwise *}
-
definition
"rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]"
text {*
@{text "rec_less"} compares two arguments and returns @{text "1"} if
the first is less than the second; otherwise returns @{text "0"}. *}
+
definition
"rec_less = CN rec_sign [rec_swap rec_minus]"
@@ -317,7 +318,7 @@
definition
"rec_ex2 f = CN rec_sign [rec_sigma2 f]"
-text {* Dvd, Quotient, Reminder *}
+text {* Dvd, Quotient, Modulo *}
definition
"rec_dvd =
@@ -331,7 +332,19 @@
in PR Z if_stmt)"
definition
- "rec_rem = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
+ "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
+
+
+section {* Prime Numbers *}
+
+definition
+ "rec_prime =
+ (let conj1 = CN rec_less [constn 1, Id 1 0] in
+ let disj = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
+ let imp = CN rec_imp [rec_dvd, disj] in
+ let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
+ CN rec_conj [conj1, conj2])"
+
section {* Correctness of Recursive Functions *}
@@ -506,8 +519,8 @@
by (simp add: Quo_div Quo_rec_quo)
lemma rem_lemma [simp]:
- shows "rec_eval rec_rem [y, x] = y mod x"
-by (simp add: rec_rem_def mod_div_equality' nat_mult_commute)
+ shows "rec_eval rec_mod [y, x] = y mod x"
+by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
section {* Prime Numbers *}
@@ -520,14 +533,6 @@
apply(auto)
done
-definition
- "rec_prime =
- (let conj1 = CN rec_less [constn 1, Id 1 0] in
- let disj = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
- let imp = CN rec_imp [rec_dvd, disj] in
- let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
- CN rec_conj [conj1, conj2])"
-
lemma prime_lemma [simp]:
"rec_eval rec_prime [x] = (if prime x then 1 else 0)"
by (auto simp add: rec_prime_def Let_def prime_alt_def)
@@ -605,7 +610,7 @@
definition
"rec_lo =
- (let calc = CN rec_noteq [CN rec_rem [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
+ (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]]
in CN rec_ifz [cond, Z, max])"
@@ -616,7 +621,9 @@
-text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *}
+text {*
+ @{text "NextPrime x"} returns the first prime number after @{text "x"};
+ @{text "Pi i"} returns the i-th prime number. *}
fun NextPrime ::"nat \<Rightarrow> nat"
where
@@ -647,56 +654,10 @@
"rec_eval rec_pi [x] = Pi x"
by (induct x) (simp_all add: rec_pi_def)
-
end
-
(*
-
-
-fun mtest where
- "mtest R 0 = if R 0 then 0 else 1"
-| "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"
-
-
-lemma
- "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"
-apply(simp only: rec_maxr2_def)
-apply(case_tac x)
-apply(clarify)
-apply(subst rec_eval.simps)
-apply(simp only: constn_lemma)
-defer
-apply(clarify)
-apply(subst rec_eval.simps)
-apply(simp only: rec_maxr2_def[symmetric])
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-
-
-definition
- "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"
-
-definition
- "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"
-
-definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
- where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"
-
-definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
- where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"
-
lemma rec_minr2_le_Suc:
"rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x"
apply(simp add: rec_minr2_def)
--- a/thys/UF_Rec.thy Thu May 02 12:49:33 2013 +0100
+++ b/thys/UF_Rec.thy Thu May 02 13:19:50 2013 +0100
@@ -95,7 +95,7 @@
"Scan r = r mod 2"
definition
- "rec_scan = CN rec_rem [Id 1 0, constn 2]"
+ "rec_scan = CN rec_mod [Id 1 0, constn 2]"
lemma scan_lemma [simp]:
"rec_eval rec_scan [r] = r mod 2"
@@ -124,7 +124,7 @@
let cond2 = CN rec_eq [Id 3 2, constn 2] in
let cond3 = CN rec_eq [Id 3 2, constn 3] in
let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0],
- CN rec_rem [Id 3 1, constn 2]] in
+ CN rec_mod [Id 3 1, constn 2]] in
CN rec_if [cond1, Id 3 0,
CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
CN rec_if [cond3, case3, Id 3 0]]])"
@@ -135,7 +135,7 @@
let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],
- CN rec_rem [Id 3 0, constn 2]] in
+ CN rec_mod [Id 3 0, constn 2]] in
let case3 = CN rec_quo [Id 2 1, constn 2] in
CN rec_if [condn 0, case0,
CN rec_if [condn 1, case1,