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