(* Title: Dual_Order.thy Author: Jose Divasón <jose.divasonm at unirioja.es> Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> *) section "Dual Order" theory Dual_Order imports Main begin subsection‹Interpretation of dual wellorder based on wellorder› lemma wf_wellorderI2: assumes wf: "wf {(x::'a::ord, y). y < x}" assumes lin: "class.linorder (λ(x::'a) y::'a. y ≤ x) (λ(x::'a) y::'a. y < x)" shows "class.wellorder (λ(x::'a) y::'a. y ≤ x) (λ(x::'a) y::'a. y < x)" using lin unfolding class.wellorder_def apply (rule conjI) apply (rule class.wellorder_axioms.intro) by (blast intro: wf_induct_rule [OF wf])