Theory Aczel_Sequences

(*<*)
theory Aczel_Sequences
imports
  HOL_Basis
begin

(*>*)
section‹ Terminated Aczel sequences\label{sec:aczel_sequences} ›

text‹

We model a ∗‹behavior› of a system as a non-empty finite or infinite sequence of the form
‹s⇩0 -a⇩1→ s⇩1 -a⇩2→ … (→ v)?› where ‹s⇩i› is a state, ‹a⇩i› an agent and ‹v› a return value for
finite sequences (see \S\ref{sec:tls}).  A ∗‹trace› is a finite sequence
‹s⇩0 -a⇩1→ s⇩1 -a⇩2→ … -a⇩n→ s⇩n → v› for ‹n ≥ 0› with optional return value ‹v› (see
\S\ref{sec:safety_logic}). States, agents and return values are of arbitrary type.

›


subsection‹ Traces\label{sec:aczel_sequences-traces} ›

setup ‹Sign.mandatory_path "trace"›

datatype (aset: 'a, sset: 's, vset: 'v) t =
  T (init: 's) (rest: "('a × 's) list") ("term": "'v option")
for
  map: map
  pred: pred
  rel: rel

declare trace.t.map_id0[simp]
declare trace.t.map_id0[unfolded id_def, simp]
declare trace.t.map_sel[simp]
declare trace.t.set_map[simp]
declare trace.t.map_comp[unfolded o_def, simp]
declare trace.t.set[simp del]

instance trace.t :: (countable, countable, countable) countable by countable_datatype

lemma split_all[no_atp]: ―‹ imitate the setup for \<^typ>‹'a × 'b› without the automation ›
  shows "(⋀x. PROP P x) ≡ (⋀s xs v. PROP P (trace.T s xs v))"
proof
  show "PROP P (trace.T s xs v)" if "⋀x. PROP P x" for s xs v by (rule that)
next
  fix x
  assume "⋀s xs v. PROP P (trace.T s xs v)"
  from ‹PROP P (trace.T (trace.init x) (trace.rest x) (trace.term x))› show "PROP P x" by simp
qed

lemma split_All[no_atp]:
  shows "(∀x. P x) ⟷ (∀s xs v. P (trace.T s xs v))" (is "?lhs ⟷ ?rhs")
proof (intro iffI allI)
  show "P x" if ?rhs for x using that by (cases x) simp_all
qed simp

lemma split_Ex[no_atp]:
  shows "(∃x. P x) ⟷ (∃s xs v. P (trace.T s xs v))" (is "?lhs ⟷ ?rhs")
proof (intro iffI allI; elim exE)
  show "∃s xs v. P (trace.T s xs v)" if "P x" for x using that by (cases x) fast
qed auto


subsection‹ Combinators on traces\label{sec:aczel_sequences-traces-combinators} ›

definition final' :: "'s ⇒ ('a × 's) list ⇒ 's" where
  "final' s xs = last (s # map snd xs)"

abbreviation (input) final :: "('a, 's, 'v) trace.t ⇒ 's" where
  "final σ ≡ trace.final' (trace.init σ) (trace.rest σ)"

definition continue :: "('a, 's, 'v) trace.t ⇒ ('a × 's) list × 'v option ⇒ ('a, 's, 'v) trace.t" (infixl ‹@-⇩S› 64) where
  "σ @-⇩S xsv = (case trace.term σ of None ⇒ trace.T (trace.init σ) (trace.rest σ @ fst xsv) (snd xsv) | Some v ⇒ σ)"

definition tl :: "('a, 's, 'v) trace.t ⇀ ('a, 's, 'v) trace.t" where
  "tl σ = (case trace.rest σ of [] ⇒ None | x # xs ⇒ Some (trace.T (snd x) xs (trace.term σ)))"

definition dropn :: "nat ⇒ ('a, 's, 'v) trace.t ⇀ ('a, 's, 'v) trace.t" where
  "dropn = (^^) trace.tl"

definition take :: "nat ⇒ ('a, 's, 'v) trace.t ⇒ ('a, 's, 'v) trace.t" where
  "take i σ = (if i ≤ length (trace.rest σ) then trace.T (trace.init σ) (List.take i (trace.rest σ)) None else σ)"

type_synonym ('a, 's) transitions = "('a × 's × 's) list"

primrec transitions' :: "'s ⇒ ('a × 's) list ⇒ ('a, 's) trace.transitions" where
  "transitions' s [] = []"
| "transitions' s (x # xs) = (fst x, s, snd x) # transitions' (snd x) xs"

abbreviation (input) transitions :: "('a, 's, 'v) trace.t ⇒ ('a, 's) trace.transitions" where
  "transitions σ ≡ trace.transitions' (trace.init σ) (trace.rest σ)"

setup ‹Sign.mandatory_path "final'"›

lemma simps[simp]:
  shows "trace.final' s [] = s"
    and "trace.final' s (x # xs) = trace.final' (snd x) xs"
    and "trace.final' s (xs @ ys) = trace.final' (trace.final' s xs) ys"
    and idle: "snd ` set xs ⊆ {s} ⟹ trace.final' s xs = s"
    and "snd ` set xs ⊆ {s} ⟹ trace.final' s (xs @ ys) = trace.final' s ys"
    and "snd ` set ys ⊆ {trace.final' s xs} ⟹ trace.final' s (xs @ ys) = trace.final' s xs"
by (simp_all add: trace.final'_def last_map image_subset_iff split: if_split_asm)

lemma map:
  shows "trace.final' (sf s) (map (map_prod af sf) xs) = sf (trace.final' s xs)"
by (simp add: trace.final'_def last_map)

lemma replicate:
  shows "trace.final' s (replicate i as) = (if i = 0 then s else snd as)"
by (simp add: trace.final'_def)

lemma map_idle:
  assumes "(λx. sf (snd x)) ` set xs ⊆ {sf s}"
  shows "sf (trace.final' s xs) = sf s"
using assms by (induct xs arbitrary: s) simp_all

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "tl"›

lemma simps[simp]:
  shows "trace.tl (trace.T s [] v) = None"
    and "trace.tl (trace.T s (x # xs) v) = Some (trace.T (snd x) xs v)"
by (simp_all add: trace.tl_def)

setup ‹Sign.parent_path›

lemma dropn_alt_def:
  shows "trace.dropn i σ
       = (case drop i ((undefined, trace.init σ) # trace.rest σ) of
           [] ⇒ None
         | x # xs ⇒ Some (trace.T (snd x) xs (trace.term σ)))"
proof(induct i arbitrary: σ)
  case 0 show ?case
    by (simp add: trace.dropn_def)
next
  case (Suc i σ) then show ?case
    by (cases σ; cases "trace.rest σ"; simp add: trace.dropn_def drop_Cons' split: list.split)
qed

setup ‹Sign.mandatory_path "dropn"›

lemma simps[simp]:
  shows 0: "trace.dropn 0 = Some"
    and Suc: "trace.dropn (Suc i) σ = Option.bind (trace.tl σ) (trace.dropn i)"
    and dropn: "Option.bind (trace.dropn i σ) (trace.dropn j) = trace.dropn (i + j) σ"
by (simp_all add: trace.dropn_def pfunpow_add)

lemma Suc_right:
  shows "trace.dropn (Suc i) σ = Option.bind (trace.dropn i σ) trace.tl"
by (simp add: trace.dropn_def pfunpow_Suc_right del: pfunpow.simps)

lemma eq_none_length_conv:
  shows "trace.dropn i σ = None ⟷ length (trace.rest σ) < i"
by (auto simp: trace.dropn_alt_def split: list.split)

lemma eq_Some_length_conv:
  shows "(∃σ'. trace.dropn i σ = Some σ') ⟷ i ≤ length (trace.rest σ)"
by (auto simp: trace.dropn_alt_def dest: drop_eq_Cons_lengthD split: list.split)

lemma eq_Some_lengthD:
  assumes "trace.dropn i σ = Some σ'"
  shows "i ≤ length (trace.rest σ)"
using assms trace.dropn.eq_Some_length_conv by blast

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "take"›

lemma sel:
  shows "trace.init (trace.take i σ) = trace.init σ"
    and "trace.rest (trace.take i σ) = List.take i (trace.rest σ)"
    and "trace.term (trace.take i σ) = (if i ≤ length (trace.rest σ) then None else trace.term σ)"
by (simp_all add: trace.take_def)

lemma 0:
  shows "trace.take 0 σ = trace.T (trace.init σ) [] None"
by (simp add: trace.take_def)

lemma Nil:
  shows "trace.take i (trace.T s [] None) = trace.T s [] None"
by (simp add: trace.take_def)

lemmas simps[simp] =
  trace.take.sel
  "trace.take.0"
  trace.take.Nil

lemma map:
  shows "trace.take i (trace.map af sf vf σ) = trace.map af sf vf (trace.take i σ)"
by (simp add: trace.take_def take_map)

lemma append:
  shows "trace.take i (trace.T s (xs @ ys) v) = trace.T s (List.take i (xs @ ys)) (if length (xs @ ys) < i then v else None)"
by (simp add: trace.take_def)

lemma take:
  shows "trace.take i (trace.take j σ) = trace.take (min i j) σ"
by (simp add: min_le_iff_disj trace.take_def)

lemma continue:
  shows "trace.take i (σ @-⇩S xsv)
       = trace.take i σ @-⇩S (List.take (i - length (trace.rest σ)) (fst xsv),
                            if i ≤ length (trace.rest σ) + length (fst xsv) then None else snd xsv)"
by (simp add: trace.continue_def trace.take_def split: option.split)

lemma all_iff:
  shows "trace.take i σ = σ ⟷ (case trace.term σ of None ⇒ length (trace.rest σ) | Some _ ⇒ Suc (length (trace.rest σ))) ≤ i" (is ?thesis1)
    and "σ = trace.take i σ ⟷ (case trace.term σ of None ⇒ length (trace.rest σ) | Some _ ⇒ Suc (length (trace.rest σ))) ≤ i" (is ?thesis2)
proof -
  show ?thesis1 by (cases σ) (simp add: trace.take_def split: option.split)
  then show ?thesis2
    by (rule eq_commute_conv)
qed

lemmas all = iffD2[OF trace.take.all_iff(1)]

lemma Ex_all:
  shows "σ = trace.take (Suc (length (trace.rest σ))) σ"
by (simp add: trace.take_def)

lemma replicate:
  shows "trace.take i (trace.T s (replicate j as) v)
      = trace.T s (replicate (min i j) as) (if i ≤ j then None else v)"
by (simp add: trace.take_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "continue"›

lemma sel[simp]:
  shows "trace.init (σ @-⇩S xs) = trace.init σ"
    and "trace.rest (σ @-⇩S xsv) = (case trace.term σ of None ⇒ trace.rest σ @ fst xsv | Some v ⇒ trace.rest σ)"
    and "trace.term (σ @-⇩S xsv) = (case trace.term σ of None ⇒ snd xsv | Some v ⇒ trace.term σ)"
by (simp_all add: trace.continue_def split: option.split)

lemma simps[simp]:
  shows "trace.T s xs None @-⇩S ysv = trace.T s (xs @ fst ysv) (snd ysv)"
    and "trace.T s xs (Some v) @-⇩S ysv = trace.T s xs (Some v)"
    and "σ @-⇩S ([], None) = σ"
by (simp_all add: trace.continue_def trace.t.expand split: option.split)

lemma Nil:
  shows "σ @-⇩S ([], trace.term σ) = σ"
    and "trace.T (trace.init σ) [] None @-⇩S (trace.rest σ, trace.term σ) = σ"
by (cases σ) (simp_all add: trace.continue_def split: option.split)

lemma map:
  shows "trace.map af sf vf (σ @-⇩S xsv) = trace.map af sf vf σ @-⇩S map_prod (map (map_prod af sf)) (map_option vf) xsv"
by (simp add: trace.continue_def split: option.split)

lemma eq_trace_conv:
  shows "σ @-⇩S xsv = trace.T s xs v ⟷ trace.init σ = s ∧ (case trace.term σ of None ⇒ trace.rest σ @ fst xsv = xs ∧ v = snd xsv | Some v' ⇒ trace.rest σ = xs ∧ v = Some v')"
    and "trace.T s xs v = σ @-⇩S xsv ⟷ trace.init σ = s ∧ (case trace.term σ of None ⇒ trace.rest σ @ fst xsv = xs ∧ v = snd xsv | Some v' ⇒ trace.rest σ = xs ∧ v = Some v')"
by (case_tac [!] σ) (auto simp: trace.continue_def split: option.split)

lemma self_conv:
  shows "(σ = σ @-⇩S xsv) ⟷ (case trace.term σ of None ⇒ xsv = ([], None) | Some _ ⇒ True)"
    and "(σ @-⇩S xsv = σ) ⟷ (case trace.term σ of None ⇒ xsv = ([], None) | Some _ ⇒ True)"
by (cases σ; cases xsv; fastforce split: option.splits)+

lemma same_eq:
  shows "(σ @-⇩S xsv = σ @-⇩S ysv) ⟷ (case trace.term σ of None ⇒ xsv = ysv | Some _ ⇒ True)"
by (fastforce simp: trace.continue_def prod.expand split: option.split)

lemma continue:
  shows "σ @-⇩S xsv @-⇩S ysv = σ @-⇩S (case snd xsv of None ⇒ (fst xsv @ fst ysv, snd ysv) | Some _ ⇒ xsv)"
by (simp add: trace.continue_def split: option.split)

lemma take_drop_id:
  shows "trace.take i σ @-⇩S case_option ([], None) (λσ'. (trace.rest σ', trace.term σ')) (trace.dropn i σ) = σ"
by (cases σ)
   (clarsimp simp: trace.take_def trace.dropn_alt_def split: list.split;
    metis append_take_drop_id list.sel(3) tl_drop)

setup ‹Sign.parent_path›


paragraph‹ Prefix ordering ›

instantiation trace.t :: (type, type, type) order
begin

definition less_eq_t :: "('a, 's, 'v) trace.t relp" where
  "less_eq_t σ⇩1 σ⇩2 ⟷ (∃xsv. σ⇩2 = σ⇩1 @-⇩S xsv)"

definition less_t :: "('a, 's, 'v) trace.t relp" where
  "less_t σ⇩1 σ⇩2 ⟷ σ⇩1 ≤ σ⇩2 ∧ σ⇩1 ≠ σ⇩2"

instance
by standard
   (auto simp: less_eq_t_def less_t_def trace.continue.self_conv trace.continue.continue trace.continue.same_eq
        split: option.splits)

end

lemma less_eqE[consumes 1, case_names prefix maximal]:
  assumes "σ⇩1 ≤ σ⇩2"
  assumes "⟦trace.term σ⇩1 = None; trace.init σ⇩1 = trace.init σ⇩2; prefix (trace.rest σ⇩1) (trace.rest σ⇩2)⟧ ⟹ P"
  assumes "⋀v. ⟦trace.term σ⇩1 = Some v; σ⇩1 = σ⇩2⟧ ⟹ P"
  shows P
using assms by (cases "trace.term σ⇩1") (auto simp: trace.less_eq_t_def trace.continue.self_conv)

lemmas less_eq_extE[consumes 1, case_names prefix maximal]
  = trace.less_eqE[of "trace.T s⇩1 xs⇩1 v⇩1" "trace.T s⇩2 xs⇩2 v⇩2", simplified, simplified conj_explode]
    for s⇩1 xs⇩1 v⇩1 s⇩2 xs⇩2 v⇩2

lemma less_eq_self_continue:
  shows "σ ≤ σ @-⇩S xsv"
using trace.less_eq_t_def by blast

lemma less_eq_same_append_conv:
  shows "trace.T s xs v ≤ trace.T s' (xs @ ys) v' ⟷ s = s' ∧ (∀v''. v = Some v'' ⟶ ys = [] ∧ v = v')"
by (auto simp: trace.less_eq_t_def trace.continue.eq_trace_conv split: option.split)

lemma less_same_append_conv:
  shows "trace.T s xs v < trace.T s' (xs @ ys) v' ⟷ s = s' ∧ v = None ∧ (ys ≠ [] ∨ (∃v''. v' = Some v''))"
by (cases v) (auto simp: trace.less_t_def trace.less_eq_same_append_conv)

lemma less_eq_Some[simp]:
  shows "trace.T s xs (Some v) ≤ σ ⟷ trace.init σ = s ∧ trace.rest σ = xs ∧ trace.term σ = Some v"
by (cases σ) (simp add: trace.less_eq_t_def)

lemma less_eq_None:
  shows "σ ≤ trace.T s xs None ⟷ trace.init σ = s ∧ prefix (trace.rest σ) xs ∧ trace.term σ = None"
    and "trace.T s xs None ≤ σ ⟷ trace.init σ = s ∧ prefix xs (trace.rest σ)"
by (case_tac [!] σ) (auto simp: trace.less_eq_same_append_conv elim!: trace.less_eqE prefixE)

lemma less:
  shows "trace.T s xs v < σ ⟷ trace.init σ = s ∧ (∃ys. trace.rest σ = xs @ ys ∧ (trace.term σ = None ⟶ ys ≠ [])) ∧ v = None"
    and "σ < trace.T s xs v  ⟷ trace.init σ = s ∧ (∃ys. xs = trace.rest σ @ ys ∧ (v = None ⟶ ys ≠ [])) ∧ trace.term σ = None"
by (case_tac [!] σ)
   (auto simp: trace.less_t_def trace.less_eq_t_def trace.continue.eq_trace_conv split: option.split_asm)

lemma less_eq_take[iff]:
  shows "trace.take i σ ≤ σ"
by (simp add: trace.take_def take_is_prefix trace.less_eq_None)

lemma less_eq_takeE:
  assumes "σ⇩1 ≤ σ⇩2"
  obtains i where "σ⇩1 = trace.take i σ⇩2"
using assms
by (cases σ⇩1)
   (auto simp: trace.take_def
        elim!: trace.less_eqE prefixE
         dest: meta_spec[where x="length (trace.rest σ⇩1)"]
                  meta_spec[where x="Suc (length (trace.rest σ⇩1))"])

lemma less_eq_take_def:
  shows "σ⇩1 ≤ σ⇩2 ⟷ (∃i. σ⇩1 = trace.take i σ⇩2)"
by (blast elim: trace.less_eq_takeE)

lemma less_take_less_eq:
  assumes "σ < trace.take (Suc i) σ'"
  shows "σ ≤ trace.take i σ'"
using assms
by (clarsimp simp: trace.less_t_def trace.less_eq_take_def trace.take.take) (metis le_SucE min_def)

lemma wfP_less:
  shows "wfP ((<) :: (_, _, _) trace.t relp)"
unfolding wfp_def
proof(rule wf_subset[rotated])
  let ?r = "inv_image ({(None, Some v) |v. True} <*lex*> {(x, y). strict_prefix x y}) (λσ. (trace.term σ, trace.rest σ))"
  show "wf ?r"
    using wfp_def wfP_strict_prefix wf_def by fastforce
  show "{(x, y). x < y} ⊆ ?r"
    by (auto simp: trace.less_t_def trace.less_eq_take_def trace.take.all_iff split: option.splits)
qed

lemma less_eq_same_cases:
  fixes ys :: "(_, _, _) trace.t"
  assumes "xs⇩1 ≤ ys"
  assumes "xs⇩2 ≤ ys"
  shows "xs⇩1 ≤ xs⇩2 ∨ xs⇩2 ≤ xs⇩1"
using assms
by (clarsimp simp: trace.less_eq_take_def trace.take.take) (metis min.absorb_iff1 nle_le)

setup ‹Sign.mandatory_path "take"›

lemma mono:
  assumes "σ⇩1 ≤ σ⇩2"
  assumes "i ≤ j"
  shows "trace.take i σ⇩1 ≤ trace.take j σ⇩2"
using assms
by (clarsimp simp: trace.less_eq_take_def trace.take.take) (metis min.assoc min.commute min_def)


setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "map"›

lemmas map = trace.t.map_comp[unfolded comp_def]

lemma monotone:
  shows "mono (trace.map af sf vf)"
by (rule monoI) (fastforce simp: trace.less_eq_take_def trace.take.map)

lemmas strengthen[strg] = st_monotone[OF trace.map.monotone]
lemmas mono = monoD[OF trace.map.monotone]

lemma monotone_less:
  shows "monotone (<) (<) (trace.map af sf vf)"
by (rule monotoneI)
   (auto simp: trace.less_t_def trace.map.mono[OF order.strict_implies_order] trace.split_all
        elim!: trace.less_eqE prefixE)

lemma less_eqR:
  assumes "σ⇩1 ≤ trace.map af sf vf σ⇩2"
  obtains σ⇩2' where "σ⇩2' ≤ σ⇩2" and "σ⇩1 = trace.map af sf vf σ⇩2'"
using assms by (fastforce simp: trace.less_eq_take_def trace.take.map)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "rel"›

lemmas eq = trace.t.rel_eq

lemmas mono = trace.t.rel_mono_strong[of ar sr vr σ⇩1 σ⇩2 ar' sr' vr'] for ar sr vr σ⇩1 σ⇩2 ar' sr' vr'

lemma strengthen[strg]:
  assumes "st_ord F ar ar'"
  assumes "st_ord F sr sr'"
  assumes "st_ord F vr vr'"
  shows "st_ord F (trace.rel ar sr vr σ⇩1 σ⇩2) (trace.rel ar' sr' vr' σ⇩1 σ⇩2)"
using assms by (cases F) (auto intro!: le_boolI elim: trace.rel.mono)

lemma length_rest:
  assumes "trace.rel ar sr vr σ⇩1 σ⇩2"
  shows "length (trace.rest σ⇩1)
       = length (trace.rest σ⇩2) ∧ (∀i<length (trace.rest σ⇩1). rel_prod ar sr (trace.rest σ⇩1 ! i) (trace.rest σ⇩2 ! i))"
by (rule rel_funE[OF trace.t.sel_transfer(2) assms]) (simp add: list_all2_conv_all_nth)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "take"›

lemma rel:
  assumes "trace.rel ar sr vr σ⇩1 σ⇩2"
  shows "trace.rel ar sr vr (trace.take i σ⇩1) (trace.take i σ⇩2)"
using assms
by (auto simp: trace.take_def trace.t.rel_sel trace.rel.length_rest
         elim: rel_funE[OF trace.t.sel_transfer(1)])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "transitions'"›

lemma prefix_conv:
  shows "prefix (trace.transitions' s xs) (trace.transitions' s ys) ⟷ prefix xs ys"
proof(induct xs arbitrary: s ys)
  case (Cons x xs s ys) then show ?case by (cases ys) auto
qed simp

lemma monotone:
  shows "monotone prefix prefix (trace.transitions' s)"
by (rule monotoneI) (simp add: trace.transitions'.prefix_conv)

lemma append:
  shows "trace.transitions' s (xs @ ys) = trace.transitions' s xs @ trace.transitions' (trace.final' s xs) ys"
by (induct xs arbitrary: s ys) simp_all

lemma eq_Nil_conv:
  shows "trace.transitions' s xs = [] ⟷ xs = []"
    and "[] = trace.transitions' s xs ⟷ xs = []"
by (case_tac [!] xs) simp_all

lemma eq_Cons_conv:
  shows "trace.transitions' s xs = y # ys ⟷ (∃a s' xs'. xs = (a, s') # xs' ∧ y = (a, s, s') ∧ ys = trace.transitions' s' xs')"
    and "y # ys = trace.transitions' s xs ⟷ (∃a s' xs'. xs = (a, s') # xs' ∧ y = (a, s, s') ∧ ys = trace.transitions' s' xs')"
by (case_tac [!] xs) auto

lemma inj_conv:
  shows "trace.transitions' s xs = trace.transitions' s ys ⟷ xs = ys"
by (induct xs arbitrary: s ys) (auto simp: trace.transitions'.eq_Nil_conv trace.transitions'.eq_Cons_conv)

lemma continue:
  shows "trace.transitions (σ @-⇩S xsv)
       = trace.transitions σ @ (case trace.term σ of None ⇒ trace.transitions' (trace.final σ) (fst xsv) | Some v ⇒ [])"
by (simp add: trace.transitions'.append last_map trace.final'_def split: option.splits)

lemma idle_conv:
  shows "set (trace.transitions' s xs) ⊆ UNIV × Id ⟷ snd ` set xs ⊆ {s}"
by (induct xs arbitrary: s) (simp; fast)+

lemma map:
  shows "trace.transitions' (sf s) (map (map_prod af sf) xs)
       = map (map_prod af (map_prod sf sf)) (trace.transitions' s xs)"
by (induct xs arbitrary: s) simp_all

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "transitions"›

lemma monotone:
  shows "monotone (≤) prefix trace.transitions"
by (rule monotoneI) (metis prefix_order.eq_iff trace.less_eqE trace.transitions'.prefix_conv)

lemmas mono = monotoneD[OF trace.transitions.monotone]

lemma subseq:
 assumes "σ ≤ σ'"
 shows "subseq (trace.transitions σ) (trace.transitions σ')"
by (rule prefix_imp_subseq[OF trace.transitions.mono[OF assms]])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

type_synonym ('a, 's) steps = "('a × 's × 's) set"

setup ‹Sign.mandatory_path "trace"›

definition steps' :: "'s ⇒ ('a × 's) list ⇒ ('a, 's) steps" where
  "steps' s xs = set (trace.transitions' s xs) - UNIV × Id"

abbreviation (input) steps :: "('a, 's, 'v) trace.t ⇒ ('a, 's) steps" where
  "steps σ ≡ trace.steps' (trace.init σ) (trace.rest σ)"

setup ‹Sign.mandatory_path "steps'"›

lemma simps[simp]:
  shows "trace.steps' s [] = {}"
    and "trace.steps' s ((a, s) # xs) = trace.steps' s xs"
    and "s ≠ snd x ⟹ trace.steps' s (x # xs) = insert (fst x, s, snd x) (trace.steps' (snd x) xs)"
    and "(a, s', s') ∉ trace.steps' s xs"
    and "snd ` set xs ⊆ {s} ⟹ trace.steps' s xs = {}"
    and "trace.steps' s [x] = (if s = snd x then {} else {(fst x, s, snd x)})"
by (simp_all add: trace.steps'_def insert_Diff_if trace.transitions'.idle_conv)

lemma Cons_eq_if:
  shows "trace.steps' s (x # xs)
      = (if s = snd x then trace.steps' s xs else insert (fst x, s, snd x) (trace.steps' (snd x) xs))"
by (auto simp: trace.steps'_def)

lemma stuttering:
  shows "trace.steps' s xs ⊆ r ∪ A × Id ⟷ trace.steps' s xs ⊆ r"
    and "trace.steps' s xs ⊆ A × Id ∪ r ⟷ trace.steps' s xs ⊆ r"
by (auto simp: trace.steps'_def)

lemma empty_conv[simp]:
  shows "trace.steps' s xs = {} ⟷ snd ` set xs ⊆ {s}" (is ?thesis1)
    and "{} = trace.steps' s xs ⟷ snd ` set xs ⊆ {s}" (is ?thesis2)
proof -
  show ?thesis1 by (simp add: trace.steps'_def trace.transitions'.idle_conv)
  then show ?thesis2
    by (rule eq_commute_conv)
qed

lemma append:
  shows "trace.steps' s (xs @ ys)
       = trace.steps' s xs ∪ trace.steps' (trace.final' s xs) ys"
by (simp add: trace.steps'_def trace.transitions'.append Un_Diff)

lemma map:
  shows "trace.steps' (sf s) (map (map_prod af sf) xs) = map_prod af (map_prod sf sf) ` trace.steps' s xs - UNIV × Id"
    and "trace.steps' s (map (map_prod af id) xs) = map_prod af id ` trace.steps' s xs - UNIV × Id"
by (force simp: trace.steps'_def trace.transitions'.map trace.transitions'.map[where sf=id, simplified])+

lemma memberD:
  assumes "(a, s, s') ∈ trace.steps' s⇩0 xs"
  shows "(a, s') ∈ set xs"
using assms by (induct xs arbitrary: s⇩0) (auto simp: trace.steps'.Cons_eq_if split: if_split_asm)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "steps"›

lemma monotone:
  shows "mono trace.steps"
by (simp add: monoI trace.steps'_def Diff_mono set_subseq[OF trace.transitions.subseq])

lemmas mono = monoD[OF trace.steps.monotone]
lemmas strengthen[strg] = st_monotone[OF trace.steps.monotone]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "aset"›

lemma simps:
  shows "trace.aset (trace.T s xs v) = fst ` set xs"
by (force simp: trace.t.set)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "sset"›

lemma simps:
  shows "trace.sset (trace.T s xs v) = insert s (snd ` set xs)"
by (fastforce simp: trace.t.set image_iff)

lemma dropn_le:
  assumes "trace.dropn i σ = Some σ'"
  shows "trace.sset σ' ⊆ trace.sset σ"
using assms
by (cases σ; cases σ')
   (fastforce simp: trace.dropn_alt_def trace.sset.simps image_iff
             split: list.split_asm
              dest: arg_cong[where f=set] in_set_dropD)

lemma take_le:
  shows "trace.sset (trace.take i σ) ⊆ trace.sset σ"
by (cases σ) (auto simp: trace.take_def trace.sset.simps dest: in_set_takeD)

lemma mono:
  shows "mono trace.sset"
by (rule monoI, unfold trace.less_eq_take_def)
   (blast dest: subsetD[OF trace.sset.take_le])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Behaviors\label{sec:aczel_sequences-behaviors} ›

setup ‹Sign.mandatory_path "behavior"›

datatype (aset: 'a, sset: 's, vset: 'v) t =
  B (init: 's) (rest: "('a × 's, 'v) tllist")
for
  map: map

definition "term" :: "('a, 's, 'v) behavior.t ⇒ 'v option" where
  "term ω = (if tfinite (behavior.rest ω) then Some (terminal (behavior.rest ω)) else None)"

declare behavior.t.map_id0[simp]
declare behavior.t.map_id0[unfolded id_def, simp]
declare behavior.t.map_sel[simp]
declare behavior.t.set_map[simp]
declare behavior.t.map_comp[unfolded o_def, simp]
declare behavior.t.set[simp del]

lemma split_all[no_atp]: ―‹ imitate the setup for \<^typ>‹'a × 'b› without the automation ›
  shows "(⋀x. PROP P x) ≡ (⋀s xs. PROP P (behavior.B s xs))"
proof
  show "PROP P (behavior.B s xs)" if "⋀x. PROP P x" for s xs by (rule that)
next
  fix x
  assume "⋀s xs. PROP P (behavior.B s xs)"
  from ‹PROP P (behavior.B (behavior.init x) (behavior.rest x))› show "PROP P x" by simp
qed

lemma split_All[no_atp]:
  shows "(∀x. P x) ⟷ (∀s xs. P (behavior.B s xs))" (is "?lhs ⟷ ?rhs")
proof (intro iffI allI)
  fix x assume ?rhs then show "P x" by (cases x) simp_all
qed simp

lemma split_Ex[no_atp]:
  shows "(∃x. P x) ⟷ (∃s xs. P (behavior.B s xs))" (is "?lhs ⟷ ?rhs")
proof (intro iffI allI; elim exE)
  fix x assume "P x" then show "∃s xs. P (behavior.B s xs)" by (cases x) fast
qed auto


subsection‹ Combinators on behaviors\label{sec:aczel_sequences-behaviors-combinators} ›

definition continue :: "('a, 's, 'v) trace.t ⇒ ('a × 's, 'v) tllist ⇒ ('a, 's, 'v) behavior.t" (infix ‹@-⇩B› 64) where
  "σ @-⇩B xs = behavior.B (trace.init σ) (tshift2 (trace.rest σ, trace.term σ) xs)"

definition tl :: "('a, 's, 'v) behavior.t ⇀ ('a, 's, 'v) behavior.t" where
  "tl ω = (case behavior.rest ω of TNil v ⇒ None | TCons x xs ⇒ Some (behavior.B (snd x) xs))"

definition dropn :: "nat ⇒ ('a, 's, 'v) behavior.t ⇀ ('a, 's, 'v) behavior.t" where
  "dropn = (^^) behavior.tl"

definition take :: "nat ⇒ ('a, 's, 'v) behavior.t ⇒ ('a, 's, 'v) trace.t" where
  "take i ω = uncurry (trace.T (behavior.init ω)) (ttake i (behavior.rest ω))"

setup ‹Sign.mandatory_path "continue"›

lemma simps:
  shows "trace.T s xs None @-⇩B ys = behavior.B s (tshift xs ys)"
    and "trace.T s xs (Some v) @-⇩B ys = behavior.B s (tshift xs (TNil v))"
    and "trace.T s (x # xs) w @-⇩B ys = behavior.B s (TCons x (tshift2 (xs, w) ys))"
by (simp_all add: behavior.continue_def)

lemma sel[simp]:
  shows init: "behavior.init (σ @-⇩B xs) = trace.init σ"
    and rest: "behavior.rest (σ @-⇩B xs) = tshift2 (trace.rest σ, trace.term σ) xs"
by (simp_all add: behavior.continue_def)

lemma term_None:
  assumes "trace.term σ = None"
  shows "σ @-⇩B xs = behavior.B (trace.init σ) (tshift (trace.rest σ) xs)"
by (simp add: assms behavior.continue_def)

lemma term_Some:
  assumes "trace.term σ = Some v"
  shows "σ @-⇩B xs = behavior.B (trace.init σ) (tshift (trace.rest σ) (TNil v))"
by (simp add: assms behavior.continue_def)

lemma tshift2:
  shows "σ @-⇩B tshift2 xsv ys = (σ @-⇩S xsv) @-⇩B ys"
by (simp add: behavior.continue_def tshift2_def tshift_append split: option.split)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "tl"›

lemma TNil:
  shows "behavior.tl (behavior.B s (TNil v)) = None"
by (simp add: behavior.tl_def)

lemma TCons:
  shows "behavior.tl (behavior.B s (TCons x xs)) = Some (behavior.B (snd x) xs)"
by (simp add: behavior.tl_def)

lemma eq_None_conv:
  shows "behavior.tl ω = None ⟷ is_TNil (behavior.rest ω)"
by (simp add: behavior.tl_def split: tllist.split)

lemma continue_Cons:
  shows "behavior.tl (trace.T s (x # xs) v @-⇩B ys) = Some (trace.T (snd x) xs v @-⇩B ys)"
by (simp add: behavior.tl_def behavior.continue_def)

lemmas simps[simp] =
  behavior.tl.TNil
  behavior.tl.TCons
  behavior.tl.eq_None_conv
  behavior.tl.continue_Cons

lemma tfiniteD:
  assumes "behavior.tl ω = Some ω'"
  shows "tfinite (behavior.rest ω') ⟷ tfinite (behavior.rest ω)"
using assms by (auto simp: behavior.tl_def split: tllist.splits)

setup ‹Sign.parent_path›

lemma dropn_alt_def:
  shows "behavior.dropn i ω
       = (case tdropn i (TCons (undefined, behavior.init ω) (behavior.rest ω)) of
           TNil _ ⇒ None
         | TCons x xs ⇒ Some (behavior.B (snd x) xs))"
proof(induct i arbitrary: ω)
  case 0 show ?case by (simp add: behavior.dropn_def)
next
  case (Suc i ω) then show ?case
    by (cases ω; cases "behavior.rest ω"; cases i;
        simp add: behavior.dropn_def tdropn_eq_TNil_conv tdropn_tlength split: tllist.splits)
qed

setup ‹Sign.mandatory_path "dropn"›

lemma simps[simp]:
  shows 0: "behavior.dropn 0 ω = Some ω"
    and TNil: "behavior.dropn i (behavior.B s (TNil v)) = (case i of 0 ⇒ Some (behavior.B s (TNil v)) | _ ⇒ None)"
by (simp_all add: behavior.dropn_def split: nat.splits)

lemma TCons:
  shows "behavior.dropn i (behavior.B s (TCons x xs))
      = (case i of 0 ⇒ Some (behavior.B s (TCons x xs)) | Suc j ⇒ behavior.dropn j (behavior.B (snd x) xs))"
by (simp add: behavior.dropn_def split: nat.splits)

lemma Suc:
  shows "behavior.dropn (Suc i) ω = Option.bind (behavior.tl ω) (behavior.dropn i)"
by (simp_all add: behavior.dropn_def)

lemma bind_tl_commute:
  shows "behavior.tl ω ⤜ behavior.dropn i = behavior.dropn i ω ⤜ behavior.tl"
by (simp add: behavior.dropn_def pfunpow_swap1)

lemma Suc_right:
  shows "behavior.dropn (Suc i) ω = Option.bind (behavior.dropn i ω) behavior.tl"
by (simp add: behavior.dropn_def pfunpow_Suc_right del: pfunpow.simps)

lemma dropn:
  shows "Option.bind (behavior.dropn i ω) (behavior.dropn j) = behavior.dropn (i + j) ω"
by (simp add: behavior.dropn_def pfunpow_add)

lemma add:
  shows "behavior.dropn (i + j) = (λω. Option.bind (behavior.dropn i ω) (behavior.dropn j))"
by (simp add: fun_eq_iff behavior.dropn.dropn)

lemma tfiniteD:
  assumes "behavior.dropn i ω = Some ω'"
  shows "tfinite (behavior.rest ω') ⟷ tfinite (behavior.rest ω)"
using assms
by (induct i arbitrary: ω')
   (auto simp: behavior.dropn.Suc_right behavior.tl.tfiniteD split: bind_split_asm)

lemma shorterD:
  assumes "behavior.dropn i ω = Some ω'"
  assumes "j ≤ i"
  shows "∃ω''. behavior.dropn j ω = Some ω''"
using assms(1) le_Suc_ex[OF assms(2)]
by (clarsimp simp flip: behavior.dropn.dropn split: Option.bind_split_asm)

lemma eq_None_tlength_conv:
  shows "behavior.dropn i ω = None ⟷ tlength (behavior.rest ω) < enat i"
proof(induct i arbitrary: ω)
  case 0 show ?case by (simp add: enat_0)
next
  case (Suc i) then show ?case
    by (cases ω; cases "behavior.rest ω"; simp add: behavior.dropn.Suc enat_0_iff flip: eSuc_enat)
qed

lemma eq_Some_tlength_conv:
  shows "(∃ω'. behavior.dropn i ω = Some ω') ⟷ enat i ≤ tlength (behavior.rest ω)"
by (metis behavior.dropn.eq_None_tlength_conv leD leI not_None_eq2)

lemma eq_Some_tlengthD:
  assumes "behavior.dropn i ω = Some ω'"
  shows "enat i ≤ tlength (behavior.rest ω)"
using assms behavior.dropn.eq_Some_tlength_conv by blast

lemma tlength_eq_SomeD:
  assumes "enat i ≤ tlength (behavior.rest ω)"
  shows "∃ω'. behavior.dropn i ω = Some ω'"
using assms behavior.dropn.eq_Some_tlength_conv by blast

lemma eq_Some_tdropnD:
  assumes "behavior.dropn i ω = Some ω'"
  shows "tdropn i (behavior.rest ω) = behavior.rest ω'"
using assms
proof(induct i arbitrary: ω)
  case (Suc i) then show ?case
    by (cases ω; cases "behavior.rest ω"; fastforce simp: behavior.dropn.Suc)
qed simp

lemma continue_shorter:
  assumes "i ≤ length (trace.rest σ)"
  shows "behavior.dropn i (σ @-⇩B xs) = Option.bind (trace.dropn i σ) (λσ'. Some (σ' @-⇩B xs))"
using assms
proof(induct i arbitrary: σ)
  case (Suc i σ) from Suc.prems show ?case
    by (cases σ; cases "trace.rest σ")
       (simp_all add: behavior.dropn.Suc flip: Suc.hyps)
qed simp

lemma continue_Some:
  assumes "length (trace.rest σ) < i"
  assumes "trace.term σ = Some v"
  shows "behavior.dropn i (σ @-⇩B xs) = None"
using assms by (simp add: behavior.dropn.eq_None_tlength_conv tlength_tshift2 tlength_tshift)

lemma continue_None:
  assumes "length (trace.rest σ) < i"
  assumes "trace.term σ = None"
  shows "behavior.dropn i (σ @-⇩B xs)
       = (case tdropn (i - Suc (length (trace.rest σ))) xs of
           TNil _ ⇒ None
         | TCons y ys ⇒ Some (behavior.B (snd y) ys))"
using assms by (cases i) (auto simp: behavior.dropn_alt_def tdropn_tshift)

lemma continue:
  shows "behavior.dropn i (σ @-⇩B xs)
       = (if i ≤ length (trace.rest σ)
            then Option.bind (trace.dropn i σ) (λσ'. Some (σ' @-⇩B xs))
            else if trace.term σ = None
                 then case tdropn (i - Suc (length (trace.rest σ))) xs of
                        TNil _ ⇒ None
                      | TCons y ys ⇒ Some (behavior.B (snd y) ys)
                 else None)"
by (clarsimp simp: behavior.dropn.continue_None behavior.dropn.continue_Some
                   behavior.dropn.continue_shorter)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "trace.take.behavior"›

lemma take:
  shows "trace.take i (behavior.take j ω) = behavior.take (min i j) ω"
by (simp add: behavior.take_def trace.take_def split_def
              ttake_eq_None_conv ttake_flat length_ttake take_fst_ttake
       split: enat.split split_min)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "behavior"›

setup ‹Sign.mandatory_path "take"›

lemma simps[simp]:
  shows 0: "behavior.take 0 ω = trace.T (behavior.init ω) [] None"
    and Suc_TNil: "behavior.take (Suc i) (behavior.B s (TNil v)) = trace.T s [] (Some v)"
by (simp_all add: behavior.take_def)

lemma sel[simp]:
  shows "trace.init (behavior.take i ω) = behavior.init ω"
    and "trace.rest (behavior.take i ω) = fst (ttake i (behavior.rest ω))"
    and "trace.term (behavior.take i ω) = snd (ttake i (behavior.rest ω))"
by (simp_all add: behavior.take_def split_def)

lemma monotone:
  shows "mono (λi. behavior.take i ω)"
by (rule monoI) (fastforce simp: trace.less_eq_take_def trace.take.behavior.take min_def)

lemmas mono = monoD[OF behavior.take.monotone]

lemma map:
  shows "behavior.take i (behavior.map af sf vf ω) = trace.map af sf vf (behavior.take i ω)"
by (induct i arbitrary: ω) (simp_all add: behavior.take_def split_def ttake_tmap split: tllist.split)

lemma continue:
  shows "behavior.take i (σ @-⇩B ω) = trace.take i σ @-⇩S ttake (i - length (trace.rest σ)) ω"
by (cases σ)
   (auto simp: behavior.take_def split_def trace.take_def ttake_tshift2 ttake_TNil
        split: option.split nat.split)

lemma all_continue:
  assumes "tlength (behavior.rest ω) < enat i"
  shows "behavior.take i ω @-⇩S xsv = behavior.take i ω"
using assms
by (auto simp: behavior.take_def split_def trace.continue_def ttake_eq_None_conv
        split: option.split)

lemma continue_same:
  shows "behavior.take i (behavior.take i ω @-⇩B xsv) = behavior.take i ω"
by (auto simp: behavior.take_def split_def ttake_tshift2 length_ttake
               ttake_eq_None_conv ttake_eq_Nil_conv ttake_eq_Some_conv ttake_TNil
        split: enat.split nat.split option.split)

lemma treplicate:
  shows "behavior.take i (behavior.B s (treplicate j as v))
       = trace.T s (List.replicate (min i j) as) (if j < i then Some v else None)"
by (simp add: behavior.take_def)

lemma trepeat:
  shows "behavior.take i (behavior.B s (trepeat as)) = trace.T s (List.replicate i as) None"
by (simp add: behavior.take_def ttake_trepeat)

lemma tshift:
  shows "behavior.take i (behavior.B s (tshift xs ys)) = trace.take i (trace.T s xs None) @-⇩S ttake (i - length xs) ys"
by (simp add: behavior.take_def trace.take_def ttake_tshift split_def)

lemma length:
  shows "length (trace.rest (behavior.take j ω))
       = (case tlength (behavior.rest ω) of enat i ⇒ min i j | ∞ ⇒ j)"
by (auto simp: length_ttake split: enat.split)

lemma add:
  shows "behavior.take (i + j) ω
       = behavior.take i ω @-⇩S (case behavior.dropn i ω of Some ω' ⇒ ttake j (behavior.rest ω'))"
by (auto simp: behavior.take_def split_def ttake_add Let_def behavior.dropn.eq_Some_tdropnD
               behavior.dropn.eq_None_tlength_conv
         dest: iffD1[OF ttake_eq_None_conv(1)]
        split: option.split)

lemma term_Some_conv:
  shows "trace.term (behavior.take j ω) = Some v
    ⟷ (tlength (behavior.rest ω) < enat j ∧ Some v = behavior.term ω)"
by (auto simp: behavior.term_def ttake_eq_Some_conv tfinite_tlength_conv)

lemma dropn:
  assumes "behavior.dropn i ω = Some ω'"
  shows "behavior.take j ω' = the (trace.dropn i (behavior.take (i + j) ω))"
using assms
proof(induct i arbitrary: j ω ω')
  case (Suc i j ω) then show ?case
    by (cases ω; cases "behavior.rest ω"; cases i)
       (auto simp: behavior.dropn.Suc behavior.take_def split_def)
qed simp

lemma continue_id:
  assumes "tlength (behavior.rest ω) < enat i"
  shows "behavior.take i ω @-⇩B xs = ω"
using assms by (simp add: behavior.continue_def tshift2_ttake_shorter)

lemma flat:
  assumes "tlength (behavior.rest ω) < enat i"
  assumes "i ≤ j"
  shows "behavior.take i ω = behavior.take j ω"
using assms by (simp add: behavior.take_def ttake_flat)

lemma eqI:
  assumes "⋀i. behavior.take i ω⇩1 = behavior.take i ω⇩2"
  shows "ω⇩1 = ω⇩2"
using assms
by (cases ω⇩1; cases ω⇩2; simp add: behavior.take_def case_prod_beta prod_eq_iff ttake_eq_imp_eq)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "continue"›

lemma take_drop_shorter:
  assumes "i ≤ j"
  shows "behavior.take i ω @-⇩S apfst (drop i) (ttake j (behavior.rest ω)) = behavior.take j ω"
using assms
by (simp add: trace.continue_def behavior.take.flat ttake_eq_None_conv ttake_eq_Some_conv trace.t.expand
        flip: take_fst_ttake[where i=i and j=j, simplified min_absorb1[OF assms]]
       split: option.split)

lemma take_drop_id:
  shows "behavior.take i ω @-⇩B behavior.rest (the (behavior.dropn i ω)) = ω"
by (cases "tlength (behavior.rest ω) < enat i")
   (simp add: behavior.take.continue_id,
    simp add: behavior.continue_def tshift2_ttake_tdropn_id behavior.dropn.tlength_eq_SomeD
        flip: behavior.dropn.eq_Some_tdropnD)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "aset"›

lemma simps:
  shows "behavior.aset (behavior.B s xs) = fst ` tset xs"
by (force simp: behavior.t.set)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "sset"›

lemma simps:
  shows "behavior.sset (behavior.B s xs) = insert s (snd ` tset xs)"
by (fastforce simp: behavior.t.set image_iff)

lemma dropn_le:
  assumes "behavior.dropn i ω = Some ω'"
  shows "behavior.sset ω' ⊆ behavior.sset ω"
using assms
by (cases ω; cases ω')
   (fastforce simp: behavior.dropn_alt_def behavior.sset.simps image_iff
             split: tllist.split_asm
              dest: arg_cong[where f=tset] in_tset_tdropnD)

lemma take_le:
  shows "trace.sset (behavior.take i ω) ⊆ behavior.sset ω"
by (cases ω)
   (auto simp: behavior.take_def behavior.sset.simps trace.sset.simps split_def
         dest: in_set_ttakeD)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "trace.dropn.behavior"›

lemma take:
  shows "trace.dropn i (behavior.take j ω)
       = (if i ≤ j then Option.bind (behavior.dropn i ω) (λω'. Some (behavior.take (j - i) ω'))
                    else None)"
proof(cases "i ≤ j")
  case False then show ?thesis
    by (clarsimp simp: trace.dropn.eq_none_length_conv length_ttake split: enat.split) linarith
next
  case True then show ?thesis
  proof(induct j arbitrary: i ω)
    case (Suc j i ω) then show ?case
      by (cases ω; cases i)
         (auto simp: behavior.dropn.Suc behavior.take_def split_def behavior.split_all
              split: tllist.splits)
  qed simp
qed

setup ‹Sign.parent_path›
(*<*)

end
(*>*)