equal
deleted
inserted
replaced
24 unproved termination condition |
24 unproved termination condition |
25 \begin{quote} |
25 \begin{quote} |
26 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"} |
26 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"} |
27 \end{quote} |
27 \end{quote} |
28 where @{term"set"} returns the set of elements of a list (no special |
28 where @{term"set"} returns the set of elements of a list (no special |
29 knowledge of sets is required in the following) and @{name"term_list_size :: |
29 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 |
30 term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle |
31 (when @{name"term"} was defined). First we have to understand why the |
31 (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 |
32 recursive call of @{term"trev"} underneath @{term"map"} leads to the above |
33 condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"} |
33 condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"} |
34 will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above |
34 will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above |
35 condition expresses that the size of the argument @{term"t : set ts"} of any |
35 condition expresses that the size of the argument @{term"t : set ts"} of any |
36 recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) = |
36 recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) = |