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 the theorem @{thm [source] 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 the theorem @{thm [source] rtranclp_idemp}›
lemma trancl_idemp: ‹(r⇧+)⇧+ = r⇧+›
  by simp

lemmas tranclp_idemp[simp] = trancl_idemp[to_pred]

text ‹This theorem already exists as theroem @{thm [source] 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 theorem @{thm [source] 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; fail)[1]
    using IH z by (fastforce intro: rtranclp.rtrancl_into_rtrancl)
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›

paragraph ‹Definition›

text ‹We define here predicates to define properties after all possible transitions.›

abbreviation (input) no_step :: "('a ⇒ 'b ⇒ bool) ⇒ 'a ⇒ bool" where
"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' ∧ no_step transf S')"

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

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


paragraph ‹Some Properties›

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 (auto simp: full1_def)

lemma not_full_rtranclp_relation: "¬full R⇧*⇧* a b"
  by (auto simp: full_def)


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 tranclp_full1_full1:
  ‹(full1 R)⇧+⇧+ a b ⟷ full1 R a b›
  by (metis (mono_tags) full1_def predicate2I tranclp.r_into_trancl tranclp_idemp
      tranclp_mono_explicit tranclp_unfold_end)

lemma rtranclp_full1_eq_or_full1:
  ‹(full1 R)⇧*⇧* a b ⟷ (a = b ∨ full1 R a b)›
  unfolding rtranclp_unfold tranclp_full1_full1 by simp

lemma no_step_full_iff_eq:
  ‹no_step R S ⟹ full R S T ⟷ S = T›
  unfolding full_def
  by (meson rtranclp.rtrancl_refl rtranclpD tranclpD)


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
  define F where ‹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)›
    unfolding 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: theorems
  @{thm [source] wf_iff_no_infinite_down_chain} and @{thm [source] 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 less_than)›
  by (auto simp: wf_less)

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

lemma power_ex_decomp:
  assumes ‹(R^^n) S T›
  shows
    ‹∃f. f 0 = S ∧ f n = T ∧ (∀i. i < n ⟶ R (f i) (f (Suc i)))›
  using assms
proof (induction n arbitrary: T)
  case 0
  then show ‹?case› by auto
next
  case (Suc n) note IH = this(1) and R = this(2)
  from R obtain T' where
    ST: ‹(R^^n) S T'› and
    T'T: ‹R T' T›
    by auto
  obtain f where
    [simp]: ‹f 0 = S› and
    [simp]: ‹f n = T'› and
    H: ‹⋀i. i < n ⟹ R (f i) (f (Suc i))›
    using IH[OF ST] by fast
  let ?f = ‹f(Suc n := T)›
  show ?case
    by (rule exI[of _ ?f])
      (use H ST T'T in auto)
qed


text ‹The following lemma gives a bound on the maximal number of transitions of a sequence that is well-founded
  under the lexicographic ordering \<^term>‹lexn› on natural numbers.
›
lemma lexn_number_of_transition:
  assumes
    le: ‹⋀i. i < n ⟹ ((f (Suc i)), (f i)) ∈ lexn less_than m› and
    upper: ‹⋀i j. i ≤ n ⟹ j < m ⟹ (f i) ! j ∈ {0..<k}› and
    ‹finite A› and
    k: ‹k > 1›
  shows ‹n < k ^ Suc m›
proof -
  define r where
    ‹r x = zip x (map (λi. k ^ (length x -i)) [0..<length x])› for x :: ‹nat list›

  define s where
    ‹s x = foldr (λa b. a + b) (map (λ(a, b). a * b) x) 0› for x :: ‹(nat × nat) list›

  have [simp]: ‹r [] = []› ‹s [] = 0›
    by (auto simp: r_def s_def)

  have upt': ‹m > 0 ⟹ [0..< m] = 0 # map Suc [0..< m - 1]› for m
    by (auto simp: map_Suc_upt upt_conv_Cons)

  have upt'': ‹m > 0 ⟹ [0..< m] = [0..< m - 1] @ [m-1]› for m
    by (cases m) (auto simp: )

  have Cons: ‹r (x # xs) = (x, k^(Suc (length xs))) # (r xs)› for x xs
   unfolding r_def
   apply (subst upt')
   apply (clarsimp simp add: upt'' comp_def nth_append Suc_diff_le simp flip: zip_map2)
   apply (clarsimp simp add: upt'' comp_def nth_append Suc_diff_le simp flip: zip_map2)
   done

  have [simp]: ‹s (ab # xs) = fst ab * snd ab + s xs› for ab xs
    unfolding s_def by (cases ab) auto

  have le2: ‹(∀a ∈ set b. a < k) ⟹ (k ^ (Suc (length b))) > s ((r b))› for b
    apply (induction b arbitrary: f)
    using k apply (auto simp: Cons)
    apply (rule order.strict_trans1)
    apply (rule_tac j = ‹(k - 1) * k *k ^ length b› in Nat.add_le_mono1)
    subgoal for a b
      by auto
    apply (rule order.strict_trans2)
    apply (rule_tac b = ‹(k - 1) * k * k ^ length b› and d = ‹(k * k ^ length b)› in add_le_less_mono)
    apply (auto simp: mult.assoc comm_semiring_1_class.semiring_normalization_rules(2))
    done

  have ‹s (r (f (Suc i))) < s (r (f i))› if ‹i < n› for i
  proof -
    have i_n: ‹Suc i ≤ n› ‹i ≤ n›
      using that by auto
    have length: ‹length (f i) = m›  ‹length (f (Suc i)) = m›
     using le[OF that] by (auto dest: lexn_length)
    define xs and ys where ‹xs = f i› and ‹ys = f (Suc i)›

    show ?thesis
      using le[OF that] upper[OF i_n(2)] upper[OF i_n(1)] length Cons
      unfolding xs_def[symmetric] ys_def[symmetric]
    proof (induction m arbitrary: xs ys)
      case 0 then show ?case by auto
    next
      case (Suc m) note IH = this(1) and H = this(2) and p = this(3-)
      have IH: ‹(tl ys, tl xs) ∈ lexn less_than m ⟹ s (r (tl ys)) < s (r (tl xs))›
        apply (rule IH)
        subgoal by auto
        subgoal for i using p(1)[of ‹Suc i›] p by (cases xs; auto)
        subgoal for i using p(2)[of ‹Suc i›] p by (cases ys; auto)
        subgoal using p by (cases xs) auto
        subgoal using p by auto
        subgoal using p by auto
        done
     have ‹s (r (tl ys)) < k ^ (Suc (length (tl ys)))›
       apply (rule le2)
       unfolding all_set_conv_all_nth
       using p by (simp add: nth_tl)
     then have ‹ab * (k * k ^ length (tl ys)) + s (r (tl ys)) <
               ab * (k * k ^ length (tl ys)) + (k * k ^ length (tl ys))› for ab
       by auto
     also have ‹… ab  ≤ (ab + 1) * (k * k ^ length (tl ys))› for ab
       by auto
     finally have less: ‹ab < ac ⟹ ab * (k * k ^ length (tl ys)) + s (r (tl ys)) <
                                    ac * (k * k ^ length (tl ys))› for ab ac
     proof -
       assume a1: "⋀ab. ab * (k * k ^ length (tl ys)) + s (r (tl ys)) <
                   (ab + 1) * (k * k ^ length (tl ys))"
       assume "ab < ac"
       then have "¬ ac * (k * k ^ length (tl ys)) < (ab + 1) * (k * k ^ length (tl ys))"
         by (metis (no_types) One_nat_def Suc_leI add.right_neutral add_Suc_right
            mult_less_cancel2 not_less)
       then show ?thesis
         using a1 by (meson le_less_trans not_less)
     qed

    have ‹ab < ac ⟹
        ab * (k * k ^ length (tl ys)) + s (r (tl ys))
        < ac * (k * k ^ length (tl xs)) + s (r (tl xs))› for ab ac
        using less[of ab ac] p by auto
    then show ?case
         apply (cases xs; cases ys)
        using IH H p(3-5) by auto
    qed
  qed
  then have ‹i≤n ⟹ s (r (f i)) + i ≤ s (r (f 0))› for i
    apply (induction i)
    subgoal by auto
    subgoal premises p for i
       using p(3)[of ‹i-1›] p(1,2)
      apply auto
      by (meson Nat.le_diff_conv2 Suc_leI Suc_le_lessD add_leD2 less_diff_conv less_le_trans p(3))
    done
  from this[of n] show ‹n < k ^ Suc m›
    using le2[of ‹f 0›] upper[of 0] k
    using le[of 0] apply (cases ‹n = 0›)
    by (auto dest!: lexn_length simp: all_set_conv_all_nth eq_commute[of _ m])
qed

end