# 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]))"
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)
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])"
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"
finally show ?case by simp
qed

lemma swap_power: "(f ^^ n) ((f ^^ m) S) = (f ^^ m) ((f ^^ n) S)"

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]))"
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])"
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)
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]))"
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"

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')"

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]))"
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]))"
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"