equal
deleted
inserted
replaced
66 lemma wf_wellorderI: |
66 lemma wf_wellorderI: |
67 assumes wf: "wf {(x::'a::ord, y). x < y}" |
67 assumes wf: "wf {(x::'a::ord, y). x < y}" |
68 assumes lin: "OFCLASS('a::ord, linorder_class)" |
68 assumes lin: "OFCLASS('a::ord, linorder_class)" |
69 shows "OFCLASS('a::ord, wellorder_class)" |
69 shows "OFCLASS('a::ord, wellorder_class)" |
70 using lin by (rule wellorder_class.intro) |
70 using lin by (rule wellorder_class.intro) |
71 (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf]) |
71 (rule class.wellorder_axioms.intro, rule wf_induct_rule [OF wf], simp) |
72 |
72 |
73 lemma (in wellorder) wf: |
73 lemma (in wellorder) wf: |
74 "wf {(x, y). x < y}" |
74 "wf {(x, y). x < y}" |
75 unfolding wf_def by (blast intro: less_induct) |
75 unfolding wf_def by (blast intro: less_induct) |
76 |
76 |