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