Theory Trace

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

section ‹Infinite Traces›

inductive sorted_list :: "'a :: order list ⇒ bool" where
  [intro]: "sorted_list []"
| [intro]: "sorted_list [x]"
| [intro]: "x ≤ y ⟹ sorted_list (y # ys) ⟹ sorted_list (x # y # ys)"

lemma sorted_list_app: "sorted_list xs ⟹ (⋀x. x ∈ set xs ⟹ x ≤ y) ⟹ sorted_list (xs @ [y])"
  by (induction xs rule: sorted_list.induct) auto

lemma sorted_list_drop: "sorted_list xs ⟹ sorted_list (drop n xs)"
proof (induction xs arbitrary: n rule: sorted_list.induct)
  case (2 x n)
  then show ?case
    by (cases n) auto
next
  case (3 x y ys n)
  then show ?case
    by (cases n) auto
qed auto

lemma sorted_list_ConsD: "sorted_list (x # xs) ⟹ sorted_list xs"
  by (auto elim: sorted_list.cases)

lemma sorted_list_Cons_nth: "sorted_list (x # xs) ⟹ j < length xs ⟹ x ≤ xs ! j"
  by (induction "x # xs" arbitrary: x xs j rule: sorted_list.induct)
     (fastforce simp: nth_Cons split: nat.splits)+

lemma sorted_list_atD: "sorted_list xs ⟹ i ≤ j ⟹ j < length xs ⟹ xs ! i ≤ xs ! j"
proof (induction xs arbitrary: i j rule: sorted_list.induct)
  case (2 x i j)
  then show ?case
    by (cases i) auto
next
  case (3 x y ys i j)
  have "x ≤ (x # y # ys) ! j"
    using 3(5) sorted_list_Cons_nth[OF sorted_list.intros(3)[OF 3(1,2)]]
    by (auto simp: nth_Cons split: nat.splits)
  then show ?case
    using 3
    by (cases i) auto
qed auto

coinductive ssorted :: "'a :: order 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_list (stake i s)"
proof (induct i arbitrary: s)
  case (Suc i)
  then show ?case
    by (cases i) (auto elim: ssorted.cases)
qed auto

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

typedef (overloaded) ('a, 'b :: timestamp) trace = "{s :: ('a set × 'b) stream.
  ssorted (smap snd s) ∧ (∀x. x ∈ snd ` sset s ⟶ x ∈ tfin) ∧ (∀i x. x ∈ tfin ⟶ (∃j. ¬snd (s !! j) ≤ snd (s !! i) + x))}"
  by (auto simp: ι_mono ι_tfin ι_progressing stream.set_map
      intro!: exI[of _ "smap (λn. ({}, ι n)) nats"] ssorted_monoI)

setup_lifting type_definition_trace

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

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

lemma τ_fin: "τ σ i ∈ tfin"
  by transfer auto

lemma ex_lt_τ: "x ∈ tfin ⟹ ∃j. ¬τ s j ≤ τ s i + x"
  by transfer auto

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)

(*<*)
end
(*>*)