equal
deleted
inserted
replaced
20 |
20 |
21 text{*\noindent |
21 text{*\noindent |
22 Remember that function @{term"size"} is defined for each \isacommand{datatype}. |
22 Remember that function @{term"size"} is defined for each \isacommand{datatype}. |
23 However, the definition does not succeed. Isabelle complains about an |
23 However, the definition does not succeed. Isabelle complains about an |
24 unproved termination condition |
24 unproved termination condition |
25 \begin{quote} |
|
26 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"} |
25 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"} |
27 \end{quote} |
|
28 where @{term"set"} returns the set of elements of a list (no special |
26 where @{term"set"} returns the set of elements of a list (no special |
29 knowledge of sets is required in the following) and @{text"term_list_size :: |
27 knowledge of sets is required in the following) and @{text"term_list_size :: |
30 term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle |
28 term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle |
31 (when @{text"term"} was defined). First we have to understand why the |
29 (when @{text"term"} was defined). First we have to understand why the |
32 recursive call of @{term"trev"} underneath @{term"map"} leads to the above |
30 recursive call of @{term"trev"} underneath @{term"map"} leads to the above |