21 Remember that function @{term size} is defined for each \isacommand{datatype}. |
21 Remember that function @{term size} is defined for each \isacommand{datatype}. |
22 However, the definition does not succeed. Isabelle complains about an |
22 However, the definition does not succeed. Isabelle complains about an |
23 unproved termination condition |
23 unproved termination condition |
24 @{prop[display]"t : set ts --> size t < Suc (size_term_list ts)"} |
24 @{prop[display]"t : set ts --> size t < Suc (size_term_list ts)"} |
25 where @{term set} returns the set of elements of a list |
25 where @{term set} returns the set of elements of a list |
26 and @{text"size_term_list :: term list \<Rightarrow> nat"} is an auxiliary |
26 and \<open>size_term_list :: term list \<Rightarrow> nat\<close> is an auxiliary |
27 function automatically defined by Isabelle |
27 function automatically defined by Isabelle |
28 (while processing the declaration of @{text term}). Why does the |
28 (while processing the declaration of \<open>term\<close>). Why does the |
29 recursive call of @{const trev} lead to this |
29 recursive call of @{const trev} lead to this |
30 condition? Because \isacommand{recdef} knows that @{term map} |
30 condition? Because \isacommand{recdef} knows that @{term map} |
31 will apply @{const trev} only to elements of @{term ts}. Thus the |
31 will apply @{const trev} only to elements of @{term ts}. Thus the |
32 condition expresses that the size of the argument @{prop"t : set ts"} of any |
32 condition expresses that the size of the argument @{prop"t : set ts"} of any |
33 recursive call of @{const trev} is strictly less than @{term"size(App f ts)"}, |
33 recursive call of @{const trev} is strictly less than @{term"size(App f ts)"}, |