1305 (@{text z} and @{term s} expect one argument), and @{text rs} stands |
1305 (@{text z} and @{term s} expect one argument), and @{text rs} stands |
1306 for a list of recursive functions. Since we know in each case |
1306 for a list of recursive functions. Since we know in each case |
1307 the arity, say @{term l}, we can define an inductive evaluation relation that |
1307 the arity, say @{term l}, we can define an inductive evaluation relation that |
1308 relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l}, |
1308 relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l}, |
1309 to what the result of the recursive function is, say @{text n}---we omit the straightforward |
1309 to what the result of the recursive function is, say @{text n}---we omit the straightforward |
1310 definition of @{term "rec_cal_rel r ns n"}. Because of space reasons, we also omit the |
1310 definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the |
1311 definition of translating |
1311 definition of translating |
1312 recursive functions into abacus programs. We can prove the following |
1312 recursive functions into abacus programs. We can prove the following |
1313 theorem about the translation: Assuming |
1313 theorem about the translation: Assuming |
1314 @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1314 @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} |
1315 then the following Hoare-triple holds |
1315 then the following Hoare-triple holds |