Theory VeriComp.Well_founded

section ‹Well-foundedness of Relations Defined as Predicate Functions›

theory Well_founded
  imports Main
begin

locale well_founded =
  fixes R :: "'a ⇒ 'a ⇒ bool" (infix "⊏" 70)
  assumes
    wf: "wfP (⊏)"
begin

lemmas induct = wfP_induct_rule[OF wf]

end

subsection ‹Unit›

lemma wfP_unit: "wfP (λ() (). False)"
  by (simp add: Nitpick.case_unit_unfold wfP_eq_minimal)

interpretation well_founded "λ() (). False"
  apply unfold_locales
  by (auto intro: wfP_unit)

subsection ‹Lexicographic product›

context
  fixes
    r1 :: "'a ⇒ 'a ⇒ bool" and
    r2 :: "'b ⇒ 'b ⇒ bool"
begin

definition lex_prodp :: "'a × 'b ⇒ 'a × 'b ⇒ bool" where
  "lex_prodp x y ≡ r1 (fst x) (fst y) ∨ fst x = fst y ∧ r2 (snd x) (snd y)"

lemma lex_prodp_lex_prod:
  shows "lex_prodp x y ⟷ (x, y) ∈ lex_prod { (x, y). r1 x y } { (x, y). r2 x y }"
  by (auto simp: lex_prod_def lex_prodp_def)

lemma lex_prodp_wfP:
  assumes
    "wfP r1" and
    "wfP r2"
  shows "wfP lex_prodp"
proof (rule wfPUNIVI)
  show "⋀P. ∀x. (∀y. lex_prodp y x ⟶ P y) ⟶ P x ⟹ (⋀x. P x)"
  proof -
    fix P
    assume "∀x. (∀y. lex_prodp y x ⟶ P y) ⟶ P x"
    hence hyps: "(⋀y1 y2. lex_prodp (y1, y2) (x1, x2) ⟹ P (y1, y2)) ⟹ P (x1, x2)" for x1 x2
      by fast
    show "(⋀x. P x)"
      apply (simp only: split_paired_all)
      apply (atomize (full))
      apply (rule allI)
      apply (rule wfP_induct_rule[OF assms(1), of "λy. ∀b. P (y, b)"])
      apply (rule allI)
      apply (rule wfP_induct_rule[OF assms(2), of "λb. P (x, b)" for x])
      using hyps[unfolded lex_prodp_def, simplified]
      by blast
  qed
qed

end

lemma lex_prodp_well_founded:
  assumes
    "well_founded r1" and
    "well_founded r2"
  shows "well_founded (lex_prodp r1 r2)"
  using well_founded.intro lex_prodp_wfP assms[THEN well_founded.wf] by auto

subsection ‹Lexicographic list›

context
  fixes order :: "'a ⇒ 'a ⇒ bool"
begin

inductive lexp :: "'a list ⇒ 'a list ⇒ bool" where
  lexp_head: "order x y ⟹ length xs = length ys ⟹ lexp (x # xs) (y # ys)" |
  lexp_tail: "lexp xs ys ⟹ lexp (x # xs) (x # ys)"

end

lemma lexp_prepend: "lexp order ys zs ⟹ lexp order (xs @ ys) (xs @ zs)"
  by (induction xs) (simp_all add: lexp_tail)

lemma lexp_lex: "lexp order xs ys ⟷ (xs, ys) ∈ lex {(x, y). order x y}"
proof
  assume "lexp order xs ys"
  thus "(xs, ys) ∈ lex {(x, y). order x y}"
    by (induction xs ys rule: lexp.induct) simp_all
next
  assume "(xs, ys) ∈ lex {(x, y). order x y}"
  thus "lexp order xs ys"
    by (auto intro!: lexp_prepend intro: lexp_head simp: lex_conv)
qed

lemma lex_list_wfP: "wfP order ⟹ wfP (lexp order)"
  by (simp add: lexp_lex wf_lex wfP_def)

lemma lex_list_well_founded:
  assumes "well_founded order"
  shows "well_founded (lexp order)"
  using well_founded.intro assms(1)[THEN well_founded.wf, THEN lex_list_wfP] by auto

end