Theory Gateway_proof

(*<*)
(*
   Title: Gateway_proof.thy  (Gateway: Verification)
   Author: Maria Spichkova <maria.spichkova at rmit.edu.au>, 2013
*) 
(*>*)

(* header {*Gateway: Verification *} *)

theory Gateway_proof 
imports Gateway_proof_aux
begin

subsection ‹Properties of the Gateway›

lemma Gateway_L1:
  assumes h1:"Gateway req dt a stop lose d ack i vc"
      and h2:"msg (Suc 0) req"
      and h3:"msg (Suc 0) a"
      and h4:"msg (Suc 0) stop" 
      and h5:"ts lose"
      and h6:"ack t = [init_state]"
      and h7:"req (Suc t) = [init]"
      and h8:"lose (Suc t) = [False]"
      and h9:"lose (Suc (Suc t)) = [False]"
  shows "ack (Suc (Suc t)) = [connection_ok]" 
proof - 
  from h1 obtain i1 i2 x y
    where a1:"Sample req dt x stop lose ack i1 vc"
      and a2:"Delay y i1 d x i2"
      and a3:"Loss lose a i2 y i"
    by (simp only: Gateway_def, auto) 
  from a2 and a3 and h3 have sg1:"msg (Suc 0) x"   
    by (simp add: Loss_Delay_msg_a) 
  from a1 and h2 and h4 and sg1 obtain st buffer where a4:
    "tiTable_SampleT req x stop lose 
        (fin_inf_append [init_state] st) (fin_inf_append [[]] buffer) ack
         i1 vc st"
     by (simp add: Sample_def Sample_L_def, auto)
  from a4 and h5 and sg1 and h4 have sg2:"st t =  hd (ack t)"
    by (simp add: tiTable_ack_st_hd)  
  from h6 and sg1 and sg2 and h4 have sg3:
   "(fin_inf_append [init_state] st) (Suc t) = init_state"
    by (simp add: correct_fin_inf_append1)
  from a4 and h7 and sg3 have sg4:"st (Suc t) = call"
    by (simp add: tiTable_SampleT_def)
  from sg4 have sg5:"(fin_inf_append [init_state] st) (Suc (Suc t)) = call"
    by (simp add: correct_fin_inf_append1)
  from a4 and sg5 and assms show ?thesis 
    by (simp add: tiTable_SampleT_def)
qed

lemma Gateway_L2:
  assumes h1:"Gateway req dt a stop lose d ack i vc"
      and h2:"msg (Suc 0) req"
      and h3:"msg (Suc 0) a"
      and h4:"msg (Suc 0) stop" 
      and h5:"ts lose"
      and h6:"ack t = [connection_ok]"
      and h7:"req (Suc t) = [send]"
      and h8:"kSuc d. lose (t + k) = [False]" 
  shows "i (Suc (t + d))  = inf_last_ti dt t"
proof - 
  from h1 obtain i1 i2 x y
    where a1:"Sample req dt x stop lose ack i1 vc"
      and a2:"Delay y i1 d x i2"
      and a3:"Loss lose a i2 y i"
    by (simp only: Gateway_def, auto) 
  from a2 and a3 and h3 have sg1:"msg (Suc 0) x"   
    by (simp add: Loss_Delay_msg_a) 
  from a1 and h2 and h4 and sg1 obtain st buffer where a4:
    "Sample_L req dt x stop lose (fin_inf_append [init_state] st) 
         (fin_inf_append [[]] buffer) ack i1 vc st buffer"
    by (simp add: Sample_def, auto)
  from a4 have sg2:"buffer t = inf_last_ti dt t"
    by (simp add: Sample_L_buffer) 
  from assms and a1 and a4 and sg1 and sg2 have sg3:"i1 (Suc t) =  buffer t"
    by (simp add: Sample_L_i1_buffer)
  from a2 and sg1 have sg4:"i2 ((Suc t) + d)  =  i1 (Suc t)"
    by (simp add: Delay_def)
  from a3 and h8 have sg5:"i ((Suc t) + d)  =  i2 ((Suc t) + d)"
    by (simp add: Loss_def, auto)
  from sg5 and sg4 and sg3 and sg2 show ?thesis by simp
qed

lemma Gateway_L3:
  assumes h1:"Gateway req dt a stop lose d ack i vc"
      and h2:"msg (Suc 0) req"
      and h3:"msg (Suc 0) a"
      and h4:"msg (Suc 0) stop" 
      and h5:"ts lose"
      and h6:"ack t = [connection_ok]"
      and h7:"req (Suc t) = [send]"
      and h8:"kSuc d. lose (t + k) = [False]" 
  shows "ack (Suc t) = [sending_data]"
proof - 
  from h1 obtain i1 i2 x y
    where a1:"Sample req dt x stop lose ack i1 vc"
      and a2:"Delay y i1 d x i2"
      and a3:"Loss lose a i2 y i"
    by (simp only: Gateway_def, auto) 
  from a2 and a3 and h3 have sg1:"msg (Suc 0) x"   
    by (simp add: Loss_Delay_msg_a) 
  from a1 and h2 and h4 and sg1 obtain st buffer where a4:
    "tiTable_SampleT req x stop lose 
        (fin_inf_append [init_state] st) (fin_inf_append [[]] buffer) ack
         i1 vc st"
     by (simp add: Sample_def Sample_L_def, auto)
  from a4 and h5 and sg1 and h4 have sg2:"st t =  hd (ack t)"
    by (simp add: tiTable_ack_st_hd)  
  from sg2 and h6 have sg3:"(fin_inf_append [init_state] st) (Suc t) = connection_ok"
    by (simp add: correct_fin_inf_append1)
  from h8 have sg4:"lose (Suc t) = [False]" by auto
  from a4 and sg3 and sg4 and h7 have sg5:"st (Suc t) = sending_data"
    by (simp add: tiTable_SampleT_def) 
  from a4 and h2 and sg1 and h4 and h5 have sg6:"ack (Suc t) = [st (Suc t)]"
    by (simp add: tiTable_ack_st)
  from sg5 and sg6 show ?thesis by simp  
qed

lemma Gateway_L4:
  assumes h1:"Gateway req dt a stop lose d ack i vc"
      and h2:"msg (Suc 0) req"
      and h3:"msg (Suc 0) a"
      and h4:"msg (Suc 0) stop" 
      and h5:"ts lose"
      and h6:"ack (t + d) = [sending_data]"
      and h7:"a (Suc t) = [sc_ack]"
      and h8:"kSuc d. lose (t + k) = [False]" 
  shows "vc (Suc (t + d)) = [vc_com]"
proof - 
  from h1 obtain i1 i2 x y
    where a1:"Sample req dt x stop lose ack i1 vc"
       and a2:"Delay y i1 d x i2"
       and a3:"Loss lose a i2 y i"
    by (simp only: Gateway_def, auto) 
  from a2 and a3 and h3 have sg1:"msg (Suc 0) x"   
    by (simp add: Loss_Delay_msg_a) 
  from a1 and h2 and h4 and sg1 obtain st buffer where a4:
    "tiTable_SampleT req x stop lose 
        (fin_inf_append [init_state] st) (fin_inf_append [[]] buffer) ack
         i1 vc st"
     by (simp add: Sample_def Sample_L_def, auto)
  from a4 and h5 and sg1 and h4 have sg2:"st (t+d) =  hd (ack (t+d))"
    by (simp add: tiTable_ack_st_hd)  
  from sg2 and h6 have sg3:"(fin_inf_append [init_state] st) (Suc (t+d)) = sending_data"
    by (simp add: correct_fin_inf_append1)
  from a3 and h8 have sg4:"y (Suc t)  =  a (Suc t)"
    by (simp add: Loss_def, auto)
  from a2 and sg1 have sg5:"x ((Suc t) + d)  =  y (Suc t)"
    by (simp add: Delay_def) 
  from sg5 and sg4 and h7 have sg6:" x (Suc (t + d)) = [sc_ack]" by simp
  from h8 have sg7:"lose (Suc (t + d)) = [False]" by auto
  from sg6 and a4 and h2 and sg1 and h4 and h5 and sg7 and sg3 show ?thesis
    by (simp add: tiTable_SampleT_def) 
qed

lemma Gateway_L5:
  assumes h1:"Gateway req dt a stop lose d ack i vc"
      and h2:"msg (Suc 0) req"
      and h3:"msg (Suc 0) a"
      and h4:"msg (Suc 0) stop" 
      and h5:"ts lose"
      and h6:"ack (t + d) = [sending_data]"
      and h7:" j  Suc d. a (t+j) = []"
      and h8:"k (d + d). lose (t + k) = [False]" 
  shows "j  d  ack (t+d+j) = [sending_data]"
proof - 
  from h1 obtain i1 i2 x y
    where a1:"Sample req dt x stop lose ack i1 vc"
       and a2:"Delay y i1 d x i2"
       and a3:"Loss lose a i2 y i"
    by (simp only: Gateway_def, auto) 
  from a2 and a3 and h3 have sg1:"msg (Suc 0) x"   
    by (simp add: Loss_Delay_msg_a) 
  from a1 and h2 and h4 and sg1 obtain st buffer where a4:
    "tiTable_SampleT req x stop lose 
        (fin_inf_append [init_state] st) (fin_inf_append [[]] buffer) ack
         i1 vc st"
     by (simp add: Sample_def Sample_L_def, auto)
  from assms and a2 and a3 and sg1 and a4 show ?thesis
  proof (induct j)
    case 0 then show ?case by simp
  next
    case (Suc j)
    then show ?case
    proof (cases "Suc j  d")
      assume "¬ Suc j  d" then show ?thesis by simp
    next
      assume a0:"Suc j  d"
      then have "d + Suc j  d + d"   by arith
      then have sg3:"Suc (d + j)  d + d" by arith
      from a4 and h2 and sg1 and h4 and h5 have sg4: 
       "st (t+d+j) =  hd (ack (t+d+j))"
        by (simp add: tiTable_ack_st_hd)  
      from Suc and a0 and sg4 have sg5:
       "(fin_inf_append [init_state] st) (Suc (t+d+j)) = sending_data"
        by (simp add: correct_fin_inf_append1) 
      from h7 and a0  have sg6:"j d. a (t + Suc j) = []" by auto 
      from sg6 and a3 and a0 and h5 have sg7:"y (t + (Suc j)) = []" 
        by (rule Loss_L5Suc)
      from sg7 and a2 have sg8a:"x (t + d + (Suc j)) = []"
        by (simp add: Delay_def)
      then  have sg8:"x (Suc (t + d + j)) = []" by simp
      have sg9:"Suc (t + d + j) = Suc (t + (d + j))" by arith  
      from a4 have sg10:
        "fin_inf_append [init_state] st (Suc (t + d + j)) = sending_data  
         x (Suc (t + d + j)) = []  
         lose (Suc (t + d + j)) = [False] 
         ack (Suc (t + d + j)) = [sending_data]"
        by (simp add: tiTable_SampleT_def)  
      from h8 and sg3 have sg11:"lose (t + Suc (d + j)) = [False]" by blast
      have "Suc (t + d + j) = t + Suc (d + j)"  by arith
      from this and sg11 have "lose (Suc (t + d + j)) = [False]" 
        by  (simp (no_asm_simp), simp) 
     from sg10 and sg5 and sg8a and this show ?thesis by simp
    qed
  qed
qed

lemma Gateway_L6_induction:
 assumes h1:"msg (Suc 0) req"
     and h2:"msg (Suc 0) x" 
     and h3:"msg (Suc 0) stop"
     and h4:"ts lose"
     and h5:"j k. lose (t + j) = [False]" 
     and h6:"m  k. req (t + m)  [send]"
     and h7:"ack t = [connection_ok]"
     and h8:"Sample req dt x1 stop lose ack i1 vc" 
     and h9:"Delay x2 i1 d x1 i2"
     and h10:"Loss lose x i2 x2 i"
     and h11:"m  k"
 shows "ack (t + m) = [connection_ok]"
using assms
proof (induct m)
  case 0 then show ?case  by simp
next
  case (Suc m)
  then have sg1:"msg (Suc 0) x1" by (simp add:  Loss_Delay_msg_a)
  from Suc and this obtain st buffer where
    a1:"tiTable_SampleT req x1 stop lose (fin_inf_append [init_state] st) 
         (fin_inf_append [[]] buffer) ack i1 vc st"  and 
    a2:" t. buffer t = (if dt t = [] then fin_inf_append [[]] buffer t else dt t)"
    by (simp add: Sample_def Sample_L_def, auto)
  from a1 and sg1 and h3 and h4 have sg2:"st (t + m) =  hd (ack (t + m))"  
    by (simp add: tiTable_ack_st_hd)
  from Suc have sg3:"ack (t + m) = [connection_ok]" by simp
  from a1 and sg2 and sg3 have sg4:
  "(fin_inf_append [init_state] st) (Suc (t + m)) = connection_ok"
    by (simp add: fin_inf_append_def)
  from Suc have sg5:"Suc m  k" by simp
  from sg5 and h5 have sg6:"lose (Suc (t + m)) = [False]" by auto
  from h6 and sg5 have sg7:"req (Suc (t + m))  [send]" by auto
  from a1 and sg3 and sg4 and sg5 and sg6 and sg7 show ?case
    by (simp add: tiTable_SampleT_def)
qed

lemma Gateway_L6:
 assumes "Gateway req dt a stop lose d ack i vc"
     and "mk. req (t + m)  [send]"
     and "jk. lose (t + j) = [False]"
     and "ack t = [connection_ok]"
     and "msg (Suc 0) req"
     and "msg (Suc 0) stop"
     and "msg (Suc 0) a"
     and "ts lose"
 shows "mk. ack (t + m) = [connection_ok]"
using assms 
by (simp add: Gateway_def, clarify, simp add: Gateway_L6_induction) 

lemma Gateway_L6a:
 assumes "Gateway req dt a stop lose d ack i vc"
     and "mk. req (t + 2 + m)  [send]"
     and "jk. lose (t + 2 + j) = [False]"
     and "ack (t + 2) = [connection_ok]"
     and "msg (Suc 0) req"
     and "msg (Suc 0) stop"
     and "msg (Suc 0) a"
     and "ts lose"
 shows "mk. ack (t + 2 + m) = [connection_ok]"
using assms by (rule Gateway_L6)

lemma aux_k3req:
assumes h1:"m<k + 3. req (t + m)  [send]"
       and h2:"m  k"
shows "req (Suc (Suc (t + m)))  [send]"
proof - 
  from h2 have "m + 2 < k + 3" by arith
  from h1 and this have "req (t + (m + 2))  [send]" by blast
  then show ?thesis by simp
qed

lemma aux3lose:
assumes h1:"jk + d + 3. lose (t + j) = [False]"
       and h2:"j  k"
shows "lose (Suc (Suc (t + j))) = [False]"
proof - 
  from h2 have "j + 2 k + d + 3" by arith
  from h1 and this have "lose (t + (j + 2)) = [False]" by blast
  then show ?thesis by simp
qed


lemma Gateway_L7:
assumes h1:"Gateway req dt a stop lose d ack i vc"
     and h2:"ts lose"
     and h3:"msg (Suc 0) a"
     and h4:"msg (Suc 0) stop" 
     and h5:"msg (Suc 0) req"
     and h6:"req (Suc t) = [init]"
     and h7:"m < (k + 3). req (t + m)  [send]"
     and h8:"req (t + 3 + k) = [send]"
     and h9:"ack t = [init_state]"
     and h10:"jk + d + 3. lose (t + j) = [False]"
     and h11:" t1  t. req t1 = []"
shows " t2 < (t + 3 + k + d). i t2 = []"
proof -
  have "Suc 0  k + d + 3" by arith
  from h10 and this have "lose (t + Suc 0) = [False]" by blast
  then have sg1:"lose (Suc t) = [False]" by simp
  have "Suc (Suc 0) k + d + 3" by arith
  from h10 and this have "lose (t + Suc (Suc 0)) = [False]" by blast
  then have sg2:"lose (Suc (Suc t)) = [False]" by simp 
  from h1 and h2 and h3 and h4 and h5 and h6 and h9 and sg1 and sg2 
     have sg3:"ack (t + 2) = [connection_ok]"
    by (simp add: Gateway_L1)
  from h7 and this have sg4:"m k. req ((t + 2) + m)  [send]" 
    by (auto, simp add: aux_k3req)  
  from h10 have sg5:"j k. lose ((t + 2) + j) = [False]" 
    by (auto, simp add: aux3lose) 
  from h1 and sg4 and sg5 and sg3 and h5 and h4 and h3 and h2 have sg6:
   "m   k. ack ((t + 2) + m) = [connection_ok]"
    by (rule Gateway_L6a)
  from sg6 have sg7:"ack (t + 2 + k) = [connection_ok]"  by auto
  from h1 obtain i1 i2 x y where
    a1:"Sample req dt x stop lose ack i1 vc" and
    a2:"Delay y i1 d x i2" and 
    a3:"Loss lose a i2 y i"
    by (simp add: Gateway_def, auto) 
  from h3 and a2 and a3  have sg8:"msg (Suc 0) x"
    by (simp add: Loss_Delay_msg_a)  
  from a1 and sg8 and h4 and h5 obtain st buffer where
    a4:"tiTable_SampleT req x stop lose (fin_inf_append [init_state] st) 
         (fin_inf_append [[]] buffer) ack i1 vc st"  and 
    a5:" t. buffer t = (if dt t = [] then fin_inf_append [[]] buffer t else dt t)"
    by (simp add: Sample_def Sample_L_def, auto)
  from a4 and h2 and sg8 and h4 and h11 and h6 and h7 and sg6 and h10 
    have sg9:" t1 < (t + 3 + k). i1 t1 = []"
    by (simp add: tiTable_i1_4)
  from sg9 and a2 have sg10:" t2 < (t + 3 + k + d). i2 t2 = []"
    by (rule Delay_L2) 
  from sg10 and a3 and h2 show ?thesis by (rule Loss_L2)
qed 

lemma Gateway_L8a:
  assumes h1:"Gateway req dt a stop lose d ack i vc" 
      and h2:"msg (Suc 0) req"
      and h3:"msg (Suc 0) stop"
      and h4:"msg (Suc 0) a"
      and h5:"ts lose"
      and h6:"j2 * d. lose (t + j) = [False]" 
      and h7:"ack t = [sending_data]"
      and h8:"t3  t + d. a t3 = []"
      and h9:"x  d + d"
  shows "ack (t + x) = [sending_data]"
proof -
  from h1 obtain i1 i2 x y where
    a1:"Sample req dt x stop lose ack i1 vc" and
    a2:"Delay y i1 d x i2" and 
    a3:"Loss lose a i2 y i"
    by (simp add: Gateway_def, auto) 
  from h8 and a3 and h5 have sg1:"t3  t + d. y t3 = []" by (rule Loss_L6)
  from sg1 and a2 have sg2:"t4  t + d + d. x t4 = []"   by (rule Delay_L4) 
  from h4 and a2 and a3 have sg3:"msg (Suc 0) x" by (simp add:  Loss_Delay_msg_a)
  from h3 and h5 and h2 and sg3 and h6 and h7 and a1 and h9 and sg2 show ?thesis
    by (simp add: Sample_sending_data)
qed


lemma Gateway_L8:
assumes "Gateway req dt a stop lose d ack i vc" 
       and "msg (Suc 0) req"
       and "msg (Suc 0) stop"
       and "msg (Suc 0) a"
       and "ts lose"
       and "j2 * d. lose (t + j) = [False]" 
       and "ack t = [sending_data]"
       and "t3  t + d. a t3 = []"
shows "x  d + d. ack (t + x) = [sending_data]"
using assms 
by (simp add: Gateway_L8a)


subsection ‹Proof of the Refinement Relation for the Gateway Requirements›

lemma Gateway_L0:
 assumes "Gateway req dt a stop lose d ack i vc"
 shows     "GatewayReq req dt a stop lose d ack i vc"
using assms
by (simp add: GatewayReq_def Gateway_L1 Gateway_L2 Gateway_L3 Gateway_L4) 
 

subsection ‹Lemmas about Gateway Requirements›

lemma GatewayReq_L1:
  assumes h1:"msg (Suc 0) req"
      and h2:"msg (Suc 0) stop"
      and h3:"msg (Suc 0) a"
      and h4:"ts lose"
      and h6:"req (t + 3 + k) = [send]" 
      and h7:"j2 * d + (4 + k). lose (t + j) = [False]"
      and h9:"m k. ack (t + 2 + m) = [connection_ok]"
      and h10:"GatewayReq req dt a stop lose d ack i vc"
 shows "ack (t + 3 + k) = [sending_data]"
proof - 
  from h9 have sg1:"ack (Suc (Suc (t + k))) = [connection_ok]" by auto 
  from h7 have sg2: 
   "kaSuc d. lose (Suc (Suc (t + k + ka))) = [False]"
    by (simp add: aux_lemma_lose_1) 
  from h1 and h2 and h3 and h4 and h6 and h10 and sg1 and sg2 have sg3:
   "ack (t + 2 + k) = [connection_ok]  
    req (Suc (t + 2 + k)) = [send]  (kSuc d. lose (t + k) = [False]) 
    ack (Suc (t + 2 + k)) = [sending_data]"
    by (simp add: GatewayReq_def)  
  have "t + 3 + k = Suc (Suc (Suc (t + k)))" by arith
  from sg3 and sg1 and h6 and h7 and this show ?thesis 
    by (simp add: eval_nat_numeral)  
qed

lemma GatewayReq_L2:
 assumes  h1:"msg (Suc 0) req"
      and h2:"msg (Suc 0) stop"
      and h3:"msg (Suc 0) a"
      and h4:"ts lose"
      and h5:"GatewayReq req dt a stop lose d ack i vc"
      and h6:"req (t + 3 + k) = [send]"
      and h7:"inf_last_ti dt t  []"
      and h8:"j2 * d + (4 + k). lose (t + j) = [False]"
      and h9:"mk. ack (t + 2 + m) = [connection_ok]"
  shows "i (t + 3 + k + d)  []"
proof -
  from h8 have sg1:"( (x::nat). x  (d+1)  lose (t+x) = [False])"
    by (simp add: aux_lemma_lose_2) 
  from h8 have sg2:"kaSuc d. lose (Suc (Suc (t + k + ka))) = [False]"
    by (simp add: aux_lemma_lose_1)
  from h9 have sg3:"ack (t + 2 + k) = [connection_ok]" by simp
  from h1 and h2 and h3 and h4 and h5 and h6 and sg2 and sg3 have sg4:
   "ack (t + 2 + k) = [connection_ok]  
    req (Suc (t + 2 + k)) = [send]  (kSuc d. lose (t + k) = [False]) 
    i (Suc (t + 2 + k + d)) = inf_last_ti dt (t + 2 + k)"
    by (simp add: GatewayReq_def, auto)  
  from h7 have sg5:"inf_last_ti dt (t + 2 + k)  []"
    by (simp add: inf_last_ti_nonempty_k)
  have sg6:"t + 3 + k = Suc (Suc (Suc (t + k)))" by arith
  have "t + 2 + k = Suc (Suc (t + k))" by arith
  from sg1 and sg2 and sg3 and sg4 and sg5 and sg6 and this and h6 show ?thesis
    by (simp add: eval_nat_numeral)
qed


subsection ‹Properties of the Gateway System›
   
lemma GatewaySystem_L1aux:
assumes "msg (Suc 0) req"
       and "msg (Suc 0) stop"
       and "msg (Suc 0) a"
       and "ts lose"
       and "msg (Suc 0) req  msg (Suc 0) a  msg (Suc 0) stop  ts lose  
        (t. (ack t = [init_state] 
          req (Suc t) = [init]  lose (Suc t) = [False]  
          lose (Suc (Suc t)) = [False] 
          ack (Suc (Suc t)) = [connection_ok]) 
         (ack t = [connection_ok]  req (Suc t) = [send]  
         (kSuc d. lose (t + k) = [False]) 
          i (Suc (t + d)) = inf_last_ti dt t  ack (Suc t) = [sending_data]) 
         (ack (t + d) = [sending_data]  a (Suc t) = [sc_ack]  
          (kSuc d. lose (t + k) = [False]) 
          vc (Suc (t + d)) = [vc_com]))"
shows  "ack (t + 3 + k + d + d) = [sending_data] 
          a (Suc (t + 3 + k + d)) = [sc_ack]  
         (kaSuc d. lose (t + 3 + k + d + ka) = [False]) 
         vc (Suc (t + 3 + k + d + d)) = [vc_com]"
using assms  by blast

lemma GatewaySystem_L3aux:
assumes "msg (Suc 0) req"
       and "msg (Suc 0) stop"
       and "msg (Suc 0) a"
       and "ts lose"
       and "msg (Suc 0) req  msg (Suc 0) a  msg (Suc 0) stop  ts lose  
        (t. (ack t = [init_state] 
          req (Suc t) = [init]  lose (Suc t) = [False]  
          lose (Suc (Suc t)) = [False] 
          ack (Suc (Suc t)) = [connection_ok]) 
         (ack t = [connection_ok]  req (Suc t) = [send]  
         (kSuc d. lose (t + k) = [False]) 
          i (Suc (t + d)) = inf_last_ti dt t  ack (Suc t) = [sending_data]) 
         (ack (t + d) = [sending_data]  a (Suc t) = [sc_ack]  
          (kSuc d. lose (t + k) = [False]) 
          vc (Suc (t + d)) = [vc_com]))"
shows "ack (t + 2 + k) = [connection_ok] 
         req (Suc (t + 2 + k)) = [send]  
         (jSuc d. lose (t + 2 + k + j) = [False]) 
         i (Suc (t + 2 + k + d)) = inf_last_ti dt (t + 2 + k)"
using assms  by blast

lemma GatewaySystem_L1:
 assumes  h2:"ServiceCenter i a" 
     and h3:"GatewayReq req dt a stop lose d ack i vc" 
     and h4:"msg (Suc 0) req"
     and h5:"msg (Suc 0) stop"
     and h6:"msg (Suc 0) a"
     and h7:"ts lose"
     and h9:"j2 * d + (4 + k). lose (t + j) = [False]" 
     and h11:"i (t + 3 + k + d)  []"
     and h14:"x  d + d. ack (t + 3 + k + x) = [sending_data]"
 shows "vc (2 * d + (t + (4 + k))) = [vc_com]"
proof - 
  from h2 have "t. a (Suc t) = (if i t = [] then [] else [sc_ack])"
    by (simp add:ServiceCenter_def) 
  then have sg1:
    "a (Suc (t + 3 + k + d)) = (if i (t + 3 + k + d) = [] then [] else [sc_ack])" 
     by blast
  from sg1 and h11 have sg2:"a (Suc (t + 3 + k + d)) = [sc_ack]" by auto
  from h14 have sg3:"ack (t + 3 + k + 2*d) = [sending_data]" by simp
  from h4 and h5 and h6 and h7 and h3 have sg4:
    "ack (t + 3 + k + d + d) = [sending_data]  a (Suc (t + 3 + k + d)) = [sc_ack]  
     (kaSuc d. lose (t + 3 + k + d + ka) = [False]) 
     vc (Suc (t + 3 + k + d + d)) = [vc_com]" 
    apply (simp only: GatewayReq_def)
    by (rule GatewaySystem_L1aux, auto) 
  from h9 have sg5:"kaSuc d. lose (d + (t + (3 + k)) + ka) = [False]"
    by (simp add: aux_lemma_lose_3)
  have sg5a:"d + (t + (3 + k)) = t + 3 + k + d" by arith
  from sg5 and sg5a have sg5b:"kaSuc d. lose (t + 3 + k + d + ka) = [False]" 
    by auto 
  have sg6:"(t + 3 + k + 2 * d)  = (2 * d + (t + (3 + k)))" by arith
  have sg7:"Suc (Suc (Suc (t + k + (d + d)))) = Suc (Suc (Suc (t + k + d + d)))" 
    by arith
  have "Suc (Suc (Suc (Suc (t + k + d + d)))) = 
            Suc (Suc (Suc (Suc (d + d + (t + k)))))" by arith
  from sg4 and sg3 and sg2 and sg5b and sg6 and sg7 and this show ?thesis
    by (simp add: eval_nat_numeral)
qed

lemma aux4lose1:
assumes h1:"j2 * d + (4 + k). lose (t + j) = [False]"
       and h2:"j  k"
shows "lose (t + (2::nat) + j) = [False]"
proof - 
  from h2 have "(2::nat) + j  (2::nat) * d + (4 + k)" by arith
  from h1 and this have "lose (t + (2 + j)) = [False]" by blast
  then show ?thesis by simp
qed

lemma aux4lose2:
assumes "j2 * d + (4 + k). lose (t + j) = [False]"
       and "3 + k + d  2 * d + (4 + k)"
shows "lose (t + (3::nat) + k + d) = [False]"
proof -
  from assms have "lose (t + ((3::nat) + k + d)) = [False]" by blast
  then show ?thesis by (simp add: arith_sum1)
qed

lemma aux4req:
assumes h1:" (m::nat)  k + 2. req (t + m)  [send]"
      and h2:"m  k"
      and h3:"req (t + 2 + m) = [send]" shows "False"
proof - 
  from h2 have "(2::nat) + m  k + (2::nat)" by arith
  from h1 and this have "req (t + (2 + m))  [send]" by blast
  from this and h3 show ?thesis by simp
qed
 
lemma GatewaySystem_L2:
 assumes h1:"Gateway req dt a stop lose d ack i vc" 
     and h2:"ServiceCenter i a" 
     and h3:"GatewayReq req dt a stop lose d ack i vc" 
     and h4:"msg (Suc 0) req"
     and h5:"msg (Suc 0) stop"
     and h6:"msg (Suc 0) a"
     and h7:"ts lose"
     and h8:"ack t = [init_state]"
     and h9:"req (Suc t) = [init]" 
     and h10:"t1t. req t1 = []"
     and h11:"m  k + 2. req (t + m)  [send]"
     and h12:"req (t + 3 + k) = [send]" 
     and h13:"inf_last_ti dt t  []"
     and h14:"j2 * d + (4 + k). lose (t + j) = [False]"
 shows "vc (2 * d + (t + (4 + k))) = [vc_com]"
proof -
  have "Suc 0  2 * d + (4 + k)" by arith
  from h14 and this have "lose (t + Suc 0) = [False]" by blast
  then have sg1:"lose (Suc t) = [False]" by simp
  have "Suc (Suc 0)  2 * d + (4 + k)" by arith
  from h14 and this have "lose (t + Suc (Suc 0)) = [False]" by blast
  then have sg2:"lose (Suc (Suc t)) = [False]" by simp 
  from h3 and h4 and h5 and h6 and h7 and h8 and h9 and sg1 and sg2 have sg3:
   "ack (t + 2) = [connection_ok]" 
    by (simp add: GatewayReq_def)
  from h14 have sg4:" jk. lose (t + 2 + j) = [False]" 
    by (clarify, rule aux4lose1, simp) 
  from h11 have sg5:"m  k. req (t + 2 + m)  [send]" 
    by (clarify, rule aux4req, auto) 
  (* stable connection *)
  from h1 and sg5 and sg4 and sg3 and h4 and h5 and h6 and h7 have sg6:
   "m  k. ack (t + 2 + m) = [connection_ok]"
    by (rule Gateway_L6)
  (* sending data*)
  from h3 and h4 and h5 and h6 and h7 and h12 and h14 and sg6 have sg10:
   "ack (t + 3 + k) = [sending_data]"
    by (simp add: GatewayReq_L1)
  from h3 and h4 and h5 and h6 and h7 and h12 and h13 and h14 and sg6 have sg11:
   "i (t + 3 + k + d)  []"
    by (simp add: GatewayReq_L2)
  (* waiting for sc-ack *)
  from h11 have sg12:"m < k + 3. req (t + m)  [send]" by auto
  from h14 have sg13:"jk + d + 3. lose (t + j) = [False]" by auto
  from h1 and h7 and h6 and h5 and h4 and h9 and sg12 
          and h12 and h8 and sg13 and h10
    have sg14:" t2 < (t + 3 + k + d). i t2 = []"
    by (simp add: Gateway_L7) 
  from sg14 and h2 have sg15:" t3  (t + 3 + k + d). a t3 = []"
    by (simp add: ServiceCenter_L2)
  from h14 have sg18:"j2 * d. lose ((t + 3 + k) + j) = [False]" 
    by (simp add: streamValue43)
  from h14  have sg16a:"j2 * d. lose (t + j + (4 + k)) = [False]" 
    by (simp add: streamValue2)
  have sg16b:"Suc (3 + k) = (4 + k)" by arith
  from sg16a and sg16b have sg16:"j2 * d. lose (t + j + Suc (3 + k)) = [False]" 
    by (simp (no_asm_simp))  
  from h1 and h4 and h5 and h6 and h7 and sg18 and sg10 and sg15 have sg19:
    "x  d + d. ack (t + 3 + k + x) = [sending_data]"
     by (simp add: Gateway_L8)
  from sg19 have sg19a:"ack (t + 3 + k + d + d) = [sending_data]" by auto
  from sg16 have sg20a:"j d. lose (t + 3 + k + d + (Suc j)) = [False]" 
    by (rule streamValue10) 
  have sg20b:"3 + k + d  2 * d + (4 + k)" by arith
  from h14 and sg20b have sg20c:"lose (t + 3 + k + d) = [False]"
    by (rule aux4lose2)
  from sg20a and sg20c have sg20:"jSuc d. lose (t + 3 + k + d + j) = [False]" 
    by (rule streamValue8) 
  from h4 and h5 and h6 and h7 and h3 have sg21:
     "ack (t + 3 + k + d + d) = [sending_data]  
      a (Suc (t + 3 + k + d)) = [sc_ack]  
      (jSuc d. lose (t + 3 + k + d + j) = [False]) 
      vc (Suc (t + 3 + k + d + d)) = [vc_com]"
     apply (simp only: GatewayReq_def) 
     by (rule GatewaySystem_L1aux, auto)  
   from h2 and sg11 have sg22:"a (Suc (t + 3 + k + d)) = [sc_ack]"
     by (simp only: ServiceCenter_def, auto)
   from sg21 and sg19a and sg22 and sg20 have sg23:
     "vc (Suc (t + 3 + k + d + d)) = [vc_com]" by simp
   have "2 * d + (t + (4 + k)) = (Suc (t + 3 + k + d + d))" by arith
   from sg23 and this show ?thesis 
     by (simp (no_asm_simp), simp)
qed

lemma GatewaySystem_L3:
 assumes h1:"Gateway req dt a stop lose d ack i vc"
     and h2:"ServiceCenter i a"
     and h3:"GatewayReq req dt a stop lose d ack i vc"
     and h4:"msg (Suc 0) req"
     and h5:"msg (Suc 0) stop"
     and h6:"msg (Suc 0) a"
     and h7:"ts lose"
     and h8: "dt (Suc t)  []  dt (Suc (Suc t))  []"
     and h9: "ack t = [init_state]"
     and h10:"req (Suc t) = [init]"
     and h11:"t1t. req t1 = []"
     and h12:"m  k + 2. req (t + m)  [send]" 
     and h13:"req (t + 3 + k) = [send]"
     and h14:"j2 * d + (4 + k). lose (t + j) = [False]"
 shows "vc (2 * d + (t + (4 + k))) = [vc_com]"
proof -
  have "Suc 0  2 * d + (4 + k)" by arith
  from h14 and this have "lose (t + Suc 0) = [False]" by blast
  then have sg1:"lose (Suc t) = [False]" by simp
  have "Suc (Suc 0)  2 * d + (4 + k)" by arith
  from h14 and this have "lose (t + Suc (Suc 0)) = [False]" by blast
  then have sg2:"lose (Suc (Suc t)) = [False]" by simp 
  from h3 and h4 and h5 and h6 and h7 and h10 and h9 and sg1 and sg2 have sg3:
   "ack (t + 2) = [connection_ok]" 
    by (simp add: GatewayReq_def)
  from h14 have sg4:" jk. lose (t + 2 + j) = [False]" 
    by (clarify, rule aux4lose1, simp) 
  from h12 have sg5:"m  k. req (t + 2 + m)  [send]" 
    by (clarify, rule aux4req, auto)  
  (* stable connection *)
  from h1 and sg5 and sg4 and sg3 and h4 and h5 and h6 and h7 have sg6:
   "m  k. ack (t + 2 + m) = [connection_ok]"
    by (rule Gateway_L6)
  from sg6 have sg6a:"ack (t + 2 + k) = [connection_ok]" by simp
  (* sending data*)
  from h3 and h4 and h5 and h6 and h7 and h13 and h14 and sg6 have sg10:
   "ack (t + 3 + k) = [sending_data]"
    by (simp add: GatewayReq_L1)
  from h3 and h4 and h5 and h6 and h7 have sg11a:
   "ack (t + 2 + k) = [connection_ok] 
    req (Suc (t + 2 + k)) = [send]  
    (jSuc d. lose ((t + 2 + k) + j) = [False]) 
    i (Suc (t + (2::nat) + k + d)) = inf_last_ti dt (t + 2 + k)"
    apply (simp only: GatewayReq_def)
    by (rule GatewaySystem_L3aux, auto) 
  have sg12:"Suc (t + 2 + k) = t + 3 + k" by arith
  from h13 and sg12 have sg12a:"req (Suc (t + 2 + k)) = [send]" 
    by (simp add: eval_nat_numeral)
  from h14 have sg13:"jSuc d. lose ((t + 2 + k) + j) = [False]"
    by (rule streamValue12) 
  from sg11a and sg6a and h13 and sg12a and sg13 have sg14:
    "i (Suc (t + (2::nat) + k + d)) = inf_last_ti dt (t + 2 + k)" by simp
  from h8 have sg15:"inf_last_ti dt (t + 2 + k)  []" 
    by (rule inf_last_ti_Suc2) 
  from sg14 and sg15 have sg16: "i (t + 3 + k + d)  []"
    by (simp add: arith_sum4)
  (* waiting for sc-ack *)
  from h14 have sg17:"jk + d + 3. lose (t + j) = [False]" by auto
  from h12 have sg18:"m < (k + 3). req (t + m)  [send]"   by auto
  from h1 and h4 and h5 and h6 and h7 and h10 and sg18 and h13 and h9 and sg17 and h11 
    have sg19:" t2 < (t + 3 + k + d). i t2 = []"
    by (simp add: Gateway_L7) 
  from h2 and sg19 have sg20:" t3  (t + 3 + k + d). a t3 = []"
    by (simp add: ServiceCenter_L2)
  from h14 have sg21:"j2 * d. lose (t + 3 + k + j) = [False]"
    by (simp add: streamValue43)
  from h1 and h4 and h5 and h6 and h7 and sg21 and sg10 and sg20 have 
    "x  d + d. ack (t + 3 + k + x) = [sending_data]"
    by (simp add: Gateway_L8)
  from h2 and h3 and h4 and h5 and h6 and h7 and h14 and sg16 and this show ?thesis
    by (simp add: GatewaySystem_L1)
qed


subsection ‹Proof of the Refinement for the Gateway System› 

lemma GatewaySystem_L0:
 assumes "GatewaySystem req dt stop lose d ack vc"
 shows    "GatewaySystemReq req dt stop lose d ack vc"
proof - 
  from assms obtain x i where
    a1:"Gateway req dt x stop lose d ack i vc" and 
    a2:"ServiceCenter i x"
    by (simp add: GatewaySystem_def, auto)
  from a1 have sg1:"GatewayReq req dt x stop lose d ack i vc"
    by (simp add: Gateway_L0)
  from a2 have sg2:"msg (Suc 0) x"
    by (simp add: ServiceCenter_a_msg)
  from assms and a1 and a2 and sg1 and sg2 show ?thesis
    apply (simp add: GatewaySystemReq_def, auto)
    apply (simp add: GatewaySystem_L3)
    apply (simp add: GatewaySystem_L3)
    apply (simp add: GatewaySystem_L3)
    by (simp add: GatewaySystem_L2)
qed

end