Theory HBDAlgebra

(**-----------------------------------------------------------------------------
 * © [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.
 *)

section‹\label{sec_Translation}Translation of Hierarchical Block Diagrams›

subsection‹Abstract Algebra of  Hierarchical Block Diagrams (except one axiom for feedback)›

theory HBDAlgebra imports ListProp
begin
  
locale BaseOperationFeedbackless =   
  (*Input output types*)
  fixes TI TO :: "'a ⇒ 'tp list"

  (*Identity*)
  fixes ID :: "'tp list ⇒ 'a"
  assumes [simp]: "TI(ID ts) = ts"
  assumes [simp]: "TO(ID ts) = ts"
  
  (*Serial*)
  fixes comp :: "'a ⇒ 'a ⇒ 'a"  (infixl "oo" 70)
  assumes TI_comp[simp]: "TI S' = TO S ⟹ TI (S oo S') = TI S"
  assumes TO_comp[simp]: "TI S' = TO S ⟹ TO (S oo S') = TO S'"
  assumes comp_id_left [simp]: "ID (TI S) oo S  = S"
  assumes comp_id_right [simp]: "S oo ID (TO S) = S"
  assumes comp_assoc: "TI T = TO S ⟹ TI R = TO T ⟹ S oo T oo R = S oo (T oo R)"
  
  
  (*Parallel*)
  fixes parallel :: "'a ⇒ 'a ⇒ 'a"  (infixl "∥" 80)
  assumes TI_par [simp]: "TI (S ∥ T) = TI S @ TI T"
  assumes TO_par [simp]: "TO (S ∥ T) = TO S @ TO T"
  assumes par_assoc: "A ∥ B ∥ C = A ∥ (B ∥ C)"
  assumes empty_par[simp]: "ID [] ∥ S = S"
  assumes par_empty[simp]: "S ∥ ID [] = S" (*can be proved*)
  assumes parallel_ID [simp]: "ID ts ∥ ID ts' = ID (ts @ ts')"
  
  (*Comp Parallel*)
  assumes comp_parallel_distrib: "TO S = TI S' ⟹ TO T = TI T' ⟹ (S ∥ T) oo (S' ∥ T') = (S oo S') ∥ (T oo T')"
  
  (*Split Sink Switch axioms*)
  fixes Split    :: "'tp list ⇒ 'a"
  fixes Sink   :: "'tp list ⇒ 'a"
  fixes Switch :: "'tp list ⇒ 'tp list ⇒ 'a"
  
  assumes TI_Split[simp]: "TI (Split ts) = ts"
  assumes TO_Split[simp]: "TO (Split ts) = ts @ ts"
  
  assumes TI_Sink[simp]: "TI (Sink ts) = ts"
  assumes TO_Sink[simp]: "TO (Sink ts) = []"
  
  assumes TI_Switch[simp]: "TI (Switch ts ts') = ts @ ts'"
  assumes TO_Switch[simp]: "TO (Switch ts ts') = ts' @ ts"
  
  (*todo: check is these can be simplified*)
  assumes Split_Sink_id[simp]: "Split ts oo Sink ts ∥ ID ts = ID ts"
  (*    assumes Split_id_Sink[simp]: "Split ts oo ID ts ∥ Sink ts = ID ts" can be proved*)
  assumes Split_Switch[simp]: "Split ts oo Switch ts ts = Split ts"
  assumes Split_assoc: "Split ts oo ID ts ∥ Split ts = Split ts oo Split ts ∥ ID ts"
  
  assumes Switch_append: "Switch ts (ts' @ ts'') = Switch ts ts' ∥ ID ts'' oo ID ts' ∥ Switch ts ts''"
  assumes Sink_append: "Sink ts ∥ Sink ts' = Sink (ts @ ts')"
  assumes Split_append: "Split (ts @ ts') = Split ts ∥ Split ts' oo ID ts ∥ Switch ts ts' ∥ ID ts'"
  
  (*Switch parallel*)
  assumes switch_par_no_vars: "TI A = ti ⟹ TO A = to ⟹ TI B = ti' ⟹ TO B = to' ⟹ Switch ti ti' oo B ∥ A oo Switch to' to = A ∥ B"
  
  (*feedback axioms*)
  fixes fb :: "'a ⇒ 'a"
  assumes TI_fb: "TI S = t # ts ⟹ TO S = t # ts' ⟹ TI (fb S) = ts" (*simp*)
  assumes TO_fb: "TI S = t # ts ⟹ TO S = t # ts' ⟹ TO (fb S) = ts'" (*simp*)
  assumes fb_comp: "TI S = t # TO A ⟹ TO S = t # TI B ⟹ fb (ID [t] ∥ A oo S oo ID [t] ∥ B) = A oo fb S oo B"
  assumes fb_par_indep: "TI S = t # ts ⟹ TO S = t # ts' ⟹ fb (S ∥ T) = fb S ∥ T"
  
  assumes fb_switch: "fb (Switch [t] [t]) = ID [t]"

begin
definition "fbtype S tsa ts ts' = (TI S = tsa @ ts ∧ TO S = tsa @ ts')"

lemma fb_comp_fbtype: "fbtype S [t] (TO A) (TI B) 
  ⟹ fb ((ID [t] ∥ A) oo S oo (ID [t] ∥ B)) = A oo fb S oo B"
  by (simp add: fbtype_def fb_comp)

lemma fb_serial_no_vars: "TO A = t # ts ⟹ TI B = t # ts 
  ⟹ fb ( ID [t] ∥ A oo Switch [t] [t] ∥ ID ts oo ID [t] ∥ B) = A oo B"
  apply (subst fb_comp)
  apply (simp_all)
  apply (subst fb_par_indep, simp_all)
  apply (simp add: fb_switch)
  by (metis comp_id_right)

lemma TI_fb_fbtype: "fbtype S [t] ts ts' ⟹ TI (fb S) = ts"
  by (simp add: fbtype_def TI_fb)
    
lemma TO_fb_fbtype: "fbtype S [t] ts ts' ⟹ TO (fb S) = ts'"
  by (simp add: fbtype_def TO_fb)

lemma fb_par_indep_fbtype: "fbtype S [t] ts ts' ⟹ fb (S ∥ T) = fb S ∥ T"
  by (simp add: fbtype_def fb_par_indep)

lemma comp_id_left_simp [simp]: "TI S = ts ⟹ ID ts oo S  = S"
  apply (cut_tac S = S in comp_id_left)
  by (simp del: comp_id_left)

      lemma comp_id_right_simp [simp]: "TO S = ts ⟹ S oo ID ts = S"
        apply (cut_tac S = S in comp_id_right)
        by (simp del: comp_id_right)

      lemma par_Sink_comp: "TI A = TO B ⟹ B ∥ Sink t oo A = (B oo A) ∥ Sink t"
        proof -
          assume [simp]: "TI A = TO B"

          have "B ∥ Sink t oo A = B ∥ Sink t oo A ∥ ID []"
            by simp          
          also have "... = (B oo A) ∥ Sink t"
            by (subst comp_parallel_distrib, simp_all)
          finally show ?thesis
            by simp
        qed

      lemma Sink_par_comp: "TI A = TO B ⟹ Sink t ∥ B oo A = Sink t ∥ (B oo A)"
        proof -
          assume [simp]: "TI A = TO B"

          have "Sink t ∥ B oo A  = Sink t ∥ B oo ID [] ∥ A"
            by simp
          also have "... = Sink t ∥ (B oo A)"
            by (subst comp_parallel_distrib, simp_all)
          finally show ?thesis
            by simp
        qed

      lemma Split_Sink_par[simp]: "TI A = ts ⟹ Split ts oo Sink ts ∥ A = A"
        proof -
          assume [simp]: "TI A = ts"
          have "Split ts oo Sink ts ∥ A = Split ts oo (Sink ts oo ID []) ∥ (ID (TI A) oo A)"
            by simp
          also have "... = Split ts oo Sink ts ∥ ID (TI A) oo A"
            by (subst comp_parallel_distrib[THEN sym], simp_all add: comp_assoc[THEN sym])
          also have "... = A"
            by simp
          finally show ?thesis
            by simp
        qed


      lemma Switch_Switch_ID[simp]: "Switch ts ts' oo Switch ts' ts = ID (ts @ ts')" 
        by (cut_tac A = "ID ts" and B = "ID ts'" in switch_par_no_vars, auto)

      lemma Switch_parallel: "TI A = ts' ⟹ TI B = ts ⟹ Switch ts ts' oo A ∥ B = B ∥ A oo Switch (TO B) (TO A)"
        proof -
          assume [simp]: "TI A = ts'" and [simp]: "TI B = ts"
          have "Switch ts ts' oo A ∥ B = Switch ts ts' oo A ∥ B oo Switch (TO A) (TO B) oo Switch (TO B) (TO A)"
            by (simp add: comp_assoc)
          also have "... = B ∥ A oo Switch (TO B) (TO A)"
            by (simp add: switch_par_no_vars)
          finally show ?thesis
            by simp
        qed


      lemma Switch_type_empty[simp]: "Switch ts [] = ID ts"
        by (metis Switch_Switch_ID Switch_append TI_Switch TO_Switch append_Nil empty_par par_empty switch_par_no_vars)

      lemma Switch_empty_type[simp]: "Switch [] ts = ID ts"
        by (metis Switch_Switch_ID Switch_type_empty TO_Switch append_Nil append_Nil2 comp_id_right_simp)

     lemma Split_id_Sink[simp]: "Split ts oo ID ts ∥ Sink ts = ID ts"
      proof - 
        have "Split ts oo ID ts ∥ Sink ts = Split ts oo (Switch ts ts oo  ID ts ∥ Sink ts)"
          by (simp add: comp_assoc [THEN sym])
        also have "... =ID ts"
          by (simp add: Switch_parallel)
        finally show ?thesis
          by simp
        qed

        
    lemma Split_par_Sink[simp]: "TI A = ts ⟹ Split ts oo A ∥ Sink ts = A"
        proof -
          assume [simp]: "TI A = ts"
          have "Split ts oo A ∥ Sink ts = Split ts oo (ID (TI A) oo A) ∥ (Sink ts oo ID [])"
            by simp
          also have "... = Split ts oo  ID (TI A) ∥ Sink ts oo A"
            by (subst comp_parallel_distrib[THEN sym], simp_all add: comp_assoc[THEN sym])
          also have "... = A"
            by simp
          finally show ?thesis
            by simp
        qed
        
      lemma Split_empty [simp]: "Split [] = ID []"
        by (metis par_empty Split_Sink_id Split_par_Sink Sink_append TI_Sink TO_Split append_is_Nil_conv comp_id_right)

      lemma Sink_empty[simp]: "Sink [] = ID []"
        by (metis Split_Sink_id Split_empty TI_Sink comp_id_left_simp par_empty)

      lemma Switch_Split: "Switch ts ts' = Split (ts @ ts') oo Sink ts ∥ ID ts' ∥ ID ts ∥ Sink ts'"
        proof - 
          have "Split (ts @ ts') oo Sink ts ∥ ID ts' ∥ ID ts ∥ Sink ts' = Split ts ∥ Split ts' oo (ID ts ∥ Switch ts ts' ∥ ID ts' oo Sink ts ∥ (ID ts' ∥ ID ts) ∥ Sink ts')"
            by (simp add: Split_append comp_assoc par_assoc del: parallel_ID)
          also have "... = Split ts ∥ Split ts' oo Sink ts ∥ Switch ts ts' ∥ Sink ts'"
            apply (subst comp_parallel_distrib)
            apply simp_all [2]
            by (subst (2) comp_parallel_distrib, simp_all)
          also have "... = Split ts ∥ Split ts' oo (Sink ts ∥ (ID ts ∥ ID ts') ∥ Sink ts' oo ID [] ∥ Switch ts ts' ∥ ID[])"
            apply (subst (2) comp_parallel_distrib)
            apply simp_all [2]
            apply (subst (3) comp_parallel_distrib)
            by simp_all
          also have "... =  Split ts ∥ Split ts' oo (Sink ts ∥ ID ts) ∥ (ID ts' ∥ Sink ts') oo Switch ts ts'"
            by (simp add: comp_assoc par_assoc del: parallel_ID)
          also have "... = Switch ts ts'"
            by (simp add: comp_parallel_distrib)
          finally show ?thesis
            by simp
        qed


      lemma Sink_cons: "Sink (t # ts) = Sink [t] ∥ Sink ts"
        by (simp add: Sink_append)

      lemma Split_cons: "Split (t # ts) = Split [t] ∥ Split ts oo ID [t] ∥ Switch [t] ts ∥ ID ts"
        by (simp add: Split_append [THEN sym])


      lemma Split_assoc_comp: "TI A = ts ⟹ TI B = ts ⟹ TI C = ts ⟹ Split ts oo A ∥ (Split ts oo B ∥ C) = Split ts oo (Split ts oo A ∥ B) ∥ C"
        proof - 
          assume [simp]: "TI A = ts" and [simp]: "TI B = ts" and [simp]: "TI C = ts"
          have "Split ts oo A ∥ (Split ts oo B ∥ C) = Split ts oo ID ts ∥ Split ts oo A ∥ (B ∥ C)"
            by (simp add: comp_assoc comp_parallel_distrib)
          also have "... = Split ts oo (Split ts oo A ∥ B) ∥ C"
            by (subst Split_assoc, simp add: comp_assoc par_assoc [THEN sym] comp_parallel_distrib)
          finally show ?thesis by simp
        qed

      lemma Split_Split_Switch: "Split ts oo Split ts ∥ Split ts oo ID ts ∥ Switch ts ts ∥ ID ts = Split ts oo Split ts ∥ Split ts"
        proof -
          have "Split ts oo Split ts ∥ Split ts = Split ts oo Split ts ∥ (Split ts oo ID ts ∥ ID ts)"
            by simp
          also have "... = Split ts oo (Split ts oo Split ts ∥ ID ts) ∥ ID ts"
            by (subst Split_assoc_comp, simp_all)
          also have "... = Split ts oo (Split ts oo (Split ts oo ID ts ∥ ID ts) ∥ ID ts) ∥ ID ts"
            by (simp)
          also have "... = Split ts oo (Split ts oo ID ts ∥ Split ts) ∥ ID ts"
            by (subst (2) Split_assoc_comp[THEN sym], simp_all)
          finally have A: "Split ts oo Split ts ∥ Split ts = Split ts oo (Split ts oo ID ts ∥ Split ts) ∥ ID ts"
            by simp
          have "Split ts oo Split ts ∥ Split ts oo ID ts ∥ Switch ts ts ∥ ID ts = Split ts oo ((Split ts oo ID ts ∥ Split ts) ∥ ID ts oo ID ts ∥ Switch ts ts ∥ ID ts)"
            by (simp add: A comp_assoc)
          also have "... = Split ts oo (Split ts oo ID ts ∥ Split ts) ∥ ID ts"
            by (simp add: comp_parallel_distrib comp_assoc)
          also have "... =  Split ts oo Split ts ∥ Split ts"
            by (simp add: A)
          finally show ?thesis by simp
        qed
        
      lemma parallel_empty_commute: "TI A = [] ⟹ TO B = [] ⟹ A ∥ B = B ∥ A"
        proof -
        assume [simp]: "TI A = []" and [simp]: "TO B = []"
        have "A ∥ B = Switch (TI B) [] oo A ∥ B"
          by simp
        also have "... = B ∥ A"
          by (subst Switch_parallel, simp_all)
        finally show ?thesis by simp
        qed

    lemma comp_assoc_middle_ext: "TI S2 = TO S1 ⟹ TI S3 = TO S2 ⟹ TI S4 = TO S3 ⟹ TI S5 = TO S4 ⟹
          S1 oo (S2 oo S3 oo S4) oo S5 = (S1 oo S2) oo S3 oo (S4 oo S5)"
        by (simp add: comp_assoc)

        lemma fb_gen_parallel: "⋀ S . fbtype S tsa ts ts' ⟹ (fb^^(length tsa)) (S ∥ T) = ((fb^^(length tsa)) (S)) ∥ T"
          apply (induction tsa, simp_all)
          apply (simp add: funpow_swap1)
          apply (subst fb_par_indep_fbtype)
          apply (simp add:  fbtype_def)
          apply (subgoal_tac "fbtype (fb S) tsa ts ts'")
          apply simp
          apply (simp add: fbtype_def, safe)
          apply (rule TI_fb_fbtype, simp add: fbtype_def)
          by (rule TO_fb_fbtype, simp add: fbtype_def)
            
        lemmas parallel_ID_sym = parallel_ID [THEN sym]
        declare parallel_ID [simp del]

        lemma fb_indep: "⋀S. fbtype S tsa (TO A) (TI B) ⟹ (fb^^(length tsa)) ((ID tsa ∥ A) oo S oo (ID tsa ∥ B)) = A oo (fb^^(length tsa)) S oo B"   
          apply (induction tsa, simp_all)
          apply (simp add: funpow_swap1)
          apply (cut_tac ts="[a]" and ts'=tsa in parallel_ID_sym)
          apply (simp add: par_assoc)
          apply (subst fb_comp_fbtype)
          apply (simp add: fbtype_def)
          apply (subgoal_tac "fbtype (fb S) tsa (TO A) (TI B)")
          apply simp
          apply (simp add: fbtype_def, safe)
          apply (rule TI_fb_fbtype, simp add: fbtype_def)
          by (rule TO_fb_fbtype, simp add: fbtype_def)

        lemma fb_indep_a: "⋀S. fbtype S tsa (TO A) (TI B) ⟹ length tsa = n ⟹ (fb ^^ n) ((ID tsa ∥ A) oo S oo (ID tsa ∥ B)) = A oo (fb ^^ n) S oo B"
          by (drule fb_indep, simp_all)

        lemma fb_comp_right: "fbtype S [t] ts (TI B) ⟹ fb (S oo (ID [t] ∥ B)) = fb S oo B"
          proof -
            assume [simp]: "fbtype S [t] ts (TI B)"
            have "fb (S oo (ID [t] ∥ B)) = fb (ID (t#ts) oo S oo (ID [t] ∥ B))"
              apply (subst comp_id_left_simp)
              apply simp_all
              apply (subgoal_tac "fbtype S [t] ts (TI B)")
              apply (simp add: fbtype_def)
              by simp
            also have "... = fb (ID ([t]) ∥ ID ts oo S oo (ID [t] ∥ B))"
              apply (cut_tac ts="[t]" and ts'="ts" in parallel_ID_sym)
              by simp
            also have "... = ID ts oo fb S oo B"
              apply (rule fb_comp_fbtype)
              by simp
            also have "... = fb S oo B"
              apply (subst comp_id_left_simp)
              apply simp_all
              apply (subgoal_tac "fbtype S [t] ts (TI B)")
              apply (simp only: TI_fb_fbtype)
              by simp
            finally show "fb (S oo (ID [t] ∥ B)) = fb S oo B"
              by simp
          qed

        lemma fb_comp_left: "fbtype S [t] (TO A) ts ⟹ fb ((ID [t] ∥ A) oo S) = A oo fb S"
          proof -
            assume [simp]: "fbtype S [t] (TO A) ts"
            have "fb ((ID [t] ∥ A) oo S) = fb ((ID [t] ∥ A) oo S oo ID (t#ts))"
              apply (subst comp_id_right_simp)
              apply simp_all
              apply (subgoal_tac "fbtype S [t] (TO A) ts")
              apply (subst TO_comp)
              apply (simp add: fbtype_def)
              apply (simp add: fbtype_def)
              by simp
            also have "... = fb (ID ([t]) ∥ A oo S oo (ID [t] ∥ ID ts))"
              apply (cut_tac ts="[t]" and ts'="ts" in parallel_ID)
              by simp
            also have "... = A oo fb S oo ID ts"
              apply (rule fb_comp_fbtype)
              by simp
            also have "... = A oo fb S"
              apply (subst comp_id_right_simp)
              apply simp_all
              apply (subgoal_tac "fbtype S [t] (TO A) ts")
              apply (subst TO_comp)
              apply (simp only: TI_fb_fbtype)
              apply (simp only: TO_fb_fbtype)
              by simp
            finally show "fb ((ID [t] ∥ A) oo S) = A oo fb S"
              by simp
          qed

        lemma fb_indep_right: "⋀S. fbtype S tsa ts (TI B) ⟹ (fb^^(length tsa)) (S oo (ID tsa ∥ B)) = (fb^^(length tsa)) S oo B"   
          apply (induction tsa, simp_all)
          apply (simp add: funpow_swap1)
          apply (cut_tac ts="[a]" and ts'=tsa in parallel_ID_sym)
          apply (simp add: par_assoc)
          apply (subst fb_comp_right)
          apply (simp add: fbtype_def)
          apply (subgoal_tac "fbtype (fb S) tsa ts (TI B)")
          apply simp
          apply (simp add: fbtype_def, safe)
          apply (rule TI_fb_fbtype, simp add: fbtype_def)
          by (rule TO_fb_fbtype, simp add: fbtype_def)

        lemma fb_indep_left: "⋀S. fbtype S tsa (TO A) ts ⟹ (fb^^(length tsa)) ((ID tsa ∥ A) oo S) = A oo (fb^^(length tsa)) S"   
          apply (induction tsa, simp_all)
          apply (simp add: funpow_swap1)
          apply (cut_tac ts="[a]" and ts'=tsa in parallel_ID_sym)
          apply (simp add: par_assoc)
          apply (subst fb_comp_left)
          apply (simp add: fbtype_def)
          apply (subgoal_tac "fbtype (fb S) tsa (TO A) ts")
          apply simp
          apply (simp add: fbtype_def, safe)
          apply (rule TI_fb_fbtype, simp add: fbtype_def)
          by (rule TO_fb_fbtype, simp add: fbtype_def)


       lemma TI_fb_fbtype_n: "⋀S. fbtype S t ts ts' ⟹ TI ((fb^^(length t)) S) = ts"
          and TO_fb_fbtype_n: "⋀S. fbtype S t ts ts' ⟹ TO ((fb^^(length t)) S) = ts'"
        apply (induction t)
        apply (simp add: fbtype_def)
        apply (simp add: fbtype_def)
        apply simp
        apply (simp add: funpow_swap1)
        apply (subgoal_tac "fbtype (fb S) t ts ts'")
        apply (simp add: fbtype_def)
        apply (simp add: fbtype_def)
        apply (cut_tac S=S and t=a and ts = "t@ts" and ts'="t@ts'"in  TI_fb_fbtype)
        apply (simp add: fbtype_def)
        apply (cut_tac S=S and t=a and ts = "t@ts" and ts'="t@ts'"in  TO_fb_fbtype)
        apply (simp add: fbtype_def)
        apply simp

        apply (simp add: funpow_swap1)
        apply (subgoal_tac "fbtype (fb S) t ts ts'")
        apply (simp add: fbtype_def)
        apply (simp add: fbtype_def)
        apply (cut_tac S=S and t=a and ts = "t@ts" and ts'="t@ts'"in  TI_fb_fbtype)
        apply (simp add: fbtype_def)
        apply (cut_tac S=S and t=a and ts = "t@ts" and ts'="t@ts'"in  TO_fb_fbtype)
        apply (simp add: fbtype_def)
        by simp

        declare parallel_ID [simp]
end
  
  
  locale BaseOperationFeedbacklessVars = BaseOperationFeedbackless +
    fixes TV :: "'var ⇒ 'b"
    fixes newvar :: "'var list ⇒ 'b ⇒ 'var"
    assumes newvar_type[simp]: "TV(newvar x t) = t"
    assumes newvar_distinct [simp]: "newvar x t ∉ set x"
    assumes "ID [TV a] = ID [TV a]"
  begin
    primrec TVs::"'var list ⇒ 'b list" where
      "TVs [] = []" |
      "TVs (a # x) = TV a # TVs x"

    lemma TVs_append: "TVs (x @ y) = TVs x @ TVs y"
      by (induction x, simp_all)
      
    definition "Arb t = fb (Split [t])"
      
    lemma TI_Arb[simp]: "TI (Arb t) = []"
      by (simp add: TI_fb Arb_def)

    lemma TO_Arb[simp]: "TO (Arb t) = [t]"
      by (simp add: TO_fb Arb_def)

    fun set_var:: "'var list ⇒ 'var ⇒ 'a" where
      "set_var [] b = Arb (TV b)" |
      "set_var (a # x) b = (if a = b then ID [TV a] ∥ Sink (TVs x) else Sink [TV a] ∥ set_var x b)" 
       
    lemma TO_set_var[simp]: "TO (set_var x a) = [TV a]"
      by (induction x, simp_all)
      
    lemma TI_set_var[simp]: "TI (set_var x a) = TVs x"
      by (induction x, simp_all)

    primrec switch :: "'var list ⇒ 'var list ⇒ 'a" ("[_ ↝ _]") where
      "[x ↝ []] = Sink (TVs x)" |
      "[x ↝ a # y] = Split (TVs x) oo set_var x a ∥ [x ↝ y]"

    lemma TI_switch[simp]: "TI [x ↝ y] = TVs x"
      by (induction y, simp_all)

    lemma TO_switch[simp]: " TO [x ↝ y] = TVs y"
      by (induction y, simp_all)

    lemma switch_not_in_Sink: "a ∉ set y ⟹  [a # x ↝ y] = Sink [TV a] ∥ [x ↝ y]"
      proof (induction y)
        case Nil
        show ?case by (simp add: Sink_append)
        next
        case (Cons b y)
          thm Cons

        have [simp]: "a ≠ b"
          using Cons by simp
        have [simp]: "a ∉ set y"
          using Cons by simp
        thm Split_append
        have "Split (TV a # TVs x) oo Sink [TV a] ∥ set_var x b ∥ (Sink [TV a] ∥ [x ↝ y]) 
          = Split [TV a] ∥ Split (TVs x) oo ID [TV a] ∥ Switch [TV a] (TVs x) ∥ ID (TVs x) oo Sink [TV a] ∥ set_var x b ∥ (Sink [TV a] ∥ [x ↝ y])"
          by (subst Split_cons, simp)
        also have "...= Split [TV a] ∥ Split (TVs x) oo (ID [TV a] ∥ Switch [TV a] (TVs x) ∥ ID (TVs x) oo Sink [TV a] ∥ (set_var x b ∥ Sink [TV a]) ∥ [x ↝ y])"
          by (simp add: par_assoc comp_assoc)
        also have "... = Split [TV a] ∥ Split (TVs x) oo Sink [TV a] ∥ (Switch [TV a] (TVs x) oo set_var x b ∥ Sink [TV a]) ∥ [x ↝ y]"
          by (simp add: comp_parallel_distrib)
        also have "... = Split [TV a] ∥ Split (TVs x) oo Sink [TV a] ∥ (Sink [TV a] ∥ set_var x b) ∥ [x ↝ y]"
          by (subst Switch_parallel, simp_all)
        also have "... = Split [TV a] ∥ Split (TVs x) oo (Sink [TV a] ∥ Sink [TV a]) ∥ (set_var x b ∥ [x ↝ y])"
          by (simp add: par_assoc)
        also have "... = Sink [TV a] ∥ (Split (TVs x) oo set_var x b ∥ [x ↝ y])"
          by (simp add: comp_parallel_distrib)
        finally show ?case
          using Cons by simp
      qed

    lemma distinct_id: "distinct x ⟹ [x ↝ x] = ID (TVs x)"
      proof (induction x)

      case Nil
      show ?case
        by simp
      next
      case (Cons a x)
        have " Split (TV a # TVs x) oo ID [TV a] ∥ Sink (TVs x) ∥ (Sink [TV a] ∥ ID (TVs x)) 
          = Split [TV a] ∥ Split (TVs x) oo ID [TV a] ∥ Switch [TV a] (TVs x) ∥ ID (TVs x) oo ID [TV a] ∥ Sink (TVs x) ∥ (Sink [TV a] ∥ ID (TVs x))"
          by (subst Split_cons, simp)
        also have "... = Split [TV a] ∥ Split (TVs x) oo (ID [TV a] ∥ Switch [TV a] (TVs x) ∥ ID (TVs x) oo ID [TV a] ∥ (Sink (TVs x) ∥ Sink [TV a]) ∥ ID (TVs x))"
          by (simp add: comp_assoc par_assoc)
        also have "... = Split [TV a] ∥ Split (TVs x) oo (ID [TV a] ∥ (Switch [TV a] (TVs x) oo Sink (TVs x) ∥ Sink [TV a]) ∥ ID (TVs x))"
          by (simp add: comp_parallel_distrib)
        also have "... = Split [TV a] ∥ Split (TVs x) oo ID [TV a] ∥ (Sink [TV a] ∥ Sink (TVs x)) ∥ ID (TVs x)"
          by (subst Switch_parallel, simp_all)
        also have "... = Split [TV a] ∥ Split (TVs x) oo (ID [TV a] ∥ Sink [TV a]) ∥ (Sink (TVs x) ∥ ID (TVs x))"
          by (simp add: par_assoc)
        also have "... = ID [TV a] ∥ ID (TVs x)"
          by (simp add: comp_parallel_distrib)
      finally show ?case
        using Cons by (simp add: switch_not_in_Sink)
      qed

      lemma set_var_nin: "a ∉ set x ⟹ set_var (x @ y) a = Sink (TVs x) ∥ set_var y a"
        by (induction x, simp_all, auto simp add: par_assoc [THEN sym] Sink_append)

      lemma set_var_in: "a ∈ set x ⟹ set_var (x @ y) a = set_var x a ∥ Sink (TVs y)"
        by (induction x, simp_all, auto simp add: par_assoc Sink_append TVs_append)
        
      

      lemma set_var_not_in: "a ∉ set y ⟹ set_var y a = Arb (TV a) ∥ Sink (TVs y)"
        apply (induction y, simp_all, auto)
        apply (simp add: par_assoc [THEN sym])
        apply (subst parallel_empty_commute [THEN sym], simp_all)
        by (subst (2) Sink_cons, simp add: par_assoc)

      lemma set_var_in_a: "a ∉ set y ⟹ set_var (x @ y) a = set_var x a ∥ Sink (TVs y)"
        by (induction x, simp_all, auto simp add: par_assoc Sink_append TVs_append set_var_not_in)

      lemma switch_append: "[x ↝ y @ z] = Split (TVs x) oo [x ↝ y] ∥ [x ↝ z]"
        by (induction y, simp_all add: Split_assoc_comp switch_not_in_Sink)

     lemma switch_nin_a_new: "set x ∩ set y' = {} ⟹ [x @ y ↝ y'] = Sink (TVs x) ∥ [y ↝ y']"
      proof (induction y')
        case Nil
        show ?case by (simp add: Sink_append TVs_append)
        next
        case (Cons a y')
        have [simp]: "a ∉ set x"
          using Cons by simp
        have [simp]: "set x ∩ set y' = {}"
          using Cons by simp

        have "Split (TVs x) ∥ Split (TVs y) oo ID (TVs x) ∥ Switch (TVs x) (TVs y) ∥ ID (TVs y) oo Sink (TVs x) ∥ set_var y a ∥ (Sink (TVs x) ∥ [y ↝ y'])
          = Split (TVs x) ∥ Split (TVs y) oo (ID (TVs x) ∥ Switch (TVs x) (TVs y) ∥ ID (TVs y) oo Sink (TVs x) ∥ (set_var y a ∥ Sink (TVs x)) ∥ [y ↝ y'])"
          by (simp add: comp_assoc par_assoc)
        also have "... = Split (TVs x) ∥ Split (TVs y) oo Sink (TVs x) ∥ Sink (TVs x) ∥ set_var y a ∥ [y ↝ y']"
          apply (simp add: comp_parallel_distrib Switch_parallel )
          by (simp add: par_assoc)
        also have "... = Split (TVs x) ∥ Split (TVs y) oo (Sink (TVs x) ∥ Sink (TVs x)) ∥ (set_var y a ∥ [y ↝ y'])"
          by (simp only: par_assoc)

        also have "... = Sink (TVs x) ∥ (Split (TVs y) oo set_var y a ∥ [y ↝ y'])"
          by (simp add: comp_parallel_distrib)

        finally show ?case
          using Cons by (simp add: Sink_append set_var_nin TVs_append Split_append)
      qed

    lemma switch_nin_b_new: "set y ∩ set z = {} ⟹ [x @ y ↝ z] = [x ↝ z] ∥ Sink (TVs y)"
      proof (induction z)
      case Nil
      show ?case by (simp add: TVs_append Sink_append)
      next
      case (Cons a z)
      have [simp]: "a ∉ set y" and [simp]: "set y ∩ set z = {}"
      using Cons by simp_all
      have "Split (TVs (x @ y)) oo set_var (x @ y) a ∥ ([x ↝ z] ∥ Sink (TVs y)) 
        = Split (TVs x) ∥ Split (TVs y) oo (ID (TVs x) ∥ Switch (TVs x) (TVs y) ∥ ID (TVs y) oo set_var x a ∥ (Sink (TVs y) ∥ [x ↝ z]) ∥ Sink (TVs y))"
        by (simp add: Split_append TVs_append set_var_in par_assoc comp_assoc set_var_in_a)
      also have "... = Split (TVs x) ∥ Split (TVs y) oo set_var x a ∥ [x ↝ z] ∥ Sink (TVs y) ∥ Sink (TVs y)"
        apply (simp add: comp_parallel_distrib Switch_parallel)
        by (simp add: par_assoc)
      also have "... =  Split (TVs x) ∥ Split (TVs y) oo (set_var x a ∥ [x ↝ z]) ∥ (Sink (TVs y) ∥ Sink (TVs y))"
        by (simp add: par_assoc)
      also have "... =  (Split (TVs x) oo set_var x a ∥ [x ↝ z]) ∥ Sink (TVs y)"
        by (simp add: comp_parallel_distrib)
      finally show ?case
      using Cons by simp
     qed


     lemma var_switch: "distinct (x @ y) ⟹ [x @ y ↝ y @ x] = Switch (TVs x) (TVs y)"
      proof -
        assume "distinct (x @ y)"
        from this have [simp]: "distinct x" and [simp]: "distinct y" and [simp]: "set x ∩ set y = {}" and [simp]: "set y ∩ set x = {}"
          by auto
        have "[x @ y ↝ y @ x] = Split (TVs x) ∥ Split (TVs y) oo (ID (TVs x) ∥ Switch (TVs x) (TVs y) ∥ ID (TVs y) oo Sink (TVs x) ∥ (ID (TVs y) ∥ ID (TVs x)) ∥ Sink (TVs y))"
          by (simp add: switch_append switch_nin_a_new switch_nin_b_new distinct_id TVs_append Split_append par_assoc comp_assoc del: parallel_ID)
        also have "... = Split (TVs x) ∥ Split (TVs y) oo Sink (TVs x) ∥ Switch (TVs x) (TVs y) ∥ Sink (TVs y)"
          by (simp add: comp_parallel_distrib)

        thm comp_parallel_distrib

        also have "... = Split (TVs x) ∥ Split (TVs y) oo (Sink (TVs x) ∥ (ID (TVs x) ∥ ID (TVs y)) ∥ Sink (TVs y) oo ID [] ∥ Switch (TVs x) (TVs y) ∥ ID [])"
          apply (subst (2) comp_parallel_distrib)
          apply simp_all [2]
          apply (subst (3) comp_parallel_distrib)
          by (simp_all)

        also have "... = Split (TVs x) ∥ Split (TVs y) oo (Sink (TVs x) ∥ ID (TVs x)) ∥ (ID (TVs y) ∥ Sink (TVs y)) oo Switch (TVs x) (TVs y)"
          by (unfold par_assoc, simp add: comp_assoc)
        also have "... = Switch (TVs x) (TVs y)"
          by (subst comp_parallel_distrib, simp_all)
       finally show ?thesis by simp
     qed

    lemma  switch_par: "distinct (x @ y) ⟹ distinct (u @ v) ⟹ TI S = TVs x ⟹ TI T = TVs y ⟹ TO S = TVs v ⟹ TO T = TVs u ⟹ 
      S ∥ T = [x @ y ↝ y @ x] oo T ∥ S oo [u @ v ↝ v @ u]"
      by (simp add: var_switch switch_par_no_vars)


    lemma par_switch: "distinct (x @ y) ⟹ set x' ⊆ set x ⟹ set y' ⊆ set y ⟹  [x ↝ x'] ∥ [y ↝ y'] = [x @ y ↝ x' @ y']"
      proof -
        assume "distinct (x @ y)"
        from this have [simp]: "distinct x" and [simp]: "distinct y" and C: "set x ∩ set y = {}" and "set y ∩ set x = {}"
          by auto
        assume A: "set x' ⊆ set x"
        assume B: "set y' ⊆ set y"
        have "[x @ y ↝ x' @ y'] 
          = Split (TVs x) ∥ Split (TVs y) oo (ID (TVs x) ∥ Switch (TVs x) (TVs y) ∥ ID (TVs y) oo [x ↝ x'] ∥ (Sink (TVs y) ∥ Sink (TVs x)) ∥ [y ↝ y'])"
          using A B apply (subst switch_append, auto)
          using C apply (subst switch_nin_b_new, auto)
          apply (subst switch_nin_a_new, auto)
          by (simp add: Split_append TVs_append comp_assoc par_assoc)
        also have "... = Split (TVs x) ∥ Split (TVs y) oo ([x ↝ x'] ∥ Sink (TVs x)) ∥ (Sink (TVs y) ∥ [y ↝ y'])"
          using A B apply (subst comp_parallel_distrib)
          apply simp_all [2]
          by (subst (2) comp_parallel_distrib, simp_all add: Switch_parallel par_assoc)
        also have "... = [x ↝ x'] ∥ [y ↝ y']"
          using A B by (simp add: comp_parallel_distrib)
        finally show ?thesis
          by simp
      qed


    lemma set_var_sink[simp]: "a ∈ set x ⟹ (TV a) = t ⟹ set_var x a oo Sink [t] = Sink (TVs x)"
      by (induction x, auto simp add: par_Sink_comp Sink_par_comp Sink_append)

    lemma switch_Sink[simp]: "⋀ ts . set u ⊆ set x ⟹ TVs u = ts ⟹ [x ↝ u] oo Sink ts = Sink (TVs x)"
      apply (induction u, simp_all)
      apply (case_tac ts, simp_all)
      apply (subst Sink_cons)
      apply (subst comp_assoc, simp_all)
      by (simp add: comp_parallel_distrib)

    lemma set_var_dup: "a ∈ set x ⟹ TV a = t ⟹ set_var x a oo Split [t] = Split (TVs x) oo set_var x a  ∥ set_var x a"
      proof (induction x)
        case Nil
        from Nil show ?case by simp
        next
        case (Cons b x)

        have "Split (TV b # TVs x) oo ID [TV b] ∥ (Sink (TVs x) ∥ (ID [TV b] ∥ Sink (TVs x))) 
          = Split [TV b] ∥ Split (TVs x) oo (ID [TV b] ∥ Switch [TV b] (TVs x) ∥ ID (TVs x) oo ID [TV b] ∥ (Sink (TVs x) ∥ ID [TV b]) ∥ Sink (TVs x))"
          by (subst Split_cons, simp add: par_assoc comp_assoc)
        also have "... = Split [TV b] ∥ Split (TVs x) oo (ID [TV b] ∥ ID [TV b]) ∥ (Sink (TVs x) ∥ Sink (TVs x))"
          apply (subst comp_parallel_distrib)
          apply (simp_all) [2]
          apply (subst (2) comp_parallel_distrib)
          by (simp_all add: Switch_parallel par_assoc del: parallel_ID) 
        also have "... = Split [TV b] ∥ Sink (TVs x)"
          by (subst comp_parallel_distrib, simp_all)
        also have "... =  ID [TV b] ∥ Sink (TVs x) oo Split [TV b]"
          by (simp add: par_Sink_comp)
        finally have [simp]: "Split (TV b # TVs x) oo ID [TV b] ∥ (Sink (TVs x) ∥ (ID [TV b] ∥ Sink (TVs x))) = ID [TV b] ∥ Sink (TVs x) oo Split [TV b]"
          by simp

        have [simp]: "a = b ⟹ ID [TV a] ∥ Sink (TVs x) oo Split [TV a] = Split (TV a # TVs x) oo ID [TV a] ∥ (Sink (TVs x) ∥ (ID [TV a] ∥ Sink (TVs x)))"
          by simp

        from Cons have "a ∈ set x ⟹ set_var x a oo Split [TV a] = Split (TVs x) oo set_var x a ∥ set_var x a"
          by simp


        have "⋀ A . TI A = TVs x ⟹ Split (TV b # TVs x) oo Sink [TV b] ∥ (A ∥ (Sink [TV b] ∥ A)) 
          = Split [TV b] ∥ Split (TVs x) oo (ID [TV b] ∥ Switch [TV b] (TVs x) ∥ ID (TVs x) oo Sink [TV b] ∥ (A ∥ Sink [TV b]) ∥ A)" 
          by (subst Split_cons, simp add: comp_assoc par_assoc) 
        also have "⋀ A . TI A = TVs x ⟹  Split [TV b] ∥ Split (TVs x) oo (ID [TV b] ∥ Switch [TV b] (TVs x) ∥ ID (TVs x) oo Sink [TV b] ∥ (A ∥ Sink [TV b]) ∥ A) 
          = Split [TV b] ∥ Split (TVs x) oo (Sink [TV b] ∥ Sink [TV b]) ∥ (A ∥ A)"
          apply (subst comp_parallel_distrib)
          apply (simp_all) [2]
          apply (subst (2) comp_parallel_distrib)
          by (simp_all add: Switch_parallel par_assoc) 
        also have "⋀ A . TI A = TVs x ⟹  Split [TV b] ∥ Split (TVs x) oo (Sink [TV b] ∥ Sink [TV b]) ∥ (A ∥ A)
          = Sink [TV b] ∥ (Split (TVs x) oo A ∥ A)"
          by (simp add: comp_parallel_distrib)
        finally have [simp]: "⋀ A . TI A = TVs x ⟹ Split (TV b # TVs x) oo Sink [TV b] ∥ (A ∥ (Sink [TV b] ∥ A)) = Sink [TV b] ∥ (Split (TVs x) oo A ∥ A)"
          by simp
        show ?case
          using Cons apply (auto simp add: par_assoc comp_assoc )
          by (simp add: Sink_par_comp)
      qed

    lemma switch_dup: "⋀ ts . set y ⊆ set x ⟹ TVs y = ts ⟹ [x ↝ y] oo Split ts = Split (TVs x) oo [x ↝ y] ∥ [x ↝ y]"
      proof (induction y)
      case Nil
      show ?case 
        using Nil by simp
      next
      case (Cons a y)

      obtain t ts' where [simp]: "ts = t # ts'" and [simp]: "TV a = t" and [simp]: "TVs y = ts'"
        using Cons by (case_tac ts, simp_all)

      have [simp]: "a ∈ set x"
        using Cons by simp
      have [simp]: "set y ⊆ set x"
        using Cons by simp

      have "Split (TVs x) oo set_var x a ∥ [x ↝ y] oo Split (t # ts') 
        = Split (TVs x) oo set_var x a ∥ [x ↝ y] oo (Split [t] ∥ Split ts' oo ID [t] ∥ Switch [t] ts' ∥ ID ts')"
        by (subst Split_cons, simp)

      also have "... = Split (TVs x) oo (set_var x a ∥ [x ↝ y] oo Split [t] ∥ Split ts') oo ID [t] ∥ Switch [t] ts' ∥ ID ts'"
        by (simp add: comp_assoc)

      also have "... = Split (TVs x) oo (set_var x a oo Split [t]) ∥ ([x ↝ y] oo Split ts') oo ID [t] ∥ Switch [t] ts' ∥ ID ts'"
        by (simp add: comp_parallel_distrib)

      also have "... = Split (TVs x) oo (Split (TVs x) oo set_var x a ∥ set_var x a) ∥ (Split (TVs x) oo [x ↝ y] ∥ [x ↝ y]) oo ID [t] ∥ Switch [t] ts' ∥ ID ts'"
        apply (simp add: set_var_dup)
        using Cons by simp

      also have "... = Split (TVs x) oo Split (TVs x) ∥ Split (TVs x) oo (set_var x a ∥ (set_var x a ∥ [x ↝ y]) ∥ [x ↝ y] oo ID [t] ∥ Switch [t] ts' ∥ ID ts')"
        by (subst comp_parallel_distrib [THEN sym], simp_all add: comp_assoc par_assoc)

      also have "... = Split (TVs x) oo Split (TVs x) ∥ Split (TVs x) oo set_var x a ∥ ( Switch (TVs x) (TVs x) oo [x ↝ y] ∥ set_var x a) ∥ [x ↝ y]"
        apply (simp add: comp_parallel_distrib)
        by (cut_tac A = "[x ↝ y]" and B = " set_var x a" in Switch_parallel, simp_all, auto)

      also have "... = Split (TVs x) oo Split (TVs x) ∥ Split (TVs x) oo (ID (TVs x) ∥ Switch (TVs x) (TVs x) ∥ ID (TVs x) oo set_var x a ∥ ([x ↝ y] ∥ set_var x a) ∥ [x ↝ y])"
        by (simp add: comp_parallel_distrib)

      also have "... = Split (TVs x) oo Split (TVs x) ∥ Split (TVs x) oo set_var x a ∥ ([x ↝ y] ∥ set_var x a) ∥ [x ↝ y]"
        by (simp add: comp_assoc [THEN sym] Split_Split_Switch)

      also have "... =  Split (TVs x) oo (Split (TVs x) oo set_var x a ∥ [x ↝ y]) ∥ (Split (TVs x) oo set_var x a ∥ [x ↝ y])"
        by (simp add: comp_parallel_distrib[THEN sym] comp_assoc par_assoc)

      finally show ?case
        using Cons by simp
    qed

    lemma TVs_length_eq: "⋀ y . TVs x = TVs y ⟹ length x = length y"
      apply (induction x)
      apply (case_tac y, simp)
      apply simp
      apply (case_tac y)
      apply (metis TVs.simps(1) TVs.simps(2) list.distinct(1))
      by simp      

    lemma set_var_comp_subst: "⋀ y . set u ⊆ set x ⟹ TVs u = TVs y  ⟹ a ∈ set y ⟹ [x ↝ u] oo set_var y a = set_var x (subst y u a)"
      apply (induction u, simp_all)
      apply (case_tac y, simp_all)
      apply (case_tac y, simp_all, auto)
      by (simp_all add: comp_assoc comp_parallel_distrib)  

    lemma switch_comp_subst: "set u ⊆ set x ⟹ set v ⊆ set y ⟹ TVs u = TVs y  ⟹ [x ↝ u] oo [y ↝ v] = [x ↝ Subst y u v]"
      apply (induction v, simp_all)
      apply (simp add: comp_assoc [THEN sym])
      apply (subst switch_dup, simp_all)
      by (simp add: comp_assoc comp_parallel_distrib set_var_comp_subst)

    declare switch.simps [simp del]

    lemma sw_hd_var: "distinct (a # b # x) ⟹ [a # b # x ↝ b # a # x] = Switch [TV a] [TV b] ∥ ID (TVs x)"
      apply (subgoal_tac "[a # b # x ↝ b # a # x] = [[a,b]↝ [b,a]] ∥ [x ↝ x]")
      apply (simp add: distinct_id)
      apply (cut_tac x = "[a]" and y = "[b]" in var_switch, simp_all)
      by (subst par_switch, simp_all)


    lemma fb_serial: "distinct (a # b # x) ⟹ TV a = TV b ⟹ TO A = TVs (b # x) ⟹ TI B = TVs (a # x)⟹ fb (([[a] ↝ [a]] ∥ A) oo [a # b # x ↝ b # a # x] oo ([[b] ↝ [b]] ∥ B)) = A oo B"
      by (cut_tac A = A and B = B and t = "TV a" and ts = "TVs x" in fb_serial_no_vars, simp_all add: distinct_id sw_hd_var)

    lemma Switch_Split: "distinct x ⟹  [x ↝ x @ x] = Split (TVs x)"
      by (simp add: distinct_id switch_append)

    lemma  switch_comp: "distinct x ⟹ perm x y ⟹ set z ⊆ set y ⟹ [x↝y] oo [y↝z] = [x↝z]"
        apply (subgoal_tac "distinct y")
        apply (subst switch_comp_subst, simp_all add: Subst_eq)
        using dist_perm by blast

    lemma  switch_comp_a: "distinct x ⟹ distinct y ⟹ set y ⊆ set x ⟹ set z ⊆ set y ⟹[x↝y] oo [y↝z] = [x↝z]"
      by (subst switch_comp_subst, simp_all add: Subst_eq)

      primrec newvars::"'var list ⇒ 'b list ⇒ 'var list" where
        "newvars x [] = []" |
        "newvars x (t # ts) = (let y = newvars x ts in newvar (y@x) t # y)"
        
     lemma newvars_type[simp]: "TVs(newvars x ts) = ts"
        by (induction ts, simp_all add: Let_def)

     lemma newvars_distinct[simp]: "distinct (newvars x ts)"
        apply (induction ts, simp_all add: Let_def)
        apply (subgoal_tac "newvar (newvars x ts @ x) a ∉ set (newvars x ts @ x)")
        apply (simp del: newvar_distinct)
        by (simp only: newvar_distinct, simp) 

     lemma newvars_old_distinct[simp]: "set (newvars x ts) ∩ set x = {}"
        apply (induction ts, simp_all add: Let_def)
        apply (subgoal_tac "newvar (newvars x ts @ x) a ∉ set (newvars x ts @ x)")
        apply (simp del: newvar_distinct)
        by (simp only: newvar_distinct, simp)

     lemma newvars_old_distinct_a[simp]: "set x ∩ set (newvars x ts) = {}"
        apply (cut_tac x = x and ts = ts in newvars_old_distinct)
        by (auto simp del: newvars_old_distinct)
    
     lemma newvars_length: "length(newvars x ts) = length ts"
        by (induction ts, simp_all add: Let_def)

      lemma TV_subst[simp]: "⋀ y . TVs x = TVs y ⟹ TV (subst x y a) = TV a"
        apply (induction x, simp_all)
        apply (case_tac y, simp_all)
        by (case_tac y, auto)

      lemma TV_Subst[simp]: "TVs x = TVs y ⟹ TVs (Subst x y z) = TVs z"
        by (induction z, simp_all)

      lemma Subst_cons: "distinct x ⟹ a ∉ set x ⟹ b ∉ set x ⟹ length x = length y 
        ⟹  Subst (a # x) (b # y) z = Subst x y (Subst [a] [b] z)"
        by (induction z, simp_all)

     declare TVs_append [simp]
     declare distinct_id [simp]

      lemma par_empty_right: "A ∥ [[] ↝ []] = A"
        by (simp)

      lemma par_empty_left: "[[] ↝ []] ∥ A = A"
        by (simp)
      lemma  distinct_vars_comp: "distinct x ⟹ perm x y ⟹ [x↝y] oo [y↝x] = ID (TVs x)"
        by (simp add: switch_comp)
          
      lemma comp_switch_id[simp]: "distinct x ⟹ TO S = TVs x ⟹ S oo [x ↝ x] = S"
        by (simp)

      lemma comp_id_switch[simp]: "distinct x ⟹ TI S = TVs x ⟹ [x ↝ x] oo S = S "
        by (simp)
          
      lemma distinct_Subst_a: "⋀ v . a ≠ aa ⟹ a ∉ set v ⟹ aa ∉ set v ⟹  distinct v ⟹ length u = length v ⟹ subst u v a ≠ subst u v aa"
        apply (induction u, simp_all)
        apply (case_tac v, simp_all, auto)
        apply (metis subst_in_set subst_notin)
        by (metis subst_in_set subst_notin)

      lemma distinct_Subst_b: "⋀ v . a ∉ set x ⟹ distinct x ⟹ a ∉ set v ⟹ distinct v ⟹ set v ∩ set x = {} ⟹ length u = length v ⟹ subst u v a ∉ set (Subst u v x) "
        apply (induction x, simp_all)
        by (rule  distinct_Subst_a, simp_all)

      lemma distinct_Subst: "distinct u ⟹ distinct (v @ x) ⟹ length u = length v ⟹ distinct (Subst u v x)"
        apply (induction x, simp_all)
        by (rule distinct_Subst_b, simp_all)

  lemma Subst_switch_more_general: "distinct u ⟹ distinct (v @ x) ⟹ set y ⊆ set x 
      ⟹ TVs u = TVs v ⟹ [x ↝ y] = [Subst u v x ↝ Subst u v y]"
        proof -
          assume [simp]: "distinct u"
          assume [simp]: "set y ⊆ set x"
          assume [simp]: " TVs u = TVs v"
          assume "distinct (v @ x)"
          from this have [simp]: "distinct v" and [simp]: "distinct x" and [simp]: "set v ∩ set x = {}"
            by simp_all

          have [simp]: "length u = length v"
            by (rule TVs_length_eq, simp)

          have [simp]: "distinct (Subst u v x)"
            by (rule distinct_Subst, simp_all)

          have [simp]: "TVs (Subst u v x) = TVs x"
            by simp

          have [simp]: "Subst x (Subst u v x) y = Subst u v y"
            by (simp add: Subst_Subst)
            
          have "[x ↝ y] = [Subst u v x ↝ Subst u v x] oo [x ↝ y]"
            by (subst comp_id_switch, simp_all)

          also have "... = [Subst u v x ↝ Subst u v y]"
            by (subst switch_comp_subst, simp_all)
          finally show ?thesis
            by simp
       qed

      lemma id_par_comp: "distinct x ⟹ TO A = TI B ⟹ [x ↝ x] ∥ (A oo B) = ([x ↝ x] ∥ A ) oo ([x ↝ x] ∥ B)"
        by (subst comp_parallel_distrib, simp_all)

      lemma par_id_comp: "distinct x ⟹ TO A = TI B ⟹ (A oo B) ∥ [x ↝ x] = (A ∥ [x ↝ x]) oo (B  ∥ [x ↝ x])"
        by (subst comp_parallel_distrib, simp_all)

      lemma  switch_parallel_a: "distinct (x @ y) ⟹ distinct (u @ v) ⟹ TI S = TVs x ⟹ TI T = TVs y ⟹ TO S = TVs u ⟹ TO T = TVs v ⟹ 
        S ∥ T oo [u@v ↝ v@u] = [x@y↝y@x] oo T ∥ S"
        apply (subst switch_par)
        apply simp_all
        apply auto
        apply (simp add: comp_assoc)
        apply (subst switch_comp)
        apply simp_all
        apply auto
        apply (subst perm_tp)
        apply simp_all
        apply (subst distinct_id)
        by auto

  declare distinct_id [simp del]

  lemma fb_gen_serial: "⋀A B v x . distinct (u @ v @ x) ⟹ TO A = TVs (v@x) ⟹ TI B = TVs (u @ x) ⟹  TVs u = TVs v 
        ⟹ (fb ^^ length u) (([u ↝ u] ∥ A) oo [u @ v @ x ↝ v @ u @ x] oo ([v ↝ v] ∥ B)) = A oo B"
        apply (induction u, simp)
        apply (simp add: distinct_id)
        apply (case_tac v, simp_all)
        proof safe
          fix a u A B x b v'
          assume [simp]:"TO A = TV b # TVs v' @ TVs x"
            and [simp]:"TI B = TV b # TVs v' @ TVs x"
            and [simp]:"a ∉ set u"
            and [simp]:"TV a = TV b"
            and [simp]:"TVs u = TVs v'"
          assume [simp]: "a ≠ b"
          from this have [simp]: "b ≠ a"
            by safe
          assume [simp]:"a ∉ set v'"
            and [simp]:"a ∉ set x"
            and [simp]:"distinct u"
            and [simp]:"b ∉ set v'"
            and [simp]:"distinct v'"
            and [simp]:"distinct x"
            and [simp]:"b ∉ set x"
            and [simp]:"set v' ∩ set x = {}"
            and [simp]:"b ∉ set u"
          assume [simp]:"set u ∩ set v' = {}" 
          from this have [simp]:"set v' ∩ set u = {}"
            by blast
          assume [simp]:"set u ∩ set x = {}"

          have [simp]: "length v' = length u"
            by (rule TVs_length_eq, simp)

          have [simp]: "perm (a # u @ b # v' @ x) (a # b # v' @ u @ x)"
            by (simp add: perm_mset )
          have [simp]: "perm (a # u @ b # v' @ x) (b # a # v' @ u @ x)"
            by (simp add: perm_mset )

          have [simp]:"perm (u @ b # v' @ x) (u @ v' @ b # x)"
            by (simp add: perm_mset )

          thm Subst_switch_more_general

          have A: "[u @ b # v' @ x ↝ b # v' @ u @ x] oo [a # v' @ u @ x ↝ v' @ a # u @ x] = [u @ b # v' @ x ↝  v' @ b # u @ x]"
            proof -
              have A: "[a # v' @ u @ x ↝ v' @ a # u @ x] = [b # v' @ u @ x ↝ v' @ b # u @ x]"
                apply (cut_tac u="[a]" and v="[b]" and x="a # v' @ u @ x" and y = "v' @ a # u @ x" in Subst_switch_more_general)
                apply simp_all
                by (simp add: Subst_append)
              have B: "[u @ b # v' @ x ↝ b # v' @ u @ x] oo [a # v' @ u @ x ↝ v' @ a # u @ x] = [u @ b # v' @ x ↝ b # v' @ u @ x] oo [b # v' @ u @ x ↝ v' @ b # u @ x]"
                by (simp add: A)
              also have "... = [u @ b # v' @ x ↝  v' @ b # u @ x]"
                apply (subst switch_comp)
                apply simp_all
                by (simp add: perm_mset union_assoc union_lcomm)
              finally show "[u @ b # v' @ x ↝ b # v' @ u @ x] oo [a # v' @ u @ x ↝ v' @ a # u @ x] = [u @ b # v' @ x ↝  v' @ b # u @ x]"
                by simp
              qed
          have B: "[u @ b # v' @ x ↝ v' @ u @ b # x] oo [v' @ u @ a # x ↝ v' @ a # u @ x] = [u @ b # v' @ x ↝ v' @ b # u @ x]"
            proof -
              have A: "[v' @ u @ a # x ↝ v' @ a # u @ x] = [v' @ u @ b # x ↝ v' @ b # u @ x]"
                apply (cut_tac u="[a]" and v="[b]" and x="v' @ u @ a # x" and y = "v' @ a # u @ x" in Subst_switch_more_general)
                apply simp_all
                by (simp add: Subst_append)
              have B: "[u @ b # v' @ x ↝ v' @ u @ b # x] oo [v' @ u @ a # x ↝ v' @ a # u @ x] = [u @ b # v' @ x ↝ v' @ u @ b # x] oo [v' @ u @ b # x ↝ v' @ b # u @ x]"
                by (simp add: A)
              also have "... = [u @ b # v' @ x ↝ v' @ b # u @ x]"
                apply (subst switch_comp)
                apply simp_all
                by (simp add: perm_mset union_assoc union_lcomm)
              finally show "[u @ b # v' @ x ↝ v' @ u @ b # x] oo [v' @ u @ a # x ↝ v' @ a # u @ x] = [u @ b # v' @ x ↝ v' @ b # u @ x]"
                by simp
            qed
          have C: "[b # v' @ x ↝ v' @ b # x] oo [u @ a # x ↝ a # u @ x] = [b # v' @ x ↝ b # v' @ x]"
            proof -
              have [simp]: "[u @ a # x ↝ a # u @ x] = [u @ b # x ↝ b # u @ x]"
                apply (cut_tac u="[a]" and v="[b]" and x="u @ a # x" and y = "a # u @ x" in Subst_switch_more_general)
                apply simp_all
                by (simp add: Subst_append)
              have [simp]: "[u @ b # x ↝ b # u @ x] = [v' @ b # x ↝ b # v' @ x]"
                apply (cut_tac u=u and v="v'" and x="u @ b # x" and y="b # u @ x" in Subst_switch_more_general)
                apply simp_all
                by (simp add: Subst_append)
              show  "[b # v' @ x ↝ v' @ b # x] oo [u @ a # x ↝ a # u @ x] = [b # v' @ x ↝ b # v' @ x]"
                apply simp
                apply (subst switch_comp)
                apply simp_all
                by (simp add: perm_mset union_assoc union_lcomm)
            qed

          assume ind_hyp: "(⋀A B v x. distinct v ∧ distinct x ∧ set v ∩ set x = {} ∧ set u ∩ set v = {} ∧ set u ∩ set x = {} ⟹
                   TO A = TVs v @ TVs x ⟹ TI B = TVs v @ TVs x ⟹ TVs v' = TVs v ⟹ (fb ^^ length u) ([u ↝ u] ∥ A oo [u @ v @ x ↝ v @ u @ x] oo [v ↝ v] ∥ B) = A oo B)"

          define A' where "A' ≡ [u↝ u] ∥ A oo [u@b#v'@x ↝ b#v'@u@x]"
          define B' where "B' ≡ [a#v'@u@x ↝ v'@a#u@x] oo [v'↝ v'] ∥ B"

          define A'' where "A'' ≡ A oo [b#v'@x ↝ v'@b#x]"
          define B'' where "B'' ≡ [u@a#x ↝ a#u@x] oo B"

          have "fb ((fb ^^ length u) ([a # u ↝ a # u] ∥ A oo [a # u @ b # v' @ x ↝ b # v' @ a # u @ x] oo [b # v' ↝ b # v'] ∥ B)) 
                = (fb ^^ length u) (fb ([a # u ↝ a # u] ∥ A oo [a # u @ b # v' @ x ↝ b # v' @ a # u @ x] oo [b # v' ↝ b # v'] ∥ B))"
            by (simp add: funpow_swap1)
          also have "... = (fb ^^ length u) (fb (([[a] ↝ [a]] ∥ A') oo [a # b # v'@ u @ x ↝ b # a # v'@ u @ x] oo ([[b] ↝ [b]] ∥ B')))"
            proof (simp add: A'_def B'_def)
              have "[[a] ↝ [a]] ∥ ([u ↝ u] ∥ A oo [u @ b # v' @ x ↝ b # v' @ u @ x]) oo 
                        [a # b # v' @ u @ x ↝ b # a # v' @ u @ x] oo [[b] ↝ [b]] ∥ ([a # v' @ u @ x ↝ v' @ a # u @ x] oo [v' ↝ v'] ∥ B) = 
                    ([a#u ↝ a#u] ∥ A oo [a#u @ b # v' @ x ↝ a#b # v' @ u @ x]) oo 
                        [a # b # v' @ u @ x ↝ b # a # v' @ u @ x] oo ([b#a # v' @ u @ x ↝ b#v' @ a # u @ x] oo [b#v' ↝ b#v'] ∥ B)"
                apply (subst id_par_comp, simp_all)
                apply (subst id_par_comp, simp_all)
                apply (simp add: par_assoc [THEN sym] par_switch)
                by (subst par_switch, simp_all, auto)
              also have "... = [a#u ↝ a#u] ∥ A oo ([a#u @ b # v' @ x ↝ a#b # v' @ u @ x] oo 
                        [a # b # v' @ u @ x ↝ b # a # v' @ u @ x] oo [b#a # v' @ u @ x ↝ b#v' @ a # u @ x]) oo [b#v' ↝ b#v'] ∥ B"
                by (simp add: comp_assoc)
              also have "... = [a#u ↝ a#u] ∥ A oo ([a#u @ b # v' @ x ↝ b#v' @ a # u @ x]) oo [b#v' ↝ b#v'] ∥ B"
                apply (subst switch_comp, simp_all)
                 using ‹a # u @ b # v' @ x <~~> a # b # v' @ u @ x› apply auto[1]
                apply auto [1]
                by (subst switch_comp, simp_all)
            finally show "(fb ^^ length u) (fb ([a # u ↝ a # u] ∥ A oo [a # u @ b # v' @ x ↝ b # v' @ a # u @ x] oo [b # v' ↝ b # v'] ∥ B)) =
              (fb ^^ length u)
               (fb ([[a] ↝ [a]] ∥ ([u ↝ u] ∥ A oo [u @ b # v' @ x ↝ b # v' @ u @ x]) oo [a # b # v' @ u @ x ↝ b # a # v' @ u @ x] oo [[b] ↝ [b]] ∥ ([a # v' @ u @ x ↝ v' @ a # u @ x] oo [v' ↝ v'] ∥ B)))"
               by simp

            qed
          also have "... = (fb ^^ length u) (A' oo B')"
            by (subst fb_serial, simp_all add: A'_def B'_def)
          also have "... = (fb ^^ length u) ([u ↝ u] ∥ A'' oo [u@v'@b#x ↝ v'@u@b#x] oo [v' ↝ v'] ∥ B'')"
            apply (simp add: A'_def B'_def A''_def B''_def)
            apply (subst id_par_comp, simp_all)
            apply (subst id_par_comp, simp_all)
            apply (simp add: par_switch)
            apply (rule_tac f = "fb ^^ length u" in arg_cong)
            apply (simp add: comp_assoc [THEN sym])
            apply (rule_tac f = "λ X . X oo [v' ↝ v'] ∥ B" in arg_cong)
            apply (simp add: comp_assoc)
            apply (rule_tac f = "λ X . [u ↝ u] ∥ A oo X" in arg_cong)
            apply (simp add: comp_assoc [THEN sym])
            apply (subst switch_comp)
               apply auto [3]
              apply (simp add: perm_append_Cons)
            by (simp add: A  B)
          also have "... = A'' oo B''"
            apply (rule ind_hyp, simp_all)
            apply (simp add: A''_def)
            by (simp add: B''_def)
          also have "... = A oo ([b # v' @ x ↝ v' @ b # x] oo [u @ a # x ↝ a # u @ x]) oo B"
            apply (simp add: A''_def B''_def)
            by (simp add: comp_assoc)
          also have "... = A oo B"
            by (simp add: C)

          finally show "fb ((fb ^^ length u) ([a # u ↝ a # u] ∥ A oo [a # u @ b # v' @ x ↝ b # v' @ a # u @ x] oo [b # v' ↝ b # v'] ∥ B)) = A oo B"
            by simp
        qed


      lemma fb_par_serial: "distinct(u @ x @ x') ⟹ distinct (u @ y @ x') ⟹ TI A = TVs x ⟹ TO A = TVs (u@y) ⟹ TI B = TVs (u@x') ⟹ TO B = TVs y' ⟹
        (fb^^(length u)) ([u @ x @ x' ↝ x @ u @ x'] oo (A ∥ B)) = (A ∥ ID (TVs x') oo [u @ y @ x' ↝ y @ u @ x'] oo ID (TVs y) ∥ B)"
        proof -
          assume A: "distinct (u @ y @ x')"
          assume E: "distinct(u @ x @ x')"
          assume [simp]: "TO A = TVs (u@y)"
          assume [simp]: "TI A = TVs x"
          assume [simp]: "TI B = TVs (u@x')"
          define v where "v ≡ newvars (u @ x @ x' @ y) (TVs u)"
          have B: "distinct (u @ v @ y @ x')"
            apply (cut_tac x = "u @ x @ x' @ y" and ts = "TVs u" in newvars_old_distinct)
            apply (unfold v_def [THEN symmetric])
            apply (cut_tac A, simp_all)
            apply safe
             apply (simp add: v_def)
             by blast

          have F: "distinct ((v @ y @ u) @ x')"
            apply (cut_tac x = "u @ x @ x' @ y" and ts = "TVs u" in newvars_old_distinct)
            apply (unfold v_def [THEN symmetric])
            apply (cut_tac A, simp_all)
            apply (simp add: v_def)
              by blast

          have [simp]: "TVs v= TVs u"
            by (simp add: v_def)
          have AA: "(fb ^^ length u) ([u ↝ u] ∥ (A ∥ [x' ↝ x']) oo [u @ v @ y @ x' ↝ v @ u @ y @ x'] oo [v ↝ v] ∥ ([u @ y @ x' ↝ y @ u @ x'] oo [y ↝ y] ∥ B)) 
              = A ∥ [x' ↝ x'] oo ([u @ y @ x' ↝ y @ u @ x'] oo [y ↝ y] ∥ B)"
            apply (cut_tac x = "y @ x'" and u = u and v = v  and A = "A ∥ [x' ↝ x']" and B = "[u @ y @ x' ↝ y @ u @ x'] oo ([y ↝ y] ∥ B)" in fb_gen_serial)
            by (cut_tac B, simp, simp_all)

          (*use "[v ↝ v] ∥ (A oo B) = [v ↝ v] ∥ A oo [v ↝ v] ∥ B"*)  
          have C: "[v ↝ v] ∥ ([u @ y @ x' ↝ y @ u @ x'] oo [y ↝ y] ∥ B) = [v @ u @ y @ x' ↝ v @ y @ u @ x'] oo [v @ y ↝ v @ y] ∥ B"
            apply (subst id_par_comp, simp_all)
            apply (simp add: v_def)
            apply (subst par_assoc [THEN sym])
            apply (subst par_switch)
            apply (cut_tac F, auto)
            apply (subst par_switch)
            by (cut_tac F, auto)

          have "[u ↝ u] ∥ (A ∥ [x' ↝ x']) oo [u @ v @ y @ x' ↝ v @ u @ y @ x'] oo [v ↝ v] ∥ ([u @ y @ x' ↝ y @ u @ x'] oo [y ↝ y] ∥ B) = 
           [u ↝ u] ∥ (A ∥ [x' ↝ x']) oo [u @ v @ y @ x' ↝ v @ u @ y @ x'] oo ([v @ u @ y @ x' ↝ v @ y @ u @ x'] oo [v @ y ↝ v @ y] ∥ B)"
           by (simp add: C)
          also have "... = [u ↝ u] ∥ (A ∥ [x' ↝ x']) oo ([u @ v @ y @ x' ↝ v @ u @ y @ x'] oo [v @ u @ y @ x' ↝ v @ y @ u @ x']) oo [v @ y ↝ v @ y] ∥ B"
            by (simp add: comp_assoc)
          also have "... = [u ↝ u] ∥ (A ∥ [x' ↝ x']) oo [u @ v @ y @ x' ↝ v @ y @ u @ x'] oo [v @ y ↝ v @ y] ∥ B"
            apply (subst switch_comp, simp_all)
            apply (cut_tac B, simp)
            apply (simp add: perm_mset)
            by auto

          thm switch_par

         also have "... = ([u @ x @ x' ↝ x @ u @ x'] oo (A ∥ [u @ x' ↝ u @ x']) oo [v @ y @ u @ x' ↝ u @ v @ y @ x']) oo  [u @ v @ y @ x' ↝ v @ y @ u @ x'] oo [v @ y ↝ v @ y] ∥ B"
          apply (subgoal_tac "[u ↝ u] ∥ (A ∥ [x' ↝ x']) = [u @ x @ x' ↝ x @ u @ x'] oo A ∥ [u @ x' ↝ u @ x'] oo [v @ y @ u @ x' ↝ u @ v @ y @ x']", simp_all)
          apply (subst par_assoc [THEN sym])
          apply (subst switch_par [of "u" "x" "v @ y" "u"])
          apply (cut_tac E, simp)
                apply (cut_tac B)
                apply simp
             apply blast
          apply simp_all
          apply (subst par_id_comp)
          apply (cut_tac A, simp)
          apply (subst TO_comp, simp_all)
          apply (subst par_id_comp)
          apply (cut_tac A, simp)
          apply (subst TI_par, simp_all)
          apply (subst par_assoc)
          apply (subst par_switch)
          apply (cut_tac E, simp_all)
          apply (subst par_switch)
          apply (cut_tac E, simp_all)
          apply (subst par_switch)
          by (cut_tac F, simp_all, auto)

         also have "... = [u @ x @ x' ↝ x @ u @ x'] oo (A ∥ [u @ x' ↝ u @ x']) oo ([v @ y @ u @ x' ↝ u @ v @ y @ x'] oo  [u @ v @ y @ x' ↝ v @ y @ u @ x']) oo [v @ y ↝ v @ y] ∥ B"
          by (simp add: comp_assoc)


         also have "... = [u @ x @ x' ↝ x @ u @ x'] oo (A ∥ [u @ x' ↝ u @ x']) oo [v @ y ↝ v @ y] ∥ B"
          apply (subst switch_comp)
          apply (cut_tac F, simp)
          apply (simp add: add.left_commute perm_mset)
          using F TO_comp by auto
         also have "... = [u @ x @ x' ↝ x @ u @ x'] oo (A ∥ [u @ x' ↝ u @ x'] oo [v @ y ↝ v @ y] ∥ B)"
          using local.comp_assoc by auto
         also have "... =([u @ x @ x' ↝ x @ u @ x'] oo A ∥ B)"
          apply (subgoal_tac "(A ∥ [u @ x' ↝ u @ x'] oo [v @ y ↝ v @ y] ∥ B) = A ∥ B")
          apply (simp_all)
          apply (subst comp_parallel_distrib, simp_all)
          apply (subst comp_switch_id, simp_all)
          apply (cut_tac B, simp)
          apply (subst comp_id_switch, simp_all)
          by (cut_tac B, simp)

         finally have [simp]: "[u ↝ u] ∥ (A ∥ [x' ↝ x']) oo [u @ v @ y @ x' ↝ v @ u @ y @ x'] oo [v ↝ v] ∥ ([u @ y @ x' ↝ y @ u @ x'] oo [y ↝ y] ∥ B) = 
           ([u @ x @ x' ↝ x @ u @ x'] oo A ∥ B)"
           by simp

        show ?thesis
          apply (cut_tac AA)
          apply simp
          using F distinct_id local.comp_assoc by auto
      qed


      (*!!!*)
      (*to prove this using dist x, s, t and set u ⊆ set x and set v ⊆ set x ⟹ x[x → u @ v] oo ([u → s] ||| [v → t]) = [x → s @ t]*)
      (* TO CHECK → the axiom still requires set (In A) ∩ set (In B) = {}, etc.) → maybe needs to be changed *)


      lemma switch_newvars: "distinct x ⟹ [newvars w (TVs x) ↝ newvars w (TVs x)] = [x ↝ x]"
        by (simp add: distinct_id)


      lemma switch_par_comp_Subst: "distinct x ⟹ distinct y' ⟹ distinct z' ⟹ set y ⊆ set x 
      ⟹ set z ⊆ set x 
        ⟹ set u ⊆ set y' ⟹ set v ⊆ set z' ⟹ TVs y = TVs y' ⟹ TVs z = TVs z' ⟹
        [x ↝ y @ z] oo [y' ↝ u] ∥ [z' ↝ v] = [x ↝ Subst y' y u @ Subst z' z v]"
        proof -
          assume [simp]: "distinct y'"
          assume [simp]: "set u ⊆ set y'"
          assume [simp]: "distinct z'"
          assume [simp]: "set v ⊆ set z'"
          assume [simp]: "distinct x"
          assume [simp]: "TVs y = TVs y'"
          assume [simp]: "TVs z = TVs z'"
          assume "set y ⊆ set x"
          assume "set z ⊆ set x"

          define y'' where "y'' ≡ newvars (y' @ z') (TVs y')"

          have [simp]: "distinct y''"
            by (simp add: y''_def)

          have [simp]: "set y' ∩ set y'' = {}"
            by (metis Un_iff disjoint_iff_not_equal newvars_old_distinct_a set_append y''_def)

          have [simp]: "set y'' ∩ set z' = {}"
            by (metis Un_iff disjoint_iff_not_equal newvars_old_distinct_a set_append y''_def)

          have [simp]: "TVs y' = TVs y''"
            by (simp add: y''_def)            

          have [simp]: "length y' = length y''"
            by (rule TVs_length_eq, simp)

          have [simp]: "TVs y = TVs y''"
            by simp

          have [simp]: "length y'' = length y"
            by (metis  ‹TVs y = TVs y''› TVs_length_eq)

          have [simp]: "length z' = length z"
            by (metis ‹TVs z = TVs z'› TVs_length_eq)

          have [simp]: "set z' ∩ set (Subst y' y'' u) = {}"
            apply (subgoal_tac "set (Subst y' y'' u) ⊆ set y''")
            apply (subgoal_tac "set z' ∩ set y'' = {}")
            apply blast
            apply (simp add: Int_commute)
            by (subst Subst_set_incl, simp_all)

          have [simp]: "Subst y'' y (Subst y' y'' u) = (Subst y' y u)"
            by (rule Subst_Subst_a, simp_all)

          have [simp]: "Subst (y'' @ z') (y @ z) (Subst y' y'' u) = (Subst y' y u)"
            apply (subst Subst_not_in)
            by simp_all

          have [simp]: "set y'' ∩ set v = {}"
            apply (subgoal_tac "set v ⊆ set z'")
            apply (subgoal_tac "set y'' ∩ set z' = {}")
            apply blast
            by simp_all

          have [simp]: "Subst (y'' @ z') (y @ z) v = (Subst z' z v)"
            by (subst Subst_not_in_a, simp_all)

          have [simp]: "Subst (y'' @ z') (y @ z) ((Subst y' y'' u) @ v) = ((Subst y' y u) @ (Subst z' z v))"
            by (simp add: Subst_append)

          have "[x ↝ y @ z] oo [y' ↝ u] ∥ [z' ↝ v] = [x ↝ y @ z] oo [y'' ↝ Subst y' y'' u] ∥ [z' ↝ v]"
            by (cut_tac x=y' and y=u and u = y' and v =y'' in Subst_switch_more_general, simp_all add: Int_commute)
          also have "... = [x ↝ y @ z] oo [y'' @ z' ↝ (Subst y' y'' u) @ v]"
            apply (subst par_switch, simp_all)
            by (subst Subst_set_incl, simp_all)
          also have "... = [x ↝ Subst (y'' @ z') (y @ z) ((Subst y' y'' u) @ v)]"
            apply (subst switch_comp_subst, auto)
            using ‹set y ⊆ set x› apply auto [1]
            using ‹set z ⊆ set x › apply auto [1]
            using Subst_set_incl ‹length y' = length y''› ‹set u ⊆ set y'› apply blast
            using ‹set v ⊆ set z'› by blast
          also have "... = [x ↝ (Subst y' y u) @ (Subst z' z v)]"
            by simp
          finally show ?thesis
            by simp
        qed
            
      lemma switch_par_comp: "distinct x ⟹ distinct y ⟹ distinct z ⟹ set y ⊆ set x ⟹ set z ⊆ set x 
        ⟹ set y' ⊆ set y ⟹ set z' ⊆ set z ⟹ [x ↝ y @ z] oo [y ↝ y'] ∥ [z ↝ z'] = [x ↝ y' @ z']"
        by (subst switch_par_comp_Subst, simp_all add: Subst_eq)

      lemma par_switch_eq: "distinct u ⟹ distinct v ⟹ distinct y' ⟹ distinct z' 
            ⟹ TI A = TVs x ⟹ TO A = TVs v ⟹ TI C = TVs v @ TVs y ⟹ TVs y = TVs y' ⟹
            TI C' = TVs v @ TVs z ⟹ TVs z = TVs z' ⟹
            set x ⊆ set u ⟹ set y ⊆ set u ⟹ set z ⊆ set u ⟹ 
            [v ↝ v] ∥ [u ↝ y] oo C = [v ↝ v] ∥ [u ↝ z] oo C' 
            ⟹ [u ↝ x @ y] oo ( A ∥ [y' ↝ y']) oo C = [u ↝ x @ z] oo ( A ∥ [z' ↝ z']) oo C'"
        proof -
          assume [simp]: "distinct u"
          assume [simp]: "set x ⊆ set u"
          assume [simp]: "set y ⊆ set u"
          assume [simp]: "TVs y = TVs y'"
          assume [simp]: "TI A = TVs x"
          assume [simp]: "distinct y'"
          assume [simp]: "TO A = TVs v"
          assume [simp]: "distinct v"
          assume [simp]: "TI C = TVs v @ TVs y"
          assume eq: "[v ↝ v] ∥ [u ↝ y] oo C = [v ↝ v] ∥ [u ↝ z] oo C'"
          assume [simp]: "TI C' = TVs v @ TVs z"
          assume [simp]: "TVs z = TVs z'"
          assume [simp]: "distinct z'"
          assume [simp]: "set z ⊆ set u"

          define x' where "x' ≡ newvars (x @ u) (TVs x)"

          have [simp]: "distinct x'"
            by (simp add: x'_def)

          have [simp]: "TVs x' = TVs x"
            by (simp add: x'_def)

          have [simp]: "length x' = length x"
            by (metis ‹TVs x' = TVs x› TVs_length_eq)

          have "[u ↝ x @ y] oo ( A ∥ [y' ↝ y']) oo C = ([u ↝ x @ u] oo [x' ↝ x'] ∥ [u ↝ y]) oo ( A ∥ [y' ↝ y']) oo C"
            by (simp add: switch_par_comp_Subst Subst_eq)
          also have "... = [u ↝ x @ u] oo ([x' ↝ x'] ∥ [u ↝ y] oo  A ∥ [y' ↝ y']) oo C"
            by (simp add: comp_assoc)
          also have "... = [u ↝ x @ u] oo A ∥ [u ↝ y] oo C"
            by (simp add: comp_parallel_distrib  )
          also have "... = [u ↝ x @ u] oo (A ∥ [u ↝ u] oo [v ↝ v] ∥ [u ↝ y]) oo C"
            by (simp add: comp_parallel_distrib)
          also have "... = [u ↝ x @ u] oo A ∥ [u ↝ u] oo ([v ↝ v] ∥ [u ↝ y] oo C)"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ x @ u] oo A ∥ [u ↝ u] oo ([v ↝ v] ∥ [u ↝ z] oo C')"
            by (simp add: eq)
          also have "... = [u ↝ x @ u] oo (A ∥ [u ↝ u] oo [v ↝ v] ∥ [u ↝ z]) oo C'"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ x @ u] oo A ∥ [u ↝ z] oo C'"
            by (simp add: comp_parallel_distrib)
          also have "... = [u ↝ x @ u] oo ([x' ↝ x'] ∥ [u ↝ z] oo A ∥ [z' ↝ z']) oo C'"
            by (simp add: comp_parallel_distrib)
          also have "... = ([u ↝ x @ u] oo [x' ↝ x'] ∥ [u ↝ z]) oo A ∥ [z' ↝ z'] oo C'"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ x @ z] oo A ∥ [z' ↝ z'] oo C'"
            by (simp add: switch_par_comp_Subst Subst_eq)
          finally show ?thesis
            by simp
        qed

      lemma paralle_switch: "∃ x y u v. distinct (x @ y) ∧ distinct (u @ v) ∧ TVs x = TI A 
        ∧ TVs u = TO A ∧ TVs y = TI B ∧ 
        TVs v = TO B ∧ A ∥ B = [x @ y ↝ y @ x] oo (B ∥ A) oo [v @ u ↝ u @ v]"
        apply (rule_tac x="newvars [] (TI A)" in exI)
        apply (rule_tac x="newvars (newvars [] (TI A)) (TI B)" in exI)
        apply (rule_tac x="newvars [] (TO A)" in exI)
        apply (rule_tac x="newvars (newvars [] (TO A)) (TO B)" in exI)
        by (subst switch_par, simp_all)

      lemma par_switch_eq_dist: "distinct (u @ v) ⟹ distinct y' ⟹ distinct z' ⟹ TI A = TVs x ⟹ TO A = TVs v ⟹ TI C = TVs v @ TVs y ⟹ TVs y = TVs y' ⟹
            TI C' = TVs v @ TVs z ⟹ TVs z = TVs z' ⟹
            set x ⊆ set u ⟹ set y ⊆ set u ⟹ set z ⊆ set u ⟹ 
            [v @ u ↝ v @ y] oo C = [v @ u ↝ v @ z] oo C' ⟹ [u ↝ x @ y] oo ( A ∥ [y' ↝ y']) oo C = [u ↝ x @ z] oo ( A ∥ [z' ↝ z']) oo C'"  
        apply (rule  par_switch_eq, simp_all)
        by (simp add: par_switch Int_commute)

      lemma par_switch_eq_dist_a: "distinct (u @ v) ⟹ TI A = TVs x ⟹ TO A = TVs v ⟹ TI C = TVs v @ TVs y ⟹ TVs y = ty ⟹ TVs z = tz ⟹
            TI C' = TVs v @ TVs z ⟹ set x ⊆ set u ⟹ set y ⊆ set u ⟹ set z ⊆ set u ⟹ 
            [v @ u ↝ v @ y] oo C = [v @ u ↝ v @ z] oo C' ⟹ [u ↝ x @ y] oo A ∥ ID ty oo C = [u ↝ x @ z] oo A ∥ ID tz oo C'"
        apply (cut_tac y' = "newvars [] ty" and z' = "newvars [] tz" and C = C 
            and x = x and y = y and z = z in par_switch_eq_dist, simp_all)
        by (simp add: distinct_id)


      lemma par_switch_eq_a: "distinct (u @ v) ⟹ distinct y' ⟹ distinct z' ⟹ distinct t' ⟹ distinct s'
            ⟹ TI A = TVs x ⟹ TO A = TVs v ⟹ TI C = TVs t @ TVs v @ TVs y ⟹ TVs y = TVs y' ⟹
            TI C' = TVs s @  TVs v @ TVs z ⟹ TVs z = TVs z' ⟹ TVs t = TVs t' ⟹  TVs s = TVs s' ⟹
            set t ⊆ set u ⟹ set x ⊆ set u ⟹ set y ⊆ set u ⟹ set s ⊆ set u ⟹ set z ⊆ set u ⟹
            [u @ v ↝ t @ v @ y] oo C = [u @ v ↝ s @ v @ z] oo C' ⟹ 
            [u ↝ t @ x @ y] oo ([t' ↝ t'] ∥ A ∥ [y' ↝ y']) oo C = [u ↝ s @ x @ z] oo ([s' ↝ s'] ∥ A ∥ [z' ↝ z']) oo C'"
        proof -

          assume [simp]: "distinct (u @ v)"
          assume [simp]: "distinct y'"
          assume [simp]: "distinct z'"
          assume [simp]: "distinct t'"
          assume [simp]: "distinct s'"
          assume [simp]: "set t ⊆ set u"
          assume [simp]: "set x ⊆ set u"
          assume [simp]: "set y ⊆ set u"
          assume [simp]: "set s ⊆ set u"
          assume [simp]: "set z ⊆ set u"
          assume [simp]: "TVs y = TVs y'"
          assume [simp]: "TVs t = TVs t'"
          assume [simp]: "TVs s = TVs s'"
          assume [simp]: "TVs z = TVs z'"
          assume [simp]: "TI A = TVs x"
          assume [simp]: "TO A = TVs v"
          assume [simp]: "TI C = TVs t @ TVs v @ TVs y"
          assume [simp]: "TI C' = TVs s @  TVs v @ TVs z"
          assume eq: "[u @ v ↝ t @ v @ y] oo C = [u @ v ↝ s @ v @ z] oo C'"

          define x' where "x' ≡ newvars u (TVs x)"
          define y'' where "y'' ≡ newvars (x' @ v) (TVs y')"
          define z'' where "z'' ≡ newvars (x' @ v) (TVs z')"


          have [simp]: "distinct u"
            using ‹distinct (u @ v)› by fastforce

          have [simp]: "distinct v"
            using ‹distinct (u @ v)› by fastforce

          have [simp]: "set u ∩ set v = {}"
            using ‹distinct (u @ v)› by fastforce


          have [simp]: "distinct x'"
            by (simp add: x'_def)

          have [simp]: "set u ∩ set x' = {}"
            by (simp add: x'_def)

          have [simp]: "TVs x' = TVs x"
            by (simp add: x'_def)

          have [simp]: "length x' = length x"
            by (metis ‹TVs x' = TVs x› TVs_length_eq)

          have [simp]: "set x' ∩ set t = {}"
            using ‹set t ⊆ set u› ‹set u ∩ set x' = {}› by blast

          have [simp]: "set x' ∩ set y = {}"
            using ‹set y ⊆ set u› ‹set u ∩ set x' = {}› by blast

          have [simp]: "distinct y''"
            by (simp add: y''_def)

          have [simp]: "set x' ∩ set y'' = {}"
            by (metis Diff_disjoint Int_commute diff_disjoint diff_union inter_subset newvars_old_distinct_a set_diff set_inter y''_def)

          have [simp]: "set y'' ∩ set v = {}"
            by (metis Diff_disjoint Int_commute diff_disjoint diff_union newvars_old_distinct_a set_diff set_inter y''_def)

          have [simp]: "TVs y'' = TVs y'"
            by (simp add: y''_def)

          have [simp]: "length t' = length t"
            by (metis ‹TVs t = TVs t'› TVs_length_eq)

          have [simp]: "length y' = length y"
            by (metis ‹TVs y = TVs y'› TVs_length_eq)

          have B: "TVs y'' = TVs y" 
            by (simp add: y''_def)

          have [simp]: "length y'' = length y"
            by (metis ‹TVs y'' = TVs y› TVs_length_eq)

          have [simp]: "set t ⊆ set u ∪ set x'"
            by (metis Un_subset_iff ‹set t ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "set y ⊆ set u ∪ set x'"
            by (metis Un_subset_iff ‹set y ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "set t ⊆ set u ∪ set v"
            by (metis Un_subset_iff ‹set t ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "set y ⊆ set u ∪ set v"
            by (metis Un_subset_iff ‹set y ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "distinct z''"
            by (simp add: z''_def)

          have [simp]: "set z'' ∩ set v = {}"
            by (metis Diff_disjoint diff_disjoint diff_union newvars_old_distinct_a set_diff z''_def)
            
          have [simp]: "set s ⊆ set u ∪ set v"
            by (metis Un_subset_iff ‹set s ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "set z ⊆ set u ∪ set v"
            by (metis Un_subset_iff ‹set z ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "TVs z' = TVs z''"
            by (simp add: z''_def)

          have [simp]: "length s' = length s"
            by (metis  ‹TVs s = TVs s'› TVs_length_eq)

          have [simp]: "length z' = length z"
            by (metis  ‹TVs z = TVs z'› TVs_length_eq)

          have A: "TVs z'' = TVs z"
            by simp

          have [simp]: "length z'' = length z"
            by (metis ‹TVs z'' = TVs z› TVs_length_eq)

          have [simp]: "set x' ∩ set z'' = {}"
            by (metis Int_commute inf_bot_right inf_left_commute inf_sup_absorb newvars_old_distinct_a set_append z''_def)

          have [simp]: "set s ⊆ set u ∪ set x'"
            by (metis Un_subset_iff ‹set s ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "set z ⊆ set u ∪ set x'"
            by (metis Un_subset_iff ‹set z ⊆ set u› sup.absorb_iff1 sup_ge1)

          have [simp]: "set x' ∩ set s = {}"
            using ‹set s ⊆ set u› ‹set u ∩ set x' = {}› by blast

          have [simp]: "set x' ∩ set z = {}"
            using ‹set z ⊆ set u› ‹set u ∩ set x' = {}› by blast

          have "[u ↝ t @ x @ y] oo ([t' ↝ t'] ∥ A ∥ [y' ↝ y']) oo C = ([u ↝ u @ x] oo [u @ x' ↝ t @ x' @ y]) oo ([t' ↝ t'] ∥ A ∥ [y' ↝ y']) oo C"
            apply (subst switch_comp_subst, simp_all)
            by (simp add: Subst_append Subst_not_in Subst_not_in_a Subst_eq)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ t @ x' @ y] oo [t' ↝ t'] ∥ A ∥ [y' ↝ y']) oo C"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ t @ x' @ y] oo [t' ↝ t'] ∥ (A ∥ [y' ↝ y'])) oo C"
            by (simp add: par_assoc)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ t @ x' @ y] oo [t' ↝ t'] ∥ (A ∥ [y'' ↝ y''])) oo C"
            by (simp add: y''_def switch_newvars)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ t @ x' @ y] oo [t' ↝ t'] ∥ ([x' @ y'' ↝ y'' @ x'] oo [y'' ↝ y''] ∥ A oo [y'' @ v ↝ v @ y''])) oo C"
            by (subst(2) switch_par, simp_all)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ t @ x' @ y] oo ([t' ↝ t'] ∥ [x' @ y'' ↝ y'' @ x'] oo [t' ↝ t'] ∥ ([y'' ↝ y''] ∥ A) oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''])) oo C"
            by (simp add: comp_parallel_distrib  )
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ t @ x' @ y] oo [t' ↝ t'] ∥ [x' @ y'' ↝ y'' @ x']) oo [t' ↝ t'] ∥ ([y'' ↝ y''] ∥ A) oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ u @ x] oo [u @ x' ↝ (Subst t' t t') @ (Subst (x' @ y'') (x' @ y) (y'' @ x'))] oo [t' ↝ t'] ∥ ([y'' ↝ y''] ∥ A) oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: switch_par_comp_Subst)
          also have "... = [u ↝ u @ x] oo [u @ x' ↝ t @ y @ x'] oo [t' ↝ t'] ∥ ([y'' ↝ y''] ∥ A) oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: Subst_append Subst_not_in Subst_not_in_a Subst_eq Int_commute)
          also have "... = [u ↝ u @ x] oo [u ↝ t @ y] ∥ [x' ↝ x'] oo ([t' ↝ t'] ∥ [y'' ↝ y'']) ∥ A oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            apply (simp add: par_assoc)
            by (cut_tac x="u" and x'="t@y" and y="x'" and y'="x'" in par_switch, simp_all)
          also have "... = [u ↝ u @ x] oo ([u ↝ t @ y] ∥ [x' ↝ x'] oo ([t' ↝ t'] ∥ [y'' ↝ y'']) ∥ A) oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: comp_assoc )
          also have "... = [u ↝ u @ x] oo ([u ↝ t @ y] oo ([t' ↝ t'] ∥ [y'' ↝ y''])) ∥ A oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: comp_parallel_distrib)
          also have "... = [u ↝ u @ x] oo [u ↝ t @ y] ∥ A oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: switch_par_comp_Subst)
          also have "... = [u ↝ u @ x] oo ([u ↝ u] oo [u ↝ t @ y]) ∥ (A oo [v ↝ v]) oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: )
          also have "... = [u ↝ u @ x] oo ([u ↝ u] ∥ A  oo [u ↝ t @ y] ∥ [v ↝ v]) oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y''] oo C"
            by (simp add: comp_parallel_distrib )
          also have "... = [u ↝ u @ x] oo [u ↝ u] ∥ A  oo ([u @ v ↝ t @ y @ v] oo [t' ↝ t'] ∥ [y'' @ v ↝ v @ y'']) oo C"
            by (simp add: comp_assoc par_switch  )
          also have "... = [u ↝ u @ x] oo [u ↝ u] ∥ A  oo [u @ v ↝ t @ v @ y] oo C"
            apply (simp add: switch_par_comp_Subst Subst_append Subst_not_in_a)
            apply (subst Subst_not_in, simp_all)
            using ‹set y'' ∩ set v = {}› by blast
          also have "... = [u ↝ u @ x] oo [u ↝ u] ∥ A  oo ([u @ v ↝ t @ v @ y] oo C)"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ u @ x] oo [u ↝ u] ∥ A oo ([u @ v ↝ s @ v @ z] oo C')"
            by (simp add: eq)
          also have "... = [u ↝ u @ x] oo [u ↝ u] ∥ A oo [u @ v ↝ s @ v @ z] oo C'"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ u @ x] oo [u ↝ u] ∥ A  oo ([u @ v ↝ s @ z @ v] oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z'']) oo C'"
            apply (subst switch_par_comp_Subst, simp_all)
            apply (simp add: Subst_append Subst_not_in_a)
            apply (subst Subst_not_in, simp_all)
            using ‹set z'' ∩ set v = {}› by blast
          also have "... = [u ↝ u @ x] oo ([u ↝ u] ∥ A  oo [u ↝ s @ z] ∥ [v ↝ v]) oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''] oo C'"
            apply (simp add: comp_assoc  )
            by (cut_tac x=u and x'="s@z" and y=v and y'=v in par_switch, simp_all)
          also have "... = [u ↝ u @ x] oo [u ↝ s @ z] ∥ A oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''] oo C'"
            by (simp add: comp_parallel_distrib)
          also have "... = [u ↝ u @ x] oo ([u ↝ s @ z] oo ([s' ↝ s'] ∥ [z'' ↝ z''])) ∥ A oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''] oo C'"
            by (simp add: switch_par_comp_Subst)
          also have "... = [u ↝ u @ x] oo ([u ↝ s @ z] ∥ [x' ↝ x'] oo ([s' ↝ s'] ∥ [z'' ↝ z'']) ∥ A) oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''] oo C'"
            by (subst comp_parallel_distrib, simp_all)
          also have "... = [u ↝ u @ x] oo [u ↝ s @ z] ∥ [x' ↝ x'] oo ([s' ↝ s'] ∥ [z'' ↝ z'']) ∥ A oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''] oo C'"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ u @ x] oo [u @ x' ↝ s @ z @ x'] oo [s' ↝ s'] ∥ ([z'' ↝ z''] ∥ A) oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''] oo C'"
            by (simp add: par_assoc par_switch)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ s @ x' @ z] oo [s' ↝ s'] ∥ [x' @ z'' ↝ z'' @ x']) oo [s' ↝ s'] ∥ ([z'' ↝ z''] ∥ A) oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''] oo C'"
            apply (subst switch_par_comp_Subst, simp_all)
            by (simp add: Subst_append Subst_not_in_a Subst_not_in Int_commute)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ s @ x' @ z] oo ([s' ↝ s'] ∥ [x' @ z'' ↝ z'' @ x'] oo [s' ↝ s'] ∥ ([z'' ↝ z''] ∥ A) oo [s' ↝ s'] ∥ [z'' @ v ↝ v @ z''])) oo C'"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ s @ x' @ z] oo [s' ↝ s'] ∥ ([x' @ z'' ↝ z'' @ x'] oo [z'' ↝ z''] ∥ A oo [z'' @ v ↝ v @ z''])) oo C'"
            by (simp add: comp_parallel_distrib  )
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ s @ x' @ z] oo [s' ↝ s'] ∥ (A ∥ [z'' ↝ z''])) oo C'"
            by (cut_tac T="[z'' ↝ z'']" and S=A and x=x' and y=z'' and u=z'' and v=v in switch_par, simp_all)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ s @ x' @ z] oo [s' ↝ s'] ∥ (A ∥ [z' ↝ z'])) oo C'"
            apply (simp only: z''_def) 
            by (subst switch_newvars, simp_all)
          also have "... = [u ↝ u @ x] oo ([u @ x' ↝ s @ x' @ z] oo [s' ↝ s'] ∥ A ∥ [z' ↝ z']) oo C'"
            by (simp add: par_assoc)
          also have "... = ([u ↝ u @ x] oo [u @ x' ↝ s @ x' @ z]) oo ([s' ↝ s'] ∥ A ∥ [z' ↝ z']) oo C'"
            by (simp add: comp_assoc  )
          also have "... = [u ↝ s @ x @ z] oo ([s' ↝ s'] ∥ A ∥ [z' ↝ z']) oo C'"
            apply (subst switch_comp_subst, simp_all)
            by (simp add: Subst_append Subst_not_in Subst_not_in_a Subst_eq)

          finally show ?thesis
            by simp
        qed

    lemma length_TVs: "length (TVs x) = length x"
        by (induction x, simp_all)

      lemma comp_par: "distinct x ⟹ set y ⊆ set x ⟹ [x ↝ x @ x] oo [x ↝ y] ∥ [x ↝ y] = [x ↝ y @ y]"
        by (subst switch_par_comp_Subst, simp_all add: set_addvars Subst_eq)

      lemma Subst_switch_a: "distinct x ⟹ distinct y ⟹ set z ⊆ set x ⟹ TVs x = TVs y ⟹ [x ↝ z] = [y ↝ Subst x y z]"
        by (metis distinct_id order_refl switch_comp_a switch_comp_subst)

       lemma change_var_names: "distinct a ⟹ distinct b ⟹ TVs a = TVs b ⟹ [a ↝ a @ a] = [b ↝ b @ b]"
         by (simp add: Switch_Split)
           
subsubsection‹Deterministic diagrams›

definition "deterministic S = (Split (TI S) oo S ∥ S = S oo Split (TO S))"
  
lemma deterministic_split:
  assumes "deterministic S"
    and "distinct (a#x)"
    and "TO S = TVs (a # x)"
  shows "S = Split (TI S) oo (S oo [ a # x ↝ [a] ]) ∥ (S oo [ a # x ↝ x ])"
proof -
  have A: "[a # x ↝ (a # x) @ a # x] oo [a # x ↝ [a]] ∥ [a # x ↝ x] = [a # x ↝ a # x]"
    by (metis Switch_Split append_Cons append_Nil assms(2) switch_append)
  have "Split (TI S) oo (S oo [ a # x ↝ [a] ]) ∥ (S oo [ a # x ↝ x ]) = Split (TI S) oo (S ∥ S  oo [ a # x ↝ [a] ] ∥ [ a # x ↝ x ])"
    by (simp add: assms(3) comp_parallel_distrib)
  also have "... = (Split (TI S) oo S ∥ S)  oo [ a # x ↝ [a] ] ∥ [ a # x ↝ x ]"
    by (simp add: assms(3) local.comp_assoc)
  also have "... = (S oo Split (TO S))  oo [ a # x ↝ [a] ] ∥ [ a # x ↝ x ]"
    using assms(1) deterministic_def by auto
  also have "... = S oo (Split (TO S)  oo [ a # x ↝ [a] ] ∥ [ a # x ↝ x ])"
    by (simp add: assms(3) local.comp_assoc)
  also have "... = S oo ([a # x ↝ (a # x) @ (a # x)]  oo [ a # x ↝ [a] ] ∥ [ a # x ↝ x ])"
    using Switch_Split assms(2) assms(3) by presburger
  also have "... = S oo [a # x ↝ a # x]"
    by (subst A, simp)
  also have "... = S"
    using assms(2) assms(3) by auto
  finally show ?thesis by simp
qed

lemma deterministicE: "deterministic A ⟹ distinct x ⟹ distinct y ⟹ TI A = TVs x ⟹ TO A = TVs y 
  ⟹ [x ↝ x @ x] oo (A ∥ A) = A oo [y ↝ y @ y]"
  by (simp add: deterministic_def Switch_Split)

lemma deterministicI: "distinct x ⟹ distinct y ⟹ TI A = TVs x ⟹ TO A = TVs y ⟹ 
  [x ↝ x @ x] oo A ∥ A = A oo [y ↝ y @ y] ⟹ deterministic A"
  by (simp add: deterministic_def Switch_Split)
    
lemma deterministic_switch: "distinct x ⟹ set y ⊆ set x ⟹ deterministic [x ↝ y]"
  by (simp add: deterministic_def switch_dup)


lemma deterministic_comp: "deterministic A ⟹ deterministic B ⟹ TO A = TI B ⟹ deterministic (A oo B)"
proof (simp add: deterministic_def) 
  assume [simp]: "Split (TI A) oo A ∥ A = A oo Split (TI B)"
  assume [simp]: "Split (TI B) oo B ∥ B = B oo Split (TO B)"
  assume [simp]: "TO A = TI B"

  have " A oo B oo Split (TO B) =
            A oo (B oo Split (TO B))"
    by (subst comp_assoc, simp_all)
  also have "... = A oo (Split (TI B) oo B ∥ B)"
    by simp
  also have "... = (A oo Split (TI B)) oo B ∥ B"
    by (subst comp_assoc, simp_all)
  also have "... = (Split (TI A) oo A ∥ A) oo B ∥ B"
    by simp
  also have "... = Split (TI A)  oo (A ∥ A oo B ∥ B)"
    by (subst comp_assoc, simp_all)
  also have "... = Split (TI A) oo (A oo B) ∥ (A oo B)"
    by (simp add: comp_parallel_distrib)
  
  finally show "Split (TI A) oo (A oo B) ∥ (A oo B) =  A oo B oo Split (TO B)"
    by simp
qed

lemma deterministic_par: "deterministic A ⟹ deterministic B ⟹ deterministic (A ∥ B)"
proof (simp add: deterministic_def)            
  assume [simp]: "Split (TI A) oo A ∥ A = A oo Split (TO A)"
  assume [simp]: "Split (TI B) oo B ∥ B = B oo Split (TO B)"

  have [simp]: "Split (TI A) ∥ Split (TI B) oo ID (TI A) ∥ ID (TI A @ TI B) ∥ ID (TI B) = Split (TI A) ∥ Split (TI B)"
    proof -
      have "TO (Split (TI A) ∥ Split (TI B)) = (TI A @ TI A) @ TI B @ TI B"
        by simp
      then show "Split (TI A) ∥ Split (TI B) oo ID (TI A) ∥ ID (TI A @ TI B) ∥ ID (TI B) = Split (TI A) ∥ Split (TI B)"
        by (metis (no_types) append_assoc comp_id_right parallel_ID_sym)
    qed

  have "Split (TI A @ TI B) oo A ∥ B ∥ (A ∥ B) = Split (TI A @ TI B) oo A ∥ (B ∥ A) ∥ B"
    by (simp add: par_assoc)
  also have "... = Split (TI A @ TI B) oo A ∥ (Switch (TI B) (TI A) oo A ∥ B oo Switch (TO A) (TO B)) ∥ B"
    by (subst (2) switch_par_no_vars[THEN sym], simp_all)
  also have "... =  Split (TI A @ TI B) oo ID (TI A) ∥ Switch (TI B) (TI A) ∥ ID (TI B) oo A ∥ (A ∥ B) ∥ B oo  ID (TO A) ∥ Switch (TO A) (TO B) ∥ ID (TO B)"
    by (simp add: comp_assoc comp_parallel_distrib)
  also have "... =  Split (TI A) ∥ Split (TI B) oo (ID (TI A) ∥ Switch (TI A) (TI B) ∥ ID (TI B) oo ID (TI A) ∥ Switch (TI B) (TI A) ∥ ID (TI B)) oo A ∥ (A ∥ B) ∥ B oo  ID (TO A) ∥ Switch (TO A) (TO B) ∥ ID (TO B)"
    by (simp add: Split_append comp_assoc)
  also have "... =  Split (TI A) ∥ Split (TI B) oo  A ∥ (A ∥ B) ∥ B oo  ID (TO A) ∥ Switch (TO A) (TO B) ∥ ID (TO B)"
    by (simp add: comp_parallel_distrib)
  also have "... =  Split (TI A) ∥ Split (TI B) oo  (A ∥ A) ∥ (B ∥ B) oo  ID (TO A) ∥ Switch (TO A) (TO B) ∥ ID (TO B)"
    by (simp add: par_assoc)
  also have "... = A ∥ B oo Split (TO A) ∥ Split (TO B) oo ID (TO A) ∥ Switch (TO A) (TO B) ∥ ID (TO B)"
    by (simp add: comp_parallel_distrib)
  also have "... = A ∥ B oo Split (TO A @ TO B)"
    by (simp add: Split_append comp_assoc)

  finally show "Split (TI A @ TI B) oo A ∥ B ∥ (A ∥ B) =  A ∥ B oo Split (TO A @ TO B)"
    by simp
qed
  
  
end
  
end