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