1 theory Recur imports Main begin
3 ML "Pretty.margin_default := 64"
7 @{thm[display] mono_def[no_vars]}
10 @{thm[display] monoI[no_vars]}
13 @{thm[display] monoD[no_vars]}
16 @{thm[display] lfp_unfold[no_vars]}
19 @{thm[display] lfp_induct[no_vars]}
22 @{thm[display] gfp_unfold[no_vars]}
25 @{thm[display] coinduct[no_vars]}
31 \bfindex{wellfounded} if it has no infinite descending chain $\cdots <
32 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
33 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
34 of an equation and $r$ the argument of some recursive call on the
35 corresponding right-hand side, induces a wellfounded relation.
37 The HOL library formalizes
38 some of the theory of wellfounded relations. For example
39 @{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
41 Finally we should mention that HOL already provides the mother of all
42 inductions, \textbf{wellfounded
43 induction}\indexbold{induction!wellfounded}\index{wellfounded
44 induction|see{induction, wellfounded}} (@{thm[source]wf_induct}):
45 @{thm[display]wf_induct[no_vars]}
46 where @{term"wf r"} means that the relation @{term r} is wellfounded
52 @{thm[display] wf_induct[no_vars]}
55 @{thm[display] less_than_iff[no_vars]}
56 \rulename{less_than_iff}
58 @{thm[display] inv_image_def[no_vars]}
59 \rulename{inv_image_def}
61 @{thm[display] measure_def[no_vars]}
62 \rulename{measure_def}
64 @{thm[display] wf_less_than[no_vars]}
65 \rulename{wf_less_than}
67 @{thm[display] wf_inv_image[no_vars]}
68 \rulename{wf_inv_image}
70 @{thm[display] wf_measure[no_vars]}
73 @{thm[display] lex_prod_def[no_vars]}
74 \rulename{lex_prod_def}
76 @{thm[display] wf_lex_prod[no_vars]}
77 \rulename{wf_lex_prod}