# Theory HBDTranslationProperties

theory HBDTranslationProperties
imports ExtendedHBDAlgebra Diagrams
```(**-----------------------------------------------------------------------------
* © [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) = {} (*required*)
⟹ 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
```