Theory Wellfounded_More

(*  Title:       More about Relations
    Author:      Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>
*)
section ‹Transitions›

text ‹This theory contains some facts about closure, the definition of full transformations, and
  well-foundedness.›

theory Wellfounded_More
imports Main

begin

subsection ‹More theorems about Closures›

text ‹This is the equivalent of @{thm rtranclp_mono} for @{term tranclp}›
lemma tranclp_mono_explicit:
  "r⇧+⇧+ a b ⟹ r ≤ s ⟹ s⇧+⇧+ a b"
    using rtranclp_mono by (auto dest!: tranclpD intro: rtranclp_into_tranclp2)

lemma tranclp_mono:
  assumes mono: "r ≤ s"
  shows "r⇧+⇧+ ≤ s⇧+⇧+"
    using rtranclp_mono[OF mono] mono by (auto dest!: tranclpD intro: rtranclp_into_tranclp2)

lemma tranclp_idemp_rel:
  "R⇧+⇧+⇧+⇧+ a b ⟷ R⇧+⇧+ a b"
  apply (rule iffI)
    prefer 2 apply blast
  by (induction rule: tranclp_induct) auto

text ‹Equivalent of @{thm rtranclp_idemp}›
lemma trancl_idemp: "(r⇧+)⇧+ = r⇧+"
  by simp

lemmas tranclp_idemp[simp] = trancl_idemp[to_pred]

text ‹This theorem already exists as @{thm Nitpick.rtranclp_unfold} (and sledgehammer uses it), but
  it makes sense to duplicate it, because it is unclear how stable the lemmas in the
  @{file "~~/src/HOL/Nitpick.thy"} theory are.›
lemma rtranclp_unfold: "rtranclp r a b ⟷ (a = b ∨ tranclp r a b)"
  by (meson rtranclp.simps rtranclpD tranclp_into_rtranclp)

(* TODO destruction rule instead of simp rule *)
lemma tranclp_unfold_end: "tranclp r a b ⟷ (∃a'. rtranclp r a a' ∧ r a' b)"
  by (metis rtranclp.rtrancl_refl rtranclp_into_tranclp1 tranclp.cases tranclp_into_rtranclp)

text ‹Near duplicate of @{thm tranclpD}:›
lemma tranclp_unfold_begin: "tranclp r a b ⟷ (∃a'. r a a' ∧ rtranclp r a' b)"
  by (meson rtranclp_into_tranclp2 tranclpD)

lemma trancl_set_tranclp: "(a, b) ∈ {(b,a). P a b}⇧+ ⟷ P⇧+⇧+ b a"
  apply (rule iffI)
    apply (induction rule: trancl_induct; simp)
  apply (induction rule: tranclp_induct; auto simp: trancl_into_trancl2)
  done

lemma tranclp_rtranclp_rtranclp_rel: "R⇧+⇧+⇧*⇧* a b ⟷ R⇧*⇧* a b"
  by (simp add: rtranclp_unfold)

lemma tranclp_rtranclp_rtranclp[simp]: "R⇧+⇧+⇧*⇧* = R⇧*⇧*"
  by (fastforce simp: rtranclp_unfold)

lemma rtranclp_exists_last_with_prop:
  assumes "R x z"
  and "R⇧*⇧* z z'" and "P x z"
  shows "∃y y'. R⇧*⇧* x y ∧ R y y' ∧ P y y' ∧ (λa b. R a b ∧ ¬P a b)⇧*⇧* y' z'"
  using assms(2,1,3)
proof (induction)
  case base
  then show ?case by auto
next
  case (step z' z'') note z = this(2) and IH =this(3)[OF this(4-5)]
  show ?case
    apply (cases "P z' z''")
      apply (rule exI[of _ z'], rule exI[of _ z''])
      using z assms(1) step.hyps(1) step.prems(2) apply auto[1]
    using IH z rtranclp.rtrancl_into_rtrancl by fastforce
qed

lemma rtranclp_and_rtranclp_left: "(λ a b. P a b ∧ Q a b)⇧*⇧* S T ⟹ P⇧*⇧* S T"
  by (induction rule: rtranclp_induct) auto

subsection ‹Full Transitions›
text ‹We define here properties to define properties after all possible transitions.›
abbreviation "no_step step S ≡ (∀S'. ¬step S S')"

definition full1 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" (*"_⇧+⇧↓"*) where
"full1 transf = (λS S'. tranclp transf S S' ∧ (∀S''. ¬ transf S' S''))"

definition full:: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" (*"_⇧↓"*) where
"full transf = (λS S'. rtranclp transf S S' ∧ (∀S''. ¬ transf S' S''))"

text ‹We define output notations only for printing:›
notation (output) full1 ("_⇧+⇧↓") 
notation (output) full ("_⇧↓")

lemma rtranclp_full1I:
  "R⇧*⇧* a b ⟹ full1 R b c ⟹ full1 R a c"
  unfolding full1_def by auto

lemma tranclp_full1I:
  "R⇧+⇧+ a b ⟹ full1 R b c ⟹ full1 R a c"
  unfolding full1_def by auto

lemma rtranclp_fullI:
  "R⇧*⇧* a b ⟹ full R b c ⟹ full R a c"
  unfolding full_def by auto

lemma tranclp_full_full1I:
  "R⇧+⇧+ a b ⟹ full R b c ⟹ full1 R a c"
  unfolding full_def full1_def by auto

lemma full_fullI:
  "R a b ⟹ full R b c ⟹ full1 R a c"
  unfolding full_def full1_def by auto

lemma full_unfold:
  "full r S S' ⟷ ((S = S' ∧ no_step r S') ∨ full1 r S S')"
  unfolding full_def full1_def by (auto simp add: rtranclp_unfold)

lemma full1_is_full[intro]: "full1 R S T ⟹ full R S T"
  by (simp add: full_unfold)

lemma not_full1_rtranclp_relation: "¬full1 R⇧*⇧* a b"
  by (meson full1_def rtranclp.rtrancl_refl)

lemma not_full_rtranclp_relation: "¬full R⇧*⇧* a b"
  by (meson full_fullI not_full1_rtranclp_relation rtranclp.rtrancl_refl)

lemma full1_tranclp_relation_full:
  "full1 R⇧+⇧+ a b ⟷ full1 R a b"
  by (metis converse_tranclpE full1_def reflclp_tranclp rtranclpD rtranclp_idemp rtranclp_reflclp
    tranclp.r_into_trancl tranclp_into_rtranclp)

lemma full_tranclp_relation_full:
  "full R⇧+⇧+ a b ⟷ full R a b"
  by (metis full_unfold full1_tranclp_relation_full tranclp.r_into_trancl tranclpD)

lemma rtranclp_full1_eq_or_full1:
  "(full1 R)⇧*⇧* a b ⟷ (a = b ∨ full1 R a b)"
proof -
  have "∀p a aa. ¬ p⇧*⇧* (a::'a) aa ∨ a = aa ∨ (∃ab. p⇧*⇧* a ab ∧ p ab aa)"
    by (metis rtranclp.cases)
  then obtain aa :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a" where
    f1: "∀p a ab. ¬ p⇧*⇧* a ab ∨ a = ab ∨ p⇧*⇧* a (aa p a ab) ∧ p (aa p a ab) ab"
    by moura
  { assume "a ≠ b"
    { assume "¬ full1 R a b ∧ a ≠ b"
      then have "a ≠ b ∧ a ≠ b ∧ ¬ full1 R (aa (full1 R) a b) b ∨ ¬ (full1 R)⇧*⇧* a b ∧ a ≠ b"
        using f1 by (metis (no_types) full1_def full1_tranclp_relation_full)
      then have ?thesis
        using f1 by blast }
    then have ?thesis
      by auto }
  then show ?thesis
    by fastforce
qed

lemma tranclp_full1_full1:
  "(full1 R)⇧+⇧+ a b ⟷ full1 R a b"
  by (metis full1_def rtranclp_full1_eq_or_full1 tranclp_unfold_begin)

subsection ‹Well-Foundedness and Full Transitions›
lemma wf_exists_normal_form:
  assumes wf:"wf {(x, y). R y x}"
  shows "∃b. R⇧*⇧* a b ∧ no_step R b"
proof (rule ccontr)
  assume "¬ ?thesis"
  then have H: "⋀b. ¬ R⇧*⇧* a b ∨ ¬no_step R b"
    by blast
  def F ≡ "rec_nat a (λi b. SOME c. R b c)"
  have [simp]: "F 0 = a"
    unfolding F_def by auto
  have [simp]: "⋀i. F (Suc i) = (SOME b. R (F i) b)"
    using F_def by simp
  { fix i
    have "∀j<i. R (F j) (F (Suc j))"
      proof (induction i)
        case 0
        then show ?case by auto
      next
        case (Suc i)
        then have "R⇧*⇧* a (F i)"
          by (induction i) auto
        then have "R (F i) (SOME b. R (F i) b)"
          using H by (simp add: someI_ex)
        then have "∀j < Suc i. R (F j) (F (Suc j))"
          using H Suc by (simp add: less_Suc_eq)
        then show ?case by fast
      qed
  }
  then have "∀j. R (F j) (F (Suc j))" by blast
  then show False
    using wf unfolding wfP_def wf_iff_no_infinite_down_chain by blast
qed

lemma wf_exists_normal_form_full:
  assumes wf:"wf {(x, y). R y x}"
  shows "∃b. full R a b"
  using wf_exists_normal_form[OF assms] unfolding full_def by blast

subsection ‹More Well-Foundedness›
text ‹A little list of theorems that could be useful, but are hidden:
  ▪ link between @{term wf} and infinite chains: @{thm wf_iff_no_infinite_down_chain},
  @{thm wf_no_infinite_down_chainE}›

lemma wf_if_measure_in_wf:
  "wf R ⟹ (⋀a b. (a, b) ∈ S ⟹ (ν a, ν b)∈R) ⟹ wf S"
  by (metis in_inv_image wfE_min wfI_min wf_inv_image)

lemma wfP_if_measure: fixes f :: "'a ⇒ nat"
shows "(⋀x y. P x ⟹ g x y  ⟹ f y < f x) ⟹ wf {(y,x). P x ∧ g x y}"
  apply(insert wf_measure[of f])
  apply(simp only: measure_def inv_image_def less_than_def less_eq)
  apply(erule wf_subset)
  apply auto
  done

lemma wf_if_measure_f:
assumes "wf r"
shows "wf {(b, a). (f b, f a) ∈ r}"
  using assms by (metis inv_image_def wf_inv_image)

lemma wf_wf_if_measure':
assumes "wf r" and H: "(⋀x y. P x ⟹ g x y ⟹ (f y, f x) ∈ r)"
shows "wf {(y,x). P x ∧ g x y}"
proof -
  have "wf {(b, a). (f b, f a) ∈ r}" using assms(1) wf_if_measure_f by auto
  then have "wf {(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r}"
    using wf_subset[of _ "{(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r}"] by auto
  moreover have "{(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r} ⊆ {(b, a). (f b, f a) ∈ r}" by auto
  moreover have "{(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r} = {(b, a). P a ∧ g a b}" using H by auto
  ultimately show ?thesis using wf_subset by simp
qed

lemma wf_lex_less: "wf (lex {(a, b). (a::nat) < b})"
proof -
  have m: "{(a, b). a < b} = measure id" by auto
  show ?thesis apply (rule wf_lex) unfolding m by auto
qed

lemma wfP_if_measure2: fixes f :: "'a ⇒ nat"
shows "(⋀x y. P x y ⟹ g x y  ⟹ f x < f y) ⟹ wf {(x,y). P x y ∧ g x y}"
  apply(insert wf_measure[of f])
  apply(simp only: measure_def inv_image_def less_than_def less_eq)
  apply(erule wf_subset)
  apply auto
  done

lemma lexord_on_finite_set_is_wf:
  assumes
    P_finite: "⋀U. P U ⟶ U ∈ A" and
    finite: "finite A" and
    wf: "wf R" and
    trans: "trans R"
  shows "wf {(T, S). (P S ∧ P T) ∧ (T, S) ∈ lexord R}"
proof (rule wfP_if_measure2)
  fix T S
  assume P: "P S ∧ P T" and
  s_le_t: "(T, S) ∈ lexord R"
  let ?f = "λS. {U. (U, S) ∈ lexord R ∧ P U ∧ P S}"
  have "?f T ⊆ ?f S"
     using s_le_t P lexord_trans trans by auto
  moreover have "T ∈ ?f S"
    using s_le_t P by auto
  moreover have "T ∉ ?f T"
    using s_le_t by (auto simp add: lexord_irreflexive local.wf)
  ultimately have "{U. (U, T) ∈ lexord R ∧ P U ∧ P T} ⊂ {U. (U, S) ∈ lexord R ∧ P U ∧ P S}"
    by auto
  moreover have "finite {U. (U, S) ∈ lexord R ∧ P U ∧ P S}"
    using finite by (metis (no_types, lifting) P_finite finite_subset mem_Collect_eq subsetI)
  ultimately show "card (?f T) < card (?f S)" by (simp add: psubset_card_mono)
qed


lemma wf_fst_wf_pair:
  assumes "wf {(M', M). R M' M} "
  shows "wf {((M', N'), (M, N)). R M' M}"
proof -
  have "wf ({(M', M). R M' M} <*lex*> {})"
    using assms by auto
  then show ?thesis
    by (rule wf_subset) auto
qed

lemma wf_snd_wf_pair:
  assumes "wf {(M', M). R M' M} "
  shows "wf {((M', N'), (M, N)). R N' N}"
proof -
  have wf: "wf {((M', N'), (M, N)). R M' M}"
    using assms wf_fst_wf_pair by auto
  then have wf: "⋀P. (∀x. (∀y. (y, x) ∈ {((M', N'), M, N). R M' M} ⟶ P y) ⟶ P x) ⟹ All P"
    unfolding wf_def by auto
  show ?thesis
    unfolding wf_def
    proof (intro allI impI)
      fix P :: "'c × 'a ⇒ bool" and x :: "'c × 'a"
      assume H: "∀x. (∀y. (y, x) ∈ {((M', N'), M, y). R N' y} ⟶ P y) ⟶ P x"
      obtain a b where x: "x = (a, b)" by (cases x)
      have P: "P x = (P ∘ (λ(a, b). (b, a))) (b, a)"
        unfolding x by auto
      show "P x"
        using wf[of "P o (λ(a, b). (b, a))"] apply rule
          using H apply simp
        unfolding P by blast
    qed
qed

lemma wf_if_measure_f_notation2:
  assumes "wf r"
  shows "wf {(b, h a)|b a. (f b, f (h a)) ∈ r}"
  apply (rule wf_subset)
  using wf_if_measure_f[OF assms, of f] by auto

lemma wf_wf_if_measure'_notation2:
assumes "wf r" and H: "(⋀x y. P x ⟹ g x y ⟹ (f y, f (h x)) ∈ r)"
shows "wf {(y,h x)| y x. P x ∧ g x y}"
proof -
  have "wf {(b, h a)|b a. (f b, f (h a)) ∈ r}" using assms(1) wf_if_measure_f_notation2 by auto
  then have "wf {(b, h a)|b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r}"
    using wf_subset[of _ "{(b, h a)| b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r}"] by auto
  moreover have "{(b, h a)|b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r}
    ⊆ {(b, h a)|b a. (f b, f (h a)) ∈ r}" by auto
  moreover have "{(b, h a)|b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r} = {(b, h a)|b a. P a ∧ g a b}"
    using H by auto
  ultimately show ?thesis using wf_subset by simp
qed

end