Theory IL_AF_Stream

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

section ‹\textsc{AutoFocus} message streams and temporal logic on intervals›

theory IL_AF_Stream
imports Main "Nat-Interval-Logic.IL_TemporalOperators" AF_Stream
begin


subsection ‹Stream views -- joining streams and intervals›

subsubsection ‹Basic definitions›

primrec f_join_aux :: "'a list ⇒ nat ⇒ iT ⇒ 'a list"
where
  "f_join_aux [] n I = []"
| "f_join_aux (x # xs) n I =
    (if n ∈ I then [x] else []) @ f_join_aux xs (Suc n) I"

text ‹
  The functions ‹f_join› and ‹i_join›
  deliver views of finite and infinite streams through intervals
  (more exactly: arbitrary natural sets).
  A stream view contains only the elements of the original stream
  at positions, which are contained in the interval.
  For instance, ‹f_join [0,10,20,30,40] {1,4} = [10,40]››

definition f_join :: "'a list ⇒ iT ⇒ 'a list"      (infixl ‹⋈⇩f› 100)
  where "xs ⋈⇩f I ≡ f_join_aux xs 0 I"

definition i_join :: "'a ilist ⇒ iT ⇒ 'a ilist"    (infixl ‹⋈⇩i› 100)
  where "f ⋈⇩i I ≡ λn. (f (I → n))"

notation
  f_join  (infixl ‹⋈⇩› 100) and
  i_join  (infixl ‹⋈⇩› 100)

text ‹
  The function ‹i_f_join› can be used for the case,
  when an infinite stream is joined with a finite interval.
  The function ‹i_join› would then deliver
  an infinite stream, whose elements after position ‹card I›
  are equal to initial stream's element at position ‹Max I›.
  The function ‹i_f_join› in contrast
  cuts the resulting stream at this position
  and returns a finite stream.›

definition i_f_join :: "'a ilist ⇒ iT ⇒ 'a list"    (infixl ‹⋈⇘i-f⇙› 100)
  where "f ⋈⇘i-f⇙ I ≡ f ⇓ Suc (Max I) ⋈⇩f I"
notation
  i_f_join  (infixl ‹⋈⇩› 100)

text ‹
  The function ‹i_f_join› should be used
  only for finite sets in order to deliver well-defined results.
  The function ‹i_join› should be used for infinite sets,
  because joining an infinite stream ‹s› and a finite set ‹I›
  using ‹i_join› would deliver an infinite stream,
  ending with an infinite sequence of elements equal to
  ‹s (Max I)›.›


subsubsection ‹Basic results›

lemma f_join_aux_length: "
  ⋀n. length (f_join_aux xs n I) = card (I ∩ {n..<n + length xs})"
apply (induct xs, simp)
apply (simp add: atLeastLessThan_def)
apply (rule_tac t="{n..}" and s="insert n {Suc n..}" in subst, fastforce)
apply simp
done

lemma f_join_aux_nth[rule_format]: "
  ∀n i. i < card (I ∩ {n..<n + length xs}) ⟶
  (f_join_aux xs n I) ! i = xs ! (((I ∩ {n..<n + length xs}) → i) - n)"
apply (induct xs, simp)
apply (clarsimp split del: if_split)
apply (subgoal_tac "{n..<Suc (n + length xs)} = insert n {Suc n..<Suc (n + length xs)}")
 prefer 2
 apply fastforce
apply (frule card_gr0_imp_not_empty[OF gr_implies_gr0])
apply (case_tac "n ∈ I")
 prefer 2
 apply (simp add: nth_Cons')
 apply (subgoal_tac "Suc n ≤ (I ∩ {Suc n..<Suc (n + length xs)}) → i", simp)
 apply (rule order_trans[OF _ iMin_le[OF inext_nth_closed]])
  apply (rule order_trans[OF _ iMin_Int_ge2])
   apply (subgoal_tac "n < n + length xs")
    prefer 2
    apply (rule ccontr, simp)
   apply (simp add: iMin_atLeastLessThan)
  apply assumption+
apply simp
apply (case_tac "I ∩ {Suc n..<Suc (n + length xs)} = {}", simp)
apply (case_tac i)
 apply (simp add: iMin_insert)
apply (subgoal_tac "Suc n ≤ iMin {Suc n..<Suc (n + length xs)}")
 prefer 2
 apply (subgoal_tac "n < n + length xs")
  prefer 2
  apply (rule ccontr, simp)
 apply (simp add: iMin_atLeastLessThan)
apply (rename_tac i1)
apply (simp del: inext_nth.simps)
apply (subst inext_nth_insert_Suc)
   apply simp
  apply (rule Suc_le_lessD)
  apply (rule order_trans[OF _ iMin_Int_ge2])
  apply assumption+
apply (simp add: nth_Cons')
apply (subgoal_tac "Suc n ≤ (I ∩ {Suc n..<Suc (n + length xs)}) → i1", simp)
apply (rule order_trans[OF _ iMin_le[OF inext_nth_closed]])
 apply (rule order_trans[OF _ iMin_Int_ge2])
 apply assumption+
done



text ‹Joining finite streams and intervals›

(*<*)
(*
lemma "[(0::nat),10,20,30,40] ⋈⇩f {1,4} = [10,40]"
by (simp add: f_join_def)
*)
(*>*)

lemma f_join_length: "length (xs ⋈⇩f I) = card (I ↓< length xs)"
by (simp add: f_join_def f_join_aux_length atLeast0LessThan cut_less_Int_conv)

lemma f_join_nth: "n < length (xs ⋈⇩f I) ⟹ (xs ⋈⇩f I) ! n = xs ! (I → n)"
apply (simp add: f_join_length)
apply (unfold f_join_def)
apply (drule back_subst[OF _ cut_less_Int_conv])
apply (simp add: f_join_aux_nth atLeast0LessThan cut_less_Int_conv[symmetric] inext_nth_cut_less_eq)
done

lemma f_join_nth2: "n < card (I ↓< length xs) ⟹ (xs ⋈⇩f I) ! n = xs ! (I → n)"
by (simp add: f_join_nth f_join_length)

lemma f_join_empty: "xs ⋈⇩f {} = []"
by (simp add: length_0_conv[symmetric] f_join_length cut_less_empty del: length_0_conv)

lemma f_join_Nil: "[] ⋈⇩f I = []"
by (simp add: length_0_conv[symmetric] f_join_length cut_less_0_empty del: length_0_conv)

lemma f_join_Nil_conv: "(xs ⋈⇩f I = []) = (I ↓< length xs = {})"
by (simp add: length_0_conv[symmetric] f_join_length card_0_eq[OF nat_cut_less_finite] del: length_0_conv)

lemma f_join_Nil_conv': "(xs ⋈⇩f I = []) = (∀i<length xs. i ∉ I)"
by (fastforce simp: f_join_Nil_conv)

lemma f_join_all_conv: "(xs ⋈⇩f I = xs) = ({..<length xs} ⊆ I)"
apply (case_tac "length xs = 0", simp add: f_join_Nil)
apply (rule iffI)
 apply (rule subsetI, rename_tac t)
 apply (clarsimp simp: list_eq_iff[of _ xs] f_join_length)
 apply (rule ccontr)
 apply (subgoal_tac "I ↓< length xs ⊂ {..<length xs}")
  prefer 2
  apply blast
 apply (drule psubset_card_mono[OF finite_lessThan])
 apply simp
apply (subgoal_tac "length (xs ⋈⇩f I) = length xs")
 prefer 2
 apply (simp add: f_join_length cut_less_Int_conv Int_absorb1)
apply (clarsimp simp: list_eq_iff[of _ xs] f_join_nth)
apply (rule arg_cong[where f="(!) xs"])
apply (subgoal_tac "I ↓< length xs = {..<length xs}")
 prefer 2
 apply fastforce
apply (subst inext_nth_cut_less_eq[where t="length xs", symmetric], simp)
apply (simp add: inext_nth_lessThan)
done

lemma f_join_all: "{..<length xs} ⊆ I ⟹ xs ⋈⇩f I = xs"
by (rule f_join_all_conv[THEN iffD2])

corollary f_join_UNIV: "xs ⋈⇩f UNIV = xs"
by (simp add: f_join_all)

lemma f_join_union: "
  ⟦ finite A; Max A < iMin B ⟧ ⟹ xs ⋈⇩f (A ∪ B) = xs ⋈⇩f A @ (xs ⋈⇩f B)"
apply (case_tac "A = {}", simp add: f_join_empty)
apply (case_tac "B = {}", simp add: f_join_empty)
apply (frule Max_less_iMin_imp_disjoint, assumption)
apply (simp add: list_eq_iff f_join_length cut_less_Un del: Max_less_iff)
apply (subgoal_tac "A ↓< length xs ∩ B ↓< length xs = {}")
 prefer 2
 apply (simp add: cut_less_Int[symmetric] cut_less_empty)
apply (frule card_Un_disjoint[OF nat_cut_less_finite nat_cut_less_finite])
apply (clarsimp simp del: Max_less_iff)
apply (subst f_join_nth)
 apply (simp add: f_join_length cut_less_Un)
apply (simp add: nth_append f_join_length del: Max_less_iff, intro conjI impI)
 apply (simp add: f_join_nth f_join_length del: Max_less_iff)
   apply (rule ssubst[OF inext_nth_card_append_eq1], assumption)
  apply (rule order_less_le_trans[OF _ cut_less_card], assumption+)
 apply simp
apply (subst f_join_nth)
 apply (simp add: f_join_length)
apply (subgoal_tac "iMin B < length xs")
 prefer 2
 apply (rule ccontr)
 apply (simp add: linorder_not_less cut_less_Min_empty)
apply (frule order_less_trans, assumption)
apply (rule arg_cong[where f="λx. xs ! x"])
apply (simp add: cut_less_Max_all inext_nth_card_append_eq2)
done

lemma f_join_singleton_if: "
  xs ⋈⇩f {n} = (if n < length xs then [xs ! n] else [])"
apply (clarsimp simp: list_eq_iff f_join_length cut_less_singleton)
apply (insert f_join_nth[of 0 xs "{n}"])
apply (simp add: f_join_length cut_less_singleton)
done

lemma f_join_insert: "
  n < length xs ⟹
  xs ⋈⇩f insert n I = xs ⋈⇩f (I ↓< n) @ (xs ! n) # (xs ⋈⇩f (I ↓> n))"
apply (rule_tac t="insert n I" and s="(I ↓< n) ∪ {n} ∪ (I ↓> n)" in subst, fastforce)
apply (insert nat_cut_less_finite[of I n])
apply (case_tac "I ↓> n = {}")
 apply (simp add: f_join_empty del: Un_insert_right)
 apply (case_tac "I ↓< n = {}")
  apply (simp add: f_join_empty f_join_singleton_if)
 apply (subgoal_tac "Max (I ↓< n) < iMin {n}")
  prefer 2
  apply (simp add: cut_less_mem_iff)
 apply (simp add: f_join_union f_join_singleton_if del: Un_insert_right)
apply (subgoal_tac "Max {n} < iMin (I ↓> n)")
 prefer 2
 apply (simp add: iMin_gr_iff cut_greater_mem_iff)
apply (case_tac "I ↓< n = {}")
 apply (simp add: f_join_empty f_join_union f_join_singleton_if del: Un_insert_left)
apply (subgoal_tac "Max (I ↓< n) < iMin {n}")
 prefer 2
 apply (simp add: cut_less_mem_iff)
apply (subgoal_tac "Max (I ↓< n ∪ {n}) < iMin (I ↓> n)")
 prefer 2
 apply (simp add: iMin_gr_iff i_cut_mem_iff)
apply (simp add: f_join_union f_join_singleton_if del: Un_insert_right)
done

lemma f_join_snoc: "
  (xs @ [x]) ⋈⇩f I =
  xs ⋈⇩f I @ (if length xs ∈ I then [x] else [])"
apply (simp add: list_eq_iff f_join_length)
apply (subgoal_tac "
  card (I ↓< Suc (length xs)) =
  card (I ↓< length xs) + (if length xs ∈ I then Suc 0 else 0)")
 prefer 2
 apply (simp add: nat_cut_le_less_conv[symmetric] cut_le_less_conv_if)
 apply (simp add: card_insert_if[OF nat_cut_less_finite] cut_less_mem_iff)
apply simp
apply (case_tac "length xs ∈ I")
 apply (clarsimp simp: f_join_length)
 apply (simp add: nth_append f_join_length, intro conjI impI)
  apply (subst f_join_nth[of _ "xs @ [x]"])
   apply (simp add: f_join_length)
  apply (simp add: nth_append less_card_cut_less_imp_inext_nth_less)
  apply (simp add: f_join_nth f_join_length)
 apply (simp add: linorder_not_less less_Suc_eq_le)
 apply (subst f_join_nth)
  apply (simp add: f_join_length)
 apply (subgoal_tac "I → i = length xs")
  prefer 2
  apply (rule_tac t="length xs" and s="Max (I ↓< Suc (length xs))" in subst)
   apply (rule Max_equality[OF _ nat_cut_less_finite])
   apply (simp add: cut_less_mem_iff)+
  apply (subst inext_nth_cut_less_eq[of _ _ "Suc (length xs)", symmetric], simp)
  apply (rule inext_nth_card_Max[OF nat_cut_less_finite])
   apply (simp add: card_gr0_imp_not_empty)
  apply simp+
apply (simp add: f_join_nth f_join_length)
apply (simp add: nth_append less_card_cut_less_imp_inext_nth_less)
done

(*<*)
(*
lemma "
  let xs = [0::nat,10,20,30]; ys =[100,110,120,130]; I = {0,2,4,6} in
  (xs @ ys) ⋈⇩f I = xs ⋈⇩f I @ (ys ⋈⇩f (I ⊕- (length xs)))"
by (simp add: Let_def f_join_def iT_Plus_neg_def)
*)
(*>*)


lemma f_join_append: "
  (xs @ ys) ⋈⇩f I = xs ⋈⇩f I @ ys ⋈⇩f (I ⊕- (length xs))"
apply (induct ys rule: rev_induct)
 apply (simp add: f_join_Nil)
apply (simp add: append_assoc[symmetric] f_join_snoc del: append_assoc)
apply (simp add: iT_Plus_neg_mem_iff add.commute[of "length xs"])
done

lemma take_f_join_eq1: "
  n < card (I ↓< length xs) ⟹
  (xs ⋈⇩f I) ↓ n = xs ⋈⇩f (I ↓< (I → n))"
apply (frule less_card_cut_less_imp_inext_nth_less)
apply (simp add: list_eq_iff f_join_length cut_cut_less min_eqR)
apply (subgoal_tac "n < card I ∨ infinite I")
 prefer 2
 apply (case_tac "finite I")
 apply (drule order_less_le_trans[OF _ cut_less_card], simp+)
apply (simp add: min_eqL cut_less_inext_nth_card_eq1)
apply clarify
apply (subst f_join_nth)
 apply (simp add: f_join_length)
apply (subst f_join_nth)
 apply (simp add: f_join_length cut_cut_less min_eqL)
 apply (simp add: cut_less_inext_nth_card_eq1)
apply (simp add: cut_less_inext_nth_card_eq1 inext_nth_cut_less_eq)
done

lemma take_f_join_eq2: "
  card (I ↓< length xs) ≤ n ⟹ (xs ⋈⇩f I) ↓ n = xs ⋈⇩f I"
by (simp add: f_join_length)
lemma take_f_join_if: "
  (xs ⋈⇩f I) ↓ n =
  (if n < card (I ↓< length xs) then xs ⋈⇩f (I ↓< (I → n)) else xs ⋈⇩f I)"
by (simp add: take_f_join_eq1 take_f_join_eq2)

lemma drop_f_join_eq1: "
  n < card (I ↓< length xs) ⟹
  (xs ⋈⇩f I) ↑ n = xs ⋈⇩f (I ↓≥ (I → n))"
apply (case_tac "I = {}")
 apply (simp add: cut_less_empty)
apply (case_tac "I ↓< length xs = {}")
 apply (simp add: cut_less_empty)
apply (rule same_append_eq[THEN iffD1, of "xs ⋈⇩f I ↓ n"])
txt ‹First, a simplification step without ‹take_f_join_eq1› required for correct transformation, in order to eliminate ‹(xs ⋈⇩f I) ↓ n› in the equation.›
apply simp
txt ‹Now, ‹take_f_join_eq1› can be applied›
apply (simp add: take_f_join_eq1)
apply (case_tac "I ↓< (I → n) = {}")
 apply (simp add: f_join_empty)
 apply (rule_tac t= "I → n" and s="iMin I" in subst)
  apply (rule ccontr)
  apply (drule neq_le_trans[of "iMin I"])
   apply (simp add: iMin_le[OF inext_nth_closed])
  apply (simp add: cut_less_Min_not_empty)
 apply (simp add: cut_ge_Min_all)
apply (subst f_join_union[OF nat_cut_less_finite, symmetric])
 apply (subgoal_tac "I ↓≥ (I → n) ≠ {}")
  prefer 2
  apply (simp add: cut_ge_not_empty_iff)
  apply (blast intro: inext_nth_closed)
 apply (simp add: nat_cut_less_finite i_cut_mem_iff iMin_gr_iff)
apply (simp add: cut_less_cut_ge_ident)
done

lemma drop_f_join_eq2: "
  card (I ↓< length xs) ≤ n ⟹ (xs ⋈⇩f I) ↑ n = []"
by (simp add: f_join_length)

lemma drop_f_join_if: "
  (xs ⋈⇩f I) ↑ n =
  (if n < card (I ↓< length xs) then xs ⋈⇩f (I ↓≥ (I → n)) else [])"
by (simp add: drop_f_join_eq1 drop_f_join_eq2)

lemma f_join_take: "xs ↓ n ⋈⇩f I = xs ⋈⇩f (I ↓< n)"
apply (clarsimp simp: list_eq_iff f_join_length cut_cut_less min.commute)
apply (simp add: f_join_nth f_join_length cut_cut_less min.commute)
apply (case_tac "n < length xs")
 apply (simp add: min_eqL inext_nth_cut_less_eq)
 apply (simp add: less_card_cut_less_imp_inext_nth_less)
apply (simp add: min_eqR linorder_not_less)
apply (subst inext_nth_cut_less_eq)
apply (rule order_less_le_trans, assumption)
apply (rule card_mono[OF nat_cut_less_finite cut_less_mono], assumption)
apply simp
done

lemma f_join_drop: "xs ↑ n ⋈⇩f I = xs ⋈⇩f (I ⊕ n)"
apply (case_tac "length xs ≤ n")
 apply (simp add: f_join_Nil)
 apply (rule sym)
 apply (simp add: f_join_Nil_conv' iT_Plus_mem_iff)
apply (rule subst[OF append_take_drop_id, of "λx. xs ↑ n ⋈⇩f I = x ⋈⇩f (I ⊕ n)" n])
apply (simp only: f_join_append)
apply (simp add: f_join_take min_eqR)
apply (simp add: iT_Plus_Plus_neg_inverse)
apply (rule_tac t="(I ⊕ n) ↓< n" and s="{}" in subst)
 apply (rule sym)
 apply (simp add: cut_less_empty_iff iT_Plus_mem_iff)
apply (simp add: f_join_empty)
done

lemma cut_less_eq_imp_f_join_eq: "
  A ↓< length xs = B ↓< length xs ⟹ xs ⋈⇩f A = xs ⋈⇩f B"
apply (clarsimp simp: list_eq_iff f_join_length f_join_nth)
apply (rule subst[OF inext_nth_cut_less_eq, of _ A "length xs"], simp)
apply (rule subst[OF inext_nth_cut_less_eq, of _ B "length xs"], simp)
apply simp
done

corollary f_join_cut_less_eq: "
  length xs ≤ t ⟹ xs ⋈⇩f (I ↓< t) = xs ⋈⇩f I"
apply (rule cut_less_eq_imp_f_join_eq)
apply (simp add: cut_cut_less min_eqR)
done

lemma take_Suc_Max_eq_imp_f_join_eq: "
  ⟦ finite I; xs ↓ Suc (Max I) = ys ↓ Suc (Max I) ⟧ ⟹
  xs ⋈⇩f I = ys ⋈⇩f I"
apply (case_tac "I = {}")
 apply (simp add: f_join_empty)
apply (simp add: list_eq_iff f_join_length)
apply (case_tac "length xs < Suc (Max I)")
 apply (case_tac "length ys < Suc (Max I)")
  apply (clarsimp simp: min_eqL, rename_tac i)
  apply (simp add: f_join_nth2)
  apply (drule_tac x="I → i" in spec)
  apply (subgoal_tac "I → i < length ys")
   prefer 2
   apply (rule less_card_cut_less_imp_inext_nth_less, simp)
  apply simp
 apply (simp add: min_eq)
apply (case_tac "length ys < Suc (Max I)")
 apply (simp add: min_eq)
apply (simp add: linorder_not_less min_eqR Suc_le_eq del: Max_less_iff)
apply (subgoal_tac "I ↓< length xs = I ↓< length ys")
 prefer 2
 apply (simp add: cut_less_Max_all)
apply (clarsimp simp: f_join_nth2 simp del: Max_less_iff, rename_tac i)
apply (drule_tac x="I → i" in spec)
apply (subgoal_tac "I → i < Suc (Max I)")
 prefer 2
 apply (simp add: less_Suc_eq_le inext_nth_closed)
apply (simp del: Max_less_iff)
done

corollary f_join_take_Suc_Max_eq: "
  finite I ⟹ xs ↓ Suc (Max I) ⋈⇩f I = xs ⋈⇩f I"
by (rule take_Suc_Max_eq_imp_f_join_eq, simp+)


text ‹Joining infinite streams and infinite intervals›

lemma i_join_nth: "(f ⋈⇩i I) n = f (I → n)"
by (simp add: i_join_def)

lemma i_join_UNIV: "f ⋈⇩i UNIV = f"
by (simp add: ilist_eq_iff i_join_nth inext_nth_UNIV)

lemma i_join_union: "
  ⟦ finite A; Max A < iMin B; B ≠ {} ⟧ ⟹
  f ⋈⇩i (A ∪ B) = (f ⇓ Suc (Max A) ⋈⇩f A) ⌢ (f ⋈⇩i B)"
apply (case_tac "A = {}")
 apply (simp add: f_join_empty)
apply (simp (no_asm) add: ilist_eq_iff, clarify)
apply (simp add: i_join_nth i_append_nth f_join_length del: Max_less_iff)
apply (subgoal_tac "A ↓< Suc (Max A) = A")
 prefer 2
 apply (simp add: nat_cut_le_less_conv[symmetric] cut_le_Max_all)
apply (simp del: Max_less_iff, intro conjI impI)
 apply (simp add: inext_nth_card_append_eq1)
 apply (simp add: f_join_nth f_join_length)
 apply (simp add: less_card_cut_less_imp_inext_nth_less)
apply (simp add: inext_nth_card_append_eq2)
done

lemma i_join_singleton: "f ⋈⇩i {a} = (λn. f a)"
by (simp add: ilist_eq_iff i_join_nth inext_nth_singleton)

lemma i_join_insert: "
  f ⋈⇩i (insert n I) =
  (f ⇓ n) ⋈⇩f (I ↓< n) ⌢ [f n] ⌢ (
    if I ↓> n = {} then (λx. f n) else f ⋈⇩i (I ↓> n))"
apply (rule ssubst[OF insert_eq_cut_less_cut_greater])
apply (case_tac "I ↓< n = {}")
 apply (simp add: f_join_empty, intro conjI impI)
  apply (simp add: i_join_singleton ilist_eq_iff i_append_nth)
 apply (subgoal_tac "Max {n} < iMin (I ↓> n)")
  prefer 2
  apply (simp add: cut_greater_Min_greater)
 apply simp
 apply (subst insert_is_Un)
 apply (subst i_join_union[OF singleton_finite])
 apply (simp add: f_join_singleton_if)+
apply (intro conjI impI)
 apply (subgoal_tac "Max (I ↓< n) < iMin {n}")
  prefer 2
  apply (simp add: nat_cut_less_Max_less)
 apply (rule_tac t="insert n (I ↓< n)" and s="(I ↓< n) ∪ {n}" in subst, simp)
 apply (subst i_join_union[OF nat_cut_less_finite _ singleton_not_empty], simp)
 apply (simp add: i_join_singleton)
 apply (rule_tac s="λx. f n" and t="[f n] ⌢ (λx. f n)" in subst)
  apply (simp add: ilist_eq_iff i_append_nth)
 apply (subst i_append_assoc[symmetric])
 apply (rule_tac t="[f n] ⌢ (λx. f n)" and s="(λx. f n)" in subst)
  apply (simp add: ilist_eq_iff i_append_nth)
 apply (rule arg_cong)
 apply (simp add: take_Suc_Max_eq_imp_f_join_eq[OF nat_cut_less_finite] min_eqR)
apply (subgoal_tac "Max (I ↓< n) < iMin {n} ∧ Max {n} < iMin (I ↓> n)", elim conjE)
 prefer 2
 apply (simp add: cut_greater_Min_greater nat_cut_less_Max_less)
apply (rule_tac t="insert n (I ↓< n ∪ I ↓> n)" and s="(I ↓< n ∪ ({n} ∪ I ↓> n))" in subst, simp)
apply (subgoal_tac "({n} ∪ I ↓> n) ≠ {} ∧ Max (I ↓< n) < iMin ({n} ∪ I ↓> n)", elim conjE)
 prefer 2
 apply (simp add: iMin_insert)
apply (simp add: i_join_union nat_cut_less_finite singleton_finite del: Un_insert_left Un_insert_right Max_less_iff)
apply (simp add: f_join_singleton_if)
apply (rule arg_cong)
apply (simp add: take_Suc_Max_eq_imp_f_join_eq[OF nat_cut_less_finite] min_eqR)
done

lemma i_join_i_append: "
  infinite I ⟹ (xs ⌢ f) ⋈⇩i I = (xs ⋈⇩f I) ⌢ (f ⋈⇩i (I ⊕- length xs))"
apply (clarsimp simp: ilist_eq_iff)
apply (simp add: i_join_nth i_append_nth f_join_length)
apply (subgoal_tac "I ↓≥ length xs ≠ {}")
 prefer 2
 apply (fastforce simp: cut_ge_not_empty_iff infinite_nat_iff_unbounded_le)
apply (simp add: inext_nth_less_less_card_conv)
apply (intro conjI impI)
 apply (simp add: f_join_nth f_join_length)
apply (subgoal_tac "I ⊕- length xs ≠ {}")
 prefer 2
 apply (simp add: iT_Plus_neg_empty_iff infinite_imp_nonempty)
apply (simp add: iT_Plus_neg_inext_nth)
apply (case_tac "I ↓< length xs = {}")
 apply (frule cut_less_empty_iff[THEN iffD1, THEN cut_ge_all_iff[THEN iffD2]])
 apply simp
apply (rule subst[OF inext_nth_card_append_eq2, OF nat_cut_less_finite], simp+)
  apply (simp add: less_imp_Max_less_iMin[OF nat_cut_less_finite] i_cut_mem_iff)
 apply simp
apply (simp add: cut_less_cut_ge_ident)
done

lemma i_take_i_join: "infinite I ⟹ f ⋈⇩i I ⇓ n = f ⇓ (I → n) ⋈⇩f I"
apply (clarsimp simp: list_eq_iff f_join_length cut_less_inext_nth_card_eq1, rename_tac i)
apply (simp add: i_join_nth)
apply (frule inext_nth_mono2_infin[THEN iffD2], assumption)
apply (rule_tac t="f (I → i)" and s="f ⇓ (I → n) ! (I → i)" in subst, simp)
apply (rule sym, rule f_join_nth)
apply (simp add: f_join_length)
apply (simp add: inext_nth_less_less_card_conv[OF nat_cut_ge_infinite_not_empty])
done

lemma i_drop_i_join: "I ≠ {} ⟹ f ⋈⇩i I ⇑ n = f ⋈⇩i (I ↓≥ (I → n))"
apply (simp (no_asm) add: ilist_eq_iff)
apply (simp add: i_join_nth inext_nth_cut_ge_inext_nth)
done

lemma i_join_i_take: "f ⇓ n ⋈⇩f I = f ⋈⇩i I ⇓ card (I ↓< n)"
apply (clarsimp simp: list_eq_iff f_join_length)
apply (frule less_card_cut_less_imp_inext_nth_less)
apply (simp add: i_join_nth f_join_length f_join_nth)
done

lemma i_join_i_drop: "I ≠ {} ⟹ f ⇑ n ⋈⇩i I = f ⋈⇩i (I ⊕ n)"
apply (simp (no_asm) add: ilist_eq_iff)
apply (simp add: i_join_nth iT_Plus_inext_nth add.commute[of _ n])
done


lemma i_join_finite_nth_ge_card_eq_nth_Max: "
  ⟦ finite I; I ≠ {}; card I ≤ Suc n ⟧ ⟹ (f ⋈⇩i I) n = f (Max I)"
by (simp add: i_join_nth inext_nth_card_Max)

lemma i_join_finite_i_drop_card_eq_const_nth_Max: "
  ⟦ finite I; I ≠ {} ⟧ ⟹ (f ⋈⇩i I) ⇑ (card I) = (λn. f (Max I))"
by (simp add: ilist_eq_iff i_join_finite_nth_ge_card_eq_nth_Max)

lemma i_join_finite_i_append_nth_Max_conv: "
  ⟦ finite I; I ≠ {} ⟧ ⟹ (f ⋈⇩i I) = f ⇓ Suc (Max I) ⋈⇩f I ⌢ (λn. f (Max I))"
apply (simp (no_asm) add: ilist_eq_iff, clarify)
apply (subgoal_tac "I ↓< (Suc (Max I)) = I")
 prefer 2
 apply (simp add: nat_cut_le_less_conv[symmetric] cut_le_Max_all)
apply (simp add: i_append_nth i_join_nth f_join_length)
apply (intro conjI impI)
 apply (simp add: f_join_nth f_join_length)
 apply (rule sym, rule i_take_nth)
 apply (simp add: less_card_cut_less_imp_inext_nth_less)
apply (simp add: inext_nth_card_Max)
done


text ‹Joining infinite streams and finite intervals›

lemma i_f_join_length: "finite I ⟹ length (f ⋈⇘i-f⇙ I) = card I"
apply (simp add: i_f_join_def f_join_length)
apply (simp add: nat_cut_le_less_conv[symmetric] cut_le_Max_all)
done

lemma i_f_join_nth: "n < card I ⟹ f ⋈⇘i-f⇙ I ! n = f (I → n)"
apply (frule card_gr0_imp_finite[OF gr_implies_gr0])
apply (frule card_gr0_imp_not_empty[OF gr_implies_gr0])
apply (simp add: i_f_join_def)
apply (subst i_take_nth[ of "I → n" "Suc (Max I)" f, symmetric])
 apply (rule le_imp_less_Suc)
 apply (simp add: Max_ge[OF _ inext_nth_closed])
apply (simp add: f_join_nth2 nat_cut_le_less_conv[symmetric] cut_le_Max_all)
done

lemma i_f_join_empty: "f ⋈⇘i-f⇙ {} = []"
by (simp add: i_f_join_def f_join_empty)

lemma i_f_join_eq_i_join_i_take: "
  finite I ⟹ f ⋈⇘i-f⇙ I = f ⋈⇩i I ⇓ (card I)"
apply (simp add: i_f_join_def)
apply (simp add: i_join_i_take nat_cut_le_less_conv[symmetric] cut_le_Max_all)
done

lemma i_f_join_union: "
  ⟦ finite A; finite B; Max A < iMin B ⟧ ⟹
  f ⋈⇘i-f⇙ (A ∪ B) = f ⋈⇘i-f⇙ A @ f ⋈⇘i-f⇙ B"
apply (case_tac "A = {}", simp add: i_f_join_empty)
apply (case_tac "B = {}", simp add: i_f_join_empty)
apply (simp add: i_f_join_def f_join_union del: Max_less_iff)
apply (subgoal_tac "Max A < Max B")
 prefer 2
 apply (rule order_less_le_trans[OF _ iMin_le_Max], assumption+)
apply (simp add: Max_Un max_eqR[OF less_imp_le])
apply (rule take_Suc_Max_eq_imp_f_join_eq, assumption)
apply (simp add: min_eqR[OF less_imp_le])
done

lemma i_f_join_singleton: "f ⋈⇘i-f⇙ {n} = [f n]"
by (simp add: i_f_join_def f_join_singleton_if)

lemma i_f_join_insert: "
  finite I ⟹
  f ⋈⇘i-f⇙ insert n I = f ⋈⇘i-f⇙ (I ↓< n) @ f n # f ⋈⇘i-f⇙ (I ↓> n)"
apply (case_tac "I = {}")
 apply (simp add: i_f_join_singleton i_cut_empty i_f_join_empty)
(*
apply (subgoal_tac "n < Suc (Max (insert n I))")
 prefer 2
 apply simp
apply (frule less_Suc_eq_le[THEN iffD1])*)
apply (simp add: i_f_join_def)
apply (simp add: f_join_insert)
apply (frule cut_greater_finite[of _ n])
apply (case_tac "I ↓> n = {}")
 apply (simp add: f_join_empty)
 apply (case_tac "I ↓< n = {}")
  apply (simp add: f_join_empty)
 apply (rule take_Suc_Max_eq_imp_f_join_eq[OF nat_cut_less_finite])
 apply simp
 apply (rule arg_cong[where f="λx. f ⇓ x"])
 apply simp
 apply (rule min_eqR, rule max.coboundedI1, rule less_imp_le)
 apply (simp add: nat_cut_less_Max_less)
apply (simp add: cut_greater_Max_eq)
apply (subgoal_tac "n < Max I")
 prefer 2
 apply (rule ccontr)
 apply (simp add: linorder_not_less cut_greater_Max_empty)
apply (simp add: max_eqR[OF less_imp_le])
apply (case_tac "I ↓< n = {}")
 apply (simp add: f_join_empty)
apply (rule take_Suc_Max_eq_imp_f_join_eq[OF nat_cut_less_finite])
apply simp
apply (rule arg_cong[where f="λx. f ⇓ x"])
apply simp
apply (rule min_eqR)
apply (blast intro: Max_subset)
done

lemma take_i_f_join_eq1: "
  n < card I ⟹ f ⋈⇘i-f⇙ I ↓ n = f ⋈⇘i-f⇙ (I ↓< (I → n))"
apply (frule card_ge_0_finite[OF gr_implies_gr0])
apply (case_tac "I = {}")
 apply (simp add: cut_less_empty i_f_join_empty)
apply (subgoal_tac "n < card (I ↓< Suc (Max I))")
 prefer 2
 apply (simp add: cut_less_Max_all)
apply (simp add: i_f_join_def take_f_join_eq1)
apply (case_tac "I ↓< (I → n) = {}")
 apply (simp add: f_join_empty)
apply (rule take_Suc_Max_eq_imp_f_join_eq[OF nat_cut_less_finite])
apply simp
apply (rule arg_cong[where f="λx. f ⇓ x"])
apply simp
apply (rule min_eqR)
apply (rule order_trans[OF less_imp_le[OF cut_less_Max_less]])
apply (simp add: nat_cut_less_finite inext_nth_closed)+
done

lemma take_i_f_join_eq2: "
  ⟦ finite I; card I ≤ n ⟧ ⟹ f ⋈⇘i-f⇙ I ↓ n = f ⋈⇘i-f⇙ I"
apply (case_tac "I = {}")
 apply (simp add: cut_less_empty i_f_join_empty)
apply (simp add: i_f_join_def take_f_join_eq2 cut_less_Max_all)
done

lemma take_i_f_join_if: "
  finite I ⟹
  f ⋈⇘i-f⇙ I ↓ n = (if n < card I then f ⋈⇘i-f⇙ (I ↓< (I → n)) else f ⋈⇘i-f⇙ I)"
by (simp add: take_i_f_join_eq1 take_i_f_join_eq2)

lemma drop_i_f_join_eq1: "
  n < card I ⟹ f ⋈⇘i-f⇙ I ↑ n = f ⋈⇘i-f⇙ (I ↓≥ (I → n))"
apply (frule card_ge_0_finite[OF gr_implies_gr0])
apply (case_tac "I = {}")
 apply (simp add: cut_ge_empty i_f_join_empty)
apply (subgoal_tac "n < card (I ↓< Suc (Max I))")
 prefer 2
 apply (simp add: cut_less_Max_all)
apply (simp add: i_f_join_def drop_f_join_eq1)
apply (subgoal_tac "I ↓≥ (I → n) ≠ {}")
 prefer 2
 apply (rule in_imp_not_empty[of "I → n"])
 apply (simp add: cut_ge_mem_iff inext_nth_closed)
apply (rule take_Suc_Max_eq_imp_f_join_eq)
 apply (rule cut_ge_finite, assumption)
apply simp
apply (rule arg_cong[where f="λx. f ⇓ x"])
apply (simp add: min_eqR cut_ge_Max_eq)
done

lemma drop_i_f_join_eq2: "
  ⟦ finite I; card I ≤ n ⟧ ⟹ f ⋈⇘i-f⇙ I ↑ n = []"
by (simp add: i_f_join_length)

lemma drop_i_f_join_if: "
  finite I ⟹
  f ⋈⇘i-f⇙ I ↑ n = (if n < card I then f ⋈⇘i-f⇙ (I ↓≥ (I → n)) else [])"
by (simp add: drop_i_f_join_eq1 drop_i_f_join_eq2)

lemma i_f_join_i_drop: "
  finite I ⟹ f ⇑ n ⋈⇘i-f⇙ I = f ⋈⇘i-f⇙ (I ⊕ n)"
apply (case_tac "I = {}")
 apply (simp add: iT_Plus_empty i_f_join_empty)
apply (simp add: i_f_join_def iT_Plus_Max)
apply (simp add: i_take_i_drop f_join_drop)
done

lemma i_take_Suc_Max_eq_imp_i_f_join_eq: "
  f ⇓ Suc (Max I) = g ⇓ Suc (Max I) ⟹ f ⋈⇘i-f⇙ I = g ⋈⇘i-f⇙ I"
by (simp add: i_f_join_def)

lemma i_take_i_join_eq_i_f_join: "
  infinite I ⟹ f ⋈⇩i I ⇓ n = f ⋈⇘i-f⇙ (I ↓< (I → n))"
apply (frule infinite_imp_nonempty)
apply (case_tac "n = 0")
 apply (simp add: cut_less_Min_empty i_f_join_empty)
apply (frule inext_nth_gr_Min_conv_infinite[THEN iffD2], simp)
apply (simp add: i_take_i_join i_f_join_def)
apply (subgoal_tac "Suc (Max (I ↓< (I → n))) ≤ I → n")
 prefer 2
 apply (rule Suc_leI)
 apply (rule nat_cut_less_Max_less)
 apply (simp add: cut_less_Min_not_empty)
apply (simp add: f_join_cut_less_eq)
apply (simp add: i_join_i_take)
apply (rule arg_cong[where f="λx. f ⋈⇩i I ⇓ card x"])
apply (clarsimp simp: gr0_conv_Suc)
apply (simp add: cut_le_less_inext_conv[OF inext_nth_closed, symmetric])
apply (simp add: nat_cut_le_less_conv[symmetric])
apply (rule arg_cong[where f="λx. I ↓≤ x"])
apply (rule sym, rule Max_equality[OF _ nat_cut_le_finite])
apply (simp add: cut_le_mem_iff inext_nth_closed)+
done


subsubsection ‹Results for intervals from ‹IL_Interval››

lemma f_join_iFROM: "xs ⋈⇩f [n…] = xs ↑ n"
apply (clarsimp simp: list_eq_iff f_join_length iFROM_cut_less iIN_card Suc_diff_Suc)
apply (subst f_join_nth2)
 apply (simp add: iFROM_cut_less iIN_card)
apply (simp add: iFROM_inext_nth)
done

lemma i_join_iFROM: "f ⋈⇩i [n…] = f ⇑ n"
by (simp add: ilist_eq_iff i_join_nth iFROM_inext_nth)

lemma f_join_iIN: "xs ⋈⇩f [n…,d] = xs ↑ n ↓ Suc d"
apply (simp add: list_eq_iff f_join_length iIN_cut_less iIN_card Suc_diff_Suc min_eq)
apply (simp add: f_join_nth2 iIN_cut_less iIN_card iIN_inext_nth)
done

lemma i_f_join_iIN: "f ⋈⇘i-f⇙ [n…,d] = f ⇑ n ⇓ Suc d"
by (simp add: i_f_join_def f_join_iIN iIN_Max i_take_drop)

lemma f_join_iTILL: "xs ⋈⇩f […n] = xs ↓ (Suc n)"
by (simp add: iIN_0_iTILL_conv[symmetric] f_join_iIN)

lemma i_f_join_iTILL: "f ⋈⇘i-f⇙ […n] = f ⇓ Suc n"
by (simp add: iIN_0_iTILL_conv[symmetric] i_f_join_iIN)


lemma f_join_f_expand_iT_Mult: "
  0 < k ⟹ xs ⊙⇩f k ⋈⇩f (I ⊗ k) = xs ⋈⇩f I"
apply (case_tac "I = {}")
 apply (simp add: iT_Mult_empty f_join_empty)
apply (simp add: list_eq_iff f_join_length)
apply (clarsimp simp: iT_Mult_cut_less2 iT_Mult_card)
apply (simp add: f_join_nth2 iT_Mult_cut_less2 iT_Mult_card)
apply (drule less_card_cut_less_imp_inext_nth_less)
apply (simp add: iT_Mult_inext_nth f_expand_nth_mult)
done

lemma i_join_i_expand_iT_Mult: "
  ⟦ 0 < k; I ≠ {} ⟧ ⟹ f ⊙⇩i k ⋈⇩i (I ⊗ k) = f ⋈⇩i I"
apply (simp (no_asm) add: ilist_eq_iff, clarify)
apply (simp add: i_join_nth iT_Mult_inext_nth i_expand_nth_mult)
done

lemma i_f_join_i_expand_iT_Mult: "
  ⟦ 0 < k; finite I ⟧ ⟹ f ⊙⇩i k ⋈⇘i-f⇙ (I ⊗ k) = f ⋈⇘i-f⇙ I"
apply (case_tac "I = {}")
 apply (simp add: iT_Mult_empty i_f_join_empty)
apply (clarsimp simp: list_eq_iff i_f_join_length iT_Mult_finite_iff iT_Mult_not_empty iT_Mult_card)
apply (simp add: i_f_join_nth iT_Mult_card iT_Mult_inext_nth i_expand_nth_mult)
done

lemma f_join_f_shrink_iT_Plus_iT_Div_mod: "
  ⟦ 0 < k; ∀x∈I. x mod k = 0 ⟧ ⟹
  (xs ⟼⇩f k) ⋈⇩f (I ⊕ (k - 1)) = xs ÷⇩f k ⋈⇩f (I ⊘ k)"
apply (case_tac "I = {}")
 apply (simp add: iT_Plus_empty iT_Div_empty f_join_empty)
apply (simp add: list_eq_iff f_join_length f_shrink_length)
apply (subgoal_tac "Suc (length xs) - k ≤ length xs - length xs mod k")
 prefer 2
 apply (case_tac "length xs < k", simp)
 apply (simp add: Suc_diff_le linorder_not_less)
 apply (rule Suc_leI)
 apply (rule diff_less_mono2, simp)
 apply (rule order_less_le_trans[OF mod_less_divisor], assumption+)
apply (rule context_conjI)
 apply (simp add: iT_Plus_cut_less iT_Div_cut_less2 iT_Plus_card)
 apply (subst iT_Div_card_inj_on)
  apply (rule mod_eq_imp_div_right_inj_on)
  apply clarsimp+
 apply (rule arg_cong[where f=card])
 apply (simp (no_asm_simp) add: set_eq_iff cut_less_mem_iff, clarify)
 apply (rule conj_cong, simp)
 apply (rule iffI)
  apply simp
   apply (frule_tac x=x and m=k in less_mod_eq_imp_add_divisor_le)
  apply (simp add: mod_diff_right_eq [symmetric])
 apply simp
apply (clarsimp simp: f_join_nth f_join_length f_shrink_length)
apply (simp add: iT_Plus_inext_nth iT_Plus_not_empty)
apply (simp add: iT_Div_mod_inext_nth)
apply (subst f_shrink_nth_eq_f_last_message_hold_nth)
 apply (drule sym, simp, thin_tac "card x = card y" for x y)
 apply (simp add: iT_Plus_cut_less iT_Plus_card)
 apply (rule less_mult_imp_div_less)
 apply (rule less_le_trans[OF less_card_cut_less_imp_inext_nth_less], assumption)
 apply (simp add: div_mult_cancel)
apply (simp add: div_mult_cancel inext_nth_closed)
done

lemma i_join_i_shrink_iT_Plus_iT_Div_mod: "
  ⟦ 0 < k; I ≠ {}; ∀x∈I. x mod k = 0 ⟧ ⟹
  (f ⟼⇩i k) ⋈⇩i (I ⊕ (k - 1))= f ÷⇩i k ⋈⇩i (I ⊘ k)"
apply (simp (no_asm) add: ilist_eq_iff, clarify)
apply (simp add: i_join_nth)
apply (simp add: i_shrink_nth_eq_i_last_message_hold_nth)
apply (simp add: iT_Plus_inext_nth iT_Div_mod_inext_nth)
apply (drule_tac x="I → x" in bspec)
 apply (simp add: inext_nth_closed)
apply (simp add: mod_0_div_mult_cancel)
done

lemma i_f_join_i_shrink_iT_Plus_iT_Div_mod: "
  ⟦ 0 < k; finite I; ∀x∈I. x mod k = 0 ⟧ ⟹
  (f ⟼⇩i k) ⋈⇘i-f⇙ (I ⊕ (k - 1))= f ÷⇩i k ⋈⇘i-f⇙ (I ⊘ k)"
apply (case_tac "I = {}")
 apply (simp add: iT_Plus_empty iT_Div_empty i_f_join_empty)
apply (simp add: i_f_join_def iT_Plus_Max iT_Div_Max)
apply (simp add: i_last_message_hold_i_take[symmetric] i_shrink_i_take_mult[symmetric])
apply (simp add: add.commute[of k])
apply (simp add: mod_0_div_mult_cancel[THEN iffD1])
apply (simp add: f_join_f_shrink_iT_Plus_iT_Div_mod[unfolded One_nat_def])
done

corollary f_join_f_shrink_iT_Plus_iT_Div_mod_subst: "
  ⟦ 0 < k; ∀x∈I. x mod k = 0;
    A = I ⊕ (k - 1); B = I ⊘ k ⟧ ⟹
  (xs ⟼⇩f k) ⋈⇩f A = xs ÷⇩f k ⋈⇩f B"
by (simp add: f_join_f_shrink_iT_Plus_iT_Div_mod[unfolded One_nat_def])
corollary i_join_i_shrink_iT_Plus_iT_Div_mod_subst: "
  ⟦ 0 < k; I ≠ {}; ∀x∈I. x mod k = 0;
    A = I ⊕ (k - 1); B = I ⊘ k ⟧ ⟹
  (f ⟼⇩i k) ⋈⇩i A = f ÷⇩i k ⋈⇩i B"
by (simp add: i_join_i_shrink_iT_Plus_iT_Div_mod[unfolded One_nat_def])
corollary i_f_join_i_shrink_iT_Plus_iT_Div_mod_subst: "
  ⟦ 0 < k; finite I; ∀x∈I. x mod k = 0;
    A = I ⊕ (k - 1); B = I ⊘ k ⟧ ⟹
  (f ⟼⇩i k) ⋈⇘i-f⇙ A= f ÷⇩i k ⋈⇘i-f⇙ B"
by (simp add: i_f_join_i_shrink_iT_Plus_iT_Div_mod[unfolded One_nat_def])



lemma f_join_f_shrink_iT_Div_mod: "
  ⟦ 0 < k; ∀x∈I. x mod k = k - 1 ⟧ ⟹
  (xs ⟼⇩f k) ⋈⇩f I = xs ÷⇩f k ⋈⇩f (I ⊘ k)"
apply (case_tac "I = {}")
 apply (simp add: iT_Div_empty f_join_empty)
apply (frule Suc_leI, drule order_le_imp_less_or_eq, erule disjE)
 prefer 2
 apply (drule sym, simp add: iT_Div_1)
apply (rule_tac t=I and s="I ⊕- (k - 1) ⊕ (k - 1)" in subst)
 apply (rule iT_Plus_neg_Plus_le_inverse)
 apply (rule ccontr)
 apply (drule_tac x="iMin I" in bspec, simp add: iMinI_ex2)
 apply (simp add: iMinI_ex2)+
apply (subgoal_tac "⋀x. x + k - Suc 0 ∈ I ⟹ x mod k = 0")
 prefer 2
 apply (rule mod_add_eq_imp_mod_0[THEN iffD1, of "k - Suc 0"])
 apply (simp add: add.commute[of k])
apply (subst iT_Plus_Div_distrib_mod_less)
 apply (clarsimp simp: iT_Plus_neg_mem_iff)
apply (simp add: iT_Plus_0)
apply (rule f_join_f_shrink_iT_Plus_iT_Div_mod[unfolded One_nat_def], simp)
apply (simp add: iT_Plus_neg_mem_iff)
done

lemma i_join_i_shrink_iT_Div_mod: "
  ⟦ 0 < k; I ≠ {}; ∀x∈I. x mod k = k - 1 ⟧ ⟹
  (f ⟼⇩i k) ⋈⇩i I= f ÷⇩i k ⋈⇩i (I ⊘ k)"
apply (simp (no_asm) add: ilist_eq_iff, clarify)
apply (simp add: i_join_nth)
apply (simp add: i_shrink_nth_eq_i_last_message_hold_nth)
apply (simp add: iT_Div_mod_inext_nth)
apply (drule_tac x="I → x" in bspec)
 apply (rule inext_nth_closed, assumption)
apply (simp add: div_mult_cancel)
apply (subgoal_tac "k - Suc 0 ≤ I → x ")
 prefer 2
 apply (rule order_trans[OF _ mod_le_dividend[where n=k]])
 apply simp
apply simp
done

lemma i_f_join_i_shrink_iT_Div_mod: "
  ⟦ 0 < k; finite I; ∀x∈I. x mod k = k - 1 ⟧ ⟹
  (f ⟼⇩i k) ⋈⇘i-f⇙ I = f ÷⇩i k ⋈⇘i-f⇙ (I ⊘ k)"
apply (case_tac "I = {}")
 apply (simp add: iT_Plus_empty iT_Div_empty i_f_join_empty)
apply (simp add: i_f_join_def)
apply (simp add: iT_Div_Max)
apply (simp add: i_last_message_hold_i_take[symmetric] i_shrink_i_take_mult[symmetric] add.commute[of k])
apply (simp add: div_mult_cancel)
apply (subgoal_tac "k - Suc 0 ≤ Max I")
 prefer 2
 apply (rule order_trans[OF _ mod_le_dividend[where n=k]])
 apply simp
apply (simp add: f_join_f_shrink_iT_Div_mod)
done

lemma f_join_f_expand_iMOD: "
  0 < k ⟹ xs ⊙⇩f k ⋈⇩f [n * k, mod k] = xs ⋈⇩f [n…]"
by (subst iFROM_mult[symmetric], rule f_join_f_expand_iT_Mult)
corollary f_join_f_expand_iMOD_0: "
  0 < k ⟹ xs ⊙⇩f k ⋈⇩f [0, mod k] = xs"
apply (drule f_join_f_expand_iMOD[of k xs 0])
apply (simp add: iFROM_0 f_join_UNIV)
done

lemma f_join_f_expand_iMODb: "
  0 < k ⟹ xs ⊙⇩f k ⋈⇩f [n * k, mod k, d] = xs ⋈⇩f [n…,d]"
by (subst iIN_mult[symmetric], rule f_join_f_expand_iT_Mult)

corollary f_join_f_expand_iMODb_0: "
  0 < k ⟹ xs ⊙⇩f k ⋈⇩f [0, mod k, n] = xs ⋈⇩f […n]"
apply (drule f_join_f_expand_iMODb[of k xs 0 n])
apply (simp add: iIN_0_iTILL_conv)
done

lemma i_join_i_expand_iMOD: "
  0 < k ⟹ f ⊙⇩i k ⋈⇩i [n * k, mod k] = f ⋈⇩i [n…]"
by (subst iFROM_mult[symmetric], rule i_join_i_expand_iT_Mult[OF _ iFROM_not_empty])

corollary i_join_i_expand_iMOD_0: "
  0 < k ⟹ f ⊙⇩i k ⋈⇩i [0, mod k] = f"
apply (drule i_join_i_expand_iMOD[of k f 0])
apply (simp add: iFROM_0 i_join_UNIV)
done

lemma i_join_i_expand_iMODb: "
  0 < k ⟹ f ⊙⇩i k ⋈⇩i [n * k, mod k, d] = f ⋈⇩i [n…,d]"
by (subst iIN_mult[symmetric], rule i_join_i_expand_iT_Mult[OF _ iIN_not_empty])

corollary i_join_i_expand_iMODb_0: "
  0 < k ⟹ f ⊙⇩i k ⋈⇩i [0, mod k, n] = f ⋈⇩i […n]"
apply (drule i_join_i_expand_iMODb[of k f 0 n])
apply (simp add: iIN_0_iTILL_conv)
done


lemma i_f_join_i_expand_iMODb: "
  0 < k ⟹ f ⊙⇩i k ⋈⇘i-f⇙ [n * k, mod k, d] = f ⋈⇘i-f⇙ [n…,d]"
by (subst iIN_mult[symmetric], rule i_f_join_i_expand_iT_Mult[OF _ iIN_finite])
corollary i_f_join_i_expand_iMODb_0: "
  0 < k ⟹ f ⊙⇩i k ⋈⇘i-f⇙ [0, mod k, n] = f ⋈⇘i-f⇙ […n]"
apply (drule i_f_join_i_expand_iMODb[of k f 0 n])
apply (simp add: iIN_0_iTILL_conv)
done


lemma f_join_f_shrink_iMOD: "
  0 < k ⟹ (xs ⟼⇩f k) ⋈⇩f [n * k + (k - 1), mod k] = xs ÷⇩f k ⋈⇩f [n…]"
apply (rule f_join_f_shrink_iT_Plus_iT_Div_mod_subst[where I="[n * k, mod k]"])
apply (simp add: iMOD_iff iMOD_add iMOD_div_ge)+
done

corollary f_join_f_shrink_iMOD_0: "
  0 < k ⟹ (xs ⟼⇩f k) ⋈⇩f [k - 1, mod k] = xs ÷⇩f k"
apply (frule f_join_f_shrink_iMOD[of k xs 0])
apply (simp add: iFROM_0 f_join_UNIV)
done

lemma f_join_f_shrink_iMODb: "
  0 < k ⟹ (xs ⟼⇩f k) ⋈⇩f [n * k + (k - 1), mod k, d] = xs ÷⇩f k ⋈⇩f [n…,d]"
apply (rule f_join_f_shrink_iT_Plus_iT_Div_mod_subst[where I="[n * k, mod k, d]"])
apply (simp add: iMODb_iff iMODb_add iMODb_div_ge)+
done

corollary f_join_f_shrink_iMODb_0: "
  0 < k ⟹ (xs ⟼⇩f k) ⋈⇩f [k - 1, mod k, n] = xs ÷⇩f k ⋈⇩f […n]"
apply (frule f_join_f_shrink_iMODb[of k xs 0 n])
apply (simp add: iIN_0_iTILL_conv)
done

lemma i_join_i_shrink_iMOD: "
  0 < k ⟹ (f ⟼⇩i k) ⋈⇩i [n * k + (k - 1), mod k] = f ÷⇩i k ⋈⇩i [n…]"
apply (rule i_join_i_shrink_iT_Plus_iT_Div_mod_subst[where I="[n * k, mod k]"])
apply (simp add: iMOD_not_empty iMOD_iff iMOD_add iMOD_div_ge)+
done

corollary i_join_i_shrink_iMOD_0: "
  0 < k ⟹ (f ⟼⇩i k) ⋈⇩i [k - 1, mod k] = f ÷⇩i k"
apply (frule i_join_i_shrink_iMOD[of k f 0])
apply (simp add: iFROM_0 i_join_UNIV)
done

lemma i_f_join_i_shrink_iMODb: "
  0 < k ⟹ (f ⟼⇩i k) ⋈⇘i-f⇙ [n * k + (k - 1), mod k, d] = f ÷⇩i k ⋈⇘i-f⇙ [n…,d]"
apply (rule i_f_join_i_shrink_iT_Plus_iT_Div_mod_subst[where I="[n * k, mod k, d]"])
apply (simp add: iMODb_finite iMODb_iff iMODb_add iMODb_div_ge)+
done

corollary i_f_join_i_shrink_iMODb_0: "
  0 < k ⟹ (f ⟼⇩i k) ⋈⇘i-f⇙ [k - 1, mod k, n] = f ÷⇩i k ⋈⇘i-f⇙ […n]"
apply (frule i_f_join_i_shrink_iMODb[of k f 0 n])
apply (simp add: iIN_0_iTILL_conv i_join_UNIV)
done


subsection ‹Streams and temporal operators›

lemma i_shrink_eq_NoMsg_iAll_conv: "
  0 < k ⟹ ((s ÷⇩i k) t = \<NoMsg>) = (□ t1 [t * k…,k - Suc 0]. s t1 = \<NoMsg>)"
apply (simp add: i_shrink_nth last_message_NoMsg_conv iAll_def Ball_def iIN_iff)
apply (rule iffI)
 apply (clarify, rename_tac i)
 apply (drule_tac x="i - t * k" in spec)
 apply simp
apply (clarify, rename_tac i)
apply (drule_tac x="t * k + i" in spec)
apply simp
done

lemma i_shrink_eq_NoMsg_iAll_conv2: "
  0 < k ⟹ ((s ÷⇩i k) t = \<NoMsg>) = (□ t1 […k - 1] ⊕ (t * k). s t1 = \<NoMsg>)"
by (simp add: iT_add i_shrink_eq_NoMsg_iAll_conv)

lemma i_shrink_eq_Msg_iEx_iAll_conv: "
  ⟦ 0 < k; m ≠ \<NoMsg> ⟧ ⟹
  ((s ÷⇩i k) t = m) =
  (◇ t1 [t * k…,k - Suc 0]. s t1 = m ∧
    (□ t2 [Suc t1…]. t2 ≤ t * k + k - Suc 0 ⟶ s t2 = \<NoMsg>))"
apply (simp add: i_shrink_nth last_message_conv)
apply (simp add: iAll_def iEx_def Ball_def Bex_def iIN_iff iFROM_iff)
apply (rule iffI)
 apply (clarsimp, rename_tac i)
 apply (rule_tac x="t * k + i" in exI)
 apply (simp add: diff_add_assoc less_imp_le_pred del: add_diff_assoc)
 apply (clarsimp, rename_tac j)
 apply (drule_tac x="j - t * k" in spec)
 apply simp
apply (clarsimp, rename_tac i)
apply (rule_tac x="i - t * k" in exI)
apply simp
done

lemma i_shrink_eq_Msg_iEx_iAll_conv2: "
  ⟦ 0 < k; m ≠ \<NoMsg> ⟧ ⟹
  ((s ÷⇩i k) t = m) =
  (◇ t1 […k - 1] ⊕ (t * k). s t1 = m ∧
    (□ t2 [1…] ⊕ t1 . t2 ≤ t * k + k - 1 ⟶ s t2 = \<NoMsg>))"
by (simp add: iT_add i_shrink_eq_Msg_iEx_iAll_conv)

lemma i_shrink_eq_Msg_iEx_iAll_cut_greater_conv: "
  ⟦ 0 < k; m ≠ \<NoMsg> ⟧ ⟹
  ((s ÷⇩i k) t = m) =
  (◇ t1 [t * k…,k - Suc 0]. s t1 = m ∧
    (□ t2 [t * k…,k - Suc 0] ↓> t1. s t2 = \<NoMsg>))"
apply (simp add: i_shrink_eq_Msg_iEx_iAll_conv)
apply (simp add: iIN_cut_greater iEx_def)
apply (rule bex_cong2[OF subset_refl])
apply (force simp: iAll_def Ball_def iT_iff)
done

lemma i_shrink_eq_Msg_iEx_iAll_cut_greater_conv2: "
  ⟦ 0 < k; m ≠ \<NoMsg> ⟧ ⟹
  ((s ÷⇩i k) t = m) =
  (◇ t1 […k - 1] ⊕ (t * k). s t1 = m ∧
    (□ t2 ([…k - 1] ⊕ (t * k)) ↓> t1. s t2 = \<NoMsg>))"
by (simp add: iT_add i_shrink_eq_Msg_iEx_iAll_cut_greater_conv)

lemma i_shrink_eq_Msg_iSince_conv: "
  ⟦ 0 < k; m ≠ \<NoMsg> ⟧ ⟹
  ((s ÷⇩i k) t = m) =
  (s t2 = \<NoMsg>. t2 𝒮 t1 [t * k…,k - Suc 0]. s t1 = m)"
by (simp add: iSince_def iIN_cut_greater i_shrink_eq_Msg_iEx_iAll_cut_greater_conv)
lemma i_shrink_eq_Msg_iSince_conv2: "
  ⟦ 0 < k; m ≠ \<NoMsg> ⟧ ⟹
  ((s ÷⇩i k) t = m) =
  (s t2 = \<NoMsg>. t2 𝒮 t1 […k - 1] ⊕ (t * k). s t1 = m)"
by (simp add: iT_add i_shrink_eq_Msg_iSince_conv)


lemma iT_Mult_iAll_i_expand_nth_iff:
  "0 < k ⟹ (□ t (I ⊗ k). P ((f ⊙⇩i k) t)) = (□ t I. P (f t))"
apply (rule iffI)
 apply clarify
 apply (drule_tac t="t * k" in ispec)
  apply (simp add: iT_Mult_mem_iff2)
 apply (simp add: i_expand_nth_mult)
apply (fastforce simp: iT_Mult_mem_iff mult.commute[of k] i_expand_nth_mod_eq_0)
done


text ‹Streams and temporal operators cycle start/finish events›

lemma i_shrink_eq_NoMsg_iAll_start_event_conv: "
  ⟦ 0 < k; ⋀t. event t = (t mod k = 0); t0 = t * k ⟧ ⟹
  ((s ÷⇩i k) t = \<NoMsg>) =
  (s t0 = \<NoMsg> ∧ (○ t' t0 [0…]. (s t1 = \<NoMsg>. t1 𝒰 t2 ([0…] ⊕ t'). event t2)))"
apply (case_tac "k = Suc 0")
 apply (simp add: iT_add iT_not_empty iNext_True)
apply (drule neq_le_trans[OF not_sym], simp)
apply (simp add: i_shrink_eq_NoMsg_iAll_conv iTL_defs Ball_def Bex_def iT_add iT_iff iFROM_cut_less iFROM_inext)
apply (rule iffI)
 apply simp
 apply (rule_tac x="t * k + k" in exI)
 apply fastforce
apply (clarify elim!: dvdE, rename_tac x1 x2)
apply (case_tac "x2 = Suc (t * k)")
 apply (simp add: mod_Suc)
apply (clarsimp elim!: dvdE, rename_tac q)
apply (drule_tac y=x1 in order_le_imp_less_or_eq, erule disjE)
 prefer 2
 apply simp
apply (drule_tac x=x1 in spec)
apply (simp add: mult.commute[of k])
apply (drule Suc_le_lessD)
apply (drule_tac y="q * k" and m=k in less_mod_eq_imp_add_divisor_le, simp)
apply simp
done

lemma i_shrink_eq_Msg_iUntil_start_event_conv: "
  ⟦ 0 < k; m ≠ \<NoMsg>; ⋀t. event t = (t mod k = 0); t0 = t * k ⟧ ⟹
  ((s ÷⇩i k) t = m) = (
  (s t0 = m ∧ (○ t' t0 [0…]. (s t1 = \<NoMsg>. t1 𝒰 t2 ([0…] ⊕ t'). event t2))) ∨
  (○ t' t0 [0…]. (¬ event t1. t1 𝒰 t2 ([0…] ⊕ t'). (
    s t2 = m ∧ ¬ event t2 ∧ (○ t'' t2 [0…].
      (s t3 = \<NoMsg>. t3 𝒰 t4 ([0…] ⊕ t''). event t4))))))"
apply (case_tac "k = Suc 0")
 apply (simp add: iT_add iT_not_empty iNext_iff)
apply (drule neq_le_trans[OF not_sym], simp)
apply (simp add: i_shrink_eq_Msg_iSince_conv iTL_defs iT_add iT_cut_greater iT_cut_less Ball_def Bex_def iT_iff iFROM_inext)
apply (rule_tac t="Suc (t * k + k - 2)" and s="t * k + k - Suc 0" in subst, simp)
apply (rule iffI)
 apply (elim exE conjE, rename_tac i)
 apply (case_tac "i = t * k")
  apply (rule disjI1)
  apply simp
  apply (rule_tac x="t * k + k" in exI)
  apply force
 apply (rule disjI2)
 apply (rule_tac x=i in exI)
 apply (case_tac "i = Suc (t * k)")
  apply simp
  apply (case_tac "Suc (t * k) < t * k + k - Suc 0")
   apply (clarsimp simp: mod_Suc)
   apply (case_tac "k = Suc (Suc 0)", simp)
   apply simp
   apply (rule_tac x="t * k + k" in exI)
   apply force
  apply clarsimp
  apply (subgoal_tac "k = Suc (Suc 0)")
   prefer 2
   apply simp
  apply (simp add: mod_Suc)
  apply (simp add: mult_2_right[symmetric] numeral_2_eq_2 del: mult_Suc_right)
  apply (rule_tac x="t * k + k" in exI)
  apply simp
 apply simp
 apply (subgoal_tac "Suc (t * k) ≤ i")
  prefer 2
  apply (rule ccontr, simp)
 apply simp
 apply (case_tac "i < t * k + k - Suc 0")
  apply clarsimp
  apply (subgoal_tac "0 < i mod k")
   prefer 2
   apply (simp add: mult.commute[of t])
   apply (rule between_imp_mod_gr0[OF Suc_le_lessD], simp+)
  apply (rule conjI)
   apply (rule_tac x="t * k + k" in exI)
   apply force
  apply clarify
  apply (simp add: mult.commute[of t])
  apply (rule between_imp_mod_gr0[OF Suc_le_lessD], assumption)
  apply simp
 apply clarsimp
 apply (subgoal_tac "Suc (Suc 0) < k")
  prefer 2
  apply simp
 apply (simp add: mod_0_imp_mod_pred)
 apply (rule conjI, blast)
 apply clarify
 apply (simp add: mult.commute[of t])
 apply (rule between_imp_mod_gr0[OF Suc_le_lessD], assumption)
 apply simp
apply (simp add: mod_Suc)
apply (erule disjE)
 apply (clarsimp simp: mult.commute[of k] elim!: dvdE, rename_tac i)
 apply (subgoal_tac "t < i")
  prefer 2
  apply (rule ccontr)
  apply (simp add: linorder_not_less)
  apply (drule_tac i=i and k=k in mult_le_mono1)
  apply simp
 apply (rule_tac x="t * k" in exI)
 apply simp
 apply (subgoal_tac "t * k < t * k + k - Suc 0")
  prefer 2
  apply simp
 apply (clarsimp, rename_tac j)
 apply (drule_tac x=j in spec)
 apply (simp add: numeral_2_eq_2 Suc_diff_Suc)
 apply (drule mp)
  apply (rule order_trans, assumption)
  apply (drule_tac m=t and n=i in Suc_leI)
  apply (drule mult_le_mono1[of "Suc t"_ k])
  apply simp
 apply simp
apply (clarsimp, rename_tac i)
apply (case_tac "i = Suc (t * k)")
 apply (clarsimp, rename_tac i1)
 apply (rule_tac x="Suc (t * k)" in exI)
 apply simp
 apply (case_tac "k = Suc (Suc 0)", simp)
 apply (clarsimp simp: mult.commute[of k] elim!: dvdE, rename_tac q)
 apply (subgoal_tac "Suc (t * k) < t * k + k - Suc 0")
  prefer 2
  apply simp
 apply (clarsimp elim!: dvdE, rename_tac j)
 apply (drule_tac x=j in spec)
 apply (simp add: numeral_3_eq_3 Suc_diff_Suc)
 apply (subgoal_tac "t * k + k ≤ q * k")
  prefer 2
  apply (rule less_mod_eq_imp_add_divisor_le)
   apply (rule Suc_le_lessD, simp)
  apply simp
 apply simp
apply (clarsimp, rename_tac i1)
apply (rule_tac x=i in exI)
apply (simp add: numeral_2_eq_2 Suc_diff_Suc)
apply (case_tac "i1 = Suc i")
 apply simp
 apply (case_tac "Suc (i mod k) = k")
  apply simp
  apply (subgoal_tac "i ≤ t * k + k - Suc 0")
   prefer 2
   apply (rule ccontr)
   apply (drule_tac x="t * k + k" in spec)
   apply (simp add: linorder_not_le)
   apply (drule pred_less_imp_le)+
   apply clarsimp
  apply simp
  apply (drule_tac x=i in le_imp_less_or_eq, erule disjE)
   apply simp
   apply (cut_tac b="k - Suc (Suc 0)" and m=k and k=t and a="Suc 0" and n=i in between_imp_mod_between)
   apply (simp add: mult.commute[of k])+
   apply (clarsimp elim!: dvdE)+
apply (rename_tac q)
apply (simp add: mult.commute[of k])
apply (subgoal_tac "Suc t ≤ q")
 prefer 2
 apply (rule Suc_leI)
 apply (rule mult_less_cancel2[where k=k, THEN iffD1, THEN conjunct2])
 apply (rule Suc_le_lessD)
 apply simp
apply (frule mult_le_mono1[of "Suc t" _ k])
apply (simp add: add.commute[of k])
apply (intro conjI impI allI)
 apply force
apply (simp add: linorder_not_less)
apply (case_tac "i > t * k + k")
 apply (drule_tac x="t * k + k" in spec)
 apply simp
apply (case_tac "i = t * k + k", simp)
apply simp
done

lemma i_shrink_eq_NoMsg_iAll_finish_event_conv: "
  ⟦ 1 < k; ⋀t. event t = (t mod k = k - 1); t0 = t * k ⟧ ⟹
  ((s ÷⇩i k) t = \<NoMsg>) =
  (s t0 = \<NoMsg> ∧ (○ t' t0 [0…]. (s t1 = \<NoMsg>. t1 𝒰 t2 ([0…] ⊕ t'). (event t2 ∧ s t2 = \<NoMsg>))))"
apply (simp add: i_shrink_eq_NoMsg_iAll_conv iT_add)
apply (unfold iTL_defs Ball_def Bex_def)
apply (simp add: iT_iff div_mult_cancel iFROM_cut_less iFROM_inext)
apply (subgoal_tac "t * k < t * k + k - Suc 0")
 prefer 2
 apply simp
apply (rule iffI)
 apply simp
 apply (rule_tac x="t * k + k - Suc 0" in exI)
 apply (simp add: mod_pred)
 apply (clarify, rename_tac t1)
 apply (drule Suc_leI[of "t * k"])
 apply (drule order_le_less[THEN iffD1], erule disjE)
  prefer 2
  apply simp
 apply (clarsimp simp: iIN_iff)
apply (clarify, rename_tac t1 t2)
apply (case_tac "t2 ≤ Suc (t * k)")
 apply (clarsimp simp: mod_Suc)
 apply (drule_tac s="Suc 0" in sym, drule_tac x="k - Suc 0" and f=Suc in arg_cong)
 apply (drule_tac y=t1 in order_le_imp_less_or_eq, erule disjE)
  apply (drule_tac n=t1 in Suc_leI)
  apply simp
 apply simp
apply clarsimp
apply (drule_tac x=t1 in spec)
apply (simp add: iIN_iff linorder_not_le)
apply (drule_tac y=t1 in order_le_imp_less_or_eq, erule disjE)
 prefer 2
 apply simp
apply (subgoal_tac "t * k + k - Suc 0 ≤ t2")
 prefer 2
 apply (rule le_diff_conv[THEN iffD2])
 apply (rule less_mod_eq_imp_add_divisor_le, simp)
 apply (simp add: mod_Suc)
apply simp
apply (drule_tac x="t * k + k - Suc 0" and y=t2 in order_le_imp_less_or_eq, erule disjE)
 prefer 2
 apply (drule_tac t=t2 in sym, simp)
 apply (drule_tac x=t1 in order_le_imp_less_or_eq, erule disjE)
 apply simp+
done

lemma i_shrink_eq_Msg_iUntil_finish_event_conv: "
  ⟦ 1 < k; m ≠ \<NoMsg>; ⋀t. event t = (t mod k = k - 1); t0 = t * k ⟧ ⟹
  ((s ÷⇩i k) t = m) = (
  (¬ event t1. t1 𝒰 t2 ([0…] ⊕ t0). event t2 ∧ s t2 = m) ∨
  (¬ event t1. t1 𝒰 t2 ([0…] ⊕ t0). (¬ event t2 ∧ s t2 = m ∧ (
    ○ t' t2 [0…]. (s t3 = \<NoMsg>. t3 𝒰 t4 ([0…] ⊕ t'). event t4 ∧ s t4 = \<NoMsg>)))))"
apply (simp add: i_shrink_eq_Msg_iSince_conv split del: if_split)
apply (simp only: iTL_defs iT_add iT_cut_greater iT_cut_less Ball_def Bex_def iT_iff iFROM_inext)
apply (subgoal_tac "t * k < t * k + k - Suc 0")
 prefer 2
 apply simp
apply (rule iffI)
 apply (subgoal_tac "⋀x. t * k ≤ x ⟹ x < t * k + k - Suc 0 ⟹ x mod k ≠ k - Suc 0")
  prefer 2
  apply (rule less_imp_neq)
  apply (rule le_pred_imp_less, simp)
  apply (simp only: mult.commute[of t k])
  apply (rule between_imp_mod_le[of "k - Suc 0 - Suc 0" k t])
  apply (simp split del: if_split)+
 apply (elim exE conjE, rename_tac t1)
 apply (drule_tac x=t1 in order_le_imp_less_or_eq, erule disjE)
  prefer 2
  apply (rule disjI1)
  apply (rule_tac x=t1 in exI)
  apply (clarsimp simp add: mod_pred iIN_iff)
 apply (rule disjI2)
 apply (rule_tac x=t1 in exI)
 apply (simp split del: if_split)
 apply (rule conjI)
  apply (rule_tac x="t * k + k - Suc 0" in exI)
  apply (clarsimp simp: mod_pred iIN_iff)
 apply (clarsimp simp: iIN_iff)
apply (erule disjE)
 apply (clarsimp, rename_tac t1)
 apply (drule_tac y=t1 in order_le_imp_less_or_eq, erule disjE)
  prefer 2
  apply (drule_tac t=t1 in sym, simp)
 apply (simp add: iIN_iff)
 apply (subgoal_tac "t1 ≤ t * k + k - Suc 0")
  prefer 2
  apply (rule ccontr)
  apply (drule_tac x="t * k + k - Suc 0" in spec)
  apply (simp add: mod_pred)
 apply (frule_tac a="t * k" and b=t1 and k="k - Suc 0" and m=k
   in le_mod_add_eq_imp_add_mod_le[OF less_imp_le, rule_format])
  apply (simp add: add.commute[of "t * k"] mod_pred)
 apply (rule_tac x=t1 in exI)
 apply simp
apply (clarsimp, rename_tac t1 t2)
apply (rule_tac x=t1 in exI)
apply (drule_tac y=t1 in order_le_imp_less_or_eq, erule disjE)
 prefer 2
 apply (drule_tac t=t1 in sym)
 apply (clarsimp simp: iIN_iff, rename_tac t3)
 apply (split if_split_asm)
  apply (subgoal_tac "t2 = Suc (t * k)")
   prefer 2
   apply simp
  apply (subgoal_tac "k = Suc (Suc 0)")
   prefer 2
   apply (simp add: mod_Suc)
  apply (simp add: mod_Suc)
 apply (simp add: iIN_iff)
 apply (subgoal_tac "t * k + k - Suc 0 ≤ t2")
  prefer 2
  apply (rule ccontr)
  apply (simp add: linorder_not_le)
  apply (drule_tac m=t2 in less_imp_le_pred)
  apply (simp only: mult.commute[of t])
  apply (frule_tac n=t2 in between_imp_mod_le[of "k - Suc (Suc 0)" k t _, OF diff_Suc_less, OF gr_implies_gr0])
   apply simp+
 apply (drule_tac x=t3 in spec)
 apply simp
 apply (drule_tac x=t3 in order_le_imp_less_or_eq)
 apply (drule_tac x="t * k + k - Suc 0" and y=t2 in order_le_imp_less_or_eq)
 apply (fastforce simp: numeral_2_eq_2 Suc_diff_Suc)
apply simp
apply (case_tac "Suc t1 = t2")
 apply (drule_tac t=t2 in sym)
 apply (simp add: iIN_iff numeral_2_eq_2 Suc_diff_Suc)
 apply (subgoal_tac "t1 ≤ t * k + k - Suc 0")
  prefer 2
  apply (rule ccontr)
  apply (drule_tac x="t * k + k - Suc 0" in spec)
  apply (simp add: mod_pred)
 apply (intro conjI impI)
 apply (subgoal_tac "Suc t1 = t * k + k - Suc 0", clarsimp)
 apply (subgoal_tac "t * k + (k - Suc 0) ≤ Suc t1")
  prefer 2
  apply (rule ccontr)
  apply (subgoal_tac "k - Suc 0 - Suc 0 < k")
   prefer 2
   apply simp
  apply (simp only: mult.commute[of t])
  apply (drule_tac n="Suc t1" in between_imp_mod_le[of "k - Suc 0 - Suc 0" k t])
  apply simp_all
apply (simp add: iIN_iff)
apply (subgoal_tac "t1 ≤ t * k + k - Suc 0")
 prefer 2
 apply (rule ccontr)
 apply (drule_tac x="t * k + k - Suc 0" in spec)
 apply (simp add: mod_pred)
apply (clarsimp, rename_tac t3)
apply (thin_tac "All (λx. A x ⟶ B (x mod k))" for A B)
apply (drule_tac x=t3 in spec)
apply (subgoal_tac "t3 ≤ t2 ⟹ s t3 = \<NoMsg>")
 prefer 2
 apply (drule_tac x=t3 and y=t2 in order_le_imp_less_or_eq, erule disjE)
  apply simp
 apply simp
apply (drule_tac P="t3 ≤ t2" in meta_mp)
 apply (subgoal_tac "t * k < t2")
  prefer 2
  apply (rule_tac y=t1 in less_trans, assumption+)
 apply (case_tac "t * k + (k - Suc 0) < t2")
  apply simp
 apply simp
apply (subgoal_tac "t * k + (k - Suc 0) ≤ t2")
 prefer 2
 apply (simp only: mult.commute[of t])
 apply (rule mult_divisor_le_mod_ge_imp_ge)
 apply simp_all
done

end