# Theory Traces

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

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
(*>*)