Theory ExtendedHBDAlgebra

theory ExtendedHBDAlgebra
imports 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.
 *)

subsection‹Abstract Algebra of  Hierarchical Block Diagrams with All Axioms›

theory ExtendedHBDAlgebra imports HBDAlgebra
begin
  
locale BaseOperation = BaseOperationFeedbackless +
  assumes fb_twice_switch_no_vars: "TI S = t' # t # ts ⟹ TO S = t' # t # ts'
      ⟹ (fb ^^ (2::nat)) (Switch [t] [t'] ∥ ID ts oo S oo Switch [t'] [t] ∥ ID ts') = (fb ^^ (2:: nat)) S"

locale BaseOperationVars = BaseOperation + BaseOperationFeedbacklessVars
begin
lemma fb_twice_switch: "distinct (a # b # x) ⟹ distinct (a # b # y) ⟹ TI S = TVs (b # a # x) ⟹ TO S = TVs (b # a # y) 
      ⟹ (fb ^^ (2::nat)) ([a # b # x ↝ b # a # x] oo S oo [b # a # y ↝ a # b # y]) = (fb ^^ (2:: nat)) S"
  apply (cut_tac S = S  and t = "TV a" and t' = "TV b" and ts = "TVs x" in fb_twice_switch_no_vars, simp_all add: distinct_id sw_hd_var)
  by (subst sw_hd_var, auto)

lemma fb_switch_a: "⋀ S . distinct (a # z @ x) ⟹ distinct (a # z @ y) ⟹ TI S = TVs (z @ a # x) ⟹ TO S = TVs (z @ a # y) 
      ⟹ (fb ^^ (Suc (length z))) ([a # z @ x ↝ z @ a # x] oo S oo [z @ a # y ↝ a # z @ y]) = (fb ^^ (Suc (length z))) S"
proof (induction z)
  case Nil
  from Nil show ?case
    by simp_all
next
        case (Cons b z)

        have "(fb ^^ Suc (length (b # z))) ([a # (b # z) @ x ↝ (b # z) @ a # x] oo S oo [(b # z) @ a # y ↝ a # (b # z) @ y]) 
            = (fb ^^ length z) ((fb ^^ (2::nat)) ([a # b # z @ x ↝ b # z @ a # x] oo S oo [b # z @ a # y ↝ a # b # z @ y]))"
          by (simp add: funpow_swap1 numeral_2_eq_2)
        also have "... = (fb ^^ length z) ((fb ^^ 2) ([b # a # z @ x ↝ a # b # z @ x] oo ([a # b # z @ x ↝ b # z @ a # x] oo S oo [b # z @ a # y ↝ a # b # z @ y]) oo [a # b # z @ y ↝ b # a # z @ y]))"
          using Cons by (subst fb_twice_switch, simp_all, auto)

        also have "... = (fb ^^ length z) ((fb ^^ 2) ([b # a # z @ x ↝ b # z @ a # x] oo S oo [b # z @ a # y ↝ b # a # z @ y]))"
          using Cons(4) Cons(5) apply (simp add: comp_assoc [THEN sym])
          using Cons(2) apply (subst switch_comp_a, auto)
          apply (simp add: comp_assoc)
          using Cons by (subst switch_comp_a, auto)
        also have "... = (fb ^^ length z) ((fb ^^ 2) ([[b] ↝ [b]] ∥ [a # z @ x ↝ z @ a # x] oo S oo [[b] ↝ [b]] ∥ [z @ a # y ↝ a # z @ y]))"
          using Cons by (subst par_switch, auto , subst par_switch, auto)
        also have "... = (fb ^^ length z) (fb (fb ([[b] ↝ [b]] ∥ [a # z @ x ↝ z @ a # x] oo S oo [[b] ↝ [b]] ∥ [z @ a # y ↝ a # z @ y])))"
          by (simp add: numeral_2_eq_2 del: )
        also have "... = (fb ^^ length z) (fb ([a # z @ x ↝ z @ a # x] oo fb S oo  [z @ a # y ↝ a # z @ y]))"
          by (simp add: Cons.prems(3) Cons.prems(4) distinct_id fb_comp)
        also have "... = (fb ^^ Suc (length z)) ([a # z @ x ↝ z @ a # x] oo fb S oo  [z @ a # y ↝ a # z @ y])"
          by (simp add: funpow_add funpow_swap1)
        also have "... = (fb ^^ Suc (length z))  (fb S)"
          using Cons by (subst Cons(1), simp_all add: TI_fb_fbtype TO_fb_fbtype fbtype_def TVs_def)
        also have "... = (fb ^^ Suc (length (a # z))) S"
          by (simp add: funpow_add funpow_swap1)
        finally show ?case by simp
      qed

      lemma swap_power: "(f ^^ n) ((f ^^ m) S) = (f ^^ m) ((f ^^ n) S)"
        by (metis add.left_commute funpow_add funpow_simps_right(1) o_apply o_id)

          
      lemma fb_switch_b: "⋀ v x y S . distinct (u @ v @ x) ⟹ distinct (u @ v @ y) ⟹ TI S = TVs (v @ u @ x) ⟹ TO S = TVs (v @ u @ y) 
      ⟹ (fb ^^ (length (u @ v))) ([u @ v @ x ↝ v @ u @ x] oo S oo [v @ u @ y ↝ u @ v @ y]) = (fb ^^ (length (u @ v))) S"
        proof (induction u)
        case Nil
          show ?case
            using Nil by simp_all
        next
        case (Cons a u)
          have "(fb ^^ length (a # u @ v)) ([a # u @ v @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ a # u @ v @ y])
              =  (fb ^^ length v) ((fb ^^ (Suc (length u)))([a # u @ v @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ a # u @ v @ y]))"
            apply (simp add: funpow_add funpow_swap1)
            by (rule swap_power)
          also have "... = (fb ^^ length v) ((fb ^^ (Suc (length u))) (
            [a # u @ v @ x ↝ u @ a # v @ x] oo ([u @ a # v @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ u @ a # v @ y]) oo [u @ a # v @ y ↝ a # u @ v @ y]))"
            using Cons apply (simp add: comp_assoc switch_comp_a)
              
            apply (subst switch_comp_a)
                apply simp_all
              apply blast
             apply blast
             apply (simp add: comp_assoc [THEN sym])
            by (subst switch_comp_a, auto)

          also have "... = (fb ^^ length v) ((fb ^^ Suc (length u)) ([u @ a # v @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ u @ a # v @ y]))"
            using Cons by (subst fb_switch_a, simp_all)

          also have "... = (fb ^^ (length (u @ (a # v)))) ([u @ a # v @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ u @ a # v @ y])"
            apply (simp add: funpow_add funpow_swap1)
            by (rule swap_power)
          also have "... =  (fb ^^ (length (u @ (a # v)))) ([u @ (a # v) @ x ↝ (a # v) @ u @ x] 
              oo ([(a # v) @ u @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ (a # v) @ u @ y])
              oo [(a # v) @ u @ y ↝ u @ (a # v) @ y])"
            using Cons(4) Cons(5)
            apply (simp add: comp_assoc)
            using Cons(3) apply (subst switch_comp_a, simp_all)
               apply blast
              apply blast
              apply blast
            apply (simp add: comp_assoc [THEN sym])
            using Cons(2) by (subst switch_comp_a, simp_all, auto)

          also have "... = (fb ^^ length (u @ a # v)) ([a # v @ u @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ a # v @ u @ y])"
            using Cons by (subst Cons(1), simp_all)
          also have "... = (fb ^^ length u) (((fb ^^ (Suc (length v)))) ([a # v @ u @ x ↝ v @ a # u @ x] oo S oo [v @ a # u @ y ↝ a # v @ u @ y]))"
            by (simp add: funpow_add funpow_swap1)
          also have "... =  (fb ^^ length u) ((fb ^^ Suc (length v)) S)"
            using Cons by (subst fb_switch_a, simp_all, blast, blast)
          also have "... = (fb ^^ length ((a # u) @ v)) S"
            by (simp add: funpow_add funpow_swap1)
 
          finally show ?case
            by simp
        qed
          
    theorem fb_perm: "⋀ v S . perm u v ⟹ distinct (u @ x) ⟹ distinct (u @ y) ⟹ fbtype S (TVs u) (TVs x) (TVs y) 
        ⟹ (fb ^^ (length u)) ([v @ x ↝ u @ x] oo S oo [u @ y ↝ v @ y]) = (fb ^^ (length u)) S"
      proof (induction u)
        case Nil
          show ?case
            using Nil by (simp add: fbtype_def TVs_def)
        next
        case (Cons a u)
          from ‹perm (a # u) v› obtain w w' where "v = w @ a # w'" and [simp]: "perm u (w @ w')"
            by (simp add: split_perm, blast)

          have [simp]: "length u = length w + length w'"
            by (metis perm_length ‹u <~~> w @ w'› length_append)

          have [simp]: "set u = set w ∪ set w'"
            by (metis Permutation.perm_set_eq ‹u <~~> w @ w'› set_append)

          have [simp]: "distinct w" and [simp]:"distinct w'"
            apply (meson Cons.prems(3) ‹perm u (w @ w')› dist_perm distinct.simps(2) distinct_append)
            by (meson Cons.prems(3) ‹perm u (w @ w')› dist_perm distinct.simps(2) distinct_append)

          have A: "set w ∩ set w' = {}"
            by (meson Cons.prems(3) ‹perm u (w @ w')› dist_perm distinct.simps(2) distinct_append)

          have "(fb ^^ length (a # u)) ([v @ x ↝ a # u @ x] oo S oo [a # u @ y ↝ v @ y]) 
            = (fb ^^ length w') ((fb ^^ (length (w @ [a]))) ([w @ a # w' @ x ↝ a # u @ x] oo S oo [a # u @ y ↝ w @ a # w' @ y]))"
            apply (simp add: funpow_add funpow_swap1)
            using ‹v = w @ a # w'› swap_power by fastforce
          thm fb_switch_a
          thm fb_switch_b
          thm fbtype_def
          also have "... = (fb ^^ length w') ((fb ^^ (length (w @ [a]))) ([w @ [a] @ w' @ x ↝ [a] @ w @ w' @ x] 
              oo ([[a] @ w @ w' @ x ↝ a # u @ x] oo S oo [a # u @ y ↝[a] @ w @ w' @ y])
              oo [[a] @ w @ w' @ y ↝ w @ [a] @ w' @ y]))"
            using A Cons apply (simp add: comp_assoc fbtype_def )
            apply (subst switch_comp_a, auto)
            apply (simp add: comp_assoc [THEN sym] )
       
            by (subst switch_comp_a, auto)
          also have "... = (fb ^^ length w') ((fb ^^ length (w @ [a])) ([a # w @ w' @ x ↝ a # u @ x] oo S oo [a # u @ y ↝ a # w @ w' @ y]))"
            
            using A Cons apply (subst fb_switch_b, simp_all add: fbtype_def)
            apply blast
            by blast

          also have "... = (fb ^^ length u) (fb ([a # w @ w' @ x ↝ a # u @ x] oo S oo [a # u @ y ↝ a # w @ w' @ y]))"
            apply (simp add: funpow_add funpow_swap1)
            using ‹v = w @ a # w'› swap_power by fastforce
          also have "... = (fb ^^ length u) (fb ([[a] ↝ [a]] ∥ [w @ w' @ x ↝ u @ x] oo S oo [[a] ↝ [a]] ∥ [u @ y ↝ w @ w' @ y]))"
            using A Cons 
            apply (subst par_switch, simp_all add: fbtype_def TVs_def)
            apply blast
              apply blast
            apply (subst par_switch)
               apply simp_all
              by blast
          also have "... = (fb ^^ length u) ([(w @ w') @ x ↝ u @ x] oo fb S oo [u @ y ↝ (w @ w') @ y])"
            using Cons apply simp
            
            by (simp add: distinct_id fb_comp fbtype_def)
 
          also have "... = (fb ^^ length u) (fb S)"
            using A Cons by (subst Cons(1), simp_all add: fbtype_def TI_fb_fbtype TO_fb_fbtype)

          also have "... = (fb ^^ length (a # u)) S"
            by (simp add: funpow_add funpow_swap1)
          finally show ?case
            by (simp)
        qed
end
end