# Theory Prime_Transformation

```section ‹Transformation to Language-Equivalent Prime FSMs›

text ‹This theory describes the transformation of FSMs into language-equivalent FSMs
that are prime, that is: observable, minimal and initially connected.›

theory Prime_Transformation
imports Minimisation Observability State_Cover OFSM_Tables_Refined "HOL-Library.List_Lexorder" Native_Word.Uint64
begin

subsection ‹Helper Functions›

text ‹The following functions transform FSMs whose states are Sets or FSets into
language-equivalent fsms whose states are lists.
These steps are required in the chosen implementation of the transformation function,
as Sets or FSets are not instances of linorder.›

lemma linorder_fset_list_bij : "bij_betw sorted_list_of_fset xs (sorted_list_of_fset ` xs)"
unfolding bij_betw_def inj_on_def
by (metis sorted_list_of_fset_simps(2))

lemma linorder_set_list_bij :
assumes "⋀ x . x ∈ xs ⟹ finite x"
shows "bij_betw sorted_list_of_set xs (sorted_list_of_set ` xs)"
proof -
have "⋀ x . x ∈ xs ⟹ set (sorted_list_of_set x) = x"
then show ?thesis
unfolding bij_betw_def inj_on_def
by metis
qed

definition fset_states_to_list_states :: "(('a::linorder) fset,'b,'c) fsm ⇒ ('a list,'b,'c) fsm" where
"fset_states_to_list_states M = rename_states M sorted_list_of_fset"

definition set_states_to_list_states :: "(('a::linorder) set,'b,'c) fsm ⇒ ('a list,'b,'c) fsm" where
"set_states_to_list_states M = rename_states M sorted_list_of_set"

lemma fset_states_to_list_states_language :
"L (fset_states_to_list_states M) = L M"
using rename_states_isomorphism_language[OF linorder_fset_list_bij]
unfolding fset_states_to_list_states_def .

lemma set_states_to_list_states_language :
assumes "⋀ x . x ∈ states M ⟹ finite x"
shows "L (set_states_to_list_states M) = L M"
using rename_states_isomorphism_language[OF linorder_set_list_bij[OF assms]]
unfolding set_states_to_list_states_def .

lemma fset_states_to_list_states_observable :
assumes "observable M"
shows "observable (fset_states_to_list_states M)"
using rename_states_observable[OF linorder_fset_list_bij assms]
unfolding fset_states_to_list_states_def .

lemma set_states_to_list_states_observable :
assumes "⋀ x . x ∈ states M ⟹ finite x"
assumes "observable M"
shows "observable (set_states_to_list_states M)"
using rename_states_observable[OF linorder_set_list_bij[OF assms(1)] assms(2)]
unfolding set_states_to_list_states_def by blast

lemma fset_states_to_list_states_minimal :
assumes "minimal M"
shows "minimal (fset_states_to_list_states M)"
using rename_states_minimal[OF linorder_fset_list_bij assms]
unfolding fset_states_to_list_states_def .

lemma set_states_to_list_states_minimal :
assumes "⋀ x . x ∈ states M ⟹ finite x"
assumes "minimal M"
shows "minimal (set_states_to_list_states M)"
using rename_states_minimal[OF linorder_set_list_bij[OF assms(1)] assms(2)]
unfolding set_states_to_list_states_def by blast

subsection ‹The Transformation Algorithm›

definition to_prime :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm ⇒ (integer,'b,'c) fsm" where
"to_prime M = restrict_to_reachable_states (
index_states_integer (
set_states_to_list_states (
minimise_refined (
index_states (
fset_states_to_list_states (
make_observable (
restrict_to_reachable_states M)))))))"

lemma to_prime_props :
"L (to_prime M) = L M"
"observable (to_prime M)"
"minimal (to_prime M)"
"reachable_states (to_prime M) = states (to_prime M)"
"inputs (to_prime M) = inputs M"
"outputs (to_prime M) = outputs M"
proof -

define M1 where M1: "M1 = restrict_to_reachable_states M"
define M2 where M2: "M2 = make_observable M1"
define M3 where M3: "M3 = fset_states_to_list_states M2"
define M4 where M4: "M4 = index_states M3"
define M5 where M5: "M5 = minimise_refined M4"
define M6 where M6: "M6 = set_states_to_list_states M5"
define M7 where M7: "M7 = index_states_integer M6"
define M8 where M8: "M8 = restrict_to_reachable_states M7"

have "to_prime M = M8"
unfolding M8 M7 M6 M5 M4 M3 M2 M1 to_prime_def by presburger

have "observable M2"
unfolding M2
using make_observable_language_observable(2) by blast
then have "observable M3"
unfolding M3
using fset_states_to_list_states_observable by blast
then have "observable M4"
unfolding M4
using index_states_observable by blast
then have "observable M5"
unfolding M5
unfolding minimise_refined_is_minimise[symmetric]
using minimise_observable by blast
then have "observable M6"
unfolding M6 M5
unfolding minimise_refined_is_minimise[symmetric]
using minimise_states_finite[OF ‹observable M4›]
using set_states_to_list_states_observable
by metis
then have "observable M7"
unfolding M7
using index_states_integer_observable by blast
then show "observable (to_prime M)"
unfolding ‹to_prime M = M8› M8
using restrict_to_reachable_states_observable by blast

have "L M = L M1"
unfolding M1 restrict_to_reachable_states_language by simp
also have "… = L M2"
unfolding M2 make_observable_language_observable(1) by simp
also have "… = L M3"
unfolding M3 fset_states_to_list_states_language by simp
also have "… = L M4"
unfolding M4 index_states_language by simp
also have "… = L M5"
unfolding M5 unfolding minimise_refined_is_minimise[symmetric]
using minimise_language[OF ‹observable M4›] by blast
also have "… = L M6"
unfolding M6 M5 unfolding minimise_refined_is_minimise[symmetric]
using set_states_to_list_states_language[OF minimise_states_finite[OF ‹observable M4›]] by blast
also have "… = L M7"
unfolding M7 using index_states_integer_language by blast
also have "… = L M8"
unfolding M8 restrict_to_reachable_states_language by simp
finally show "L (to_prime M) = L M"
unfolding ‹to_prime M = M8› by blast

have "minimal M5"
unfolding M5 unfolding minimise_refined_is_minimise[symmetric]
using minimise_minimal[OF ‹observable M4›] .
then have "minimal M6"
unfolding M6 M5 unfolding minimise_refined_is_minimise[symmetric]
using set_states_to_list_states_minimal[OF minimise_states_finite[OF ‹observable M4›]] by blast
then have "minimal M7"
unfolding M7 using index_states_integer_minimal by blast
then show "minimal (to_prime M)"
unfolding ‹to_prime M = M8› M8
using restrict_to_reachable_states_minimal by blast

show "reachable_states (to_prime M) = states (to_prime M)"
unfolding ‹to_prime M = M8› M8 restrict_to_reachable_states_reachable_states by presburger

have "inputs M = inputs M1"
unfolding M1 restrict_to_reachable_states_simps by simp
also have "… = inputs M2"
unfolding M2 make_observable_language_observable Let_def add_transitions_simps create_unconnected_fsm_simps by blast
also have "… = inputs M3"
unfolding M3 fset_states_to_list_states_def by simp
also have "… = inputs M4"
unfolding M4 index_states.simps by simp
also have "… = inputs M5"
unfolding M5 unfolding minimise_refined_is_minimise[symmetric]
using minimise_props[OF ‹observable M4›] by blast
also have "… = inputs M6"
unfolding M6 M5 set_states_to_list_states_def by simp
also have "… = inputs M7"
unfolding M7 index_states.simps by simp
also have "… = inputs M8"
unfolding M8 restrict_to_reachable_states_simps by simp
finally show "inputs (to_prime M) = inputs M"
unfolding ‹to_prime M = M8› by blast

have "outputs M = outputs M1"
unfolding M1 restrict_to_reachable_states_simps by simp
also have "… = outputs M2"
unfolding M2 make_observable_language_observable Let_def add_transitions_simps create_unconnected_fsm_simps by blast
also have "… = outputs M3"
unfolding M3 fset_states_to_list_states_def by simp
also have "… = outputs M4"
unfolding M4 index_states.simps by simp
also have "… = outputs M5"
unfolding M5 unfolding minimise_refined_is_minimise[symmetric]
using minimise_props[OF ‹observable M4›] by blast
also have "… = outputs M6"
unfolding M6 M5 set_states_to_list_states_def by simp
also have "… = outputs M7"
unfolding M7 index_states.simps by simp
also have "… = outputs M8"
unfolding M8 restrict_to_reachable_states_simps by simp
finally show "outputs (to_prime M) = outputs M"
unfolding ‹to_prime M = M8› by blast
qed

subsection ‹Renaming states to Words›

lemma uint64_nat_bij : "(x :: nat) < 2^64 ⟹ nat_of_uint64 (uint64_of_nat x) = x"
by transfer (simp add: unsigned_of_nat take_bit_nat_eq_self)

fun index_states_uint64 :: "('a::linorder,'b,'c) fsm ⇒ (uint64,'b,'c) fsm" where
"index_states_uint64 M = rename_states M (uint64_of_nat ∘ assign_indices (states M))"

lemma assign_indices_uint64_bij_betw :
assumes "size M < 2^64"
shows "bij_betw (uint64_of_nat ∘ assign_indices (states M)) (FSM.states M) ((uint64_of_nat ∘ assign_indices (states M)) ` FSM.states M)"
proof -
have *: "inj_on (assign_indices (FSM.states M)) (FSM.states M)"
using assign_indices_bij[OF fsm_states_finite[of M]]
unfolding bij_betw_def
by auto
moreover have "⋀ q . q ∈ states M ⟹ assign_indices (states M) q < 2^64"
using assms assign_indices_bij[OF fsm_states_finite[of M]]
unfolding size_def
by (meson bij_betwE lessThan_iff less_imp_le less_le_trans)
ultimately have "inj_on (uint64_of_nat ∘ assign_indices (states M)) (FSM.states M)"
unfolding inj_on_def
by (metis comp_apply uint64_nat_bij)
then show ?thesis
unfolding bij_betw_def
by auto
qed

lemma index_states_uint64_language :
assumes "size M < 2^64"
shows  "L (index_states_uint64 M) = L M"
using rename_states_isomorphism_language[of "uint64_of_nat ∘ assign_indices (states M)" M, OF assign_indices_uint64_bij_betw[OF assms]]
by auto

lemma index_states_uint64_observable :
assumes "size M < 2^64" and "observable M"
shows "observable (index_states_uint64 M)"
using rename_states_observable[of "uint64_of_nat ∘ assign_indices (states M)" M, OF assign_indices_uint64_bij_betw[OF assms(1)] assms(2)]
unfolding index_states_uint64.simps .

lemma index_states_uint64_minimal :
assumes "size M < 2^64" and "minimal M"
shows "minimal (index_states_uint64 M)"
using rename_states_minimal[of "uint64_of_nat ∘ assign_indices (states M)" M, OF assign_indices_uint64_bij_betw[OF assms(1)] assms(2)]
unfolding index_states_uint64.simps .

(* TODO: remove superfluous restriction to reachable states *)
definition to_prime_uint64 :: "('a :: linorder,'b :: linorder,'c :: linorder) fsm ⇒ (uint64,'b,'c) fsm" where
"to_prime_uint64 M = restrict_to_reachable_states (index_states_uint64 (to_prime M))"

lemma to_prime_uint64_props :
assumes "size (to_prime M) < 2^64"
shows
"L (to_prime_uint64 M) = L M"
"observable (to_prime_uint64 M)"
"minimal (to_prime_uint64 M)"
"reachable_states (to_prime_uint64 M) = states (to_prime_uint64 M)"
"inputs (to_prime_uint64 M) = inputs M"
"outputs (to_prime_uint64 M) = outputs M"
using restrict_to_reachable_states_reachable_states[of "index_states_uint64 (to_prime M)"]
unfolding to_prime_uint64_def
using index_states_uint64_language[OF assms]
unfolding restrict_to_reachable_states_language
using restrict_to_reachable_states_observable[OF index_states_uint64_observable[OF assms to_prime_props(2)]]
using restrict_to_reachable_states_minimal[OF index_states_uint64_minimal[OF assms to_prime_props(3)]]
unfolding index_states_uint64.simps
unfolding restrict_to_reachable_states_simps
unfolding rename_states_simps(3,4)
unfolding to_prime_props(1,5,6)
by blast+

end ```