Theory HBDTranslationProperties

(**-----------------------------------------------------------------------------
 * © [I Dragomir, V Preoteasa, S Tripakis]
 *
 * Contributors:
 *  Viorel Preoteasa
 *  Iulia Dragomir
 *
 * This software is governed by the MIT licence and abiding by the rules of
 * distribution of free software. You can use, modify and/or redistribute the
 * software under the terms of the MIT licence included in this distribution.
 *)

subsection‹Properties for Proving the Abstract Translation Algorithm›

theory HBDTranslationProperties imports ExtendedHBDAlgebra Diagrams
begin
context BaseOperationVars
begin
  
lemma io_diagram_fb_perm_eq: "io_diagram A ⟹ fb_perm_eq A"
proof (simp add: fb_perm_eq_def, safe)
  fix x
  assume [simp]: "perm x (VarFB A)"
  assume [simp]: "io_diagram A"
    
  have [simp]: "perm (VarFB A) x"
    by (simp add: perm_sym)
      
  have [simp]: "set (VarFB A) ∩ set (InFB A) = {}"
    by (simp add: VarFB_def Var_def InFB_def)
      
      
  have [simp]: "set (VarFB A) ∩ set (OutFB A) = {}"
    by (simp add: VarFB_def Var_def OutFB_def)
      
  have [simp]: "perm (Out A) (VarFB A @ OutFB A)"
    by (metis OutFB_def VarFB_def Var_def ‹io_diagram A› diff_inter_left perm_switch_aux_c perm_sym io_diagram_def)
      
  have [simp]: "set x ⊆ set (VarFB A) ∪ set (OutFB A)"
    using ‹perm x (VarFB A)› perm_set_eq by blast
      
  have [simp]: "distinct x"
    using ‹perm x (VarFB A)› 
    by (metis VarFB_def Var_def ‹perm (VarFB A) x› ‹io_diagram A› dist_perm distinct_inter io_diagram_def)
  have "set x ∩ set (InFB A) = {}"
    using ‹perm x (VarFB A)›
    by (metis Diff_disjoint InFB_def perm_diff_eq set_diff)
      
  have [simp]: "set (In A) ⊆ set (VarFB A) ∪ set (InFB A)"
    by (simp add: InFB_def set_diff)
      
  have [simp]: "set x ∩ set (InFB A) = {}"
    by (simp add: ‹set x ∩ set (InFB A) = {}›)
      
  have [simp]: "TI (Trs A) = TVs (In A)"
    using ‹io_diagram A› io_diagram_distinct(3) by blast
  have [simp]: "TO (Trs A) = TVs (Out A)"
    using ‹io_diagram A› io_diagram_distinct(4) by blast
  have [simp]: "distinct (Out A)"
    using ‹io_diagram A› io_diagram_distinct(2) by blast
    
  have "(fb ^^ length (VarFB A)) ([VarFB A @ InFB A ↝ In A] oo Trs A oo [Out A ↝ VarFB A @ OutFB A]) 
    = (fb ^^ length (VarFB A)) ([x @ InFB A ↝ VarFB A @ InFB A] 
      oo ([VarFB A @ InFB A ↝ In A] oo Trs A oo [Out A ↝ VarFB A @ OutFB A]) 
      oo [VarFB A @ OutFB A ↝ x @ OutFB A])"
    
    by (subst fb_perm, simp_all add: fbtype_def)
  also have "... = (fb ^^ length (VarFB A)) ( ([x @ InFB A ↝ VarFB A @ InFB A] 
      oo [VarFB A @ InFB A ↝ In A]) oo Trs A oo ([Out A ↝ VarFB A @ OutFB A]
      oo [VarFB A @ OutFB A ↝ x @ OutFB A]))"
    by (simp add: comp_assoc)
  also have "... = (fb ^^ length (VarFB A)) ( ([x @ InFB A ↝ In A]) oo Trs A oo ([Out A ↝ x @ OutFB A]))"
    apply (subgoal_tac "[x @ InFB A ↝ VarFB A @ InFB A] oo [VarFB A @ InFB A ↝ In A] = [x @ InFB A ↝ In A]")
     apply simp
     apply (subgoal_tac "[Out A ↝ VarFB A @ OutFB A] oo [VarFB A @ OutFB A ↝ x @ OutFB A] = [Out A ↝ x @ OutFB A]")
      apply simp
     by (simp_all add:  switch_comp)
      
    
  finally show "(fb ^^ length (VarFB A)) ([VarFB A @ InFB A ↝ In A] oo Trs A oo [Out A ↝ VarFB A @ OutFB A]) =
         (fb ^^ length (VarFB A)) ([x @ InFB A ↝ In A] oo Trs A oo [Out A ↝ x @ OutFB A])"
    by simp
qed
  
theorem FeedbackSerial: "io_diagram A ⟹ io_diagram B ⟹ set (In A) ∩ set (In B) = {} 
  ⟹ set (Out A) ∩ set (Out B) = {} ⟹ FB (A ||| B) = FB (FB (A) ;; FB (B))"
  
  apply (rule FeedbackSerial_Feedbackless, simp_all)
  apply (rule io_diagram_fb_perm_eq)
  by (simp add: io_diagram_Parallel)
  
lemmas fb_perm_sym = fb_perm [THEN sym]
  
declare length_TVs [simp del]

declare [[simp_trace_depth_limit=40]]
  

lemma in_out_equiv_FB: "io_diagram B ⟹ in_out_equiv A B ⟹ in_out_equiv (FB A) (FB B)"
  apply (rule in_out_equiv_FB_less, simp_all)
  apply (rule io_diagram_fb_perm_eq)
  using in_out_equiv_io_diagram by blast

end
 
end