equal
deleted
inserted
replaced
143 That is, @{term"while b c s"} is equivalent to the imperative program |
143 That is, @{term"while b c s"} is equivalent to the imperative program |
144 \begin{verbatim} |
144 \begin{verbatim} |
145 x := s; while b(x) do x := c(x); return x |
145 x := s; while b(x) do x := c(x); return x |
146 \end{verbatim} |
146 \end{verbatim} |
147 In general, @{term s} will be a tuple (better still: a record). As an example |
147 In general, @{term s} will be a tuple (better still: a record). As an example |
148 consider the tail recursive variant of function @{term find} above: |
148 consider the following definition of function @{term find} above: |
149 *} |
149 *} |
150 |
150 |
151 constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
151 constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
152 "find2 f x \<equiv> |
152 "find2 f x \<equiv> |
153 fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))" |
153 fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))" |