# Theory ListSlice

(*  Title:      ListSlice.thy
Date:       Oct 2006
Author:     David Trachtenherz
*)

section ‹Additional definitions and results for lists›

theory ListSlice
imports "List-Infinite.ListInf"
begin

subsection ‹Slicing lists into lists of lists›

definition ilist_slice  :: "'a ilist ⇒ nat ⇒ 'a list ilist"
where "ilist_slice f k ≡ λx. map f [x * k..<Suc x * k]"

primrec list_slice_aux :: "'a list ⇒ nat ⇒ nat ⇒ 'a list list"
where
"list_slice_aux xs k 0 = []"
| "list_slice_aux xs k (Suc n) = take k xs # list_slice_aux (xs ↑ k) k n"

definition list_slice :: "'a list ⇒ nat ⇒ 'a list list"
where "list_slice xs k ≡ list_slice_aux xs k (length xs div k)"

definition list_slice2 :: "'a list ⇒ nat ⇒ 'a list list"
where "list_slice2 xs k ≡
list_slice xs k @ (if length xs mod k = 0 then [] else [xs ↑ (length xs div k * k)])"

text ‹
No function ‹list_unslice› for finite lists is needed
because the corresponding functionality is already provided by ‹concat›.
Therefore, only a ‹ilist_unslice› function for infinite lists is defined.›

definition ilist_unslice  :: "'a list ilist ⇒ 'a ilist"
where "ilist_unslice f ≡ λn. f (n div length (f 0)) ! (n mod length (f 0))"

lemma list_slice_aux_length: "⋀xs. length (list_slice_aux xs k n) = n"
by (induct n, simp+)

lemma list_slice_aux_nth: "
⋀m xs. m < n ⟹ (list_slice_aux xs k n) ! m = (xs ↑ (m * k) ↓ k)"
apply (induct n)
apply simp
apply (simp add: nth_Cons' diff_mult_distrib)
done

lemma list_slice_length: "length (list_slice xs k) = length xs div k"
by (simp add: list_slice_def list_slice_aux_length)

lemma list_slice_0: "list_slice xs 0 = []"
by (simp add: list_slice_def)

lemma list_slice_1: "list_slice xs (Suc 0) = map (λx. [x]) xs"
by (fastforce simp: list_eq_iff list_slice_def list_slice_aux_nth list_slice_aux_length)

lemma list_slice_less: "length xs < k ⟹ list_slice xs k = []"
by (simp add: list_slice_def)

lemma list_slice_Nil: "list_slice [] k = []"
by (simp add: list_slice_def)

lemma list_slice_nth: "
m < length xs div k ⟹ list_slice xs k ! m = xs ↑ (m * k) ↓ k"
by (simp add: list_slice_def list_slice_aux_nth)

lemma list_slice_nth_length: "
m < length xs div k ⟹ length ((list_slice xs k) ! m) = k"
apply (case_tac "length xs < k")
apply simp
apply (simp add: list_slice_nth)
apply simp
done

lemma list_slice_nth_eq_sublist_list: "
m < length xs div k ⟹ list_slice xs k ! m = sublist_list xs [m * k..<m * k + k]"
apply (simp add: list_slice_nth)
apply (rule take_drop_eq_sublist_list)
apply (rule less_div_imp_mult_add_divisor_le, assumption+)
done

lemma list_slice_nth_nth: "
⟦ m < length xs div k; n < k ⟧ ⟹
(list_slice xs k) ! m ! n = xs ! (m * k + n)"
apply (frule list_slice_nth_length[of m xs k])
apply (simp add: list_slice_nth)
done

lemma list_slice_nth_nth_rev: "
n < length xs div k * k ⟹
(list_slice xs k) ! (n div k) ! (n mod k) = xs ! n"
apply (case_tac "k = 0", simp)
apply (simp add: list_slice_nth_nth div_less_conv)
done

lemma list_slice_eq_list_slice_take: "
list_slice (xs ↓ (length xs div k * k)) k = list_slice xs k"
apply (case_tac "k = 0")
apply (simp add: list_slice_0)
apply (simp add: list_eq_iff list_slice_length)
apply (simp add: div_mult_le min_eqR list_slice_nth)
apply (clarify, rename_tac i)
apply (subgoal_tac "k ≤ length xs div k * k - i * k")
prefer 2
apply (drule_tac m=i in Suc_leI)
apply (drule mult_le_mono1[of _ _ k])
apply simp
apply (subgoal_tac "length xs div k * k - i * k ≤ length xs - i * k")
prefer 2
apply (simp add: div_mult_cancel)
apply (simp add: min_eqR)
by (simp add: less_diff_conv)

lemma list_slice_append_mult: "
⋀xs. length xs = m * k ⟹
list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k"
apply (case_tac "k = 0")
apply (simp add: list_slice_0)
apply (induct m)
apply (simp add: list_slice_Nil)
apply (simp add: list_slice_def)
done

lemma list_slice_append_mod: "
length xs mod k = 0 ⟹
list_slice (xs @ ys) k = list_slice xs k @ list_slice ys k"
by (auto intro: list_slice_append_mult elim!: dvdE)

lemma list_slice_div_eq_1[rule_format]: "
length xs div k = Suc 0 ⟹ list_slice xs k = [take k xs]"
by (simp add: list_slice_def)

lemma list_slice_div_eq_Suc[rule_format]: "
length xs div k = Suc n ⟹
list_slice xs k = list_slice (xs ↓ (n * k)) k @ [xs ↑ (n * k) ↓ k]"
apply (case_tac "k = 0", simp)
apply (subgoal_tac "n * k < length xs")
prefer 2
apply (case_tac "length xs = 0", simp)
apply (drule_tac arg_cong[where f="λx. x - Suc 0"], drule sym)
apply (simp add: diff_mult_distrib div_mult_cancel)
apply (insert list_slice_append_mult[of "take (n * k) xs" n k "drop (n * k) xs"])
apply (simp add: min_eqR)
apply (rule list_slice_div_eq_1)
apply (simp add: div_diff_mult_self1)
done

lemma list_slice2_mod_0: "
length xs mod k = 0 ⟹ list_slice2 xs k = list_slice xs k"
by (simp add: list_slice2_def)

lemma list_slice2_mod_gr0: "
0 < length xs mod k ⟹ list_slice2 xs k = list_slice xs k @ [xs ↑ (length xs div k * k)]"
by (simp add: list_slice2_def)

lemma list_slice2_length: "
length (list_slice2 xs k) = (
if length xs mod k = 0 then length xs div k else Suc (length xs div k))"
by (simp add: list_slice2_def list_slice_length)

lemma list_slice2_0: "
list_slice2 xs 0 = (if (length xs = 0) then [] else [xs])"
by (simp add: list_slice2_def list_slice_0)

lemma list_slice2_1: "list_slice2 xs (Suc 0) = map (λx. [x]) xs"
by (simp add: list_slice2_def list_slice_1)

lemma list_slice2_le: "
length xs ≤ k ⟹ list_slice2 xs k = (if length xs = 0 then [] else [xs])"
apply (case_tac "k = 0")
apply (simp add: list_slice2_0)
apply (drule order_le_less[THEN iffD1], erule disjE)
apply (simp add: list_slice2_def list_slice_def)
apply (simp add: list_slice2_def list_slice_div_eq_1)
done

lemma list_slice2_Nil: "list_slice2 [] k = []"
by (simp add: list_slice2_def list_slice_Nil)

lemma list_slice2_list_slice_nth: "
m < length xs div k ⟹ list_slice2 xs k ! m = list_slice xs k ! m"
by (simp add: list_slice2_def list_slice_length nth_append)

lemma list_slice2_last: "
⟦ length xs mod k > 0; m = length xs div k ⟧ ⟹
list_slice2 xs k ! m = xs ↑ (length xs div k * k)"
by (simp add: list_slice2_def nth_append list_slice_length)

lemma list_slice2_nth: "
⟦ m < length xs div k ⟧ ⟹
list_slice2 xs k ! m = xs ↑ (m * k) ↓ k"
by (simp add: list_slice2_def list_slice_length nth_append list_slice_nth)

lemma list_slice2_nth_length_eq1: "
m < length xs div k ⟹ length (list_slice2 xs k ! m) = k"
by (simp add: list_slice2_def nth_append list_slice_length list_slice_nth_length)

lemma list_slice2_nth_length_eq2: "
⟦ length xs mod k > 0; m = length xs div k ⟧ ⟹
length (list_slice2 xs k ! m) = length xs mod k"
by (simp add: list_slice2_def list_slice_length nth_append minus_div_mult_eq_mod [symmetric])

lemma list_slice2_nth_nth_eq1: "
⟦ m < length xs div k; n < k ⟧ ⟹
(list_slice2 xs k) ! m ! n = xs ! (m * k + n)"
by (simp add: list_slice2_list_slice_nth list_slice_nth_nth)

lemma list_slice2_nth_nth_eq2: "
⟦ m = length xs div k; n < length xs mod k ⟧ ⟹
(list_slice2 xs k) ! m ! n = xs ! (m * k + n)"
by (simp add: mult.commute[of _ k] minus_mod_eq_mult_div [symmetric] list_slice2_last)

lemma list_slice2_nth_nth_rev: "
n < length xs ⟹ (list_slice2 xs k) ! (n div k) ! (n mod k) = xs ! n"
apply (case_tac "k = 0")
apply (clarsimp simp: list_slice2_0)
apply (case_tac "n div k < length xs div k")
apply (simp add: list_slice2_nth_nth_eq1)
apply (frule div_le_mono[OF less_imp_le, of _ _ k])
apply simp
apply (drule sym)
apply (subgoal_tac "n mod k < length xs mod k")
prefer 2
apply (rule ccontr)
apply (simp add: linorder_not_less)
apply (drule less_mod_ge_imp_div_less[of n "length xs" k], simp+)
apply (simp add: list_slice2_nth_nth_eq2)
done

lemma list_slice2_append_mult: "
length xs = m * k ⟹
list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k"
apply (case_tac "k = 0")
apply (simp add: list_slice2_0)
apply (clarsimp simp: list_slice2_def list_slice_append_mult)
done

lemma list_slice2_append_mod: "
length xs mod k = 0 ⟹
list_slice2 (xs @ ys) k = list_slice2 xs k @ list_slice2 ys k"
by (auto intro: list_slice2_append_mult elim!: dvdE)

lemma ilist_slice_nth: "
(ilist_slice f k) m = map f [m * k..<Suc m * k]"
by (simp add: ilist_slice_def)

lemma ilist_slice_nth_length: "length ((ilist_slice f k) m) = k"
by (simp add: ilist_slice_def)

lemma ilist_slice_nth_nth: "
n < k ⟹ (ilist_slice f k) m ! n = f (m * k + n)"
by (simp add: ilist_slice_def)

lemma ilist_slice_nth_nth_rev: "
0 < k ⟹ (ilist_slice f k) (n div k) ! (n mod k) = f n"
by (simp add: ilist_slice_nth_nth)

lemma list_slice_concat: "
concat (list_slice xs k) = xs ↓ (length xs div k * k)"
(is "?P xs k")
apply (case_tac "k = 0")
apply (simp add: list_slice_0)
apply simp
apply (subgoal_tac "⋀m. ∀xs. length xs div k = m ⟶ ?P xs k", simp)
apply (induct_tac m)
apply (intro allI impI)
apply (simp add: in_set_conv_nth div_eq_0_conv' list_slice_less)
apply clarify
apply (subgoal_tac "n * k + k ≤ length xs")
prefer 2
apply (simp add: le_less_div_conv[symmetric])
apply (simp add: list_slice_div_eq_Suc)
apply (drule_tac x="xs ↓ (n * k)" in spec)
apply (simp add: min_eqR)
done

lemma list_slice_unslice_mult: "
length xs = m * k ⟹ concat (list_slice xs k) = xs"
apply (case_tac "k = 0")
apply (simp add: list_slice_Nil)
apply (simp add: list_slice_concat)
done

lemma ilist_slice_unslice: "0 < k ⟹ ilist_unslice (ilist_slice f k) = f"
by (simp add: ilist_unslice_def ilist_slice_nth_length ilist_slice_nth_nth)

lemma i_take_ilist_slice_eq_list_slice: "
0 < k ⟹ ilist_slice f k ⇓ n = list_slice (f ⇓ (n * k)) k"
apply (simp add: list_eq_iff list_slice_length ilist_slice_nth list_slice_nth)
apply (clarify, rename_tac i)
apply (subgoal_tac "k ≤ n * k - i * k")
prefer 2
apply (drule_tac m=i in Suc_leI)
apply (drule mult_le_mono1[of _ _ k])
apply simp
apply simp
done

lemma list_slice_i_take_eq_i_take_ilist_slice: "
list_slice (f ⇓ n) k = ilist_slice f k ⇓ (n div k)"
apply (case_tac "k = 0")
apply (simp add: list_slice_0)
apply (simp add: i_take_ilist_slice_eq_list_slice)
apply (subst list_slice_eq_list_slice_take[of "f ⇓ n", symmetric])
apply (simp add: div_mult_le min_eqR)
done

lemma ilist_slice_i_append_mod: "
length xs mod k = 0 ⟹
ilist_slice (xs ⌢ f) k = list_slice xs k ⌢ ilist_slice f k"
apply (simp add: ilist_eq_iff ilist_slice_nth i_append_nth list_slice_length)
apply (clarsimp simp: mult.commute[of k] elim!: dvdE, rename_tac n i)
apply (intro conjI impI)
apply (simp add: list_slice_nth)
apply (subgoal_tac "k ≤ n * k - i * k")
prefer 2
apply (drule_tac m=i in Suc_leI)
apply (drule mult_le_mono1[of _ _ k])
apply simp
apply (fastforce simp: list_eq_iff i_append_nth min_eqR)
apply (simp add: ilist_eq_iff list_eq_iff i_append_nth linorder_not_less)
apply (clarify, rename_tac j)
apply (subgoal_tac "n * k ≤ i * k + j")
prefer 2
apply (simp add: diff_mult_distrib)
done

corollary ilist_slice_append_mult: "
length xs = m * k ⟹
ilist_slice (xs ⌢ f) k = list_slice xs k ⌢ ilist_slice f k"
by (simp add: ilist_slice_i_append_mod)

end


# Theory AF_Stream

(*  Title:      AF_Stream.thy
Date:       Jan 2007
Author:     David Trachtenherz
*)

section ‹\textsc{AutoFocus} message streams›

theory AF_Stream
imports ListSlice
begin

subsection ‹Basic definitions›

subsubsection ‹Time-synchronous streams›

datatype 'a message_af = NoMsg | Msg 'a

notation (latex)
NoMsg  ("\<NoMsg>") and
Msg  ("\<Msg>")

text ‹Abbreviation for finite streams›
type_synonym 'a fstream_af = "'a message_af list"

text ‹Abbreviation for infinite streams›
type_synonym 'a istream_af = "'a message_af ilist"

lemma not_NoMsg_eq: "(m ≠ \<NoMsg>) = (∃x. m = \<Msg> x)"
by (case_tac m, simp_all)

lemma not_Msg_eq: "(∀x. m ≠ \<Msg> x) = (m = \<NoMsg>) "
by (case_tac m, simp_all)

primrec the_af :: "'a message_af ⇒ 'a"
where "the_af (\<Msg> x) = x"

text ‹
By this definition one can determine,
whether data elements of different data structures with messages,
especially product types of arbitrary sizes and records,
are pointwise equal to NoMsg, i.e., contain only NoMsg entries.›

consts is_NoMsg :: "'a ⇒ bool"

overloading is_NoMsg ≡ "is_NoMsg :: 'a message_af ⇒ bool"
begin

primrec is_NoMsg :: "'a message_af ⇒ bool"
where
"is_NoMsg \<NoMsg> = True"
| "is_NoMsg (\<Msg> x) = False"

end

overloading is_NoMsg ≡ "is_NoMsg :: ('a × 'b) ⇒ bool"
begin

definition is_NoMsg_tuple_def  :
"is_NoMsg (p::'a × 'b) ≡ (is_NoMsg (fst p) ∧ is_NoMsg (snd p))"

end

overloading is_NoMsg ≡ "is_NoMsg :: 'a set ⇒ bool"
begin

definition is_NoMsg_set_def :
"is_NoMsg (A::'a set) ≡ (∀x∈A. is_NoMsg x)"

end

record SomeRecordExample =
Field1 :: "nat message_af"
Field2 :: "int message_af"
Field3 :: "int message_af"
overloading is_NoMsg ≡ "is_NoMsg :: 'a SomeRecordExample_scheme ⇒ bool"
begin

definition is_NoMsg_SomeRecordExample_def :
"is_NoMsg (r:: 'a SomeRecordExample_scheme) ≡
Field1 r = \<NoMsg> ∧ Field2 r = \<NoMsg> ∧ Field3 r = \<NoMsg>"

end

definition is_Msg :: "'a ⇒ bool"
where "is_Msg x ≡ (¬ is_NoMsg x)"

lemma is_NoMsg_message_af_conv: "is_NoMsg m = (case m of \<NoMsg> ⇒ True | \<Msg> x ⇒ False)"
by (case_tac m, simp+)

lemma is_NoMsg_message_af_conv2: "is_NoMsg m = (m = \<NoMsg>)"
by (case_tac m, simp+)

lemma is_Msg_message_af_conv: "is_Msg m = (case m of \<NoMsg> ⇒ False | \<Msg> x ⇒ True)"
by (unfold is_Msg_def, case_tac m, simp+)

lemma is_Msg_message_af_conv2: "is_Msg m = (m ≠ \<NoMsg>)"
by (unfold is_Msg_def, case_tac m, simp+)

text ‹Collection for definitions for ‹is_NoMsg›.›

named_theorems is_NoMsg_defs

declare
is_NoMsg_tuple_def[is_NoMsg_defs]
is_NoMsg_set_def [is_NoMsg_defs]
is_NoMsg_SomeRecordExample_def[is_NoMsg_defs]
is_Msg_def[is_NoMsg_defs]

lemma not_is_NoMsg: "(¬ is_NoMsg m) = is_Msg m"
by (simp add: is_NoMsg_defs)

lemma not_is_Msg: "(¬ is_Msg m) = is_NoMsg m"
by (simp add: is_NoMsg_defs)

lemma "is_NoMsg (\<NoMsg>::(nat message_af))"
by simp

lemma "is_NoMsg (\<NoMsg>::(nat message_af), \<NoMsg>::(nat message_af))"
by (simp add: is_NoMsg_defs)

lemma "is_NoMsg (\<NoMsg>::(nat message_af), \<NoMsg>::(nat message_af), \<NoMsg>::(nat message_af))"
by (simp add: is_NoMsg_defs)

lemma "is_Msg (\<NoMsg>::(nat message_af), \<Msg> (1::nat), \<NoMsg>::(nat message_af))"
by (simp add: is_NoMsg_defs)

lemma "is_NoMsg {\<NoMsg>::(nat message_af), \<NoMsg>}"
by (simp add: is_NoMsg_defs)

lemma "is_Msg {\<NoMsg>::(nat message_af), \<Msg> 1}"
by (simp add: is_NoMsg_defs)

lemma "is_NoMsg ⦇ Field1 = \<NoMsg>, Field2 = \<NoMsg>, Field3 = \<NoMsg> ⦈"
by (simp add: is_NoMsg_defs)

lemma "is_Msg  ⦇ Field1 = \<NoMsg>, Field2 = Msg 1, Field3 = \<NoMsg> ⦈"
by (simp add: is_NoMsg_defs)

subsubsection ‹Time abstraction›

(* Time abstraction:
Extracts non-empty messages from a stream =
time abstraction for time-synchronous streams*)
primrec untime :: "'a fstream_af ⇒ 'a list" (*("®_" 100)*)
where
"untime [] = []"
| "untime (x#xs) =
(if x = \<NoMsg>
then (untime xs)
else (the_af x) # (untime xs))"

lemma untime_eq_filter[rule_format]: "
map (λx. \<Msg> x) (untime s) = filter (λx. x ≠ \<NoMsg>) s"
apply (induct s, simp)
apply (case_tac a, simp_all)
done

text ‹The following lemma involves @{term the_af} function
and thus is some more limited than the previous lemma›
corollary untime_eq_filter2[rule_format]: "
untime s = map (λx. the_af x) (filter (λx. x ≠ \<NoMsg>) s)"
by (induct s, simp_all)

definition untime_length :: "'a fstream_af ⇒ nat"
where "untime_length s ≡ length (untime s)"

primrec untime_length_cnt :: "'a fstream_af ⇒ nat"
where
"untime_length_cnt [] = 0"
| "untime_length_cnt (x # xs) =
(if x = \<NoMsg> then 0 else Suc 0) + untime_length_cnt xs"

lemma untime_length_eq_untime_length_cnt: "
untime_length s = untime_length_cnt s"
by (induct s, simp_all add: untime_length_def)

definition untime_length_filter :: "'a fstream_af ⇒ nat"
where "untime_length_filter s ≡ length (filter (λx. x ≠ \<NoMsg>) s)"

lemma untime_length_filter_eq_untime_length: "
untime_length_filter s = untime_length s"
apply (unfold untime_length_def untime_length_filter_def)
apply (simp add: untime_eq_filter2)
done

lemma untime_empty_conv: "(untime s = []) = (∀n<length s. s ! n = \<NoMsg>)"
apply (induct s)
apply simp
apply (force simp add: nth.simps split: nat.split)
done

lemma untime_not_empty_conv: "(untime s ≠ []) = (∃n<length s. s ! n ≠ \<NoMsg>)"
by (simp add: untime_empty_conv)

corollary untime_empty_imp_NoMsg[rule_format]: "
⟦ untime s = []; n < length s ⟧ ⟹ s ! n = \<NoMsg>"
by (rule untime_empty_conv[THEN iffD1, rule_format])

lemma untime_nth_eq_filter: "
n < untime_length s ⟹
\<Msg> (untime s ! n) = (filter (λx. x ≠ \<NoMsg>) s) ! n"
by (simp add: untime_eq_filter[symmetric] untime_length_def)

corollary untime_nth_eq_filter2: "
n < untime_length s ⟹
untime s ! n = the_af ((filter (λx. x ≠ \<NoMsg>) s) ! n)"
by (simp add: untime_length_def untime_nth_eq_filter[symmetric])

lemma untime_hd_eq_filter_hd: "
untime s ≠ [] ⟹
\<Msg> (hd (untime s)) = hd (filter (λx. x ≠ \<NoMsg>) s)"
by (simp add: untime_eq_filter[symmetric] hd_eq_first[symmetric])

corollary untime_hd_eq_filter_hd2: "
untime s ≠ [] ⟹
hd (untime s) = the_af (hd (filter (λx. x ≠ \<NoMsg>) s))"
by (simp add: untime_hd_eq_filter_hd[symmetric])

lemma untime_last_eq_filter_last: "
untime s ≠ [] ⟹
\<Msg> (last (untime s)) = last (filter (λx. x ≠ \<NoMsg>) s)"
by (simp add: untime_eq_filter[symmetric] last_nth)

corollary untime_last_eq_filter_last2: "
untime s ≠ [] ⟹
last (untime s) = the_af (last (filter (λx. x ≠ \<NoMsg>) s))"
by (simp add: untime_last_eq_filter_last[symmetric])

subsection ‹Expanding and compressing lists and streams›

subsubsection ‹Expanding message streams›

primrec f_expand :: "'a fstream_af ⇒ nat ⇒ 'a fstream_af" (infixl "⊙⇩f" 100)
where
f_expand_Nil: "[] ⊙⇩f k = []"
| f_expand_Cons: "(x # xs) ⊙⇩f k =
(if 0 < k then x # \<NoMsg>⇗k - Suc 0⇖ @ (xs ⊙⇩f k) else [])"

definition i_expand :: "'a istream_af ⇒ nat ⇒ 'a istream_af" (infixl "⊙⇩i" 100)
where
"i_expand ≡ λf k n.
(if k = 0 then \<NoMsg> else
if n mod k = 0 then f (n div k) else \<NoMsg>)"

primrec f_expand_Suc :: "'a fstream_af ⇒ nat ⇒ 'a fstream_af" (infixl "⊙⇘fSuc⇙" 100)
where
"f_expand_Suc [] k = []"
| "f_expand_Suc (x # xs) k = x # \<NoMsg>⇗k⇖ @ (f_expand_Suc xs k)"

definition i_expand_Suc :: "'a istream_af ⇒ nat ⇒ 'a istream_af" (infixl "⊙⇘iSuc⇙" 100)
where "i_expand_Suc ≡ λf k n. if n mod (Suc k) = 0 then f (n div (Suc k)) else \<NoMsg>"

notation
f_expand  (infixl "⊙" 100) and
i_expand  (infixl "⊙" 100)

lemma length_f_expand_Suc[simp]: "length (f_expand_Suc xs k) = length xs * Suc k"
by (induct xs, simp+)

lemma i_expand_if: "
f ⊙⇩i k = (if k = 0 then (λn. \<NoMsg>) else
(λn. if n mod k = 0 then f (n div k) else \<NoMsg>))"
by (simp add: i_expand_def ilist_eq_iff)

lemma f_expand_one: "0 < k ⟹ [a] ⊙⇩f k = a # \<NoMsg>⇗k - Suc 0⇖"
by simp

lemma f_expand_0[simp]: "xs ⊙⇩f 0 = []"
by (induct xs, simp+)
corollary f_expand_0_is_zero_element: "xs ⊙⇩f 0 = ys ⊙⇩f 0"
by simp
lemma i_expand_0[simp]: "f ⊙⇩i 0 = (λn. \<NoMsg>)"
by (simp add: i_expand_def)
corollary i_expand_0_is_zero_element: "f ⊙⇩i 0 = g ⊙⇩i 0"
by simp

lemma f_expand_gr0_f_expand_Suc: "0 < k ⟹ xs ⊙⇩f k = f_expand_Suc xs (k - Suc 0)"
by (induct xs, simp+)
lemma i_expand_gr0_i_expand_Suc: "0 < k ⟹ f ⊙⇩i k = i_expand_Suc f (k - Suc 0)"
by (simp add: i_expand_def i_expand_Suc_def ilist_eq_iff)
lemma i_expand_gr0: "
0 < k ⟹ f ⊙⇩i k = (λn. if n mod k = 0 then f (n div k) else \<NoMsg>)"
by (simp add: i_expand_if)
lemma f_expand_1[simp]: "xs ⊙⇩f Suc 0 = xs"
by (induct xs, simp+)
lemma i_expand_1[simp]: "f ⊙⇩i Suc 0 = f"
by (simp add: i_expand_gr0)

lemma f_expand_length[simp]: "length (xs ⊙⇩f k) = length xs * k"
apply (case_tac k, simp)
apply (simp add: f_expand_gr0_f_expand_Suc)
done

lemma f_expand_empty_conv: "(xs ⊙⇩f k = []) = (xs = [] ∨ k = 0)"
by (simp add: length_0_conv[symmetric] del: length_0_conv)
lemma f_expand_not_empty_conv: "(xs ⊙⇩f k ≠ []) = (xs ≠ [] ∧ 0 < k)"
by (simp add: f_expand_empty_conv)

lemma f_expand_Cons: "
0 < k ⟹ (x # xs) ⊙⇩f k = x # \<NoMsg>⇗k - Suc 0⇖ @ (xs ⊙⇩f k)"
by simp
lemma f_expand_append[simp]: "⋀ys. (xs @ ys) ⊙⇩f k = (xs ⊙⇩f k) @ (ys ⊙⇩f k)"
apply (case_tac "k = 0", simp)
apply (induct xs, simp+)
done

lemma f_expand_snoc: "
0 < k ⟹ (xs @ [x]) ⊙⇩f k = xs ⊙⇩f k @ x # replicate (k - Suc 0) \<NoMsg>"
by simp

lemma f_expand_nth_mult: "⋀n.
⟦ n < length xs; 0 < k ⟧ ⟹ (xs ⊙⇩f k) ! (n * k) = xs ! n"
apply (induct xs)
apply simp
apply (case_tac n, simp)
apply (simp add: nth_append append_Cons[symmetric] del: append_Cons)
done

lemma i_expand_nth_mult: "0 < k ⟹ (f ⊙⇩i k) (n * k) = f n"
by (simp add: i_expand_gr0)

lemma f_expand_nth_if: "⋀n.
n < length xs * k ⟹
(xs ⊙⇩f k) ! n = (if n mod k = 0 then xs ! (n div k) else \<NoMsg>)"
apply (case_tac "k = 0", simp)
apply (simp, intro conjI impI)
apply (clarsimp simp: f_expand_nth_mult mult.commute[of k] elim!: dvdE)
apply (induct xs, simp)
apply (simp add: nth_append append_Cons[symmetric] del: append_Cons)
apply (intro conjI impI)
apply (simp add: nth_Cons')
apply (case_tac "length xs = 0", simp)
apply (simp add: add.commute[of k] diff_less_conv[symmetric] mod_diff_self2)
done

corollary f_expand_nth_mod_eq_0: "
⟦ n < length xs * k; n mod k = 0 ⟧ ⟹ (xs ⊙⇩f k) ! n = xs ! (n div k)"
by (simp add: f_expand_nth_if)

corollary f_expand_nth_mod_neq_0: "
⟦ n < length xs * k; 0 < n mod k ⟧ ⟹ (xs ⊙⇩f k) ! n = \<NoMsg>"
by (simp add: f_expand_nth_if)

lemma f_expand_nth_0_upto_k_minus_1_if: "
⟦ t < length xs; n = t * k + i; i < k ⟧ ⟹
(xs ⊙⇩f k) ! n = (if i = 0 then xs ! t else \<NoMsg>)"
apply (subst f_expand_nth_if)
apply (drule Suc_leI[of t])
apply (drule mult_le_mono1[of _ _ k])
apply simp+
done

lemma f_expand_take_mult: "xs ⊙⇩f k ↓ (n * k) = (xs ↓ n) ⊙⇩f k"
apply (clarsimp simp add: list_eq_iff min_def)
apply (rename_tac i)
apply (case_tac "¬ i < n * k", simp)
apply (subgoal_tac "i < length xs * k")
prefer 2
apply (rule_tac y="n * k" in order_le_less_trans, simp+)
apply (clarsimp simp: f_expand_nth_if elim!: dvdE)
done

lemma f_expand_take_mod: "
n mod k = 0 ⟹ xs ⊙⇩f k ↓ n = xs ↓ (n div k) ⊙⇩f k"
by (clarsimp simp: mult.commute[of k] f_expand_take_mult elim!: dvdE)

lemma f_expand_drop_mult: "xs ⊙⇩f k ↑ (n * k) = (xs ↑ n) ⊙⇩f k"
apply (insert arg_cong[OF append_take_drop_id, of "λx. x ⊙⇩f k" n xs])
apply (drule ssubst[OF append_take_drop_id, of _ "xs ⊙⇩f k" "n * k"])
apply (simp only: f_expand_append)
apply (simp only: f_expand_take_mult)
apply simp
done

lemma f_expand_drop_mod: "
n mod k = 0 ⟹ xs ⊙⇩f k ↑ n = xs ↑ (n div k) ⊙⇩f k"
by (clarsimp simp: mult.commute[of k] f_expand_drop_mult elim!: dvdE)

lemma f_expand_take_mult_Suc: "
⟦ n < length xs; i < k ⟧ ⟹
xs ⊙⇩f k ↓ (n * k + Suc i) = (xs ↓ n) ⊙⇩f k @ (xs ! n # \<NoMsg>⇗i⇖)"
apply (subgoal_tac "n * k + Suc i ≤ length xs * k")
prefer 2
apply (drule Suc_leI[of n])
apply (drule mult_le_mono1[of "Suc n" _ k])
apply simp
apply (clarsimp simp: list_eq_iff min_eqR nth_append f_expand_nth_if min_def nth_Cons' elim!: dvdE)
apply (simp add: mult.commute[of k] linorder_not_less)
apply (drule_tac n=ka in le_neq_implies_less, simp+)
apply (drule_tac n=ka in Suc_leI)
apply (drule_tac j=ka in mult_le_mono1[of _ _ k])
apply simp
done

lemma f_expand_take_Suc: "
n < length xs * k ⟹
xs ⊙⇩f k ↓ Suc n = (xs ↓ (n div k)) ⊙⇩f k @ (xs ! (n div k) # \<NoMsg>⇗n mod k⇖)"
apply (case_tac "k = 0", simp)
apply (insert f_expand_take_mult_Suc[of "n div k" xs "n mod k" k])
apply (simp add: div_less_conv)
done

lemma i_expand_nth_if: "
0 < k ⟹ (f ⊙⇩i k) n = (if n mod k = 0 then f (n div k) else \<NoMsg>)"
by (simp add: i_expand_gr0)
corollary i_expand_nth_mod_eq_0: "
⟦ 0 < k; n mod k = 0 ⟧ ⟹ (f ⊙⇩i k) n = f (n div k)"
by (simp add: i_expand_gr0)
corollary i_expand_nth_mod_neq_0: "
0 < n mod k ⟹ (f ⊙⇩i k) n = \<NoMsg>"
apply (case_tac "k = 0", simp)
apply (simp add: i_expand_gr0)
done

lemma i_expand_nth_0_upto_k_minus_1_if: "
⟦ n = t * k + i; i < k ⟧ ⟹
(f ⊙⇩i k) n = (if i = 0 then f t else \<NoMsg>)"
by (simp add: i_expand_nth_if)

lemma i_expand_i_take_mult: "f ⊙⇩i k ⇓ (n * k) = (f ⇓ n) ⊙⇩f k"
apply (case_tac "k = 0", simp)
apply (clarsimp simp: list_eq_iff i_expand_nth_if f_expand_nth_if elim!: dvdE)
done

lemma i_expand_i_take_mod: "
n mod k = 0 ⟹ f ⊙⇩i k ⇓ n = f ⇓ (n div k) ⊙⇩f k"
by (clarsimp simp: mult.commute[of k] i_expand_i_take_mult elim!: dvdE)

lemma i_expand_i_drop_mult: "(f ⊙⇩i k) ⇑ (n * k) = (f ⇑ n) ⊙⇩i k"
apply (case_tac "k = 0", simp)
apply (clarsimp simp: ilist_eq_iff i_expand_nth_if)
done

lemma i_expand_i_drop_mod: "
n mod k = 0 ⟹ f ⊙⇩i k ⇑ n = f ⇑ (n div k) ⊙⇩i k"
by (clarsimp simp: mult.commute[of k] i_expand_i_drop_mult elim!: dvdE)

lemma i_expand_i_take_mult_Suc: "
i < k ⟹ f ⊙⇩i k ⇓ (n * k + Suc i) = (f ⇓ n) ⊙⇩f k @ (f n # \<NoMsg>⇗i⇖)"
apply (clarsimp simp: list_eq_iff, rename_tac i')
apply (clarsimp simp: i_expand_nth_if f_expand_nth_if nth_append nth_Cons' elim!: dvdE)
apply (simp add: linorder_not_less mult.commute[of k])
apply (drule_tac n=ka in le_neq_implies_less, simp+)
apply (drule_tac n=ka in Suc_leI)
apply (drule_tac j=ka in mult_le_mono1[of _ _ k])
apply simp
done

lemma i_expand_i_take_Suc: "
0 < k ⟹ f ⊙⇩i k ⇓ Suc n = (f ⇓ (n div k)) ⊙⇩f k @ (f (n div k) # \<NoMsg>⇗n mod k⇖)"
apply (insert i_expand_i_take_mult_Suc[of "n mod k" k "n div k" f])
apply simp
done

lemma f_expand_nth_interval_eq_nth_append_replicate_NoMsg[rule_format]: "
⟦ 0 < k; t < length xs; t * k ≤ t1; t1 ≤ t * k + k - Suc 0 ⟧ ⟹
xs ⊙⇩f k ↓ Suc t1 ↑ (t * k) = xs ! t # \<NoMsg>⇗t1 - t * k⇖"
apply (rule_tac t="Suc t1" and s="t * k + Suc (t1 - t * k)" in subst, simp)
apply (subst f_expand_take_mult_Suc)
apply simp+
done

lemma f_expand_nth_interval_eq_replicate_NoMsg: "
⟦ 0 < k; t * k < t1; t1 ≤ t2; t2 ≤ t * k + k; t2 ≤ length xs * k⟧ ⟹
xs ⊙⇩f k ↓ t2 ↑ t1 = \<NoMsg>⇗t2 - t1⇖"
apply (clarsimp simp: list_eq_iff min_eqR f_expand_nth_if elim!: dvdE, rename_tac i q)
apply (drule_tac i=i and k=t1 in add_less_mono2, simp)
apply (drule_tac i="t * k" and j=t1 and m=i in trans_less_add1)
apply (drule_tac x="t * k" and y="t1 + i" and m=k in less_mod_eq_imp_add_divisor_le, simp)
apply simp
done

lemma i_expand_nth_interval_eq_nth_append_replicate_NoMsg[rule_format]: "
⟦ 0 < k; t * k ≤ t1; t1 ≤ t * k + k - Suc 0 ⟧ ⟹
f ⊙⇩i k ⇓ Suc t1 ↑ (t * k) = f t # \<NoMsg>⇗t1 - t * k⇖"
by (simp add: list_eq_iff Suc_diff_le i_expand_nth_if nth_Cons')

lemma i_expand_nth_interval_eq_replicate_NoMsg: "
⟦ 0 < k; t * k < t1; t1 ≤ t2; t2 ≤ t * k + k ⟧ ⟹
f ⊙⇩i k ⇓ t2 ↑ t1 = \<NoMsg>⇗t2 - t1⇖"
apply (clarsimp simp: list_eq_iff i_expand_nth_if add.commute[of k])
apply (drule_tac i=i and k=t1 in add_less_mono2, simp)
apply (drule_tac i="t * k" and j=t1 and m=i in trans_less_add1)
apply (drule_tac x="t * k" and y="t1 + i" and m=k in less_mod_eq_imp_add_divisor_le, simp)
apply simp
done

lemma f_expand_replicate_NoMsg[simp]: "(\<NoMsg>⇗n⇖) ⊙⇩f k =  \<NoMsg>⇗n * k⇖"
by (clarsimp simp: list_eq_iff f_expand_nth_if elim!: dvdE)

lemma i_expand_const_NoMsg[simp]: "(λn. \<NoMsg>) ⊙⇩i k = (λn. \<NoMsg>)"
by (simp add: i_expand_def ilist_eq_iff)

lemma f_expand_assoc: "xs ⊙⇩f a ⊙⇩f b = xs ⊙⇩f (a * b)"
apply (induct xs)
apply simp
done

lemma i_expand_assoc: "f ⊙⇩i a ⊙⇩i b = f ⊙⇩i (a * b)"
by (fastforce simp: i_expand_def ilist_eq_iff)

lemma f_expand_commute: "xs ⊙⇩f a ⊙⇩f b = xs ⊙⇩f b ⊙⇩f a"
by (simp add: f_expand_assoc mult.commute[of b])

lemma i_expand_commute: "f ⊙⇩i a ⊙⇩i b = f ⊙⇩i b ⊙⇩i a"
by (simp add: i_expand_assoc mult.commute[of b])

lemma i_expand_i_append: "(xs ⌢ f) ⊙⇩i k = xs ⊙⇩f k ⌢ (f ⊙⇩i k)"
apply (case_tac "k = 0", simp)
apply (clarsimp simp add: ilist_eq_iff i_expand_gr0 i_append_nth)
apply (case_tac "x < length xs * k")
apply (frule_tac n=x and k="length xs" in div_less_conv[THEN iffD2, of k, rule_format], simp)
apply (simp add: f_expand_nth_if)
apply (simp add: linorder_not_less)
apply (frule div_le_mono[of _ _ k])
apply (simp add: mod_diff_mult_self1 div_diff_mult_self1)
done

lemma f_expand_eq_conv: "
0 < k ⟹ (xs ⊙⇩f k = ys ⊙⇩f k) = (xs = ys)"
apply (rule iffI)
apply (clarsimp simp: list_eq_iff, rename_tac i)
apply (drule_tac x="i * k" in spec)
apply (simp add: f_expand_nth_mult)
apply simp
done

lemma i_expand_eq_conv: "
0 < k ⟹ (f ⊙⇩i k = g ⊙⇩i k) = (f = g)"
apply (rule iffI)
apply (clarsimp simp: ilist_eq_iff, rename_tac i)
apply (drule_tac x="i * k" in spec)
apply (simp add: i_expand_nth_mult)
apply simp
done

lemma f_expand_eq_conv': "
(xs' ⊙⇩f k = xs) =
(length xs' * k = length xs ∧
(∀i<length xs. xs ! i = (if i mod k = 0 then xs' ! (i div k) else \<NoMsg>)))"
by (fastforce simp: list_eq_iff f_expand_nth_if)

lemma i_expand_eq_conv': "
0 < k ⟹ (f' ⊙⇩i k = f) =
(∀i. f i = (if i mod k = 0 then f' (i div k) else \<NoMsg>))"
by (fastforce simp: ilist_eq_iff i_expand_nth_if)

subsubsection ‹Aggregating lists›

definition f_aggregate :: "'a list ⇒ nat ⇒ ('a list ⇒ 'a) ⇒ 'a list"
where "f_aggregate s k ag ≡ map ag (list_slice s k)"

definition i_aggregate :: "'a ilist ⇒ nat ⇒ ('a list ⇒ 'a) ⇒ 'a ilist"
where "i_aggregate s k ag ≡ λn. ag (s ⇑ (n * k) ⇓ k)"

lemma f_aggregate_0[simp]: "f_aggregate xs 0 ag = []"
by (simp add: f_aggregate_def list_slice_0)

lemma f_aggregate_1: "
(⋀x. ag [x] = x) ⟹
f_aggregate xs (Suc 0) ag = xs"
by (simp add: list_eq_iff f_aggregate_def list_slice_1)

lemma f_aggregate_Nil[simp]: "f_aggregate [] k ag = []"
by (simp add: f_aggregate_def list_slice_Nil)

lemma f_aggregate_length[simp]: "length (f_aggregate xs k ag) = length xs div k"
by (simp add: f_aggregate_def list_slice_length)

lemma f_aggregate_empty_conv: "
0 < k ⟹ (f_aggregate xs k ag = []) = (length xs < k)"
by (simp add: length_0_conv[symmetric] div_eq_0_conv' del: length_0_conv )

lemma f_aggregate_one: "
⟦ 0 < k; length xs = k ⟧ ⟹ f_aggregate xs k ag = [ag xs]"
by (simp add: f_aggregate_def list_slice_def)

lemma f_aggregate_Cons: "
⟦ 0 < k; length xs = k ⟧ ⟹
f_aggregate (xs @ ys) k ag = ag xs # (f_aggregate ys k ag)"
by (simp add: f_aggregate_def list_slice_def)

lemma f_aggregate_eq_f_aggregate_take: "
f_aggregate (xs ↓ (length xs div k * k)) k ag = f_aggregate xs k ag"
by (simp add: f_aggregate_def list_slice_eq_list_slice_take)

lemma f_aggregate_nth: "
n < length xs div k ⟹
(f_aggregate xs k ag) ! n = ag (xs ↑ (n * k) ↓ k)"
by (simp add: f_aggregate_def list_slice_length list_slice_nth)

lemma f_aggregate_nth_eq_sublist_list: "
n < length xs div k ⟹
(f_aggregate xs k ag) ! n = ag (sublist_list xs [n * k..<n * k + k])"
apply (simp add: f_aggregate_nth take_drop_eq_sublist_list)
done

lemma f_aggregate_take_nth: "
⋀xs m. ⟦ n < length xs div k; n < m div k ⟧ ⟹
f_aggregate (xs ↓ m) k ag ! n = f_aggregate xs k ag ! n"
apply (simp add: f_aggregate_nth drop_take)
apply (drule_tac n=m in less_div_imp_mult_add_divisor_le)
apply (simp add: min_eqL)
done

lemma f_aggregate_hd: "
⟦ 0 < k; k ≤ length xs ⟧ ⟹
hd (f_aggregate xs k ag) = ag (xs ↓ k)"
apply (drule div_le_mono[of _ _ k])
apply (simp add: Suc_le_eq)
apply (subst hd_eq_first[symmetric])
apply (simp add: length_greater_0_conv[symmetric])
apply (simp add: f_aggregate_nth)
done

lemma f_aggregate_append_mod: "
length xs mod k = 0 ⟹
f_aggregate (xs @ ys) k ag =
f_aggregate xs k ag @ f_aggregate ys k ag"
by (simp add: f_aggregate_def list_slice_append_mod)
lemma f_aggregate_append_mult: "
length xs = m * k ⟹
f_aggregate (xs @ ys) k ag =
f_aggregate xs k ag @ f_aggregate ys k ag"
by (simp add: f_aggregate_append_mod)

lemma f_aggregate_snoc: "
⟦ 0 < k; length ys = k; length xs mod k = 0 ⟧ ⟹
f_aggregate (xs @ ys) k ag = f_aggregate xs k ag @ [ag ys]"
by (simp add: f_aggregate_append_mod f_aggregate_one)

lemma f_aggregate_take: "
f_aggregate (xs ↓ n) k ag = f_aggregate xs k ag ↓ (n div k)"
apply (case_tac "k = 0", simp)
apply (simp add: list_eq_iff)
apply (case_tac "length xs ≤ n")
apply (simp add: min_eqL div_le_mono f_aggregate_nth)
apply (clarsimp simp: linorder_not_le min_eqR div_le_mono f_aggregate_nth drop_take)
apply (simp add: min_eqL)
apply (subgoal_tac "i < length xs div k")
prefer 2
apply (drule_tac y=n in order_le_less_trans, assumption)
apply (drule_tac m="i * k + k" and k=k in div_le_mono[OF less_imp_le])
apply simp
apply (simp add: f_aggregate_nth)
done

lemma f_aggregate_take_mult: "
f_aggregate (xs ↓ (n * k)) k ag = f_aggregate xs k ag ↓ n"
by (simp add: f_aggregate_take)

lemma f_aggregate_drop_mult: "
f_aggregate (xs ↑ (n * k)) k ag = f_aggregate xs k ag ↑ n"
by (simp add: list_eq_iff div_diff_mult_self1 f_aggregate_nth add_mult_distrib add.commute[of "n * k"])
lemma f_aggregate_drop_mod: "
n mod k = 0 ⟹ f_aggregate (xs ↑ n) k ag = f_aggregate xs k ag ↑ (n div k)"
by (clarsimp simp: mult.commute[of k] f_aggregate_drop_mult elim!: dvdE)

lemma f_aggregate_assoc: "
(⋀xs. length xs mod a = 0 ⟹ ag (f_aggregate xs a ag) = ag xs) ⟹
f_aggregate (f_aggregate xs a ag) b ag = f_aggregate xs (a * b) ag"
apply (clarsimp simp add: list_eq_iff div_mult2_eq f_aggregate_nth, rename_tac i)
apply (simp add: take_drop f_aggregate_take_mult[symmetric])
apply (simp add: add_mult_distrib2 mult.commute[of _ a] f_aggregate_drop_mult[symmetric] mult.assoc[symmetric])
apply (drule_tac x="(xs ↓ (a * b + a * i * b) ↑ (a * i * b))" in meta_spec)
apply (subgoal_tac "a * b + a * i * b ≤ length xs")
prefer 2
apply (simp add: div_mult2_eq[symmetric])
apply (drule_tac x=i in less_div_imp_mult_add_divisor_le)
apply (simp add: mult.assoc[symmetric] mult.commute[of _ a] add.commute[of _ "a * b"])
apply (simp add: min_eqR)
done

lemma f_aggregate_commute: "
⟦ ⋀xs. length xs mod a = 0 ⟹ ag (f_aggregate xs a ag) = ag xs;
⋀xs. length xs mod b = 0 ⟹ ag (f_aggregate xs b ag) = ag xs ⟧ ⟹
f_aggregate (f_aggregate xs a ag) b ag = f_aggregate (f_aggregate xs b ag) a ag"
by (simp add: f_aggregate_assoc mult.commute[of _ b])

lemma i_aggregate_0[simp]: "i_aggregate f 0 ag = (λx. ag [])"
by (simp add: i_aggregate_def)
lemma i_aggregate_1: "(⋀x. ag [x] = x) ⟹ i_aggregate f (Suc 0) ag = f"
by (simp add: i_aggregate_def i_take_first)
lemma i_aggregate_nth: "i_aggregate f k ag n = ag (f ⇑ (n * k) ⇓ k)"
by (simp add: i_aggregate_def)
lemma i_aggregate_hd: "i_aggregate f k ag 0 = ag (f ⇓ k)"
by (simp add: i_aggregate_nth)

lemma i_aggregate_nth_eq_map: "i_aggregate f k ag n = ag (map f [n * k..<n * k + k])"
by (simp add: i_aggregate_nth i_take_drop_eq_map)

lemma i_aggregate_i_append_mod: "
length xs mod k = 0 ⟹
i_aggregate (xs ⌢ f) k ag = f_aggregate xs k ag ⌢ i_aggregate f k ag"
apply (clarsimp simp: ilist_eq_iff i_aggregate_nth i_append_nth f_aggregate_nth mult.commute[of k] diff_mult_distrib elim!: dvdE, rename_tac i n)
apply (drule_tac n=i in Suc_leI)
apply (drule mult_le_mono1[of _ _ k])
apply simp
done

lemma i_aggregate_i_append_mult: "
length xs = m * k ⟹
i_aggregate (xs ⌢ f) k ag = f_aggregate xs k ag ⌢ i_aggregate f k ag"
by (rule i_aggregate_i_append_mod, simp)

lemma i_aggregate_Cons: "
⟦ 0 < k; length xs = k ⟧ ⟹
i_aggregate (xs ⌢ f) k ag = [ag xs] ⌢ (i_aggregate f k ag)"
apply (insert i_aggregate_i_append_mod[of xs k f ag], simp)
apply (simp add: f_aggregate_def list_slice_div_eq_1)
done

lemma i_aggregate_take_nth: "
n < m div k ⟹ f_aggregate (f ⇓ m) k ag ! n = i_aggregate f k ag n"
apply (simp add: f_aggregate_nth i_aggregate_nth)
apply (simp add: i_take_drop_map i_take_drop_eq_map take_map)
done

lemma i_aggregate_i_take: "
f_aggregate (f ⇓ n) k ag = i_aggregate f k ag ⇓ (n div k)"
by (simp add: list_eq_iff i_aggregate_take_nth)

lemma i_aggregate_i_take_mult: "
0 < k ⟹ f_aggregate (f ⇓ (n * k)) k ag = i_aggregate f k ag ⇓ n"
by (simp add: i_aggregate_i_take)

lemma i_aggregate_i_drop_mult: "
i_aggregate (f ⇑ (n * k)) k ag = i_aggregate f k ag ⇑ n"

lemma i_aggregate_i_drop_mod: "
n mod k = 0 ⟹
i_aggregate (f ⇑ n) k ag = i_aggregate f k ag ⇑ (n div k)"
by (clarsimp simp: mult.commute[of k] i_aggregate_i_drop_mult ilist_eq_iff elim!: dvdE)

lemma i_aggregate_assoc: "
⟦ 0 < a; 0 < b;
⋀xs. length xs mod a = 0 ⟹ ag (f_aggregate xs a ag) = ag xs ⟧ ⟹
i_aggregate (i_aggregate f a ag) b ag = i_aggregate f (a * b) ag"
apply (simp add: ilist_eq_iff i_aggregate_nth)
apply (simp add: i_aggregate_i_drop_mult[symmetric] i_aggregate_i_take_mult[symmetric] mult.commute[of a] mult.assoc)
done

lemma i_aggregate_commute: "
⟦ 0 < a; 0 < b;
⋀xs. length xs mod a = 0 ⟹ ag (f_aggregate xs a ag) = ag xs;
⋀xs. length xs mod b = 0 ⟹ ag (f_aggregate xs b ag) = ag xs ⟧ ⟹
i_aggregate (i_aggregate xs a ag) b ag = i_aggregate (i_aggregate xs b ag) a ag"
by (simp add: i_aggregate_assoc mult.commute[of _ b])

subsubsection ‹Compressing message streams›

text ‹Determines the last non-empty message.›
primrec last_message :: "'a fstream_af ⇒ 'a message_af"
where
"last_message [] = \<NoMsg>"
| "last_message (x # xs) = (if last_message xs = \<NoMsg> then x else last_message xs)"

definition f_shrink :: "'a fstream_af ⇒ nat ⇒ 'a fstream_af" (infixl "÷⇩f" 100)
where "f_shrink xs k ≡ f_aggregate xs k last_message"

definition i_shrink :: "'a istream_af ⇒ nat ⇒ 'a istream_af" (infixl "÷⇩i" 100)
where "i_shrink f k ≡ i_aggregate f k last_message"

notation
f_shrink  (infixl "÷" 100) and
i_shrink  (infixl "÷" 100)

lemmas f_shrink_defs = f_shrink_def f_aggregate_def
lemmas i_shrink_defs = i_shrink_def i_aggregate_def

lemma last_message_Nil: "last_message [] = \<NoMsg>"
by simp

lemma last_message_one: "last_message [m] = m"
by simp

lemma last_message_replicate: "0 < n ⟹ last_message (m⇗n⇖) = m"
apply (induct n, simp)
apply (case_tac n, simp+)
done

lemma last_message_replicate_NoMsg: "last_message (\<NoMsg>⇗n⇖) = \<NoMsg>"
apply (case_tac "n = 0", simp)
apply (simp add: last_message_replicate)
done

lemma last_message_Cons_NoMsg: "last_message (\<NoMsg> # xs) = last_message xs"
by simp

lemma last_message_append_one: "
last_message (xs @ [m]) = (if m = \<NoMsg> then last_message xs else m)"
apply (induct xs, simp)
apply (case_tac "m = \<NoMsg>", simp+)
done

lemma last_message_append: "⋀xs.
last_message (xs @ ys) = (
if last_message ys = \<NoMsg> then last_message xs else last_message ys)"
apply (induct ys, simp)
apply (drule_tac x="xs @ [a]" in meta_spec)
apply (simp add: last_message_append_one)
done

corollary last_message_append_replicate_NoMsg: "
last_message (xs @ \<NoMsg>⇗n⇖) = last_message xs"
by (simp add: last_message_append last_message_replicate_NoMsg)

lemma last_message_replicate_NoMsg_append: "
last_message (\<NoMsg>⇗n⇖ @ xs) = last_message xs"
by (simp add: last_message_append last_message_replicate_NoMsg)

lemma last_message_NoMsg_conv: "
(last_message xs = \<NoMsg>) = (∀i<length xs. xs ! i = \<NoMsg>)"
apply (induct xs, simp)
apply (simp add: nth_Cons')
apply (safe, simp_all)
apply (rename_tac i)
apply (drule_tac x="Suc i" in spec)
apply simp
done

lemma last_message_not_NoMsg_conv: "
(last_message xs ≠ \<NoMsg>) = (∃i<length xs. xs ! i ≠ \<NoMsg>)"
by (simp add: last_message_NoMsg_conv)

lemma not_NoMsg_imp_last_message: "
⟦ i < length xs; xs ! i ≠ \<NoMsg> ⟧ ⟹ last_message xs ≠ \<NoMsg>"
by (rule last_message_not_NoMsg_conv[THEN iffD2, OF exI, OF conjI])

lemma last_message_exists_nth: "
last_message xs ≠ \<NoMsg> ⟹
∃i<length xs. last_message xs = xs ! i ∧ (∀j<length xs. i < j ⟶ xs ! j = \<NoMsg>)"
apply (induct xs, simp)
apply (rename_tac a xs)
apply (case_tac "last_message xs = \<NoMsg>")
apply (rule_tac x=0 in exI)
apply clarsimp
apply (rename_tac j, case_tac j, simp)
apply (simp add: last_message_NoMsg_conv)
apply (rule ccontr)
apply (clarsimp, rename_tac i)
apply (drule_tac x="Suc i" in spec)
apply (clarsimp simp: nth_Cons')
done

lemma last_message_exists_nth': "
last_message xs ≠ \<NoMsg> ⟹ ∃i<length xs. last_message xs = xs ! i"
by (blast dest: last_message_exists_nth)

lemma last_messageI2_aux: "⋀i.
⟦ i < length xs; xs ! i ≠ \<NoMsg>;
∀j. i < j ∧ j < length xs ⟶ xs ! j = \<NoMsg> ⟧ ⟹
last_message xs = xs ! i"
apply (induct xs, simp)
apply (simp add: nth_Cons')
apply (case_tac i)
apply simp
apply (subgoal_tac "∀j. j < length xs ⟶ xs ! j = \<NoMsg>")
prefer 2
apply (clarify, drule_tac x="Suc j" in spec)
apply simp
apply (simp add: last_message_NoMsg_conv)
apply clarsimp
apply (rename_tac i)
apply (intro conjI impI)
apply (simp add: not_NoMsg_imp_last_message)
apply (subgoal_tac "∀j. i < j ∧ j < length xs ⟶ xs ! j = \<NoMsg>")
prefer 2
apply (clarify, drule_tac x="Suc j" in spec)
apply simp
apply simp
done

lemma last_messageI2: "
⟦ i < length xs; xs ! i ≠ \<NoMsg>;
⋀j. ⟦ i < j; j < length xs ⟧ ⟹ xs ! j = \<NoMsg> ⟧ ⟹
last_message xs = xs ! i"
by (blast intro: last_messageI2_aux)

lemma last_messageI: "
⟦ m ≠ \<NoMsg>; i < length xs; xs ! i = m;
⋀j. ⟦ i < j; j < length xs ⟧ ⟹ xs ! j = \<NoMsg> ⟧ ⟹
last_message xs = m"
by (blast intro: last_messageI2)

lemma last_message_Msg_eq_last: "
⟦ xs ≠ []; last xs ≠ \<NoMsg> ⟧ ⟹ last_message xs = last xs"
by (simp add: last_nth last_messageI2)

lemma last_message_conv: "
m ≠ \<NoMsg> ⟹
(last_message xs = m) =
(∃i<length xs. xs ! i = m ∧ (∀j<length xs. i < j ⟶ xs ! j = \<NoMsg>))"
apply (rule iffI)
apply (cut_tac xs=xs in last_message_exists_nth, simp)
apply clarify
apply (rule_tac x=i in exI)
apply simp
apply (clarsimp simp: last_messageI)
done

lemma last_message_conv_if: "
(last_message xs = m) =
(if m = \<NoMsg> then ∀i<length xs. xs ! i = \<NoMsg>
else ∃i<length xs. xs ! i = m ∧ (∀j<length xs. i < j ⟶ xs ! j = \<NoMsg>))"
by (simp add: last_message_NoMsg_conv last_message_conv)

lemma last_message_not_NoMsg_eq_conv: "
⟦ last_message xs ≠ \<NoMsg>; last_message ys ≠ \<NoMsg> ⟧ ⟹
(last_message xs = last_message ys) =
(∃i j. i < length xs ∧ j < length ys ∧ xs ! i ≠ \<NoMsg> ∧
xs ! i = ys ! j ∧
(∀n<length xs. i < n ⟶ xs ! n = \<NoMsg>) ∧
(∀n<length ys. j < n ⟶ ys ! n = \<NoMsg>))"
apply (simp add: last_message_conv[where m="last_message ys"])
apply (frule last_message_exists_nth[of xs])
apply (frule last_message_exists_nth[of ys])
apply (rule iffI)
apply (clarsimp, rename_tac i j)
apply (rule_tac x=j in exI, simp)
apply (rule_tac x=i in exI, simp)
apply (clarsimp, rename_tac i1 j1 i j)
apply (rule_tac x=i in exI, simp)
apply (subgoal_tac "last_message ys = ys ! j", simp)
apply (rule last_messageI2)
apply simp+
done

lemma f_shrink_0[simp]: "xs ÷⇩f 0 = []"
by (simp add: f_shrink_defs list_slice_0)

lemma f_shrink_1[simp]: "xs ÷⇩f Suc 0 = xs"
by (simp add: f_shrink_def f_aggregate_1)

lemma f_shrink_Nil[simp]: "[] ÷⇩f k = []"
by (simp add: f_shrink_def list_slice_Nil)

lemma f_shrink_length: "length (xs ÷⇩f k) = length xs div k"
by (simp add: f_shrink_def)

lemma f_shrink_empty_conv: "0 < k ⟹ (xs ÷⇩f k = []) = (length xs < k)"
by (simp add: f_shrink_def f_aggregate_empty_conv)

lemma f_shrink_Cons: "
⟦ 0 < k; length xs = k ⟧ ⟹ (xs @ ys) ÷⇩f k = last_message xs # (ys ÷⇩f k)"
by (simp add: f_shrink_def f_aggregate_Cons)

lemma f_shrink_one: "
⟦ 0 < k; length xs = k ⟧ ⟹ xs ÷⇩f k = [last_message xs]"
by (simp add: f_shrink_def f_aggregate_one)

lemma f_shrink_eq_f_shrink_take: "
xs ↓ (length xs div k * k) ÷⇩f k = xs ÷⇩f k"
by (simp add: f_shrink_defs list_slice_eq_list_slice_take)

lemma f_shrink_nth: "
n < length xs div k ⟹
(xs ÷⇩f k) ! n = last_message (xs ↑ (n * k) ↓ k)"
by (simp add: f_shrink_def f_aggregate_nth)

lemma f_shrink_nth_eq_sublist_list: "
n < length xs div k ⟹
(xs ÷⇩f k) ! n = last_message (sublist_list xs [n * k..<n * k + k])"
by (simp add: f_shrink_def f_aggregate_nth_eq_sublist_list)

lemma f_shrink_take_nth: "
⟦ n < length xs div k; n < m div k ⟧ ⟹ (xs ↓ m) ÷⇩f k ! n = xs ÷⇩f k ! n"
by (simp add: f_shrink_def f_aggregate_take_nth)

lemma f_shrink_hd: "
⟦ 0 < k; k ≤ length xs ⟧ ⟹ hd (xs ÷⇩f k) = last_message (xs ↓ k)"
by (simp add: f_shrink_def f_aggregate_hd)

lemma f_shrink_append_mod: "
length xs mod k = 0 ⟹ (xs @ ys) ÷⇩f k = xs ÷⇩f k @ (ys ÷⇩f k)"
by (simp add: f_shrink_defs list_slice_append_mod)

lemma f_shrink_append_mult: "
length xs = m * k ⟹ (xs @ ys) ÷⇩f k = xs ÷⇩f k @ (ys ÷⇩f k)"
by (simp add: f_shrink_append_mod)

lemma f_shrink_snoc: "
⟦ 0 < k; length ys = k; length xs mod k = 0 ⟧ ⟹
(xs @ ys) ÷⇩f k = xs ÷⇩f k @ [last_message ys]"
by (simp add: f_shrink_append_mod f_shrink_one)

lemma f_shrink_last_message[rule_format]: "
length xs mod k = 0 ⟶ last_message (xs ÷⇩f k) = last_message xs"
apply (case_tac "k = 0", simp)
apply (rule append_constant_length_induct[of k])
apply simp
apply (simp add: f_shrink_Cons last_message_append)
done

lemma f_shrink_replicate: "m⇗n⇖ ÷⇩f k = m⇗n div k⇖"
apply (case_tac "k = 0", simp)
apply (case_tac "n < k")
apply (simp add: f_shrink_empty_conv)
apply (clarsimp simp: list_eq_iff f_shrink_length f_shrink_nth)
apply (rule last_message_replicate)
apply (clarsimp simp: min_def)
apply (drule mult_less_mono1[of _ "n div k" k], simp)
apply (simp add: div_mult_cancel)
done

lemma f_shrink_f_expand_id: "0 < k ⟹ xs ⊙⇩f k ÷⇩f k = xs"
apply (simp add: list_eq_iff)
apply (simp add: f_shrink_length f_shrink_nth f_expand_drop_mult f_expand_take_mod drop_take_1 last_message_replicate_NoMsg)
done

lemma f_expand_f_shrink_id_take[rule_format]: "
⟦ ∀i<length xs. 0 < i mod k ⟶ xs ! i = \<NoMsg> ⟧ ⟹
xs ÷⇩f k ⊙⇩f k = xs ↓ (length xs div k * k)"
apply (case_tac "k = 0", simp)
apply (induct xs rule: append_constant_length_induct[of k])
apply (simp add: f_shrink_empty_conv[symmetric])
apply (drule meta_mp)
apply clarify
apply (drule_tac x="length xs + i" in spec, simp)
apply (simp add: f_shrink_append_mod)
apply (rule_tac t=xs and s="(xs ! 0) # replicate (k - Suc 0) \<NoMsg>" in subst)
apply (simp (no_asm_simp) add: list_eq_iff nth_Cons')
apply (clarify, rename_tac i)
apply (drule_tac x=i in spec)
apply (simp add: nth_append)
apply (simp (no_asm_simp) add: list_eq_iff)
apply (clarsimp simp: f_shrink_length f_expand_nth_if f_shrink_nth last_message_replicate_NoMsg nth_Cons')
done

corollary f_expand_f_shrink_id_mod_0: "
⟦ length xs mod k = 0;
⋀i. ⟦ i < length xs; 0 < i mod k ⟧ ⟹ xs ! i = \<NoMsg> ⟧ ⟹
xs ÷⇩f k ⊙⇩f k = xs"
by (clarsimp simp: f_expand_f_shrink_id_take)

lemma f_shrink_take: "
xs ↓ n ÷⇩f k = xs ÷⇩f k ↓ (n div k)"
by (simp add: f_shrink_def f_aggregate_take)

lemma f_shrink_take_mult: "xs ↓ (n * k) ÷⇩f k = xs ÷⇩f k ↓ n"
by (simp add: f_shrink_def f_aggregate_take_mult)

lemma f_shrink_drop_mult: "xs ↑ (n * k) ÷⇩f k = xs ÷⇩f k ↑ n"
by (simp add: f_shrink_def f_aggregate_drop_mult)

lemma f_shrink_drop_mod: "
n mod k = 0 ⟹ xs ↑ n ÷⇩f k = xs ÷⇩f k ↑ (n div k)"
by (simp add: f_shrink_def f_aggregate_drop_mod)

lemma f_shrink_eq_conv: "
(xs ÷⇩f k1 = ys ÷⇩f k2) =
(length xs div k1 = length ys div k2 ∧
(∀i<length xs div k1.
last_message (xs ↑ (i * k1) ↓ k1) = last_message (ys ↑ (i * k2) ↓ k2)))"
apply (case_tac "k1 = 0")
apply (simp add: eq_commute[of "[]"] length_0_conv[symmetric] f_shrink_length del: length_0_conv)
apply (case_tac "k2 = 0")
apply (fastforce simp: f_shrink_empty_conv div_eq_0_conv')
apply (simp add: list_eq_iff f_shrink_length)
apply (rule conj_cong, simp)
apply (rule all_imp_eqI, simp)
apply (simp add: f_shrink_nth)
done

lemma f_shrink_eq_conv': "
(xs' ÷⇩f k = xs) =
(length xs' div k = length xs ∧
(∀i<length xs.
if xs ! i = \<NoMsg> then (∀j<k. xs' ! (i * k + j) = \<NoMsg>)
else (∃n<k. xs' ! (i * k + n) = xs ! i ∧
(∀j<k. n < j ⟶ xs' ! (i * k + j) = \<NoMsg>))))"
apply (case_tac "k = 0", fastforce)
apply (simp add: list_eq_iff f_shrink_length split del: if_split)
apply (rule conj_cong, simp)
apply (rule all_imp_eqI, simp)
apply (cut_tac x=i in less_div_imp_mult_add_divisor_le[of _ "length xs'" k], simp)
apply (clarsimp simp: f_shrink_nth last_message_conv_if min_eqR)
apply (rule ex_imp_eqI, simp)
apply simp
done

lemma f_shrink_assoc: "xs ÷⇩f a ÷⇩f b = xs ÷⇩f (a * b)"
by (unfold f_shrink_def, rule f_aggregate_assoc, fold f_shrink_def, rule f_shrink_last_message)

lemma f_shrink_commute: "xs ÷⇩f a ÷⇩f b = xs ÷⇩f b ÷⇩f a"
by (simp add: f_shrink_assoc mult.commute[of a])

lemma i_shrink_0[simp]: "f ÷⇩i 0 = (λn. \<NoMsg>)"
by (simp add: i_shrink_defs)
lemma i_shrink_1[simp]: "f ÷⇩i Suc 0 = f"
by (simp add: i_shrink_def i_aggregate_1)
lemma i_shrink_nth: "(f ÷⇩i k) n = last_message (f ⇑ (n * k) ⇓ k)"
by (simp add: i_shrink_defs)
lemma i_shrink_nth_eq_map: "(f ÷⇩i k) n = last_message (map f [n * k..<n * k + k])"
by (simp add: i_shrink_def i_aggregate_nth_eq_map)
lemma i_shrink_hd: "(f ÷⇩i k) 0 = last_message (f ⇓ k)"
by (simp add: i_shrink_nth)

lemma i_shrink_i_append_mod: "
length xs mod k = 0 ⟹ (xs ⌢ f) ÷⇩i k = xs ÷⇩f k ⌢ (f ÷⇩i k)"
by (simp add: f_shrink_def i_shrink_def i_aggregate_i_append_mod)

lemma i_shrink_i_append_mult: "
length xs = m * k ⟹ (xs ⌢ f) ÷⇩i k = xs ÷⇩f k ⌢ (f ÷⇩i k)"
by (simp add: i_shrink_i_append_mod)

lemma i_shrink_Cons: "
⟦ 0 < k; length xs = k ⟧ ⟹ (xs ⌢ f) ÷⇩i k = [last_message xs] ⌢ (f ÷⇩i k)"
by (simp add: f_shrink_def i_shrink_def i_aggregate_Cons)

lemma i_shrink_take_nth: "
n < m div k ⟹ (f ⇓ m) ÷⇩f k ! n = (f ÷⇩i k) n"
by (simp add: f_shrink_def i_shrink_def i_aggregate_take_nth)

lemma i_shrink_const[simp]: "0 < k ⟹ (λx. m) ÷⇩i k = (λx. m)"
by (simp add: ilist_eq_iff i_shrink_nth last_message_replicate)

lemma i_shrink_const_NoMsg[simp]: "(λx. \<NoMsg>) ÷⇩i k = (λx. \<NoMsg>)"
by (case_tac "k = 0", simp+)

lemma i_shrink_i_expand_id: "0 < k ⟹ f ⊙⇩i k ÷⇩i k = f"
by (simp add: ilist_eq_iff i_shrink_nth i_expand_i_drop_mult i_expand_i_take_mod i_drop_i_take_1 last_message_replicate_NoMsg)

lemma i_shrink_i_take_mult: "0 < k ⟹ f ⇓ (n * k) ÷⇩f k = f ÷⇩i k ⇓ n"
by (simp add: f_shrink_def i_shrink_def i_aggregate_i_take_mult)

lemma i_shrink_i_take: "
f ⇓ n ÷⇩f k = f ÷⇩i k ⇓ (n div k)"
by (simp add: f_shrink_def i_shrink_def i_aggregate_i_take)

lemma i_shrink_i_drop_mult: "f ⇑ (n * k) ÷⇩i k = f ÷⇩i k ⇑ n"
by (simp add: f_shrink_def i_shrink_def i_aggregate_i_drop_mult)
lemma i_shrink_i_drop_mod: "
n mod k = 0 ⟹ f ⇑ n ÷⇩i k = f ÷⇩i k ⇑ (n div k)"
by (simp add: f_shrink_def i_shrink_def i_aggregate_i_drop_mod)

lemma i_shrink_eq_conv: "
(f ÷⇩i k1 = g ÷⇩i k2) =
(∀i. last_message (f ⇑ (i * k1) ⇓ k1) =
last_message (g ⇑ (i * k2) ⇓ k2))"
by (simp add: ilist_eq_iff i_shrink_nth)

lemma i_shrink_eq_conv': "
(f' ÷⇩i k = f) =
(∀i. if f i = \<NoMsg> then ∀j<k. f' (i * k + j) = \<NoMsg>
else ∃n<k. f' (i * k + n) = f i ∧
(∀j<k. n < j ⟶ f' (i * k + j) = \<NoMsg>))"
apply (simp add: ilist_eq_iff)
apply (case_tac "k = 0", fastforce)
apply (rule all_eqI, rename_tac i)
apply (simp add: i_shrink_nth)
apply (case_tac "f i = NoMsg")
apply (simp add: last_message_NoMsg_conv)
apply (force simp add: last_message_conv)
done

lemma i_shrink_assoc: "f ÷⇩i a ÷⇩i b = f ÷⇩i (a * b)"
apply (case_tac "a = 0", simp)
apply (case_tac "b = 0", simp)
apply (unfold i_shrink_def, rule i_aggregate_assoc, simp+)
apply (fold f_shrink_def, simp add: f_shrink_last_message)
done

lemma i_shrink_commute: "f ÷⇩i a ÷⇩i b = f ÷⇩i b ÷⇩i a"
by (simp add: i_shrink_assoc mult.commute[of a])

subsubsection ‹Holding last messages in everly cycle of a stream›

primrec last_message_hold_init :: "'a fstream_af ⇒ 'a message_af ⇒ 'a fstream_af"
where
"last_message_hold_init [] m = []"
| "last_message_hold_init (x # xs) m =
(if x = \<NoMsg> then m else x) #
(last_message_hold_init xs (if x = \<NoMsg> then m else x))"

definition last_message_hold :: "'a fstream_af ⇒ 'a fstream_af"
where "last_message_hold xs ≡ last_message_hold_init xs \<NoMsg>"

lemma last_message_hold_init_length[simp]: "
⋀m. length (last_message_hold_init xs m) = length xs"
by (induct xs, simp+)

lemma last_message_hold_init_nth: "
⋀i m. i < length xs ⟹
(last_message_hold_init xs m) ! i = last_message (m # xs ↓ Suc i)"
apply (induct xs, simp)
apply (simp add: nth_Cons')
done

lemma last_message_hold_init_snoc: "
last_message_hold_init (xs @ [x]) m =
last_message_hold_init xs m @
[if x = \<NoMsg> then last_message (m # xs) else x]"
by (simp add: list_eq_iff nth_append last_message_hold_init_nth last_message_append)

lemma last_message_hold_init_append[rule_format]: "
⋀xs m. last_message_hold_init (xs @ ys) m =
last_message_hold_init xs m @ last_message_hold_init ys (last_message (m # xs))"
apply (induct ys, simp)
apply (rule_tac x=a in subst[OF append_eq_Cons, rule_format])
apply (simp only: append_Cons[symmetric] append_assoc[symmetric])
apply (simp add: last_message_hold_init_snoc last_message_append)
done

lemma last_message_hold_length[simp]: "length (last_message_hold xs) = length xs"
by (simp add: last_message_hold_def)

lemma last_message_hold_Nil[simp]: "last_message_hold [] = []"
by (simp add: last_message_hold_def)

lemma last_message_hold_one[simp]: "last_message_hold [x] = [x]"
by (simp add: last_message_hold_def)

lemma last_message_hold_nth: "
i < length xs ⟹ last_message_hold xs ! i = last_message (xs ↓ Suc i)"
by (simp add: last_message_hold_def last_message_hold_init_nth)

lemma last_message_hold_last: "
xs ≠ [] ⟹ last (last_message_hold xs) = last_message xs"
apply (subgoal_tac "last_message_hold xs ≠ []")
prefer 2
apply (simp add: length_greater_0_conv[symmetric] del: length_greater_0_conv)
apply (simp add: last_nth last_message_hold_nth length_greater_0_conv[symmetric] del: length_greater_0_conv)
done

lemma last_message_hold_take: "
last_message_hold xs ↓ n = last_message_hold (xs ↓ n)"
apply (case_tac "length xs ≤ n", simp)
apply (simp add: list_eq_iff last_message_hold_nth min_eqL)
done

lemma last_message_hold_snoc: "
last_message_hold (xs @ [x]) =
last_message_hold xs @ [if x = \<NoMsg> then last_message xs else x]"
by (simp add: last_message_hold_def last_message_hold_init_snoc)

lemma last_message_hold_append: "
last_message_hold (xs @ ys) =
last_message_hold xs @ last_message_hold_init ys (last_message xs)"
by (simp add: last_message_hold_def last_message_hold_init_append)

lemma last_message_hold_append': "
last_message_hold (xs @ ys) =
last_message_hold xs @ tl (last_message_hold (last_message xs # ys))"
apply (simp add: last_message_hold_append)
apply (simp add: last_message_hold_def)
done

lemma last_message_last_message_hold[simp]: "
last_message (last_message_hold xs) = last_message xs"
apply (induct xs rule: rev_induct, simp)
apply (simp add: last_message_hold_snoc last_message_append)
done

lemma last_message_hold_idem[simp]: "
last_message_hold (last_message_hold xs) = last_message_hold xs"
by (simp add: list_eq_iff last_message_hold_nth last_message_hold_take)

text ‹
Returns for each point in time the currently last non-empty message
of the current stream cycle of length ‹k›.›

definition f_last_message_hold :: "'a fstream_af ⇒ nat ⇒ 'a fstream_af" (infixl "⟼⇩f" 100)
where "f_last_message_hold xs k ≡ concat (map last_message_hold (list_slice2 xs k))"

definition i_last_message_hold :: "'a istream_af ⇒ nat ⇒ 'a istream_af" (infixl "⟼⇩i" 100)
where "i_last_message_hold f k ≡ λn. last_message (f ⇑ (n - n mod k) ⇓ Suc (n mod k))"

notation
f_last_message_hold  (infixl "⟼" 100) and
i_last_message_hold  (infixl "⟼" 100)

lemma f_last_message_hold_0[simp]: "xs ⟼⇩f 0 = last_message_hold xs"
by (simp add: f_last_message_hold_def list_slice2_0)

lemma f_last_message_hold_1[simp]: "xs ⟼⇩f (Suc 0) = xs"
apply (simp add: f_last_message_hold_def list_slice2_1)
apply (induct xs, simp+)
done

lemma f_last_message_hold_Nil[simp]: "[] ⟼⇩f k = []"
by (simp add: f_last_message_hold_def list_slice2_Nil)

lemma f_last_message_hold_length[simp]: "length (xs ⟼⇩f k) = length xs"
apply (case_tac "k = 0", simp)
apply (simp add: f_last_message_hold_def)
apply (induct xs rule: append_constant_length_induct[of k])
apply (simp add: list_slice2_le)
apply (simp add: list_slice2_append_mod list_slice2_mod_0 list_slice_div_eq_1)
done

lemma f_last_message_hold_le: "length xs ≤ k ⟹ xs ⟼⇩f k = last_message_hold xs"
by (simp add: f_last_message_hold_def list_slice2_le)

lemma f_last_message_hold_append_mult: "
length xs = m * k ⟹ (xs @ ys) ⟼⇩f k = xs ⟼⇩f k @ (ys ⟼⇩f k)"
by (simp add: f_last_message_hold_def list_slice2_append_mod)

lemma f_last_message_hold_append_mod: "
length xs mod k = 0 ⟹ (xs @ ys) ⟼⇩f k = xs ⟼⇩f k @ (ys ⟼⇩f k)"
by (simp add: f_last_message_hold_def list_slice2_append_mod)

lemma f_last_message_hold_nth[rule_format]: "
∀n. n < length xs ⟶ xs ⟼⇩f k ! n = last_message (xs ↑ (n div k * k) ↓ Suc (n mod k))"
apply (case_tac "k = 0")
apply (simp add: last_message_hold_nth)
apply (induct xs rule: append_constant_length_induct[of k])
apply (simp add: f_last_message_hold_def list_slice2_le last_message_hold_nth)
apply (simp add: f_last_message_hold_append_mod nth_append)
apply (intro allI conjI impI)
apply (simp add: f_last_message_hold_def list_slice2_mod_0 list_slice_div_eq_1 last_message_hold_nth)
apply (case_tac "n < k", simp)
apply (simp add: linorder_not_less last_message_append div_mult_cancel)
apply (subgoal_tac "k + n mod k ≤ n")
prefer 2
apply (drule div_le_mono[of _ _ k], drule mult_le_mono1[of _ _ k])
apply (simp add: div_mult_cancel)
done

lemma f_last_message_hold_take: "xs ↓ n ⟼⇩f k = xs ⟼⇩f k ↓ n"
by (clarsimp simp: list_eq_iff f_last_message_hold_nth drop_take div_mult_cancel min_eqL)

lemma f_last_message_hold_drop_mult: "
xs ↑ (n * k) ⟼⇩f k = xs ⟼⇩f k ↑ (n * k)"
apply (rule subst[OF append_take_drop_id, of _ "n * k" xs])
apply (case_tac "length xs ≤ n * k", simp)
apply (simp add: f_last_message_hold_append_mod min_eqR del: append_take_drop_id)
done

lemma f_last_message_hold_drop_mod: "
n mod k = 0 ⟹ xs ↑ n ⟼⇩f k = xs ⟼⇩f k ↑ n"
by (clarsimp simp: mult.commute[of k] f_last_message_hold_drop_mult elim!: dvdE)

lemma f_last_message_hold_idem: "xs ⟼⇩f k ⟼⇩f k = xs ⟼⇩f k"
apply (case_tac "k = 0", simp)
apply (simp add: list_eq_iff f_last_message_hold_nth f_last_message_hold_drop_mod[symmetric] f_last_message_hold_take[symmetric])
apply (simp add: f_last_message_hold_le min.coboundedI2 Suc_mod_le_divisor)
done

lemma f_shrink_nth_eq_f_last_message_hold_last: "
n < length xs div k ⟹ xs ÷⇩f k ! n = last (xs ⟼⇩f k ↑ (n * k) ↓ k)"
apply (case_tac "k = 0", simp)
apply (case_tac "xs = []", simp)
apply (simp add: f_shrink_nth f_last_message_hold_drop_mult[symmetric] f_last_message_hold_take[symmetric])
apply (simp add: f_last_message_hold_le last_message_hold_last)
done

lemma f_shrink_nth_eq_f_last_message_hold_nth: "
n < length xs div k ⟹ xs ÷⇩f k ! n = xs ⟼⇩f k ! (n * k + k - Suc 0)"
apply (case_tac "k = 0", simp)
apply (simp add: f_shrink_nth_eq_f_last_message_hold_last)
apply (simp add: last_nth min_eqR)
done

lemma last_message_f_last_message_hold: "
last_message (xs ⟼⇩f k) = last_message xs"
apply (case_tac "k = 0", simp)
apply (induct xs rule: append_constant_length_induct[of k])
apply (simp add: f_last_message_hold_le)
apply (simp add: f_last_message_hold_append_mult last_message_append f_last_message_hold_le)
done

lemma i_last_message_hold_0[simp]: "f ⟼⇩i 0 = (λn. last_message (f ⇓ Suc n))"
by (simp add: i_last_message_hold_def)
lemma i_last_message_hold_1[simp]: "f ⟼⇩i Suc 0 = f"
by (simp add: i_last_message_hold_def i_drop_i_take_1)

lemma i_last_message_hold_nth: "
(f ⟼⇩i k) n = last_message (f ⇑ (n - n mod k) ⇓ Suc (n mod k))"
by (simp add: i_last_message_hold_def)

lemma i_last_message_hold_i_append_mult: "
length xs = m * k ⟹ (xs ⌢ f) ⟼⇩i k = (xs ⟼⇩f k) ⌢ (f ⟼⇩i k)"
apply (case_tac "k = 0", simp)
apply (clarsimp simp: ilist_eq_iff i_last_message_hold_nth i_append_nth f_last_message_hold_nth div_mult_cancel linorder_not_less)
apply (subgoal_tac "length xs ≤ x - x mod k")
prefer 2
apply (drule div_le_mono[of _ _ k])
apply (simp add: div_mult_cancel[symmetric])
apply (simp add: mod_diff_mult_self1)
apply (drule_tac j="x - x mod k" and k="x mod k" in add_le_mono1)
apply (simp add: add.commute[of "m * k"])
done

lemma i_last_message_hold_i_append_mod: "
length xs mod k = 0 ⟹ (xs ⌢ f) ⟼⇩i k = (xs ⟼⇩f k) ⌢ (f ⟼⇩i k)"
by (clarsimp simp: mult.commute[of k] elim!: dvdE, rule i_last_message_hold_i_append_mult)

lemma i_last_message_hold_i_take: "f ⇓ n ⟼⇩f k = (f ⟼⇩i k) ⇓ n"
by (simp add: list_eq_iff f_last_message_hold_nth i_last_message_hold_nth div_mult_cancel i_take_drop min_eqR)

lemma i_last_message_hold_i_drop_mult: "
f ⇑ (n * k) ⟼⇩i k = f ⟼⇩i k ⇑ (n * k)"
by (simp add: ilist_eq_iff i_last_message_hold_nth)

lemma i_last_message_hold_i_drop_mod: "
n mod k = 0 ⟹ f ⇑ n ⟼⇩i k = f ⟼⇩i k ⇑ n"
by (clarsimp simp: mult.commute[of k] elim!: dvdE, rule i_last_message_hold_i_drop_mult)

lemma i_last_message_hold_idem: "f ⟼⇩i k ⟼⇩i k = f ⟼⇩i k"
by (simp add: ilist_eq_iff i_last_message_hold_nth minus_mod_eq_mult_div i_last_message_hold_i_drop_mod[symmetric] i_last_message_hold_i_take[symmetric] last_message_f_last_message_hold)

lemma i_shrink_nth_eq_i_last_message_hold_nth: "
0 < k ⟹ (f ÷⇩i k) n = (f ⟼⇩i k) (n * k + k - Suc 0)"
apply (simp add: i_shrink_nth i_last_message_hold_nth)
done

lemma i_shrink_nth_eq_i_last_message_hold_last: "
0 < k ⟹ (f ÷⇩i k) n = last (f ⟼⇩i k ⇑ (n * k) ⇓ k)"
by (simp add: last_nth i_shrink_nth_eq_i_last_message_hold_nth)

subsubsection ‹Compressing lists›

text ‹
Lists/Non-message streams
do not have to permit the empty message ‹\<NoMsg>›
to be element.
Thus, they are compressed by factor @{term k}
by just aggregating every sequence of length k
to its last element.›

definition f_shrink_last :: "'a list ⇒ nat ⇒ 'a list"   (infixl "÷⇘fl⇙" 100)
where "f_shrink_last xs k ≡ f_aggregate xs k last"

definition i_shrink_last :: "'a ilist ⇒ nat ⇒ 'a ilist" (infixl "÷⇘il⇙" 100)
where "i_shrink_last f k ≡ i_aggregate f k last"

notation
f_shrink_last  (infixl "÷⇩l" 100) and
i_shrink_last  (infixl "÷⇩l" 100)

lemma f_shrink_last_0[simp]: "xs ÷⇘fl⇙ 0 = []"
by (simp add: f_shrink_last_def f_aggregate_def list_slice_0)

lemma f_shrink_last_1[simp]: "xs ÷⇘fl⇙ Suc 0 = xs"
by (simp add: f_shrink_last_def f_aggregate_1)

lemma f_shrink_last_Nil[simp]: "[] ÷⇘fl⇙ k = []"
by (simp add: f_shrink_last_def f_aggregate_def list_slice_Nil)

lemma f_shrink_last_length: "length (xs ÷⇘fl⇙ k) = length xs div k"
by (simp add: f_shrink_last_def)

lemma f_shrink_last_empty_conv: "
0 < k ⟹ (xs ÷⇘fl⇙ k = []) = (length xs < k)"
by (simp add: f_shrink_last_def f_aggregate_empty_conv)

lemma f_shrink_last_Cons: "
⟦ 0 < k;
length xs = k ⟧ ⟹ (xs @ ys) ÷⇘fl⇙ k = last xs # (ys ÷⇘fl⇙ k)"
by (simp add: f_shrink_last_def f_aggregate_Cons)

lemma f_shrink_last_one: "
⟦ 0 < k; length xs = k ⟧ ⟹ xs ÷⇘fl⇙ k = [last xs]"
by (simp add: f_shrink_last_def f_aggregate_one)

lemma f_shrink_last_eq_f_shrink_last_take: "
xs ↓ (length xs div k * k) ÷⇘fl⇙ k = xs ÷⇘fl⇙ k"
by (simp add: f_shrink_last_def f_aggregate_eq_f_aggregate_take)

lemma f_shrink_last_nth: "
n < length xs div k ⟹ (xs ÷⇘fl⇙ k) ! n = xs ! (n * k + k - Suc 0)"
apply (case_tac "k = 0", simp)
apply (simp add: f_shrink_last_def f_aggregate_nth last_take2)
done

corollary f_shrink_last_nth': "
n < length xs div k ⟹ (xs ÷⇘fl⇙ k) ! n = xs ! (Suc n * k - Suc 0)"

lemma f_shrink_last_hd: "
⟦ 0 < k; k ≤ length xs ⟧ ⟹ hd (xs ÷⇘fl⇙ k) = xs ! (k - Suc 0)"
by (simp add: f_shrink_last_def f_aggregate_hd last_take2)

lemma f_shrink_last_map: "(map f xs) ÷⇘fl⇙ k = map f (xs ÷⇘fl⇙ k)"
apply (case_tac "k = 0", simp)
apply (clarsimp simp: list_eq_iff f_shrink_last_length)
apply (simp add: f_shrink_last_nth)
done

lemma f_shrink_last_append_mod: "
length xs mod k = 0 ⟹ (xs @ ys) ÷⇘fl⇙ k = xs ÷⇘fl⇙ k @ (ys ÷⇘fl⇙ k)"
by (simp add: f_shrink_last_def f_aggregate_append_mod)

lemma f_shrink_last_append_mult: "
length xs = m * k ⟹ (xs @ ys) ÷⇘fl⇙ k = xs ÷⇘fl⇙ k @ (ys ÷⇘fl⇙ k)"
by (unfold f_shrink_last_def, rule f_aggregate_append_mult)

lemma f_shrink_last_snoc: "
⟦ 0 < k; length ys = k; length xs mod k = 0 ⟧ ⟹
(xs @ ys) ÷⇘fl⇙ k = xs ÷⇘fl⇙ k @ [last ys]"
by (simp add: f_shrink_last_append_mod f_shrink_last_one)

lemma f_shrink_last_last: "
length xs mod k = 0 ⟹ last (xs ÷⇘fl⇙ k) = last xs"
apply (case_tac "k = 0", simp)
apply (case_tac "xs = []", simp)
apply (subgoal_tac "k ≤ length xs")
prefer 2
apply (rule ccontr, simp)
apply (rule subst[OF append_take_drop_id[of "length xs - k" xs]])
apply (subst f_shrink_last_snoc)
apply (simp add: min_eqR mod_diff_self2)+
done

lemma f_shrink_last_replicate: "m⇗n⇖ ÷⇘fl⇙ k = m⇗n div k⇖"
apply (case_tac "k = 0", simp)
apply (clarsimp simp: list_eq_iff f_shrink_last_length)
apply (simp add: f_shrink_last_nth)
done

lemma f_shrink_last_take: "
xs ↓ n ÷⇘fl⇙ k = xs ÷⇘fl⇙ k ↓ (n div k)"
by (unfold f_shrink_last_def, rule f_aggregate_take)

lemma f_shrink_last_take_mult: "xs ↓ (n * k) ÷⇘fl⇙ k = xs ÷⇘fl⇙ k ↓ n"
by (unfold f_shrink_last_def, rule f_aggregate_take_mult)

lemma f_shrink_last_drop_mult: "xs ↑ (n * k) ÷⇘fl⇙ k = xs ÷⇘fl⇙ k ↑ n"
by (unfold f_shrink_last_def, rule f_aggregate_drop_mult)

lemma f_shrink_last_drop_mod: "
n mod k = 0 ⟹ xs ↑ n ÷⇘fl⇙ k = xs ÷⇘fl⇙ k ↑ (n div k)"
by (unfold f_shrink_last_def, rule f_aggregate_drop_mod)

lemma f_shrink_last_assoc: "xs ÷⇘fl⇙ a ÷⇘fl⇙ b = xs ÷⇘fl⇙ (a * b)"
by (unfold f_shrink_last_def, rule f_aggregate_assoc, fold f_shrink_last_def, rule f_shrink_last_last)

lemma f_shrink_last_commute: "xs ÷⇘fl⇙ a ÷⇘fl⇙ b = xs ÷⇘fl⇙ b ÷⇘fl⇙ a"
by (simp add: f_shrink_last_assoc mult.commute[of a])

lemma i_shrink_last_1[simp]: "f ÷⇘il⇙ Suc 0 = f"
by (simp add: i_shrink_last_def i_aggregate_1)

lemma i_shrink_last_nth: "0 < k ⟹ (f ÷⇘il⇙ k) n =  f (n * k + k - Suc 0)"
by (simp add: i_shrink_last_def i_aggregate_nth last_i_take2)

lemma i_shrink_last_nth': "0 < k ⟹ (f ÷⇘il⇙ k) n =  f (Suc n * k - Suc 0)"

lemma i_shrink_last_hd: "(f ÷⇘il⇙ k) 0 = last (f ⇓ k)"
apply (case_tac "k = 0")
apply (simp add: i_shrink_last_def)
apply (simp add: i_shrink_last_nth last_i_take2)
done

lemma i_shrink_last_o: "0 < k ⟹ (f ∘ g) ÷⇘il⇙ k = f ∘ (g ÷⇘il⇙ k)"
by (simp add: ilist_eq_iff i_shrink_last_nth)

lemma i_shrink_last_i_append_mod: "
length xs mod k = 0 ⟹ (xs ⌢ f) ÷⇘il⇙ k = xs ÷⇘fl⇙ k ⌢ (f ÷⇘il⇙ k)"
by (simp add: f_shrink_last_def i_shrink_last_def i_aggregate_i_append_mod)

lemma i_shrink_last_i_append_mult: "
length xs = m * k ⟹ (xs ⌢ f) ÷⇘il⇙ k = xs ÷⇘fl⇙ k ⌢ (f ÷⇘il⇙ k)"
by (simp add: i_shrink_last_i_append_mod)

lemma i_shrink_last_Cons: "
⟦ 0 < k; length xs = k ⟧ ⟹ (xs ⌢ f) ÷⇘il⇙ k = [last xs] ⌢ (f ÷⇘il⇙ k)"
by (simp add: f_shrink_last_def i_shrink_last_def i_aggregate_Cons)

lemma i_shrink_last_const: "0 < k ⟹ (λx. m) ÷⇘il⇙ k = (λx. m)"
by (simp add: ilist_eq_iff i_shrink_last_nth)

lemma i_shrink_last_i_take_mult: "
0 < k ⟹ f ⇓ (n * k) ÷⇘fl⇙ k = f ÷⇘il⇙ k ⇓ n"
by (simp add: f_shrink_last_def i_shrink_last_def i_aggregate_i_take_mult)

lemma i_shrink_last_i_take: "
f ⇓ n ÷⇘fl⇙ k = f ÷⇘il⇙ k ⇓ (n div k)"
by (simp add: f_shrink_last_def i_shrink_last_def i_aggregate_i_take)

lemma i_shrink_last_i_drop_mult: "f ⇑ (n * k) ÷⇘il⇙ k = f ÷⇘il⇙ k ⇑ n"
by (simp add: f_shrink_last_def i_shrink_last_def i_aggregate_i_drop_mult)
lemma i_shrink_last_i_drop_mod: "
n mod k = 0 ⟹ f ⇑ n ÷⇘il⇙ k = f ÷⇘il⇙ k ⇑ (n div k)"
by (simp add: f_shrink_last_def i_shrink_last_def i_aggregate_i_drop_mod)

lemma i_shrink_last_assoc: "f ÷⇘il⇙ a ÷⇘il⇙ b = f ÷⇘il⇙ (a * b)"
apply (unfold i_shrink_last_def)
apply (case_tac "b = 0", simp)
apply (case_tac "a = 0", simp add: i_aggregate_def)
apply (simp add: i_aggregate_assoc f_shrink_last_last[unfolded f_shrink_last_def])
done

lemma i_shrink_last_commute: "f ÷⇘il⇙ a ÷⇘il⇙ b = f ÷⇘il⇙ b ÷⇘il⇙ a"
by (simp add: i_shrink_last_assoc mult.commute[of a])

text ‹
Shrinking a message stream with ‹last_message› as aggregation function
corresponds to shrinking the stream holding last message in each cycle
with ‹last› as aggregation function.›

lemma f_shrink_eq_f_last_message_hold_shrink_last: "
xs ÷⇩f k = xs ⟼⇩f k ÷⇘fl⇙ k"
by (simp add: list_eq_iff f_shrink_length f_shrink_last_length f_shrink_nth_eq_f_last_message_hold_nth f_shrink_last_nth)

lemma i_shrink_eq_i_last_message_hold_shrink_last: "
0 < k ⟹ f ÷⇩i k = f ⟼⇩i k ÷⇘il⇙ k"
by (simp add: ilist_eq_iff i_shrink_last_nth i_shrink_nth_eq_i_last_message_hold_nth)

end


# Theory AF_Stream_Exec

(*  Title:      AF_Stream_Exec.thy
Date:       Dec 2006
Author:     David Trachtenherz
*)

section ‹Processing of message streams›

theory AF_Stream_Exec
imports AF_Stream "List-Infinite.ListInf_Prefix" "List-Infinite.SetIntervalStep"
begin

subsection ‹Executing components with state transition functions›

subsubsection ‹Basic definitions›

text ‹
Function type for functions converting
an input value to an input port message for a component›
type_synonym ('a, 'in) Port_Input_Value = "'a ⇒ 'in message_af"

text ‹
Function type for functions extracting
the output value of a single output port from
a component value›
type_synonym ('comp, 'out) Port_Output_Value = "'comp ⇒ 'out message_af"

text ‹
Function type for functions extracting
the local state of a component from
a component value›
type_synonym ('comp, 'state) Comp_Local_State = "'comp ⇒ 'state"

text ‹
Function type for transition functions
computing the component's value after processing
an input for a single time unit›
type_synonym ('comp, 'input) Comp_Trans_Fun = "'input ⇒ 'comp ⇒ 'comp"

― ‹Execute a component for all inputs in the input stream @{typ "'input list"}›
primrec f_Exec_Comp :: "('comp, 'input) Comp_Trans_Fun ⇒ 'input list ⇒ 'comp ⇒ 'comp"
where
f_Exec_Nil:  "f_Exec_Comp trans_fun [] c = c"
| f_Exec_Cons: "f_Exec_Comp trans_fun (x#xs) c = f_Exec_Comp trans_fun xs (trans_fun x c)"

― ‹Execute the component for at most n steps›
definition f_Exec_Comp_N :: "('comp, 'input) Comp_Trans_Fun ⇒ nat ⇒ 'input list ⇒ 'comp ⇒ 'comp"
where "f_Exec_Comp_N trans_fun n xs c ≡ f_Exec_Comp trans_fun (xs ↓ n) c"

― ‹Produce the component stream for all inputs in the input stream›
primrec f_Exec_Comp_Stream :: "('comp, 'input) Comp_Trans_Fun ⇒ 'input list ⇒ 'comp ⇒ 'comp list"
where
f_Exec_Stream_Nil:  "f_Exec_Comp_Stream trans_fun [] c = []"
| f_Exec_Stream_Cons: "f_Exec_Comp_Stream trans_fun (x # xs) c =
(trans_fun x c) # ( f_Exec_Comp_Stream trans_fun xs (trans_fun x c) )"

primrec f_Exec_Comp_Stream_Init ::
"('comp, 'input) Comp_Trans_Fun ⇒ 'input list ⇒ 'comp ⇒ 'comp list"
where
f_Exec_Stream_Init_Nil:  "f_Exec_Comp_Stream_Init trans_fun [] c = [c]"
| f_Exec_Stream_Init_Cons: "f_Exec_Comp_Stream_Init trans_fun (x # xs) c =
c # ( f_Exec_Comp_Stream_Init trans_fun xs (trans_fun x c) )"

definition i_Exec_Comp_Stream ::
"('comp, 'input) Comp_Trans_Fun ⇒ 'input ilist ⇒ 'comp ⇒ 'comp ilist"
where "i_Exec_Comp_Stream ≡ λtrans_fun input c n. f_Exec_Comp trans_fun (input ⇓ Suc n) c"

definition i_Exec_Comp_Stream_Init ::
"('comp, 'input) Comp_Trans_Fun ⇒ 'input ilist ⇒ 'comp ⇒ 'comp ilist"
where "i_Exec_Comp_Stream_Init ≡ λtrans_fun input c n. f_Exec_Comp trans_fun (input ⇓ n) c"

subsubsection ‹Basic results›

lemma f_Exec_one: "f_Exec_Comp trans_fun [m] c = trans_fun m c"
by simp

lemma f_Exec_Stream_length[rule_format, simp]:"
∀c. length (f_Exec_Comp_Stream trans_fun xs c) = length xs"
by (induct xs, simp_all)

lemma f_Exec_Stream_empty_conv:"
(f_Exec_Comp_Stream trans_fun xs c = []) = (xs = [])"
by (simp add: length_0_conv[symmetric] del: length_0_conv)

lemma f_Exec_Stream_not_empty_conv:"
(f_Exec_Comp_Stream trans_fun xs c ≠ []) = (xs ≠ [])"
by (simp add: f_Exec_Stream_empty_conv)

lemma f_Exec_eq_f_Exec_Stream_last[rule_format]:"
∀c. f_Exec_Comp trans_fun xs c = last (c # (f_Exec_Comp_Stream trans_fun xs c))"
by (induct xs, simp_all)

corollary f_Exec_eq_f_Exec_Stream_last2[rule_format]: "
xs ≠ [] ⟹
f_Exec_Comp trans_fun xs c = last (f_Exec_Comp_Stream trans_fun xs c)"
by (simp add: f_Exec_eq_f_Exec_Stream_last f_Exec_Stream_empty_conv[symmetric, of xs trans_fun c])

corollary f_Exec_eq_f_Exec_Stream_last_if: "
f_Exec_Comp trans_fun xs c = (if xs = [] then c else last (f_Exec_Comp_Stream trans_fun xs c))"
by (simp add: f_Exec_eq_f_Exec_Stream_last2)

corollary f_Exec_take_eq_last_f_Exec_Stream_take:"
⟦ xs ≠ []; 0 < n ⟧ ⟹
f_Exec_Comp trans_fun (xs ↓ n) c =
last (f_Exec_Comp_Stream trans_fun (xs ↓ n) c)"
by (simp add: f_Exec_eq_f_Exec_Stream_last2 take_not_empty_conv)

corollary f_Exec_N_eq_last_f_Exec_Stream_take:"
⟦ xs ≠ []; 0 < n ⟧ ⟹
f_Exec_Comp_N trans_fun n xs c =
last (f_Exec_Comp_Stream trans_fun (xs ↓ n) c)"
by (simp add: f_Exec_Comp_N_def f_Exec_take_eq_last_f_Exec_Stream_take)

lemma f_Exec_Stream_nth: "
⋀n c. n < length xs ⟹
f_Exec_Comp_Stream trans_fun xs c ! n = f_Exec_Comp trans_fun (xs ↓ Suc n) c"
apply (induct xs, simp)
apply (simp add: nth_Cons')
done

lemma f_Exec_Stream_nth2: "
n ≤ length xs ⟹
(c # f_Exec_Comp_Stream trans_fun xs c) ! n = f_Exec_Comp trans_fun (xs ↓ n) c"
by (simp add: nth_Cons' f_Exec_Stream_nth)

lemma f_Exec_N_all:"
length xs ≤ n ⟹
f_Exec_Comp_N trans_fun n xs c = f_Exec_Comp trans_fun xs c"
by (simp add: f_Exec_Comp_N_def)

lemma f_Exec_Stream_append[rule_format]:"∀c.
f_Exec_Comp_Stream trans_fun (xs @ ys) c =
(f_Exec_Comp_Stream trans_fun xs c) @
(f_Exec_Comp_Stream trans_fun ys (f_Exec_Comp trans_fun xs c))"
by (induct xs, simp_all)

corollary f_Exec_Stream_append_last_Cons[rule_format]:"
f_Exec_Comp_Stream trans_fun (xs @ ys) c =
(f_Exec_Comp_Stream trans_fun xs c) @
(f_Exec_Comp_Stream trans_fun ys (last (c # (f_Exec_Comp_Stream  trans_fun xs c))))"
by (simp add: f_Exec_Stream_append f_Exec_eq_f_Exec_Stream_last)

corollary f_Exec_Stream_append_last[rule_format]:"
xs ≠ [] ⟹
f_Exec_Comp_Stream trans_fun (xs @ ys) c =
(f_Exec_Comp_Stream trans_fun xs c) @
(f_Exec_Comp_Stream trans_fun ys (last (f_Exec_Comp_Stream  trans_fun xs c)))"
by (simp add: f_Exec_Stream_append_last_Cons f_Exec_Stream_empty_conv)

corollary f_Exec_Stream_append_if:"
f_Exec_Comp_Stream trans_fun (xs @ ys) c =
(f_Exec_Comp_Stream trans_fun xs c) @
(f_Exec_Comp_Stream trans_fun ys (
if xs = [] then c else last (f_Exec_Comp_Stream trans_fun xs c)))"
by (simp add: f_Exec_Stream_append f_Exec_eq_f_Exec_Stream_last_if)
corollary f_Exec_append:"
f_Exec_Comp trans_fun (xs @ ys) c =
f_Exec_Comp trans_fun ys (f_Exec_Comp trans_fun xs c)"
by (simp add: f_Exec_eq_f_Exec_Stream_last f_Exec_Stream_append_if f_Exec_Stream_empty_conv)

corollary f_Exec_Stream_Cons_rev: "
xs ≠ [] ⟹
(trans_fun (hd xs) c) #
f_Exec_Comp_Stream trans_fun (tl xs) (trans_fun (hd xs) c) =
f_Exec_Comp_Stream trans_fun xs c"
by (subst f_Exec_Stream_Cons[symmetric], simp)

lemma f_Exec_Stream_snoc: "
f_Exec_Comp_Stream trans_fun (xs @ [x]) c =
f_Exec_Comp_Stream trans_fun xs c @
[trans_fun x (f_Exec_Comp trans_fun xs c)]"
by (simp add: f_Exec_Stream_append)

lemma f_Exec_snoc: "
f_Exec_Comp trans_fun (xs @ [x]) c =
trans_fun x (f_Exec_Comp trans_fun xs c)"
by (simp add: f_Exec_append)

lemma f_Exec_N_append[rule_format]:"
f_Exec_Comp_N trans_fun (a + b) xs c =
f_Exec_Comp_N trans_fun b (xs ↑ a) (f_Exec_Comp_N trans_fun a xs c)"
apply (simp add: f_Exec_Comp_N_def f_Exec_append[symmetric])
apply (rule subst[of "xs ↓ (a + b) ↓ a" "xs ↓ a" ], simp add: min_eqL)
apply (subst append_take_drop_id, simp)
done

corollary f_Exec_N_Suc[rule_format]:"
f_Exec_Comp_N trans_fun (Suc n) xs c =
f_Exec_Comp_N trans_fun (Suc 0) (xs ↑ n) (f_Exec_Comp_N trans_fun n xs c)"
by (simp add: f_Exec_N_append[symmetric])

corollary f_Exec_N_Suc2[rule_format]:"
n < length xs ⟹
f_Exec_Comp_N trans_fun (Suc n) xs c =
trans_fun (xs ! n) (f_Exec_Comp_N trans_fun n xs c)"
by (simp add: f_Exec_Comp_N_def take_Suc_conv_app_nth f_Exec_append)

theorem f_Exec_Stream_take:"
(f_Exec_Comp_Stream trans_fun xs c) ↓ n =
f_Exec_Comp_Stream trans_fun (xs ↓ n) c"
apply (case_tac "length xs ≤ n", simp)
apply (rule subst[OF append_take_drop_id, of _ n xs])
apply (simp add: f_Exec_Stream_append del: append_take_drop_id)
done

theorem f_Exec_Stream_drop:"
(f_Exec_Comp_Stream trans_fun xs c) ↑ n =
f_Exec_Comp_Stream trans_fun (xs ↑ n)
(f_Exec_Comp trans_fun (xs ↓ n) c)"
apply (case_tac "length xs ≤ n", simp)
apply (rule subst[OF append_take_drop_id, of _ n xs])
apply (simp add: f_Exec_Stream_append del: append_take_drop_id)
done

lemma i_Exec_Stream_nth: "
i_Exec_Comp_Stream trans_fun input c n = f_Exec_Comp trans_fun (input ⇓ Suc n) c"
by (simp add: i_Exec_Comp_Stream_def)

lemma i_Exec_Stream_nth_Suc: "
i_Exec_Comp_Stream trans_fun input c (Suc n) =
trans_fun (input (Suc n)) (i_Exec_Comp_Stream trans_fun input c n)"
by (simp add: i_Exec_Stream_nth i_take_Suc_conv_app_nth f_Exec_append)

lemma i_Exec_Stream_nth_Suc_first: "
i_Exec_Comp_Stream trans_fun input c (Suc n) =
(i_Exec_Comp_Stream trans_fun (input ⇑ Suc 0) (trans_fun (input 0) c) n)"
by (simp add: i_Exec_Stream_nth i_take_Suc)

lemma f_Exec_Stream_nth_eq_i_Exec_Stream_nth: "
n < n' ⟹
f_Exec_Comp_Stream trans_fun (input ⇓ n') c ! n =
i_Exec_Comp_Stream trans_fun input c n"
by (simp add: f_Exec_Stream_nth i_Exec_Stream_nth min_eqR)

lemma i_Exec_Stream_append: "
i_Exec_Comp_Stream trans_fun (xs ⌢ input) c =
f_Exec_Comp_Stream trans_fun xs c ⌢
i_Exec_Comp_Stream trans_fun input (f_Exec_Comp trans_fun xs c)"
by (simp add: ilist_eq_iff i_Exec_Stream_nth f_Exec_Stream_nth f_Exec_append i_append_nth Suc_diff_le)

lemma i_Exec_Stream_append_last_Cons: "
i_Exec_Comp_Stream trans_fun (xs ⌢ input) c =
f_Exec_Comp_Stream trans_fun xs c ⌢
i_Exec_Comp_Stream trans_fun input (
last (c # f_Exec_Comp_Stream trans_fun xs c))"
by (simp add: f_Exec_eq_f_Exec_Stream_last i_Exec_Stream_append)

lemma i_Exec_Stream_append_last: "
xs ≠ [] ⟹
i_Exec_Comp_Stream trans_fun (xs ⌢ input) c =
f_Exec_Comp_Stream trans_fun xs c ⌢
i_Exec_Comp_Stream trans_fun input (
last (f_Exec_Comp_Stream trans_fun xs c))"
by (simp add: f_Exec_Stream_empty_conv i_Exec_Stream_append_last_Cons)

lemma i_Exec_Stream_append_if: "
i_Exec_Comp_Stream trans_fun (xs ⌢ input) c =
f_Exec_Comp_Stream trans_fun xs c ⌢
i_Exec_Comp_Stream trans_fun input (
if xs = [] then c
else last (f_Exec_Comp_Stream trans_fun xs c))"
by (simp add: i_Exec_Stream_append_last)

corollary i_Exec_Stream_Cons: "
i_Exec_Comp_Stream trans_fun ([x] ⌢ input) c =
[trans_fun x c] ⌢ i_Exec_Comp_Stream trans_fun input (trans_fun x c)"
by (simp add: i_Exec_Stream_append)

corollary i_Exec_Stream_Cons_rev: "
[trans_fun (input 0) c] ⌢
i_Exec_Comp_Stream trans_fun (input ⇑ Suc 0) (trans_fun (input 0) c) =
i_Exec_Comp_Stream trans_fun input c"
apply (insert i_Exec_Stream_append[of trans_fun "[input 0]" "input ⇑ Suc 0" c])
apply (simp add: i_drop_Suc_conv_tl)
done

theorem i_Exec_Stream_take:"
(i_Exec_Comp_Stream trans_fun input c) ⇓ n =
f_Exec_Comp_Stream trans_fun (input ⇓ n) c"
by (simp add: list_eq_iff f_Exec_Stream_nth i_Exec_Stream_nth min_eqR)

theorem i_Exec_Stream_drop:"
(i_Exec_Comp_Stream trans_fun input c) ⇑ n =
i_Exec_Comp_Stream trans_fun (input ⇑ n) (f_Exec_Comp trans_fun (input ⇓ n) c)"
apply (rule subst[OF i_append_i_take_i_drop_id, of _ n input])
apply (simp add: i_Exec_Stream_append  i_drop_def del: i_append_i_take_i_drop_id)
done

lemma f_Exec_Stream_expand_aggregate_map_take: "
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) k ag ↓ n =
f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs ↓ n) ⊙⇩f k) c)) k ag"
by (simp add: f_aggregate_take_mult[symmetric] take_map f_Exec_Stream_take f_expand_take_mult)

corollary f_Exec_Stream_expand_aggregate_take: "
f_aggregate (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c) k ag ↓ n =
f_aggregate (f_Exec_Comp_Stream trans_fun ((xs ↓ n) ⊙⇩f k) c) k ag"
by (insert f_Exec_Stream_expand_aggregate_map_take[of n id trans_fun xs k c ag], simp add: map_id)

lemma i_Exec_Stream_expand_aggregate_map_take: "
0 < k ⟹
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c)) k ag ⇓ n =
f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((input ⇓ n) ⊙⇩f k) c)) k ag"
by (simp add: i_aggregate_i_take_mult[symmetric] i_Exec_Stream_take i_expand_i_take_mult)

corollary i_Exec_Stream_expand_aggregate_take: "
0 < k ⟹
i_aggregate (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c) k ag ⇓ n =
f_aggregate (f_Exec_Comp_Stream trans_fun ((input ⇓ n) ⊙⇩f k) c) k ag"
by (drule i_Exec_Stream_expand_aggregate_map_take[of k n id trans_fun input c ag], simp add: map_id)

lemma f_Exec_Stream_expand_aggregate_map_drop: "
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) k ag ↑ n =
f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs ↑ n) ⊙⇩f k) (
f_Exec_Comp trans_fun ((xs ↓ n) ⊙⇩f k) c))) k ag"
by (simp add: f_aggregate_drop_mult[symmetric] drop_map f_Exec_Stream_drop f_expand_take_mult f_expand_drop_mult)

corollary f_Exec_Stream_expand_aggregate_drop: "
f_aggregate (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c) k ag ↑ n =
f_aggregate (f_Exec_Comp_Stream trans_fun ((xs ↑ n) ⊙⇩f k) (
f_Exec_Comp trans_fun ((xs ↓ n) ⊙⇩f k) c)) k ag"
by (insert f_Exec_Stream_expand_aggregate_map_drop[of n id trans_fun xs k c ag], simp add: map_id)

lemma i_Exec_Stream_expand_aggregate_map_drop: "
0 < k ⟹
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c)) k ag ⇑ n =
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun ((input ⇑ n) ⊙⇩i k) (
f_Exec_Comp trans_fun ((input ⇓ n) ⊙⇩f k) c))) k ag"
by (simp add: i_aggregate_i_drop_mult[symmetric] i_Exec_Stream_drop i_expand_i_take_mult i_expand_i_drop_mult)

corollary i_Exec_Stream_expand_aggregate_drop: "
0 < k ⟹
i_aggregate (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c) k ag ⇑ n =
i_aggregate (i_Exec_Comp_Stream trans_fun ((input ⇑ n) ⊙⇩i k) (
f_Exec_Comp trans_fun ((input ⇓ n) ⊙⇩f k) c)) k ag"
by (drule i_Exec_Stream_expand_aggregate_map_drop[of k n id trans_fun input c ag], simp)

lemma f_Exec_Stream_expand_aggregate_map_nth_eq_i_nth: "
⟦ 0 < k; n < n' ⟧ ⟹
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (input ⇓ n' ⊙⇩f k) c)) k ag ! n =
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c)) k ag n"
apply (simp add: f_aggregate_nth i_aggregate_nth f_Exec_Stream_take f_Exec_Stream_drop i_Exec_Stream_take i_Exec_Stream_drop drop_map take_map)
apply (simp add: f_expand_take_mod i_expand_i_take_mod f_expand_drop_mod i_expand_i_drop_mod i_drop_i_take_1 drop_take_1 min_eqR)
done

corollary f_Exec_Stream_expand_aggregate_map_nth_eq_i_nth': "
0 < k ⟹
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (input ⇓ Suc n ⊙⇩f k) c)) k ag ! n =
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c)) k ag n"
by (simp add: f_Exec_Stream_expand_aggregate_map_nth_eq_i_nth)

corollary f_Exec_Stream_expand_aggregate_nth_eq_i_nth: "
⟦ 0 < k; n < n' ⟧ ⟹
f_aggregate (f_Exec_Comp_Stream trans_fun (input ⇓ n' ⊙⇩f k) c) k ag ! n =
i_aggregate (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c) k ag n"
by (drule f_Exec_Stream_expand_aggregate_map_nth_eq_i_nth[where f=id], simp_all add: map_id)

corollary f_Exec_Stream_expand_aggregate_nth_eq_i_nth': "
0 < k ⟹
f_aggregate (f_Exec_Comp_Stream trans_fun (input ⇓ Suc n ⊙⇩f k) c) k ag ! n =
i_aggregate (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c) k ag n"
by (simp add: f_Exec_Stream_expand_aggregate_nth_eq_i_nth)

lemma f_Exec_Stream_expand_shrink_last_map_nth_eq_f_Exec_Comp: "
⟦ 0 < k; n < length xs ⟧ ⟹
map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c) ÷⇘fl⇙ k ! n =
f (f_Exec_Comp trans_fun ((xs ↓ Suc n) ⊙⇩f k) c)"
apply (simp add: f_shrink_last_map f_shrink_last_length f_shrink_last_nth)
apply (subgoal_tac "n * k + k - Suc 0 < length xs * k")
prefer 2
apply (drule Suc_leI[of n])
apply (drule mult_le_mono1[of _ _ k], simp)
apply (simp add: f_Exec_Stream_nth add.commute[of k] f_expand_take_mult[symmetric])
done

corollary f_Exec_Stream_expand_shrink_last_nth_eq_f_Exec_Comp: "
⟦ 0 < k; n < length xs ⟧ ⟹
f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c ÷⇘fl⇙ k ! n =
f_Exec_Comp trans_fun ((xs ↓ Suc n) ⊙⇩f k) c"
by (drule f_Exec_Stream_expand_shrink_last_map_nth_eq_f_Exec_Comp[where f=id], simp_all add: map_id)

lemma f_Exec_Stream_expand_aggregate_map_nth: "
⟦ 0 < k; n < length xs ⟧ ⟹
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) k ag ! n =
ag (map f (f_Exec_Comp_Stream trans_fun (xs ! n # \<NoMsg>⇗k - Suc 0⇖)
(f_Exec_Comp trans_fun (xs ↓ n ⊙⇩f k) c)))"
apply (simp add: f_aggregate_nth take_map drop_map)
apply (simp add: take_map drop_map f_Exec_Stream_drop f_Exec_Stream_take f_expand_take_mod f_expand_drop_mod drop_take_1)
done

corollary f_Exec_Stream_expand_aggregate_nth: "
⟦ 0 < k; n < length xs ⟧ ⟹
f_aggregate (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c) k ag ! n =
ag (f_Exec_Comp_Stream trans_fun (xs ! n # \<NoMsg>⇗k - Suc 0⇖)
(f_Exec_Comp trans_fun (xs ↓ n ⊙⇩f k) c))"
by (drule f_Exec_Stream_expand_aggregate_map_nth[where f=id], simp_all add: map_id)

corollary f_Exec_Stream_expand_shrink_map_nth: "
⟦ 0 < k; n < length xs ⟧ ⟹
(map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) ÷⇩f k ! n =
last_message (map f (f_Exec_Comp_Stream trans_fun (xs ! n # \<NoMsg>⇗k - Suc 0⇖)
(f_Exec_Comp trans_fun (xs ↓ n ⊙⇩f k) c)))"
by (simp add: f_shrink_def f_Exec_Stream_expand_aggregate_map_nth)

lemma i_Exec_Stream_expand_aggregate_map_nth: "
0 < k ⟹
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c)) k ag n =
ag (map f (f_Exec_Comp_Stream trans_fun (input n # \<NoMsg>⇗k - Suc 0⇖)
(f_Exec_Comp trans_fun ((input ⇓ n) ⊙⇩f k) c)))"
by (simp add: i_aggregate_nth i_Exec_Stream_drop i_Exec_Stream_take i_expand_i_take_mod i_expand_i_drop_mod i_drop_i_take_1)

corollary i_Exec_Stream_expand_aggregate_nth: "
0 < k ⟹
i_aggregate (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c) k ag n =
ag (f_Exec_Comp_Stream trans_fun (input n # \<NoMsg>⇗k - Suc 0⇖)
(f_Exec_Comp trans_fun ((input ⇓ n) ⊙⇩f k) c))"
by (drule i_Exec_Stream_expand_aggregate_map_nth[where f=id], simp add: map_id)

corollary i_Exec_Stream_expand_shrink_map_nth: "
0 < k ⟹
((f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c)) ÷⇩i k) n =
last_message (map f (f_Exec_Comp_Stream trans_fun (input n # \<NoMsg>⇗k - Suc 0⇖)
(f_Exec_Comp trans_fun (input ⇓ n ⊙⇩f k) c)))"
by (simp add: i_shrink_def i_Exec_Stream_expand_aggregate_map_nth)

lemma f_Exec_Stream_expand_snoc: "
⟦ 0 < k; n < length xs ⟧ ⟹
f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c ↑ (n * k) ↓ k =
f_Exec_Comp_Stream trans_fun (xs ! n # \<NoMsg>⇗k - Suc 0⇖)
(f_Exec_Comp trans_fun (xs ↓ n ⊙⇩f k) c)"
by (simp add: f_Exec_Stream_drop f_Exec_Stream_take f_expand_take_mod f_expand_drop_mod drop_take_1)

lemma f_Exec_Stream_expand_map_aggregate_append: "
f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs @ ys) ⊙⇩f k) c)) k ag =
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) k ag @
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (ys ⊙⇩f k) (
f_Exec_Comp trans_fun (xs ⊙⇩f k) c))) k ag"
by (simp add: f_Exec_Stream_append f_aggregate_append_mod)

lemma i_Exec_Stream_expand_map_aggregate_append: "
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun ((xs ⌢ input) ⊙⇩i k) c)) k ag =
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) k ag ⌢
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) (
f_Exec_Comp trans_fun (xs ⊙⇩f k) c))) k ag"
by (simp add: i_expand_i_append i_Exec_Stream_append i_aggregate_i_append_mod)

lemma f_Exec_Stream_expand_map_aggregate_Cons: "
0 < k ⟹
f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((x # xs) ⊙⇩f k) c)) k ag =
ag (map f (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>⇗k - Suc 0⇖) c)) #
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) (
f_Exec_Comp trans_fun (x # \<NoMsg>⇗k - Suc 0⇖) c))) k ag"
apply (subst append_eq_Cons[of x xs, symmetric])
apply (subst f_Exec_Stream_expand_map_aggregate_append)
apply (simp add: f_aggregate_one)
done

lemma f_Exec_Stream_expand_map_aggregate_snoc: "
0 < k ⟹
f_aggregate (map f (f_Exec_Comp_Stream trans_fun ((xs @ [x]) ⊙⇩f k) c)) k ag =
f_aggregate (map f (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) k ag @
[ag (map f (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>⇗k - Suc 0⇖) (
f_Exec_Comp trans_fun (xs ⊙⇩f k) c)))]"
apply (subst f_Exec_Stream_expand_map_aggregate_append)
apply (simp add: f_aggregate_one)
done

lemma i_Exec_Stream_expand_map_aggregate_Cons: "
0 < k ⟹
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (([x] ⌢ input) ⊙⇩i k) c)) k ag =
[ag (map f (f_Exec_Comp_Stream trans_fun (x # \<NoMsg>⇗k - Suc 0⇖) c))] ⌢
i_aggregate (f ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) (
f_Exec_Comp trans_fun (x # \<NoMsg>⇗k - Suc 0⇖) c))) k ag"
apply (subst i_Exec_Stream_expand_map_aggregate_append)
apply (simp add: f_aggregate_one)
done

lemma f_Exec_N_eq_f_Exec_Stream_nth:"
n ≤ length xs ⟹
f_Exec_Comp_N trans_fun n xs c = (c # f_Exec_Comp_Stream trans_fun xs c) ! n"
by (simp add: f_Exec_Comp_N_def f_Exec_Stream_nth2)

theorem f_Exec_Stream_causal: "
xs ↓ n = ys ↓ n ⟹
(f_Exec_Comp_Stream trans_fun xs c) ↓ n = (f_Exec_Comp_Stream trans_fun ys c) ↓ n"
by (simp add: f_Exec_Stream_take)
theorem i_Exec_Stream_causal: "
input1 ⇓ n = input2 ⇓ n ⟹
(i_Exec_Comp_Stream trans_fun input1 c) ⇓ n = (i_Exec_Comp_Stream trans_fun input2 c) ⇓ n"
by (simp add: i_Exec_Stream_take)

text ‹Results for ‹f_Exec_Comp_Stream_Init››

text ‹
‹f_Exec_Comp_Stream_Init› computes the execution stream of a component
with the initial value of the component
at the beginning of the result stream.›

lemma f_Exec_Stream_Init_length[rule_format, simp]:"
∀c. length (f_Exec_Comp_Stream_Init trans_fun xs c) = Suc (length xs)"
by (induct xs, simp_all)

lemma f_Exec_Stream_Init_not_empty:"
(f_Exec_Comp_Stream_Init trans_fun xs c ≠ [])"
by (simp add: length_0_conv[symmetric] del: length_0_conv)

lemma f_Exec_eq_f_Exec_Stream_Init_last[rule_format]:"
∀c. f_Exec_Comp trans_fun xs c = last (f_Exec_Comp_Stream_Init trans_fun xs c)"
by (induct xs, simp_all add: f_Exec_Stream_Init_not_empty)

lemma f_Exec_Stream_Init_eq_f_Exec_Stream_Cons[rule_format]: "
∀c. f_Exec_Comp_Stream_Init trans_fun xs c = c # f_Exec_Comp_Stream trans_fun xs c"
by (induct xs, simp_all)

corollary f_Exec_Stream_Init_eq_f_Exec_Stream_Cons_output: "
output_fun c = \<NoMsg> ⟹
map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c) =
\<NoMsg> # map output_fun (f_Exec_Comp_Stream trans_fun xs c)"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)

corollary f_Exec_Stream_Init_tl_eq_f_Exec_Stream: "
tl (f_Exec_Comp_Stream_Init trans_fun xs c) = f_Exec_Comp_Stream trans_fun xs c"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)

lemma f_Exec_N_eq_last_f_Exec_Stream_Init_take:"
f_Exec_Comp_N trans_fun n xs c =
last (f_Exec_Comp_Stream_Init trans_fun (xs ↓ n) c)"
by (simp add: f_Exec_Comp_N_def f_Exec_eq_f_Exec_Stream_Init_last)

lemma f_Exec_Stream_Init_nth: "
n ≤ length xs ⟹
f_Exec_Comp_Stream_Init trans_fun xs c ! n = f_Exec_Comp trans_fun (xs ↓ n) c"
apply (subst f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)
apply (case_tac n, simp)
apply (simp add: f_Exec_Stream_nth)
done

lemma f_Exec_Stream_Init_nth_0: "f_Exec_Comp_Stream_Init trans_fun xs c ! 0 = c"
by (simp add: f_Exec_Stream_Init_nth)

lemma f_Exec_Stream_Init_hd: "hd (f_Exec_Comp_Stream_Init trans_fun xs c) = c"
by (simp add: hd_conv_nth f_Exec_Stream_Init_not_empty f_Exec_Stream_Init_nth_0)

lemma f_Exec_Stream_Init_nth_Suc_eq_f_Exec_Stream_nth: "
f_Exec_Comp_Stream_Init trans_fun xs c ! (Suc n) = f_Exec_Comp_Stream trans_fun xs c ! n"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)

lemma f_Exec_Stream_Init_append:"
f_Exec_Comp_Stream_Init trans_fun (xs @ ys) c =
(f_Exec_Comp_Stream_Init trans_fun xs c) @
tl (f_Exec_Comp_Stream_Init trans_fun ys (f_Exec_Comp trans_fun xs c))"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_append)

corollary f_Exec_Stream_Init_append_last:"
f_Exec_Comp_Stream_Init trans_fun (xs @ ys) c =
(f_Exec_Comp_Stream_Init trans_fun xs c) @
tl (f_Exec_Comp_Stream_Init trans_fun ys (last (f_Exec_Comp_Stream_Init trans_fun xs c)))"
by (simp add: f_Exec_Stream_Init_append f_Exec_eq_f_Exec_Stream_Init_last)

lemma f_Exec_Stream_Init_f_Exec_Stream_append:"
f_Exec_Comp_Stream_Init trans_fun (xs @ ys) c =
(f_Exec_Comp_Stream_Init trans_fun xs c) @
(f_Exec_Comp_Stream trans_fun ys (f_Exec_Comp trans_fun xs c))"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_append)

lemma f_Exec_Stream_Init_take:"
(f_Exec_Comp_Stream_Init trans_fun xs c) ↓ Suc n =
f_Exec_Comp_Stream_Init trans_fun (xs ↓ n) c"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_take)

lemma f_Exec_Stream_Init_drop:"
n ≤ length xs ⟹
(f_Exec_Comp_Stream_Init trans_fun xs c) ↑ n =
f_Exec_Comp_Stream_Init trans_fun (xs ↑ n)
(f_Exec_Comp trans_fun (xs ↓ n) c)"
apply (case_tac n, simp)
apply (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_drop)
apply (simp add: take_Suc_conv_app_nth f_Exec_append Cons_nth_drop_Suc[symmetric])
done

lemma f_Exec_Stream_Init_drop_geq_not_valid:"
length xs ≤ n ⟹
(f_Exec_Comp_Stream_Init trans_fun xs c) ↑ Suc n ≠
f_Exec_Comp_Stream_Init trans_fun arbitrary_input arbitrary_comp"
by (simp add: f_Exec_Stream_Init_not_empty[symmetric])

lemma i_Exec_Stream_Init_nth: "
i_Exec_Comp_Stream_Init trans_fun input c n = f_Exec_Comp trans_fun (input ⇓ n) c"
by (simp add: i_Exec_Comp_Stream_Init_def)

lemma i_Exec_Stream_Init_nth_0: "
i_Exec_Comp_Stream_Init trans_fun input c 0 = c"
by (simp add: i_Exec_Stream_Init_nth)

lemma i_Exec_Stream_Init_nth_Suc_eq_i_Exec_Stream_nth: "
i_Exec_Comp_Stream_Init trans_fun input c (Suc n) = i_Exec_Comp_Stream trans_fun input c n"
by (simp add: i_Exec_Stream_Init_nth i_Exec_Stream_nth)

lemma i_Exec_Stream_Init_eq_i_Exec_Stream_Cons: "
i_Exec_Comp_Stream_Init trans_fun input c = [c] ⌢ i_Exec_Comp_Stream trans_fun input c"
by (simp add: ilist_eq_iff i_Exec_Stream_Init_nth i_append_nth i_Exec_Stream_nth)

corollary i_Exec_Stream_Init_eq_i_Exec_Stream_Cons_output: "
output_fun c = \<NoMsg> ⟹
output_fun ∘ i_Exec_Comp_Stream_Init trans_fun input c =
[\<NoMsg>] ⌢ (output_fun ∘ i_Exec_Comp_Stream trans_fun input c)"
by (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)

lemma i_Exec_Stream_Init_append:"
i_Exec_Comp_Stream_Init trans_fun (input1 ⌢ input2) c =
(f_Exec_Comp_Stream_Init trans_fun input1 c) ⌢
((i_Exec_Comp_Stream_Init trans_fun input2 (f_Exec_Comp trans_fun input1 c)) ⇑ Suc 0)"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_append)

corollary i_Exec_Stream_Init_append_last:"
i_Exec_Comp_Stream_Init trans_fun (input1 ⌢ input2) c =
(f_Exec_Comp_Stream_Init trans_fun input1 c) ⌢
((i_Exec_Comp_Stream_Init trans_fun input2 (last (f_Exec_Comp_Stream_Init trans_fun input1 c))) ⇑ Suc 0)"
by (simp add: i_Exec_Stream_Init_append f_Exec_eq_f_Exec_Stream_Init_last)

lemma i_Exec_Stream_Init_i_Exec_Stream_append:"
i_Exec_Comp_Stream_Init trans_fun (input1 ⌢ input2) c =
(f_Exec_Comp_Stream_Init trans_fun input1 c) ⌢
(i_Exec_Comp_Stream trans_fun input2 (f_Exec_Comp trans_fun input1 c))"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_append)

lemma i_Exec_Stream_Init_take:"
(i_Exec_Comp_Stream_Init trans_fun input c) ⇓ Suc n =
f_Exec_Comp_Stream_Init trans_fun (input ⇓ n) c"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_take)
lemma i_Exec_Stream_Init_drop:"
(i_Exec_Comp_Stream_Init trans_fun input c) ⇑ n =
i_Exec_Comp_Stream_Init trans_fun (input ⇑ n)
(f_Exec_Comp trans_fun (input ⇓ n) c)"
apply (case_tac n, simp)
apply (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_drop)
apply (simp add: ilist_eq_iff i_take_Suc_conv_app_nth f_Exec_append i_Exec_Stream_nth i_append_nth i_take_first i_take_drop_eq_map)
apply (simp add: upt_conv_Cons)
done

theorem f_Exec_Stream_Init_strictly_causal: "
xs ↓ n = ys ↓ n ⟹
(f_Exec_Comp_Stream_Init trans_fun xs c) ↓ Suc n = (f_Exec_Comp_Stream_Init trans_fun ys c) ↓ Suc n"
by (simp add: f_Exec_Stream_Init_take)

theorem i_Exec_Stream_Init_strictly_causal: "
input1 ⇓ n = input2 ⇓ n ⟹
(i_Exec_Comp_Stream_Init trans_fun input1 c) ⇓ Suc n = (i_Exec_Comp_Stream_Init trans_fun input2 c) ⇓ Suc n"
by (simp add: i_Exec_Stream_Init_take)

theorem f_Exec_N_eq_f_Exec_Stream_Init_nth:"
n ≤ length xs ⟹
f_Exec_Comp_N trans_fun n xs c = f_Exec_Comp_Stream_Init trans_fun xs c ! n"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_N_eq_f_Exec_Stream_nth)

text ‹Basic results for previous element functions›

text ‹
The functions ‹list_Previous› and ‹ilist_Previous›
return the previous element of the list relatively to the specified position @{term n}
or the initial element if @{term n} is 0,›

definition list_Previous :: "'value list ⇒ 'value ⇒ nat ⇒ 'value"
where "list_Previous xs init n ≡
case n of
0 ⇒ init
| Suc n' ⇒ xs ! n'"

definition ilist_Previous :: "'value ilist ⇒ 'value ⇒ nat ⇒ 'value"
where "ilist_Previous f init n ≡
case n of
0 ⇒ init
| Suc n' ⇒ f n'"

abbreviation "list_Previous'" :: "'value list ⇒ 'value ⇒ nat ⇒ 'value"
( "_⇗←'' _⇖ _" [1000, 10, 100] 100)
where "xs⇗←' init⇖ n ≡ list_Previous xs init n"

abbreviation "ilist_Previous'" :: "'value ilist ⇒ 'value ⇒ nat ⇒ 'value"
( "_⇗← _⇖ _" [1000, 10, 100] 100)
where "f⇗← init⇖ n ≡ ilist_Previous f init n"

lemma list_Previous_nth: "xs⇗←' init⇖ n = (case n of 0 ⇒ init | Suc n' ⇒ xs ! n')"
by (simp add: list_Previous_def)

lemma ilist_Previous_nth: "f⇗← init⇖ n = (case n of 0 ⇒ init | Suc n' ⇒ f n')"
by (simp add: ilist_Previous_def)

lemma list_Previous_nth_if: "xs⇗←' init⇖ n = (if n = 0 then init else xs ! (n - Suc 0))"
by (case_tac n, simp_all add: list_Previous_nth)

lemma ilist_Previous_nth_if: "f⇗← init⇖ n = (if n = 0 then init else f (n - Suc 0))"
by (case_tac n, simp_all add: ilist_Previous_nth)

lemma list_Previous_Cons: "xs⇗←' init⇖ n = (init # xs) ! n"
by (case_tac n, simp_all add: list_Previous_nth)

lemma ilist_Previous_Cons: "f⇗← init⇖ n = ([init] ⌢ f) n"
by (case_tac n, simp_all add: ilist_Previous_nth)

lemma list_Previous_0: "xs⇗←' init⇖ 0 = init"
by (simp add: list_Previous_def)

lemma ilist_Previous_0: "f⇗← init⇖ 0 = init"
by (simp add: ilist_Previous_def)

lemma list_Previous_gr0: "0 < n ⟹ xs⇗←' init⇖ n = xs ! (n - Suc 0)"
by (case_tac n, simp_all add: list_Previous_nth)

lemma ilist_Previous_gr0: "0 < n ⟹ f⇗← init⇖ n = f (n - Suc 0)"
by (case_tac n, simp_all add: ilist_Previous_nth)

lemma list_Previous_Suc: "xs⇗←' init⇖ (Suc n) = xs ! n"
by (simp add: list_Previous_def)

lemma ilist_Previous_Suc: "f⇗← init⇖ (Suc n) = f n"
by (simp add: ilist_Previous_def)

lemma f_Exec_Stream_Previous_f_Exec_Stream_Init: "
f_Exec_Comp_Stream_Init trans_fun xs c ! n =
(f_Exec_Comp_Stream trans_fun xs c)⇗←' c⇖ n"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons list_Previous_Cons)

lemma i_Exec_Stream_Previous_i_Exec_Stream_Init: "
i_Exec_Comp_Stream_Init trans_fun input c n =
(i_Exec_Comp_Stream trans_fun input c)⇗← c⇖ n"
by (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons ilist_Previous_Cons)

lemma f_Exec_Stream_hd: "
0 < length xs ⟹ hd (f_Exec_Comp_Stream trans_fun xs c) = trans_fun (hd xs) c"
by (case_tac xs, simp+)

lemma f_Exec_Stream_nth_0: "
0 < length xs ⟹ (f_Exec_Comp_Stream trans_fun xs c) ! 0= trans_fun (xs ! 0) c"
by (case_tac xs, simp+)

text ‹
The calculation of the n-th result stream element
from the previous result stream element and the current input stream element.›
lemma f_Exec_Stream_nth_gr0_calc: "
⟦ n < length xs; 0 < n ⟧ ⟹
f_Exec_Comp_Stream trans_fun xs c ! n =
trans_fun (xs ! n) (f_Exec_Comp_Stream trans_fun xs c ! (n - 1))"
by (simp add: f_Exec_Stream_nth take_Suc_conv_app_nth f_Exec_append)

lemma f_Exec_Stream_nth_calc_Previous: "
n < length xs ⟹
f_Exec_Comp_Stream trans_fun xs c ! n =
trans_fun (xs ! n) ((f_Exec_Comp_Stream trans_fun xs c)⇗←' c⇖ n)"
apply (case_tac n)
apply (simp add: list_Previous_0 f_Exec_Stream_nth_0)
apply (simp add: list_Previous_def f_Exec_Stream_nth_gr0_calc)
done

lemma i_Exec_Stream_nth_0: "
(i_Exec_Comp_Stream trans_fun input c) 0 = trans_fun (input 0) c"
by (simp add: i_Exec_Stream_nth i_take_first)

lemma i_Exec_Stream_nth_gr0_calc: "
0 < n ⟹
(i_Exec_Comp_Stream trans_fun input c) n =
trans_fun (input n) ((i_Exec_Comp_Stream trans_fun input c) (n - 1))"
by (simp add: i_Exec_Stream_nth i_take_Suc_conv_app_nth f_Exec_append)

text ‹
The component state (and thus its output) at time point @{term "n"}
is computed from the previous state
(the state at time @{term "n-1"} for @{term "n > 0"}
or the initial state for @{term "n = 0"})
and the input at time @{term "n"}.›
lemma i_Exec_Stream_nth_calc_Previous: "
i_Exec_Comp_Stream trans_fun input c n =
trans_fun (input n) ((i_Exec_Comp_Stream trans_fun input c)⇗← c⇖ n)"
by (simp add: i_Exec_Stream_nth ilist_Previous_nth_if i_take_first i_take_Suc_conv_app_nth f_Exec_append)

lemma f_Exec_Stream_Init_nth_Suc_calc: "
n < length xs ⟹
f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n =
trans_fun (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n)"
by (simp add: f_Exec_Stream_Init_eq_f_Exec_Stream_Cons f_Exec_Stream_nth nth_Cons' length_greater_0_conv[THEN iffD1, OF gr_implies_gr0] take_Suc_conv_app_nth f_Exec_append)

lemma f_Exec_Stream_Init_nth_Plus1_calc: "
n < length xs ⟹
f_Exec_Comp_Stream_Init trans_fun xs c ! (n + 1)=
trans_fun (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n)"
by (simp add: f_Exec_Stream_Init_nth_Suc_calc)

lemma f_Exec_Stream_Init_nth_gr0_calc: "
⟦ n ≤ length xs; 0 < n ⟧ ⟹
f_Exec_Comp_Stream_Init trans_fun xs c ! n =
trans_fun (xs ! (n - 1)) (f_Exec_Comp_Stream_Init trans_fun xs c ! (n - 1))"
by (clarsimp simp: gr0_conv_Suc f_Exec_Stream_Init_nth_Suc_calc)

text ‹
At the beginning,
the component state (and thus its output)
for the execution stream with initial state
is represented by the initial state,
contrary to the @{term "i_Exec_Comp_Stream"}
that does not contain the initial state.›

text ‹
The component state (and thus its output) at time point @{term "n + 1"}
for the execution stream with initial state
is computed from the previous state
(the state at time @{term "n"})
and the previous input
(input at time @{term "n"}),
contrary to the @{term "i_Exec_Comp_Stream"},
where each state at time @{term "n"}
represents the resulting state after processing the input at time @{term "n"}.›

lemma i_Exec_Stream_Init_nth_Suc_calc: "
i_Exec_Comp_Stream_Init trans_fun input c (Suc n) =
trans_fun (input n) (i_Exec_Comp_Stream_Init trans_fun input c n)"
by (simp add: i_Exec_Stream_Init_nth i_take_Suc_conv_app_nth f_Exec_append)

lemma i_Exec_Stream_Init_nth_Plus1_calc: "
i_Exec_Comp_Stream_Init trans_fun input c (n + 1) =
trans_fun (input n) (i_Exec_Comp_Stream_Init trans_fun input c n)"
by (simp add: i_Exec_Stream_Init_nth_Suc_calc)

lemma i_Exec_Stream_Init_nth_gr0_calc: "
0 < n ⟹
i_Exec_Comp_Stream_Init trans_fun input c n =
trans_fun (input (n - 1)) (i_Exec_Comp_Stream_Init trans_fun input c (n - 1))"
by (clarsimp simp: gr0_conv_Suc i_Exec_Stream_Init_nth_Suc_calc)

text ‹Correlation between Pre/Post-Conditions for
‹f_Exec_Comp_Stream› and ‹f_Exec_Comp_Stream_Init››

lemma f_Exec_Stream_Pre_Post1: "
⟦ n < length xs;
c_n = (f_Exec_Comp_Stream trans_fun xs c)⇗←' c⇖ n; x_n = xs ! n ⟧ ⟹
(P1 x_n ∧ P2 c_n ⟶ Q (f_Exec_Comp_Stream trans_fun xs c ! n)) =
(P1 x_n ∧ P2 c_n ⟶ Q (trans_fun x_n c_n))"
by (simp add: f_Exec_Stream_nth_calc_Previous)

text ‹Direct relation between input and result after transition›
lemma f_Exec_Stream_Pre_Post2: "
⟦ n < length xs;
c_n = (f_Exec_Comp_Stream trans_fun xs c)⇗←' c⇖ n; x_n = xs ! n ⟧ ⟹
(P c_n ⟶ Q (xs ! n) (f_Exec_Comp_Stream trans_fun xs c ! n)) =
(P c_n ⟶ Q x_n (trans_fun x_n c_n))"
by (simp add: f_Exec_Stream_nth_calc_Previous)

lemma f_Exec_Stream_Pre_Post2_Suc: "
⟦ Suc n < length xs;
c_n = f_Exec_Comp_Stream trans_fun xs c ! n; x_n1 = xs ! Suc n ⟧ ⟹
(P c_n ⟶ Q (xs ! Suc n) (f_Exec_Comp_Stream trans_fun xs c ! Suc n)) =
(P c_n ⟶ Q x_n1 (trans_fun x_n1 c_n))"
by (simp add: f_Exec_Stream_nth_gr0_calc)

lemma f_Exec_Stream_Init_Pre_Post1: "
⟦ n < length xs;
c_n = f_Exec_Comp_Stream_Init trans_fun xs c ! n; x_n = xs ! n ⟧ ⟹
(P1 x_n ∧ P2 c_n ⟶ Q (f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n)) =
(P1 x_n ∧ P2 c_n ⟶ Q (trans_fun x_n c_n))"
by (simp add: f_Exec_Stream_Init_nth_Suc_calc)

text ‹Direct relation between input and state before transition›
lemma f_Exec_Stream_Init_Pre_Post2: "
⟦ n < length xs;
c_n = f_Exec_Comp_Stream_Init trans_fun xs c ! n; x_n = xs ! n ⟧ ⟹
(P (xs ! n) (f_Exec_Comp_Stream_Init trans_fun xs c ! n) ⟶
Q (f_Exec_Comp_Stream_Init trans_fun xs c ! Suc n)) =
(P x_n c_n ⟶ Q (trans_fun x_n c_n))"
by (simp add: f_Exec_Stream_Init_nth_Suc_calc)

lemma i_Exec_Stream_Pre_Post1: "
⟦ c_n = (i_Exec_Comp_Stream trans_fun input c)⇗← c⇖ n; x_n = input n ⟧ ⟹
(P1 x_n ∧ P2 c_n ⟶ Q (i_Exec_Comp_Stream trans_fun input c n)) =
(P1 x_n ∧ P2 c_n ⟶ Q (trans_fun x_n c_n))"
by (simp add: i_Exec_Stream_nth_calc_Previous)

text ‹Direct relation between input and result after transition›
lemma i_Exec_Stream_Pre_Post2: "
⟦ c_n = (i_Exec_Comp_Stream trans_fun input c)⇗← c⇖ n; x_n = input n ⟧ ⟹
(P c_n ⟶ Q (input n) (i_Exec_Comp_Stream trans_fun input c n)) =
(P c_n ⟶ Q x_n (trans_fun x_n c_n))"
by (simp add: i_Exec_Stream_nth_calc_Previous)

lemma i_Exec_Stream_Pre_Post2_Suc: "
⟦ c_n = i_Exec_Comp_Stream trans_fun input c n; x_n1 = input (Suc n) ⟧ ⟹
(P c_n ⟶ Q (input (Suc n)) (i_Exec_Comp_Stream trans_fun input c (Suc n))) =
(P c_n ⟶ Q x_n1 (trans_fun x_n1 c_n))"
by (simp add: i_Exec_Stream_nth_gr0_calc)

lemma i_Exec_Stream_Init_Pre_Post1: "
⟦ c_n = i_Exec_Comp_Stream_Init trans_fun input c n; x_n = input n ⟧ ⟹
(P1 x_n ∧ P2 c_n ⟶ Q (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))) =
(P1 x_n ∧ P2 c_n ⟶ Q (trans_fun x_n c_n))"
by (simp add: i_Exec_Stream_Init_nth_Suc_calc)

text ‹Direct relation between input and state before transition›
lemma i_Exec_Stream_Init_Pre_Post2: "
⟦ c_n = i_Exec_Comp_Stream_Init trans_fun input c n; x_n = input n ⟧ ⟹
(P (input n) (i_Exec_Comp_Stream_Init trans_fun input c n) ⟶
Q (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))) =
(P x_n c_n ⟶ Q (trans_fun x_n c_n))"
by (simp add: i_Exec_Stream_Init_nth_Suc_calc)

text ‹Basic results for stream prefices›

lemma f_Exec_Stream_prefix: "
prefix xs ys ⟹
prefix (f_Exec_Comp_Stream trans_fun xs c)
(f_Exec_Comp_Stream trans_fun ys c)"
by (clarsimp simp: prefix_def f_Exec_Stream_append)

lemma i_Exec_Stream_prefix: "
xs ⊑ input ⟹
f_Exec_Comp_Stream trans_fun xs c ⊑
i_Exec_Comp_Stream trans_fun input c"
by (simp add: iprefix_eq_iprefix_take i_Exec_Stream_take)

lemma f_Exec_N_prefix: "
⟦ n ≤ length xs; prefix xs ys ⟧ ⟹
f_Exec_Comp_N trans_fun n xs c =
f_Exec_Comp_N trans_fun n ys c"
by (simp add: f_Exec_Comp_N_def prefix_imp_take_eq)

theorem f_Exec_Stream_prefix_causal[rule_format]:"
n ≤ length (xs ⊓ ys) ⟹
f_Exec_Comp_Stream trans_fun xs c ↓ n =
f_Exec_Comp_Stream trans_fun ys c ↓ n"
by (rule f_Exec_Stream_causal, rule inf_prefix_take_correct)

lemma f_Exec_Stream_Init_prefix:"
prefix xs ys ⟹
prefix (f_Exec_Comp_Stream_Init trans_fun xs c)
(f_Exec_Comp_Stream_Init trans_fun ys c)"
by (clarsimp simp: prefix_def f_Exec_Stream_Init_append)

lemma i_Exec_Stream_Init_prefix: "
xs ⊑ input ⟹
f_Exec_Comp_Stream_Init trans_fun xs c ⊑
i_Exec_Comp_Stream_Init trans_fun input c"
by (simp add: iprefix_eq_iprefix_take i_Exec_Stream_Init_take)

theorem f_Exec_Stream_Init_prefix_strictly_causal[rule_format]:"
n ≤ length (xs ⊓ ys) ⟹
f_Exec_Comp_Stream_Init trans_fun xs c ↓ Suc n =
f_Exec_Comp_Stream_Init trans_fun ys c ↓ Suc n"
by (rule f_Exec_Stream_Init_strictly_causal, rule inf_prefix_take_correct)

text ‹
A predicate indicating
whether a component is deterministically dependent
on the local state extracted by the the given local state function.›
definition Deterministic_Trans_Fun ::
"('comp, 'input) Comp_Trans_Fun ⇒ ('comp, 'state) Comp_Local_State ⇒ bool"
where "Deterministic_Trans_Fun trans_fun localState ≡
∀c1 c2 x. localState c1 = localState c2 ⟶ trans_fun x c1 = trans_fun x c2"

lemma Deterministic_f_Exec: "
⟦ Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2; xs ≠ [] ⟧ ⟹
f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2"
apply (unfold Deterministic_Trans_Fun_def)
apply (case_tac xs, simp)
apply (rename_tac y ys)
apply (drule_tac x=c1 in spec)
apply (drule_tac x=c2 in spec)
apply simp
done

lemma Deterministic_f_Exec_Stream: "
⟦ Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2 ⟧ ⟹
f_Exec_Comp_Stream trans_fun xs c1 = f_Exec_Comp_Stream trans_fun xs c2"
apply (clarsimp simp: list_eq_iff f_Exec_Stream_nth)
apply (rule Deterministic_f_Exec)
apply (simp add: length_greater_0_conv[THEN iffD1, OF gr_implies_gr0])+
done

lemma Deterministic_i_Exec_Stream: "
⟦ Deterministic_Trans_Fun trans_fun localState; localState c1 = localState c2 ⟧ ⟹
i_Exec_Comp_Stream trans_fun input c1 = i_Exec_Comp_Stream trans_fun input c2"
apply (clarsimp simp: ilist_eq_iff i_Exec_Stream_nth)
apply (rule Deterministic_f_Exec)
apply simp+
done

subsubsection ‹Connected streams›

text ‹
A predicate indicating for two message streams,
that the ports, they correspond to, are connected.
The predicate implies strict causality.›

definition f_Streams_Connected :: "'a fstream_af ⇒ 'a fstream_af ⇒ bool"
where "f_Streams_Connected outS inS ≡ inS = \<NoMsg> # outS"

definition i_Streams_Connected :: "'a istream_af ⇒ 'a istream_af ⇒ bool"
where "i_Streams_Connected outS inS ≡ inS = [\<NoMsg>] ⌢ outS"

lemmas Streams_Connected_defs =
f_Streams_Connected_def
i_Streams_Connected_def

lemma f_Streams_Connected_imp_not_empty: "f_Streams_Connected outS inS ⟹ inS ≠ []"
by (simp add: f_Streams_Connected_def)

lemma f_Streams_Connected_nth_conv: "
f_Streams_Connected outS inS =
(length inS = Suc (length outS) ∧
(∀i<length inS. inS ! i = (case i of 0 ⇒ \<NoMsg> | Suc k ⇒ outS ! k)))"
by (simp add: f_Streams_Connected_def list_eq_iff nth_Cons)

lemma f_Streams_Connected_nth_conv_if: "
f_Streams_Connected outS inS =
(length inS = Suc (length outS) ∧
(∀i<length inS. inS ! i = (if i = 0 then \<NoMsg> else outS ! (i - Suc 0))))"
apply (subst f_Streams_Connected_nth_conv)
apply (rule conj_cong, simp)
apply (rule all_imp_eqI, simp)
apply (rename_tac i, case_tac i, simp+)
done

lemma i_Streams_Connected_nth_conv: "
i_Streams_Connected outS inS =
(∀i. inS i = (case i of 0 ⇒ \<NoMsg> | Suc k ⇒ outS k))"
by (simp add: i_Streams_Connected_def ilist_eq_iff i_append_nth_Cons)

lemma i_Streams_Connected_nth_conv_if: "
i_Streams_Connected outS inS =
(∀i. inS i = (if i = 0 then \<NoMsg> else outS (i - Suc 0)))"
apply (subst i_Streams_Connected_nth_conv)
apply (rule all_eqI)
apply (rename_tac i, case_tac i, simp+)
done

lemma f_Exec_Stream_Init_eq_output_channel: "
⟦ output_fun c = \<NoMsg>;
f_Streams_Connected
(map output_fun (f_Exec_Comp_Stream trans_fun xs c))
channel ⟧ ⟹
map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c) = channel"
by (simp add: f_Streams_Connected_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)

lemma i_Exec_Stream_Init_eq_output_channel: "
⟦ output_fun c = \<NoMsg>;
i_Streams_Connected
(output_fun ∘ (i_Exec_Comp_Stream trans_fun input c))
channel ⟧ ⟹
output_fun ∘ (i_Exec_Comp_Stream_Init trans_fun input c) = channel"
by (simp add: i_Streams_Connected_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)

lemma f_Exec_Stream_output_causal: "
⟦ xs ↓ n = ys ↓ n;
output1 = map output_fun (f_Exec_Comp_Stream trans_fun xs c);
output2 = map output_fun (f_Exec_Comp_Stream trans_fun ys c) ⟧ ⟹
output1 ↓ n = output2 ↓ n"
by (simp add: take_map f_Exec_Stream_causal[of n xs])

lemma f_Exec_Stream_Init_output_strictly_causal: "
⟦ xs ↓ n = ys ↓ n;
output1 = map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c);
output2 = map output_fun (f_Exec_Comp_Stream_Init trans_fun ys c) ⟧ ⟹
output1 ↓ Suc n = output2 ↓ Suc n"
by (simp add: take_map f_Exec_Stream_Init_strictly_causal[of n xs])

lemma i_Exec_Stream_output_causal: "
⟦ input1 ⇓ n = input2 ⇓ n;
output1 = output_fun ∘ i_Exec_Comp_Stream trans_fun input1 c;
output2 = output_fun ∘ i_Exec_Comp_Stream trans_fun input2 c ⟧ ⟹
output1 ⇓ n = output2 ⇓ n"
by (simp add: i_Exec_Stream_causal[of n input1])

lemma i_Exec_Stream_Init_output_strictly_causal: "
⟦ input1 ⇓ n = input2 ⇓ n;
output1 = output_fun ∘ i_Exec_Comp_Stream_Init trans_fun input1 c;
output2 = output_fun ∘ i_Exec_Comp_Stream_Init trans_fun input2 c ⟧ ⟹
output1 ⇓ Suc n = output2 ⇓ Suc n"
by (simp add: i_Exec_Stream_Init_strictly_causal[of n input1])

lemma f_Exec_Stream_Connected_strictly_causal: "
⟦ xs ↓ n = ys ↓ n;
f_Streams_Connected
(map output_fun (f_Exec_Comp_Stream trans_fun xs c))
channel1;
f_Streams_Connected
(map output_fun (f_Exec_Comp_Stream trans_fun ys c))
channel2 ⟧ ⟹
channel1 ↓ Suc n = channel2 ↓ Suc n"
by (simp add: f_Streams_Connected_def take_map f_Exec_Stream_take)

lemma i_Exec_Stream_Connected_strictly_causal: "
⟦ input1 ⇓ n = input2 ⇓ n;
i_Streams_Connected
(portOutput ∘ (i_Exec_Comp_Stream trans_fun input1 c))
channel1;
i_Streams_Connected
(portOutput ∘ (i_Exec_Comp_Stream trans_fun input2 c))
channel2 ⟧ ⟹
channel1 ⇓ Suc n = channel2 ⇓ Suc n"
by (simp add: i_Streams_Connected_def i_take_Suc_Cons i_Exec_Stream_take)

text ‹
A predicate for the semantics with initial state in result stream
indicating for two message streams that the ports, they correspond to, are connected.›
definition f_Streams_Connected_Init :: "'a fstream_af ⇒ 'a fstream_af ⇒ bool"
where "f_Streams_Connected_Init outS inS ≡ inS = outS"

definition i_Streams_Connected_Init :: "'a istream_af ⇒ 'a istream_af ⇒ bool"
where "i_Streams_Connected_Init outS inS ≡ inS = outS"

lemmas Streams_Connected_Init_defs =
f_Streams_Connected_Init_def
i_Streams_Connected_Init_def

lemma f_Streams_Connected_Init_nth_conv: "
f_Streams_Connected_Init outS inS =
(length inS = length outS ∧ (∀i<length inS. inS ! i = outS ! i))"
by (simp add: f_Streams_Connected_Init_def list_eq_iff)

lemma i_Streams_Connected_Init_nth_conv: "
i_Streams_Connected_Init outS inS =
(∀i. inS i = outS i)"
by (simp add: i_Streams_Connected_Init_def ilist_eq_iff)

lemma f_Exec_Stream_Init_eq_output_channel2: "
⟦ output_fun c = \<NoMsg>;
f_Streams_Connected_Init
(map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c))
channel ⟧ ⟹
map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c) = channel"
by (simp add: f_Streams_Connected_Init_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons)
lemma i_Exec_Stream_Init_eq_output_channel2: "
⟦ output_fun c = \<NoMsg>;
i_Streams_Connected_Init
(output_fun ∘ (i_Exec_Comp_Stream_Init trans_fun input c))
channel ⟧ ⟹
output_fun ∘ (i_Exec_Comp_Stream_Init trans_fun input c) = channel"
by (simp add: i_Streams_Connected_Init_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)

lemma f_Exec_Stream_Connected_Init_strictly_causal: "
⟦ xs ↓ n = ys ↓ n;
f_Streams_Connected_Init
(map output_fun (f_Exec_Comp_Stream_Init trans_fun xs c))
channel1;
f_Streams_Connected_Init
(map output_fun (f_Exec_Comp_Stream_Init trans_fun ys c))
channel2 ⟧ ⟹
channel1 ↓ Suc n = channel2 ↓ Suc n"
by (simp add: f_Streams_Connected_Init_def f_Exec_Stream_Init_eq_f_Exec_Stream_Cons take_map f_Exec_Stream_take)

lemma i_Exec_Stream_Connected_Init_strictly_causal: "
⟦ input1 ⇓ n = input2 ⇓ n;
i_Streams_Connected_Init
(portOutput ∘ (i_Exec_Comp_Stream_Init trans_fun input1 c))
channel1;
i_Streams_Connected_Init
(portOutput ∘ (i_Exec_Comp_Stream_Init trans_fun input2 c))
channel2 ⟧ ⟹
channel1 ⇓ Suc n = channel2 ⇓ Suc n"
by (simp add: i_Streams_Connected_Init_def i_Exec_Stream_Init_eq_i_Exec_Stream_Cons i_Exec_Stream_take)

subsubsection ‹Additional auxiliary results›

text ‹The following lemma shows that,
if the system state is different at some time points
with respect to a certain predicate @{term P},
then there exists a defined time point between these two,
where the state change has taken place›

lemma f_State_Change_exists_set: "
⟦ n1 ≤ n2; n1 ∈ I; n2 ∈ I;
¬ P (f_Exec_Comp trans_fun (input ↓ n1) c);
P (f_Exec_Comp trans_fun (input ↓ n2) c) ⟧ ⟹
∃n∈I. n1 ≤ n ∧ n < n2 ∧
¬ P (f_Exec_Comp trans_fun (input ↓ n) c) ∧
P (f_Exec_Comp trans_fun (input ↓ (inext n I)) c)"
by (rule inext_predicate_change_exists)

lemma f_State_Change_exists: "
⟦ n1 ≤ n2;
¬ P (f_Exec_Comp trans_fun (input ↓ n1) c);
P (f_Exec_Comp trans_fun (input ↓ n2) c) ⟧ ⟹
∃n≥n1. n < n2 ∧
¬ P (f_Exec_Comp trans_fun (input ↓ n) c) ∧
P (f_Exec_Comp trans_fun (input ↓ (Suc n)) c)"
by (rule nat_Suc_predicate_change_exists)

lemma i_State_Change_exists_set: "
⟦ n1 ≤ n2; n1 ∈ I; n2 ∈ I;
¬ P (i_Exec_Comp_Stream trans_fun input c n1);
P (i_Exec_Comp_Stream trans_fun input c n2) ⟧ ⟹
∃n∈I. n1 ≤ n ∧ n < n2 ∧
¬ P (i_Exec_Comp_Stream trans_fun input c n) ∧
P (i_Exec_Comp_Stream trans_fun input c (inext n I))"
by (rule inext_predicate_change_exists)

lemma i_State_Change_exists: "
⟦ n1 ≤ n2;
¬ P (i_Exec_Comp_Stream trans_fun input c n1);
P (i_Exec_Comp_Stream trans_fun input c n2) ⟧ ⟹
∃n≥n1. n < n2 ∧
¬ P (i_Exec_Comp_Stream trans_fun input c n) ∧
P (i_Exec_Comp_Stream trans_fun input c (Suc n))"
by (rule nat_Suc_predicate_change_exists)

lemma i_State_Change_Init_exists_set: "
⟦ n1 ≤ n2; n1 ∈ I; n2 ∈ I;
¬ P (i_Exec_Comp_Stream_Init trans_fun input c n1);
P (i_Exec_Comp_Stream_Init trans_fun input c n2) ⟧ ⟹
∃n∈I. n1 ≤ n ∧ n < n2 ∧
¬ P (i_Exec_Comp_Stream_Init trans_fun input c n) ∧
P (i_Exec_Comp_Stream_Init trans_fun input c (inext n I))"
by (rule inext_predicate_change_exists)

lemma i_State_Change_Init_exists: "
⟦ n1 ≤ n2;
¬ P (i_Exec_Comp_Stream_Init trans_fun input c n1);
P (i_Exec_Comp_Stream_Init trans_fun input c n2) ⟧ ⟹
∃n≥n1. n < n2 ∧
¬ P (i_Exec_Comp_Stream_Init trans_fun input c n) ∧
P (i_Exec_Comp_Stream_Init trans_fun input c (Suc n))"
by (rule nat_Suc_predicate_change_exists)

subsection ‹Components with accelerated execution›

text ‹
This section deals with variable execution speed components.
A component accelerated by a (clocking) factor @{term k}
processes streams expanded by factor @{term k}
and its output streams are compressed by factor @{term k}.›

subsubsection ‹Equivalence relation for executions›

text ‹
A predicate indicating for
two components together with transition functions
and a given equivalence predicate for their local states,
that the components exhibit equivalent observable behaviour
after expanding input streams and shrinking output streams
by a constant factor,
given that their local states are equivalent
with respect to the specified equivalence relations.›

definition
Equiv_Exec :: "
'input ⇒
('state1 ⇒ 'state2 ⇒ bool) ⇒ ― ‹Equivalence predicate for local states›
('comp1, 'state1) Comp_Local_State ⇒
('comp2, 'state2) Comp_Local_State ⇒
('input, 'input1) Port_Input_Value ⇒ ― ‹Input adaptor for first component›
('input, 'input2) Port_Input_Value ⇒ ― ‹Input adaptor for second component›
('comp1, 'output) Port_Output_Value ⇒
('comp2, 'output) Port_Output_Value ⇒
('comp1, 'input1 message_af) Comp_Trans_Fun ⇒
('comp2, 'input2 message_af) Comp_Trans_Fun ⇒
nat ⇒ nat ⇒ 'comp1 ⇒ 'comp2 ⇒ bool"
where
"Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ≡
equiv_states (localState1 c1) (localState2 c2) ⟶ (
last_message (map output_fun1 (
f_Exec_Comp_Stream trans_fun1 (input_fun1 m # \<NoMsg>⇗k1 - Suc 0⇖) c1)) =
last_message (map output_fun2 (
f_Exec_Comp_Stream trans_fun2 (input_fun2 m # \<NoMsg>⇗k2 - Suc 0⇖) c2)) ∧
equiv_states
(localState1 (f_Exec_Comp trans_fun1 (input_fun1 m # \<NoMsg>⇗k1 - Suc 0⇖) c1))
(localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # \<NoMsg>⇗k2 - Suc 0⇖) c2)))"

text ‹
Predicate indicating for
two components together with transition functions
and a given equivalence predicate for their local states,
that the equivalence predicate is stable
with respect to component execution,
i.e., it determines the equivalence
of components' local states
both for the initial states and after the components
have processed an arbitrary input.
The restricting version @{term "Equiv_Exec_stable_set"}
guarantees stability only for inputs from a given restriction set,
the not-restricting version guarantees stability for all inputs.›
definition
Equiv_Exec_stable_set :: "
'input set ⇒
('state1 ⇒ 'state2 ⇒ bool) ⇒ ― ‹Equivalence predicate for local states›
('comp1, 'state1) Comp_Local_State ⇒
('comp2, 'state2) Comp_Local_State ⇒
('input, 'input1) Port_Input_Value ⇒ ― ‹Input adaptor for first component›
('input, 'input2) Port_Input_Value ⇒ ― ‹Input adaptor for second component›
('comp1, 'output) Port_Output_Value ⇒
('comp2, 'output) Port_Output_Value ⇒
('comp1, 'input1 message_af) Comp_Trans_Fun ⇒
('comp2, 'input2 message_af) Comp_Trans_Fun ⇒
nat ⇒ nat ⇒ 'comp1 ⇒ 'comp2 ⇒ bool"
where
"Equiv_Exec_stable_set A
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ≡
∀input m. set input ⊆ A ∧ m ∈ A ⟶
Equiv_Exec m
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2
(f_Exec_Comp trans_fun1 (map input_fun1 input ⊙⇩f k1) c1)
(f_Exec_Comp trans_fun2 (map input_fun2 input ⊙⇩f k2) c2)"

definition
Equiv_Exec_stable :: "
('state1 ⇒ 'state2 ⇒ bool) ⇒ ― ‹Equivalence predicate for local states›
('comp1, 'state1) Comp_Local_State ⇒
('comp2, 'state2) Comp_Local_State ⇒
('input, 'input1) Port_Input_Value ⇒ ― ‹Input adaptor for first component›
('input, 'input2) Port_Input_Value ⇒ ― ‹Input adaptor for second component›
('comp1, 'output) Port_Output_Value ⇒
('comp2, 'output) Port_Output_Value ⇒
('comp1, 'input1 message_af) Comp_Trans_Fun ⇒
('comp2, 'input2 message_af) Comp_Trans_Fun ⇒
nat ⇒ nat ⇒ 'comp1 ⇒ 'comp2 ⇒ bool"
where
"Equiv_Exec_stable
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ≡
∀input m.
Equiv_Exec m
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2
(f_Exec_Comp trans_fun1 (map input_fun1 input ⊙⇩f k1) c1)
(f_Exec_Comp trans_fun2 (map input_fun2 input ⊙⇩f k2) c2)"

lemma Equiv_Exec_equiv_statesI: "
⟦ equiv_states (localState1 c1) (localState2 c2);
Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ⟧ ⟹
equiv_states
(localState1 (f_Exec_Comp trans_fun1 (input_fun1 m # \<NoMsg>⇗k1 - Suc 0⇖) c1))
(localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # \<NoMsg>⇗k2 - Suc 0⇖) c2))"
by (simp add: Equiv_Exec_def)

lemma Equiv_Exec_output_eqI: "
⟦ equiv_states (localState1 c1) (localState2 c2);
Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ⟧ ⟹
last_message (map output_fun1 (
f_Exec_Comp_Stream trans_fun1 (input_fun1 m # \<NoMsg>⇗k1 - Suc 0⇖) c1)) =
last_message (map output_fun2 (
f_Exec_Comp_Stream trans_fun2 (input_fun2 m # \<NoMsg>⇗k2 - Suc 0⇖) c2))"
by (simp add: Equiv_Exec_def)

lemma Equiv_Exec_equiv_statesI': "
⟦ equiv_states (localState1 c1) (localState2 c2);
Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ⟧ ⟹
equiv_states
(localState1 (f_Exec_Comp trans_fun1 NoMsg⇗k1 - Suc 0⇖ (trans_fun1 (input_fun1 m) c1)))
(localState2 (f_Exec_Comp trans_fun2 NoMsg⇗k2 - Suc 0⇖ (trans_fun2 (input_fun2 m) c2)))"
by (simp add: Equiv_Exec_def)

lemma Equiv_Exec_le1: "
⟦ k1 ≤ Suc 0; k2 ≤ Suc 0;
equiv_states (localState1 c1) (localState2 c2);
Equiv_Exec m
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ⟧ ⟹
output_fun1 (trans_fun1 (input_fun1 m) c1) =
output_fun2 (trans_fun2 (input_fun2 m) c2) ∧
equiv_states
(localState1 (trans_fun1 (input_fun1 m) c1))
(localState2 (trans_fun2 (input_fun2 m) c2))"
by (simp add: Equiv_Exec_def)

lemma Equiv_Exec_stable_set_UNIV: "
Equiv_Exec_stable_set
UNIV equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 =
Equiv_Exec_stable
equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2"
by (simp add: Equiv_Exec_stable_set_def Equiv_Exec_stable_def)

lemma Equiv_Exec_stable_setI: "
⟦ Equiv_Exec_stable_set A
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2;
set input ⊆ A; m ∈ A ⟧ ⟹
Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2
(f_Exec_Comp trans_fun1 (map input_fun1 input ⊙⇩f k1) c1)
(f_Exec_Comp trans_fun2 (map input_fun2 input ⊙⇩f k2) c2)"
by (simp add: Equiv_Exec_stable_set_def)

lemma Equiv_Exec_stableI: "
Equiv_Exec_stable
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 ⟹
Equiv_Exec m
equiv_states localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2
(f_Exec_Comp trans_fun1 (map input_fun1 input ⊙⇩f k1) c1)
(f_Exec_Comp trans_fun2 (map input_fun2 input ⊙⇩f k2) c2)"
by (simp add: Equiv_Exec_stable_def)

text ‹Reflexitity, symmetry and transitivity results for @{term "Equiv_Exec"}›

lemma Equiv_Exec_refl: "
⟦ ⋀c. equiv_states (localState c) (localState c) ⟧ ⟹
Equiv_Exec
m equiv_states
localState localState input_fun input_fun output_fun output_fun
trans_fun trans_fun k k c c"
by (simp add: Equiv_Exec_def)

lemma Equiv_Exec_sym[rule_format]: "
⟦ ∀c1 c2.
equiv_states (localState1 c1) (localState2 c2) =
equiv_states (localState2 c2) (localState1 c1) ⟧ ⟹
Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 =
Equiv_Exec
m equiv_states
localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1
trans_fun2 trans_fun1 k2 k1 c2 c1"
by (fastforce simp: Equiv_Exec_def)

lemma Equiv_Exec_sym2: "
⟦ equiv_states_sym = (λs1 s2. equiv_states s2 s1) ⟧ ⟹
Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 =
Equiv_Exec
m equiv_states_sym
localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1
trans_fun2 trans_fun1 k2 k1 c2 c1"
by (fastforce simp: Equiv_Exec_def)

lemma Equiv_Exec_sym2_ex: "
∃equiv_states_sym.
Equiv_Exec
m equiv_states
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2 =
Equiv_Exec
m equiv_states_sym
localState2 localState1 input_fun2 input_fun1 output_fun2 output_fun1
trans_fun2 trans_fun1 k2 k1 c2 c1"
by (rule exI, rule Equiv_Exec_sym2, simp)

lemma Equiv_Exec_trans: "
⟦ Equiv_Exec
m equiv_states12
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2;
Equiv_Exec
m equiv_states23
localState2 localState3 input_fun2 input_fun3 output_fun2 output_fun3
trans_fun2 trans_fun3 k2 k3 c2 c3;
equiv_states13 = (λs1 s3. (
if s1 = localState1 c1 ∧ s3 = localState3 c3 then
equiv_states12 s1 (localState2 c2) ∧
equiv_states23 (localState2 c2) s3
else
equiv_states12 s1 (
localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # \<NoMsg>⇗k2 - Suc 0⇖) c2))) ∧
equiv_states23 (
localState2 (f_Exec_Comp trans_fun2 (input_fun2 m # \<NoMsg>⇗k2 - Suc 0⇖) c2)) s3) ⟧ ⟹
Equiv_Exec
m equiv_states13
localState1 localState3 input_fun1 input_fun3 output_fun1 output_fun3
trans_fun1 trans_fun3 k1 k3 c1 c3"
by (fastforce simp: Equiv_Exec_def)

lemma Equiv_Exec_trans_ex: "
⟦ Equiv_Exec
m equiv_states12
localState1 localState2 input_fun1 input_fun2 output_fun1 output_fun2
trans_fun1 trans_fun2 k1 k2 c1 c2;
Equiv_Exec
m equiv_states23
localState2 localState3 input_fun2 input_fun3 output_fun2 output_fun3
trans_fun2 trans_fun3 k2 k3 c2 c3 ⟧ ⟹
∃equiv_states13. Equiv_Exec
m equiv_states13
localState1 localState3 input_fun1 input_fun3 output_fun1 output_fun3
trans_fun1 trans_fun3 k1 k3 c1 c3"
by (blast intro: Equiv_Exec_trans)

text ‹A predicate indicating for
a given local state extraction function and
a given transition function,
that components, whose states are equal with regard to the
local state extraction function,
are transformed into equal componenents,
when the transition function is applied with the same input.›
definition Exec_Equal_State ::
"('comp, 'state) Comp_Local_State ⇒ ('comp, 'input message_af) Comp_Trans_Fun ⇒ bool"
where "Exec_Equal_State localState trans_fun ≡
∀c1 c2 m. localState c1 = localState c2 ⟶ trans_fun m c1 = trans_fun m c2"

lemma Exec_Equal_StateD: "
⟦ Exec_Equal_State localState trans_fun;
localState c1 = localState c2 ⟧ ⟹
trans_fun m c1 = trans_fun m c2"
by (unfold Exec_Equal_State_def, blast)

lemma Exec_Equal_StateD': "
Exec_Equal_State localState trans_fun ⟹
∀c1 c2 m. localState c1 = localState c2 ⟶ trans_fun m c1 = trans_fun m c2"
by (unfold Exec_Equal_State_def, blast)

lemma Exec_Equal_StateI: "
(⋀c1 c2 m. localState c1 = localState c2 ⟹ trans_fun m c1 = trans_fun m c2)
⟹ Exec_Equal_State localState trans_fun"
by (unfold Exec_Equal_State_def, blast)

lemma f_Exec_Equal_State: "⋀c1 c2.
⟦ Exec_Equal_State localState trans_fun;
localState c1 = localState c2; xs ≠ [] ⟧ ⟹
f_Exec_Comp trans_fun xs c1 = f_Exec_Comp trans_fun xs c2"
apply (induct xs, simp)
apply (case_tac "xs = []")
apply simp
apply (rule Exec_Equal_StateD, assumption+)
apply (drule_tac x="trans_fun a c1" in meta_spec)
apply (drule_tac x="trans_fun a c2" in meta_spec)
apply (drule_tac ?c1.0=c1 and ?c2.0=c2 and m=a in Exec_Equal_StateD, assumption)
apply simp
done

lemma f_Exec_Stream_Equal_State: "
⟦ Exec_Equal_State localState trans_fun;
localState c1 = localState c2 ⟧ ⟹
f_Exec_Comp_Stream trans_fun xs c1 =
f_Exec_Comp_Stream trans_fun xs c2"
apply (clarsimp simp: list_eq_iff f_Exec_Stream_nth)
apply (drule gr_implies_gr0)
apply (rule f_Exec_Equal_State)
apply simp+
done

lemma i_Exec_Stream_Equal_State: "
⟦ Exec_Equal_State localState trans_fun;
localState c1 = localState c2 ⟧ ⟹
i_Exec_Comp_Stream trans_fun input c1 =
i_Exec_Comp_Stream trans_fun input c2"
apply (clarsimp simp: ilist_eq_iff i_Exec_Stream_nth)
apply (rule f_Exec_Equal_State)
apply simp+
done

subsubsection ‹Idle states›

definition State_Idle ::
"('comp, 'state) Comp_Local_State ⇒ ('comp ⇒ 'output message_af) ⇒
('comp, 'input message_af) Comp_Trans_Fun ⇒ 'state ⇒ bool"
where "State_Idle localState output_fun trans_fun state ≡
∀c. localState c = state ⟶
localState (trans_fun \<NoMsg> c) = state ∧
output_fun (trans_fun \<NoMsg> c) = \<NoMsg>"

lemma State_IdleD: "
⟦ State_Idle localState output_fun trans_fun state;
localState c = state ⟧ ⟹
localState (trans_fun \<NoMsg> c) = state ∧
output_fun (trans_fun \<NoMsg> c) = \<NoMsg>"
by (unfold State_Idle_def, blast)

lemma State_IdleD': "
State_Idle localState output_fun trans_fun state ⟹
∀c. localState c = state ⟶
localState (trans_fun \<NoMsg> c) = state ∧
output_fun (trans_fun \<NoMsg> c) = \<NoMsg>"
by (unfold State_Idle_def, blast)

lemma State_IdleI: "
⟦ ⋀c. localState c = state ⟹
localState (trans_fun \<NoMsg> c) = state ∧
output_fun (trans_fun \<NoMsg> c) = \<NoMsg> ⟧ ⟹
State_Idle localState output_fun trans_fun state"
by (unfold State_Idle_def, blast)

lemma State_Idle_step[rule_format]: "
⟦ State_Idle localState output_fun trans_fun (localState c) ⟧ ⟹
State_Idle localState output_fun trans_fun (localState (trans_fun \<NoMsg> c))"
apply (frule State_IdleD[OF _ refl], erule conjE)
apply (rule State_IdleI, rename_tac c0)
apply (drule_tac c=c0 in State_IdleD)
apply simp+
done

lemma f_Exec_State_Idle_replicate_NoMsg_state[rule_format]: "
⋀c. State_Idle localState output_fun trans_fun (localState c) ⟹
localState (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c) = localState c"
apply (induct n, simp)
apply (frule State_Idle_step)
apply (drule_tac c=c in State_IdleD, rule refl)
apply simp
done

lemma f_Exec_State_Idle_replicate_NoMsg_gr0_output[rule_format]: "⋀c.
⟦ State_Idle localState output_fun trans_fun (localState c); 0 < n ⟧ ⟹
output_fun (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c) = \<NoMsg>"
apply (induct n, simp)
apply (case_tac "n = 0")
apply simp
apply (rule State_IdleD[THEN conjunct2], assumption, simp)
apply (drule State_Idle_step)
apply simp
done

lemma f_Exec_State_Idle_replicate_NoMsg_output[rule_format]: "
⟦ State_Idle localState output_fun trans_fun (localState c);
output_fun c = \<NoMsg> ⟧ ⟹
output_fun (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c) = \<NoMsg>"
apply (case_tac "n = 0", simp)
apply (simp add: f_Exec_State_Idle_replicate_NoMsg_gr0_output)
done

lemma f_Exec_Stream_State_Idle_replicate_NoMsg_output[rule_format]: "
⟦ State_Idle localState output_fun trans_fun (localState c) ⟧ ⟹
map output_fun (f_Exec_Comp_Stream trans_fun \<NoMsg>⇗n⇖ c) = \<NoMsg>⇗n⇖"
by (simp add: list_eq_iff f_Exec_Stream_nth min_eqL f_Exec_State_Idle_replicate_NoMsg_gr0_output del: replicate.simps)

corollary f_Exec_State_Idle_append_replicate_NoMsg_state: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun xs c)) ⟧ ⟹
localState (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗n⇖) c) =
localState (f_Exec_Comp trans_fun xs c)"
by (simp add: f_Exec_append f_Exec_State_Idle_replicate_NoMsg_state)

corollary f_Exec_State_Idle_append_replicate_NoMsg_ge_state: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗m⇖) c));
m ≤ n ⟧ ⟹
localState (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗n⇖) c) =
localState (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗m⇖) c)"
apply (rule_tac t=n and s="m + (n - m)" in subst, simp)
apply (simp only: replicate_add append_assoc[symmetric])
apply (rule f_Exec_State_Idle_append_replicate_NoMsg_state, simp)
done

corollary f_Exec_State_Idle_replicate_NoMsg_ge_state: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun \<NoMsg>⇗m⇖ c));
m ≤ n ⟧ ⟹
localState (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c) =
localState (f_Exec_Comp trans_fun \<NoMsg>⇗m⇖ c)"
by (cut_tac f_Exec_State_Idle_append_replicate_NoMsg_ge_state[where xs="[]"], simp+)

corollary f_Exec_State_Idle_append_replicate_NoMsg_gr0_output: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun xs c));
0 < n ⟧ ⟹
output_fun (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗n⇖) c) = \<NoMsg>"
by (simp add: f_Exec_append f_Exec_State_Idle_replicate_NoMsg_gr0_output)

corollary f_Exec_Stream_State_Idle_append_replicate_NoMsg_gr0_output: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun xs c)) ⟧ ⟹
map output_fun (f_Exec_Comp_Stream trans_fun (xs @ \<NoMsg>⇗n⇖) c) =
map output_fun (f_Exec_Comp_Stream trans_fun xs c) @ \<NoMsg>⇗n⇖"
by (simp add: f_Exec_Stream_append f_Exec_Stream_State_Idle_replicate_NoMsg_output)

corollary f_Exec_State_Idle_append_replicate_NoMsg_gr_output: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗m⇖) c));
m < n ⟧ ⟹
output_fun (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗n⇖) c) = \<NoMsg>"
apply (rule_tac t=n and s="m + (n - m)" in subst, simp)
apply (simp only: replicate_add append_assoc[symmetric])
apply (rule f_Exec_State_Idle_append_replicate_NoMsg_gr0_output, simp+)
done

corollary f_Exec_State_Idle_append_replicate_NoMsg_ge_output: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗m⇖) c));
output_fun (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗m⇖) c) = \<NoMsg>; m ≤ n ⟧ ⟹
output_fun (f_Exec_Comp trans_fun (xs @ \<NoMsg>⇗n⇖) c) = \<NoMsg>"
by (fastforce simp: order_le_less f_Exec_State_Idle_append_replicate_NoMsg_gr_output)

corollary f_Exec_State_Idle_replicate_NoMsg_gr_output: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun \<NoMsg>⇗m⇖ c));
m < n ⟧ ⟹
output_fun (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c) = \<NoMsg>"
by (cut_tac xs="[]" in f_Exec_State_Idle_append_replicate_NoMsg_gr_output, simp+)

corollary f_Exec_State_Idle_replicate_NoMsg_ge_output: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun \<NoMsg>⇗m⇖ c));
output_fun (f_Exec_Comp trans_fun \<NoMsg>⇗m⇖ c) = \<NoMsg>; m ≤ n ⟧ ⟹
output_fun (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c) = \<NoMsg>"
by (fastforce simp: order_le_less f_Exec_State_Idle_replicate_NoMsg_gr_output)

lemma State_Idle_append_replicate_NoMsg_output_last_message: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun xs c)) ⟧ ⟹
last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs @ \<NoMsg>⇗n⇖) c)) =
last_message (map output_fun (f_Exec_Comp_Stream trans_fun xs c))"
by (simp add: f_Exec_Stream_State_Idle_append_replicate_NoMsg_gr0_output last_message_append_replicate_NoMsg)

lemma State_Idle_append_replicate_NoMsg_output_Msg_eq_last_message: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun xs c));
output_fun (f_Exec_Comp trans_fun xs c) ≠ \<NoMsg>;
xs ≠ [] ⟧ ⟹
last_message (map output_fun (f_Exec_Comp_Stream trans_fun (xs @ \<NoMsg>⇗n⇖) c)) =
output_fun (f_Exec_Comp trans_fun xs c)"
apply (simp add: State_Idle_append_replicate_NoMsg_output_last_message f_Exec_eq_f_Exec_Stream_last2 )
apply (subst last_message_Msg_eq_last)
apply (simp add: map_last f_Exec_Stream_not_empty_conv)+
done

corollary State_Idle_output_Msg_eq_last_message: "
⟦ State_Idle localState output_fun trans_fun (
localState (f_Exec_Comp trans_fun xs c));
output_fun (f_Exec_Comp trans_fun xs c) ≠ \<NoMsg>;
xs ≠ [] ⟧ ⟹
last_message (map output_fun (f_Exec_Comp_Stream trans_fun xs c)) =
output_fun (f_Exec_Comp trans_fun xs c)"
by (rule_tac n=0 in subst[OF State_Idle_append_replicate_NoMsg_output_Msg_eq_last_message, rule_format], simp+)

lemma State_Idle_imp_exists_state_change: "
⟦ ¬ State_Idle localState output_fun trans_fun (localState c);
State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c)) ⟧ ⟹
∃i<n. (
¬ State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>⇗i⇖ c)) ∧ (
∀j≤n. i < j ⟶ State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>⇗j⇖ c))))"
apply (cut_tac
a=0 and b=n and
P="λx. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg⇗x⇖ c))"
in nat_Suc_predicate_change_exists, simp+)
apply (clarify, rename_tac n1)
apply (rule_tac x=n1 in exI)
apply clarsimp
apply (rule_tac t="j" and s="Suc n1 + (j - Suc n1)" in subst, simp)
done

lemma State_Idle_imp_exists_state_change2: "
⟦ ¬ State_Idle localState output_fun trans_fun (localState c);
State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>⇗n⇖ c)) ⟧ ⟹
∃i<n. (
(∀j≤i. ¬ State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>⇗i⇖ c))) ∧
(∀j≤n. i < j ⟶ State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun \<NoMsg>⇗j⇖ c))))"
apply (frule State_Idle_imp_exists_state_change, assumption)
apply (clarify, rename_tac i)
apply (rule_tac x=i in exI)
apply simp
done

subsubsection ‹Basic definitions for accelerated execution›

text ‹Stream processing with accelerated components›

definition f_Exec_Comp_Stream_Acc_Output ::
"nat ⇒ ― ‹Acceleration factor›
('comp ⇒ 'output message_af) ⇒ ― ‹Output extraction function›
('comp, 'input message_af) Comp_Trans_Fun ⇒
'input fstream_af ⇒ 'comp ⇒
'output fstream_af"
where "f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c ≡
(map output_fun (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) ÷⇩f k"

definition f_Exec_Comp_Stream_Acc_LocalState ::
"nat ⇒ ― ‹Acceleration factor›
('comp ⇒ 'state) ⇒ ― ‹Local state extraction function›
('comp, 'input message_af) Comp_Trans_Fun ⇒
'input fstream_af ⇒ 'comp ⇒
'state list"
where "f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c ≡
(map localState (f_Exec_Comp_Stream trans_fun (xs ⊙⇩f k) c)) ÷⇘fl⇙ k"

definition i_Exec_Comp_Stream_Acc_Output ::
"nat ⇒ ― ‹Acceleration factor›
('comp ⇒ 'output message_af) ⇒ ― ‹Output extraction function›
('comp, 'input message_af) Comp_Trans_Fun ⇒
'input istream_af ⇒ 'comp ⇒
'output istream_af"
where "i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c ≡
(output_fun ∘ (i_Exec_Comp_Stream trans_fun (input ⊙⇩i k) c)) ÷⇩i k"

definition i_Exec_Comp_Stream_Acc_LocalState ::
"nat ⇒ ― ‹Acceleration factor›
('comp ⇒ 'state) ⇒ ― ‹Local state extraction function›
('comp, 'input message_af) Comp_Trans_Fun ⇒
'input istream_af ⇒ 'comp ⇒
'state ilist"
where "i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c