Theory Traces

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Traces
imports Main
begin
(*>*)

section‹Traces›

text‹

A \emph{trace} is a non-empty sequence of states. This custom type has
the advantage over the standard HOL list type of providing a more
suitable induction rule. We use these to give a semantics to
knowledge-based programs in \S\ref{sec:kbps-theory-kbps-semantics}.

›

datatype 's Trace = tInit "'s"
                  | tStep "'s Trace" "'s" (infixl "↝" 65)

fun tFirst :: "'s Trace ⇒ 's" where
    "tFirst (tInit s) = s"
  | "tFirst (t ↝ s) = tFirst t"

fun tLast :: "'s Trace ⇒ 's" where
    "tLast (tInit s) = s"
  | "tLast (t ↝ s) = s"
(*<*)

lemma tLast_tInit_comp[simp]: "tLast ∘ tInit = id"
  by (rule ext) simp
(*>*)

text‹

We provide a few of the standard list operations: @{term "tLength"},
@{term "tMap"} and @{term "tZip"}. Our later ease hinges on taking the
length of a trace to be zero-based.

›

fun tLength :: "'s Trace ⇒ nat" where
    "tLength (tInit s) = 0"
  | "tLength (t ↝ s) = 1 + tLength t"

(*<*)
lemma tLength_0_conv:
  "(tLength t = 0) ⟷ (∃s. t = tInit s)"
  by (cases t) simp_all

lemma tLength_g0_conv:
  "(tLength t > 0) ⟷ (∃s t'. t = t' ↝ s ∧ tLength t = Suc (tLength t'))"
  by (cases t) simp_all

lemma tLength_Suc:
  "tLength t = Suc n ⟹ (∃s t'. t = t' ↝ s ∧ tLength t' = n)"
  by (cases t) simp_all

lemma trace_induct2[consumes 1, case_names tInit tStep]:
  assumes tLen: "tLength t = tLength t'"
      and tI: "⋀s s'. P (tInit s) (tInit s')"
      and tS: "⋀s s' t t'. ⟦ tLength t = tLength t'; P t t' ⟧
               ⟹ P (t ↝ s) (t' ↝ s')"
  shows "P t t'"
using tLen
proof (induct t arbitrary: t')
  case (tInit s t') with tI show ?case by (auto iff: tLength_0_conv)
next
  case (tStep t s t') with tS show ?case by (cases t') simp_all
qed
(*>*)

fun tMap where
  "tMap f (tInit x) = tInit (f x)"
| "tMap f (xs ↝ x) = tMap f xs ↝ f x"

(*<*)
lemma tLength_tMap[iff]: "tLength (tMap f t) = tLength t"
  by (induct t) simp_all

lemma tMap_is_tInit[iff]: "(tMap f t = tInit s) ⟷ (∃s'. t = tInit s' ∧ f s' = s)"
  by (cases t) simp_all

lemma tInit_is_tMap[iff]: "(tInit s = tMap f t) ⟷ (∃s'. t = tInit s' ∧ f s' = s)"
  by (cases t) auto

lemma tStep_is_tMap_conv[iff]:
 "(tp ↝ s = tMap f t) ⟷ (∃tp' s'. t = tp' ↝ s' ∧ s = f s' ∧ tp = tMap f tp')"
  by (cases t) auto

lemma tMap_is_tStep_conv[iff]:
 "(tMap f t = tp ↝ s) ⟷ (∃tp' s'. t = tp' ↝ s' ∧ s = f s' ∧ tMap f tp' = tp)"
  by (cases t) auto

lemma tMap_eq_imp_tLength_eq:
  assumes "tMap f t = tMap f' t'"
  shows "tLength t = tLength t'"
using assms
proof (induct t arbitrary: t')
  case (tStep tp s t')
  then obtain tp' s' where t': "t' = tp' ↝ s'" by fastforce
  moreover with tStep have "tLength tp' = tLength tp" by simp
  with t' show ?case by simp
qed auto

lemma tMap_tFirst[iff]:
  "tFirst (tMap f t) = f (tFirst t)"
  by (induct t) simp_all

lemma tMap_tLast[iff]:
  "tLast (tMap f t) = f (tLast t)"
  by (induct t) simp_all

lemma tMap_tFirst_inv:
  assumes M: "tMap f t = tMap f' t'"
  shows "f (tFirst t) = f' (tFirst t')"
proof -
  from M have L: "tLength t = tLength t'" by (rule tMap_eq_imp_tLength_eq)
  from L M show ?thesis by (induct rule: trace_induct2, simp_all)
qed

lemma tMap_tLast_inv:
  assumes M: "tMap f t = tMap f' t'"
  shows "f (tLast t) = f' (tLast t')"
proof -
  from M have L: "tLength t = tLength t'" by (rule tMap_eq_imp_tLength_eq)
  from L M show ?thesis by (induct rule: trace_induct2, simp_all)
qed
(*>*)

fun tZip where
  "tZip f (tInit x) (tInit y) = tInit (f x y)"
| "tZip f (xs ↝ x) (ys ↝ y) = tZip f xs ys ↝ f x y"
(*<*)

lemma tLength_tZip[iff]: "tLength xs = tLength ys ⟹ tLength (tZip f xs ys) = tLength xs"
  by (induct rule: trace_induct2) simp_all

(*>*)
(*<*)
end
(*>*)