Theory Wqo_Instances

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Instances of Well-Quasi-Orders›

theory Wqo_Instances
imports Kruskal
begin


subsection ‹The Option Type is Well-Quasi-Ordered›

instantiation option :: (wqo) wqo
begin
definition "x ≤ y ⟷ option_le (≤) x y"
definition "(x :: 'a option) < y ⟷ x ≤ y ∧ ¬ (y ≤ x)"

instance
  by (rule wqo.intro_of_class)
     (auto simp: less_eq_option_def [abs_def] less_option_def [abs_def])
end


subsection ‹The Sum Type is Well-Quasi-Ordered›

instantiation sum :: (wqo, wqo) wqo
begin
definition "x ≤ y ⟷ sum_le (≤) (≤) x y"
definition "(x :: 'a + 'b) < y ⟷ x ≤ y ∧ ¬ (y ≤ x)"

instance
  by (rule wqo.intro_of_class)
     (auto simp: less_eq_sum_def [abs_def] less_sum_def [abs_def])
end


subsection ‹Pairs are Well-Quasi-Ordered›

text ‹If types @{typ "'a"} and @{typ "'b"} are well-quasi-ordered by ‹P›
and ‹Q›, then pairs of type @{typ "'a × 'b"} are well-quasi-ordered by
the pointwise combination of ‹P› and ‹Q›.›

instantiation prod :: (wqo, wqo) wqo
begin
definition "p ≤ q ⟷ prod_le (≤) (≤) p q"
definition "(p :: 'a × 'b) < q ⟷ p ≤ q ∧ ¬ (q ≤ p)"

instance
  by (rule wqo.intro_of_class)
     (auto simp: less_eq_prod_def [abs_def] less_prod_def [abs_def])
end


subsection ‹Lists are Well-Quasi-Ordered›

text ‹If the type @{typ "'a"} is well-quasi-ordered by ‹P›, then
lists of type @{typ "'a list"} are well-quasi-ordered by the homeomorphic
embedding relation.›

instantiation list :: (wqo) wqo
begin
definition "xs ≤ ys ⟷ list_emb (≤) xs ys"
definition "(xs :: 'a list) < ys ⟷ xs ≤ ys ∧ ¬ (ys ≤ xs)"

instance
  by (rule wqo.intro_of_class)
     (auto simp: less_eq_list_def [abs_def] less_list_def [abs_def])
end

end