# HG changeset patch # User Christian Urban # Date 1367497190 -3600 # Node ID 6e7244ae43b8f0d453af0af6a7ef6fe8369d831b # Parent aea02b5a58d2f7e24dd1d95450f1965669b7f1b6 polised a bit of the Recs-theory diff -r aea02b5a58d2 -r 6e7244ae43b8 paper.pdf Binary file paper.pdf has changed diff -r aea02b5a58d2 -r 6e7244ae43b8 thys/Recs.thy --- 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 \ 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 \ nat list \ bool) \ nat \ nat list \ nat" - where "Minr R x ys = Min ({z | z. z \ x \ R z ys} \ {Suc x})" - -definition Maxr :: "(nat \ nat list \ bool) \ nat \ nat list \ nat" - where "Maxr R x ys = Max ({z | z. z \ x \ R z ys} \ {0})" - lemma rec_minr2_le_Suc: "rec_eval (rec_minr2 f) [x, y1, y2] \ Suc x" apply(simp add: rec_minr2_def) diff -r aea02b5a58d2 -r 6e7244ae43b8 thys/UF_Rec.thy --- 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,