Theory Trace

(*<*)
theory Trace
  imports "HOL-Library.Stream"
begin
(*>*)

section ‹Traces and trace prefixes›

subsection ‹Infinite traces›

coinductive ssorted :: "'a :: linorder stream ⇒ bool" where
  "shd s ≤ shd (stl s) ⟹ ssorted (stl s) ⟹ ssorted s"

lemma ssorted_siterate[simp]: "(⋀n. n ≤ f n) ⟹ ssorted (siterate f n)"
  by (coinduction arbitrary: n) auto

lemma ssortedD: "ssorted s ⟹ s !! i ≤ stl s !! i"
  by (induct i arbitrary: s) (auto elim: ssorted.cases)

lemma ssorted_sdrop: "ssorted s ⟹ ssorted (sdrop i s)"
  by (coinduction arbitrary: i s) (auto elim: ssorted.cases ssortedD)

lemma ssorted_monoD: "ssorted s ⟹ i ≤ j ⟹ s !! i ≤ s !! j"
proof (induct "j - i" arbitrary: j)
  case (Suc x)
  from Suc(1)[of "j - 1"] Suc(2-4) ssortedD[of s "j - 1"]
    show ?case by (cases j) (auto simp: le_Suc_eq Suc_diff_le)
qed simp

lemma sorted_stake: "ssorted s ⟹ sorted (stake i s)"
  by (induct i arbitrary: s)
    (auto elim: ssorted.cases simp: in_set_conv_nth
      intro!: ssorted_monoD[of _ 0, simplified, THEN order_trans, OF _ ssortedD])

lemma ssorted_monoI: "∀i j. i ≤ j ⟶ s !! i ≤ s !! j ⟹ ssorted s"
  by (coinduction arbitrary: s)
    (auto dest: spec2[of _ "Suc _" "Suc _"] spec2[of _ 0 "Suc 0"])

lemma ssorted_iff_mono: "ssorted s ⟷ (∀i j. i ≤ j ⟶ s !! i ≤ s !! j)"
  using ssorted_monoI ssorted_monoD by metis

lemma ssorted_iff_le_Suc: "ssorted s ⟷ (∀i. s !! i ≤ s !! Suc i)"
  using mono_iff_le_Suc[of "snth s"] by (simp add: mono_def ssorted_iff_mono)

definition "sincreasing s = (∀x. ∃i. x < s !! i)"

lemma sincreasingI: "(⋀x. ∃i. x < s !! i) ⟹ sincreasing s"
  by (simp add: sincreasing_def)

lemma sincreasing_grD:
  fixes x :: "'a :: semilattice_sup"
  assumes "sincreasing s"
  shows "∃j>i. x < s !! j"
proof -
  let ?A = "insert x {s !! n | n. n ≤ i}"
  from assms obtain j where *: "Sup_fin ?A < s !! j"
    by (auto simp: sincreasing_def)
  then have "x < s !! j"
    by (rule order.strict_trans1[rotated]) (auto intro: Sup_fin.coboundedI)
  moreover have "i < j"
  proof (rule ccontr)
    assume "¬ i < j"
    then have "s !! j ∈ ?A" by (auto simp: not_less)
    then have "s !! j ≤ Sup_fin ?A"
      by (auto intro: Sup_fin.coboundedI)
    with * show False by simp
  qed
  ultimately show ?thesis by blast
qed

lemma sincreasing_siterate_nat[simp]:
  fixes n :: nat
  assumes "(⋀n. n < f n)"
  shows "sincreasing (siterate f n)"
unfolding sincreasing_def proof
  fix x
  show "∃i. x < siterate f n !! i"
  proof (induction x)
    case 0
    have "0 < siterate f n !! 1"
      using order.strict_trans1[OF le0 assms] by simp
    then show ?case ..
  next
    case (Suc x)
    then obtain i where "x < siterate f n !! i" ..
    then have "Suc x < siterate f n !! Suc i"
      using order.strict_trans1[OF _ assms] by (simp del: snth.simps)
    then show ?case ..
  qed
qed

lemma sincreasing_stl: "sincreasing s ⟹ sincreasing (stl s)" for s :: "'a :: semilattice_sup stream"
  by (auto 0 4 simp: gr0_conv_Suc intro!: sincreasingI dest: sincreasing_grD[of s 0])

typedef 'a trace = "{s :: ('a set × nat) stream. ssorted (smap snd s) ∧ sincreasing (smap snd s)}"
  by (intro exI[of _ "smap (λi. ({}, i)) nats"])
    (auto simp: stream.map_comp stream.map_ident cong: stream.map_cong)

setup_lifting type_definition_trace

lift_definition Γ :: "'a trace ⇒ nat ⇒ 'a set" is
  "λs i. fst (s !! i)" .
lift_definition τ :: "'a trace ⇒ nat ⇒ nat" is
  "λs i. snd (s !! i)" .

lemma stream_eq_iff: "s = s' ⟷ (∀n. s !! n = s' !! n)"
  by (metis stream.map_cong0 stream_smap_nats)

lemma trace_eqI: "(⋀i. Γ σ i = Γ σ' i) ⟹ (⋀i. τ σ i = τ σ' i) ⟹ σ = σ'"
  by transfer (auto simp: stream_eq_iff intro!: prod_eqI)

lemma τ_mono[simp]: "i ≤ j ⟹ τ s i ≤ τ s j"
  by transfer (auto simp: ssorted_iff_mono)

lemma ex_le_τ: "∃j≥i. x ≤ τ s j"
  by (transfer fixing: i x) (auto dest!: sincreasing_grD[of _ i x] less_imp_le)

lemma le_τ_less: "τ σ i ≤ τ σ j ⟹ j < i ⟹ τ σ i = τ σ j"
  by (simp add: antisym)

lemma less_τD: "τ σ i < τ σ j ⟹ i < j"
  by (meson τ_mono less_le_not_le not_le_imp_less)

abbreviation "Δ s i ≡ τ s i - τ s (i - 1)"

lift_definition map_Γ :: "('a set ⇒ 'b set) ⇒ 'a trace ⇒ 'b trace" is
  "λf s. smap (λ(x, i). (f x, i)) s"
  by (auto simp: stream.map_comp prod.case_eq_if cong: stream.map_cong)

lemma Γ_map_Γ[simp]: "Γ (map_Γ f s) i = f (Γ s i)"
  by transfer (simp add: prod.case_eq_if)

lemma τ_map_Γ[simp]: "τ (map_Γ f s) i = τ s i"
  by transfer (simp add: prod.case_eq_if)

lemma map_Γ_id[simp]: "map_Γ id s = s"
  by transfer (simp add: stream.map_id)

lemma map_Γ_comp: "map_Γ g (map_Γ f s) = map_Γ (g ∘ f) s"
  by transfer (simp add: stream.map_comp comp_def prod.case_eq_if case_prod_beta')

lemma map_Γ_cong: "σ⇩1 = σ⇩2 ⟹ (⋀x. f⇩1 x = f⇩2 x) ⟹ map_Γ f⇩1 σ⇩1 = map_Γ f⇩2 σ⇩2"
  by transfer (auto intro!: stream.map_cong)


subsection ‹Finite trace prefixes›

typedef 'a prefix = "{p :: ('a set × nat) list. sorted (map snd p)}"
  by (auto intro!: exI[of _ "[]"])

setup_lifting type_definition_prefix

lift_definition pmap_Γ :: "('a set ⇒ 'b set) ⇒ 'a prefix ⇒ 'b prefix" is
  "λf. map (λ(x, i). (f x, i))"
  by (simp add: split_beta comp_def)

lift_definition last_ts :: "'a prefix ⇒ nat" is
  "λp. (case p of [] ⇒ 0 | _ ⇒ snd (last p))" .

lift_definition first_ts :: "nat ⇒ 'a prefix ⇒ nat" is
  "λn p. (case p of [] ⇒ n | _ ⇒ snd (hd p))" .

lift_definition pnil :: "'a prefix" is "[]" by simp

lift_definition plen :: "'a prefix ⇒ nat" is "length" .

lift_definition psnoc :: "'a prefix ⇒ 'a set × nat ⇒ 'a prefix" is
  "λp x. if (case p of [] ⇒ 0 | _ ⇒ snd (last p)) ≤ snd x then p @ [x] else []"
proof (goal_cases sorted_psnoc)
  case (sorted_psnoc p x)
  then show ?case
    by (induction p) (auto split: if_splits list.splits)
qed

instantiation prefix :: (type) order begin

lift_definition less_eq_prefix :: "'a prefix ⇒ 'a prefix ⇒ bool" is
  "λp q. ∃r. q = p @ r" .

definition less_prefix :: "'a prefix ⇒ 'a prefix ⇒ bool" where
  "less_prefix x y = (x ≤ y ∧ ¬ y ≤ x)"

instance
proof (standard, goal_cases less refl trans antisym)
  case (less x y)
  then show ?case unfolding less_prefix_def ..
next
  case (refl x)
  then show ?case by transfer auto
next
  case (trans x y z)
  then show ?case by transfer auto
next
  case (antisym x y)
  then show ?case by transfer auto
qed

end

lemma psnoc_inject[simp]:
  "last_ts p ≤ snd x ⟹ last_ts q ≤ snd y ⟹ psnoc p x = psnoc q y ⟷ (p = q ∧ x = y)"
  by transfer auto

lift_definition prefix_of :: "'a prefix ⇒ 'a trace ⇒ bool" is "λp s. stake (length p) s = p" .

lemma prefix_of_pnil[simp]: "prefix_of pnil σ"
  by transfer auto

lemma plen_pnil[simp]: "plen pnil = 0"
  by transfer auto

lemma prefix_of_pmap_Γ[simp]: "prefix_of π σ ⟹ prefix_of (pmap_Γ f π) (map_Γ f σ)"
  by transfer auto

lemma plen_mono: "π ≤ π' ⟹ plen π ≤ plen π'"
  by transfer auto

lemma prefix_of_psnocE: "prefix_of (psnoc p x) s ⟹ last_ts p ≤ snd x ⟹
  (prefix_of p s ⟹ Γ s (plen p) = fst x ⟹ τ s (plen p) = snd x ⟹ P) ⟹ P"
  by transfer (simp del: stake.simps add: stake_Suc)

lemma le_pnil[simp]: "pnil ≤ π"
  by transfer auto

lift_definition take_prefix :: "nat ⇒ 'a trace ⇒ 'a prefix" is stake
  by (auto dest: sorted_stake)

lemma plen_take_prefix[simp]: "plen (take_prefix i σ) = i"
  by transfer auto

lemma plen_psnoc[simp]: "last_ts π ≤ snd x ⟹ plen (psnoc π x) = plen π + 1"
  by transfer auto

lemma prefix_of_take_prefix[simp]: "prefix_of (take_prefix i σ) σ"
  by transfer auto

lift_definition pdrop :: "nat ⇒ 'a prefix ⇒ 'a prefix" is drop
  by (auto simp: drop_map[symmetric] sorted_wrt_drop)

lemma pdrop_0[simp]: "pdrop 0 π = π"
  by transfer auto

lemma prefix_of_antimono: "π ≤ π' ⟹ prefix_of π' s ⟹ prefix_of π s"
  by transfer (auto simp del: stake_add simp add: stake_add[symmetric])

lemma prefix_of_imp_linear: "prefix_of π σ ⟹ prefix_of π' σ ⟹ π ≤ π' ∨ π' ≤ π"
proof transfer
  fix π π' and σ :: "('a set × nat) stream"
  assume assms: "stake (length π) σ = π" "stake (length π') σ = π'"
  show "(∃r. π' = π @ r) ∨ (∃r. π = π' @ r)"
  proof (cases "length π" "length π'" rule: le_cases)
    case le
    then have "π' = take (length π) π' @ drop (length π) π'"
      by simp
    moreover have "take (length π) π' = π"
      using assms le by (metis min.absorb1 take_stake)
    ultimately show ?thesis by auto
  next
    case ge
    then have "π = take (length π') π @ drop (length π') π"
      by simp
    moreover have "take (length π') π = π'"
      using assms ge by (metis min.absorb1 take_stake)
    ultimately show ?thesis by auto
  qed
qed

lemma ex_prefix_of: "∃s. prefix_of p s"
proof (transfer, intro bexI CollectI conjI)
  fix p :: "('a set × nat) list"
  assume *: "sorted (map snd p)"
  let ?σ = "p @- smap (Pair undefined) (fromN (snd (last p)))"
  show "stake (length p) ?σ = p" by (simp add: stake_shift)
  have le_last: "snd (p ! i) ≤ snd (last p)" if "i < length p" for i
    using sorted_nth_mono[OF *, of i "length p - 1"] that
    by (cases p) (auto simp: last_conv_nth nth_Cons')
  with * show "ssorted (smap snd ?σ)"
    by (force simp: ssorted_iff_mono sorted_iff_nth_mono shift_snth)
  show "sincreasing (smap snd ?σ)"
  proof (rule sincreasingI)
    fix x
    have "x < smap snd ?σ !! Suc (length p + x)"
      by simp (metis Suc_pred add.commute diff_Suc_Suc length_greater_0_conv less_add_Suc1 less_diff_conv)
    then show "∃i. x < smap snd ?σ !! i" ..
  qed
qed

lemma τ_prefix_conv: "prefix_of p s ⟹ prefix_of p s' ⟹ i < plen p ⟹ τ s i = τ s' i"
  by transfer (simp add: stake_nth[symmetric])

lemma Γ_prefix_conv: "prefix_of p s ⟹ prefix_of p s' ⟹ i < plen p ⟹ Γ s i = Γ s' i"
  by transfer (simp add: stake_nth[symmetric])

lemma sincreasing_sdrop:
  fixes s :: "('a :: semilattice_sup) stream"
  assumes "sincreasing s"
  shows "sincreasing (sdrop n s)"
proof (rule sincreasingI)
  fix x
  obtain i where "n < i" and "x < s !! i"
    using sincreasing_grD[OF assms] by blast
  then have "x < sdrop n s !! (i - n)"
    by (simp add: sdrop_snth)
  then show "∃i. x < sdrop n s !! i" ..
qed

lemma ssorted_shift:
  "ssorted (xs @- s) = (sorted xs ∧ ssorted s ∧ (∀x∈set xs. ∀y∈sset s. x ≤ y))"
proof safe
  assume *: "ssorted (xs @- s)"
  then show "sorted xs"
    by (auto simp: ssorted_iff_mono shift_snth sorted_iff_nth_mono split: if_splits)
  from ssorted_sdrop[OF *, of "length xs"] show "ssorted s"
    by (auto simp: sdrop_shift)
  fix x y assume "x ∈ set xs" "y ∈ sset s"
  then obtain i j where "i < length xs" "xs ! i = x" "s !! j = y"
    by (auto simp: set_conv_nth sset_range)
  with ssorted_monoD[OF *, of i "j + length xs"] show "x ≤ y" by auto
next
  assume "sorted xs" "ssorted s" "∀x∈set xs. ∀y∈sset s. x ≤ y"
  then show "ssorted (xs @- s)"
  proof (coinduction arbitrary: xs s)
    case (ssorted xs s)
    with ‹ssorted s› show ?case
      by (subst (asm) ssorted.simps) (auto 0 4 simp: neq_Nil_conv shd_sset intro: exI[of _ "_ # _"])
  qed
qed

lemma sincreasing_shift:
  assumes "sincreasing s"
  shows "sincreasing (xs @- s)"
proof (rule sincreasingI)
  fix x
  from assms obtain i where "x < s !! i"
    unfolding sincreasing_def by blast
  then have "x < (xs @- s) !! (length xs + i)"
    by simp
  then show "∃i. x < (xs @- s) !! i" ..
qed

lift_definition replace_prefix :: "'a prefix ⇒ 'a trace ⇒ 'a trace" is
   "λπ σ. if ssorted (smap snd (π @- sdrop (length π) σ)) then
     π @- sdrop (length π) σ else smap (λi. ({}, i)) nats"
  by (auto split: if_splits simp: stream.map_comp stream.map_ident sdrop_smap[symmetric]
    simp del: sdrop_smap intro!: sincreasing_shift sincreasing_sdrop cong: stream.map_cong)

lemma prefix_of_replace_prefix:
  "prefix_of (pmap_Γ f π) σ ⟹ prefix_of π (replace_prefix π σ)"
proof (transfer; safe; goal_cases)
  case (1 f π σ)
  then show ?case
    by (subst (asm) (2) stake_sdrop[symmetric, of _ "length π"])
      (auto 0 3 simp: ssorted_shift split_beta o_def stake_shift sdrop_smap[symmetric]
        ssorted_sdrop not_le simp del: sdrop_smap)
qed

lemma map_Γ_replace_prefix:
  "∀x. f (f x) = f x ⟹ prefix_of (pmap_Γ f π) σ ⟹ map_Γ f (replace_prefix π σ) = map_Γ f σ"
proof (transfer; safe; goal_cases)
  case (1 f π σ)
  then show ?case
    by (subst (asm) (2) stake_sdrop[symmetric, of σ "length π"],
        subst (3) stake_sdrop[symmetric, of σ "length π"])
      (auto simp: ssorted_shift split_beta o_def stake_shift sdrop_smap[symmetric] ssorted_sdrop
        not_le simp del: sdrop_smap cong: map_cong)
qed

lemma prefix_of_pmap_Γ_D:
  assumes "prefix_of (pmap_Γ f π) σ"
  shows "∃σ'. prefix_of π σ' ∧ prefix_of (pmap_Γ f π) (map_Γ f σ')"
proof -
  from assms(1) obtain σ' where 1: "prefix_of π σ'"
    using ex_prefix_of by blast
  then have "prefix_of (pmap_Γ f π) (map_Γ f σ')"
    by transfer simp
  with 1 show ?thesis by blast
qed

lemma prefix_of_map_Γ_D:
  assumes "prefix_of π' (map_Γ f σ)"
  shows "∃π''. π' = pmap_Γ f π'' ∧ prefix_of π'' σ"
  using assms
  by transfer (auto intro!: exI[of _ "stake (length _) _"] elim: sym dest: sorted_stake)

lift_definition pts :: "'a prefix ⇒ nat list" is "map snd" .

lemma pts_pmap_Γ[simp]: "pts (pmap_Γ f π) = pts π"
  by (transfer fixing: f) (simp add: split_beta)

(*<*)
end
(*>*)