|
79490
|
1 |
(*
|
|
|
2 |
Author: Jonas Stahl
|
|
|
3 |
|
|
|
4 |
Automatic definition of running time functions from HOL functions
|
|
|
5 |
following the translation described in Section 1.5, Running Time, of the book
|
|
|
6 |
Functional Data Structures and Algorithms. A Proof Assistant Approach.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
theory Define_Time_Function
|
|
|
10 |
imports Main
|
|
79969
|
11 |
keywords "time_fun" :: thy_decl
|
|
|
12 |
and "time_function" :: thy_goal
|
|
|
13 |
and "time_definition" :: thy_goal
|
|
79490
|
14 |
and "equations"
|
|
79969
|
15 |
and "time_fun_0" :: thy_decl
|
|
79490
|
16 |
begin
|
|
|
17 |
|
|
|
18 |
ML_file Define_Time_0.ML
|
|
|
19 |
ML_file Define_Time_Function.ML
|
|
|
20 |
|
|
|
21 |
declare [[time_prefix = "T_"]]
|
|
|
22 |
|
|
|
23 |
text \<open>The pre-defined functions below are assumed to have constant running time.
|
|
|
24 |
In fact, we make that constant 0.
|
|
|
25 |
This does not change the asymptotic running time of user-defined functions using the
|
|
|
26 |
pre-defined functions because 1 is added for every user-defined function call.
|
|
|
27 |
|
|
|
28 |
Note: Many of the functions below are polymorphic and reside in type classes.
|
|
|
29 |
The constant-time assumption is justified only for those types where the hardware offers
|
|
|
30 |
suitable support, e.g. numeric types. The argument size is implicitly bounded, too.
|
|
|
31 |
|
|
|
32 |
The constant-time assumption for \<open>(=)\<close> is justified for recursive data types such as lists and trees
|
|
|
33 |
as long as the comparison is of the form \<open>t = c\<close> where \<open>c\<close> is a constant term, for example \<open>xs = []\<close>.\<close>
|
|
|
34 |
|
|
79969
|
35 |
time_fun_0 "(+)"
|
|
|
36 |
time_fun_0 "(-)"
|
|
|
37 |
time_fun_0 "(*)"
|
|
|
38 |
time_fun_0 "(/)"
|
|
|
39 |
time_fun_0 "(div)"
|
|
|
40 |
time_fun_0 "(<)"
|
|
|
41 |
time_fun_0 "(\<le>)"
|
|
|
42 |
time_fun_0 "Not"
|
|
|
43 |
time_fun_0 "(\<and>)"
|
|
|
44 |
time_fun_0 "(\<or>)"
|
|
|
45 |
time_fun_0 "Num.numeral_class.numeral"
|
|
|
46 |
time_fun_0 "(=)"
|
|
79490
|
47 |
|
|
|
48 |
end |