# HG changeset patch # User Christian Urban # Date 1369430332 -3600 # Node ID 5704925ad1381fc4ac30a1d3285824a41674f7c0 # Parent ca1fe315cb0a970494d1f4c7583f484c3a8812dd started with the definitions of the recursive functions for the UF diff -r ca1fe315cb0a -r 5704925ad138 thys2/Recs.thy --- a/thys2/Recs.thy Fri May 24 20:35:28 2013 +0100 +++ b/thys2/Recs.thy Fri May 24 22:18:52 2013 +0100 @@ -340,17 +340,22 @@ definition "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]" +text {* Iteration *} -section {* Prime Numbers *} +definition + "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])" -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])" +fun Iter where + "Iter f 0 = id" +| "Iter f (Suc n) = f \ (Iter f n)" +lemma iter_comm: + "(Iter f n) (f x) = f ((Iter f n) x)" +by (induct n) (simp_all) + +lemma iter_lemma [simp]: + "rec_eval (rec_iter f) [n, x] = Iter (\x. rec_eval f [x]) n x" +by (induct n) (simp_all add: rec_iter_def) section {* Correctness of Recursive Functions *} @@ -529,20 +534,6 @@ by (simp add: rec_mod_def mod_div_equality' nat_mult_commute) -section {* Prime Numbers *} - -lemma prime_alt_def: - fixes p::nat - shows "prime p = (1 < p \ (\m \ p. m dvd p \ m = 1 \ m = p))" -apply(auto simp add: prime_nat_def dvd_def) -apply(drule_tac x="k" in spec) -apply(auto) -done - -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) - section {* Bounded Maximisation *} fun BMax_rec where @@ -776,90 +767,20 @@ by (simp add: enclen_def) - -section {* Discrete Logarithms *} - -definition - "rec_lg = - (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] 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])" - -definition - "Lg x y = (if 1 < x \ 1 < y then BMax_rec (\u. y ^ u \ x) x else 0)" - -lemma lg_lemma [simp]: - "rec_eval rec_lg [x, y] = Lg x y" -by (simp add: rec_lg_def Lg_def Let_def) - -definition - "Lo x y = (if 1 < x \ 1 < y then BMax_rec (\u. x mod (y ^ u) = 0) x else 0)" - -definition - "rec_lo = - (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])" - -lemma lo_lemma [simp]: - "rec_eval rec_lo [x, y] = Lo x y" -by (simp add: rec_lo_def Lo_def Let_def) - -section {* NextPrime number function *} +definition + "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" -text {* - @{text "NextPrime x"} returns the first prime number after @{text "x"}; - @{text "Pi i"} returns the i-th prime number. *} - -definition NextPrime ::"nat \ nat" - where - "NextPrime x = (LEAST y. y \ Suc (fact x) \ x < y \ prime y)" - -definition rec_nextprime :: "recf" - where - "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in - let conj2 = CN rec_less [Id 2 1, Id 2 0] in - let conj3 = CN rec_prime [Id 2 0] in - let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3] - in MN (CN rec_not [conjs]))" - -lemma nextprime_lemma [simp]: - "rec_eval rec_nextprime [x] = NextPrime x" -by (simp add: rec_nextprime_def Let_def NextPrime_def) - -lemma NextPrime_simps [simp]: - shows "NextPrime 2 = 3" - and "NextPrime 3 = 5" -apply(simp_all add: NextPrime_def) -apply(rule Least_equality) -apply(auto) -apply(eval) -apply(rule Least_equality) -apply(auto) -apply(eval) -apply(case_tac "y = 4") -apply(auto) +lemma ldec_iter: + "ldec z n = pdec1 ((Iter pdec2 n) z) - 1" +apply(induct n arbitrary: z) +apply(simp_all) +apply(subst iter_comm) +apply(simp) done -fun Pi :: "nat \ nat" - where - "Pi 0 = 2" | - "Pi (Suc x) = NextPrime (Pi x)" - -lemma Pi_simps [simp]: - shows "Pi 1 = 3" - and "Pi 2 = 5" -using NextPrime_simps -by(simp_all add: numeral_eq_Suc One_nat_def) - -definition - "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])" - -lemma pi_lemma [simp]: - "rec_eval rec_pi [x] = Pi x" -by (induct x) (simp_all add: rec_pi_def) +lemma ldec_lemma [simp]: + "rec_eval rec_ldec [z, n] = ldec z n" +by (simp add: ldec_iter rec_ldec_def) end diff -r ca1fe315cb0a -r 5704925ad138 thys2/UF_Rec.thy --- a/thys2/UF_Rec.thy Fri May 24 20:35:28 2013 +0100 +++ b/thys2/UF_Rec.thy Fri May 24 22:18:52 2013 +0100 @@ -448,37 +448,25 @@ apply(simp only: Stop.simps[symmetric]) done -text {* UNTIL HERE *} section {* Universal Function as Recursive Functions *} definition - "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]" - -fun rec_listsum2 :: "nat \ nat \ recf" - where - "rec_listsum2 vl 0 = CN Z [Id vl 0]" -| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]" - -fun rec_strt' :: "nat \ nat \ recf" - where - "rec_strt' xs 0 = Z" -| "rec_strt' xs (Suc n) = - (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in - let t1 = CN rec_power [constn 2, dbound] in - let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in - CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])" - -fun rec_map :: "recf \ nat \ recf list" - where - "rec_map rf vl = map (\i. CN rf [Id vl i]) [0.. recf" - where - "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)" + "rec_read = CN rec_ldec [Id 1 0, constn 0]" definition - "rec_scan = CN rec_mod [Id 1 0, constn 2]" + "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]" + +lemma read_lemma [simp]: + "rec_eval rec_read [x] = Read x" +by (simp add: rec_read_def) + +lemma write_lemma [simp]: + "rec_eval rec_write [x, y] = Write x y" +by (simp add: rec_write_def) + + + definition "rec_newleft =