Theory Word_Prefixes

section ‹Finite Prefixes of Infinite Sequences›

theory Word_Prefixes
imports
  List_Prefixes
  "../Extensions/List_Extensions"
  Transition_Systems_and_Automata.Sequence
begin

  definition prefix_fininf :: "'a list ⇒ 'a stream ⇒ bool" (infix "≤⇩F⇩I" 50)
    where "u ≤⇩F⇩I v ≡ ∃ w. u @- w = v"

  lemma prefix_fininfI[intro]:
    assumes "u @- w = v"
    shows "u ≤⇩F⇩I v"
    using assms unfolding prefix_fininf_def by auto
  lemma prefix_fininfE[elim]:
    assumes "u ≤⇩F⇩I v"
    obtains w
    where "v = u @- w"
    using assms unfolding prefix_fininf_def by auto

  lemma prefix_fininfI_empty[intro!]: "[] ≤⇩F⇩I w" by force
  lemma prefix_fininfI_item[intro!]:
    assumes "a = b" "u ≤⇩F⇩I v"
    shows "a # u ≤⇩F⇩I b ## v"
    using assms by force
  lemma prefix_fininfE_item[elim!]:
    assumes "a # u ≤⇩F⇩I b ## v"
    obtains "a = b" "u ≤⇩F⇩I v"
    using assms by force

  lemma prefix_fininf_item[simp]: "a # u ≤⇩F⇩I a ## v ⟷ u ≤⇩F⇩I v" by force
  lemma prefix_fininf_list[simp]: "w @ u ≤⇩F⇩I w @- v ⟷ u ≤⇩F⇩I v" by (induct w, auto)
  lemma prefix_fininf_conc[intro]: "u ≤⇩F⇩I u @- v" by auto
  lemma prefix_fininf_prefix[intro]: "stake k w ≤⇩F⇩I w" using stake_sdrop by blast
  lemma prefix_fininf_set_range[dest]: "u ≤⇩F⇩I v ⟹ set u ⊆ sset v" by auto

  lemma prefix_fininf_absorb:
    assumes "u ≤⇩F⇩I v @- w" "length u ≤ length v"
    shows "u ≤ v"
  proof -
    obtain x where 1: "u @- x = v @- w" using assms(1) by auto
    have "u ≤ u @ stake (length v - length u) x" by rule
    also have "… = stake (length v) (u @- x)" using assms(2) by (simp add: stake_shift)
    also have "… = stake (length v) (v @- w)" unfolding 1 by rule
    also have "… = v" using eq_shift by blast
    finally show ?thesis by this
  qed
  lemma prefix_fininf_extend:
    assumes "u ≤⇩F⇩I v @- w" "length v ≤ length u"
    shows "v ≤ u"
  proof -
    obtain x where 1: "u @- x = v @- w" using assms(1) by auto
    have "v ≤ v @ stake (length u - length v) w" by rule
    also have "… = stake (length u) (v @- w)" using assms(2) by (simp add: stake_shift)
    also have "… = stake (length u) (u @- x)" unfolding 1 by rule
    also have "… = u" using eq_shift by blast
    finally show ?thesis by this
  qed
  lemma prefix_fininf_length:
    assumes "u ≤⇩F⇩I w" "v ≤⇩F⇩I w" "length u ≤ length v"
    shows "u ≤ v"
  proof -
    obtain u' v' where 1: "w = u @- u'" "w = v @- v'" using assms(1, 2) by blast+
    have "u = stake (length u) (u @- u')" using shift_eq by blast
    also have "… = stake (length u) w" unfolding 1(1) by rule
    also have "… = stake (length u) (v @- v')" unfolding 1(2) by rule
    also have "… = take (length u) v" using assms by (simp add: min.absorb2 stake_append)
    also have "… ≤ v" by rule
    finally show ?thesis by this
  qed

  lemma prefix_fininf_append:
    assumes "u ≤⇩F⇩I v @- w"
    obtains (absorb) "u ≤ v" | (extend) z where "u = v @ z" "z ≤⇩F⇩I w"
  proof (cases "length u" "length v" rule: le_cases)
    case le
    obtain x where 1: "u @- x = v @- w" using assms(1) by auto
    show ?thesis
    proof (rule absorb)
      have "u ≤ u @ stake (length v - length u) x" by rule
      also have "… = stake (length v) (u @- x)" using le by (simp add: stake_shift)
      also have "… = stake (length v) (v @- w)" unfolding 1 by rule
      also have "… = v" using eq_shift by blast
      finally show "u ≤ v" by this
    qed
  next
    case ge
    obtain x where 1: "u @- x = v @- w" using assms(1) by auto
    show ?thesis
    proof (rule extend)
      have "u = stake (length u) (u @- x)" using shift_eq by auto
      also have "… = stake (length u) (v @- w)" unfolding 1 by rule
      also have "… = v @ stake (length u - length v) w" using ge by (simp add: stake_shift)
      finally show "u = v @ stake (length u - length v) w" by this
      show "stake (length u - length v) w ≤⇩F⇩I w" by rule
    qed
  qed

  lemma prefix_fin_prefix_fininf_trans[trans, intro]: "u ≤ v ⟹ v ≤⇩F⇩I w ⟹ u ≤⇩F⇩I w"
    by (metis Prefix_Order.prefixE prefix_fininf_def shift_append)

  lemma prefix_finE_nth:
    assumes "u ≤ v" "i < length u"
    shows "u ! i = v ! i"
  proof -
    obtain w where 1: "v = u @ w" using assms(1) by auto
    show ?thesis unfolding 1 using assms(2) by (simp add: nth_append)
  qed
  lemma prefix_fininfI_nth:
    assumes "⋀ i. i < length u ⟹ u ! i = w !! i"
    shows "u ≤⇩F⇩I w"
  proof (rule prefix_fininfI)
    show "u @- sdrop (length u) w = w" by (simp add: assms list_eq_iff_nth_eq shift_eq)
  qed

  definition chain :: "(nat ⇒ 'a list) ⇒ bool"
    where "chain w ≡ mono w ∧ (∀ k. ∃ l. k < length (w l))"
  definition limit :: "(nat ⇒ 'a list) ⇒ 'a stream"
    where "limit w ≡ smap (λ k. w (SOME l. k < length (w l)) ! k) nats"

  lemma chainI[intro?]:
    assumes "mono w"
    assumes "⋀ k. ∃ l. k < length (w l)"
    shows "chain w"
    using assms unfolding chain_def by auto
  lemma chainD_mono[dest?]:
    assumes "chain w"
    shows "mono w"
    using assms unfolding chain_def by auto
  lemma chainE_length[elim?]:
    assumes "chain w"
    obtains l
    where "k < length (w l)"
    using assms unfolding chain_def by auto

  lemma chain_prefix_limit:
    assumes "chain w"
    shows "w k ≤⇩F⇩I limit w"
  proof (rule prefix_fininfI_nth)
    fix i
    assume 1: "i < length (w k)"
    have 2: "mono w" "⋀ k. ∃ l. k < length (w l)" using chainD_mono chainE_length assms by blast+
    have 3: "i < length (w (SOME l. i < length (w l)))" using someI_ex 2(2) by this
    show "w k ! i = limit w !! i"
    proof (cases "k" "SOME l. i < length (w l)" rule: le_cases)
      case (le)
      have 4: "w k ≤ w (SOME l. i < length (w l))" using monoD 2(1) le by this
      show ?thesis unfolding limit_def using prefix_finE_nth 4 1 by auto
    next
      case (ge)
      have 4: "w (SOME l. i < length (w l)) ≤ w k" using monoD 2(1) ge by this
      show ?thesis unfolding limit_def using prefix_finE_nth 4 3 by auto
    qed
  qed

  lemma chain_construct_1:
    assumes "P 0 x⇩0" "⋀ k x. P k x ⟹ ∃ x'. P (Suc k) x' ∧ f x ≤ f x'"
    assumes "⋀ k x. P k x ⟹ k ≤ length (f x)"
    obtains Q
    where "⋀ k. P k (Q k)" "chain (f ∘ Q)"
  proof -
    obtain x' where 1:
      "P 0 x⇩0" "⋀ k x. P k x ⟹ P (Suc k) (x' k x) ∧ f x ≤ f (x' k x)"
      using assms(1, 2) by metis
    define Q where "Q ≡ rec_nat x⇩0 x'"
    have [simp]: "Q 0 = x⇩0" "⋀ k. Q (Suc k) = x' k (Q k)" unfolding Q_def by simp+
    have 2: "⋀ k. P k (Q k)"
    proof -
      fix k
      show "P k (Q k)" using 1 by (induct k, auto)
    qed
    show ?thesis
    proof (intro that chainI monoI, unfold comp_apply)
      fix k
      show "P k (Q k)" using 2 by this
    next
      fix x y :: nat
      assume "x ≤ y"
      thus "f (Q x) ≤ f (Q y)"
      proof (induct "y - x" arbitrary: x y)
        case 0
        show ?case using 0 by simp
      next
        case (Suc k)
        have "f (Q x) ≤ f (Q (Suc x))" using 1(2) 2 by auto
        also have "… ≤ f (Q y)" using Suc(2) by (intro Suc(1), auto)
        finally show ?case by this
      qed
    next
      fix k
      have 3: "P (Suc k) (Q (Suc k))" using 2 by this
      have 4: "Suc k ≤ length (f (Q (Suc k)))" using assms(3) 3 by this
      have 5: "k < length (f (Q (Suc k)))" using 4 by auto
      show "∃ l. k < length (f (Q l))" using 5 by blast
    qed
  qed
  lemma chain_construct_2:
    assumes "P 0 x⇩0" "⋀ k x. P k x ⟹ ∃ x'. P (Suc k) x' ∧ f x ≤ f x' ∧ g x ≤ g x'"
    assumes "⋀ k x. P k x ⟹ k ≤ length (f x)" "⋀ k x. P k x ⟹ k ≤ length (g x)"
    obtains Q
    where "⋀ k. P k (Q k)" "chain (f ∘ Q)" "chain (g ∘ Q)"
  proof -
    obtain x' where 1:
      "P 0 x⇩0" "⋀ k x. P k x ⟹ P (Suc k) (x' k x) ∧ f x ≤ f (x' k x) ∧ g x ≤ g (x' k x)"
      using assms(1, 2) by metis
    define Q where "Q ≡ rec_nat x⇩0 x'"
    have [simp]: "Q 0 = x⇩0" "⋀ k. Q (Suc k) = x' k (Q k)" unfolding Q_def by simp+
    have 2: "⋀ k. P k (Q k)"
    proof -
      fix k
      show "P k (Q k)" using 1 by (induct k, auto)
    qed
    show ?thesis
    proof (intro that chainI monoI, unfold comp_apply)
      fix k
      show "P k (Q k)" using 2 by this
    next
      fix x y :: nat
      assume "x ≤ y"
      thus "f (Q x) ≤ f (Q y)"
      proof (induct "y - x" arbitrary: x y)
        case 0
        show ?case using 0 by simp
      next
        case (Suc k)
        have "f (Q x) ≤ f (Q (Suc x))" using 1(2) 2 by auto
        also have "… ≤ f (Q y)" using Suc(2) by (intro Suc(1), auto)
        finally show ?case by this
      qed
    next
      fix k
      have 3: "P (Suc k) (Q (Suc k))" using 2 by this
      have 4: "Suc k ≤ length (f (Q (Suc k)))" using assms(3) 3 by this
      have 5: "k < length (f (Q (Suc k)))" using 4 by auto
      show "∃ l. k < length (f (Q l))" using 5 by blast
    next
      fix x y :: nat
      assume "x ≤ y"
      thus "g (Q x) ≤ g (Q y)"
      proof (induct "y - x" arbitrary: x y)
        case 0
        show ?case using 0 by simp
      next
        case (Suc k)
        have "g (Q x) ≤ g (Q (Suc x))" using 1(2) 2 by auto
        also have "… ≤ g (Q y)" using Suc(2) by (intro Suc(1), auto)
        finally show ?case by this
      qed
    next
      fix k
      have 3: "P (Suc k) (Q (Suc k))" using 2 by this
      have 4: "Suc k ≤ length (g (Q (Suc k)))" using assms(4) 3 by this
      have 5: "k < length (g (Q (Suc k)))" using 4 by auto
      show "∃ l. k < length (g (Q l))" using 5 by blast
    qed
  qed
  lemma chain_construct_2':
    assumes "P 0 u⇩0 v⇩0" "⋀ k u v. P k u v ⟹ ∃ u' v'. P (Suc k) u' v' ∧ u ≤ u' ∧ v ≤ v'"
    assumes "⋀ k u v. P k u v ⟹ k ≤ length u" "⋀ k u v. P k u v ⟹ k ≤ length v"
    obtains u v
    where "⋀ k. P k (u k) (v k)" "chain u" "chain v"
  proof -
    obtain Q where 1: "⋀ k. (case_prod ∘ P) k (Q k)" "chain (fst ∘ Q)" "chain (snd ∘ Q)"
    proof (rule chain_construct_2)
      show "∃ x'. (case_prod ∘ P) (Suc k) x' ∧ fst x ≤ fst x' ∧ snd x ≤ snd x'"
        if "(case_prod ∘ P) k x" for k x using assms that by auto
      show "(case_prod ∘ P) 0 (u⇩0, v⇩0)" using assms by auto
      show "k ≤ length (fst x)" if "(case_prod ∘ P) k x" for k x using assms that by auto
      show "k ≤ length (snd x)" if "(case_prod ∘ P) k x" for k x using assms that by auto
    qed rule
    show ?thesis
    proof
      show "P k ((fst ∘ Q) k) ((snd ∘ Q) k)" for k using 1(1) by (auto simp: prod.case_eq_if)
      show "chain (fst ∘ Q)" "chain (snd ∘ Q)" using 1(2, 3) by this
    qed
  qed

end