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  yA. R** y x  ¬ (zA. 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 "zf ` B. y. R y z  y  f ` B"
    using wf[unfolded wfp_on_iff_ex_minimal, rule_format, of "f ` B"] by blast
  thus "zB. 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 "zAB'. 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