Theory FR_proof

(*<*)
(*
   Title: FR.thy  (FlexRay: Verification)
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2013
*) 
(*>*)
section ‹FlexRay: Verification›

theory  FR_proof
imports FR
begin


subsection ‹Properties of the function Send›

lemma Send_L1:
assumes "Send return send get activation"
       and "send t   []"
shows  "(activation t)  []"
using assms by (simp add: Send_def, auto)

lemma Send_L2:
assumes "Send return send get activation"
       and "(activation t)   []"
       and "return t  []"
shows  "(send t)  []"
using assms  by (simp add: Send_def) 


subsection ‹Properties of the component Scheduler›

lemma Scheduler_L1:
assumes h1:"Scheduler C activation"
        and h2:"(activation t)  []"
shows "(t mod (cycleLength C)) mem (schedule C)"
using assms
proof - 
   { assume  a1:"¬ t mod cycleLength C mem schedule C"
      from h1 have 
      "if t mod cycleLength C mem schedule C 
       then activation t = [t mod cycleLength C]
       else activation t = []"
         by (simp add: Scheduler_def Let_def)
     from a1 and this have "activation t = []" by simp
     from this and h2 have sg3:"False" by simp
   } from this have  sg4:"(t mod (cycleLength C)) mem (schedule C)" by blast
  from this show ?thesis by simp
qed

lemma Scheduler_L2:
assumes "Scheduler C activation"
       and "¬ (t mod cycleLength C) mem (schedule C)"
shows "activation t = []"
using assms by (simp add: Scheduler_def Let_def)  

lemma Scheduler_L3:
assumes "Scheduler C activation"
       and "(t mod cycleLength C) mem (schedule C)"
shows "activation t  []"
using assms by (simp add: Scheduler_def Let_def)

lemma Scheduler_L4:
assumes "Scheduler C activation"
       and "(t mod cycleLength C) mem (schedule C)"
shows "activation t = [t mod cycleLength C]"
using assms by (simp add: Scheduler_def Let_def)
 
lemma correct_DisjointSchedules1:
assumes h1:"DisjointSchedules n nC"
       and h2:"IdenticCycleLength n nC"
       and h3:"(t mod cycleLength (nC i)) mem schedule (nC i)" 
       and h4:"i < n"
       and h5:"j < n"
       and h6:"i  j"
shows "¬ (t mod cycleLength (nC j) mem schedule (nC j))"
proof -
  from h1 and h4 and h5 and h6 have sg1:"disjoint (schedule (nC i)) (schedule (nC j))"
    by (simp add: DisjointSchedules_def) 
  from h2 and h4 and h5 have sg2:"cycleLength (nC i) = cycleLength (nC j)"
    by (metis IdenticCycleLength_def)
  from sg1 and h3 have sg3:"¬ (t mod (cycleLength (nC i))) mem (schedule (nC j))" 
    by (simp add: mem_notdisjoint2)
  from sg2 and sg3 show ?thesis by simp
qed


subsection ‹Disjoint Frames›

lemma disjointFrame_L1:
assumes h1:"DisjointSchedules n nC"  
       and h2:"IdenticCycleLength n nC"
       and h3:" i < n. FlexRayController (nReturn i) rcv 
                      (nC i) (nStore i) (nSend i) (nGet i)"
       and h4:"nSend i t  []"
       and h5:"i < n"
       and h6:"j < n"
       and h7:"i  j"
shows "nSend j t = []"
proof - 
  from h3 and h5 have sg1:
   "FlexRayController (nReturn i) rcv (nC i) (nStore i) (nSend i) (nGet i)"
    by auto
  from h3 and h6 have sg2:
   "FlexRayController (nReturn j) rcv (nC j) (nStore j) (nSend j) (nGet j)"
    by auto
  from sg1 obtain activation1 where
     a1:"Scheduler (nC i) activation1" and 
     a2:"BusInterface activation1 (nReturn i) rcv (nStore i) (nSend i) (nGet i)"
     by (simp add: FlexRayController_def, auto)
  from sg2 obtain activation2 where
     a3:"Scheduler (nC j) activation2" and 
     a4:"BusInterface activation2 (nReturn j) rcv (nStore j) (nSend j) (nGet j)"
     by (simp add: FlexRayController_def, auto)
  from h1 and h5 and h6 and h7 have sg3:"disjoint (schedule (nC i)) (schedule (nC j))"
    by (simp add: DisjointSchedules_def) 
  from a2 have  sg4a:"Send (nReturn i) (nSend i) (nGet i) activation1" 
     by (simp add:  BusInterface_def)
  from sg4a and h4 have sg5:"activation1 t   []" by (simp add: Send_L1)
  from a1 and sg5 have sg6:"(t mod (cycleLength (nC i))) mem (schedule (nC i))" 
     by (simp add: Scheduler_L1)
  from h2 and h5 and h6 have sg7:"cycleLength (nC i) = cycleLength (nC j)"
    by (metis IdenticCycleLength_def)  
  from sg3 and sg6 have sg8:"¬ (t mod (cycleLength (nC i))) mem (schedule (nC j))" 
    by (simp add: mem_notdisjoint2)
  from sg8 and sg7 have sg9:"¬ (t mod (cycleLength (nC j))) mem (schedule (nC j))" 
    by simp
  from sg9 and a3 have sg10:"activation2 t = []" by (simp add: Scheduler_L2) 
  from a4 have sg11:"Send (nReturn j) (nSend j) (nGet j) activation2" 
     by (simp add:  BusInterface_def)
  from sg11 and sg10 show ?thesis by (simp add: Send_def)
qed

lemma disjointFrame_L2:
assumes "DisjointSchedules n nC"  
       and "IdenticCycleLength n nC"
       and " i < n. FlexRayController (nReturn i) rcv 
                      (nC i) (nStore i) (nSend i) (nGet i)"
shows "inf_disj n nSend"
using assms
  apply (simp add: inf_disj_def, clarify)
  by (rule disjointFrame_L1, auto)


lemma disjointFrame_L3:
assumes h1:"DisjointSchedules n nC"  
     and h2:"IdenticCycleLength n nC"
     and h3:" i < n. FlexRayController (nReturn i) rcv 
                      (nC i) (nStore i) (nSend i) (nGet i)"
    and h4:"t mod cycleLength (nC i) mem schedule (nC i)"
    and h5:"i < n"
    and h6:"j < n"
    and h7:"i  j"
shows "nSend j t = []"
proof - 
  from h2 and h5 and h6 have sg1:"cycleLength (nC i) = cycleLength (nC j)"
    by (metis IdenticCycleLength_def)  
  from h1 and h5 and h6 and h7 have sg2:"disjoint (schedule (nC i)) (schedule (nC j))"
    by (simp add: DisjointSchedules_def) 
  from sg2 and h4 have sg3:"¬ (t mod (cycleLength (nC i))) mem (schedule (nC j))" 
    by (simp add: mem_notdisjoint2)
  from sg1 and sg3 have sg4:"¬ (t mod (cycleLength (nC j))) mem (schedule (nC j))" 
    by simp
  from h3 and h6 have sg5:
   "FlexRayController (nReturn j) rcv (nC j) (nStore j) (nSend j) (nGet j)"
    by auto
  from sg5 obtain activation2 where
     a1:"Scheduler (nC j) activation2" and 
     a2:"BusInterface activation2 (nReturn j) rcv (nStore j) (nSend j) (nGet j)"
     by (simp add: FlexRayController_def, auto)
  from sg4 and a1 have sg6:"activation2 t = []" by (simp add: Scheduler_L2) 
  from a2 have sg7:"Send (nReturn j) (nSend j) (nGet j) activation2" 
     by (simp add:  BusInterface_def)
  from sg7 and sg6 show ?thesis by (simp add: Send_def)
qed


subsection ‹Properties of the sheaf of channels nSend›

lemma fr_Send1:
assumes frc:"FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
        and h1:"¬ (t mod cycleLength (nC i) mem schedule (nC i))"
 shows      "(nSend i) t = []"
proof - 
  from frc obtain activation where 
    a1:"Scheduler (nC i) activation"  and
    a2:"BusInterface activation (nReturn i) recv (nStore i) (nSend i) (nGet i)"
    by (simp add: FlexRayController_def, auto)
  from a1 and h1 have sg1:"activation t = []" by (simp add: Scheduler_L2)
  from a2 have sg2:"Send (nReturn i) (nSend i) (nGet i) activation"
    by (simp add: BusInterface_def)
  from sg2 and sg1 show ?thesis by (simp add: Send_def)
qed

lemma fr_Send2:
 assumes h1:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
     and h2:"DisjointSchedules n nC"
     and h3:"IdenticCycleLength n nC"
     and h4:"t mod cycleLength (nC k) mem schedule (nC k)"
     and h5:"k < n"
 shows "nSend k t = nReturn k t"
proof - 
 from h1 and h5 have sg1:
   "FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)"
    by auto
  from sg1 obtain activation where
     a1:"Scheduler (nC k) activation" and 
     a2:"BusInterface activation (nReturn k) recv (nStore k) (nSend k) (nGet k)"
     by (simp add: FlexRayController_def, auto)
  from a1 and h4 have sg3:"activation t  []" by (simp add: Scheduler_L3)
  from a2 have  sg4:"Send (nReturn k) (nSend k) (nGet k) activation" 
     by (simp add:  BusInterface_def)
  from sg4 and sg3 show ?thesis by (simp add: Send_def)
qed

lemma fr_Send3:
 assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
     and "DisjointSchedules n nC"
     and "IdenticCycleLength n nC"
     and "t mod cycleLength (nC k) mem schedule (nC k)"
     and "k < n"
     and "nReturn k t  []"
 shows "nSend k t  []"
using assms by (simp add: fr_Send2)

lemma fr_Send4:
 assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
     and "DisjointSchedules n nC"
     and "IdenticCycleLength n nC"
     and "t mod cycleLength (nC k) mem schedule (nC k)"
     and "k < n"
     and "nReturn k t  []"
 shows "k. k < n  nSend k t  []"
using assms
by (metis  fr_Send3)

lemma fr_Send5:
 assumes h1:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
     and h2:"DisjointSchedules n nC"
     and h3:"IdenticCycleLength n nC"
     and h4:"t mod cycleLength (nC k) mem schedule (nC k)"
     and h5:"k < n"
     and h6:"nReturn k t  []"
     and h7:"k<n. nSend k t = []"
 shows "False"
proof - 
  from h1 and h2 and h3 and h4 and h5 and h6 have sg1:"nSend k t  []"
    by (simp add: fr_Send2)
  from h7 and h5 have sg2:"nSend k t = []" by blast 
  from sg1 and sg2 show ?thesis by simp    
qed

lemma fr_Send6:
assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
       and "DisjointSchedules n nC"
       and "IdenticCycleLength n nC"
       and "t mod cycleLength (nC k) mem schedule (nC k)"
       and "k < n"
       and "nReturn k t  []"
shows "k<n. nSend k t  []"
using assms
by (metis fr_Send3)

lemma fr_Send7:
assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
       and "DisjointSchedules n nC"
       and "IdenticCycleLength n nC"
       and "t mod cycleLength (nC k) mem schedule (nC k)"
       and "k < n"
       and "j < n"
       and "nReturn k t = []"
shows "nSend j t = []"
using assms
by (metis (full_types) disjointFrame_L3 fr_Send2)

lemma fr_Send8:
assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
       and "DisjointSchedules n nC"
       and "IdenticCycleLength n nC"
       and "t mod cycleLength (nC k) mem schedule (nC k)"
       and "k < n"
       and "nReturn k t = []"
shows "¬ (k<n. nSend k t  [])"
using assms by (auto, simp add: fr_Send7)

lemma fr_nC_Send:
assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
       and "k < n"
       and "DisjointSchedules n nC"
       and "IdenticCycleLength n nC"
       and "t mod cycleLength (nC k) mem schedule (nC k)"
shows "j. j < n  j  k  (nSend j) t = []"
using assms by (clarify, simp add: disjointFrame_L3)

lemma length_nSend:
assumes h1:"BusInterface activation (nReturn i) recv (nStore i) (nSend i) (nGet i)"
       and h2:"t. length (nReturn i t)  Suc 0"
shows   "length (nSend i t)  Suc 0"
proof - 
  from h1 have sg1:"Send (nReturn i) (nSend i) (nGet i) activation"
    by (simp add: BusInterface_def)
  from sg1 have sg2:
   "if activation t = [] then nGet i t = []  nSend i t = []
    else nGet i t = activation t  nSend i t = nReturn i t"
    by (simp add: Send_def)
  show ?thesis
  proof (cases "activation t = []")
    assume a1:"activation t = []"
    from sg2 and a1 show ?thesis by simp
  next
    assume a2:"activation t  []"
    from h2 have sg3:"length (nReturn i t)  Suc 0" by auto
    from sg2 and a2 and sg3 show ?thesis by simp
  qed
qed

lemma msg_nSend:
assumes "BusInterface activation (nReturn i) recv (nStore i) (nSend i) (nGet i)"
       and "msg (Suc 0) (nReturn i)"
shows "msg (Suc 0) (nSend i)"
using assms by (simp add: msg_def, clarify, simp add: length_nSend)

lemma Broadcast_nSend_empty1:
assumes h1:"Broadcast n nSend recv"
       and h2:"k<n. nSend k t = []"
shows      "recv t = []"
using assms 
by (metis Broadcast_def)


subsection ‹Properties of the sheaf of channels  nGet›

lemma fr_nGet1a:
assumes h1:"FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)" 
       and h2:"t mod cycleLength (nC k) mem schedule (nC k)"
shows "nGet k t = [t mod cycleLength (nC k)]"
proof -
  from h1  obtain activation1 where
     a1:"Scheduler (nC k) activation1" and 
     a2:"BusInterface activation1 (nReturn k) recv (nStore k) (nSend k) (nGet k)"
     by (simp add: FlexRayController_def, auto)
   from a2 have sg1:"Send (nReturn k) (nSend k) (nGet k) activation1"
     by (simp add: BusInterface_def)
   from sg1 have sg2:
    "if activation1 t = [] then nGet k t = []  nSend k t = []
     else nGet k t = activation1 t  nSend k t = nReturn k t" 
     by (simp add: Send_def)
  from a1 and h2 have sg3:"activation1 t = [t mod cycleLength (nC k)]"
     by (simp add: Scheduler_L4)
  from sg2 and sg3 show ?thesis  by simp
qed

lemma fr_nGet1:
assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)" 
       and "t mod cycleLength (nC k) mem schedule (nC k)"
       and "k < n"
shows "nGet k t = [t mod cycleLength (nC k)]"
using assms
by (metis  fr_nGet1a)

lemma fr_nGet2a:
assumes h1:"FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)" 
       and h2:"¬ (t mod cycleLength (nC k) mem schedule (nC k))"
shows "nGet k t = []" 
proof -
   from h1 obtain activation1 where
     a1:"Scheduler (nC k) activation1" and 
     a2:"BusInterface activation1 (nReturn k) recv (nStore k) (nSend k) (nGet k)"
     by (simp add: FlexRayController_def, auto)
   from a2 have sg2:"Send (nReturn k) (nSend k) (nGet k) activation1"
     by (simp add: BusInterface_def)
   from sg2 have sg3:
    "if activation1 t = [] then nGet k t = []  nSend k t = []
     else nGet k t = activation1 t  nSend k t = nReturn k t" 
     by (simp add: Send_def)
  from a1 and h2 have sg4:"activation1 t = []"
     by (simp add: Scheduler_L2)
  from sg3 and sg4 show ?thesis  by simp
qed

lemma fr_nGet2:
assumes h1:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)" 
     and h2:"¬ (t mod cycleLength (nC k) mem schedule (nC k))"
     and h3:"k < n"
 shows "nGet k t = []"
proof -
  from h1 and h3 have sg1:
    "FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)"
    by auto
  from sg1 and h2 show ?thesis by (rule fr_nGet2a)
qed

lemma length_nGet1:
 assumes "FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)"
 shows    "length (nGet k t)  Suc 0"
proof (cases "t mod cycleLength (nC k) mem schedule (nC k)")
  assume "t mod cycleLength (nC k) mem schedule (nC k)"
  from assms and this have "nGet k t = [t mod cycleLength (nC k)]" 
    by (rule fr_nGet1a)
  then show ?thesis by auto
next
  assume "¬ (t mod cycleLength (nC k) mem schedule (nC k))"
  from assms and this have "nGet k t = []" by (rule fr_nGet2a)
  then show ?thesis by auto
qed

lemma msg_nGet1:
 assumes "FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)"
 shows    "msg (Suc 0) (nGet k)"
using assms 
by (simp add: msg_def, auto, rule length_nGet1)

lemma msg_nGet2:
assumes "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
       and "k < n"
shows "msg (Suc 0) (nGet k)"
using assms
by (metis msg_nGet1) 


subsection ‹Properties of the sheaf of channels nStore›

lemma fr_nStore_nReturn1:
 assumes h0:"Broadcast n nSend recv"
     and h1:"inf_disj n nSend"
     and h2:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)" 
     and h3:"DisjointSchedules n nC"
     and h4:"IdenticCycleLength n nC"
     and h5:"t mod cycleLength (nC k) mem schedule (nC k)"
     and h6:"k < n"
     and h7:"j < n"
     and h8:"j  k"
 shows  "nStore j t = nReturn k t"
proof - 
  from h2 and h6 have sg1:
    "FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)"
    by auto
  from h2 and h7 have sg2:
    "FlexRayController (nReturn j) recv (nC j) (nStore j) (nSend j) (nGet j)"
    by auto
   from sg1 obtain activation1 where
     a1:"Scheduler (nC k) activation1" and 
     a2:"BusInterface activation1 (nReturn k) recv (nStore k) (nSend k) (nGet k)"
     by (simp add: FlexRayController_def, auto)
  from sg2 obtain activation2 where
     a3:"Scheduler (nC j) activation2" and 
     a4:"BusInterface activation2 (nReturn j) recv (nStore j) (nSend j) (nGet j)"
     by (simp add: FlexRayController_def, auto)
  from a4 have sg3:"Receive recv (nStore j) activation2"
     by (simp add: BusInterface_def)
  from this have sg4:
   "if activation2 t = [] then nStore j t = recv t else nStore j t = []"
    by (simp add: Receive_def)
  from a1 and h5 have sg5:"activation1 t  []"
     by (simp add: Scheduler_L3)
 from h4 and h6 and h7 have sg6:"cycleLength (nC k) = cycleLength (nC j)"
    by (metis IdenticCycleLength_def)  
  from h3 and h6 and h7 and h8 have sg7:"disjoint (schedule (nC k)) (schedule (nC j))"
    by (simp add: DisjointSchedules_def) 
  from sg7 and h5 have sg8:"¬ (t mod (cycleLength (nC k))) mem (schedule (nC j))" 
    by (simp add: mem_notdisjoint2)
  from sg6 and sg8 have sg9:"¬ (t mod (cycleLength (nC j))) mem (schedule (nC j))" 
    by simp
  from sg9 and a3 have sg10:"activation2 t = []" by (simp add: Scheduler_L2) 
  from sg10 and sg4 have sg11:"nStore j t = recv t" by simp
  from h0 have sg15:
   "if k<n. nSend k t  [] 
    then recv t = nSend (SOME k. k < n  nSend k t  []) t
    else recv t = []"
    by (simp add: Broadcast_def)
  show ?thesis
  proof (cases "nReturn k t = []") 
    assume a5: "nReturn k t = []"
    from h2 and h3 and h4 and h5 and h6 and a5 have sg16:"¬ (k<n. nSend k t  [])"
      by (simp add: fr_Send8)
    from sg16 and sg15 have sg17:"recv t = []" by simp
    from sg11 and sg17 have sg18:"nStore j t = []" by simp
    from this and a5 show ?thesis by simp
  next
    assume a6:"nReturn k t  []"
    from h2 and h3 and h4 and h5 and h6 and a6 have sg19:"k<n. nSend k t  []"
      by (simp add: fr_Send6)
    from h2 and h3 and h4 and h5 and h6 and a6 have sg20:"nSend k t  []"
      by (simp add: fr_Send3)
    from h1 and sg20 and h6 have sg21:"(SOME k. k < n  nSend k t  []) = k"
      by (simp add: inf_disj_index)
    from sg15 and sg19 have sg22:"recv t = nSend (SOME k. k < n  nSend k t  []) t" 
      by simp
    from sg22 and sg21 have sg23:"recv t = nSend k t" by simp
    from h2 and h3 and h4 and h5 and h6 have sg24:"nSend k t =  nReturn k t"
      by (simp add: fr_Send2)
    from sg11 and sg23 and sg24 show ?thesis by simp
  qed
qed


lemma fr_nStore_nReturn2:
 assumes h1:"Cable n nSend recv"
     and h2:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)" 
     and h3:"DisjointSchedules n nC"
     and h4:"IdenticCycleLength n nC"
     and h5:"t mod cycleLength (nC k) mem schedule (nC k)"
     and h6:"k < n"
     and h7:"j < n"
     and h8:"j  k"
 shows  "nStore j t = nReturn k t"
proof - 
  from h1 have sg1:"inf_disj n nSend  Broadcast n nSend recv"
    by (simp add: Cable_def) 
  from  h3 and h4 and h2 have sg2:"inf_disj n nSend" 
    by (simp add: disjointFrame_L2)
  from sg1 and sg2 have sg3:"Broadcast n nSend recv" by simp
  from sg3 and sg2 and assms show ?thesis  by (simp add: fr_nStore_nReturn1)
qed

lemma fr_nStore_empty1:
 assumes h1:"Cable n nSend recv"
     and h2:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)" 
     and h3:"DisjointSchedules n nC"
     and h4:"IdenticCycleLength n nC"
     and h5:"(t mod cycleLength (nC k) mem schedule (nC k))"
     and h6:"k < n"
 shows  "nStore k t = []"
proof - 
  from h2 and h6 have sg1:
    "FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)"
    by auto
   from sg1 obtain activation1 where
     a1:"Scheduler (nC k) activation1" and 
     a2:"BusInterface activation1 (nReturn k) recv (nStore k) (nSend k) (nGet k)"
     by (simp add: FlexRayController_def, auto)
  from a2 have sg2:"Receive recv (nStore k) activation1"
     by (simp add: BusInterface_def)
  from this have sg3:
   "if activation1 t = [] then nStore k t = recv t else nStore k t = []"
    by (simp add: Receive_def)
  from a1 and h5 have sg4:"activation1 t  []"
     by (simp add: Scheduler_L3)
 from sg3 and sg4 show ?thesis by simp
qed

lemma fr_nStore_nReturn3:
 assumes "Cable n nSend recv"
     and "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)" 
     and "DisjointSchedules n nC"
     and "IdenticCycleLength n nC"
     and "t mod cycleLength (nC k) mem schedule (nC k)"
     and "k < n"
 shows  "j. j < n  j  k  nStore j t = nReturn k t"
using assms
by (clarify, simp add: fr_nStore_nReturn2)

lemma length_nStore:
 assumes h1:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
     and h2:"DisjointSchedules n nC"
     and h3:"IdenticCycleLength n nC"
     and h4:"inf_disj n nSend"
     and h5:"i < n"  
     and h6:" i<n. msg (Suc 0) (nReturn i)"
     and h7:"Broadcast n nSend recv"
 shows "length (nStore i t)  Suc 0"
proof -
  from h7 have sg1:
   "if k<n. nSend k t  [] 
    then recv t = nSend (SOME k. k < n  nSend k t  []) t 
    else recv t = []"
   by (simp add: Broadcast_def)
  show ?thesis 
  proof (cases "k<n. nSend k t  []")
    assume "k<n. nSend k t  []"
    from this obtain k where a2:"k<n" and a3:"nSend k t  []"  by auto
    from h1 and a2 have 
      "FlexRayController (nReturn k) recv (nC k) (nStore k) (nSend k) (nGet k)"
      by auto
    then obtain activation1 where
      a4:"Scheduler (nC k) activation1" and 
      a5:"BusInterface activation1 (nReturn k) recv (nStore k) (nSend k) (nGet k)" 
      by (simp add: FlexRayController_def, auto)
    from a5 have sg5:"Send (nReturn k) (nSend k) (nGet k) activation1" 
      by (simp add:  BusInterface_def)
    from a5 have sg6:"Receive recv (nStore k) activation1"
      by (simp add: BusInterface_def)
    from sg5 and a3 have sg7:"(activation1 t)  []" by (simp add: Send_L1)
    from sg6 have sg8:
     "if activation1 t = [] 
      then nStore k t = recv t else nStore k t = []"
      by (simp add: Receive_def)
    from sg8 and sg7 have sg9:"nStore k t = []" by simp
    from a4 and sg7 have sg10:"(t mod (cycleLength (nC k))) mem (schedule (nC k))"
      by (simp add: Scheduler_L1)
    show ?thesis 
    proof (cases "i = k")
      assume  "i = k"
      from sg9 and this show ?thesis by simp
    next
      assume "i  k"
      from h7 and h4 and h1 and h2 and h3 and sg10 and a2 and h5 and this have sg11:
       "nStore i t = nReturn k t"
        by (simp add: fr_nStore_nReturn1)
      from h6 and a2 have sg12:"msg (Suc 0) (nReturn k)" by auto
      from a2 and h6 have sg13:"length (nReturn k t)  Suc 0" 
        by (simp add: msg_def)  
      from sg11 and sg13  show ?thesis by simp
    qed
  next
    assume "¬ (k<n. nSend k t  [])"
    from h7 and this have sg14:"recv t = []" by (simp add: Broadcast_nSend_empty1)  
    from h1 and h5 have 
      "FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
      by auto
   then obtain activation2 where
      a11:"Scheduler (nC i) activation2" and 
      a12:"BusInterface activation2 (nReturn i) recv (nStore i) (nSend i) (nGet i)" 
      by (simp add: FlexRayController_def, auto)
    from a12 have "Receive recv (nStore i) activation2"
      by (simp add: BusInterface_def)
    then have sg17:
     "if activation2 t = [] 
      then nStore i t = recv t else nStore i t = []"
      by (simp add: Receive_def)
    show ?thesis
    proof (cases "activation2 t = []")
      assume aa3:"activation2 t = []"
      from sg17 and aa3 and sg14 have "nStore i t = []" by simp
      then show ?thesis by simp
    next
      assume aa4:"activation2 t  []"
      from sg17 and aa4 have "nStore i t = []" by simp
      then show ?thesis by simp
    qed
  qed
qed

lemma msg_nStore:
assumes " i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
       and "DisjointSchedules n nC"
       and "IdenticCycleLength n nC"
       and "inf_disj n nSend"
       and "i < n"  
       and " i<n. msg (Suc 0) (nReturn i)"
       and "Cable n nSend recv"
shows "msg (Suc 0) (nStore i)"
using assms
  apply (simp (no_asm) add: msg_def, simp add: Cable_def, clarify)
  by (simp add: length_nStore)


subsection ‹Refinement Properties› 

lemma fr_refinement_FrameTransmission:
assumes "Cable n nSend recv"
       and "i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)" 
       and "DisjointSchedules n nC"
       and "IdenticCycleLength n nC" 
shows "FrameTransmission n nStore nReturn nGet nC"
using assms 
  apply (simp add: FrameTransmission_def Let_def, auto)
  apply (simp add: fr_nGet1)
  by (simp add: fr_nStore_nReturn3)

lemma FlexRayArch_CorrectSheaf:
 assumes "FlexRayArch n nReturn nC nStore nGet"
 shows    "CorrectSheaf n"
using assms by (simp add: FlexRayArch_def)

lemma FlexRayArch_FrameTransmission:
 assumes h1:"FlexRayArch n nReturn nC nStore nGet"
     and h2:"i<n. msg (Suc 0) (nReturn i)"
     and h3:"DisjointSchedules n nC"
     and h4:"IdenticCycleLength n nC"
 shows      "FrameTransmission n nStore nReturn nGet nC"
proof - 
  from assms obtain nSend recv where
    a1:"Cable n nSend recv" and 
    a2:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
    by (simp add: FlexRayArch_def  FlexRayArchitecture_def, auto)
  from a1 and a2 and h3 and h4 show ?thesis 
    by (rule fr_refinement_FrameTransmission)
qed

lemma FlexRayArch_nGet:
 assumes h1:"FlexRayArch n nReturn nC nStore nGet"
     and h2:"i<n. msg (Suc 0) (nReturn i)"
     and h3:"DisjointSchedules n nC"
     and h4:"IdenticCycleLength n nC"
     and h5:"i < n"
 shows      "msg (Suc 0) (nGet i)"
proof - 
 from assms obtain nSend recv where
    a1:"Cable n nSend recv" and 
    a2:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
    by (simp add: FlexRayArch_def  FlexRayArchitecture_def, auto)
  from a2 and h5 show ?thesis by (rule msg_nGet2)
qed

lemma FlexRayArch_nStore:
 assumes h1:"FlexRayArch n nReturn nC nStore nGet"
     and h2:"i<n. msg (Suc 0) (nReturn i)"
     and h3:"DisjointSchedules n nC"
     and h4:"IdenticCycleLength n nC"
     and h5:"i < n"
 shows      "msg (Suc 0) (nStore i)"
proof - 
 from assms obtain nSend recv where
    a1:"Cable n nSend recv" and 
    a2:"i<n. FlexRayController (nReturn i) recv (nC i) (nStore i) (nSend i) (nGet i)"
    by (simp add: FlexRayArch_def  FlexRayArchitecture_def, auto)
  from h3 and h4 and a2 have sg1:"inf_disj n nSend" by (simp add: disjointFrame_L2)
  from a2 and h3 and h4 and sg1 and h5 and h2 and a1  show ?thesis 
    by (rule msg_nStore)
qed

theorem main_fr_refinement:
 assumes "FlexRayArch n nReturn nC nStore nGet"
 shows     "FlexRay n nReturn nC nStore nGet"
using assms
  by (simp add: FlexRay_def
                FlexRayArch_CorrectSheaf 
                FlexRayArch_FrameTransmission 
                FlexRayArch_nGet 
                FlexRayArch_nStore)
     
end