equal
deleted
inserted
replaced
76 apply (simp add: wellorder_class.intro class.wellorder_axioms.intro wf_induct_rule [OF wf]) |
76 apply (simp add: wellorder_class.intro class.wellorder_axioms.intro wf_induct_rule [OF wf]) |
77 done |
77 done |
78 |
78 |
79 lemma (in wellorder) wf: "wf {(x, y). x < y}" |
79 lemma (in wellorder) wf: "wf {(x, y). x < y}" |
80 unfolding wf_def by (blast intro: less_induct) |
80 unfolding wf_def by (blast intro: less_induct) |
|
81 |
|
82 lemma (in wellorder) wfP_less[simp]: "wfP (<)" |
|
83 by (simp add: wf wfP_def) |
81 |
84 |
82 |
85 |
83 subsection \<open>Basic Results\<close> |
86 subsection \<open>Basic Results\<close> |
84 |
87 |
85 text \<open>Point-free characterization of well-foundedness\<close> |
88 text \<open>Point-free characterization of well-foundedness\<close> |