60 |
60 |
61 As a simple example we define division on @{typ nat}: |
61 As a simple example we define division on @{typ nat}: |
62 *} |
62 *} |
63 |
63 |
64 consts divi :: "nat \<times> nat \<Rightarrow> nat" |
64 consts divi :: "nat \<times> nat \<Rightarrow> nat" |
65 recdef (permissive) divi "measure(\<lambda>(m,n). m)" |
65 recdef divi "measure(\<lambda>(m,n). m)" |
66 "divi(m,n) = (if n = 0 then arbitrary else |
66 "divi(m,0) = arbitrary" |
67 if m < n then 0 else divi(m-n,n)+1)" (* FIXME hide permissive!? *) |
67 "divi(m,n) = (if m < n then 0 else divi(m-n,n)+1)" |
68 |
68 |
69 text{*\noindent Of course we could also have defined |
69 text{*\noindent Of course we could also have defined |
70 @{term"divi(m,0)"} to be some specific number, for example 0. The |
70 @{term"divi(m,0)"} to be some specific number, for example 0. The |
71 latter option is chosen for the predefined @{text div} function, which |
71 latter option is chosen for the predefined @{text div} function, which |
72 simplifies proofs at the expense of deviating from the |
72 simplifies proofs at the expense of deviating from the |
73 standard mathematical division function. |
73 standard mathematical division function. |
74 |
74 |
75 As a more substantial example we consider the problem of searching a graph. |
75 As a more substantial example we consider the problem of searching a graph. |
76 For simplicity our graph is given by a function @{term f} of |
76 For simplicity our graph is given by a function @{term f} of |
77 type @{typ"'a \<Rightarrow> 'a"} which |
77 type @{typ"'a \<Rightarrow> 'a"} which |
78 maps each node to its successor; the graph is really a tree. |
78 maps each node to its successor; the graph has out-degree 1. |
79 The task is to find the end of a chain, modelled by a node pointing to |
79 The task is to find the end of a chain, modelled by a node pointing to |
80 itself. Here is a first attempt: |
80 itself. Here is a first attempt: |
81 @{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"} |
81 @{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"} |
82 This may be viewed as a fixed point finder or as one half of the well known |
82 This may be viewed as a fixed point finder or as the second half of the well |
83 \emph{Union-Find} algorithm. |
83 known \emph{Union-Find} algorithm. |
84 The snag is that it may not terminate if @{term f} has non-trivial cycles. |
84 The snag is that it may not terminate if @{term f} has non-trivial cycles. |
85 Phrased differently, the relation |
85 Phrased differently, the relation |
86 *} |
86 *} |
87 |
87 |
88 constdefs step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set" |
88 constdefs step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set" |