Theory Wellfounded_Extra

theory Wellfounded_Extra
  imports
    Main
    "Ordered_Resolution_Prover.Lazy_List_Chain"
begin

lemma wf_onI:
  "(⋀P x. (⋀y. y ∈ A ⟹ (⋀z. z ∈ A ⟹ (z, y) ∈ r ⟹ P z) ⟹ P y) ⟹ x ∈ A ⟹ P x) ⟹ wf_on A r"
  unfolding wf_on_def by metis

lemma wfI: "(⋀P x. (⋀y. (⋀z. (z, y) ∈ r ⟹ P z) ⟹ P y) ⟹ P x) ⟹ wf r"
  by (auto simp: wf_on_def)

lemma wf_on_induct[consumes 1, case_names less in_dom]:
  assumes
    "wf_on A r" and
    "⋀x. x ∈ A ⟹ (⋀y. y ∈ A ⟹ (y, x) ∈ r ⟹ P y) ⟹ P x" and
    "x ∈ A"
  shows "P x"
  using assms unfolding wf_on_def by metis


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_onE_pf[OF wf ‹B ⊆ A›]
  by (metis Image_iff assms(3) subsetI)

lemma wfE_min:
  assumes wf: "wf R" and Q: "x ∈ Q"
  obtains z where "z ∈ Q" "⋀y. (y, z) ∈ R ⟹ y ∉ Q"
  using Q wfE_pf[OF wf, of Q] by blast

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"
proof (rule wf_onI_pf)
  fix B
  show "B ⊆ A ⟹ B ⊆ R `` B ⟹ B = {}"
  using assms by (metis ImageE subset_eq)
qed

lemma ex_trans_min_element_if_wf_on:
  assumes wf: "wf_on A r" and x_in: "x ∈ A"
  shows "∃y ∈ A. (y, x) ∈ r* ∧ ¬(∃z ∈ A. (z, y) ∈ r)"
  using wf
proof (induction x rule: wf_on_induct)
  case (less x)
  thus ?case
    by (metis rtrancl.rtrancl_into_rtrancl rtrancl.rtrancl_refl)
next
  case in_dom
  thus ?case
    using x_in by metis
qed

lemma ex_trans_min_element_if_wfp_on: "wfp_on A R ⟹ x ∈ A ⟹ ∃y∈A. R** y x ∧ ¬ (∃z∈A. R z y)"
  by (rule ex_trans_min_element_if_wf_on[to_pred])

text ‹Well-foundedness of the empty relation›

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

lemma wfp_on_if_convertible_to_wfp:
  assumes
    wf: "wfp_on (f ` A) Q" and
    convertible: "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ R x y ⟹ Q (f x) (f y))"
  shows "wfp_on A R"
  unfolding wfp_on_iff_ex_minimal
proof (intro allI impI)
  fix B assume "B ⊆ A" and "B ≠ {}"
  moreover from wf have "wfp_on A (inv_imagep Q f)"
    by (rule wfp_on_inv_imagep)
  ultimately obtain y where "y ∈ B" and "⋀z. Q (f z) (f y) ⟹ z ∉ B"
    unfolding wfp_on_iff_ex_minimal in_inv_imagep by metis
  thus "∃z ∈ B. ∀y. R y z ⟶ y ∉ B"
    using ‹B ⊆ A› convertible by blast
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 wf_on_lex_prod:
  assumes wfA: "wf_on A rA" and wfB: "wf_on B rB" and AB_subset: "AB ⊆ A × B"
  shows "wf_on AB (rA <*lex*> rB)"
  unfolding wf_on_iff_ex_minimal
proof (intro allI impI)
  fix AB' assume "AB' ⊆ AB" and "AB' ≠ {}"
  hence "fst ` AB' ⊆ A" and "snd ` AB' ⊆ B"
    using AB_subset by auto

  from ‹fst ` AB' ⊆ A› ‹AB' ≠ {}› obtain a where
    a_in: "a ∈ fst ` AB'" and
    a_minimal: "(∀y. (y, a) ∈ rA ⟶ y ∉ fst ` AB')"
    using wfA[unfolded wf_on_iff_ex_minimal, rule_format, of "fst ` AB'"]
    by auto

  from ‹snd ` AB' ⊆ B› ‹AB' ≠ {}› a_in obtain b where
    b_in: "b ∈ snd ` {p ∈ AB'. fst p = a}" and
    b_minimal: "(∀y. (y, b) ∈ rB ⟶ y ∉ snd ` {p ∈ AB'. fst p = a})"
    using wfB[unfolded wf_on_iff_ex_minimal, rule_format, of "snd ` {p ∈ AB'. fst p = a}"]
    by blast

  show "∃z∈AB'. ∀y. (y, z) ∈ rA <*lex*> rB ⟶ y ∉ AB'"
  proof (rule bexI)
    show "(a, b) ∈ AB'"
      using b_in by (simp add: image_iff)
  next
    show "∀y. (y, (a, b)) ∈ rA <*lex*> rB ⟶ y ∉ AB'"
    proof (intro allI impI)
      fix p assume "(p, (a, b)) ∈ rA <*lex*> rB"
      hence "(fst p, a) ∈ rA ∨ fst p = a ∧ (snd p, b) ∈ rB"
        unfolding lex_prod_def by auto
      thus "p ∉ AB'"
      proof (elim disjE conjE)
        assume "(fst p, a) ∈ rA"
        hence "fst p ∉ fst ` AB'"
          using a_minimal by simp
        thus ?thesis
          by (rule contrapos_nn) simp
      next
        assume "fst p = a" and "(snd p, b) ∈ rB"
        hence "snd p ∉ snd ` {p ∈ AB'. fst p = a}"
          using b_minimal by simp
        thus "p ∉ AB'"
          by (rule contrapos_nn) (simp add: ‹fst p = a›)
      qed
    qed
  qed
qed

lemma wfp_on_lex_prodp: "wfp_on A RA ⟹ wfp_on B RB ⟹ AB ⊆ A × B ⟹ wfp_on AB (lex_prodp RA RB)"
  using wf_on_lex_prod[of A _ B _ AB, 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)
  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 subset_refl])
  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 wfp_on_iff_wfp: "wfp_on A R ⟷ wfp (λx y. R x y ∧  x ∈ A ∧ y ∈ A)"
  by (smt (verit, del_insts) UNIV_I subsetI wfp_on_def wfp_on_antimono_strong wfp_on_subset)

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_antimono_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_antimono_strong)
  thus "wfp_on {x. R** x0 x} R¯¯"
    unfolding wfp_on_iff_wfp[of "{x. R** x0 x}" "R¯¯"] by argo
qed

end