Theory Wellfounded_Extra

theory Wellfounded_Extra
  imports
    Main
    "Ordered_Resolution_Prover.Lazy_List_Chain"
begin


subsection ‹Basic Results›

subsubsection ‹Minimal-element characterization of well-foundedness›

lemma minimal_if_wf_on:
  assumes wf: "wf_on A R" and "B ⊆ A" and "B ≠ {}"
  shows "∃z ∈ B. ∀y. (y, z) ∈ R ⟶ y ∉ B"
  using wf_on_iff_ex_minimal[THEN iffD1, rule_format, OF assms] .

lemma wfE_min':
  "wf R ⟹ Q ≠ {} ⟹ (⋀z. z ∈ Q ⟹ (⋀y. (y, z) ∈ R ⟹ y ∉ Q) ⟹ thesis) ⟹ thesis"
  using wfE_min[of R _ Q] by blast

lemma wf_on_if_minimal:
  assumes "⋀B. B ⊆ A ⟹ B ≠ {} ⟹ ∃z ∈ B. ∀y. (y, z) ∈ R ⟶ y ∉ B"
  shows "wf_on A R"
  using wf_on_iff_ex_minimal[THEN iffD2, rule_format, OF assms] .

definition inv_imagep_on :: "'a set ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where
  "inv_imagep_on A R f = (λx y. x ∈ A ∧ y ∈ A ∧ R (f x) (f y))"

lemma wfp_on_inv_imagep:
  assumes wf: "wfp_on (f ` A) R"
  shows "wfp_on A (inv_imagep R f)"
  unfolding wfp_on_iff_ex_minimal
proof (intro allI impI)
  fix B assume "B ⊆ A" and "B ≠ {}"
  hence "∃z∈f ` B. ∀y. R y z ⟶ y ∉ f ` B"
    using wf[unfolded wfp_on_iff_ex_minimal, rule_format, of "f ` B"] by blast
  thus "∃z∈B. ∀y. inv_imagep R f y z ⟶ y ∉ B"
    unfolding inv_imagep_def
    by (metis image_iff)
qed

definition lex_prodp where
  "lex_prodp RA RB x y ⟷ RA (fst x) (fst y) ∨ fst x = fst y ∧ RB (snd x) (snd y)"

lemma lex_prodp_lex_prod_iff[pred_set_conv]:
  "lex_prodp RA RB x y ⟷ (x, y) ∈ lex_prod {(x, y). RA x y} {(x, y). RB x y}"
  unfolding lex_prodp_def lex_prod_def by auto

lemma lex_prod_lex_prodp_iff:
  "lex_prod {(x, y). RA x y} {(x, y). RB x y} = {(x, y). lex_prodp RA RB x y}"
  unfolding lex_prodp_def lex_prod_def by auto

lemma wfp_on_lex_prodp: "wfp_on A RA ⟹ wfp_on B RB ⟹ wfp_on (A × B) (lex_prodp RA RB)"
  using wf_on_lex_prod[of A _ B _, to_pred, unfolded lex_prod_lex_prodp_iff, to_pred] .

corollary wfp_lex_prodp: "wfp RA ⟹ wfp RB ⟹ wfp (lex_prodp RA RB)"
  using wfp_on_lex_prodp[of UNIV _ UNIV, simplified] .

lemma wfp_on_sup_if_convertible_to_wfp:
  includes lattice_syntax
  assumes
    wf_S: "wfp_on A S" and
    wf_Q: "wfp_on (f ` A) Q" and
    convertible_R: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ Q (f x) (f y)" and
    convertible_S: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ S x y ⟹ Q (f x) (f y) ∨ f x = f y"
  shows "wfp_on A (R ⊔ S)"
proof (rule wfp_on_if_convertible_to_wfp_on)
  show "wfp_on ((λx. (f x, x)) ` A) (lex_prodp Q S)"
  proof (rule wfp_on_subset)
    show "wfp_on (f ` A × A) (lex_prodp Q S)"
      by (rule wfp_on_lex_prodp[OF wf_Q wf_S])
  next
    show "(λx. (f x, x)) ` A ⊆ f ` A × A"
      by auto
  qed
next
  fix x y
  show "x ∈ A ⟹ y ∈ A ⟹ (R ⊔ S) x y ⟹ lex_prodp Q S (f x, x) (f y, y)"
    using convertible_R convertible_S
    by (auto simp add: lex_prodp_def)
qed

lemma chain_lnth_rtranclp:
  assumes
    chain: "Lazy_List_Chain.chain R xs" and
    len: "enat j < llength xs"
  shows "R** (lhd xs) (lnth xs j)"
  using len
proof (induction j)
  case 0
  from chain obtain x xs' where "xs = LCons x xs'"
    by (auto elim: chain.cases)
  thus ?case
    by simp
next
  case (Suc j)
  then show ?case
    by (metis Suc_ile_eq chain chain_lnth_rel less_le_not_le rtranclp.simps)
qed

lemma chain_conj_rtranclpI:
  fixes xs :: "'a llist"
  assumes "Lazy_List_Chain.chain (λx y. R x y) (LCons init xs)"
  shows "Lazy_List_Chain.chain (λx y. R x y ∧ R** init x) (LCons init xs)"
proof (intro lnth_rel_chain allI impI conjI)
  show "¬ lnull (LCons init xs)"
    by simp
next
  fix j
  assume hyp: "enat (j + 1) < llength (LCons init xs)"

  from hyp show "R (lnth (LCons init xs) j) (lnth (LCons init xs) (j + 1))"
    using assms[THEN chain_lnth_rel, of j] by simp

  from hyp show "R** init (lnth (LCons init xs) j)"
    using assms[THEN chain_lnth_rtranclp, of j]
    by (simp add: Suc_ile_eq)
qed

lemma rtranclp_implies_ex_lfinite_chain:
  assumes run: "R** x0 x"
  shows "∃xs. lfinite xs ∧ chain (λy z. R y z ∧ R** x0 y) (LCons x0 xs) ∧ llast (LCons x0 xs) = x"
  using run
proof (induction x rule: rtranclp_induct)
  case base
  then show ?case
    by (meson chain.chain_singleton lfinite_code(1) llast_singleton)
next
  case (step y z)
  from step.IH obtain xs where
    "lfinite xs" and "chain (λy z. R y z ∧ R** x0 y) (LCons x0 xs)" and "llast (LCons x0 xs) = y"
    by auto
  let ?xs = "lappend xs (LCons z LNil)"
  show ?case
  proof (intro exI conjI)
    show "lfinite ?xs"
      using ‹lfinite xs› by simp
  next
    show "chain (λy z. R y z ∧ R** x0 y) (LCons x0 ?xs)"
      using ‹chain (λy z. R y z ∧ R** x0 y) (LCons x0 xs)› ‹llast (LCons x0 xs) = y›
        chain.chain_singleton chain_lappend step.hyps(1) step.hyps(2)
      by fastforce
  next
    show "llast (LCons x0 ?xs) = z"
      by (simp add: ‹lfinite xs› llast_LCons)
  qed
qed

lemma chain_conj_rtranclpD:
  fixes xs :: "'a llist"
  assumes inf: "¬ lfinite xs" and chain: "chain (λy z. R y z ∧ R** x0 y) xs"
  shows "∃ys. lfinite ys ∧ chain (λy z. R y z ∧ R** x0 y) (lappend ys xs) ∧ lhd (lappend ys xs) = x0"
  using chain
proof (cases "λy z. R y z ∧ R** x0 y" xs rule: chain.cases)
  case (chain_singleton x)
  with inf have False
    by simp
  thus ?thesis ..
next
  case (chain_cons xs' x)
  hence "R** x0 x"
    by auto
  thus ?thesis
  proof (cases R x0 x rule: rtranclp.cases)
    case rtrancl_refl
    then show ?thesis
      using chain local.chain_cons(1) by force
  next
    case (rtrancl_into_rtrancl xn)
    then obtain ys where
      lfin_ys: "lfinite ys" and
      chain_ys: "chain (λy z. R y z ∧ R** x0 y) (LCons x0 ys)" and
      llast_ys: "llast (LCons x0 ys) = xn"
      by (auto dest: rtranclp_implies_ex_lfinite_chain)
    show ?thesis
    proof (intro exI conjI)
      show "lfinite (LCons x0 ys)"
        using lfin_ys
        by simp
    next
      have "R (llast (LCons x0 ys)) (lhd xs)"
        using rtrancl_into_rtrancl(2) chain_cons(1) llast_ys
        by simp
      moreover have "R** x0 (llast (LCons x0 ys))"
        using rtrancl_into_rtrancl(1,2)
        using lappend_code(2)[of x0 ys xs]
          lhd_LCons[of x0 "(lappend ys xs)"] local.chain_cons(1)
        using llast_ys
        by fastforce
      ultimately show "chain (λy z. R y z ∧ R** x0 y) (lappend (LCons x0 ys) xs)"
        using chain_lappend[OF chain_ys chain]
        by metis
    next
      show "lhd (lappend (LCons x0 ys) xs) = x0"
        by simp
    qed 
  qed
qed

lemma wfp_on_rtranclp_conversep_iff_no_infinite_down_chain_llist:
  fixes R x0
  shows "wfp_on {x. R** x0 x} R¯¯ ⟷ (∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain R (LCons x0 xs))"
proof (rule iffI)
  assume "wfp_on {x. R** x0 x} R¯¯"
  hence "wfp (λz y. R¯¯ z y ∧ z ∈ {x. R** x0 x} ∧ y ∈ {x. R** x0 x})"
    using wfp_on_iff_wfp by blast
  hence "wfp (λz y. R y z ∧ R** x0 y)"
    by (auto elim: wfp_on_mono_strong)
  hence "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain (λy z. R y z ∧ R** x0 y) xs"
    unfolding wfP_iff_no_infinite_down_chain_llist
    by (metis (no_types, lifting) Lazy_List_Chain.chain_mono conversepI)
  hence "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain (λy z. R y z ∧ R** x0 y) (LCons x0 xs)"
    by (meson lfinite_LCons)
  thus "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain R (LCons x0 xs)"
    using chain_conj_rtranclpI
    by fastforce
next
  assume "∄xs. ¬ lfinite xs ∧ Lazy_List_Chain.chain R (LCons x0 xs)"
  hence no_inf_chain: "∄xs. ¬ lfinite xs ∧ chain (λy z. R y z ∧ R** x0 y) (LCons x0 xs)"
    by (metis (mono_tags, lifting) Lazy_List_Chain.chain_mono)
  have "∄xs. ¬ lfinite xs ∧ chain (λy z. R y z ∧ R** x0 y) xs"
  proof (rule notI, elim exE conjE)
    fix xs assume "¬ lfinite xs" and "chain (λy z. R y z ∧ R** x0 y) xs"
    then obtain ys where
      "lfinite ys" and "chain (λy z. R y z ∧ R** x0 y) (lappend ys xs)" and "lhd (lappend ys xs) = x0"
    by (auto dest: chain_conj_rtranclpD)
    hence "∃xs. ¬ lfinite xs ∧ chain (λy z. R y z ∧ R** x0 y) (LCons x0 xs)"
    proof (intro exI conjI)
      show "¬ lfinite (ltl (lappend ys xs))"
        using ‹¬ lfinite xs› lfinite_lappend lfinite_ltl
        by blast
    next
      show "chain (λy z. R y z ∧ R** x0 y) (LCons x0 (ltl (lappend ys xs)))"
        using ‹chain (λy z. R y z ∧ R** x0 y) (lappend ys xs)› ‹lhd (lappend ys xs) = x0›
          chain_not_lnull lhd_LCons_ltl
        by fastforce
    qed
    with no_inf_chain show False
      by argo
  qed
  hence "Wellfounded.wfP (λz y. R y z ∧ y ∈ {x. R** x0 x})"
    unfolding wfP_iff_no_infinite_down_chain_llist
    using Lazy_List_Chain.chain_mono by fastforce
  hence "wfp (λz y. R¯¯ z y ∧ z ∈ {x. R** x0 x} ∧ y ∈ {x. R** x0 x})"
    by (auto elim: wfp_on_mono_strong)
  thus "wfp_on {x. R** x0 x} R¯¯"
    unfolding wfp_on_iff_wfp[of "{x. R** x0 x}" "R¯¯"] by argo
qed

end