Theory Partial_Order_Reduction.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 "FI" 50)
    where "u FI v   w. u @- w = v"

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

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

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

  lemma prefix_fininf_absorb:
    assumes "u FI 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 FI 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 FI w" "v FI 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 FI v @- w"
    obtains (absorb) "u  v" | (extend) z where "u = v @ z" "z FI 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 FI w" by rule
    qed
  qed

  lemma prefix_fin_prefix_fininf_trans[trans, intro]: "u  v  v FI w  u FI 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 FI 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 FI 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 x0" " 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 x0" " 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 x0 x'"
    have [simp]: "Q 0 = x0" " 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 x0" " 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 x0" " 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 x0 x'"
    have [simp]: "Q 0 = x0" " 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 u0 v0" " 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 (u0, v0)" 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