|
1 theory Recur imports Main begin |
|
2 |
|
3 |
|
4 text{* |
|
5 @{thm[display] mono_def[no_vars]} |
|
6 \rulename{mono_def} |
|
7 |
|
8 @{thm[display] monoI[no_vars]} |
|
9 \rulename{monoI} |
|
10 |
|
11 @{thm[display] monoD[no_vars]} |
|
12 \rulename{monoD} |
|
13 |
|
14 @{thm[display] lfp_unfold[no_vars]} |
|
15 \rulename{lfp_unfold} |
|
16 |
|
17 @{thm[display] lfp_induct[no_vars]} |
|
18 \rulename{lfp_induct} |
|
19 |
|
20 @{thm[display] gfp_unfold[no_vars]} |
|
21 \rulename{gfp_unfold} |
|
22 |
|
23 @{thm[display] coinduct[no_vars]} |
|
24 \rulename{coinduct} |
|
25 *} |
|
26 |
|
27 text{*\noindent |
|
28 A relation $<$ is |
|
29 \bfindex{wellfounded} if it has no infinite descending chain $\cdots < |
|
30 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set |
|
31 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side |
|
32 of an equation and $r$ the argument of some recursive call on the |
|
33 corresponding right-hand side, induces a wellfounded relation. |
|
34 |
|
35 The HOL library formalizes |
|
36 some of the theory of wellfounded relations. For example |
|
37 @{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is |
|
38 wellfounded. |
|
39 Finally we should mention that HOL already provides the mother of all |
|
40 inductions, \textbf{wellfounded |
|
41 induction}\indexbold{induction!wellfounded}\index{wellfounded |
|
42 induction|see{induction, wellfounded}} (@{thm[source]wf_induct}): |
|
43 @{thm[display]wf_induct[no_vars]} |
|
44 where @{term"wf r"} means that the relation @{term r} is wellfounded |
|
45 |
|
46 *} |
|
47 |
|
48 text{* |
|
49 |
|
50 @{thm[display] wf_induct[no_vars]} |
|
51 \rulename{wf_induct} |
|
52 |
|
53 @{thm[display] less_than_iff[no_vars]} |
|
54 \rulename{less_than_iff} |
|
55 |
|
56 @{thm[display] inv_image_def[no_vars]} |
|
57 \rulename{inv_image_def} |
|
58 |
|
59 @{thm[display] measure_def[no_vars]} |
|
60 \rulename{measure_def} |
|
61 |
|
62 @{thm[display] wf_less_than[no_vars]} |
|
63 \rulename{wf_less_than} |
|
64 |
|
65 @{thm[display] wf_inv_image[no_vars]} |
|
66 \rulename{wf_inv_image} |
|
67 |
|
68 @{thm[display] wf_measure[no_vars]} |
|
69 \rulename{wf_measure} |
|
70 |
|
71 @{thm[display] lex_prod_def[no_vars]} |
|
72 \rulename{lex_prod_def} |
|
73 |
|
74 @{thm[display] wf_lex_prod[no_vars]} |
|
75 \rulename{wf_lex_prod} |
|
76 |
|
77 *} |
|
78 |
|
79 end |
|
80 |