equal
deleted
inserted
replaced
32 of an equation and $r$ the argument of some recursive call on the |
32 of an equation and $r$ the argument of some recursive call on the |
33 corresponding right-hand side, induces a wellfounded relation. |
33 corresponding right-hand side, induces a wellfounded relation. |
34 |
34 |
35 The HOL library formalizes |
35 The HOL library formalizes |
36 some of the theory of wellfounded relations. For example |
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 |
37 \<^prop>\<open>wf r\<close>\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is |
38 wellfounded. |
38 wellfounded. |
39 Finally we should mention that HOL already provides the mother of all |
39 Finally we should mention that HOL already provides the mother of all |
40 inductions, \textbf{wellfounded |
40 inductions, \textbf{wellfounded |
41 induction}\indexbold{induction!wellfounded}\index{wellfounded |
41 induction}\indexbold{induction!wellfounded}\index{wellfounded |
42 induction|see{induction, wellfounded}} (@{thm[source]wf_induct}): |
42 induction|see{induction, wellfounded}} (@{thm[source]wf_induct}): |
43 @{thm[display]wf_induct[no_vars]} |
43 @{thm[display]wf_induct[no_vars]} |
44 where @{term"wf r"} means that the relation @{term r} is wellfounded |
44 where \<^term>\<open>wf r\<close> means that the relation \<^term>\<open>r\<close> is wellfounded |
45 |
45 |
46 \<close> |
46 \<close> |
47 |
47 |
48 text\<open> |
48 text\<open> |
49 |
49 |