Theory Trace

(*<*)
theory Trace
  imports "MFOTL_Monitor.Interval" "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])

definition "sfinite s = (∀i. finite (s !! i))"

lemma sfiniteI: "(⋀i. finite (s !! i)) ⟹ sfinite s"
  by (simp add: sfinite_def)

typedef 'a trace = "{s :: ('a set × nat) stream. ssorted (smap snd s) ∧ sincreasing (smap snd s) ∧ sfinite (smap fst s)}"
  by (intro exI[of _ "smap (λi. ({}, i)) nats"])
    (auto simp: stream.map_comp stream.map_ident sfinite_def 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)"

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 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 τ_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 pts :: "'a prefix ⇒ nat list" is "map snd" .

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

subsection ‹Earliest and Latest Time-Points›

definition ETP:: "'a trace ⇒ nat ⇒ nat"  where
  "ETP σ t = (LEAST i. τ σ i ≥ t)"

definition LTP:: "'a trace ⇒ nat ⇒ nat" where
  "LTP σ t = Max {i. (τ σ i) ≤ t}"

abbreviation "δ σ i j ≡ (τ σ i - τ σ j)"

abbreviation "ETP_p σ i b ≡ ETP σ ((τ σ i) - b)"
abbreviation "LTP_p σ i I ≡ min i (LTP σ ((τ σ i) - left I))"
abbreviation "ETP_f σ i I ≡ max i (ETP σ ((τ σ i) + left I))"
abbreviation "LTP_f σ i b ≡ LTP σ ((τ σ i) + b)"

definition max_opt where
  "max_opt a b = (case (a,b) of (Some x, Some y) ⇒ Some (max x y) | _ ⇒ None)"

definition "LTP_p_safe σ i I = (if τ σ i - left I ≥ τ σ 0 then LTP_p σ i I else 0)"

lemma i_ETP_tau: "i ≥ ETP σ n ⟷ τ σ i ≥ n"
proof
  assume P: "i ≥ ETP σ n"
  define j where j_def: "j ≡ ETP σ n"
  then have i_j: "τ σ i ≥ τ σ j" using P by auto
  from j_def have "τ σ j ≥ n"
    unfolding ETP_def using LeastI_ex ex_le_τ by force
  then show "τ σ i ≥ n" using i_j by auto
next
  assume Q: "τ σ i ≥ n"
  then show "ETP σ n ≤ i" unfolding ETP_def
    by (auto simp add: Least_le)
qed

lemma tau_LTP_k: 
  assumes "τ σ 0 ≤ n" "LTP σ n < k"
  shows "τ σ k > n"
proof -
  have "finite {i. τ σ i ≤ n}"
    by (rule ccontr, unfold infinite_nat_iff_unbounded_le mem_Collect_eq)
      (metis Suc_le_eq i_ETP_tau  leD)
  then show ?thesis
    using assms(2) Max.coboundedI linorder_not_less
    unfolding LTP_def by auto
qed

lemma i_LTP_tau:
  assumes n_asm: "n ≥ τ σ 0"
  shows "(i ≤ LTP σ n ⟷ τ σ i ≤ n)"
proof
  define A and j where A_def: "A ≡ {i. τ σ i ≤ n}" and j_def: "j ≡ LTP σ n"
  assume P: "i ≤ LTP σ n"
  from n_asm A_def have A_ne: "A ≠ {}" by auto
  from j_def have i_j: "τ σ i ≤ τ σ j" using P by auto
  have not_in: "k ∉ A" if "j < k" for k
    using n_asm that tau_LTP_k leD
    unfolding A_def j_def by blast
  then have "A ⊆ {0..<Suc j}"
    using assms not_less_eq
    unfolding A_def j_def 
    by fastforce
  then have fin_A: "finite A"
    using subset_eq_atLeast0_lessThan_finite[of A "Suc j"]
    by simp
  from A_ne j_def have "τ σ j ≤ n"
    using Max_in[of A] A_def fin_A 
    unfolding LTP_def 
    by simp
  then show "τ σ i ≤ n" using i_j by auto
next
  define A and j where A_def: "A ≡ {i. τ σ i ≤ n}" and j_def: "j ≡ LTP σ n"
  assume Q: "τ σ i ≤ n" 
  have not_in: "k ∉ A" if "j < k" for k
    using n_asm that tau_LTP_k leD
    unfolding A_def j_def by blast
  then have "A ⊆ {0..<Suc j}"
    using assms not_less_eq
    unfolding A_def j_def 
    by fastforce
  then have fin_A: "finite A"
    using subset_eq_atLeast0_lessThan_finite[of A "Suc j"]
    by simp
  moreover have "i ∈ A" using Q A_def by auto
  ultimately show "i ≤ LTP σ n" 
    using Max_ge[of A] A_def 
    unfolding LTP_def
    by auto
qed

lemma ETP_δ: "i ≥ ETP σ (τ σ l + n) ⟹ δ σ i l ≥ n"
proof -
  assume P: "i ≥ ETP σ (τ σ l + n)"
  then have "τ σ i ≥ τ σ l + n" by (auto simp add: i_ETP_tau)
  then show ?thesis by auto
qed

lemma ETP_ge: "ETP σ (τ σ l + n + 1) > l"
proof -
  define j where j_def: "j ≡ τ σ l + n + 1"
  then have etp_j: "τ σ (ETP σ j) ≥ j" unfolding ETP_def
    using LeastI_ex ex_le_τ by force
  then have "τ σ (ETP σ j) > τ σ l" using j_def by auto
  then show ?thesis using j_def less_τD by blast
qed

lemma i_le_LTPi: "i ≤ LTP σ (τ σ i)"
  using τ_mono i_LTP_tau[of σ "τ σ i" i]
  by auto

lemma i_le_LTPi_add: "i ≤ LTP σ (τ σ i + n)"
  using i_le_LTPi
  by (simp add: add_increasing2 i_LTP_tau)

lemma i_le_LTPi_minus:
  assumes "τ σ 0 + n ≤ τ σ i" "i > 0" "n > 0"
  shows "LTP σ (τ σ i - n) < i"
  unfolding LTP_def
proof (subst Max_less_iff; (intro ballI; elim CollectE)?)
  show "finite {j. τ σ j ≤ τ σ i - n}"
    unfolding finite_nat_set_iff_bounded_le
  proof (intro exI[of _ i], safe)
    fix j
    assume "τ σ j ≤ τ σ i - n"
    with assms(1,3) show "j ≤ i"
      by (metis add_leD2 add_strict_increasing le_add_diff_inverse less_τD less_or_eq_imp_le)
  qed
next
  from assms(1) show "{j. τ σ j ≤ τ σ i - n} ≠ {}"
    by (auto simp: le_diff_conv2)
next
  fix j
  assume "τ σ j ≤ τ σ i - n"
  with assms(1,3) show "j < i"
    by (metis add_leD2 add_strict_increasing le_add_diff_inverse less_τD)
qed

lemma i_ge_etpi: "ETP σ (τ σ i) ≤ i"
  using i_ETP_tau by auto

(*<*)
end
(*>*)