Theory IL_AF_Stream_Exec

Up to index of Isabelle/HOL/List-Infinite/Nat-Interval-Logic/AutoFocus-Stream

theory IL_AF_Stream_Exec
imports IL_AF_Stream AF_Stream_Exec
(*  Title:      IL_AF_Exec_Stream.thy
    Date:       Nov 2007
    Author:     David Trachtenherz
*)

header {* \textsc{AutoFocus} message stream processing and temporal logic on intervals *}

theory IL_AF_Stream_Exec
imports Main IL_AF_Stream AF_Stream_Exec
begin

subsection {* Correlation between Pre/Post-Conditions for @{text f_Exec_Comp_Stream} and @{text f_Exec_Comp_Stream_Init} *}

thm 
  i_Exec_Stream_Pre_Post1
  i_Exec_Stream_Pre_Post2
  i_Exec_Stream_Init_Pre_Post1
  i_Exec_Stream_Init_Pre_Post2
thm i_Exec_Stream_Pre_Post1
lemma i_Exec_Stream_Pre_Post1_iAll: "
  [| result = i_Exec_Comp_Stream trans_fun input c; 
    ∀x_n c_n. P1 x_n ∧ P2 c_n --> Q (trans_fun x_n c_n) |] ==>
  \<box> t I. (P1 (input t) ∧ P2 (result\<leftarrow> c t) --> Q (result t))"
by (simp add: i_Exec_Stream_Pre_Post1)
text {* Direct relation between input and result after transition *}
thm i_Exec_Stream_Pre_Post2
lemma i_Exec_Stream_Pre_Post2_iAll: "
  [| result = i_Exec_Comp_Stream trans_fun input c; 
    ∀x_n c_n. P c_n --> Q x_n (trans_fun x_n c_n) |] ==>
  \<box> t I. P (result\<leftarrow> c t) --> Q (input t) (result t)"
by (simp add: i_Exec_Stream_Pre_Post2)
lemma i_Exec_Stream_Pre_Post3_iAll_iNext: "
  [| result = i_Exec_Comp_Stream trans_fun input c; 
    ∀x_n c_n. P c_n --> Q x_n (trans_fun x_n c_n);
    ∀t∈I. inext t I' = Suc t |] ==>
  \<box> t I. P (result t) --> (\<bigcirc> t1 t I'. Q (input t1) (result t1))"
by (rule iallI, simp add: iNext_def i_Exec_Stream_Pre_Post2_Suc)

thm i_Exec_Stream_Init_Pre_Post1
lemma i_Exec_Stream_Init_Pre_Post1_iAll_iNext: "
  [| result = i_Exec_Comp_Stream_Init trans_fun input c; 
    ∀x_n c_n. P1 x_n ∧ P2 c_n --> Q (trans_fun x_n c_n);
    ∀t∈I. inext t I' = Suc t |] ==>
  \<box> t I. (P1 (input t) ∧ P2 (result t) --> (\<bigcirc> t1 t I'. Q (result t1)))"
by (rule iallI, simp add: iNext_def i_Exec_Stream_Init_Pre_Post1)

text {* Direct relation between input and state before transition *}
thm i_Exec_Stream_Init_Pre_Post2
lemma i_Exec_Stream_Init_Pre_Post2_iAll_iNext: "
  [| result = i_Exec_Comp_Stream_Init trans_fun input c; 
    ∀x_n c_n. P x_n c_n --> Q (trans_fun x_n c_n);
    ∀t∈I. inext t I' = Suc t |] ==>
  \<box> t I. (P (input t) (result t) --> (\<bigcirc> t1 t I'. Q (result t1)))"
by (rule iallI, simp add: iNext_def i_Exec_Stream_Init_Pre_Post2)

text {* Relation between input and output *}
thm i_Exec_Stream_Pre_Post3_iAll_iNext
lemma i_Exec_Stream_Init_Pre_Post3_iAll_iNext: "
  [| result = i_Exec_Comp_Stream_Init trans_fun input c; 
    ∀x_n c_n. P c_n --> Q x_n (trans_fun x_n c_n);
    ∀t∈I. inext t I' = Suc t |] ==>
  \<box> t I. (P (result t) --> (\<bigcirc> t1 t I'. Q (input\<leftarrow> \<NoMsg> t1) (result t1)))"
apply (rule iallI, unfold iNext_def)
apply (simp add: ilist_Previous_Suc i_Exec_Stream_Init_nth_Suc_eq_i_Exec_Stream_nth i_Exec_Stream_Previous_i_Exec_Stream_Init)
thm i_Exec_Stream_Pre_Post2_iAll[OF refl]
apply (blast dest: i_Exec_Stream_Pre_Post2_iAll[OF refl])
done



subsection {* @{text "i_Exec_Comp_Stream_Acc_Output"} and temporal operators with bounded intervals. *}

text {* Temporal relation between uncompressed and compressed output of accelerated components. *}

thm i_shrink_eq_NoMsg_iAll_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv: "
  0 < k ==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (\<box> t1 [t * k…,k - Suc 0]. (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) t1 = \<NoMsg>)"
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_NoMsg_iAll_conv)
lemma i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv2: "
  0 < k ==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (\<box> t1 […k - Suc 0] ⊕ (t * k). (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) t1 = \<NoMsg>)"
by (simp add: iT_add i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv)

lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_NoMsg_iAll_conv: "
  0 < k ==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (\<box> t1 [Suc (t * k)…,k - Suc 0]. (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) t1 = \<NoMsg>)"
apply (unfold i_Exec_Comp_Stream_Acc_Output_def)
thm i_shrink_eq_NoMsg_iAll_conv
apply (simp add: i_shrink_eq_NoMsg_iAll_conv i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)
apply (rule_tac t="[Suc (t * k)…,k - Suc 0]" and s="[t * k…,k - Suc 0] ⊕ 1" in subst)
 apply (simp add: iIN_add)
apply (simp add: iT_Plus_iAll_conv)
done

thm i_shrink_eq_Msg_iEx_iAll_cut_greater_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_iEx_iAll_cut_greater_conv: "
  [| 0 < k; m ≠ \<NoMsg>; s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |] ==>
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  (\<diamond> t1 [t * k…,k - Suc 0]. (s t1 = m ∧ 
    (\<box> t2 [t * k…,k - Suc 0] \<down>> t1 . s t2 = \<NoMsg>)))"
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_Msg_iEx_iAll_cut_greater_conv)
thm i_shrink_eq_Msg_iEx_iAll_cut_greater_conv2
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_iEx_iAll_cut_greater_conv2: "
  [| 0 < k; m ≠ \<NoMsg>; s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |] ==>
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  (\<diamond> t1 […k - Suc 0] ⊕ (t * k). (s t1 = m ∧ 
    (\<box> t2 ([…k - Suc 0] ⊕ (t * k)) \<down>> t1 . s t2 = \<NoMsg>)))"
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_Msg_iEx_iAll_cut_greater_conv2)


thm i_shrink_eq_Msg_iSince_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv: "
  [| 0 < k; m ≠ \<NoMsg>; s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |] ==>
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  (s t2 = \<NoMsg>. t2 \<S> t1 [t * k…,k - Suc 0]. s t1 = m)"
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_Msg_iSince_conv)
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv2: "
  [| 0 < k; m ≠ \<NoMsg>; s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |] ==>
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  (s t2 = \<NoMsg>. t2 \<S> t1 […k - Suc 0] ⊕ (t * k). s t1 = m)"
by (simp add: i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv iT_add)

thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv[OF _ _ refl]
lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_Msg_iSince_conv: "
  [| 0 < k; m ≠ \<NoMsg>; s = (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) |] ==>
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  (s t2 = \<NoMsg>. t2 \<S> t1 [Suc (t * k)…,k - Suc 0]. s t1 = m)"
apply (unfold i_Exec_Comp_Stream_Acc_Output_def)
apply (simp add: i_shrink_eq_Msg_iSince_conv i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)
apply (rule_tac t="[Suc (t * k)…,k - Suc 0]" and s="[t * k…,k - Suc 0] ⊕ 1" in subst)
 apply (simp add: iIN_add)
apply (simp add: iT_Plus_iSince_conv)
done
thm i_Exec_Comp_Stream_Acc_Output__Init__eq_Msg_iSince_conv[OF _ _ refl]

lemma i_Exec_Comp_Stream_Acc_Output__eq_iAll_iSince_conv: "
  [| 0 < k; s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |] ==>
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  ((m = \<NoMsg> --> (\<box> t1 [t * k…,k - Suc 0]. s t1 = \<NoMsg>)) ∧
  ((m ≠ \<NoMsg> --> (s t2 = \<NoMsg>. t2 \<S> t1 [t * k…,k - Suc 0]. s t1 = m))))"
apply (case_tac "m = \<NoMsg>")
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv)
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv)
done
lemma i_Exec_Comp_Stream_Acc_Output__eq_iAll_iSince_conv2: "
  [| 0 < k; s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |] ==>
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  ((m = \<NoMsg> --> (\<box> t1 […k - Suc 0] ⊕ (t * k). s t1 = \<NoMsg>)) ∧
  ((m ≠ \<NoMsg> --> (s t2 = \<NoMsg>. t2 \<S> t1 […k - Suc 0] ⊕ (t * k). s t1 = m))))"
by (simp add: i_Exec_Comp_Stream_Acc_Output__eq_iAll_iSince_conv iT_add)



subsection {* @{text "i_Exec_Comp_Stream_Acc_Output"} and temporal operators with unbounded intervals and start/finish events. *}


thm i_shrink_eq_NoMsg_iAll_start_event_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_start_event_conv: "
  [| 0 < k; !! t. event t = (t mod k = 0); t0 = t * k;
    s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |]==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (s t0 = \<NoMsg> ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 [0…] ⊕ t'. event t2)))"
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_NoMsg_iAll_start_event_conv)
lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_NoMsg_iAll_start_event_conv: "
  [| 0 < k; !! t. event t = ((t + k - Suc 0) mod k = 0); t0 = Suc (t * k);
    s = (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) |]==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (s t0 = \<NoMsg> ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 [0…] ⊕ t'. event t2)))"
apply (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_NoMsg_iAll_start_event_conv)
apply (simp add: iT_add iNext_def iFROM_inext iT_iff)
apply (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)
apply (rule_tac t="[Suc (Suc (t*k))…]" and s="[Suc (t*k)…] ⊕ Suc 0" in subst)
 apply (simp add: iFROM_add)
thm iT_Plus_iUntil_conv
apply (simp add: iT_Plus_iUntil_conv)
done
lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_NoMsg_iAll_start_event2_conv: "
  [| Suc 0 < k; !! t. event t = (t mod k = Suc 0); t0 = Suc (t * k);
    s = (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) |]==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (s t0 = \<NoMsg> ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 [0…] ⊕ t'. event t2)))"
thm i_Exec_Comp_Stream_Acc_Output__Init__eq_NoMsg_iAll_start_event_conv
thm mod_eq_Suc_0_conv
by (simp add: i_Exec_Comp_Stream_Acc_Output__Init__eq_NoMsg_iAll_start_event_conv mod_eq_Suc_0_conv)

thm i_shrink_eq_Msg_iUntil_start_event_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_iUntil_start_event_conv: "
  [| 0 < k; m ≠ \<NoMsg>; !!t. event t = (t mod k = 0); t0 = t * k;
    s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |] ==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = (
  (s t0 = m ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 ([0…] ⊕ t'). event t2))) ∨
  (\<bigcirc> t' t0 [0…]. (¬ event t1. t1 \<U> t2 ([0…] ⊕ t'). (
    s t2 = m ∧ ¬ event t2 ∧ (\<bigcirc> t'' t2 [0…]. 
      (s t3 = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t''). event t4))))))"
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_Msg_iUntil_start_event_conv)
lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_Msg_iUntil_start_event_conv: "
  [| 0 < k; m ≠ \<NoMsg>; !!t. event t = ((t + k - Suc 0) mod k = 0); t0 = Suc (t * k);
    s = (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) |] ==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = (
  (s t0 = m ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 ([0…] ⊕ t'). event t2))) ∨
  (\<bigcirc> t' t0 [0…]. (¬ event t1. t1 \<U> t2 ([0…] ⊕ t'). (
    s t2 = m ∧ ¬ event t2 ∧ (\<bigcirc> t'' t2 [0…]. 
      (s t3 = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t''). event t4))))))"
apply (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_Msg_iUntil_start_event_conv)
apply (simp add: iNext_def iFROM_inext iFROM_iff iT_add)
apply (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)
apply (simp only: Suc_eq_plus1 iFROM_add[symmetric])
apply (simp add: iT_Plus_iUntil_conv)
apply (simp only: Suc_eq_plus1 iFROM_add[symmetric])
apply (simp add: iT_Plus_iUntil_conv)
done
lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_Msg_iUntil_start_event2_conv: "
  [| Suc 0 < k; m ≠ \<NoMsg>; !!t. event t = (t mod k = Suc 0); t0 = Suc (t * k);
    s = (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) |] ==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = (
  (s t0 = m ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 ([0…] ⊕ t'). event t2))) ∨
  (\<bigcirc> t' t0 [0…]. (¬ event t1. t1 \<U> t2 ([0…] ⊕ t'). (
    s t2 = m ∧ ¬ event t2 ∧ (\<bigcirc> t'' t2 [0…]. 
      (s t3 = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t''). event t4))))))"
by (simp add: i_Exec_Comp_Stream_Acc_Output__Init__eq_Msg_iUntil_start_event_conv mod_eq_Suc_0_conv)


thm i_shrink_eq_NoMsg_iAll_finish_event_conv
thm i_shrink_eq_Msg_iUntil_finish_event_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_finish_event_conv: "
  [| Suc 0 < k; !! t. event t = (t mod k = k - Suc 0); t0 = t * k;
    s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |]==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (s t0 = \<NoMsg> ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 [0…] ⊕ t'. event t2 ∧ s t2 = \<NoMsg>)))"
by (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_NoMsg_iAll_finish_event_conv)
lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_NoMsg_iAll_finish_event_conv: "
  [| Suc 0 < k; !! t. event t = (t mod k = 0); t0 = Suc (t * k);
    s = (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) |]==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = \<NoMsg>) = 
  (s t0 = \<NoMsg> ∧ (\<bigcirc> t' t0 [0…]. (s t1 = \<NoMsg>. t1 \<U> t2 [0…] ⊕ t'. event t2 ∧ s t2 = \<NoMsg>)))"
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_finish_event_conv)
apply (simp add: iNext_def iFROM_inext iFROM_iff iT_add)
apply (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)
apply (rule_tac t="[Suc (Suc (t * k))…]" and s="[Suc (t * k)…] ⊕ 1" in subst)
 apply (simp add: iFROM_add)
thm iT_Plus_iUntil_conv
apply (simp add: iT_Plus_iUntil_conv)
apply (simp add: mod_eq_divisor_minus_Suc_0_conv)
done

thm i_shrink_eq_Msg_iUntil_finish_event_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_iUntil_finish_event_conv: "
  [| 0 < k; m ≠ \<NoMsg>; !! t. event t = (t mod k = k - Suc 0); t0 = t * k;
    s = (output_fun o i_Exec_Comp_Stream trans_fun (input \<odot>i k) c) |]==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  ((¬ event t1. t1 \<U> t2 ([0…] ⊕ t0). event t2 ∧ s t2 = m) ∨
  (¬ event t1. t1 \<U> t2 ([0…] ⊕ t0). (¬ event t2 ∧ s t2 = m ∧ (
    \<bigcirc> t' t2 [0…]. (s t3 = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t'). event t4 ∧ s t4 = \<NoMsg>)))))"
apply (case_tac "k = Suc 0")
 apply (simp add: iT_add iT_not_empty iFROM_Min)
apply (drule neq_le_trans[OF not_sym], simp)
thm i_shrink_eq_Msg_iUntil_finish_event_conv[unfolded One_nat_def]
apply (simp add: i_Exec_Comp_Stream_Acc_Output_def i_shrink_eq_Msg_iUntil_finish_event_conv)
done

lemma i_Exec_Comp_Stream_Acc_Output__Init__eq_Msg_iUntil_finish_event_conv: "
  [| Suc 0 < k; m ≠ \<NoMsg>; !! t. event t = (t mod k = 0); t0 = Suc (t * k);
    s = (output_fun o i_Exec_Comp_Stream_Init trans_fun (input \<odot>i k) c) |]==> 
  ((i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c) t = m) = 
  ((¬ event t1. t1 \<U> t2 ([0…] ⊕ t0). event t2 ∧ s t2 = m) ∨
  (¬ event t1. t1 \<U> t2 ([0…] ⊕ t0). (¬ event t2 ∧ s t2 = m ∧ (
    \<bigcirc> t' t2 [0…]. (s t3 = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t'). event t4 ∧ s t4 = \<NoMsg>)))))"
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_Msg_iUntil_finish_event_conv)
apply (simp add: iNext_def iFROM_inext iT_iff)
apply (simp add: i_Exec_Stream_Init_eq_i_Exec_Stream_Cons)
apply (simp add: iT_Plus_iUntil_conv)
apply (simp add: mod_eq_divisor_minus_Suc_0_conv add_Suc[symmetric] del: add_Suc)
done


subsection {* @{text "i_Exec_Comp_Stream_Acc_Output"} and temporal operators with idle states. *}

thm 
  f_expand_nth_interval_eq_nth_append_replicate_NoMsg
  f_expand_nth_interval_eq_replicate_NoMsg
  i_expand_nth_interval_eq_nth_append_replicate_NoMsg
  i_expand_nth_interval_eq_replicate_NoMsg

thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv


thm i_Exec_Stream_Acc_Output__State_Idle_nth
lemma i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv: "
  [| 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = \<NoMsg>) =
  (output_fun (s t1) = \<NoMsg>. t1 \<U> t2 ([0…] ⊕ t0). (
   output_fun (s t2) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t2))))"
apply (case_tac "k = Suc 0")
 apply (simp add: iUntil_def)
 apply (rule iffI)
  apply (rule_tac t=t in iexI)
   apply (simp add: iT_add iT_cut_less)
  apply (simp add: iT_add iT_iff)
 apply (clarify, rename_tac t1)
 apply (simp add: iT_add iT_iff iT_cut_less)
 apply (drule order_le_less[THEN iffD1])
 apply (erule disjE)
  apply (drule_tac t=t in ispec)
  apply (simp add: iT_iff)+
apply (drule order_neq_le_trans[OF not_sym Suc_leI], assumption)
thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv)
apply (simp add: iT_add i_Exec_Stream_nth i_Exec_Stream_Acc_LocalState_nth)
apply (simp add: i_take_Suc_conv_app_nth[of t])
apply (simp add: i_expand_i_take_mult[symmetric] f_Exec_append)
apply (subgoal_tac "∀t1 ∈ [t * k…,k - Suc 0]. input \<odot>i k \<Down> Suc t1 \<up> (t * k) = input t # \<NoMsg>t1 - t * k")
 prefer 2
 apply (simp add: i_expand_nth_interval_eq_nth_append_replicate_NoMsg iIN_iff)
apply (case_tac "output_fun (f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc (t * k)) c) ≠ \<NoMsg>")
 apply (subgoal_tac "
   ¬ (\<box> t1 [t * k…,k - Suc 0]. output_fun (f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc t1) c) = \<NoMsg>)")
  prefer 2
  apply simp
  apply (rule_tac t="t * k" in iexI, assumption)
  apply (simp add: iIN_iff)
 apply (simp add: not_iUntil del: not_iAll)
 apply (clarsimp simp: iT_iff, rename_tac t1 t2)
 apply (case_tac "t1 = t * k", simp)
 apply (drule order_le_neq_trans[OF _ not_sym], assumption)
 apply (rule_tac t="t * k" in iexI, simp)
 apply (simp add: iFROM_cut_less1 iIN_iff)

apply (case_tac "
  State_Idle localState output_fun trans_fun
    (localState ((trans_fun (input t) (f_Exec_Comp trans_fun (input \<odot>i k \<Down> (t * k)) c))))")
 apply (subgoal_tac "
   (\<box> t1 [t * k…,k - Suc 0]. output_fun (f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc t1) c) = NoMsg)")
  prefer 2
  apply (clarsimp simp: iIN_iff, rename_tac t1)
  thm subst[OF i_take_drop_append, rule_format]
  apply (rule_tac m="t * k" and n="Suc t1" in subst[OF i_take_drop_append, rule_format], simp)
  apply (drule_tac x=t1 in bspec, simp add: iT_iff)
  apply (simp add: f_Exec_append del: i_take_drop_append)
  apply (simp add: i_take_Suc_conv_app_nth f_Exec_append i_expand_nth_mult)
  thm f_Exec_State_Idle_replicate_NoMsg_output
  apply (rule f_Exec_State_Idle_replicate_NoMsg_output, assumption+)
 apply (simp add: iUntil_def)
 apply (rule_tac t="t * k" in iexI)
  apply (simp add: i_take_Suc_conv_app_nth f_Exec_append i_expand_nth_mult iFROM_cut_less)
 apply (simp add: iFROM_iff)
apply (subgoal_tac "∀i < k. input \<odot>i k \<Up> Suc (t * k) \<Down> i = NoMsgi")
 prefer 2
 apply (simp add: list_eq_iff i_expand_nth_if)
apply (rule iffI)
 thm State_Idle_imp_exists_state_change2
 apply (frule State_Idle_imp_exists_state_change2, assumption)
 apply (elim exE conjE, rename_tac i)
 apply (frule Suc_less_pred_conv[THEN iffD2])
 apply (simp only: iUntil_def)
 apply (rule_tac t="Suc (t * k + i)" in iexI)
  apply (rule conjI)
   apply (drule_tac t="Suc (t * k + i)" in ispec)
    apply (simp add: iIN_iff)
   apply (rule conjI, simp)
   apply (rule_tac t="Suc (Suc (t * k + i))" and s="Suc (t * k) + Suc i" in subst, simp)
   apply (subst i_take_add)
   apply (drule_tac x="Suc i" in spec)+
   apply (simp add: i_take_Suc_conv_app_nth f_Exec_append i_expand_nth_mult)
  apply (rule iallI, rename_tac t1)
  apply (drule_tac t=t1 in ispec)
   apply (drule_tac m="Suc i" in less_imp_le_pred)
   apply (clarsimp simp: iIN_iff iFROM_cut_less1)
   apply (rule order_trans, assumption)
   apply simp
  apply assumption
 apply (simp add: iFROM_iff)
apply (rule iallI)
apply (unfold iUntil_def, elim iexE conjE, rename_tac t2)
apply (case_tac "t1 < t2")
 apply (drule_tac t=t1 in ispec)
  apply (simp add: cut_less_mem_iff iT_iff)
 apply simp
apply (simp add: linorder_not_less)
apply (case_tac "t1 = t2", simp)
apply (drule le_neq_trans[OF _ not_sym], assumption)
apply (drule_tac i=t2 in less_imp_add_positive, elim exE conjE, rename_tac i)
apply (drule_tac t=t1 in sym)
apply (simp del: add_Suc add: add_Suc[symmetric] i_take_add f_Exec_append iFROM_iff)
apply (rule_tac t="input \<odot>i k \<Up> Suc t2 \<Down> i" and s="\<NoMsg>i" in subst)
 apply (rule list_eq_iff[THEN iffD2])
 apply simp
 apply (intro allI impI, rename_tac i1)
 apply (simp add: i_expand_nth_if)
 apply (subst imp_conv_disj, rule disjI1)
 thm if_not_P'
 apply simp
 apply (subgoal_tac "t * k < Suc (t2 + i1) ∧ Suc (t2 + i1) < t * k + k", elim conjE)
  prefer 2
  apply (simp add: iIN_iff)
 apply (simp only: mult_commute[of _ k])
 apply (rule between_imp_mod_gr0, assumption+)
thm f_Exec_State_Idle_replicate_NoMsg_gr0_output
apply (rule f_Exec_State_Idle_replicate_NoMsg_gr0_output, assumption+)
done
thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv[OF _ _ refl refl]

lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_imp: "
  [| 0 < k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    t0 = t * k;
    t1 ∈ [0…, k - Suc 0] ⊕ t0;
    State_Idle localState output_fun trans_fun (localState (s t1));
    output_fun (s t1) ≠ \<NoMsg> |] ==> 
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = output_fun (s t1)"
apply (case_tac "k = Suc 0")
 apply (simp add: iIN_0 iT_Plus_singleton)
apply (drule order_neq_le_trans[OF not_sym], rule Suc_leI, assumption)
apply (simp add: iT_add iT_iff, erule conjE)
apply (simp only: i_Exec_Stream_Acc_Output_nth i_Exec_Stream_nth)
apply (rule_tac t="Suc t1" and s="t * k + (Suc t1 - t * k)" in subst, simp)
apply (simp only: i_take_add f_Exec_append i_expand_i_take_mult)
apply (subgoal_tac "input \<odot>i k \<Up> (t * k) \<Down> (Suc t1 - t * k) = input t # \<NoMsg>t1 - t * k")
 prefer 2
 apply (simp add: i_take_i_drop)
 apply (subst i_expand_nth_interval_eq_nth_append_replicate_NoMsg)
 apply (simp del: f_Exec_Comp_Stream.simps)+
apply (subgoal_tac "∃i. k - Suc 0 = t1 - t * k + i")
 prefer 2
 thm le_iff_add[THEN iffD1]
 apply (rule le_iff_add[THEN iffD1])
 apply (simp add: le_diff_conv)
apply (erule exE)
apply (simp only: replicate_add)
apply (subst append_Cons[symmetric])
thm State_Idle_append_replicate_NoMsg_output_last_message
apply (subst State_Idle_append_replicate_NoMsg_output_last_message)
 apply (simp only: f_Exec_append[symmetric])
 apply (rule_tac t="input \<Down> t \<odot>f k @ input t # NoMsgt1 - t * k" and s="input \<odot>i k \<Down> Suc t1" in subst)
  apply (subst i_expand_i_take_mult[symmetric])
  apply (drule_tac t="input t # NoMsgt1 - t * k" in sym)
  apply (simp add: i_take_add[symmetric])
 apply assumption
apply (subgoal_tac "
  f_Exec_Comp_Stream trans_fun (input t # NoMsgt1 - t * k)
   (f_Exec_Comp trans_fun (input \<Down> t \<odot>f k) c) ≠ []")
 prefer 2
 apply (simp add: f_Exec_Stream_not_empty_conv)
thm last_message_Msg_eq_last
apply (rule ssubst[OF last_message_Msg_eq_last])
  apply simp
 apply (subst map_last, simp)
 thm f_Exec_eq_f_Exec_Stream_last2
 apply (subst f_Exec_eq_f_Exec_Stream_last2[symmetric], simp)
 apply (subst f_Exec_append[symmetric])
 apply (rule_tac t="input \<Down> t \<odot>f k @ input t # NoMsgt1 - t * k" and s="input \<odot>i k \<Down> Suc t1" in subst)
  apply (subst i_expand_i_take_mult[symmetric])
  apply (rule_tac t="Suc t1" and s="t * k + (Suc t1 - t * k)" in subst, simp)
  apply (subst i_take_add, simp)
 apply assumption
apply (subst map_last, simp)
apply (subst f_Exec_eq_f_Exec_Stream_last2[symmetric], simp+)
done


thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2: "
  [| 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    t1 ∈ [0…, k - Suc 0] ⊕ t0;
    State_Idle localState output_fun trans_fun (localState (s t1));
    output_fun (s t1) ≠ \<NoMsg> |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  (\<diamond> t1 [0…, k - Suc 0] ⊕ t0. (
      (output_fun (s t1) = m ∧ State_Idle localState output_fun trans_fun (localState (s t1)))))"
apply (case_tac "k = Suc 0")
 apply (simp add: iIN_0 iT_Plus_singleton)
apply (drule order_neq_le_trans[OF not_sym], rule Suc_leI, assumption)
apply simp
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_imp
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_imp)
apply (rule iffI)
 apply blast
apply (clarify, rename_tac t1')
apply (subgoal_tac "t1' = t1")
 prefer 2
 apply (rule ccontr)
 apply (simp add: i_Exec_Stream_nth)
 apply (subgoal_tac "
   !! n1 n2. 
   [| n1 < n2; n1 ∈ [0…,k - Suc 0] ⊕ t * k; n2 ∈ [0…,k - Suc 0] ⊕ t * k; 
     State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc n1) c));
     output_fun (f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc n2) c) ≠ NoMsg |] ==> 
   False")
  prefer 2
  apply (drule_tac i=n1 in less_imp_add_positive, elim exE conjE, rename_tac i)
  apply (drule_tac t=n2 in sym, simp)
  apply (simp only: add_Suc[symmetric] i_take_add f_Exec_append)
  thm i_expand_nth_interval_eq_replicate_NoMsg
  apply (subgoal_tac "input \<odot>i k \<Up> Suc n1 \<Down> i = \<NoMsg>i")
   prefer 2
   apply (subst i_take_i_drop)
   apply (rule_tac t="\<NoMsg>i" and s="\<NoMsg>i + Suc n1 - Suc n1" in subst, simp)
   thm i_expand_nth_interval_eq_replicate_NoMsg
   apply (rule_tac t=t in i_expand_nth_interval_eq_replicate_NoMsg)
   apply (simp add: iT_add iT_iff)+
  thm f_Exec_State_Idle_replicate_NoMsg_gr0_output
  apply (frule_tac c="f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc n1) c" and n=i
     in f_Exec_State_Idle_replicate_NoMsg_gr0_output)
  apply (fastsimp dest: linorder_neq_iff[THEN iffD1])+
done

text {* Here the property to be checked uses only unbounded intervals suitable for LTL. *}
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv: "
  [| 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    t1 ∈ [0…, k - Suc 0] ⊕ t0;
    State_Idle localState output_fun trans_fun (localState (s t1));
    output_fun (s t1) ≠ \<NoMsg> |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  ((¬ State_Idle localState output_fun trans_fun (localState (s t2))). t2 \<U> t1 [0…] ⊕ t0. (
      (output_fun (s t1) = m ∧ State_Idle localState output_fun trans_fun (localState (s t1)))))"
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2
apply (subst i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2, assumption+)
apply (unfold iUntil_def)
apply (rule iffI)
 apply (elim iexE conjE, rename_tac t2)
 apply (rule_tac t=t2 in iexI) 
  prefer 2
  apply (simp add: iT_add iT_iff)
 apply simp
 apply (rule iallI, rename_tac t2')
 apply (rule ccontr)
 apply (simp add: cut_less_mem_iff iT_iff iT_add, elim conjE)
 apply (frule_tac n=t2' in le_imp_less_Suc)
 apply (frule_tac i=t2' in less_imp_add_positive, elim exE conjE, rename_tac i)
 apply (drule_tac t=t2 in sym)
 apply (simp only: i_Exec_Stream_nth add_Suc[symmetric] i_take_add f_Exec_append)
 apply (simp only: i_take_i_drop)
 apply (subgoal_tac "input \<odot>i k \<Down> (i + Suc t2') \<up> Suc t2' = \<NoMsg>i")
  prefer 2
  thm i_expand_nth_interval_eq_replicate_NoMsg
  apply (rule_tac t="\<NoMsg>i" and s="\<NoMsg>i + Suc t2' - Suc t2'" in subst, simp)
  apply (rule_tac t=t in i_expand_nth_interval_eq_replicate_NoMsg)
  apply simp+
 thm f_Exec_State_Idle_replicate_NoMsg_gr0_output
 apply (drule_tac c="(f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc t2') c)" and n=i
   in f_Exec_State_Idle_replicate_NoMsg_gr0_output, assumption)
 apply simp
apply (fastsimp simp: iT_add iT_iff i_Exec_Stream_Acc_LocalState_nth i_Exec_Stream_nth)
done

lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp2: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    t1 ∈ [0…, k - Suc 0] ⊕ t0;
    output_fun (s t1) = m;
    \<bigcirc> t2 t1 [0…]. 
     ((output_fun (s t3) = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t2). 
      (output_fun (s t4) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t4))))) |] ==> 
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m"
apply (clarsimp simp: iUntil_def iNext_def iT_inext iT_iff, rename_tac t2)
apply (simp only: i_Exec_Stream_Acc_Output_nth i_Exec_Stream_Acc_LocalState_nth i_Exec_Stream_nth)
apply (rule last_message_conv[THEN iffD2], assumption)
apply (clarsimp simp: iT_add iT_iff simp del: f_Exec_Comp_Stream.simps)
apply (subgoal_tac "t1 - t * k < k")
 prefer 2
 apply simp
apply (rule_tac x="t1 - t * k" in exI)
apply (rule conjI, simp)
apply (rule conjI)
 apply (simp add: f_Exec_Stream_nth min_eqL del: f_Exec_Comp.simps f_Exec_Comp_Stream.simps)
 apply (simp only: f_Exec_append[symmetric])
 thm i_expand_i_take_mult_Suc
 apply (subst i_expand_i_take_mult_Suc[symmetric], assumption)
 apply simp
apply (intro allI impI)
apply (simp only: f_Exec_Stream_length length_Cons length_replicate Suc_pred
  nth_map f_Exec_Stream_nth take_Suc_Cons take_replicate min_eqL[OF less_imp_le_pred])
apply (subst f_Exec_append[symmetric])
apply (subst i_expand_i_take_mult_Suc[symmetric], assumption)
apply (case_tac "t2 ≤ t * k + j")
 prefer 2
 apply fastsimp
apply (drule_tac x=t2 in order_le_less[THEN iffD1, rule_format])
apply (erule disjE)
 prefer 2
 apply simp
apply (subgoal_tac "
  State_Idle localState output_fun trans_fun 
    (localState (f_Exec_Comp trans_fun (input \<odot>i k \<Down> (t * k + Suc j)) c))")
 prefer 2
 apply (rule_tac t="t * k + Suc j" and s="Suc t2 + (t * k + j - t2)" in subst, simp)
 apply (simp only: i_take_add f_Exec_append)
 apply (simp only: i_take_i_drop)
 apply simp
 thm i_expand_nth_interval_eq_replicate_NoMsg
 apply (rule_tac t=t in ssubst[OF i_expand_nth_interval_eq_replicate_NoMsg, rule_format], simp+)
 thm f_Exec_State_Idle_replicate_NoMsg_state
 apply (simp add: f_Exec_State_Idle_replicate_NoMsg_state)
apply (subgoal_tac "t1 div k = t ∧ t2 div k = t", elim conjE)
 prefer 2
 thm le_less_imp_div
 apply (simp add: le_less_imp_div)
apply (simp only: i_expand_i_take_Suc i_expand_i_take_mult_Suc f_Exec_append)
apply (simp add: f_Exec_append)
thm f_Exec_State_Idle_replicate_NoMsg_gr_output
apply (rule_tac m="t2 mod k" in f_Exec_State_Idle_replicate_NoMsg_gr_output, assumption)
apply (simp add: mod_div_equality')
done

lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    \<box> t1 [0…, k - Suc 0] ⊕ t0. ¬ (
      State_Idle localState output_fun trans_fun (localState (s t1)) ∧
      output_fun (s t1) ≠ \<NoMsg>) |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  (\<diamond> t1 [0…, k - Suc 0] ⊕ t0. (
     (output_fun (s t1) = m) ∧
     (\<bigcirc> t2 t1 [0…]. 
      ((output_fun (s t3) = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t2). 
      (output_fun (s t4) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t4))))))))"
apply (rule iffI)
 apply (simp only: i_Exec_Stream_Acc_Output_nth i_Exec_Stream_nth)
 apply (simp only: iNext_def iFROM_iff iFROM_inext)
 thm last_message_conv
 thm last_message_conv[THEN iffD1]
 apply (frule last_message_conv[THEN iffD1], assumption)
 apply (elim exE conjE, rename_tac i)
 apply (simp add: f_Exec_Stream_nth min_eqL del: f_Exec_Comp.simps f_Exec_Comp_Stream.simps de_Morgan_conj)
 apply (subgoal_tac "
   \<box> t' ([0…] ⊕ (Suc (t * k + i))) \<down>< (t * k + k).
   output_fun (f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc t') c) = \<NoMsg>")
  prefer 2
  apply (rule iallI, rename_tac t')
  apply (simp only: iT_add iT_iff cut_less_mem_iff, erule conjE)
  apply (drule_tac x="t' - t * k" in spec)
  apply (subgoal_tac "t' - t * k < k")
   prefer 2
   apply simp
  apply (simp add: f_Exec_Stream_nth min_eqL del: f_Exec_Comp_Stream.simps de_Morgan_conj)
  apply (subgoal_tac "t * k ≤ t'")
   prefer 2
   apply simp
  apply (rule_tac t="Suc t'" and s="t * k + (Suc t' - t * k)" in subst, simp)
  apply (simp only: i_take_add f_Exec_append i_expand_i_take_mult)
  apply (simp add: i_take_i_drop)
  thm i_expand_nth_interval_eq_nth_append_replicate_NoMsg
  apply (rule ssubst[OF i_expand_nth_interval_eq_nth_append_replicate_NoMsg])
  apply (simp del: f_Exec_Comp_Stream.simps de_Morgan_conj)+
 apply (rule_tac t="t * k + i" in iexI)
  prefer 2
  apply (simp add: iT_add iT_iff)
 apply (rule conjI)
  thm i_expand_i_take_mult_Suc
  apply (simp add: add_Suc_right[symmetric] i_expand_i_take_mult_Suc f_Exec_append del: add_Suc_right)
 apply (simp only: i_Exec_Stream_Acc_LocalState_nth i_expand_i_take_mult[symmetric] mult_Suc add_commute[of k])
 apply (subgoal_tac "
   ¬ State_Idle localState output_fun trans_fun
       (localState (f_Exec_Comp trans_fun (input \<odot>i k \<Down> (t * k + Suc i)) c))")
  prefer 2
  apply (drule_tac t="t * k + i" in ispec)
   apply (simp add: iT_add iT_iff)
  apply (simp add: add_Suc_right[symmetric] i_expand_i_take_mult_Suc f_Exec_append i_expand_i_take_mult del: add_Suc_right)
 apply (thin_tac "last_message ?x = m")
 apply (drule_tac 
   a="t * k + k" and b="t * k + Suc (k - Suc 0)" and
   P="λx. State_Idle localState output_fun trans_fun
          (localState (f_Exec_Comp trans_fun (input \<odot>i k \<Down> x) c))" in back_subst, simp)
  apply (simp only: i_expand_i_take_mult_Suc f_Exec_append)
 thm State_Idle_imp_exists_state_change
 apply (frule_tac n="k - Suc 0 - i" in State_Idle_imp_exists_state_change)
  apply (simp add: f_Exec_append[symmetric] replicate_add[symmetric])
 apply (elim exE conjE, rename_tac i1)
 thm less_diff_conv[THEN iffD1, rule_format]
 apply (frule_tac i=i1 in less_diff_conv[THEN iffD1, rule_format])
 thm subst[OF add_commute, rule_format]
 apply (drule_tac a=i1 and P="λx. (x < k - Suc 0)" in subst[OF add_commute, rule_format])
 apply (frule Suc_less_pred_conv[THEN iffD2])
 apply (simp only: iUntil_def)
 apply (rule_tac t="t * k + Suc (i + i1)" in iexI)
  prefer 2
  apply (simp add: iT_add iT_iff)
 apply (rule conjI)
  apply (drule_tac t="t * k + Suc (i + i1)" in ispec)
   apply (simp add: iT_add iT_iff cut_less_mem_iff)
  apply (subgoal_tac "Suc (t * k + Suc (i + i1)) = t * k + Suc (Suc (i + i1))")
   prefer 2
   apply simp
  thm i_expand_i_take_mult_Suc
  apply (simp only: i_expand_i_take_mult_Suc f_Exec_append)
  apply (simp add: add_Suc_right[symmetric] replicate_add f_Exec_append del: add_Suc_right replicate.simps)
 apply (clarsimp simp: cut_less_mem_iff iT_add iT_iff simp del: f_Exec_Comp_Stream.simps, rename_tac t')
 apply (subgoal_tac "∃i'>i. t' = t * k + i'")
  prefer 2
  apply (rule_tac x="t' - t * k" in exI)
  apply simp
 apply (thin_tac "iAll ?I ?P")+
 apply (elim exE conjE)
 apply (subgoal_tac "i' < k")
  prefer 2
  apply simp
 apply (simp add: add_Suc_right[symmetric] i_expand_i_take_mult_Suc f_Exec_append f_Exec_Stream_nth min_eqL i_expand_i_take_mult del: add_Suc_right f_Exec_Comp_Stream.simps)
apply (elim iexE conjE, rename_tac t1)
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp2
apply (rule i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp2, assumption+)
done

text {* Here the property to be checked uses only unbounded intervals suitable for LTL. *}
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    (¬ State_Idle localState output_fun trans_fun (localState (s t1))). t1 \<U> t2 [0…] ⊕ t0. (
    (output_fun (s t2) = m) ∧
    (\<bigcirc> t3 t2 [0…]. 
      ((output_fun (s t4) = \<NoMsg>. t4 \<U> t5 ([0…] ⊕ t3). 
       (output_fun (s t5) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t5))))))) |] ==> 
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m"
apply (case_tac "
  \<diamond> t1 [0…, k - Suc 0] ⊕ t0. (
      State_Idle localState output_fun trans_fun (localState (s t1)) ∧
      output_fun (s t1) ≠ \<NoMsg>)")
 apply (clarsimp, rename_tac t1)
 thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_imp[OF Suc_lessD refl refl]
 apply (frule i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_imp[OF Suc_lessD refl refl], assumption+)
 apply (simp only: iNext_def iT_inext iT_iff iUntil_def)
 apply (elim iexE conjE, rename_tac t2 t3)
 apply (subgoal_tac "t2 ≤ t1")
  prefer 2
  apply (rule ccontr)
  apply (drule_tac t=t1 in ispec)
   apply (simp add: cut_less_mem_iff iT_add iT_iff)
  apply simp
 apply (thin_tac "iAll ?I ?P")
 apply (subgoal_tac "t1 ≤ t2")
  prefer 2
  apply (rule ccontr)
  apply (subgoal_tac "t3 < t1 --> output_fun (i_Exec_Comp_Stream trans_fun (input \<odot>i k) c t1) = \<NoMsg>")
   prefer 2
   apply (rule impI)
   apply (subgoal_tac "t * k ≤ t3")
    prefer 2
    apply (simp add: iT_add iT_iff)
   apply (subgoal_tac "t1 div k = t ∧ t3 div k = t", elim conjE)
    prefer 2
    apply (simp add: iT_add iT_iff le_less_imp_div)
   apply (simp (no_asm_simp) add: i_Exec_Stream_nth i_expand_i_take_Suc f_Exec_append)
   thm f_Exec_State_Idle_replicate_NoMsg_gr_output
   apply (rule_tac m="t3 mod k" in f_Exec_State_Idle_replicate_NoMsg_gr_output[of localState output_fun trans_fun])
    apply (simp add: i_Exec_Stream_nth i_expand_i_take_Suc f_Exec_append)
   apply (simp add: mod_div_equality')
  apply (case_tac "t1 < t3")
   apply (drule_tac t=t1 in ispec)
    apply (simp add: cut_less_mem_iff iT_add iT_iff)
   apply simp+
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2
apply (rule ssubst[OF i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2], simp+)
apply (simp only: iNext_def iT_inext iT_iff iUntil_def)
apply (elim iexE conjE, rename_tac t1 t2)
apply (subgoal_tac "t1 ≤ t * k + (k - Suc 0)")
 prefer 2
 apply (rule ccontr)
 apply (simp add: i_Exec_Stream_Acc_LocalState_nth i_expand_i_take_mult[symmetric] add_commute[of k])
 apply (thin_tac "iAll ?I ?P")
 apply (drule_tac t="t * k + (k - Suc 0)" in ispec)
  apply (simp add: cut_less_mem_iff iT_add iT_iff)
 apply (simp add: i_Exec_Stream_nth)
apply (rule_tac t=t1 in iexI)
 prefer 2
 apply (simp add: iT_add iT_iff)
apply simp
apply (rule_tac t=t2 in iexI)
apply simp+
done
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    \<box> t1 [0…, k - Suc 0] ⊕ t0. ¬ (
      State_Idle localState output_fun trans_fun (localState (s t1)) ∧
      output_fun (s t1) ≠ \<NoMsg>) |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  ((¬ State_Idle localState output_fun trans_fun (localState (s t1))). t1 \<U> t2 [0…] ⊕ t0. (
     (output_fun (s t2) = m) ∧
     (\<bigcirc> t3 t2 [0…]. 
       ((output_fun (s t4) = \<NoMsg>. t4 \<U> t5 ([0…] ⊕ t3). 
        (output_fun (s t5) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t5))))))))"
apply (rule iffI)
 thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2
 thm subst[OF i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2, where P="λx. x"]
 apply (frule subst[OF i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2, where P="λx. x"], assumption+)
 apply (simp only: iNext_def iT_inext iT_iff iUntil_def)
 apply (elim iexE conjE, rename_tac t1 t2)
 apply (rule_tac t=t1 in iexI)
  prefer 2
  apply (simp add: iT_add iT_iff)
 apply (intro conjI)
   apply simp
  apply (rule_tac t=t2 in iexI)
   prefer 2
   apply (simp add: iT_add iT_iff)
  apply simp
 apply (rule iallI, rename_tac t')
 apply (rule ccontr)
 apply (clarsimp simp: cut_less_mem_iff)
 apply (drule_tac i=t' in less_imp_add_positive)
 apply (elim exE conjE, rename_tac i)
 apply (drule_tac t=t1 in sym)
 apply (simp only: i_Exec_Stream_nth)
 apply (simp only: add_Suc[symmetric] i_take_add f_Exec_append)
 apply (simp only: i_take_i_drop)
 thm i_expand_nth_interval_eq_replicate_NoMsg
 apply (subgoal_tac "i + Suc t' ≤ t * k + k")
  prefer 2
  apply (simp add: iT_add iT_iff)
 apply (simp only: iT_add iT_iff)
 thm i_expand_nth_interval_eq_replicate_NoMsg[of k t "Suc t'", OF _ le_imp_less_Suc le_add2]
 apply (simp only: i_expand_nth_interval_eq_replicate_NoMsg[of k t, OF _ le_imp_less_Suc le_add2])
 thm f_Exec_State_Idle_replicate_NoMsg_gr0_output
 apply (drule_tac c="f_Exec_Comp trans_fun (input \<odot>i k \<Down> Suc t') c" and n=i in f_Exec_State_Idle_replicate_NoMsg_gr0_output)
 apply simp+
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp
apply (rule i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp, simp+)
done

thm 
  i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2
  i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  (\<diamond> t1 [0…, k - Suc 0] ⊕ t0. (
    output_fun (s t1) = m ∧ 
    (State_Idle localState output_fun trans_fun (localState (s t1)) ∨
    (\<bigcirc> t2 t1 [0…]. 
      ((output_fun (s t3) = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t2). 
       (output_fun (s t4) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t4)))))))))"
apply (subst conj_disj_distribL)
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2
apply (case_tac "
  \<diamond> t1 [0…,k - Suc 0] ⊕ t0.
    (State_Idle localState output_fun trans_fun (localState (s t1)) ∧ output_fun (s t1) ≠ \<NoMsg>)")
 apply (elim iexE conjE, rename_tac t1)
 apply (rule iffI)
  thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2[THEN iffD1, OF Suc_lessD]
  apply (frule i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2[THEN iffD1, OF Suc_lessD], assumption+)
  apply fastsimp
 apply (elim iexE conjI, rename_tac t2)
 apply (erule disjE)
  thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2
  apply (rule i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv2[THEN iffD2], simp+)
  apply (rule_tac t=t2 in iexI, simp+)
 thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp2
 apply (rule_tac ?t1.0=t2 in i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp2, simp+)
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2[OF _ _ _ refl refl]
apply (rule ssubst[OF i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv2[OF _ _ _ refl refl]], simp+)
apply fastsimp
done
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2': "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  ((\<diamond> t1 [0…, k - Suc 0] ⊕ t0. (
      output_fun (s t1) = m ∧ State_Idle localState output_fun trans_fun (localState (s t1)))) ∨
  (\<diamond> t1 [0…, k - Suc 0] ⊕ t0. (  
      ((output_fun (s t1) = m) ∧
        (\<bigcirc> t2 t1 [0…]. 
          ((output_fun (s t3) = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t2). 
           (output_fun (s t4) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t4))))))))))"
apply (subst i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2, assumption+)
apply blast
done

thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2
lemma i_Exec_Comp_Stream_Acc_Output__eq_iAll_iUntil_State_Idle_conv2: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) = (
  (m = \<NoMsg> --> 
    (output_fun (s t1) = \<NoMsg>. t1 \<U> t2 ([0…] ⊕ t0). (
     output_fun (s t2) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t2))))) ∧
  (m ≠ \<NoMsg> --> 
    (\<diamond> t1 [0…, k - Suc 0] ⊕ t0. (
      output_fun (s t1) = m ∧ 
      (State_Idle localState output_fun trans_fun (localState (s t1)) ∨
      (\<bigcirc> t2 t1 [0…]. 
        ((output_fun (s t3) = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t2). 
         (output_fun (s t4) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t4)))))))))))"
apply (case_tac "m = \<NoMsg>")
 apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv)
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2)
done

thm 
  i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv
  i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv': "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c |] ==> 
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  (((¬ State_Idle localState output_fun trans_fun (localState (s t2))). t2 \<U> t1 [0…] ⊕ t0. 
    (output_fun (s t1) = m ∧ State_Idle localState output_fun trans_fun (localState (s t1)))) ∨
  ((¬ State_Idle localState output_fun trans_fun (localState (s t2))). t2 \<U> t1 [0…] ⊕ t0. 
   (output_fun (s t1) = m ∧
   (\<bigcirc> t3 t1 [0…]. 
     ((output_fun (s t4) = \<NoMsg>. t4 \<U> t5 ([0…] ⊕ t3). 
      (output_fun (s t5) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t5)))))))))"
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv
apply (case_tac "
  \<diamond> t1 [0…,k - Suc 0] ⊕ t0.
    (State_Idle localState output_fun trans_fun (localState (s t1)) ∧ output_fun (s t1) ≠ \<NoMsg>)")
 apply (elim iexE conjE, rename_tac t1)
 apply (rule iffI)
  thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv[THEN iffD1, OF Suc_lessD]
  apply (frule i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv[THEN iffD1, OF Suc_lessD], simp+)
 apply (erule disjE)
  thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv
  apply (rule i_Exec_Comp_Stream_Acc_Output__eq_Msg_with_State_Idle_conv[THEN iffD2], simp+)
 thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp
 apply (rule_tac i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_imp, simp+)
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv[OF _ _ _ refl refl]
apply (subst i_Exec_Comp_Stream_Acc_Output__eq_Msg_before_State_Idle_conv[OF _ _ _ refl refl], simp+)
apply (rule iffI)
 apply simp
apply (unfold iUntil_def, erule disjE)
 apply (elim iexE conjE, rename_tac t1)
 apply (case_tac "t1 ≤ t * k + (k - Suc 0)")
  prefer 2
  apply (simp add: i_Exec_Stream_Acc_LocalState_nth i_Exec_Stream_nth i_expand_i_take_mult[symmetric])
  apply (thin_tac "iAll ?I ?P")
  apply (drule_tac t="t * k + (k - Suc 0)" in ispec)
   apply (simp add: cut_less_mem_iff iT_add iT_iff)
  apply (simp add: add_commute[of k])
 apply (fastsimp simp: iT_add iT_iff)+
done
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c |] ==>
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) =
  (((¬ State_Idle localState output_fun trans_fun (localState (s t2))). t2 \<U> t1 [0…] ⊕ t0. 
    (output_fun (s t1) = m ∧ 
      (State_Idle localState output_fun trans_fun (localState (s t1)) ∨
      (\<bigcirc> t3 t1 [0…]. 
          ((output_fun (s t4) = \<NoMsg>. t4 \<U> t5 ([0…] ⊕ t3). 
           (output_fun (s t5) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t5))))))))))"
apply (subst i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv', assumption+)
apply (subst iUntil_disj_distrib[symmetric])
apply (rule iUntil_cong2)
apply blast
done

thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv
lemma i_Exec_Comp_Stream_Acc_Output__eq_iUntil_State_Idle_conv: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c |] ==>
  (i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m) = (
  (m = \<NoMsg> --> 
    (output_fun (s t1) = \<NoMsg>. t1 \<U> t2 ([0…] ⊕ t0). (
     output_fun (s t2) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t2))))) ∧
  (m ≠ \<NoMsg> --> 
    (((¬ State_Idle localState output_fun trans_fun (localState (s t2))). t2 \<U> t1 [0…] ⊕ t0. 
      (output_fun (s t1) = m ∧ 
        (State_Idle localState output_fun trans_fun (localState (s t1)) ∨
        (\<bigcirc> t3 t1 [0…]. 
            ((output_fun (s t4) = \<NoMsg>. t4 \<U> t5 ([0…] ⊕ t3). 
             (output_fun (s t5) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t5))))))))))))"
apply (case_tac "m = \<NoMsg>")
 apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv)
apply (simp add: i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv)
done




text {* Sufficient conditions for output messages. *}
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2'
corollary i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iEx_imp1: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    (\<diamond> t1 [0…, k - Suc 0] ⊕ t0. (
       output_fun (s t1) = m ∧ State_Idle localState output_fun trans_fun (localState (s t1)))) |] ==> 
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m"
by (blast intro: i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2'[THEN iffD2])
corollary i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iEx_imp2: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    \<diamond> t1 [0…, k - Suc 0] ⊕ t0. (  
          ((output_fun (s t1) = m) ∧
            (\<bigcirc> t2 t1 [0…]. 
              ((output_fun (s t3) = \<NoMsg>. t3 \<U> t4 ([0…] ⊕ t2). 
               (output_fun (s t4) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t4)))))))) |] ==> 
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m"
by (blast intro: i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2'[THEN iffD2])

thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv'
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iUntil_imp1: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    (¬ State_Idle localState output_fun trans_fun (localState (s t2))). t2 \<U> t1 [0…] ⊕ t0. 
    (output_fun (s t1) = m ∧ State_Idle localState output_fun trans_fun (localState (s t1))) |] ==> 
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m"
by (blast intro: i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv'[THEN iffD2])
lemma i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iUntil_imp2: "
  [| Suc 0 < k;
    State_Idle localState output_fun trans_fun (
      i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun input c t);
    m ≠ \<NoMsg>; 
    t0 = t * k;
    s = i_Exec_Comp_Stream trans_fun (input \<odot>i k) c;
    (¬ State_Idle localState output_fun trans_fun (localState (s t2))). t2 \<U> t1 [0…] ⊕ t0. 
    (output_fun (s t1) = m ∧
    (\<bigcirc> t3 t1 [0…]. 
      ((output_fun (s t4) = \<NoMsg>. t4 \<U> t5 ([0…] ⊕ t3). 
       (output_fun (s t5) = \<NoMsg> ∧ State_Idle localState output_fun trans_fun (localState (s t5))))))) |] ==> 
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c t = m"
by (blast intro: i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv'[THEN iffD2])

text {* List of selected lemmas about output of accelerated components. *}
thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_iAll_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_iEx_iAll_cut_greater_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_iSince_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_iAll_iSince_conv

thm i_Exec_Comp_Stream_Acc_Output__eq_NoMsg_State_Idle_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv2'
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_conv'

thm i_Exec_Comp_Stream_Acc_Output__eq_iAll_iUntil_State_Idle_conv2
thm i_Exec_Comp_Stream_Acc_Output__eq_iUntil_State_Idle_conv

thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iEx_imp1
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iEx_imp2
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iUntil_imp1
thm i_Exec_Comp_Stream_Acc_Output__eq_Msg_State_Idle_iUntil_imp2


end