Theory Nominal_Myhill_Nerode
section ‹
Myhill-Nerode Theorem for $G$-automata
›
text ‹
We prove the Myhill-Nerode Theorem for $G$-automata / nominal $G$-automata
following the proofs from \cite{bojanczyk2014automata} (The standard Myhill-Nerode theorem is also
proved, as a special case of the $G$-Myhill-Nerode theorem).
Concretely, we formalize the following results from \cite{bojanczyk2014automata}:
lemmas: 3.4, 3.5, 3.6, 3.7, 4.8, 4.9;
proposition: 5.1;
theorems: 3.8 (Myhill-Nerode for $G$-automata), 5.2 (Myhill-Nerode for nominal $G$-automata).
Throughout this document, we maintain the following convention for isar proofs:
If we \texttt{obtain} some term \texttt{t} for which some result holds, we name it \texttt{H\_t}.
An assumption which is an induction hypothesis is named \texttt{A\_IH}
Assumptions start with an "\texttt{A}" and intermediate results start with a "\texttt{H}".
Typically we just name them via indexes, i.e. as \texttt{A\_i} and \texttt{H\_j}.
When encountering nested isar proofs we add an index for how nested the assumption / intermediate
result is.
For example if we have an isar proof in an isar proof in an isar proof, we would name assumptions
of the most nested proof \texttt{A3\_i}.
›
theory Nominal_Myhill_Nerode
imports
Main
HOL.Groups
HOL.Relation
HOL.Fun
"HOL-Algebra.Group_Action"
"HOL-Library.Adhoc_Overloading"
"HOL-Algebra.Elementary_Groups"
begin
text ‹
\texttt{GMN\_simps} will contain selection of lemmas / definitions is updated through out
the document.
›
named_theorems GMN_simps
lemmas GMN_simps
text ‹
We will use the $\star$-symbol for the set of words of elements of a set, $A^{\star}$, the induced
group action on the set of words $\phi^{\star}$ and for the extended transition function
$\delta^{\star}$, thus we introduce the map \texttt{star} and apply \texttt{adhoc\_overloading} to
get the notation working in all three situations:
›
consts star :: "'typ1 ⇒ 'typ2" ("_⇧⋆" [1000] 999)
adhoc_overloading
star lists
text ‹
We use $\odot$ to convert between the definition of group actions via group homomoprhisms
and the more standard infix group action notation.
We deviate from \cite{bojanczyk2014automata} in that we consider left group actions,
rather than right group actions:
›
definition
make_op :: "('grp ⇒ 'X ⇒ 'X) ⇒ 'grp ⇒ 'X ⇒ 'X" (infixl "(⊙ı)" 70)
where " (⊙ ⇘φ⇙) ≡ (λg. (λx. φ g x))"
lemmas make_op_def [simp, GMN_simps]
subsection ‹
Extending Group Actions
›
text ‹
The following lemma is used for a proof in the locale \texttt{alt\_grp\_act}:
›
lemma pre_image_lemma:
"⟦S ⊆ T; x ∈ T ∧ f ∈ Bij T; (restrict f S) ` S = S; f x ∈ S⟧ ⟹ x ∈ S"
apply (clarsimp simp add: extensional_def subset_eq Bij_def bij_betw_def restrict_def inj_on_def)
by (metis imageE)
text ‹
The locale \texttt{alt\_grp\_act} is just a renaming of the locale \texttt{group\_action}.
This was done to obtain more easy to interpret type names and context variables closer
to the notation of \cite{bojanczyk2014automata}:
›
locale alt_grp_act = group_action G X φ
for
G :: "('grp, 'b) monoid_scheme" and
X :: "'X set" (structure) and
φ
begin
lemma alt_grp_act_is_left_grp_act:
shows "x ∈ X ⟹ 𝟭⇘G⇙ ⊙⇘φ⇙ x = x" and
"g ∈ carrier G ⟹ h ∈ carrier G ⟹ x ∈ X ⟹ (g ⊗⇘G⇙ h) ⊙⇘φ⇙ x = g ⊙⇘φ⇙ (h ⊙⇘φ⇙ x)"
proof-
assume
A_0: "x ∈ X"
show "𝟭⇘G⇙ ⊙⇘φ⇙ x = x"
using group_action_axioms
apply (simp add: group_action_def BijGroup_def)
by (metis A_0 id_eq_one restrict_apply')
next
assume
A_0: "g ∈ carrier G" and
A_1: "h ∈ carrier G" and
A_2: "x ∈ X"
show "g ⊗⇘G⇙ h ⊙⇘φ⇙ x = g ⊙⇘φ⇙ (h ⊙⇘φ⇙ x)"
using group_action_axioms
apply (simp add: group_action_def group_hom_def group_hom_axioms_def hom_def BijGroup_def)
using composition_rule A_0 A_1 A_2
by auto
qed
definition
induced_star_map :: "('grp ⇒ 'X ⇒'X) ⇒ 'grp ⇒ 'X list ⇒ 'X list"
where "induced_star_map func = (λg∈carrier G. (λlst ∈ X⇧⋆. map (func g) lst))"
text ‹
Because the adhoc overloading is used within a locale, isues will be encountered later due to there
being multiple instances of the locale \texttt{alt\_grp\_act} in a single context:
›
adhoc_overloading
star induced_star_map
definition
induced_quot_map ::
"'Y set ⇒ ('grp ⇒ 'Y ⇒ 'Y) ⇒ ('Y ×'Y) set ⇒ 'grp ⇒ 'Y set ⇒ 'Y set" ("[_]⇩_ı" 60)
where "([ func ]⇩R ⇘S⇙) = (λg∈carrier G. (λx ∈ (S // R). R `` {(func g) (SOME z. z∈x)}))"
lemmas induced_star_map_def [simp, GMN_simps]
induced_quot_map_def [simp, GMN_simps]
lemma act_maps_n_distrib:
"∀g∈carrier G. ∀w∈X⇧⋆. ∀v∈X⇧⋆. (φ⇧⋆) g (w @ v) = ((φ⇧⋆) g w) @ ((φ⇧⋆) g v)"
by (auto simp add: group_action_def group_hom_def group_hom_axioms_def hom_def)
lemma triv_act:
"a ∈ X ⟹ (φ 𝟭⇘G⇙) a = a"
using group_hom.hom_one[of "G" "BijGroup X" "φ"] group_BijGroup[where S = "X"]
apply (clarsimp simp add: group_action_def group_hom_def group_hom_axioms_def BijGroup_def)
by (metis id_eq_one restrict_apply')
lemma triv_act_map:
"∀w∈X⇧⋆. ((φ⇧⋆) 𝟭⇘G⇙) w = w"
using triv_act
apply clarsimp
apply (rule conjI; rule impI)
apply clarify
using map_idI
apply metis
using group.subgroup_self group_hom group_hom.axioms(1) subgroup.one_closed
by blast
proposition lists_a_Gset:
"alt_grp_act G (X⇧⋆) (φ⇧⋆)"
proof-
have H_0: "⋀g. g ∈ carrier G ⟹
restrict (map (φ g)) (X⇧⋆) ∈ carrier (BijGroup (X⇧⋆))"
proof-
fix g
assume
A1_0: "g ∈ carrier G"
from A1_0 have H1_0: "inj_on (λx. if x ∈ X⇧⋆ then map (φ g) x else undefined) (X⇧⋆)"
apply (clarsimp simp add: inj_on_def)
by (metis (mono_tags, lifting) inj_onD inj_prop list.inj_map_strong)
from A1_0 have H1_1: "⋀y z. ∀x∈set y. x ∈ X ⟹ z ∈ set y ⟹ φ g z ∈ X"
using element_image
by blast
have H1_2: "(inv ⇘G⇙ g) ∈ carrier G"
by (meson A1_0 group.inv_closed group_hom group_hom.axioms(1))
have H1_3: "⋀x. x ∈ X⇧⋆ ⟹
map (comp (φ g) (φ (inv ⇘G⇙ g))) x = map (φ (g ⊗⇘G⇙ (inv ⇘G⇙ g))) x"
using alt_grp_act_axioms
apply (simp add: alt_grp_act_def group_action_def group_hom_def group_hom_axioms_def hom_def
BijGroup_def)
apply (rule meta_mp[of "⋀x. x ∈ carrier G ⟹ φ x ∈ Bij X"])
apply (metis A1_0 H1_2 composition_rule in_lists_conv_set)
by blast
from H1_2 have H1_4: "⋀x. x ∈ X⇧⋆ ⟹ map (φ (inv ⇘G⇙ g)) x ∈ X⇧⋆"
using surj_prop
by fastforce
have H1_5: "⋀y. ∀x∈set y. x ∈ X ⟹ y ∈ map (φ g) ` X⇧⋆"
apply (simp add: image_def)
using H1_3 H1_4
by (metis A1_0 group.r_inv group_hom group_hom.axioms(1) in_lists_conv_set map_idI map_map
triv_act)
show "restrict (map (φ g)) (X⇧⋆) ∈ carrier (BijGroup (X⇧⋆))"
apply (clarsimp simp add: restrict_def BijGroup_def Bij_def
extensional_def bij_betw_def)
apply (rule conjI)
using H1_0
apply simp
using H1_1 H1_5
by (auto simp add: image_def)
qed
have H_1: "⋀x y. ⟦x ∈ carrier G; y ∈ carrier G; x ⊗⇘G⇙ y ∈ carrier G⟧ ⟹
restrict (map (φ (x ⊗⇘G⇙ y))) (X⇧⋆) =
restrict (map (φ x)) (X⇧⋆) ⊗⇘BijGroup (X⇧⋆)⇙
restrict (map (φ y)) (X⇧⋆)"
proof-
fix x y
assume
A1_0: "x ∈ carrier G" and
A1_1: " y ∈ carrier G" and
A1_2: "x ⊗⇘G⇙ y ∈ carrier G"
have H1_0: "⋀z. z ∈ carrier G ⟹
bij_betw (λx. if x ∈ X⇧⋆ then map (φ z) x else undefined) (X⇧⋆) (X⇧⋆)"
using ‹⋀g. g ∈ carrier G ⟹ restrict (map (φ g)) (X⇧⋆) ∈ carrier (BijGroup (X⇧⋆))›
by (auto simp add: BijGroup_def Bij_def bij_betw_def inj_on_def)
from A1_1 have H1_1: "⋀lst. lst ∈ X⇧⋆ ⟹ (map (φ y)) lst ∈ X⇧⋆"
by (metis group_action.surj_prop group_action_axioms lists_image rev_image_eqI)
have H1_2: "⋀a. a ∈ X⇧⋆ ⟹ map (λxb.
if xb ∈ X
then φ x ((φ y) xb)
else undefined) a = map (φ x) (map (φ y) a)"
by auto
have H1_3: "(λxa. if xa ∈ X⇧⋆ then map (φ (x ⊗⇘G⇙ y)) xa else undefined) =
compose (X⇧⋆) (λxa. if xa ∈ X⇧⋆ then map (φ x) xa else undefined)
(λx. if x ∈ X⇧⋆ then map (φ y) x else undefined)"
using alt_grp_act_axioms
apply (clarsimp simp add: compose_def alt_grp_act_def group_action_def
group_hom_def group_hom_axioms_def hom_def BijGroup_def restrict_def)
using A1_0 A1_1 H1_2 H1_1 bij_prop0
by auto
show "restrict (map (φ (x ⊗⇘G⇙ y))) (X⇧⋆) =
restrict (map (φ x)) (X⇧⋆) ⊗⇘BijGroup (X⇧⋆)⇙
restrict (map (φ y)) (X⇧⋆)"
apply (clarsimp simp add: restrict_def BijGroup_def Bij_def extensional_def)
apply (simp add: H1_3)
using A1_0 A1_1 H1_0
by auto
qed
show "alt_grp_act G (X⇧⋆) (φ⇧⋆)"
apply (clarsimp simp add: alt_grp_act_def group_action_def group_hom_def group_hom_axioms_def)
apply (intro conjI)
using group_hom group_hom_def
apply (auto)[1]
apply (simp add: group_BijGroup)
apply (clarsimp simp add: hom_def)
apply (intro conjI; clarify)
apply (rule H_0)
apply simp
apply (rule conjI; rule impI)
apply (rule H_1)
apply simp+
apply (rule meta_mp[of "⋀x y. x ∈ carrier G ⟹
y ∈ carrier G ⟹ x ⊗⇘G⇙ y ∈ carrier G"])
apply blast
by (meson group.subgroup_self group_hom group_hom.axioms(1) subgroup.m_closed)
qed
end
lemma alt_group_act_is_grp_act [simp, GMN_simps]:
"alt_grp_act = group_action"
using alt_grp_act_def
by blast
lemma prod_group_act:
assumes
grp_act_A: "alt_grp_act G A φ" and
grp_act_B: "alt_grp_act G B ψ"
shows "alt_grp_act G (A×B) (λg∈carrier G. λ(a, b) ∈ (A × B). (φ g a, ψ g b))"
apply (simp add: alt_grp_act_def group_action_def group_hom_def)
apply (intro conjI)
subgoal
using grp_act_A grp_act_B
by (auto simp add: alt_grp_act_def group_action_def group_hom_def)
subgoal
using grp_act_A grp_act_B
by (auto simp add: alt_grp_act_def group_action_def group_hom_def group_BijGroup)
apply (clarsimp simp add: group_hom_axioms_def hom_def BijGroup_def)
apply (intro conjI; clarify)
subgoal for g
apply (clarsimp simp add: Bij_def bij_betw_def inj_on_def restrict_def extensional_def)
apply (intro conjI)
using grp_act_A
apply (simp add: alt_grp_act_def group_action_def group_hom_def group_hom_axioms_def
BijGroup_def hom_def Pi_def compose_def Bij_def bij_betw_def inj_on_def)
using grp_act_B
apply (simp add: alt_grp_act_def group_action_def group_hom_def group_hom_axioms_def
BijGroup_def hom_def Pi_def compose_def Bij_def bij_betw_def inj_on_def)
apply (rule meta_mp[of "φ g ∈ Bij A ∧ ψ g ∈ Bij B"])
apply (clarsimp simp add: Bij_def bij_betw_def)
using grp_act_A grp_act_B
apply (simp add: alt_grp_act_def group_action_def group_hom_def group_hom_axioms_def
BijGroup_def hom_def Pi_def Bij_def)
using grp_act_A grp_act_B
apply (clarsimp simp add: compose_def restrict_def image_def alt_grp_act_def
group_action_def group_hom_def group_hom_axioms_def BijGroup_def hom_def Pi_def Bij_def
bij_betw_def)
apply (rule subset_antisym)
apply blast+
by (metis alt_group_act_is_grp_act group_action.bij_prop0 grp_act_A grp_act_B)
apply (intro conjI; intro impI)
apply (clarify)
apply (intro conjI; intro impI)
apply (rule conjI)
subgoal for x y
apply unfold_locales
apply (clarsimp simp add: Bij_def compose_def restrict_def bij_betw_def)
apply (rule extensionalityI[where A = "A × B"])
apply (clarsimp simp add: extensional_def)
using grp_act_A grp_act_B
apply (simp add: alt_grp_act_def group_action_def group_hom_def group_hom_axioms_def
BijGroup_def hom_def Pi_def Bij_def compose_def extensional_def)
apply (simp add: fun_eq_iff; rule conjI; rule impI)
using group_action.composition_rule[of G A φ] group_action.composition_rule[of G B ψ] grp_act_A
grp_act_B
apply force
by blast
apply (simp add: ‹⋀g. g ∈ carrier G ⟹ (λ(a, b)∈A × B. (φ g a, ψ g b)) ∈ Bij (A × B)›)
apply (simp add: ‹Group.group G› group.subgroup_self subgroup.m_closed)
by (simp add: ‹⋀g. g ∈ carrier G ⟹ (λ(a, b)∈A × B. (φ g a, ψ g b)) ∈ Bij (A × B)›)+
subsection ‹
Equivariance and Quotient Actions
›
locale eq_var_subset = alt_grp_act G X φ
for
G :: "('grp, 'b) monoid_scheme" and
X :: "'X set" (structure) and
φ +
fixes
Y
assumes
is_subset: "Y ⊆ X" and
is_equivar: "∀g∈carrier G. (φ g) ` Y = Y"
lemma (in alt_grp_act) eq_var_one_direction:
"⋀Y. Y ⊆ X ⟹ ∀g∈carrier G. (φ g) ` Y ⊆ Y ⟹ eq_var_subset G X φ Y"
proof-
fix Y
assume
A_0: "Y ⊆ X" and
A_1: "∀g∈carrier G. (φ g) ` Y ⊆ Y"
have H_0: "⋀g. g ∈ carrier G ⟹ (inv⇘G⇙ g) ∈ carrier G"
by (meson group.inv_closed group_hom group_hom.axioms(1))
hence H_1: "⋀g y. g ∈ carrier G ⟹ y ∈ Y ⟹ (φ (inv⇘G⇙ g)) y ∈ Y"
using A_1
by (simp add: image_subset_iff)
have H_2: "⋀g y. g ∈ carrier G ⟹ y ∈ Y ⟹ φ g ((φ (inv⇘G⇙ g)) y) = y"
by (metis A_0 bij_prop1 orbit_sym_aux subsetD)
show "eq_var_subset G X φ Y"
apply (simp add: eq_var_subset_def eq_var_subset_axioms_def)
apply (intro conjI)
apply (simp add: group_action_axioms)
apply (rule A_0)
apply (clarify)
apply (rule subset_antisym)
using A_1
apply simp
apply (simp add: image_def)
apply (rule subsetI)
apply clarify
using H_1 H_2
by metis
qed
text ‹
The following lemmas are used for proofs in the locale \texttt{eq\_var\_rel}:
›
lemma some_equiv_class_id:
"⟦equiv X R; w ∈ X // R; x ∈ w⟧ ⟹ R `` {x} = R `` {SOME z. z ∈ w}"
by (smt (z3) Eps_cong equiv_Eps_in equiv_class_eq_iff quotient_eq_iff)
lemma nested_somes:
"⟦equiv X R; w ∈ X // R⟧ ⟹ (SOME z. z ∈ w) = (SOME z. z ∈ R``{(SOME z'. z' ∈ w)})"
by (metis proj_Eps proj_def)
locale eq_var_rel = alt_grp_act G X φ
for
G :: "('grp, 'b) monoid_scheme" and
X :: "'X set" (structure) and
φ +
fixes R
assumes
is_subrel:
"R ⊆ X × X" and
is_eq_var_rel:
"⋀a b. (a, b) ∈ R ⟹ ∀g ∈ carrier G. (g ⊙⇘φ⇙ a, g ⊙⇘φ⇙ b) ∈ R"
begin
lemma is_eq_var_rel' [simp, GMN_simps]:
"⋀a b. (a, b) ∈ R ⟹ ∀g ∈ carrier G. ((φ g) a, (φ g) b) ∈ R"
using is_eq_var_rel
by auto
lemma is_eq_var_rel_rev:
"a ∈ X ⟹ b ∈ X ⟹ g ∈ carrier G ⟹ (g ⊙⇘φ⇙ a, g ⊙⇘φ⇙ b) ∈ R ⟹ (a, b) ∈ R"
proof -
assume
A_0: "(g ⊙⇘φ⇙ a, g ⊙⇘φ⇙ b) ∈ R" and
A_1: "a ∈ X" and
A_2: "b ∈ X" and
A_3: "g ∈ carrier G"
have H_0: " group_action G X φ" and
H_1: "R ⊆ X × X" and
H_2: "⋀a b g. (a, b) ∈ R ⟹ g ∈ carrier G ⟹ (φ g a, φ g b) ∈ R"
by (simp add: group_action_axioms is_subrel)+
from H_0 have H_3: "group G"
by (auto simp add: group_action_def group_hom_def)
have H_4: "(φ (inv⇘G⇙ g) (φ g a), φ (inv⇘G⇙ g) (φ g b)) ∈ R"
apply (rule H_2)
using A_0 apply simp
by (simp add: A_3 H_3)
from H_3 A_3 have H_5: "(inv⇘G⇙ g) ∈ carrier G"
by auto
hence H_6: "⋀e. e ∈ X ⟹ φ (inv⇘G⇙ g) (φ g e) = φ ((inv⇘G⇙ g) ⊗⇘G⇙ g) e"
using H_0 A_3 group_action.composition_rule
by fastforce
hence H_7: "⋀e. e ∈ X ⟹ φ (inv⇘G⇙ g) (φ g e) = φ 𝟭⇘G⇙ e"
using H_3 A_3 group.l_inv
by fastforce
hence H_8: "⋀e. e ∈ X ⟹ φ (inv⇘G⇙ g) (φ g e) = e"
using H_0
by (simp add: A_3 group_action.orbit_sym_aux)
thus "(a, b) ∈ R"
using A_1 A_2 H_4
by simp
qed
lemma equiv_equivar_class_some_eq:
assumes
A_0: "equiv X R" and
A_1: "w ∈ X // R" and
A_2: "g ∈ carrier G"
shows "([ φ ]⇩R) g w = R `` {(SOME z'. z' ∈ φ g ` w)}"
proof-
obtain z where H_z: "w = R `` {z} ∧ z ∈ w"
by (metis A_0 A_1 equiv_class_self quotientE)
have H_0: "⋀x. (φ g z, x) ∈ R ⟹ x ∈ φ g ` {y. (z, y) ∈ R}"
proof-
fix y
assume
A1_0: "(φ g z, y) ∈ R"
obtain y' where H2_y': "y' = φ (inv⇘G⇙ g) y ∧ y' ∈ X"
using eq_var_rel_axioms
apply (clarsimp simp add: eq_var_rel_def group_action_def group_hom_def)
by (meson A_0 eq_var_rel_axioms A_2 A1_0 equiv_class_eq_iff eq_var_rel.is_eq_var_rel
group.inv_closed element_image)
from A_1 A_2 H2_y' have H2_0: "φ g y' = y"
apply (clarsimp simp add: eq_var_rel_def eq_var_rel_axioms_def)
using A_2 A1_0 group_action.bij_prop1[where G = "G" and E = "X" and φ = "φ"]
by (metis A_0 alt_group_act_is_grp_act alt_grp_act_axioms equiv_class_eq_iff orbit_sym_aux)
from A_1 A_2 A1_0 have H2_1: "(z, y') ∈ R"
by (metis H2_0 A_0 A_2 H2_y' H_z equiv_class_eq_iff is_eq_var_rel_rev
quotient_eq_iff make_op_def)
thus "y ∈ φ g ` {v. (z, v) ∈ R}"
using H2_0
by (auto simp add: image_def)
qed
have H_1: "φ g ` (R `` {z}) = R `` {φ g z}"
apply (clarsimp simp add: Relation.Image_def)
apply (rule subset_antisym; simp add: Set.subset_eq; rule allI; rule impI)
using eq_var_rel_axioms A_2 eq_var_rel.is_eq_var_rel
apply simp
by (simp add: H_0)
have H_2: "φ g ` w ∈ X // R"
using eq_var_rel_axioms A_1 A_2 H_1
by (metis A_0 H_z equiv_class_eq_iff quotientI quotient_eq_iff element_image)
thus "([φ]⇩R) g w = R `` {SOME z'. z' ∈ φ g ` w}"
using A_0 A_1 A_2
apply (clarsimp simp add: Image_def)
apply (intro subset_antisym)
apply (clarify)
using A_0 H_z imageI insert_absorb insert_not_empty some_in_eq some_equiv_class_id
apply (smt (z3) A_1 Eps_cong Image_singleton_iff equiv_Eps_in)
apply (clarify)
by (smt (z3) Eps_cong equiv_Eps_in image_iff in_quotient_imp_closed quotient_eq_iff)
qed
lemma ec_er_closed_under_action:
assumes
A_0: "equiv X R" and
A_1: "g ∈ carrier G" and
A_2: "w ∈ X//R"
shows "φ g ` w ∈ X // R"
proof-
obtain z where H_z: "R `` {z} = w ∧ z ∈ X"
by (metis A_2 quotientE)
have H_0: "equiv X R ⟹ g ∈ carrier G ⟹ w ∈ X // R ⟹
{y. (φ g z, y) ∈ R} ⊆ {y. ∃x. (z, x) ∈ R ∧ y = φ g x}"
proof (clarify)
fix x
assume
A1_0: "equiv X R" and
A1_1: "g ∈ carrier G" and
A1_2: "w ∈ X // R" and
A1_3: "(φ g z, x) ∈ R"
obtain x' where H2_x': "x = φ g x' ∧ x' ∈ X"
using group_action_axioms
by (metis A1_1 is_subrel A1_3 SigmaD2 group_action.bij_prop1 subsetD)
thus "∃y. (z, y) ∈ R ∧ x = φ g y"
using is_eq_var_rel_rev[where g = "g" and a = "z" and b = "x'"] A1_3
by (auto simp add: eq_var_rel_def eq_var_rel_axioms_def A1_1 A1_2 group_action_axioms H_z
H2_x')
qed
have H_1: "φ g ` R `` {z} = R `` {φ g z}"
using A_0 A_1 A_2
apply (clarsimp simp add: eq_var_rel_axioms_def eq_var_rel_def
Image_def image_def)
apply (intro subset_antisym)
apply (auto)[1]
by (rule H_0)
thus "φ g ` w ∈ X // R"
using H_1 H_z
by (metis A_1 quotientI element_image)
qed
text ‹
The following lemma corresponds to the first part of lemma 3.5 from \cite{bojanczyk2014automata}:
›
lemma quot_act_wd:
"⟦equiv X R; x ∈ X; g ∈ carrier G⟧ ⟹ g ⊙⇘[φ]⇩R⇙ (R `` {x}) = (R `` {g ⊙⇘φ⇙ x})"
apply (clarsimp simp add: eq_var_rel_def eq_var_rel_axioms_def)
apply (rule conjI; rule impI)
apply (smt (verit, best) Eps_cong Image_singleton_iff eq_var_rel.is_eq_var_rel'
eq_var_rel_axioms equiv_Eps_in equiv_class_eq)
by (simp add: quotientI)+
text ‹
The following lemma corresponds to the second part of lemma 3.5 from \cite{bojanczyk2014automata}:
›
lemma quot_act_is_grp_act:
"equiv X R ⟹ alt_grp_act G (X // R) ([φ]⇩R)"
proof-
assume A_0: "equiv X R"
have H_0: "⋀x. Group.group G ⟹
Group.group (BijGroup X) ⟹
R ⊆ X × X ⟹
φ ∈ carrier G → carrier (BijGroup X) ⟹
∀x∈carrier G. ∀y∈carrier G. φ (x ⊗⇘G⇙ y) = φ x ⊗⇘BijGroup X⇙ φ y ⟹
x ∈ carrier G ⟹ (λxa∈X // R. R `` {φ x (SOME z. z ∈ xa)}) ∈ carrier (BijGroup (X // R))"
proof-
fix g
assume
A1_0: "Group.group G" and
A1_1: "Group.group (BijGroup X)" and
A1_2: "φ ∈ carrier G → carrier (BijGroup X)" and
A1_3: "∀x∈carrier G. ∀y∈carrier G. φ (x ⊗⇘G⇙ y) = φ x ⊗⇘BijGroup X⇙ φ y" and
A1_4: "g ∈ carrier G"
have H_0: "group_action G X φ"
apply (clarsimp simp add: group_action_def group_hom_def group_hom_axioms_def)
apply (simp add: A1_0 A1_1)+
apply (simp add: hom_def)
apply (rule conjI)
using A1_2
apply blast
by (simp add: A1_3)
have H1_0: "⋀x y. ⟦x ∈ X // R; y ∈ X // R; R `` {φ g (SOME z. z ∈ x)} =
R `` {φ g (SOME z. z ∈ y)}⟧ ⟹ x ⊆ y"
proof (clarify; rename_tac a)
fix x y a
assume
A2_0: "x ∈ X // R" and
A2_1: "y ∈ X // R" and
A2_2: "R `` {φ g (SOME z. z ∈ x)} = R `` {φ g (SOME z. z ∈ y)}" and
A2_3: "a ∈ x"
obtain b where H2_b: "R `` {b} = y ∧ b ∈ X"
by (metis A2_1 quotientE)
obtain a' b' where H2_a'_b': "a'∈ x ∧ b'∈ y ∧ R `` {φ g a'} = R `` {φ g b'}"
by (metis A_0 A2_1 A2_2 A2_3 equiv_Eps_in some_eq_imp)
from H2_a'_b' have H2_2: "(φ g a', φ g b') ∈ R"
by (metis A_0 A1_4 A2_1 Image_singleton_iff eq_var_rel.is_eq_var_rel' eq_var_rel_axioms
quotient_eq_iff)
hence H2_0: "(φ (inv⇘G⇙ g) (φ g a'), φ (inv⇘G⇙ g) (φ g b')) ∈ R"
by (simp add: A1_0 is_eq_var_rel A1_4)
have H2_1: "a' ∈ X ∧ b' ∈ X"
using A_0 A2_0 A2_1 H2_a'_b' in_quotient_imp_subset
by blast
hence H2_2: "(a', b') ∈ R"
using H2_0
by (metis A1_4 H_0 group_action.orbit_sym_aux)
have H2_3: "(a, a') ∈ R"
by (meson A_0 A2_0 A2_3 H2_a'_b' quotient_eq_iff)
hence H2_4: "(b', a) ∈ R"
using H2_2
by (metis A_0 A2_0 A2_1 A2_3 H2_a'_b' quotient_eqI quotient_eq_iff)
thus "a ∈ y"
by (metis A_0 A2_1 H2_a'_b' in_quotient_imp_closed)
qed
have H1_1: "⋀x. x ∈ X // R ⟹ ∃xa∈X // R. x = R `` {φ g (SOME z. z ∈ xa)}"
proof -
fix x
assume
A2_0: "x ∈ X // R"
have H2_0: "⋀e. R `` {e} ∈ X // R ⟹ R `` {e} ⊆ R `` {φ g (φ (inv⇘G⇙ g) e)}"
proof (rule subsetI)
fix e y
assume
A3_0: "R `` {e} ∈ X // R" and
A3_1: "y ∈ R `` {e}"
have H3_0: "y ∈ X"
using A3_1 is_subrel
by blast
from H_0 have H3_1: "φ g (φ (inv⇘G⇙ g) y) = y"
by (metis (no_types, lifting) A1_0 A1_4 H3_0 group.inv_closed group.inv_inv
group_action.orbit_sym_aux)
from A3_1 have H3_2: "(e, y) ∈ R"
by simp
hence H3_3: "((φ (inv⇘G⇙ g) e), (φ (inv⇘G⇙ g) y)) ∈ R"
using is_eq_var_rel A1_4 A1_0
by simp
hence H3_4: "(φ g (φ (inv⇘G⇙ g) e), φ g (φ (inv⇘G⇙ g) y)) ∈ R"
using is_eq_var_rel A1_4 A1_0
by simp
hence H3_5: "(φ g (φ (inv⇘G⇙ g) e), y) ∈ R"
using H3_1
by simp
thus "y ∈ R `` {φ g (φ (inv⇘G⇙ g) e)}"
by simp
qed
hence H2_1: "⋀e. R `` {e} ∈ X // R ⟹ R `` {e} = R `` {φ g (φ (inv⇘G⇙ g) e)}"
by (metis A_0 proj_def proj_in_iff equiv_class_eq_iff subset_equiv_class)
have H2_2: "⋀e f. R `` {e} ∈ X // R ⟹ R `` {f} ∈ X // R ⟹
R `` {e} = R `` {f} ⟹ ∀f'∈ R `` {f}. R `` {e} = R `` {f'}"
by (metis A_0 Image_singleton_iff equiv_class_eq)
have H2_3: "x ∈ X // R ⟹ ∃e∈X. x = R `` {e}"
by (meson quotientE)
have H2_4: "⋀e. R `` {e} ∈ X // R ⟹ R `` {e} = R `` {φ g (φ (inv⇘G⇙ g) e)} ∧
(φ (inv⇘G⇙ g) e) ∈ R `` {φ (inv⇘G⇙ g) e}"
by (smt (z3) A_0 A1_0 A1_4 H_0 H2_1 Image_singleton_iff equiv_class_eq_iff
group.inv_closed group_action.element_image in_quotient_imp_non_empty
subset_empty subset_emptyI)
have H2_5: "⋀e. R `` {e} ∈ X // R ⟹ ∀z∈R `` {φ (inv⇘G⇙ g) e}. (φ (inv⇘G⇙ g) e, z) ∈ R"
by simp
hence H2_6: "⋀e. R `` {e} ∈ X // R ⟹
∀z∈R `` {φ (inv⇘G⇙ g) e}. (φ g (φ (inv⇘G⇙ g) e), φ g z) ∈ R"
using is_eq_var_rel' A1_4 A1_0
by blast
hence H2_7: "⋀e. R `` {e} ∈ X // R ⟹ ∀z∈R `` {φ (inv⇘G⇙ g) e}. (e, φ g z) ∈ R"
using H2_1
by blast
hence H2_8: "⋀e. R `` {e} ∈ X // R ⟹ ∀z∈R `` {φ (inv⇘G⇙ g) e}. R `` {e} = R `` {φ g z}"
by (meson A_0 equiv_class_eq_iff)
have H2_9: "⋀e. R `` {e} ∈ X // R ⟹
R `` {e} = R `` {φ g (SOME z. z ∈ R `` {φ (inv⇘G⇙ g) e})}"
proof-
fix e
assume
A3_0: "R `` {e} ∈ X // R"
show "R `` {e} = R `` {φ g (SOME z. z ∈ R `` {φ (inv⇘G⇙ g) e})}"
apply (rule someI2[where Q = "λz. R `` {e} = R `` {φ g z}" and
P = "λz. z ∈ R `` {φ (inv⇘G⇙ g) e}" and a = "φ (inv⇘G⇙ g) e"])
using A3_0 H2_4
apply blast
using A3_0 H2_8
by auto
qed
have H2_10: "∀e. (R `` {e} ∈ X // R ⟶
(R `` {e} = R `` {φ g (SOME z. z ∈ R `` {φ (inv⇘G⇙ g) e})}))"
using H2_9
by auto
hence H2_11: "∀e. (R `` {e} ∈ X // R ⟶
(∃xa∈X // R. R `` {e} = R `` {φ g (SOME z. z ∈ xa)}))"
using H2_8
apply clarsimp
by (smt (verit, best) A_0 H2_3 H2_5 H2_4 equiv_Eps_in equiv_class_eq_iff quotientI)
have H2_12: "⋀x. x ∈ X // R ⟹ ∃e∈X. x = R `` {e} "
by (meson quotientE)
have H2_13: "⋀x. x ∈ X // R ⟹ ∃xa∈X // R. x = R `` {φ g (SOME z. z ∈ xa)}"
using H2_11 H2_12
by blast
show "∃xa∈X // R. x = R `` {φ g (SOME z. z ∈ xa)}"
by (simp add: A2_0 H2_13)
qed
show "(λx∈X // R. R `` {φ g (SOME z. z ∈ x)}) ∈ carrier (BijGroup (X // R))"
apply (clarsimp simp add: BijGroup_def Bij_def bij_betw_def)
apply (clarsimp simp add: inj_on_def)
apply (rule conjI)
apply (clarsimp)
apply (rule subset_antisym)
apply (simp add: H1_0)
apply (simp add: ‹⋀y x. ⟦x ∈ X // R;
y ∈ X // R; R `` {φ g (SOME z. z ∈ x)} = R `` {φ g (SOME z. z ∈ y)}⟧ ⟹ x ⊆ y›)
apply (rule subset_antisym; clarify)
subgoal for x y
by (metis A_0 is_eq_var_rel' A1_4 Eps_cong equiv_Eps_preserves equiv_class_eq_iff
quotientI)
apply (clarsimp simp add: Set.image_def)
by (simp add: H1_1)
qed
have H_1: "⋀x y. ⟦Group.group G; Group.group (BijGroup X); R ⊆ X × X;
φ ∈ carrier G → carrier (BijGroup X);
∀x∈carrier G. ∀y∈carrier G. φ (x ⊗⇘G⇙ y) = φ x ⊗⇘BijGroup X⇙ φ y;
x ∈ carrier G; y ∈ carrier G; x ⊗⇘G⇙ y ∈ carrier G⟧ ⟹
(λxa∈X // R. R `` {(φ x ⊗⇘BijGroup X⇙ φ y) (SOME z. z ∈ xa)}) =
(λxa∈X // R. R `` {φ x (SOME z. z ∈ xa)}) ⊗⇘BijGroup (X // R)⇙
(λx∈X // R. R `` {φ y (SOME z. z ∈ x)})"
proof -
fix x y
assume
A1_1: "Group.group G" and
A1_2: "Group.group (BijGroup X)" and
A1_3: "φ ∈ carrier G → carrier (BijGroup X)" and
A1_4: "∀x∈carrier G. ∀y∈carrier G. φ (x ⊗⇘G⇙ y) = φ x ⊗⇘BijGroup X⇙ φ y" and
A1_5: "x ∈ carrier G" and
A1_6: "y ∈ carrier G" and
A1_7: "x ⊗⇘G⇙ y ∈ carrier G"
have H1_0: "⋀w::'X set. w ∈ X // R ⟹
R `` {(φ x ⊗⇘BijGroup X⇙ φ y) (SOME z. z ∈ w)} =
((λv∈X // R. R `` {φ x (SOME z. z ∈ v)}) ⊗⇘BijGroup (X // R)⇙
(λx∈X // R. R `` {φ y (SOME z. z ∈ x)})) w"
proof-
fix w
assume
A2_0: "w ∈ X // R"
have H2_4: "φ y ` w ∈ X // R"
using ec_er_closed_under_action[where w = "w" and g = "y"]
by (clarsimp simp add: group_hom_axioms_def hom_def A_0 A1_1 A1_2 is_eq_var_rel' A1_3 A1_4
A1_6 A2_0)
hence H2_1: "R `` {(φ x ⊗⇘BijGroup X⇙ φ y) (SOME z. z ∈ w)} =
R `` {φ (x ⊗⇘G⇙ y) (SOME z. z ∈ w)}"
using A1_4 A1_5 A1_6
by auto
also have H2_2: "... = R `` {SOME z. z ∈ φ (x ⊗⇘G⇙ y) ` w}"
using A1_7 equiv_equivar_class_some_eq[where w = "w" and g = "x ⊗⇘G⇙ y"]
by (clarsimp simp add: A1_7 A_0 A2_0 group_action_def group_hom_def group_hom_axioms_def
hom_def)
also have H2_3: "... = R `` {SOME z. z ∈ φ x ` φ y ` w}"
apply (rule meta_mp[of "¬(∃x. x ∈ w ∧ x ∉ X)"])
using A1_1 is_eq_var_rel' A1_3 A1_4 A1_5 A1_6 A2_0
apply (clarsimp simp add: image_def BijGroup_def restrict_def compose_def Pi_def)
apply (smt (z3) Eps_cong)
apply (clarify)
using A_0 A2_0 in_quotient_imp_subset
by auto
also have H2_5: "... = R `` {φ x (SOME z. z ∈ φ y ` w)}"
using equiv_equivar_class_some_eq[where w = "φ y ` w" and g = "x"]
apply (clarsimp simp add: A_0 group_action_def group_hom_def group_hom_axioms_def hom_def)
by (simp add: A1_1 A1_2 is_eq_var_rel' A1_3 A1_4 A1_5 H2_4)
also have H2_6: "... = R `` {φ x (SOME z. z ∈ R``{(SOME z'. z' ∈ φ y ` w)})}"
using H2_4 nested_somes[where w = "φ y ` w" and X = "X" and R = "R"] A_0
by presburger
also have H2_7: "... = R `` {φ x (SOME z. z ∈ R `` {φ y (SOME z'. z' ∈ w)})}"
using equiv_equivar_class_some_eq[where g = "y" and w = "w"] H2_6
by (simp add: A_0 group_action_def
group_hom_def group_hom_axioms_def hom_def A1_1 A1_2 is_eq_var_rel' A1_3 A1_4 A2_0 A1_6)
also have H2_9: "... = ((λv∈X // R. R `` {φ x (SOME z. z ∈ v)}) ⊗⇘BijGroup (X // R)⇙
(λx∈X // R. R `` {φ y (SOME z. z ∈ x)})) w"
proof-
have H3_0: "⋀u. R `` {φ y (SOME z. z ∈ w)} ∈ X // R ⟹ u ∈ carrier G ⟹
(λv∈X // R. R `` {φ u (SOME z. z ∈ v)}) ∈ Bij (X // R)"
proof -
fix u
assume
A4_0: "R `` {φ y (SOME z. z ∈ w)} ∈ X // R" and
A4_1: "u ∈ carrier G"
have H4_0: "∀g ∈ carrier G.
(λx∈X // R. R `` {φ g (SOME z. z ∈ x)}) ∈ carrier (BijGroup (X // R))"
by (simp add: A_0 A1_1 A1_2 A1_3 A1_4 H_0 is_subrel)
thus "(λv∈X // R. R `` {φ u (SOME z. z ∈ v)}) ∈ Bij (X // R)"
by (auto simp add: BijGroup_def A4_1)
qed
have H3_1: "R `` {φ y (SOME z. z ∈ w)} ∈ X // R"
proof-
have H4_0: "φ y ` w ∈ X // R"
using ec_er_closed_under_action
by (simp add: H2_4)
hence H4_1: "R `` {(SOME z. z ∈ φ y ` w)} = φ y ` w"
apply (clarsimp simp add: image_def)
apply (rule subset_antisym)
using A_0 equiv_Eps_in in_quotient_imp_closed
apply fastforce
using A_0 equiv_Eps_in quotient_eq_iff
by fastforce
have H4_2: "R `` {φ y (SOME z. z ∈ w)} = R `` {(SOME z. z ∈ φ y ` w)}"
using equiv_equivar_class_some_eq[where g = "y" and w = "w"]
by (metis A_0 A2_0 H4_0 H4_1 equiv_Eps_in imageI some_equiv_class_id)
from H4_0 H4_1 H4_2 show "R `` {φ y (SOME z. z ∈ w)} ∈ X // R"
by auto
qed
show ?thesis
apply (rule meta_mp[of "R `` {φ y (SOME z. z ∈ w)} ∈ X // R"])
apply (rule meta_mp[of "∀u ∈ carrier G.
(λv∈X // R. R `` {φ u (SOME z. z ∈ v)}) ∈ Bij (X // R)"])
using A2_0 A1_5 A1_6
apply ( simp add: BijGroup_def compose_def)
apply clarify
by (simp add: H3_0 H3_1)+
qed
finally show "R `` {(φ x ⊗⇘BijGroup X⇙ φ y) (SOME z. z ∈ w)} =
((λv∈X // R. R `` {φ x (SOME z. z ∈ v)}) ⊗⇘BijGroup (X // R)⇙
(λx∈X // R. R `` {φ y (SOME z. z ∈ x)})) w"
by simp
qed
have H1_1: "⋀w::'X set. w ∉ X // R ⟹
((λv∈X // R. R `` {φ x (SOME z. z ∈ v)}) ⊗⇘BijGroup (X // R)⇙
(λx∈X // R. R `` {φ y (SOME z. z ∈ x)})) w = undefined"
proof -
fix w
assume
A2_0: "w ∉ X // R"
have H2_0: "⋀u. u∈ carrier G ⟹ (λv∈X // R. R `` {φ u (SOME z. z ∈ v)}) ∈ Bij (X // R)"
using H_0
apply (clarsimp simp add: A_0 A1_1 A1_2 is_eq_var_rel' A1_3 A1_4 is_subrel)
by (simp add: BijGroup_def)
hence H2_1: "(λx'∈X // R. R `` {φ y (SOME z. z ∈ x')}) ∈ Bij (X // R)"
using A1_6
by auto
from H2_0 have H2_2: "(λx'∈X // R. R `` {φ x (SOME z. z ∈ x')}) ∈ Bij (X // R)"
by (simp add: A1_5)
thus "((λv∈X // R. R `` {φ x (SOME z. z ∈ v)}) ⊗⇘BijGroup (X // R)⇙
(λx∈X // R. R `` {φ y (SOME z. z ∈ x)})) w = undefined"
using H2_1 H2_2
by (auto simp add: BijGroup_def compose_def A2_0)
qed
from H1_0 H1_1 have "⋀w. (λxa∈X // R. R `` {(φ x ⊗⇘BijGroup X⇙ φ y) (SOME z. z ∈ xa)}) w =
((λxa∈X // R. R `` {φ x (SOME z. z ∈ xa)}) ⊗⇘BijGroup (X // R)⇙
(λx'∈X // R. R `` {φ y (SOME z. z ∈ x')})) w"
by auto
thus "(λxa∈X // R. R `` {(φ x ⊗⇘BijGroup X⇙ φ y) (SOME z. z ∈ xa)}) =
(λxa∈X // R. R `` {φ x (SOME z. z ∈ xa)}) ⊗⇘BijGroup (X // R)⇙
(λx∈X // R. R `` {φ y (SOME z. z ∈ x)})"
by (simp add: restrict_def)
qed
show ?thesis
apply (clarsimp simp add: group_action_def group_hom_def)
using eq_var_rel_axioms
apply (clarsimp simp add: eq_var_rel_def eq_var_rel_axioms_def
group_action_def group_hom_def)
apply (rule conjI)
apply (simp add: group_BijGroup)
apply (clarsimp simp add: group_hom_axioms_def hom_def)
apply (intro conjI)
apply (rule funcsetI; simp)
apply (simp add: H_0)
apply (clarify; rule conjI; intro impI)
apply (simp add: H_1)
by (auto simp add: group.is_monoid monoid.m_closed)
qed
end
locale eq_var_func = GA_0: alt_grp_act G X φ + GA_1: alt_grp_act G Y ψ
for
G :: "('grp, 'b) monoid_scheme" and
X :: "'X set" and
φ and
Y :: "'Y set" and
ψ +
fixes
f :: "'X ⇒ 'Y"
assumes
is_ext_func_bet:
"f ∈ (X →⇩E Y)" and
is_eq_var_func:
"⋀a g. a ∈ X ⟹ g ∈ carrier G ⟹ f (g ⊙⇘φ⇙ a) = g ⊙⇘ψ⇙ (f a)"
begin
lemma is_eq_var_func' [simp]:
"a ∈ X ⟹ g ∈ carrier G ⟹ f (φ g a) = ψ g (f a)"
using is_eq_var_func
by auto
end
lemma G_set_equiv:
"alt_grp_act G A φ ⟹ eq_var_subset G A φ A"
by (auto simp add: eq_var_subset_def eq_var_subset_axioms_def group_action_def
group_hom_def group_hom_axioms_def hom_def BijGroup_def Bij_def bij_betw_def)
subsection ‹
Basic ($G$)-Automata Theory
›
locale language =
fixes A :: "'alpha set" and
L
assumes
is_lang: "L ⊆ A⇧⋆"
locale G_lang = alt_grp_act G A φ + language A L
for
G :: "('grp, 'b) monoid_scheme" and
A :: "'alpha set" (structure) and
φ L +
assumes
L_is_equivar:
"eq_var_subset G (A⇧⋆) (induced_star_map φ) L"
begin
lemma G_lang_is_lang[simp]: "language A L"
by (simp add: language_axioms)
end
sublocale G_lang ⊆ language
by simp
fun give_input :: "('state ⇒ 'alpha ⇒ 'state) ⇒ 'state ⇒ 'alpha list ⇒ 'state"
where "give_input trans_func s Nil = s"
| "give_input trans_func s (a#as) = give_input trans_func (trans_func s a) as"
adhoc_overloading
star give_input
locale det_aut =
fixes
labels :: "'alpha set" and
states :: "'state set" and
init_state :: "'state" and
fin_states :: "'state set" and
trans_func :: "'state ⇒ 'alpha ⇒ 'state" ("δ")
assumes
init_state_is_a_state:
"init_state ∈ states" and
fin_states_are_states:
"fin_states ⊆ states" and
trans_func_ext:
"(λ(state, label). trans_func state label) ∈ (states × labels) →⇩E states"
begin
lemma trans_func_well_def:
"⋀state label. state ∈ states ⟹ label ∈ labels ⟹ (δ state label) ∈ states"
using trans_func_ext
by auto
lemma give_input_closed:
"input ∈ (labels⇧⋆) ⟹ s ∈ states ⟹ (δ⇧⋆) s input ∈ states"
apply (induction input arbitrary: s)
by (auto simp add: trans_func_well_def)
lemma input_under_concat:
"w ∈ labels⇧⋆ ⟹ v ∈ labels⇧⋆ ⟹ (δ⇧⋆) s (w @ v) = (δ⇧⋆) ((δ⇧⋆) s w) v"
apply (induction w arbitrary: s)
by auto
lemma eq_pres_under_concat:
assumes
"w ∈ labels⇧⋆" and
"w' ∈ labels⇧⋆" and
"s ∈ states" and
"(δ⇧⋆) s w = (δ⇧⋆) s w'"
shows "∀v ∈ labels⇧⋆. (δ⇧⋆) s (w @ v) = (δ⇧⋆) s (w' @ v)"
using input_under_concat[where w = w and s = s] input_under_concat[where w = w' and s = s] assms
by auto
lemma trans_to_charact:
"⋀s a w. ⟦s ∈ states; a ∈ labels; w ∈ labels⇧⋆; s = (δ⇧⋆) i w⟧ ⟹ (δ⇧⋆) i (w @ [a]) = δ s a"
proof-
fix s a w
assume
A_0: "s ∈ states" and
A_1: "a ∈ labels" and
A_2: "w ∈ labels⇧⋆" and
A_3: "s = (δ⇧⋆) i w"
have H_0: "trans_func s a = (δ⇧⋆) s [a]"
by auto
from A_2 A_3 H_0 have H_1: "(δ⇧⋆) s [a] = (δ⇧⋆) ((δ⇧⋆) i w) [a]"
by simp
from A_1 A_2 have H_2: "(δ⇧⋆) ((δ⇧⋆) i w) [a] = (δ⇧⋆) i (w @ [a])"
using input_under_concat
by force
show "(δ⇧⋆) i (w @ [a]) = δ s a"
using A_1 H_0 A_3 H_1 H_2
by force
qed
end
locale aut_hom = Aut0: det_aut A S⇩0 i⇩0 F⇩0 δ⇩0 + Aut1: det_aut A S⇩1 i⇩1 F⇩1 δ⇩1 for
A :: "'alpha set" and
S⇩0 :: "'states_0 set" and
i⇩0 and F⇩0 and δ⇩0 and
S⇩1 :: "'states_1 set" and
i⇩1 and F⇩1 and δ⇩1 +
fixes f :: "'states_0 ⇒ 'states_1"
assumes
hom_is_ext:
"f ∈ S⇩0 →⇩E S⇩1" and
pres_init:
"f i⇩0 = i⇩1" and
pres_final:
"s ∈ F⇩0 ⟷ f s ∈ F⇩1 ∧ s ∈ S⇩0" and
pres_trans:
"s⇩0 ∈ S⇩0 ⟹ a ∈ A ⟹ f (δ⇩0 s⇩0 a) = δ⇩1 (f s⇩0) a"
begin
lemma hom_translation:
"input ∈ (A⇧⋆) ⟹ s ∈ S⇩0 ⟹ (f ((δ⇩0⇧⋆) s input)) = ((δ⇩1⇧⋆) (f s) input)"
apply (induction input arbitrary: s)
by (auto simp add: Aut0.trans_func_well_def pres_trans)
lemma recognise_same_lang:
"input ∈ A⇧⋆ ⟹ ((δ⇩0⇧⋆) i⇩0 input) ∈ F⇩0 ⟷ ((δ⇩1⇧⋆) i⇩1 input) ∈ F⇩1"
using hom_translation[where input = input and s = i⇩0]
apply (clarsimp simp add: Aut0.init_state_is_a_state pres_init pres_final)
apply (induction input)
apply (clarsimp simp add: Aut0.init_state_is_a_state)
using Aut0.give_input_closed Aut0.init_state_is_a_state
by blast
end
locale aut_epi = aut_hom +
assumes
is_epi: "f ` S⇩0 = S⇩1"
locale det_G_aut =
is_aut: det_aut A S i F δ +
labels_a_G_set: alt_grp_act G A φ +
states_a_G_set: alt_grp_act G S ψ +
accepting_is_eq_var: eq_var_subset G S ψ F +
init_is_eq_var: eq_var_subset G S ψ "{i}" +
trans_is_eq_var: eq_var_func G "S × A"
"λg∈carrier G. λ(s, a) ∈ (S × A). (ψ g s, φ g a)"
S "ψ" "(λ(s, a) ∈ (S × A). δ s a)"
for A :: "'alpha set" (structure) and
S :: "'states set" and
i F δ and
G :: "('grp, 'b) monoid_scheme" and
φ ψ
begin
adhoc_overloading
star labels_a_G_set.induced_star_map
lemma give_input_eq_var:
"eq_var_func G
(A⇧⋆ × S) (λg∈carrier G. λ(w, s) ∈ (A⇧⋆ × S). ((φ⇧⋆) g w, ψ g s))
S ψ
(λ(w, s) ∈ (A⇧⋆ × S). (δ⇧⋆) s w)"
proof-
have H_0: "⋀a w s g.
(⋀s. s ∈ S ⟹ (φ⇧⋆) g w ∈ A⇧⋆ ∧ ψ g s ∈ S ⟹
(δ⇧⋆) (ψ g s) ((φ⇧⋆) g w) = ψ g ((δ⇧⋆) s w)) ⟹
s ∈ S ⟹
g ∈ carrier G ⟹
a ∈ A ⟹ ∀x∈set w. x ∈ A ⟹ ψ g s ∈ S ⟹ ∀x∈set ((φ⇧⋆) g (a # w)). x ∈ A ⟹
(δ⇧⋆) (ψ g s) ((φ⇧⋆) g (a # w)) = ψ g ((δ⇧⋆) (δ s a) w)"
proof-
fix a w s g
assume
A_IH: "(⋀s. s ∈ S ⟹
(φ⇧⋆) g w ∈ A⇧⋆ ∧ ψ g s ∈ S ⟹
(δ⇧⋆) (ψ g s) ((φ⇧⋆) g w) = ψ g ((δ⇧⋆) s w))" and
A_0: "s ∈ S" and
A_1: "ψ g s ∈ S" and
A_2: "∀x∈set ((φ⇧⋆) g (a # w)). x ∈ A" and
A_3: "g ∈ carrier G" and
A_4: " a ∈ A" and
A_5: "∀x∈set w. x ∈ A"
have H_0: "((φ⇧⋆) g (a # w)) = (φ g a) # (φ⇧⋆) g w"
using A_4 A_5 A_3
by auto
hence H_1: "(δ⇧⋆) (ψ g s) ((φ⇧⋆) g (a # w))
= (δ⇧⋆) (ψ g s) ((φ g a) # (φ⇧⋆) g w)"
by simp
have H_2: "... = (δ⇧⋆) ((δ⇧⋆) (ψ g s) [φ g a]) ((φ⇧⋆) g w)"
using is_aut.input_under_concat
by simp
have H_3: "(δ⇧⋆) (ψ g s) [φ g a] = ψ g (δ s a)"
using trans_is_eq_var.eq_var_func_axioms A_4 A_5 A_0 A_1 A_3 apply (clarsimp simp del:
GMN_simps simp add: eq_var_func_def eq_var_func_axioms_def make_op_def)
apply (rule meta_mp[of "ψ g s ∈ S ∧ φ g a ∈ A ∧ s ∈ S ∧ a ∈ A"])
apply presburger
apply (clarify)
using labels_a_G_set.element_image
by presburger
have H_4: "(δ⇧⋆) (ψ g (δ s a)) ((φ⇧⋆) g w) = ψ g ((δ⇧⋆) (δ s a) w)"
apply (rule A_IH[where s1 = "δ s a"])
subgoal
using A_4 A_5 A_0
by (auto simp add: is_aut.trans_func_well_def)
using A_4 A_5 A_0 A_3 ‹δ s a ∈ S› states_a_G_set.element_image
by (metis A_2 Cons_in_lists_iff H_0 in_listsI)
show "(δ⇧⋆) (ψ g s) ((φ⇧⋆) g (a # w)) = ψ g ((δ⇧⋆) (δ s a) w)"
using H_0 H_1 H_2 H_3 H_4
by presburger
qed
show ?thesis
apply (subst eq_var_func_def)
apply (subst eq_var_func_axioms_def)
apply (rule conjI)
apply (rule prod_group_act[where G = G and A = "A⇧⋆" and φ = "(φ⇧⋆)"
and B = S and ψ = ψ])
using labels_a_G_set.lists_a_Gset
apply blast
apply (simp add: states_a_G_set.group_action_axioms)
apply (rule conjI)
apply (simp add: states_a_G_set.group_action_axioms)
apply (rule conjI)
apply (subst extensional_funcset_def)
apply (subst restrict_def)
apply (subst Pi_def)
apply (subst extensional_def)
apply (auto simp add: in_listsI is_aut.give_input_closed)[1]
apply (subst restrict_def)
apply (clarsimp simp del: GMN_simps simp add: make_op_def)
apply (rule conjI; intro impI)
subgoal for w s g
apply (induction w arbitrary: s)
apply simp
apply (clarsimp simp del: GMN_simps)
by (simp add: H_0 del: GMN_simps)
apply clarsimp
by (metis (no_types, lifting) image_iff in_lists_conv_set labels_a_G_set.surj_prop list.set_map
states_a_G_set.element_image)
qed
definition
accepted_words :: "'alpha list set"
where "accepted_words = {w. w ∈ A⇧⋆ ∧ ((δ⇧⋆) i w) ∈ F}"
lemma induced_g_lang:
"G_lang G A φ accepted_words"
proof-
have H_0: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ∧ (δ⇧⋆) i w ∈ F ⟹ map (φ g) w ∈ A⇧⋆"
apply (clarsimp)
using labels_a_G_set.element_image
by blast
have H_1: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ (δ⇧⋆) i w ∈ F ⟹ (δ⇧⋆) i (map (φ g) w) ∈ F"
proof -
fix g w
assume
A_0: "g ∈ carrier G" and
A_1: "w ∈ A⇧⋆" and
A_2: "(δ⇧⋆) i w ∈ F"
have H1_0: "ψ g ((δ⇧⋆) i w) ∈ F"
using accepting_is_eq_var.eq_var_subset_axioms
A_0 A_2 accepting_is_eq_var.is_equivar
by blast
have H1_1: "ψ g i = i"
using init_is_eq_var.eq_var_subset_axioms A_0
init_is_eq_var.is_equivar
by auto
have H1_2: "⋀w g. ⟦g ∈ carrier G; w ∈ A⇧⋆; (δ⇧⋆) i w ∈ F⟧ ⟹ (φ⇧⋆) g w ∈ A⇧⋆"
using H_0
by auto
from A_1 have H1_3: "w ∈ A⇧⋆"
by auto
show "(δ⇧⋆) i (map (φ g) w) ∈ F"
using give_input_eq_var A_0 A_1 H1_1 H1_3
apply (clarsimp simp del: GMN_simps simp add: eq_var_func_def eq_var_func_axioms_def
make_op_def)
using A_2 H1_0 is_aut.init_state_is_a_state H1_2
by (smt (verit, best) H1_3 labels_a_G_set.induced_star_map_def restrict_apply)
qed
show ?thesis
apply (clarsimp simp del: GMN_simps simp add: G_lang_def accepted_words_def G_lang_axioms_def)
apply (rule conjI)
using labels_a_G_set.alt_grp_act_axioms
apply (auto)[1]
apply (intro conjI)
apply (simp add: language.intro)
apply (rule alt_grp_act.eq_var_one_direction)
using labels_a_G_set.alt_grp_act_axioms labels_a_G_set.lists_a_Gset
apply blast
apply (clarsimp )
apply (clarsimp)
by (simp add: H_0 H_1 in_listsI)
qed
end
locale reach_det_aut =
det_aut A S i F δ
for A :: "'alpha set" (structure) and
S :: "'states set" and
i F δ +
assumes
is_reachable:
"s ∈ S ⟹ ∃input ∈ A⇧⋆. (δ⇧⋆) i input = s"
locale reach_det_G_aut =
det_G_aut A S i F δ G φ ψ + reach_det_aut A S i F δ
for A :: "'alpha set" (structure) and
S :: "'states set" and
i and F and δ and
G :: "('grp, 'b) monoid_scheme" and
φ ψ
begin
text ‹
To avoid duplicate variant of "star":
›
no_adhoc_overloading
star labels_a_G_set.induced_star_map
end
sublocale reach_det_G_aut ⊆ reach_det_aut
using reach_det_aut_axioms
by simp
locale G_aut_hom = Aut0: reach_det_G_aut A S⇩0 i⇩0 F⇩0 δ⇩0 G φ ψ⇩0 +
Aut1: reach_det_G_aut A S⇩1 i⇩1 F⇩1 δ⇩1 G φ ψ⇩1 +
hom_f: aut_hom A S⇩0 i⇩0 F⇩0 δ⇩0 S⇩1 i⇩1 F⇩1 δ⇩1 f +
eq_var_f: eq_var_func G S⇩0 ψ⇩0 S⇩1 ψ⇩1 f for
A :: "'alpha set" and
S⇩0 :: "'states_0 set" and
i⇩0 and F⇩0 and δ⇩0 and
S⇩1 :: "'states_1 set" and
i⇩1 and F⇩1 and δ⇩1 and
G :: "('grp, 'b) monoid_scheme" and
φ ψ⇩0 ψ⇩1 f
locale G_aut_epi = G_aut_hom +
assumes
is_epi: "f ` S⇩0 = S⇩1"
locale det_aut_rec_lang = det_aut A S i F δ + language A L
for A :: "'alpha set" (structure) and
S :: "'states set" and
i F δ L +
assumes
is_recognised:
"w ∈ L ⟷ w ∈ A⇧⋆ ∧ ((δ⇧⋆) i w) ∈ F"
locale det_G_aut_rec_lang = det_G_aut A S i F δ G φ ψ + det_aut_rec_lang A S i F δ L
for A :: "'alpha set" (structure) and
S :: "'states set" and
i F δ and
G :: "('grp, 'b) monoid_scheme" and
φ ψ L
begin
lemma lang_is_G_lang: "G_lang G A φ L"
proof-
have H0: "L = accepted_words"
apply (simp add: accepted_words_def)
apply (subst is_recognised [symmetric])
by simp
show "G_lang G A φ L"
apply (subst H0)
apply (rule det_G_aut.induced_g_lang[of A S i F δ G φ ψ])
by (simp add: det_G_aut_axioms)
qed
text ‹
To avoid ambiguous parse trees:
›
no_notation trans_is_eq_var.GA_0.induced_quot_map ("[_]⇩_ı" 60)
no_notation states_a_G_set.induced_quot_map ("[_]⇩_ı" 60)
end
locale reach_det_aut_rec_lang = reach_det_aut A S i F δ + det_aut_rec_lang A S i F δ L
for A :: "'alpha set" and
S :: "'states set" and
i F δ and
L :: "'alpha list set"
locale reach_det_G_aut_rec_lang = det_G_aut_rec_lang A S i F δ G φ ψ L +
reach_det_G_aut A S i F δ G φ ψ
for A :: "'alpha set" and
S :: "'states set" and
i F δ and
G :: "('grp, 'b) monoid_scheme" and
φ ψ and
L :: "'alpha list set"
sublocale reach_det_G_aut_rec_lang ⊆ det_G_aut_rec_lang
apply (simp add: det_G_aut_rec_lang_def)
using reach_det_G_aut_rec_lang_axioms
by (simp add: det_G_aut_axioms det_aut_rec_lang_axioms)
locale det_G_aut_recog_G_lang = det_G_aut_rec_lang A S i F δ G φ ψ L + G_lang G A φ L
for A :: "'alpha set" (structure) and
S :: "'states set" and
i F δ and
G :: "('grp, 'b) monoid_scheme" and
φ ψ and
L :: "'alpha list set"
sublocale det_G_aut_rec_lang ⊆ det_G_aut_recog_G_lang
apply (simp add: det_G_aut_recog_G_lang_def)
apply (rule conjI)
apply (simp add: det_G_aut_rec_lang_axioms)
by (simp add: lang_is_G_lang)
locale reach_det_G_aut_rec_G_lang = reach_det_G_aut_rec_lang A S i F δ G φ ψ L + G_lang G A φ L
for A :: "'alpha set" (structure) and
S :: "'states set" and
i F δ and
G :: "('grp, 'b) monoid_scheme" and
φ ψ L
sublocale reach_det_G_aut_rec_lang ⊆ reach_det_G_aut_rec_G_lang
apply (simp add: reach_det_G_aut_rec_G_lang_def)
apply (rule conjI)
apply (simp add: reach_det_G_aut_rec_lang_axioms)
by (simp add: lang_is_G_lang)
lemma (in reach_det_G_aut)
"reach_det_G_aut_rec_lang A S i F δ G φ ψ accepted_words"
apply (clarsimp simp del: simp add: reach_det_G_aut_rec_lang_def
det_G_aut_rec_lang_def det_aut_rec_lang_axioms_def)
apply (intro conjI)
apply (simp add: det_G_aut_axioms)
apply (clarsimp simp add: reach_det_G_aut_axioms accepted_words_def reach_det_aut_rec_lang_def)
apply (simp add: det_aut_rec_lang_def det_aut_rec_lang_axioms.intro is_aut.det_aut_axioms
language_def)
by (simp add: reach_det_G_aut_axioms)
lemma (in det_G_aut) action_on_input:
"⋀ g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ ψ g ((δ⇧⋆) i w) = (δ⇧⋆) i ((φ⇧⋆) g w)"
proof-
fix g w
assume
A_0: "g ∈ carrier G" and
A_1: "w ∈ A⇧⋆"
have H_0: "(δ⇧⋆) (ψ g i) ((φ⇧⋆) g w) = (δ⇧⋆) i ((φ⇧⋆) g w)"
using A_0 init_is_eq_var.is_equivar
by fastforce
have H_1: "ψ g ((δ⇧⋆) i w) = (δ⇧⋆) (ψ g i) ((φ⇧⋆) g w)"
using A_0 A_1 give_input_eq_var
apply (clarsimp simp del: GMN_simps simp add: eq_var_func_axioms_def eq_var_func_def
make_op_def)
apply (rule meta_mp[of "((φ⇧⋆) g w) ∈ A⇧⋆ ∧ ψ g i ∈ S"])
using is_aut.init_state_is_a_state A_1
apply presburger
using det_G_aut_axioms
apply (clarsimp simp add: det_G_aut_def)
apply (rule conjI; rule impI; rule conjI)
using labels_a_G_set.element_image
apply fastforce
using is_aut.init_state_is_a_state states_a_G_set.element_image
by blast+
show "ψ g ((δ⇧⋆) i w) = (δ⇧⋆) i ((φ⇧⋆) g w)"
using H_0 H_1
by simp
qed
definition (in det_G_aut)
reachable_states :: "'states set" ("S⇩r⇩e⇩a⇩c⇩h")
where "S⇩r⇩e⇩a⇩c⇩h = {s . ∃ w ∈ A⇧⋆. (δ⇧⋆) i w = s}"
definition (in det_G_aut)
reachable_trans :: "'states ⇒ 'alpha ⇒ 'states" ("δ⇩r⇩e⇩a⇩c⇩h")
where "δ⇩r⇩e⇩a⇩c⇩h s a = (λ(s', a') ∈ S⇩r⇩e⇩a⇩c⇩h × A. δ s' a') (s, a)"
definition (in det_G_aut)
reachable_action :: "'grp ⇒ 'states ⇒ 'states" ("ψ⇩r⇩e⇩a⇩c⇩h")
where "ψ⇩r⇩e⇩a⇩c⇩h g s = (λ(g', s') ∈ carrier G × S⇩r⇩e⇩a⇩c⇩h. ψ g' s') (g, s)"
lemma (in det_G_aut) reachable_action_is_restict:
"⋀g s. g ∈ carrier G ⟹ s ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ ψ⇩r⇩e⇩a⇩c⇩h g s = ψ g s"
by (auto simp add: reachable_action_def reachable_states_def)
lemma (in det_G_aut_rec_lang) reach_det_aut_is_det_aut_rec_L:
"reach_det_G_aut_rec_lang A S⇩r⇩e⇩a⇩c⇩h i (F ∩ S⇩r⇩e⇩a⇩c⇩h) δ⇩r⇩e⇩a⇩c⇩h G φ ψ⇩r⇩e⇩a⇩c⇩h L"
proof-
have H_0: "(λ(x, y). δ⇩r⇩e⇩a⇩c⇩h x y) ∈ S⇩r⇩e⇩a⇩c⇩h × A →⇩E S⇩r⇩e⇩a⇩c⇩h"
proof-
have H1_0: "(λ(x, y). δ x y) ∈ extensional (S × A)"
using is_aut.trans_func_ext
by (simp add: PiE_iff)
have H1_1: "(λ(s', a') ∈ S⇩r⇩e⇩a⇩c⇩h × A. δ s' a') ∈ extensional (S⇩r⇩e⇩a⇩c⇩h × A)"
using H1_0
by simp
have H1_2: "(λ(s', a')∈S⇩r⇩e⇩a⇩c⇩h × A. δ s' a') = (λ(x, y). δ⇩r⇩e⇩a⇩c⇩h x y)"
by (auto simp add: reachable_trans_def)
show "(λ(x, y). δ⇩r⇩e⇩a⇩c⇩h x y) ∈ S⇩r⇩e⇩a⇩c⇩h × A →⇩E S⇩r⇩e⇩a⇩c⇩h"
apply (clarsimp simp add: PiE_iff)
apply (rule conjI)
apply (clarify)
using reachable_trans_def
apply (simp add: reachable_states_def)[1]
apply (metis Cons_in_lists_iff append_Nil2 append_in_lists_conv is_aut.give_input_closed
is_aut.init_state_is_a_state is_aut.trans_to_charact)
using H1_1 H1_2
by simp
qed
have H_1: "⋀g. g ∈ carrier G ⟹
(⋀s. ψ⇩r⇩e⇩a⇩c⇩h g s = (if s ∈ S⇩r⇩e⇩a⇩c⇩h then case (g, s) of (x, xa) ⇒ ψ x xa else undefined)) ⟹
bij_betw (ψ⇩r⇩e⇩a⇩c⇩h g) S⇩r⇩e⇩a⇩c⇩h S⇩r⇩e⇩a⇩c⇩h"
proof-
fix g
assume
A1_0: "g ∈ carrier G" and
A1_1: "(⋀s. ψ⇩r⇩e⇩a⇩c⇩h g s =
(if s ∈ S⇩r⇩e⇩a⇩c⇩h
then case (g, s) of (x, xa) ⇒ ψ x xa
else undefined))"
have H1_0: "⋀r. r ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ (ψ⇩r⇩e⇩a⇩c⇩h g) r ∈ S⇩r⇩e⇩a⇩c⇩h"
using A1_0
apply (clarsimp simp add: reachable_states_def reachable_action_def)
apply (rule meta_mp[of "⋀w. w ∈ A⇧⋆ ⟹ ((φ⇧⋆) g w) ∈ A⇧⋆"])
using action_on_input[where g = g]
apply (metis in_listsI)
by (metis alt_group_act_is_grp_act group_action.element_image labels_a_G_set.lists_a_Gset)
have H1_1: "⋀f T U. bij_betw f T T ⟹ f ` U = U ⟹ U ⊆ T ⟹ bij_betw (restrict f U) U U"
apply (clarsimp simp add: bij_betw_def inj_on_def image_def)
by (meson in_mono)
have H1_2: "ψ⇩r⇩e⇩a⇩c⇩h g = restrict (ψ g) S⇩r⇩e⇩a⇩c⇩h"
using reachable_action_def A1_0
by (auto simp add: restrict_def)
have H1_3: "bij_betw (ψ g) S S ⟹ (ψ⇩r⇩e⇩a⇩c⇩h g) ` S⇩r⇩e⇩a⇩c⇩h = S⇩r⇩e⇩a⇩c⇩h
⟹ S⇩r⇩e⇩a⇩c⇩h ⊆ S ⟹ bij_betw (ψ⇩r⇩e⇩a⇩c⇩h g) S⇩r⇩e⇩a⇩c⇩h S⇩r⇩e⇩a⇩c⇩h"
by (metis H1_2 bij_betw_imp_inj_on inj_on_imp_bij_betw inj_on_restrict_eq inj_on_subset)
have H1_4: "⋀w s. s = (δ⇧⋆) i w ⟹
∀x∈set w. x ∈ A ⟹
∃x. (∃w∈ A⇧⋆. (δ⇧⋆) i w = x) ∧ (δ⇧⋆) i w = ψ⇩r⇩e⇩a⇩c⇩h g x"
proof-
fix w s
assume
A2_0: "∀x∈set w. x ∈ A" and
A2_1: "s = (δ⇧⋆) i w"
have H2_0: "(inv ⇘G⇙ g) ∈ carrier G"
apply (rule meta_mp[of "group G"])
using A1_0
apply simp
using det_G_aut_rec_lang_axioms
by (auto simp add: det_G_aut_rec_lang_def
det_aut_rec_lang_axioms_def det_G_aut_def group_action_def group_hom_def)
have H2_1: "ψ (inv ⇘G⇙ g) s = (δ⇧⋆) i ((φ⇧⋆) (inv ⇘G⇙ g) w)"
apply (simp del: GMN_simps add: A2_1)
apply (rule action_on_input[where g = "(inv ⇘G⇙ g)" and w = w])
using H2_0 A2_0
by auto
have H2_2: "((φ⇧⋆) (inv ⇘G⇙ g) w) ∈ A⇧⋆"
using A2_0 H2_0 det_G_aut_rec_lang_axioms
apply (clarsimp)
using labels_a_G_set.surj_prop list.set_map
by fastforce
have H2_3: "∃w∈A⇧⋆. (δ⇧⋆) i w = ψ (inv ⇘G⇙ g) s"
by (metis H2_1 H2_2)
from H2_3 have H2_4: "ψ (inv ⇘G⇙ g) s ∈ S⇩r⇩e⇩a⇩c⇩h"
by (simp add: reachable_states_def)
have H2_5: "ψ⇩r⇩e⇩a⇩c⇩h g (ψ (inv ⇘G⇙ g) s) = ψ g (ψ (inv ⇘G⇙ g) s)"
apply (rule reachable_action_is_restict)
using A1_0 H2_4
by simp+
have H2_6: "(δ⇧⋆) i w = ψ⇩r⇩e⇩a⇩c⇩h g (ψ (inv ⇘G⇙ g) s)"
apply (simp add: H2_5 A2_1)
by (metis A1_0 A2_0 in_listsI A2_1 H2_5 is_aut.give_input_closed
is_aut.init_state_is_a_state states_a_G_set.bij_prop1 states_a_G_set.orbit_sym_aux)
show " ∃x. (∃w∈A⇧⋆. (δ⇧⋆) i w = x) ∧ (δ⇧⋆) i w = ψ⇩r⇩e⇩a⇩c⇩h g x"
using H2_3 H2_6
by blast
qed
show "bij_betw (ψ⇩r⇩e⇩a⇩c⇩h g) S⇩r⇩e⇩a⇩c⇩h S⇩r⇩e⇩a⇩c⇩h"
apply (rule H1_3)
apply (simp add: A1_0 bij_betw_def states_a_G_set.inj_prop states_a_G_set.surj_prop)
apply (clarsimp simp add: image_def H1_0)
apply (rule subset_antisym; simp add: Set.subset_eq; clarify)
using H1_0
apply auto[1]
subgoal for s
apply (clarsimp simp add: reachable_states_def)
by (simp add: H1_4)
apply (simp add: reachable_states_def Set.subset_eq; rule allI; rule impI)
using is_aut.give_input_closed is_aut.init_state_is_a_state
by auto
qed
have H_2: "group G"
using det_G_aut_rec_lang_axioms
by (auto simp add: det_G_aut_rec_lang_def det_G_aut_def group_action_def
group_hom_def)
have H_3: "⋀g. g ∈ carrier G ⟹ ψ⇩r⇩e⇩a⇩c⇩h g ∈ carrier (BijGroup S⇩r⇩e⇩a⇩c⇩h)"
subgoal for g
using reachable_action_def[where g = g]
apply (simp add: BijGroup_def Bij_def extensional_def)
by (simp add: H_1)
done
have H_4: "⋀x y. x ∈ carrier G ⟹ y ∈ carrier G ⟹ ψ⇩r⇩e⇩a⇩c⇩h (x ⊗⇘G⇙ y) = ψ⇩r⇩e⇩a⇩c⇩h x ⊗⇘BijGroup S⇩r⇩e⇩a⇩c⇩h⇙
ψ⇩r⇩e⇩a⇩c⇩h y"
proof -
fix g h
assume
A1_0: "g ∈ carrier G" and
A1_1: "h ∈ carrier G"
have H1_0: "⋀g . g ∈ carrier G ⟹ ψ⇩r⇩e⇩a⇩c⇩h g = restrict (ψ g) S⇩r⇩e⇩a⇩c⇩h"
using reachable_action_def
by (auto simp add: restrict_def)
from H1_0 have H1_1: "ψ⇩r⇩e⇩a⇩c⇩h (g ⊗⇘G⇙ h) = restrict (ψ (g ⊗⇘G⇙ h)) S⇩r⇩e⇩a⇩c⇩h"
by (simp add: A1_0 A1_1 H_2 group.subgroup_self subgroup.m_closed)
have H1_2: "ψ⇩r⇩e⇩a⇩c⇩h g ⊗⇘BijGroup S⇩r⇩e⇩a⇩c⇩h⇙ ψ⇩r⇩e⇩a⇩c⇩h h =
(restrict (ψ g) S⇩r⇩e⇩a⇩c⇩h) ⊗⇘BijGroup S⇩r⇩e⇩a⇩c⇩h⇙
(restrict (ψ h) S⇩r⇩e⇩a⇩c⇩h)"
using A1_0 A1_1 H1_0
by simp
have H1_3: "⋀g. g ∈ carrier G ⟹ ψ⇩r⇩e⇩a⇩c⇩h g ∈ carrier (BijGroup S⇩r⇩e⇩a⇩c⇩h)"
by (simp add: H_3)
have H1_4: "⋀x y. x∈carrier G ⟹ y∈carrier G ⟹ ψ (x ⊗⇘G⇙ y) = ψ x ⊗⇘BijGroup S⇙ ψ y"
using det_G_aut_axioms
by (simp add: det_G_aut_def group_action_def group_hom_def group_hom_axioms_def hom_def)
hence H1_5: "ψ (g ⊗⇘G⇙ h) = ψ g ⊗⇘BijGroup S⇙ ψ h"
using A1_0 A1_1
by simp
have H1_6: "(λx. if x ∈ S⇩r⇩e⇩a⇩c⇩h
then if (if x ∈ S⇩r⇩e⇩a⇩c⇩h
then ψ h x
else undefined) ∈ S⇩r⇩e⇩a⇩c⇩h
then ψ g (if x ∈ S⇩r⇩e⇩a⇩c⇩h
then ψ h x
else undefined)
else undefined
else undefined) =
(λx. if x ∈ S⇩r⇩e⇩a⇩c⇩h
then ψ g (ψ h x)
else undefined)"
apply (rule meta_mp[of "⋀x. x ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ (ψ h x) ∈ S⇩r⇩e⇩a⇩c⇩h"])
using H1_3[where g1 = h] A1_1 H1_0
by (auto simp add: A1_1 BijGroup_def Bij_def bij_betw_def)
have H1_7: "... = (λx. if x ∈ S⇩r⇩e⇩a⇩c⇩h
then if x ∈ S
then ψ g (ψ h x)
else undefined
else undefined)"
apply (clarsimp simp add: reachable_states_def)
by (metis is_aut.give_input_closed is_aut.init_state_is_a_state)
have H1_8: "(restrict (ψ g) S⇩r⇩e⇩a⇩c⇩h) ⊗⇘BijGroup S⇩r⇩e⇩a⇩c⇩h⇙ (restrict (ψ h) S⇩r⇩e⇩a⇩c⇩h) =
restrict (ψ (g ⊗⇘G⇙ h)) S⇩r⇩e⇩a⇩c⇩h"
apply (rule meta_mp[of "⋀g. g ∈ carrier G ⟹ restrict (ψ g) S⇩r⇩e⇩a⇩c⇩h ∈ Bij S⇩r⇩e⇩a⇩c⇩h ∧
ψ g ∈ Bij S"])
apply (clarsimp simp add: H1_5 BijGroup_def; intro conjI; intro impI)
subgoal
using A1_0 A1_1
apply (clarsimp simp add: compose_def restrict_def)
by (simp add: H1_6 H1_7)
apply (simp add: A1_0 A1_1)+
subgoal for g
using H1_3[where g1 = g] H1_0[of g]
by (simp add: BijGroup_def states_a_G_set.bij_prop0)
done
show "ψ⇩r⇩e⇩a⇩c⇩h (g ⊗⇘G⇙ h) =
ψ⇩r⇩e⇩a⇩c⇩h g ⊗⇘BijGroup S⇩r⇩e⇩a⇩c⇩h⇙ ψ⇩r⇩e⇩a⇩c⇩h h"
by (simp add: H1_1 H1_2 H1_8)
qed
have H_5: "⋀w' w g. g ∈ carrier G ⟹
(δ⇧⋆) i w ∈ F ⟹ ∀x∈set w. x ∈ A ⟹ (δ⇧⋆) i w' = (δ⇧⋆) i w ⟹ ∀x∈set w'. x ∈ A ⟹
∃w'∈ A⇧⋆. (δ⇧⋆) i w' = ψ g ((δ⇧⋆) i w)"
proof -
fix w' w g
assume
A1_0: "g ∈ carrier G" and
A1_1: "(δ⇧⋆) i w ∈ F" and
A1_2: "∀x∈set w. x ∈ A" and
A1_3: "(δ⇧⋆) i w' = (δ⇧⋆) i w" and
A1_4: "∀x∈set w. x ∈ A"
from A1_1 A1_2 have H1_0: "((δ⇧⋆) i w) ∈ S⇩r⇩e⇩a⇩c⇩h"
using reachable_states_def
by auto
have H1_1: "ψ g ((δ⇧⋆) i w) = ((δ⇧⋆) i ((φ⇧⋆) g w))"
using give_input_eq_var
apply (clarsimp simp add: eq_var_func_def eq_var_func_axioms_def simp del: GMN_simps)
using A1_0 A1_2 action_on_input
by blast
have H1_2: "(φ⇧⋆) g w ∈ A⇧⋆"
using A1_0 A1_2
by (metis in_listsI alt_group_act_is_grp_act group_action.element_image
labels_a_G_set.lists_a_Gset)
show "∃wa∈A⇧⋆. (δ⇧⋆) i wa = ψ g ((δ⇧⋆) i w)"
by (metis H1_1 H1_2)
qed
have H_6: "alt_grp_act G S⇩r⇩e⇩a⇩c⇩h ψ⇩r⇩e⇩a⇩c⇩h"
apply (clarsimp simp add: group_action_def group_hom_def group_hom_axioms_def hom_def)
apply (intro conjI)
apply (simp add: H_2)
subgoal
by (simp add: group_BijGroup)
apply clarify
apply (simp add: H_3)
by (simp add: H_4)
have H_7: "⋀g w. g ∈ carrier G ⟹ (δ⇧⋆) i w ∈ F ⟹ ∀x∈set w. x ∈ A ⟹
∃x. x ∈ F ∧ (∃w∈A⇧⋆. (δ⇧⋆) i w = x) ∧ (δ⇧⋆) i w = ψ g x"
proof-
fix g w
assume
A1_0: "g ∈ carrier G" and
A1_1: "(δ⇧⋆) i w ∈ F" and
A1_2: "∀x∈set w. x ∈ A"
have H1_0: "(inv ⇘G⇙ g) ∈ carrier G"
by (meson A1_0 group.inv_closed group_hom.axioms(1) labels_a_G_set.group_hom)
have H1_1: "((δ⇧⋆) i w) ∈ S⇩r⇩e⇩a⇩c⇩h"
using A1_1 A1_2 reachable_states_def
by auto
have H1_2: "ψ⇩r⇩e⇩a⇩c⇩h (inv ⇘G⇙ g) ((δ⇧⋆) i w) = ψ (inv ⇘G⇙ g) ((δ⇧⋆) i w)"
apply (rule reachable_action_is_restict)
using H1_0 H1_1
by auto
have H1_3: "ψ⇩r⇩e⇩a⇩c⇩h g (ψ (inv ⇘G⇙ g) ((δ⇧⋆) i w)) = ((δ⇧⋆) i w)"
by (smt (verit) A1_0 H1_1 H_6 H1_2
alt_group_act_is_grp_act group_action.bij_prop1 group_action.orbit_sym_aux)
have H1_4: "ψ (inv ⇘G⇙ g) ((δ⇧⋆) i w) ∈ F"
using A1_1 H1_0 accepting_is_eq_var.is_equivar
by blast
have H1_5: "ψ (inv ⇘G⇙ g) ((δ⇧⋆) i w) ∈ F ∧ (δ⇧⋆) i w = ψ g (ψ (inv ⇘G⇙ g) ((δ⇧⋆) i w))"
using H1_4 H1_3 A1_0 A1_1 H1_0 H1_1 reachable_action_is_restict
by (metis H_6 alt_group_act_is_grp_act
group_action.element_image)
have H1_6: "ψ (inv ⇘G⇙ g) ((δ⇧⋆) i w) = ((δ⇧⋆) i ((φ⇧⋆) (inv ⇘G⇙ g) w))"
using give_input_eq_var
apply (clarsimp simp add: eq_var_func_def eq_var_func_axioms_def simp del: GMN_simps)
using A1_2 H1_0 action_on_input
by blast
have H1_7: "(φ⇧⋆) (inv ⇘G⇙ g) w ∈ A⇧⋆"
by (metis A1_2 in_listsI H1_0 alt_group_act_is_grp_act group_action.element_image
labels_a_G_set.lists_a_Gset)
thus "∃x. x ∈ F ∧ (∃w∈A⇧⋆. (δ⇧⋆) i w = x) ∧ (δ⇧⋆) i w = ψ g x"
using H1_5 H1_6 H1_7
by metis
qed
have H_8: "⋀r a g . r ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ a ∈ A ⟹ ψ⇩r⇩e⇩a⇩c⇩h g r ∈ S⇩r⇩e⇩a⇩c⇩h ∧ φ g a ∈ A ⟹ g ∈ carrier G ⟹
δ⇩r⇩e⇩a⇩c⇩h (ψ⇩r⇩e⇩a⇩c⇩h g r) (φ g a) = ψ⇩r⇩e⇩a⇩c⇩h g (δ⇩r⇩e⇩a⇩c⇩h r a)"
proof-
fix r a g
assume
A1_0: "r ∈ S⇩r⇩e⇩a⇩c⇩h" and
A1_1: "a ∈ A" and
A1_2: "ψ⇩r⇩e⇩a⇩c⇩h g r ∈ S⇩r⇩e⇩a⇩c⇩h ∧ φ g a ∈ A" and
A1_3: "g ∈ carrier G"
have H1_0: "r ∈ S ∧ ψ g r ∈ S"
apply (rule conjI)
subgoal
using A1_0
apply (clarsimp simp add: reachable_states_def)
by (simp add: in_listsI is_aut.give_input_closed is_aut.init_state_is_a_state)
using ‹r ∈ S› A1_3 states_a_G_set.element_image
by blast
have H1_1: "⋀a b g . a ∈ S ∧ b ∈ A ⟹ g ∈ carrier G ⟹
(if ψ g a ∈ S ∧ φ g b ∈ A then δ (ψ g a) (φ g b) else undefined) =
ψ g (δ a b)"
using det_G_aut_axioms A1_0 A1_1 A1_3
apply (clarsimp simp add: det_G_aut_def eq_var_func_def eq_var_func_axioms_def)
by presburger+
hence H1_2: "ψ g (δ r a) = (δ (ψ g r) (φ g a))"
using H1_1[where a1 = r and b1 = a and g1 = g] H1_0 A1_1 A1_2 A1_3
by simp
have H1_3: "⋀a w. a ∈ A ⟹ w ∈ A⇧⋆ ⟹ ∃w'∈ A⇧⋆. (δ⇧⋆) i w' = δ ((δ⇧⋆) i w) a"
proof -
fix a w
assume
A2_0: "a ∈ A" and
A2_1: "w ∈ A⇧⋆"
have H2_0: "(w @ [a]) ∈ A⇧⋆ ∧ (w @ [a]) ∈ A⇧⋆ ⟹ (δ⇧⋆) i (w @ [a]) = δ ((δ⇧⋆) i w) a"
by (simp add: is_aut.give_input_closed is_aut.trans_to_charact
is_aut.init_state_is_a_state)
show "∃w'∈A⇧⋆. (δ⇧⋆) i w' = δ ((δ⇧⋆) i w) a"
using H2_0
apply clarsimp
by (metis A2_0 A2_1 append_in_lists_conv lists.Cons lists.Nil)
qed
have H1_4: "ψ⇩r⇩e⇩a⇩c⇩h g (δ⇩r⇩e⇩a⇩c⇩h r a) = ψ g (δ r a)"
apply (clarsimp simp add: reachable_action_def reachable_trans_def)
using A1_0 A1_1 A1_3 H1_0 H1_3
using reachable_states_def by fastforce
have H1_5:"ψ g r = ψ⇩r⇩e⇩a⇩c⇩h g r"
using A1_0 A1_3
by (auto simp add: reachable_action_def)
hence H1_6: "ψ g r ∈ S⇩r⇩e⇩a⇩c⇩h"
using A1_2
by simp
have H1_7: "δ⇩r⇩e⇩a⇩c⇩h (ψ⇩r⇩e⇩a⇩c⇩h g r) (φ g a) = δ (ψ g r) (φ g a)"
using A1_0 A1_1 A1_2 A1_3
by (auto simp del: simp add:reachable_trans_def reachable_action_def )
show "δ⇩r⇩e⇩a⇩c⇩h (ψ⇩r⇩e⇩a⇩c⇩h g r) (φ g a) = ψ⇩r⇩e⇩a⇩c⇩h g (δ⇩r⇩e⇩a⇩c⇩h r a)"
using H1_2 H1_4 H1_7
by auto
qed
have H_9: "⋀a w s. ⟦(⋀s. s ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ (δ⇧⋆) s w = (δ⇩r⇩e⇩a⇩c⇩h⇧⋆) s w);
a ∈ A ∧ (∀x∈set w. x ∈ A); s ∈ S⇩r⇩e⇩a⇩c⇩h⟧ ⟹ (δ⇧⋆) (δ s a) w = (δ⇩r⇩e⇩a⇩c⇩h⇧⋆) (δ⇩r⇩e⇩a⇩c⇩h s a) w"
proof-
fix a w s
assume
A1_IH: "(⋀s. s ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ (δ⇧⋆) s w = (δ⇩r⇩e⇩a⇩c⇩h⇧⋆) s w)" and
A1_0: "a ∈ A ∧ (∀x∈set w. x ∈ A)" and
A1_1: "s ∈ S⇩r⇩e⇩a⇩c⇩h"
have H1_0: "δ⇩r⇩e⇩a⇩c⇩h s a = δ s a"
using A1_1
apply (clarsimp simp add: reachable_trans_def)
apply (rule meta_mp[of "det_aut A S i F δ"])
using det_aut.trans_func_ext[where labels = A and states = S and
init_state = i and fin_states = F and trans_func = δ]
apply (simp add: extensional_def)
by (auto simp add: A1_0)
show "(δ⇧⋆) (δ s a) w = (δ⇩r⇩e⇩a⇩c⇩h⇧⋆) (δ⇩r⇩e⇩a⇩c⇩h s a) w"
apply (simp add: H1_0)
apply (rule A1_IH[where s1 = "δ s a"])
using A1_0 A1_1
apply (simp add: reachable_states_def)
by (metis Cons_in_lists_iff append_Nil2 append_in_lists_conv is_aut.give_input_closed
is_aut.init_state_is_a_state is_aut.trans_to_charact)
qed
show ?thesis
apply (clarsimp simp del: GMN_simps simp add: reach_det_G_aut_rec_lang_def
det_G_aut_rec_lang_def det_G_aut_def det_aut_def)
apply (intro conjI)
subgoal
apply (simp add: reachable_states_def)
by (meson give_input.simps(1) lists.Nil)
apply (simp add: H_0)
using labels_a_G_set.alt_grp_act_axioms
apply (auto)[1]
apply (rule H_6)
subgoal
apply (clarsimp simp add: eq_var_subset_def eq_var_subset_axioms_def)
apply (rule conjI)
using H_6
apply (auto)[1]
apply (simp del: add: reachable_states_def)[1]
apply (clarify; rule subset_antisym; simp add: Set.subset_eq; clarify)
apply (rule conjI)
subgoal for g _ w
apply (clarsimp simp add: reachable_action_def reachable_states_def)
using accepting_is_eq_var.is_equivar
by blast
subgoal for g _ w
apply (clarsimp simp add: reachable_action_def reachable_states_def)
apply (rule conjI; clarify)
apply (auto)[2]
by (simp add: H_5)
apply (clarsimp simp add: reachable_states_def Int_def reachable_action_def )
apply (clarsimp simp add: image_def)
by (simp add: H_7)
subgoal
apply (clarsimp simp add: eq_var_subset_def)
apply (rule conjI)
using H_6
apply (auto)[1]
apply (clarsimp simp add: eq_var_subset_axioms_def)
apply (simp add: ‹i ∈ S⇩r⇩e⇩a⇩c⇩h›)
apply (simp add: reachable_action_def)
using ‹i ∈ S⇩r⇩e⇩a⇩c⇩h› init_is_eq_var.is_equivar
by fastforce
subgoal
apply (clarsimp simp add: eq_var_func_def eq_var_func_axioms_def)
apply (intro conjI)
using H_6 alt_grp_act.axioms
labels_a_G_set.group_action_axioms prod_group_act labels_a_G_set.alt_grp_act_axioms
apply blast
using H_6
apply (auto)[1]
apply (rule funcsetI; clarsimp)
subgoal for s a
apply (clarsimp simp add: reachable_states_def reachable_trans_def)
by (metis Cons_in_lists_iff append_Nil2 append_in_lists_conv in_listsI
is_aut.give_input_closed is_aut.init_state_is_a_state is_aut.trans_to_charact)
apply (intro allI; clarify; rule conjI; intro impI)
apply (simp add: H_8)
using G_set_equiv H_6 eq_var_subset.is_equivar
labels_a_G_set.element_image
by fastforce
apply (rule meta_mp[of "⋀w s. w ∈ A⇧⋆ ⟹ s ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ (δ⇧⋆) s w = (δ⇩r⇩e⇩a⇩c⇩h⇧⋆) s w"])
subgoal
using det_G_aut_rec_lang_axioms
apply (clarsimp simp add: det_aut_rec_lang_axioms_def det_aut_rec_lang_def
det_G_aut_rec_lang_def det_aut_def)
apply (intro conjI)
using ‹i ∈ S⇩r⇩e⇩a⇩c⇩h›
apply blast
using H_0
apply blast
by (metis (mono_tags, lifting) ‹i ∈ S⇩r⇩e⇩a⇩c⇩h› mem_Collect_eq reachable_states_def)
subgoal for w s
apply (induction w arbitrary: s)
apply (clarsimp)
apply (simp add: in_lists_conv_set)
by (simp add: H_9)
apply (clarsimp simp add: reach_det_G_aut_def det_G_aut_def det_aut_def)
apply (intro conjI)
apply (simp add: ‹i ∈ S⇩r⇩e⇩a⇩c⇩h›)
apply (simp add: H_0)
apply (simp add: labels_a_G_set.group_action_axioms)
using ‹alt_grp_act G S⇩r⇩e⇩a⇩c⇩h ψ⇩r⇩e⇩a⇩c⇩h›
apply (auto)[1]
apply (simp add: ‹eq_var_subset G S⇩r⇩e⇩a⇩c⇩h ψ⇩r⇩e⇩a⇩c⇩h (F ∩ S⇩r⇩e⇩a⇩c⇩h)›)
apply (simp add: ‹eq_var_subset G S⇩r⇩e⇩a⇩c⇩h ψ⇩r⇩e⇩a⇩c⇩h {i}›)
using ‹eq_var_func G (S⇩r⇩e⇩a⇩c⇩h × A) (λg∈carrier G. λ(s, a)∈S⇩r⇩e⇩a⇩c⇩h × A. (ψ⇩r⇩e⇩a⇩c⇩h g s, φ g a))
S⇩r⇩e⇩a⇩c⇩h ψ⇩r⇩e⇩a⇩c⇩h (λ(x, y)∈S⇩r⇩e⇩a⇩c⇩h × A. δ⇩r⇩e⇩a⇩c⇩h x y)›
apply blast
apply (simp add: reach_det_aut_axioms_def reach_det_aut_def reachable_states_def)
apply (rule meta_mp[of "⋀s input. s ∈ S⇩r⇩e⇩a⇩c⇩h ⟹ input ∈ A⇧⋆ ⟹
(δ⇩r⇩e⇩a⇩c⇩h⇧⋆) s input = (δ⇧⋆) s input"])
using ‹i ∈ S⇩r⇩e⇩a⇩c⇩h›
apply (metis (no_types, lifting) ‹(⋀w s. ⟦w ∈ A⇧⋆; s ∈ S⇩r⇩e⇩a⇩c⇩h⟧ ⟹
(δ⇧⋆) s w = (δ⇩r⇩e⇩a⇩c⇩h⇧⋆) s w) ⟹ det_aut_rec_lang A S⇩r⇩e⇩a⇩c⇩h i (F ∩ S⇩r⇩e⇩a⇩c⇩h) δ⇩r⇩e⇩a⇩c⇩h L› det_aut_rec_lang_def
reachable_states_def)
by (simp add: ‹⋀w s. ⟦w ∈ A⇧⋆; s ∈ S⇩r⇩e⇩a⇩c⇩h⟧ ⟹ (δ⇧⋆) s w = (δ⇩r⇩e⇩a⇩c⇩h⇧⋆) s w›)
qed
subsection ‹
Syntactic Automaton
›
context language begin
definition
rel_MN :: "('alpha list × 'alpha list) set" ("≡⇩M⇩N")
where "rel_MN = {(w, w') ∈ (A⇧⋆)×(A⇧⋆). (∀v ∈ A⇧⋆. (w @ v) ∈ L ⟷ (w' @ v) ∈ L)}"
lemma MN_rel_equival:
"equiv (A⇧⋆) rel_MN"
by (auto simp add: rel_MN_def equiv_def refl_on_def sym_def trans_def)
abbreviation
MN_equiv
where "MN_equiv ≡ A⇧⋆ // rel_MN"
definition
alt_natural_map_MN :: "'alpha list ⇒ 'alpha list set " ("[_]⇩M⇩N")
where "[w]⇩M⇩N = rel_MN `` {w}"
definition
MN_trans_func :: "('alpha list set) ⇒ 'alpha ⇒ 'alpha list set" ("δ⇩M⇩N")
where "MN_trans_func W' a' =
(λ(W,a) ∈ MN_equiv × A. rel_MN `` {(SOME w. w ∈ W) @ [a]}) (W', a')"
abbreviation
MN_init_state
where "MN_init_state ≡ [Nil::'alpha list]⇩M⇩N"
abbreviation
MN_fin_states
where "MN_fin_states ≡ {v. ∃w∈L. v = [w]⇩M⇩N}"
lemmas
alt_natural_map_MN_def [simp, GMN_simps]
MN_trans_func_def [simp, GMN_simps]
end
context G_lang begin
adhoc_overloading
star induced_star_map
lemma MN_quot_act_wd:
"w' ∈ [w]⇩M⇩N ⟹ ∀g ∈ carrier G. (g ⊙ ⇘φ⇧⋆⇙ w') ∈ [g ⊙ ⇘φ⇧⋆⇙ w]⇩M⇩N"
proof-
assume A_0: "w' ∈ [w]⇩M⇩N"
have H_0: "⋀g. ⟦(w, w') ∈ ≡⇩M⇩N; g ∈ carrier G; group_hom G (BijGroup A) φ;
group_hom G (BijGroup (A⇧⋆)) (λg∈carrier G. restrict (map (φ g)) (A⇧⋆)); L ⊆ A⇧⋆;
∀g∈carrier G. map (φ g) ` (L ∩ A⇧⋆) ∪ (λx. undefined) ` (L ∩ {x. x ∉ A⇧⋆}) = L;
∀x∈set w. x ∈ A; w' ∈ A⇧⋆⟧ ⟹ (map (φ g) w, map (φ g) w') ∈ ≡⇩M⇩N"
proof-
fix g
assume
A1_0: "(w, w') ∈ ≡⇩M⇩N" and
A1_1: "g ∈ carrier G" and
A1_2: "group_hom G (BijGroup A) φ" and
A1_3: "group_hom G (BijGroup (A⇧⋆)) (λg∈carrier G. restrict (map (φ g)) (A⇧⋆))" and
A1_4: "L ⊆ A⇧⋆" and
A1_5: "∀g∈carrier G.
map (φ g) ` (L ∩ A⇧⋆) ∪ (λx. undefined) ` (L ∩ {x. x ∉ A⇧⋆}) = L" and
A1_6: "∀x∈set w. x ∈ A" and
A1_7: "w' ∈ A⇧⋆"
have H1_0: "⋀v w w'. ⟦g ∈ carrier G; group_hom G (BijGroup A) φ;
group_hom G (BijGroup (A⇧⋆)) (λg∈carrier G. restrict (map (φ g)) (A⇧⋆));
L ⊆ A⇧⋆; ∀g∈carrier G.
{y. ∃x∈L ∩ A⇧⋆. y = map (φ g) x} ∪ {y. y = undefined ∧ (∃x. x ∈ L ∧ x ∉ A⇧⋆)} = L;
∀x∈set w. x ∈ A; ∀v∈A⇧⋆. (w @ v ∈ L) = (w' @ v ∈ L); ∀x∈set w'. x ∈ A; ∀x∈set v. x ∈ A;
map (φ g) w @ v ∈ L⟧ ⟹ map (φ g) w' @ v ∈ L"
proof -
fix v w w'
assume
A2_0: "g ∈ carrier G" and
A2_1: "L ⊆ A⇧⋆" and
A2_2: "group_hom G (BijGroup A) φ" and
A2_3: "group_hom G (BijGroup (A⇧⋆)) (λg∈carrier G. restrict (map (φ g)) (A⇧⋆))" and
A2_4: "∀g∈carrier G. {y. ∃x∈L ∩ A⇧⋆. y = map (φ g) x} ∪
{y. y = undefined ∧ (∃x. x ∈ L ∧ x ∉ A⇧⋆)} = L" and
A2_5: "∀x∈set w. x ∈ A" and
A2_6: "∀x∈set w'. x ∈ A" and
A2_7: "∀v∈A⇧⋆. (w @ v ∈ L) = (w' @ v ∈ L)" and
A2_8: "∀x∈set v. x ∈ A" and
A2_9: "map (φ g) w @ v ∈ L"
have H2_0: "∀g∈carrier G. {y. ∃x∈L ∩ A⇧⋆. y = map (φ g) x} = L"
using A2_1 A2_4 subset_eq
by (smt (verit, ccfv_SIG) Collect_mono_iff sup.orderE)
hence H2_1: "∀g∈carrier G. {y. ∃x∈L. y = map (φ g) x} = L"
using A2_1 inf.absorb_iff1
by (smt (verit, ccfv_SIG) Collect_cong)
hence H2_2: "∀g∈carrier G.∀x∈L. map (φ g) x ∈ L"
by auto
from A2_2 have H2_3: "∀h∈carrier G. ∀a∈A. (φ h) a ∈ A"
by (auto simp add: group_hom_def BijGroup_def group_hom_axioms_def hom_def Bij_def
bij_betw_def)
from A2_8 have H2_4: "v ∈ A⇧⋆"
by (simp add: in_listsI)
hence H2_5: "∀h∈carrier G. map (φ h) v ∈ A⇧⋆"
using H2_3
by fastforce
hence H2_6: "∀h∈carrier G. (w @ (map (φ h) v) ∈ L) = (w' @ (map (φ h) v) ∈ L)"
using A2_7
by force
hence H2_7: "(w @ (map (φ (inv⇘G⇙ g)) v) ∈ L) = (w' @ (map (φ (inv⇘G⇙ g)) v) ∈ L)"
using A2_0
by (meson A2_7 A2_1 append_in_lists_conv in_mono)
have "(map (φ g) w) ∈ (A⇧⋆)"
using A2_0 A2_2 A2_5 H2_3
by (auto simp add: group_hom_def group_hom_axioms_def hom_def BijGroup_def Bij_def
bij_betw_def)
hence H2_8: "∀w∈A⇧⋆. ∀g∈carrier G. map (φ (inv⇘G⇙ g)) ((map (φ g) w) @ v) =
w @ (map (φ (inv⇘G⇙ g)) v)"
using act_maps_n_distrib triv_act_map A2_0 A2_2 A2_3 H2_4
apply (clarsimp)
by (smt (verit, del_insts) comp_apply group_action.intro group_action.orbit_sym_aux map_idI)
have H2_9: "map (φ (inv⇘G⇙ g)) ((map (φ g) w) @ v) ∈ L"
using A2_9 H2_1 H2_2 A2_1
apply clarsimp
by (metis A2_0 A2_2 group.inv_closed group_hom.axioms(1) list.map_comp map_append)
hence H2_10: "w @ (map (φ (inv⇘G⇙ g)) v) ∈ L"
using H2_8 A2_0
by (auto simp add: A2_5 in_listsI)
hence H2_11: "w' @ (map (φ (inv⇘G⇙ g)) v) ∈ L"
using H2_7
by simp
hence H2_12: "map (φ (inv⇘G⇙ g)) ((map (φ g) w') @ v) ∈ L"
using A2_0 H2_8 A2_1 subsetD
by (metis append_in_lists_conv)
have H2_13: "∀g∈carrier G. restrict (map (φ g)) (A⇧⋆) ∈ Bij (A⇧⋆)"
using alt_grp_act.lists_a_Gset[where G = "G" and X = "A" and φ = "φ"] A1_3
by (auto simp add: group_action_def
group_hom_def group_hom_axioms_def Pi_def hom_def BijGroup_def)
have H2_14: "∀g∈carrier G. restrict (map (φ g)) L ` L = L"
using H2_2
apply (clarsimp simp add: Set.image_def)
using H2_1
by blast
have H2_15: "map (φ g) w' ∈ A⇧⋆"
using A2_0 A2_1 H2_13 H2_2
by (metis H2_11 append_in_lists_conv image_eqI lists_image subset_eq surj_prop)
have H2_16: "inv⇘G⇙ g ∈ carrier G"
by (metis A2_0 A2_2 group.inv_closed group_hom.axioms(1))
thus "map (φ g) w' @ v ∈ L"
using A2_0 A2_1 A2_2 H2_4 H2_12 H2_13 H2_14 H2_15 H2_16 group.inv_closed group_hom.axioms(1)
alt_grp_act.lists_a_Gset[where G = "G" and X = "A" and φ = "φ"]
pre_image_lemma[where S = "L" and T = "A⇧⋆" and f = "map (φ (inv⇘G⇙ g))" and
x = "((map (φ g) w') @ v)"]
apply (clarsimp simp add: group_action_def)
by (smt (verit, best) A2_1 FuncSet.restrict_restrict H2_14 H2_15 H2_16 H2_4
append_in_lists_conv inf.absorb_iff2 map_append map_map pre_image_lemma restrict_apply'
restrict_apply')
qed
show "(map (φ g) w, map (φ g) w') ∈ ≡⇩M⇩N"
apply (clarsimp simp add: rel_MN_def Set.image_def)
apply (intro conjI)
using A1_1 A1_6 group_action.surj_prop group_action_axioms
apply fastforce
using A1_1 A1_7 image_iff surj_prop
apply fastforce
apply (clarify; rule iffI)
subgoal for v
apply (rule H1_0[where v1 ="v" and w1 = "w" and w'1 = "w'"])
using A1_0 A1_1 A1_2 A1_3 A1_4 A1_5 A1_6 A1_7
by (auto simp add: rel_MN_def Set.image_def)
apply (rule H1_0[where w1 = "w'" and w'1 = "w"])
using A1_0 A1_1 A1_2 A1_3 A1_4 A1_5 A1_6 A1_7
by (auto simp add: rel_MN_def Set.image_def)
qed
show ?thesis
using G_lang_axioms A_0
apply (clarsimp simp add: G_lang_def G_lang_axioms_def eq_var_subset_def
eq_var_subset_axioms_def alt_grp_act_def group_action_def)
apply (intro conjI; clarify)
apply (rule conjI; rule impI)
apply (simp add: H_0)
by (auto simp add: rel_MN_def)
qed
text ‹
The following lemma corresponds to lemma 3.4 from \cite{bojanczyk2014automata}:
›
lemma MN_rel_eq_var:
"eq_var_rel G (A⇧⋆) (φ⇧⋆) ≡⇩M⇩N"
apply (clarsimp simp add: eq_var_rel_def alt_grp_act_def eq_var_rel_axioms_def)
apply (intro conjI)
apply (metis L_is_equivar alt_grp_act.axioms eq_var_subset.axioms(1) induced_star_map_def)
using L_is_equivar
apply (simp add: rel_MN_def eq_var_subset_def eq_var_subset_axioms_def)
apply fastforce
apply (clarify)
apply (intro conjI; rule impI; rule conjI; rule impI)
apply (simp add: in_lists_conv_set)
apply (clarsimp simp add: rel_MN_def)
apply (intro conjI)
apply (clarsimp simp add: rel_MN_def)
subgoal for w v g w'
using L_is_equivar
apply (clarsimp simp add: restrict_def eq_var_subset_def eq_var_subset_axioms_def)
by (meson element_image)
apply(metis image_mono in_listsI in_mono list.set_map lists_mono subset_code(1) surj_prop)
apply (clarify; rule iffI)
subgoal for w v g u
using G_lang_axioms MN_quot_act_wd[where w = "w" and w'= "v"]
by (auto simp add: rel_MN_def G_lang_def G_lang_axioms_def
eq_var_subset_def eq_var_subset_axioms_def Set.subset_eq element_image)
subgoal for w v g u
using G_lang_axioms MN_quot_act_wd[where w = "w" and w'= "v"]
by (auto simp add: rel_MN_def G_lang_def G_lang_axioms_def
eq_var_subset_def eq_var_subset_axioms_def Set.subset_eq element_image)
using G_lang_axioms MN_quot_act_wd
by (auto simp add: rel_MN_def G_lang_def G_lang_axioms_def
eq_var_subset_def eq_var_subset_axioms_def Set.subset_eq element_image)
lemma quot_act_wd_alt_notation:
"w ∈ A⇧⋆ ⟹ g ∈ carrier G ⟹ g ⊙⇘[φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆⇙⇙ ([w]⇩M⇩N) = ([g ⊙⇘φ⇧⋆⇙ w]⇩M⇩N)"
using eq_var_rel.quot_act_wd[where G = G and φ = "φ⇧⋆" and X = "A⇧⋆" and R = "≡⇩M⇩N" and x = w
and g = g]
by (simp del: GMN_simps add: alt_natural_map_MN_def MN_rel_eq_var MN_rel_equival)
lemma MN_trans_func_characterization:
"v ∈ (A⇧⋆) ⟹ a ∈ A ⟹ δ⇩M⇩N [v]⇩M⇩N a = [v @ [a]]⇩M⇩N"
proof-
assume
A_0: "v ∈ (A⇧⋆)" and
A_1: "a ∈ A"
have H_0: "⋀u. u ∈ [v]⇩M⇩N ⟹ (u @ [a]) ∈ [v @ [a]]⇩M⇩N"
by (auto simp add: rel_MN_def A_1 A_0)
hence H_1: "(SOME w. (v, w) ∈ ≡⇩M⇩N) ∈ [v]⇩M⇩N ⟹ ((SOME w. (v, w) ∈ ≡⇩M⇩N) @ [a]) ∈ [v @ [a]]⇩M⇩N"
by auto
from A_0 have "(v, v) ∈ ≡⇩M⇩N ∧ v ∈ [v]⇩M⇩N"
by (auto simp add: rel_MN_def)
hence H_2: "(SOME w. (v, w) ∈ ≡⇩M⇩N) ∈ [v]⇩M⇩N"
apply (clarsimp simp add: rel_MN_def)
apply (rule conjI)
apply (smt (verit, ccfv_SIG) A_0 in_listsD verit_sko_ex_indirect)
by (smt (verit, del_insts) A_0 in_listsI tfl_some)
hence H_3: " ((SOME w. (v, w) ∈ ≡⇩M⇩N) @ [a]) ∈ [v @ [a]]⇩M⇩N"
using H_1
by simp
thus "δ⇩M⇩N [v]⇩M⇩N a = [v @ [a]]⇩M⇩N"
using A_0 A_1 MN_rel_equival
apply (clarsimp simp add: equiv_def)
apply (rule conjI; rule impI)
apply (metis MN_rel_equival equiv_class_eq)
by (simp add: A_0 quotientI)
qed
lemma MN_trans_eq_var_func :
"eq_var_func G
(MN_equiv × A) (λg∈carrier G. λ(W, a) ∈ (MN_equiv × A). (([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g W, φ g a))
MN_equiv ([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙)
(λ(w, a) ∈ MN_equiv × A. δ⇩M⇩N w a)"
proof-
have H_0: "alt_grp_act G MN_equiv ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙)"
using MN_rel_eq_var MN_rel_equival eq_var_rel.quot_act_is_grp_act
alt_group_act_is_grp_act restrict_apply
by fastforce
have H_1: "⋀a b g.
a ∈ MN_equiv ⟹
b ∈ A ⟹
(([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g a ∈ MN_equiv ∧ φ g b ∈ A ⟶
g ∈ carrier G ⟶ δ⇩M⇩N (([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g a) (φ g b) = ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g (δ⇩M⇩N a b)) ∧
((([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g a ∈ MN_equiv ⟶ φ g b ∉ A) ⟶
g ∈ carrier G ⟶ undefined = ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g (δ⇩M⇩N a b))"
proof -
fix C a g
assume
A1_0: "C ∈ MN_equiv" and
A1_1: "a ∈ A"
have H1_0: "g ∈ carrier G ⟹ φ g a ∈ A"
by (meson A1_1 element_image)
from A1_0 obtain c where H1_c: "[c]⇩M⇩N = C ∧ c ∈ A⇧⋆"
by (auto simp add: quotient_def)
have H1_1: "g ∈ carrier G ⟹ δ⇩M⇩N (([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C) (φ g a) = ([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (δ⇩M⇩N [c]⇩M⇩N a)"
proof-
assume
A2_0: "g ∈ carrier G"
have H2_0: "φ g a ∈ A"
using H1_0 A2_0
by simp
have H2_1: "(φ⇧⋆) g ∈ Bij (A⇧⋆)" using G_lang_axioms lists_a_Gset A2_0
apply (clarsimp simp add: G_lang_def G_lang_axioms_def group_action_def
group_hom_def hom_def group_hom_axioms_def BijGroup_def image_def)
by (meson Pi_iff restrict_Pi_cancel)
hence H2_2: "(φ⇧⋆) g c ∈ (A⇧⋆)"
using H1_c
apply (clarsimp simp add: Bij_def bij_betw_def inj_on_def Image_def image_def)
apply (rule conjI; rule impI; clarify)
using surj_prop
apply fastforce
using A2_0
by blast
from H1_c have H2_1: "([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g (≡⇩M⇩N `` {c}) = ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C"
by auto
also have H2_2: "([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C = [(φ⇧⋆) g c]⇩M⇩N"
using eq_var_rel.quot_act_wd[where R = "≡⇩M⇩N" and G = G and X = "A⇧⋆" and φ = "φ⇧⋆" and g = g
and x = c]
by (clarsimp simp del: GMN_simps simp add: alt_natural_map_MN_def make_op_def MN_rel_eq_var
MN_rel_equival H1_c A2_0 H2_1)
hence H2_3: "δ⇩M⇩N (([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C) (φ g a) = δ⇩M⇩N ([(φ⇧⋆) g c]⇩M⇩N) (φ g a)"
using H2_2
by simp
also have H2_4: "... = [((φ⇧⋆) g c) @ [(φ g a)]]⇩M⇩N"
using MN_trans_func_characterization[where v = "(φ⇧⋆) g c" and a = "φ g a"] H1_c A2_0
G_set_equiv H2_0 eq_var_subset.is_equivar insert_iff lists_a_Gset
by blast
also have H2_5: "... = [(φ⇧⋆) g (c @ [a])]⇩M⇩N"
using A2_0 H1_c A1_1
by auto
also have H2_6: "... = ([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g [(c @ [a])]⇩M⇩N"
apply (rule meta_mp[of "c @ [a] ∈ A⇧⋆"])
using eq_var_rel.quot_act_wd[where R = "≡⇩M⇩N" and G = G and X = "A⇧⋆" and φ = "φ⇧⋆" and g = g
and x = "c @ [a]"]
apply (clarsimp simp del: GMN_simps simp add: make_op_def MN_rel_eq_var MN_rel_equival H1_c
A2_0 H2_1)
using H1_c A1_1
by auto
also have H2_7: "... = ([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (δ⇩M⇩N [c]⇩M⇩N a)"
using MN_trans_func_characterization[where v = "c" and a = "a"] H1_c A1_1
by metis
finally show "δ⇩M⇩N (([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C) (φ g a) = ([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (δ⇩M⇩N [c]⇩M⇩N a)"
using H2_1
by metis
qed
show "(([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C ∈ MN_equiv ∧ φ g a ∈ A ⟶
g ∈ carrier G ⟶
δ⇩M⇩N (([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C) (φ g a) =
([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g (δ⇩M⇩N C a)) ∧
((([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g C ∈ MN_equiv ⟶ φ g a ∉ A) ⟶
g ∈ carrier G ⟶ undefined = ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g (δ⇩M⇩N C a))"
apply (rule conjI; clarify)
using H1_1 H1_c
apply blast
by (metis A1_0 H1_0 H_0 alt_group_act_is_grp_act
group_action.element_image)
qed
show ?thesis
apply (subst eq_var_func_def)
apply (subst eq_var_func_axioms_def)
apply (rule conjI)
subgoal
apply (rule prod_group_act[where G = G and A = "MN_equiv" and φ = "[(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙"
and B = A and ψ = φ])
apply (rule H_0)
using G_lang_axioms
by (auto simp add: G_lang_def G_lang_axioms_def)
apply (rule conjI)
subgoal
using MN_rel_eq_var MN_rel_equival eq_var_rel.quot_act_is_grp_act
using alt_group_act_is_grp_act restrict_apply
by fastforce
apply (rule conjI)
subgoal
apply (subst extensional_funcset_def)
apply (subst restrict_def)
apply (subst Pi_def)
apply (subst extensional_def)
apply (clarsimp)
by (metis MN_rel_equival append_in_lists_conv equiv_Eps_preserves lists.Cons lists.Nil
quotientI)
apply (subst restrict_def)
apply (clarsimp simp del: GMN_simps simp add: make_op_def)
by (simp add: H_1 del: GMN_simps)
qed
lemma MN_quot_act_on_empty_str:
"⋀g. ⟦g ∈ carrier G; ([], x) ∈ ≡⇩M⇩N⟧ ⟹ x ∈ map (φ g) ` ≡⇩M⇩N `` {[]}"
proof-
fix g
assume
A_0: "g ∈ carrier G" and
A_1: "([], x) ∈ ≡⇩M⇩N"
from A_1 have H_0: "x ∈ (A⇧⋆)"
by (auto simp add: rel_MN_def)
from A_0 H_0 have H_1: "x = (φ⇧⋆) g ((φ⇧⋆) (inv ⇘G⇙ g) x)"
by (smt (verit) alt_grp_act_def group_action.bij_prop1 group_action.orbit_sym_aux lists_a_Gset)
have H_2: "inv ⇘G ⇙ g ∈ carrier G"
using A_0 MN_rel_eq_var
by (auto simp add: eq_var_rel_def eq_var_rel_axioms_def group_action_def group_hom_def)
have H_3: "([], (φ⇧⋆) (inv ⇘G⇙ g) x) ∈ ≡⇩M⇩N"
using A_0 A_1 H_0 MN_rel_eq_var
apply (clarsimp simp add: eq_var_rel_def eq_var_rel_axioms_def)
apply (rule conjI; clarify)
apply (smt (verit, best) H_0 list.simps(8) lists.Nil)
using H_2
by simp
hence H_4: "∃y∈≡⇩M⇩N `` {[]}. x = map (φ g) y"
using A_0 H_0 H_1 H_2
apply clarsimp
by (metis H_0 Image_singleton_iff insert_iff insert_image lists_image surj_prop)
thus "x ∈ map (φ g) ` ≡⇩M⇩N `` {[]}"
by (auto simp add: image_def)
qed
lemma MN_init_state_equivar:
"eq_var_subset G (A⇧⋆) (φ⇧⋆) MN_init_state"
apply (rule alt_grp_act.eq_var_one_direction)
using lists_a_Gset
apply (auto)[1]
apply (clarsimp)
subgoal for w a
by (auto simp add: rel_MN_def)
apply (simp add: Set.subset_eq; clarify)
apply (clarsimp simp add: image_def Image_def Int_def)
apply (erule disjE)
subgoal for g w
using MN_rel_eq_var
apply (clarsimp simp add: eq_var_rel_def eq_var_rel_axioms_def)
by (metis (full_types, opaque_lifting) in_listsI list.simps(8) lists.Nil)
by (auto simp add: ‹⋀a w. ⟦([], w) ∈ ≡⇩M⇩N; a ∈ set w⟧ ⟹ a ∈ A›)
lemma MN_init_state_equivar_v2:
"eq_var_subset G (MN_equiv) ([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆ ⇙) {MN_init_state}"
proof-
have H_0: "∀g∈carrier G. (φ⇧⋆) g ` MN_init_state = MN_init_state ⟹
∀g∈carrier G. ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g MN_init_state = MN_init_state"
proof (clarify)
fix g
assume
A_0: "g ∈ carrier G"
have H_0: "⋀x. [x]⇩M⇩N = ≡⇩M⇩N `` {x}"
by simp
have H_1: "([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g [[]]⇩M⇩N = [(φ⇧⋆) g []]⇩M⇩N"
using eq_var_rel.quot_act_wd[where R = "≡⇩M⇩N" and G = G and X = "A⇧⋆" and φ = "φ⇧⋆" and g = g
and x = "[]"] MN_rel_eq_var MN_rel_equival
by (clarsimp simp del: GMN_simps simp add: H_0 make_op_def A_0)
from A_0 H_1 show "([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g [[]]⇩M⇩N = [[]]⇩M⇩N"
by auto
qed
show ?thesis
using MN_init_state_equivar
apply (clarsimp simp add: eq_var_subset_def simp del: GMN_simps)
apply (rule conjI)
subgoal
by (metis MN_rel_eq_var MN_rel_equival eq_var_rel.quot_act_is_grp_act)
apply (clarsimp del: subset_antisym simp del: GMN_simps simp add: eq_var_subset_axioms_def)
apply (rule conjI)
apply (auto simp add: quotient_def)[1]
by (simp add: H_0 del: GMN_simps)
qed
lemma MN_final_state_equiv:
"eq_var_subset G (MN_equiv) ([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆ ⇙) MN_fin_states"
proof-
have H_0: "⋀g x w. g ∈ carrier G ⟹ w ∈ L ⟹ ∃wa∈L. ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g [w]⇩M⇩N = [wa]⇩M⇩N"
proof-
fix g w
assume
A1_0: "g ∈ carrier G" and
A1_1: "w ∈ L"
have H1_0: "⋀v. v ∈ L ⟹ (φ⇧⋆) g v ∈ L"
using A1_0 G_lang_axioms
apply (clarsimp simp add: G_lang_def G_lang_axioms_def eq_var_subset_def
eq_var_subset_axioms_def)
by blast
hence H1_1: "(φ⇧⋆) g w ∈ L"
using A1_1
by simp
from A1_1 have H1_2: "⋀v. v ∈ [w]⇩M⇩N ⟹ v ∈ L"
apply (clarsimp simp add: rel_MN_def)
by (metis lists.simps self_append_conv)
have H1_3: "([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g [w]⇩M⇩N = [(φ⇧⋆) g w]⇩M⇩N"
using eq_var_rel.quot_act_wd[where R = "≡⇩M⇩N" and G = G and X = "A⇧⋆" and φ = "φ⇧⋆" and g = g
and x = "w"] MN_rel_eq_var MN_rel_equival G_lang_axioms
by (clarsimp simp add: A1_0 A1_1 G_lang_axioms_def G_lang_def eq_var_subset_def
eq_var_subset_axioms_def subset_eq)
show "∃wa∈L. ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) g [w]⇩M⇩N = [wa]⇩M⇩N"
using H1_1 H1_3
by blast
qed
show ?thesis
apply (rule alt_grp_act.eq_var_one_direction)
using MN_init_state_equivar_v2 eq_var_subset.axioms(1)
apply blast
apply (clarsimp)
subgoal for w
using G_lang_axioms
by (auto simp add: quotient_def G_lang_axioms_def G_lang_def eq_var_subset_def
eq_var_subset_axioms_def)
apply (simp add: Set.subset_eq del: GMN_simps; clarify)
by (simp add: H_0 del: GMN_simps)
qed
interpretation syntac_aut :
det_aut "A" "MN_equiv" "MN_init_state" "MN_fin_states" "MN_trans_func"
proof-
have H_0: "⋀state label. state ∈ MN_equiv ⟹ label ∈ A ⟹ δ⇩M⇩N state label ∈ MN_equiv"
proof -
fix state label
assume
A_0: "state ∈ MN_equiv" and
A_1: "label ∈ A"
obtain w where H_w: "state = [w]⇩M⇩N ∧ w ∈ A⇧⋆"
by (metis A_0 alt_natural_map_MN_def quotientE)
have H_0: "δ⇩M⇩N [w]⇩M⇩N label = [w @ [label]]⇩M⇩N"
using MN_trans_func_characterization[where v = w and a = label] H_w A_1
by simp
have H_1: "⋀v. v ∈ A⇧⋆ ⟹ [v]⇩M⇩N ∈ MN_equiv"
by (simp add: in_listsI quotientI)
show "δ⇩M⇩N state label ∈ MN_equiv"
using H_w H_0 H_1
by (simp add: A_1)
qed
show "det_aut A MN_equiv MN_init_state MN_fin_states δ⇩M⇩N"
apply (clarsimp simp del: GMN_simps simp add: det_aut_def alt_natural_map_MN_def)
apply (intro conjI)
apply (auto simp add: quotient_def)[1]
using G_lang_axioms
apply (auto simp add: quotient_def G_lang_axioms_def G_lang_def
eq_var_subset_def eq_var_subset_axioms_def)[1]
apply (auto simp add: extensional_def PiE_iff simp del: MN_trans_func_def)[1]
apply (simp add: H_0 del: GMN_simps)
by auto
qed
corollary syth_aut_is_det_aut:
"det_aut A MN_equiv MN_init_state MN_fin_states δ⇩M⇩N"
using local.syntac_aut.det_aut_axioms
by simp
lemma give_input_transition_func:
"w ∈ (A⇧⋆) ⟹ ∀v ∈ (A⇧⋆). [v @ w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v]⇩M⇩N w"
proof-
assume
A_0: "w ∈ A⇧⋆"
have H_0: "⋀ a w v. ⟦a ∈ A; w ∈ A⇧⋆; ∀v∈A⇧⋆. [v @ w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v]⇩M⇩N w; v ∈ A⇧⋆⟧ ⟹
[v @ a # w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v]⇩M⇩N (a # w)"
proof-
fix a w v
assume
A1_IH: "∀v∈ A⇧⋆. [v @ w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v]⇩M⇩N w" and
A1_0: "a ∈ A" and
A1_1: "v ∈ A⇧⋆" and
A1_2: "w ∈ A⇧⋆"
from A1_IH A1_1 A1_2 have H1_1: "[v @ w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v]⇩M⇩N w"
by auto
have H1_2: "[(v @ [a]) @ w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v @ [a]]⇩M⇩N w"
apply (rule meta_mp[of "(v @ [a]) ∈ (A⇧⋆)"])
using A1_IH A1_2 H1_1
apply blast
using A1_0 A1_1
by auto
have H1_3: "δ⇩M⇩N [v]⇩M⇩N a = [v @ [a]]⇩M⇩N"
using MN_trans_func_characterization[where a = a] A1_0 A1_1
by auto
hence H1_4: "[v @ a # w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v @ [a]]⇩M⇩N w"
using H1_2
by auto
also have H1_5: "... = (δ⇩M⇩N⇧⋆) (δ⇩M⇩N [v]⇩M⇩N a) w"
using H1_4 H1_3 A1_1
by auto
thus "[v @ a # w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [v]⇩M⇩N (a # w)"
using calculation
by auto
qed
from A_0 show ?thesis
apply (induction w)
apply (auto)[1]
by (simp add: H_0 del: GMN_simps)
qed
lemma MN_unique_init_state:
"w ∈ (A⇧⋆) ⟹ [w]⇩M⇩N = (δ⇩M⇩N⇧⋆) [Nil]⇩M⇩N w"
using give_input_transition_func[where w = w]
by (metis append_self_conv2 lists.Nil)
lemma fin_states_rep_by_lang:
"w ∈ A⇧⋆ ⟹ [w]⇩M⇩N ∈ MN_fin_states ⟹ w ∈ L"
proof-
assume
A_0: "w ∈ A⇧⋆" and
A_1: "[w]⇩M⇩N ∈ MN_fin_states"
from A_1 have H_0: "∃w'∈[w]⇩M⇩N. w' ∈ L"
apply (clarsimp)
by (metis A_0 MN_rel_equival equiv_class_self proj_def proj_in_iff)
from H_0 obtain w' where H_w': "w'∈[w]⇩M⇩N ∧ w' ∈ L"
by auto
have H_1: "⋀v. v ∈ A⇧⋆ ⟹ w'@v ∈ L ⟹ w@v ∈ L"
using H_w' A_1 A_0
by (auto simp add: rel_MN_def)
show "w ∈ L"
using H_1 H_w'
apply clarify
by (metis append_Nil2 lists.Nil)
qed
text ‹
The following lemma corresponds to lemma 3.6 from \cite{bojanczyk2014automata}:
›
lemma syntactic_aut_det_G_aut:
"det_G_aut A MN_equiv MN_init_state MN_fin_states MN_trans_func G φ ([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆⇙)"
apply (clarsimp simp add: det_G_aut_def simp del: GMN_simps)
apply (intro conjI)
using syth_aut_is_det_aut
apply (auto)[1]
using alt_grp_act_axioms
apply (auto)[1]
using MN_init_state_equivar_v2 eq_var_subset.axioms(1)
apply blast
using MN_final_state_equiv
apply presburger
using MN_init_state_equivar_v2
apply presburger
using MN_trans_eq_var_func
by linarith
lemma syntactic_aut_det_G_aut_rec_L:
"det_G_aut_rec_lang A MN_equiv MN_init_state MN_fin_states MN_trans_func G φ
([φ⇧⋆]⇩≡⇩M⇩N ⇘A⇧⋆⇙) L"
apply (clarsimp simp add: det_G_aut_rec_lang_def det_aut_rec_lang_axioms_def
det_aut_rec_lang_def simp del: GMN_simps)
apply (intro conjI)
using syntactic_aut_det_G_aut syth_aut_is_det_aut
apply (auto)[1]
using syntactic_aut_det_G_aut syth_aut_is_det_aut
apply (auto)[1]
apply (rule allI; rule iffI)
apply (rule conjI)
using L_is_equivar eq_var_subset.is_subset image_iff image_mono insert_image insert_subset
apply blast
using MN_unique_init_state L_is_equivar eq_var_subset.is_subset
apply blast
using MN_unique_init_state fin_states_rep_by_lang in_lists_conv_set
by (smt (verit) mem_Collect_eq)
lemma syntact_aut_is_reach_aut_rec_lang:
"reach_det_G_aut_rec_lang A MN_equiv MN_init_state MN_fin_states MN_trans_func G φ
([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) L"
apply (clarsimp simp del: GMN_simps simp add: reach_det_G_aut_rec_lang_def
det_G_aut_rec_lang_def det_aut_rec_lang_axioms_def reach_det_G_aut_def
reach_det_aut_def reach_det_aut_axioms_def det_G_aut_def det_aut_rec_lang_def)
apply (intro conjI)
using syth_aut_is_det_aut
apply blast
using alt_grp_act_axioms
apply (auto)[1]
subgoal
using MN_init_state_equivar_v2 eq_var_subset.axioms(1)
by blast
using MN_final_state_equiv
apply presburger
using MN_init_state_equivar_v2
subgoal
by presburger
using MN_trans_eq_var_func
apply linarith
using syth_aut_is_det_aut
apply (auto)[1]
apply (metis (mono_tags, lifting) G_lang.MN_unique_init_state G_lang_axioms
det_G_aut_rec_lang_def det_aut_rec_lang.is_recognised syntactic_aut_det_G_aut_rec_L)
using syth_aut_is_det_aut
apply (auto)[1]
using alt_grp_act_axioms
apply (auto)[1]
using ‹alt_grp_act G MN_equiv ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙)›
apply blast
using ‹eq_var_subset G MN_equiv ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) MN_fin_states›
apply blast
using ‹eq_var_subset G MN_equiv ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙) {MN_init_state}›
apply blast
using MN_trans_eq_var_func
apply blast
using syth_aut_is_det_aut
apply auto[1]
by (metis MN_unique_init_state alt_natural_map_MN_def quotientE)
end
subsection ‹
Proving the Myhill-Nerode Theorem for $G$-Automata
›
context det_G_aut begin
no_adhoc_overloading
star labels_a_G_set.induced_star_map
end
context reach_det_G_aut_rec_lang begin
adhoc_overloading
star labels_a_G_set.induced_star_map
definition
states_to_words :: "'states ⇒ 'alpha list"
where "states_to_words = (λs ∈ S. SOME w. w ∈ A⇧⋆ ∧ ((δ⇧⋆) i w = s))"
definition
words_to_syth_states :: "'alpha list ⇒ 'alpha list set"
where "words_to_syth_states w = [w]⇩M⇩N"
definition
induced_epi:: "'states ⇒ 'alpha list set"
where "induced_epi = compose S words_to_syth_states states_to_words"
lemma induced_epi_wd1:
"s ∈ S ⟹ ∃w. w ∈ A⇧⋆ ∧ ((δ⇧⋆) i w = s)"
using reach_det_G_aut_rec_lang_axioms is_reachable
by auto
lemma induced_epi_wd2:
"w ∈ A⇧⋆ ⟹ w' ∈ A⇧⋆ ⟹ (δ⇧⋆) i w = (δ⇧⋆) i w' ⟹ [w]⇩M⇩N = [w']⇩M⇩N"
proof-
assume
A_0: "w ∈ A⇧⋆" and
A_1: "w' ∈ A⇧⋆" and
A_2: "(δ⇧⋆) i w = (δ⇧⋆) i w'"
have H_0: "⋀v. v ∈ A⇧⋆ ⟹ w @ v ∈ L ⟷ w' @ v ∈ L"
apply clarify
by (smt (z3) A_0 A_1 A_2 append_in_lists_conv is_aut.eq_pres_under_concat
is_aut.init_state_is_a_state is_lang is_recognised subsetD)+
show "[w]⇩M⇩N = [w']⇩M⇩N "
apply (simp add: rel_MN_def)
using H_0 A_0 A_1
by auto
qed
lemma states_to_words_on_final:
"states_to_words ∈ (F → L)"
proof-
have H_0: "⋀x. x ∈ F ⟹ x ∈ S ⟹ (SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = x) ∈ L"
proof-
fix s
assume
A1_0: "s ∈ F"
have H1_0: "∃w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s"
using A1_0 is_reachable
by (metis is_aut.fin_states_are_states subsetD)
have H1_1: "⋀w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s ⟹ w ∈ L"
using A1_0 is_recognised
by auto
show "(SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s) ∈ L "
by (metis (mono_tags, lifting) H1_0 H1_1 someI_ex)
qed
show ?thesis
apply (clarsimp simp add: states_to_words_def)
apply (rule conjI; rule impI)
apply ( simp add: H_0)
using is_aut.fin_states_are_states
by blast
qed
lemma induced_epi_eq_var:
"eq_var_func G S ψ MN_equiv ([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) induced_epi"
proof-
have H_0: "⋀ s g. ⟦s ∈ S; g ∈ carrier G; ψ g s ∈ S⟧ ⟹
words_to_syth_states (states_to_words (ψ g s)) =
([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (words_to_syth_states (states_to_words s))"
proof-
fix s g
assume
A1_0: "s ∈ S" and
A1_1: "g ∈ carrier G" and
A1_2: "ψ g s ∈ S"
have H1_0: "([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (words_to_syth_states (states_to_words s)) =
[(φ⇧⋆) g (SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s)]⇩M⇩N"
apply (clarsimp simp del: GMN_simps simp add: words_to_syth_states_def
states_to_words_def A1_0)
apply (rule meta_mp[of "(SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s) ∈ A⇧⋆"])
using quot_act_wd_alt_notation[where w = "(SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s)" and g = g] A1_1
apply simp
using A1_0
by (metis (mono_tags, lifting) induced_epi_wd1 some_eq_imp)
have H1_1: "⋀g s' w'. ⟦s'∈ S; w'∈ A⇧⋆; g ∈ carrier G; (φ⇧⋆) g w' ∈ A⇧⋆ ∧ ψ g s' ∈ S⟧
⟹ (δ⇧⋆) (ψ g s') ((φ⇧⋆) g w') = ψ g ((δ⇧⋆) s' w')"
using give_input_eq_var
apply (clarsimp simp del: GMN_simps simp add: eq_var_func_axioms_def eq_var_func_def
make_op_def)
by (meson in_listsI)
have H1_2: "{w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = ψ g s} =
{w'. ∃w ∈ A⇧⋆. (φ⇧⋆) g w = w' ∧ (δ⇧⋆) i w = s}"
proof (rule subset_antisym; clarify)
fix w'
assume
A2_0: "(δ⇧⋆) i w' = ψ g s" and
A2_1: "∀x∈set w'. x ∈ A"
have H2_0: "(inv ⇘G⇙ g) ∈ carrier G"
by (meson A1_1 group.inv_closed group_hom.axioms(1) states_a_G_set.group_hom)
have H2_1: "(φ⇧⋆) g ((φ⇧⋆) (inv ⇘G⇙ g) w') = w'"
by (smt (verit) A1_1 A2_1 alt_group_act_is_grp_act group_action.bij_prop1
group_action.orbit_sym_aux in_listsI labels_a_G_set.lists_a_Gset)
have H2_2: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ (δ⇧⋆) i ((φ⇧⋆) g w) = (δ⇧⋆) (ψ g i) ((φ⇧⋆) g w)"
using init_is_eq_var.eq_var_subset_axioms init_is_eq_var.is_equivar
by auto
have H2_3: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ (δ⇧⋆) (ψ g i) ((φ⇧⋆) g w) = ψ g ((δ⇧⋆) i w)"
apply (rule H1_1[where s'1 = i])
apply (simp add: A2_1 in_lists_conv_set H2_0 is_aut.init_state_is_a_state)+
using is_aut.init_state_is_a_state labels_a_G_set.element_image
states_a_G_set.element_image
by blast
have H2_4: "ψ (inv ⇘G⇙ g) ((δ⇧⋆) i w') = s"
using A2_0 H2_0
by (simp add: A1_0 A1_1 states_a_G_set.orbit_sym_aux)
have H2_5: "(δ⇧⋆) i ((φ⇧⋆) (inv ⇘G⇙ g) w') = s"
apply (rule meta_mp[of "w'∈ A⇧⋆"])
using H2_0 H2_1 H2_4 A2_1 H2_2 H2_3
apply presburger
using A2_1
by auto
have H2_6: "(φ⇧⋆) (inv⇘G⇙ g) w' ∈ A⇧⋆"
using H2_0 A2_1
by (metis alt_group_act_is_grp_act group_action.element_image in_listsI
labels_a_G_set.lists_a_Gset)
thus "∃w∈A⇧⋆. (φ⇧⋆) g w = w' ∧ (δ⇧⋆) i w = s"
using H2_1 H2_5 H2_6
by blast
next
fix x w
assume
A2_0: "∀x∈set w. x ∈ A" and
A2_1: "s = (δ⇧⋆) i w"
show "(φ⇧⋆) g w ∈ A⇧⋆ ∧ (δ⇧⋆) i ((φ⇧⋆) g w) = ψ g ((δ⇧⋆) i w) "
apply (rule conjI)
apply (rule meta_mp[of "(inv ⇘G⇙ g) ∈ carrier G"])
using alt_group_act_is_grp_act group_action.element_image in_listsI
labels_a_G_set.lists_a_Gset
apply (metis A1_1 A2_0)
apply (meson A1_1 group.inv_closed group_hom.axioms(1) states_a_G_set.group_hom)
apply (rule meta_mp[of "ψ g i = i"])
using H1_1[where s'1 = i and g1 = "g"]
apply (metis A1_1 A2_0 action_on_input in_listsI)
using init_is_eq_var.eq_var_subset_axioms init_is_eq_var.is_equivar
by (simp add: A1_1)
qed
have H1_3: "∃w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s"
using A1_0 is_reachable
by auto
have H1_4: "∃w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = ψ g s"
using A1_2 induced_epi_wd1
by auto
have H1_5: "[(φ⇧⋆) g (SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s)]⇩M⇩N = [SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = ψ g s]⇩M⇩N"
proof (rule subset_antisym; clarify)
fix w'
assume
A2_0: "w' ∈ [(φ⇧⋆) g (SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s)]⇩M⇩N"
have H2_0: "⋀w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s ⟹ w' ∈ [(φ⇧⋆) g w]⇩M⇩N"
using A2_0 H1_3 H1_2 H1_4 induced_epi_wd2 mem_Collect_eq tfl_some
by (smt (verit, best))
obtain w'' where H2_w'': "w' ∈ [(φ⇧⋆) g w'']⇩M⇩N ∧ w'' ∈ A⇧⋆ ∧ (δ⇧⋆) i w'' = s"
using A2_0 H1_3 tfl_some
by (metis (mono_tags, lifting))
from H1_2 H2_w'' have H2_1: "(δ⇧⋆) i ((φ⇧⋆) g w'') = ψ g s"
by blast
have H2_2: "⋀w. w ∈ A⇧⋆ ⟹ (δ⇧⋆) i w = ψ g s ⟹ w' ∈ [w]⇩M⇩N"
proof -
fix w''
assume
A3_0: "w'' ∈ A⇧⋆" and
A3_1: "(δ⇧⋆) i w'' = ψ g s"
have H3_0: "(inv ⇘G⇙g) ∈ carrier G"
by (metis A1_1 group.inv_closed group_hom.axioms(1) states_a_G_set.group_hom)
from A3_0 H3_0 have H3_1: "(φ⇧⋆) (inv ⇘G⇙ g) w'' ∈ A⇧⋆"
by (metis alt_grp_act.axioms group_action.element_image
labels_a_G_set.lists_a_Gset)
have H3_2: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ (δ⇧⋆) i ((φ⇧⋆) g w) = (δ⇧⋆) (ψ g i) ((φ⇧⋆) g w)"
using init_is_eq_var.eq_var_subset_axioms init_is_eq_var.is_equivar
by auto
have H3_3: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ (δ⇧⋆) (ψ g i) ((φ⇧⋆) g w) = ψ g ((δ⇧⋆) i w)"
apply (rule H1_1[where s'1 = i])
apply (simp add: A3_1 in_lists_conv_set H2_1 is_aut.init_state_is_a_state)+
using is_aut.init_state_is_a_state labels_a_G_set.element_image
states_a_G_set.element_image
by blast
have H3_4: "s = (δ⇧⋆) i ((φ⇧⋆) (inv ⇘G⇙ g) w'')"
using A3_0 A3_1 H3_0 H3_2 H3_3 A1_0 A1_1 states_a_G_set.orbit_sym_aux
by auto
from H3_4 show " w' ∈ [w'']⇩M⇩N"
by (metis (mono_tags, lifting) A1_1 G_set_equiv H2_1 H2_w'' ‹(δ⇧⋆) i w'' = ψ g s› A3_0
eq_var_subset.is_equivar image_eqI induced_epi_wd2
labels_a_G_set.lists_a_Gset)
qed
from H2_2 show "w' ∈ [SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = ψ g s]⇩M⇩N"
by (smt (verit) H1_4 some_eq_ex)
next
fix w'
assume
A2_0: "w' ∈ [SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = ψ g s]⇩M⇩N"
obtain w'' where H2_w'': "w' ∈ [(φ⇧⋆) g w'']⇩M⇩N ∧ w'' ∈ A⇧⋆ ∧ (δ⇧⋆) i w'' = s"
using A2_0 H1_3 tfl_some
by (smt (verit) H1_2 mem_Collect_eq)
from H1_2 H2_w'' have H2_0: "(δ⇧⋆) i ((φ⇧⋆) g w'') = ψ g s"
by blast
have H2_1: "⋀w. w ∈ A⇧⋆ ⟹ (δ⇧⋆) i w = s ⟹ w' ∈ [(φ⇧⋆) g w]⇩M⇩N"
proof -
fix w''
assume
A3_0: "w'' ∈ A⇧⋆" and
A3_1: "(δ⇧⋆) i w'' = s"
have H3_0: "(inv ⇘G⇙g) ∈ carrier G"
by (metis A1_1 group.inv_closed group_hom.axioms(1) states_a_G_set.group_hom)
have H3_1: "(φ⇧⋆) (inv ⇘G⇙ g) w'' ∈ A⇧⋆"
using A3_0 H3_0
by (metis alt_group_act_is_grp_act group_action.element_image labels_a_G_set.lists_a_Gset)
have H3_2: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ (δ⇧⋆) i ((φ⇧⋆) g w) =
(δ⇧⋆) (ψ g i) ((φ⇧⋆) g w)"
using init_is_eq_var.eq_var_subset_axioms init_is_eq_var.is_equivar
by auto
have H3_3: "⋀g w. g ∈ carrier G ⟹ w ∈ A⇧⋆ ⟹ (δ⇧⋆) (ψ g i) ((φ⇧⋆) g w) =
ψ g ((δ⇧⋆) i w)"
apply (rule H1_1[where s'1 = i])
apply (simp add: A3_1 in_lists_conv_set H2_0 is_aut.init_state_is_a_state)+
using is_aut.init_state_is_a_state labels_a_G_set.element_image
states_a_G_set.element_image
by blast
have H3_4: "ψ (inv ⇘G⇙ g) s = (δ⇧⋆) i ((φ⇧⋆) (inv ⇘G⇙ g) w'')"
using A3_0 A3_1 H3_0 H3_2 H3_3
by auto
show "w' ∈ [(φ⇧⋆) g w'']⇩M⇩N "
using H3_4 H3_1
by (smt (verit, del_insts) A1_1 A3_0 A3_1 in_listsI H3_2 H3_3
‹⋀thesis. (⋀w''. w' ∈ [(φ⇧⋆) g w'']⇩M⇩N ∧ w'' ∈ A⇧⋆ ∧
(δ⇧⋆) i w'' = s ⟹ thesis) ⟹ thesis›
alt_group_act_is_grp_act group_action.surj_prop image_eqI induced_epi_wd2
labels_a_G_set.lists_a_Gset)
qed
show "w' ∈ [(φ⇧⋆) g (SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s)]⇩M⇩N"
using H2_1 H1_3
by (metis (mono_tags, lifting) someI)
qed
show "words_to_syth_states (states_to_words (ψ g s)) =
([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (words_to_syth_states (states_to_words s))"
using H1_5
apply (clarsimp simp del: GMN_simps simp add: words_to_syth_states_def states_to_words_def)
apply (intro conjI; clarify; rule conjI)
using H1_0
apply (auto del: subset_antisym simp del: GMN_simps simp add: words_to_syth_states_def
states_to_words_def)[1]
using A1_2
apply blast
using A1_0
apply blast
using A1_0
by blast
qed
show ?thesis
apply (clarsimp del: subset_antisym simp del: GMN_simps simp add: eq_var_func_def
eq_var_func_axioms_def)
apply (intro conjI)
subgoal
using states_a_G_set.alt_grp_act_axioms
by auto
apply (metis MN_rel_eq_var MN_rel_equival eq_var_rel.quot_act_is_grp_act)
apply (clarsimp simp add: FuncSet.extensional_funcset_def Pi_def)
apply (rule conjI)
apply (clarify)
subgoal for s
using is_reachable[where s = s]
apply (clarsimp simp add: induced_epi_def compose_def states_to_words_def
words_to_syth_states_def)
by (smt (verit) ‹s ∈ S ⟹ ∃input∈A⇧⋆. (δ⇧⋆) i input = s› alt_natural_map_MN_def
lists_eq_set quotientI rel_MN_def singleton_conv someI)
apply (clarsimp simp del: GMN_simps simp add: induced_epi_def make_op_def
compose_def)
apply (clarify)
apply (clarsimp simp del: GMN_simps simp add: induced_epi_def compose_def make_op_def)
apply (rule conjI; rule impI)
apply (simp add: H_0)
using states_a_G_set.element_image
by blast
qed
text ‹
The following lemma corresponds to lemma 3.7 from \cite{bojanczyk2014automata}:
›
lemma reach_det_G_aut_rec_lang:
"G_aut_epi A S i F δ MN_equiv MN_init_state MN_fin_states δ⇩M⇩N G φ ψ ([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) induced_epi"
proof-
have H_0: "⋀s. s ∈ MN_equiv ⟹ ∃input∈ A⇧⋆. (δ⇩M⇩N⇧⋆) MN_init_state input = s"
proof-
fix s
assume
A_0: "s ∈ MN_equiv"
from A_0 have H_0: "∃w. w ∈ A⇧⋆ ∧ s = [w]⇩M⇩N"
by (auto simp add: quotient_def)
show "∃input∈A⇧⋆. (δ⇩M⇩N⇧⋆) MN_init_state input = s"
using H_0
by (metis MN_unique_init_state)
qed
have H_1: "⋀s⇩0 a. s⇩0 ∈ S ⟹ a ∈ A ⟹ induced_epi (δ s⇩0 a) = δ⇩M⇩N (induced_epi s⇩0) a"
proof-
fix s⇩0 a
assume
A1_0: "s⇩0 ∈ S" and
A1_1: "a ∈ A"
obtain w where H1_w: "w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s⇩0"
using A1_0 induced_epi_wd1
by auto
have H1_0: "[SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s⇩0]⇩M⇩N = [w]⇩M⇩N"
by (metis (mono_tags, lifting) H1_w induced_epi_wd2 some_eq_imp)
have H1_1: "(δ⇧⋆) i (SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = δ s⇩0 a) = (δ⇧⋆) i (w @ [a])"
using A1_0 A1_1 H1_w is_aut.trans_to_charact[where s = s⇩0 and a = a and w = w]
by (smt (verit, del_insts) induced_epi_wd1 is_aut.trans_func_well_def tfl_some)
have H1_2: "w @ [a] ∈ A⇧⋆" using H1_w A1_1 by auto
have H1_3: "[(SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s⇩0) @ [a]]⇩M⇩N = [w @ [a]]⇩M⇩N"
by (metis (mono_tags, lifting) A1_1 H1_0 H1_w MN_trans_func_characterization someI)
have H1_4: "... = [SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = δ s⇩0 a]⇩M⇩N"
apply (rule sym)
apply (rule induced_epi_wd2[where w = "SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = δ s⇩0 a"
and w'= "w @ [a]"])
apply (metis (mono_tags, lifting) A1_0 A1_1 H1_w some_eq_imp H1_2 is_aut.trans_to_charact)
apply (rule H1_2)
using H1_1
by simp
show "induced_epi (δ s⇩0 a) = δ⇩M⇩N (induced_epi s⇩0) a"
apply (clarsimp del: subset_antisym simp del: GMN_simps simp add: induced_epi_def
words_to_syth_states_def states_to_words_def compose_def is_aut.trans_func_well_def)
using A1_1 H1_w H1_0 H1_3 H1_4 MN_trans_func_characterization A1_0
is_aut.trans_func_well_def
by presburger
qed
have H_2: "induced_epi ` S = MN_equiv"
proof-
have H1_0: "∀s ∈ S. ∃v∈ A⇧⋆. (δ⇧⋆) i v = s ∧ [SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s]⇩M⇩N = [v]⇩M⇩N"
by (smt (verit) is_reachable tfl_some)
have H1_1: "⋀v. v∈ A⇧⋆ ⟹ (δ⇧⋆) i v ∈ S"
using is_aut.give_input_closed
by (auto simp add: is_aut.init_state_is_a_state)
show ?thesis
apply (clarsimp simp del: GMN_simps simp add: induced_epi_def words_to_syth_states_def
states_to_words_def compose_def image_def)
using H1_0 H1_1
apply (clarsimp)
apply (rule subset_antisym; simp del: GMN_simps add: Set.subset_eq)
apply (metis (no_types, lifting) quotientI)
by (metis (no_types, lifting) alt_natural_map_MN_def induced_epi_wd2 quotientE)
qed
show ?thesis
apply (simp del: GMN_simps add: G_aut_epi_def G_aut_epi_axioms_def)
apply (rule conjI)
subgoal
apply (clarsimp simp del: GMN_simps simp add: G_aut_hom_def aut_hom_def reach_det_G_aut_def
is_reachable det_G_aut_def reach_det_aut_def reach_det_aut_axioms_def)
apply (intro conjI)
apply (simp add: is_aut.det_aut_axioms)
using labels_a_G_set.alt_grp_act_axioms
apply (auto)[1]
using states_a_G_set.alt_grp_act_axioms
apply blast
apply (simp add: accepting_is_eq_var.eq_var_subset_axioms)
using init_is_eq_var.eq_var_subset_axioms
apply (auto)[1]
apply (simp add: trans_is_eq_var.eq_var_func_axioms)
apply (simp add: is_aut.det_aut_axioms)
using syth_aut_is_det_aut
apply simp
using labels_a_G_set.alt_grp_act_axioms
apply (auto)[1]
apply (metis MN_rel_eq_var MN_rel_equival eq_var_rel.quot_act_is_grp_act)
using MN_final_state_equiv
apply presburger
using MN_init_state_equivar_v2
apply presburger
using MN_trans_eq_var_func
apply blast
using syth_aut_is_det_aut
apply auto[1]
apply (clarify)
apply (simp add: H_0 del: GMN_simps)
apply (simp add: is_aut.det_aut_axioms)
using syth_aut_is_det_aut
apply blast
apply (clarsimp del: subset_antisym simp del: GMN_simps simp add: aut_hom_axioms_def
FuncSet.extensional_funcset_def Pi_def extensional_def)[1]
apply (intro conjI)
apply (clarify)
apply (simp add: induced_epi_def)
apply (simp add: induced_epi_def words_to_syth_states_def states_to_words_def
compose_def)
apply (rule meta_mp[of "(δ⇧⋆) i Nil = i"])
using induced_epi_wd2[where w = "Nil"]
apply (auto simp add: is_aut.init_state_is_a_state del: subset_antisym)[2]
subgoal for x
apply (rule quotientI)
using is_reachable[where s = x] someI[where P = "λw. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = x"]
by blast
apply (auto simp add: induced_epi_def words_to_syth_states_def states_to_words_def
compose_def)[1]
apply (simp add: induced_epi_def states_to_words_def compose_def
is_aut.init_state_is_a_state)
apply (metis (mono_tags, lifting) ‹⋀w'. ⟦[] ∈ A⇧⋆; w' ∈ A⇧⋆;
(δ⇧⋆) i [] = (δ⇧⋆) i w'⟧ ⟹ MN_init_state = [w']⇩M⇩N›
alt_natural_map_MN_def give_input.simps(1) lists.Nil some_eq_imp
words_to_syth_states_def)
apply (clarify)
subgoal for s
apply (rule iffI)
apply (smt (verit) Pi_iff compose_eq in_mono induced_epi_def is_aut.fin_states_are_states
states_to_words_on_final words_to_syth_states_def)
apply (clarsimp simp del: GMN_simps simp add: induced_epi_def words_to_syth_states_def
states_to_words_def compose_def)
apply (rule meta_mp[of "(SOME w. w ∈ A⇧⋆ ∧ (δ⇧⋆) i w = s) ∈ L"])
apply (smt (verit) induced_epi_wd1 is_recognised someI)
using fin_states_rep_by_lang is_reachable mem_Collect_eq
by (metis (mono_tags, lifting))
apply (clarsimp simp del: GMN_simps)
apply (simp add: H_1)
using induced_epi_eq_var
by blast
by (simp add: H_2)
qed
end
lemma (in det_G_aut) finite_reachable:
"finite (orbits G S ψ) ⟹ finite (orbits G S⇩r⇩e⇩a⇩c⇩h ψ⇩r⇩e⇩a⇩c⇩h)"
proof-
assume
A_0: "finite (orbits G S ψ)"
have H_0: "S⇩r⇩e⇩a⇩c⇩h ⊆ S"
apply (clarsimp simp add: reachable_states_def)
by (simp add: in_listsI is_aut.give_input_closed is_aut.init_state_is_a_state)
have H_1: "{{ψ g x |g. g ∈ carrier G} |x. x ∈ S⇩r⇩e⇩a⇩c⇩h} ⊆
{{ψ g x |g. g ∈ carrier G} |x. x ∈ S}"
by (smt (verit, best) Collect_mono_iff H_0 subsetD)
have H_2: "⋀x. x ∈ S⇩r⇩e⇩a⇩c⇩h ⟹
{ψ g x |g. g ∈ carrier G} = {ψ⇩r⇩e⇩a⇩c⇩h g x |g. g ∈ carrier G}"
using reachable_action_is_restict
by (metis)
hence H_3: "{{ψ g x |g. g ∈ carrier G} |x. x ∈ S⇩r⇩e⇩a⇩c⇩h} =
{{ψ⇩r⇩e⇩a⇩c⇩h g x |g. g ∈ carrier G} |x. x ∈ S⇩r⇩e⇩a⇩c⇩h}"
by blast
show "finite (orbits G S⇩r⇩e⇩a⇩c⇩h ψ⇩r⇩e⇩a⇩c⇩h)"
using A_0 apply (clarsimp simp add: orbits_def orbit_def)
using Finite_Set.finite_subset H_1 H_3
by auto
qed
lemma (in det_G_aut)
orbs_pos_card: "finite (orbits G S ψ) ⟹ card (orbits G S ψ) > 0"
apply (clarsimp simp add: card_gt_0_iff orbits_def)
using is_aut.init_state_is_a_state
by auto
lemma (in reach_det_G_aut_rec_lang) MN_B2T:
assumes
Fin: "finite (orbits G S ψ)"
shows
"finite (orbits G (language.MN_equiv A L) (([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙)))"
proof-
have H_0: "finite {{ψ g x |g. g ∈ carrier G} |x. x ∈ S}"
using Fin
by (auto simp add: orbits_def orbit_def)
have H_1: "induced_epi ` S = MN_equiv"
using reach_det_G_aut_rec_lang
by (auto simp del: GMN_simps simp add: G_aut_epi_def G_aut_epi_axioms_def)
have H_2: "⋀B f. finite B ⟹ finite {f b| b. b ∈ B} "
by auto
have H_3: "finite {{ψ g x |g. g ∈ carrier G} |x. x ∈ S} ⟹
finite {induced_epi ` b |b. b ∈ {{ψ g x |g. g ∈ carrier G} |x. x ∈ S}}"
using H_2[where f1 = "(λx. induced_epi ` x)" and B1 = "{{ψ g x |g. g ∈ carrier G} |x. x ∈ S}"]
by auto
have H_4: "⋀s. s ∈ S ⟹ ∃b. {induced_epi (ψ g s) |g. g ∈ carrier G}
= {y. ∃x∈b. y = induced_epi x} ∧ (∃x. b = {ψ g x |g. g ∈ carrier G} ∧ x ∈ S)"
proof-
fix s
assume
A2_0: "s ∈ S"
have H2_0: "{induced_epi (ψ g s) |g. g ∈ carrier G} = {y. ∃x ∈ {ψ g s |g. g ∈ carrier G}. y =
induced_epi x}"
by blast
have H2_1: "(∃x. {ψ g s |g. g ∈ carrier G} = {ψ g x |g. g ∈ carrier G} ∧ x ∈ S)"
using A2_0
by auto
show "∃b. {induced_epi (ψ g s) |g. g ∈ carrier G} =
{y. ∃x∈b. y = induced_epi x} ∧ (∃x. b = {ψ g x |g. g ∈ carrier G} ∧ x ∈ S)"
using A2_0 H2_0 H2_1
by meson
qed
have H_5: "{induced_epi ` b |b. b ∈ {{ψ g x |g. g ∈ carrier G} |x. x ∈ S}} =
{{induced_epi (ψ g s) | g . g ∈ carrier G} |s. s ∈ S}"
apply (clarsimp simp add: image_def)
apply (rule subset_antisym; simp add: Set.subset_eq; clarify)
apply auto[1]
apply (simp)
by (simp add: H_4)
from H_3 H_5 have H_6: "finite {{ψ g x |g. g ∈ carrier G} |x. x ∈ S} ⟹
finite {{induced_epi (ψ g s) | g . g ∈ carrier G} |s. s ∈ S}"
by metis
have H_7: "finite {{induced_epi (ψ g x) |g. g ∈ carrier G} |x. x ∈ S}"
apply (rule H_6)
by (simp add: H_0)
have H_8: "⋀x. x ∈ S ⟹ {induced_epi (ψ g x) |g. g ∈ carrier G} =
{([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (induced_epi x) |g. g ∈ carrier G}"
using induced_epi_eq_var
apply (simp del: GMN_simps add: eq_var_func_def eq_var_func_axioms_def make_op_def)
by blast
hence H_9: "{{induced_epi (ψ g x) |g. g ∈ carrier G} |x. x ∈ S} =
{{([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (induced_epi x) |g. g ∈ carrier G} |x. x ∈ S}"
by blast
have H_10: "⋀f g X B C. g ` B = C ⟹
{{f x (g b)|x. x∈X}|b. b ∈ B} = {{f x c|x. x ∈ X}|c. c ∈ C}"
by auto
have H_11: "{{([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g (induced_epi x) |g. g ∈ carrier G} |x. x ∈ S} =
{{([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g W |g. g ∈ carrier G} |W. W ∈ MN_equiv}"
apply (rule H_10[where f2 = "([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙)" and X2 = "carrier G" and g2 = induced_epi
and B2 = S and C2 = MN_equiv])
using H_1
by simp
have H_12: "{{([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙) g W |g. g ∈ carrier G} |W. W ∈ MN_equiv} =
orbits G (language.MN_equiv A L) (([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙))"
by (auto simp add: orbits_def orbit_def)
show "finite (orbits G (language.MN_equiv A L) (([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙)))"
using H_9 H_11 H_12 H_7
by presburger
qed
context det_G_aut_rec_lang begin
text ‹
To avoid duplicate variant of "star":
›
no_adhoc_overloading
star labels_a_G_set.induced_star_map
end
context det_G_aut_rec_lang begin
adhoc_overloading
star labels_a_G_set.induced_star_map
end
lemma (in det_G_aut_rec_lang) MN_prep:
"∃S'. ∃δ'. ∃F'. ∃ψ'.
(reach_det_G_aut_rec_lang A S' i F' δ' G φ ψ' L ∧
(finite (orbits G S ψ) ⟶ finite (orbits G S' ψ')))"
by (meson G_lang_axioms finite_reachable reach_det_G_aut_rec_lang.intro
reach_det_aut_is_det_aut_rec_L)
lemma (in det_G_aut_rec_lang) MN_fin_orbs_imp_fin_states:
assumes
Fin: "finite (orbits G S ψ)"
shows
"finite (orbits G (language.MN_equiv A L) (([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙)))"
using MN_prep
by (metis assms reach_det_G_aut_rec_lang.MN_B2T)
text ‹
The following theorem corresponds to theorem 3.8 from \cite{bojanczyk2014automata}, i.e. the
Myhill-Nerode theorem for G-automata.
The left to right direction (see statement below) of the typical Myhill-Nerode theorem would
qantify over types (if some condition holds, then there exists some automaton accepting the
language). As it is not possible to qantify over types in this way, the equivalence is spit into
two directions. In the left to right direction, the explicit type of the syntactic automaton is
used. In the right to left direction some type, 's, is fixed.
As the two directions are split, the opertunity was taken to strengthen the right to left direction:
We do not assume the given automaton is reachable.
This splitting of the directions will be present in all other Myhill-Nerode theorems that will be
proved in this document.
›
theorem (in G_lang) G_Myhill_Nerode :
assumes
"finite (orbits G A φ)"
shows
G_Myhill_Nerode_LR: "finite (orbits G MN_equiv ([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙)) ⟹
(∃S F :: 'alpha list set set. ∃i :: 'alpha list set. ∃δ. ∃ψ.
reach_det_G_aut_rec_lang A S i F δ G φ ψ L ∧ finite (orbits G S ψ))" and
G_Myhill_Nerode_RL: "(∃S F :: 's set. ∃i :: 's. ∃δ. ∃ψ.
det_G_aut_rec_lang A S i F δ G φ ψ L ∧ finite (orbits G S ψ))
⟹ finite (orbits G MN_equiv ([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙))"
subgoal
using syntact_aut_is_reach_aut_rec_lang
by blast
by (metis det_G_aut_rec_lang.MN_fin_orbs_imp_fin_states)
subsection ‹
Proving the standard Myhill-Nerode Theorem
›
text ‹
Any automaton is a $G$-automaton with respect to the trivial group and action,
hence the standard Myhill-Nerode theorem is a special case of the $G$-Myhill-Nerode theorem.
›
interpretation triv_act:
alt_grp_act "singleton_group (undefined)" X "(λx ∈ {undefined}. one (BijGroup X))"
apply (simp add: group_action_def group_hom_def group_hom_axioms_def)
apply (intro conjI)
apply (simp add: group_BijGroup)
using trivial_hom
by (smt (verit) carrier_singleton_group group.hom_restrict group_BijGroup restrict_apply
singleton_group)
lemma (in det_aut) triv_G_aut:
fixes triv_G
assumes H_triv_G: "triv_G = (singleton_group (undefined))"
shows "det_G_aut labels states init_state fin_states δ
triv_G (λx ∈ {undefined}. one (BijGroup labels)) (λx ∈ {undefined}. one (BijGroup states))"
apply (simp add: det_G_aut_def group_hom_def group_hom_axioms_def
eq_var_subset_def eq_var_subset_axioms_def eq_var_func_def eq_var_func_axioms_def)
apply (intro conjI)
apply (rule det_aut_axioms)
apply (simp add: assms triv_act.group_action_axioms)+
using fin_states_are_states
apply (auto)[1]
apply (clarify; rule conjI; rule impI)
apply (simp add: H_triv_G BijGroup_def image_def)
using fin_states_are_states
apply auto[1]
apply (simp add: H_triv_G BijGroup_def image_def)
apply (simp add: assms triv_act.group_action_axioms)
apply (simp add: init_state_is_a_state)
apply (clarify; rule conjI; rule impI)
apply (simp add: H_triv_G BijGroup_def image_def init_state_is_a_state)+
apply (clarsimp simp add: group_action_def BijGroup_def hom_def group_hom_def
group_hom_axioms_def)
apply (rule conjI)
apply (smt (verit) BijGroup_def Bij_imp_funcset Id_compose SigmaE case_prod_conv
group_BijGroup id_Bij restrict_ext restrict_extensional)
apply (rule meta_mp[of "undefined ⊗⇘singleton_group undefined⇙ undefined = undefined"])
apply (auto)[1]
apply (metis carrier_singleton_group comm_groupE(1) singletonD singletonI
singleton_abelian_group)
apply (simp add: assms triv_act.group_action_axioms)
apply (auto simp add: trans_func_well_def)[1]
by (clarsimp simp add: BijGroup_def trans_func_well_def H_triv_G)
lemma triv_orbits:
"orbits (singleton_group (undefined)) S (λx ∈ {undefined}. one (BijGroup S)) =
{{s} |s. s ∈ S}"
apply (simp add: BijGroup_def singleton_group_def orbits_def orbit_def)
by auto
lemma fin_triv_orbs:
"finite (orbits (singleton_group (undefined)) S (λx ∈ {undefined}. one (BijGroup S))) = finite S"
apply (subst triv_orbits)
apply (rule meta_mp[of "bij_betw (λs ∈ S. {s}) S {{s} |s. s ∈ S}"])
using bij_betw_finite
apply (auto)[1]
by (auto simp add: bij_betw_def image_def)
context language begin
interpretation triv_G_lang:
G_lang "singleton_group (undefined)" A "(λx ∈ {undefined}. one (BijGroup A))" L
apply (simp add: G_lang_def G_lang_axioms_def eq_var_subset_def eq_var_subset_axioms_def)
apply (intro conjI)
apply (simp add: triv_act.group_action_axioms)
apply (simp add: language_axioms)
using triv_act.lists_a_Gset
apply fastforce
apply (rule is_lang)
apply (clarsimp simp add: BijGroup_def image_def)
apply (rule subset_antisym; simp add: Set.subset_eq; clarify)
using is_lang
apply (auto simp add: map_idI)[1]
using is_lang map_idI
by (metis in_listsD in_mono inf.absorb_iff1 restrict_apply)
definition triv_G :: "'grp monoid"
where "triv_G = (singleton_group (undefined))"
definition triv_act :: "'grp ⇒ 'alpha ⇒ 'alpha"
where "triv_act = (λx ∈ {undefined}. 𝟭⇘BijGroup A⇙)"
corollary standard_Myhill_Nerode:
assumes
H_fin_alph: "finite A"
shows
standard_Myhill_Nerode_LR: "finite MN_equiv ⟹
(∃S F :: 'alpha list set set. ∃i :: 'alpha list set. ∃δ.
reach_det_aut_rec_lang A S i F δ L ∧ finite S)" and
standard_Myhill_Nerode_RL: "(∃S F :: 's set. ∃i :: 's. ∃δ.
det_aut_rec_lang A S i F δ L ∧ finite S) ⟹ finite MN_equiv"
proof-
assume
A_0: "finite MN_equiv"
have H_0: "reach_det_aut_rec_lang A MN_equiv MN_init_state MN_fin_states δ⇩M⇩N L"
using triv_G_lang.syntact_aut_is_reach_aut_rec_lang
apply (clarsimp simp add: reach_det_G_aut_rec_lang_def det_G_aut_rec_lang_def
reach_det_aut_rec_lang_def reach_det_aut_def reach_det_aut_axioms_def det_G_aut_def)
by (smt (z3) alt_natural_map_MN_def quotientE triv_G_lang.MN_unique_init_state)
show "∃S F:: 'alpha list set set. ∃i :: 'alpha list set. ∃δ.
reach_det_aut_rec_lang A S i F δ L ∧ finite S"
using A_0 H_0
by auto
next
assume
A_0: "∃S F:: 's set. ∃i :: 's. ∃δ. det_aut_rec_lang A S i F δ L ∧ finite S"
obtain S F :: "'s set" and i :: "'s" and δ
where H_MN: "det_aut_rec_lang A S i F δ L ∧ finite S"
using A_0
by auto
have H_0: "det_G_aut A S i F δ triv_G (λx∈{undefined}. 𝟭⇘BijGroup A⇙)
(λx∈{undefined}. 𝟭⇘BijGroup S⇙)"
apply (rule det_aut.triv_G_aut[of A S i F δ triv_G])
using H_MN
apply (simp add: det_aut_rec_lang_def)
by (rule triv_G_def)
have H_1: "det_G_aut_rec_lang A S i F δ triv_G (λx∈{undefined}. 𝟭⇘BijGroup A⇙)
(λx∈{undefined}. 𝟭⇘BijGroup S⇙) L"
by (auto simp add: det_G_aut_rec_lang_def H_0 H_MN)
have H_2: "(∃S F:: 's set. ∃i :: 's. ∃δ ψ.
det_G_aut_rec_lang A S i F δ (singleton_group undefined) (λx∈{undefined}. 𝟭⇘BijGroup A⇙)
ψ L ∧ finite (orbits (singleton_group undefined) S ψ))"
using H_1
by (metis H_MN fin_triv_orbs triv_G_def)
have H_3: "finite (orbits triv_G A triv_act)"
apply (subst triv_G_def; subst triv_act_def; subst fin_triv_orbs[of A])
by (rule H_fin_alph)
have H_4:"finite (orbits triv_G MN_equiv (triv_act.induced_quot_map (A⇧⋆)
(triv_act.induced_star_map A triv_act) ≡⇩M⇩N))"
using H_3
apply (simp add: triv_G_def triv_act_def del: GMN_simps)
using triv_G_lang.G_Myhill_Nerode H_2
by blast
have H_5:"triv_act.induced_star_map A triv_act = (λx ∈ {undefined}. 𝟭⇘BijGroup (A⇧⋆)⇙)"
apply (simp add: BijGroup_def restrict_def fun_eq_iff triv_act_def)
by (clarsimp simp add: list.map_ident_strong)
have H_6: "(triv_act.induced_quot_map (A⇧⋆) (triv_act.induced_star_map A
triv_act) ≡⇩M⇩N) = (λx ∈ {undefined}. 𝟭⇘BijGroup MN_equiv⇙)"
apply (subst H_5)
apply (simp add: BijGroup_def fun_eq_iff Image_def)
apply (rule allI; rule conjI; intro impI)
apply (smt (verit) Collect_cong Collect_mem_eq Eps_cong MN_rel_equival equiv_Eps_in
in_quotient_imp_closed quotient_eq_iff)
using MN_rel_equival equiv_Eps_preserves
by auto
show "finite MN_equiv"
apply (subst fin_triv_orbs [symmetric]; subst H_6 [symmetric]; subst triv_G_def [symmetric])
by (rule H_4)
qed
end
section ‹
Myhill-Nerode Theorem for Nominal $G$-Automata
›
subsection ‹
Data Symmetries, Supports and Nominal Actions
›
text ‹
The following locale corresponds to the definition 2.2 from \cite{bojanczyk2014automata}.
Note that we let $G$ be an arbitrary group instead of a subgroup of \texttt{BijGroup} $D$,
but assume there is a homomoprhism $\pi: G \to \texttt{BijGroup} D$.
By \texttt{group\_hom.img\_is\_subgroup} this is an equivalent definition:
›
locale data_symm = group_action G D π
for
G :: "('grp, 'b) monoid_scheme" and
D :: "'D set" ("𝔻") and
π
text ‹
The following locales corresponds to definition 4.3 from \cite{bojanczyk2014automata}:
›
locale supports = data_symm G D π + alt_grp_act G X φ
for
G :: "('grp, 'b) monoid_scheme" and
D :: "'D set" ("𝔻") and
π and
X :: "'X set" (structure) and
φ +
fixes
C :: "'D set" and
x :: "'X"
assumes
is_in_set:
"x ∈ X" and
is_subset:
"C ⊆ 𝔻" and
supports:
"g ∈ carrier G ⟹ (∀c. c ∈ C ⟶ π g c = c) ⟹ g ⊙⇘φ⇙ x = x"
begin
text ‹
The following lemma corresponds to lemma 4.9 from \cite{bojanczyk2014automata}:
›
lemma image_supports:
"⋀g. g ∈ carrier G ⟹ supports G D π X φ (π g ` C) (g ⊙⇘φ⇙ x)"
proof-
fix g
assume
A_0: "g ∈ carrier G"
have H_0: "⋀h. data_symm G 𝔻 π ⟹
group_action G X φ ⟹
x ∈ X ⟹
C ⊆ 𝔻 ⟹
∀g. g ∈ carrier G ⟶ (∀c. c ∈ C ⟶ π g c = c) ⟶ φ g x = x ⟹
h ∈ carrier G ⟹ ∀c. c ∈ π g ` C ⟶ π h c = c ⟹
φ h (φ g x) = φ g x"
proof-
fix h
assume
A1_0: "data_symm G 𝔻 π" and
A1_1: "group_action G X φ" and
A1_2: "∀g. g ∈ carrier G ⟶ (∀c. c ∈ C ⟶ π g c = c) ⟶ φ g x = x" and
A1_3: "h ∈ carrier G" and
A1_4: "∀c. c ∈ π g ` C ⟶ π h c = c"
have H1_0: "⋀g. g ∈ carrier G ⟹ (∀c. c ∈ C ⟶ π g c = c) ⟹ φ g x = x"
using A1_2
by auto
have H1_1: "∀c. c ∈ C ⟶ π ((inv⇘G⇙ g) ⊗⇘G⇙ h ⊗⇘G⇙ g) c = c ⟹
φ ((inv⇘G⇙ g) ⊗⇘G⇙ h ⊗⇘G⇙ g) x = x"
apply (rule H1_0[of "((inv⇘G⇙ g) ⊗⇘G⇙ h ⊗⇘G⇙ g)"])
apply (meson A_0 A1_3 group.subgroupE(3) group.subgroup_self group_hom group_hom.axioms(1)
subgroup.m_closed)
by simp
have H2: "π (((inv⇘G⇙ g) ⊗⇘G⇙ h) ⊗⇘G⇙ g) = compose 𝔻 (π ((inv⇘G⇙ g) ⊗⇘G⇙ h)) (π g)"
using A1_0
apply (clarsimp simp add: data_symm_def group_action_def BijGroup_def group_hom_def
group_hom_axioms_def hom_def restrict_def)
apply (rule meta_mp[of "π g ∈ Bij 𝔻 ∧ π ((inv⇘G⇙ g) ⊗⇘G⇙ h) ∈ Bij 𝔻"])
apply (smt (verit) A_0 A1_3 data_symm.axioms data_symm_axioms group.inv_closed
group.surj_const_mult group_action.bij_prop0 image_eqI)
apply (rule conjI)
using A_0
apply blast
by (meson A_0 A1_3 data_symm.axioms data_symm_axioms group.subgroupE(3) group.subgroupE(4)
group.subgroup_self group_action.bij_prop0)
also have H1_3: "... = compose 𝔻 (compose 𝔻 (π (inv⇘G⇙ g) ) (π h)) (π g)"
using A1_0
apply (clarsimp simp add: data_symm_def group_action_def BijGroup_def comp_def
group_hom_def group_hom_axioms_def hom_def restrict_def)
apply (rule meta_mp[of "π (inv⇘G⇙ g) ∈ Bij 𝔻 ∧ π h ∈ Bij 𝔻"])
apply (simp add: A_0 A1_3)
apply (rule conjI)
apply (simp add: A_0 Pi_iff)
using A1_3
by blast
also have H1_4: "... = compose 𝔻 ((π (inv⇘G⇙ g)) ∘ (π h)) (π g)"
using A1_0
apply (clarsimp simp add: data_symm_def group_action_def BijGroup_def comp_def group_hom_def
group_hom_axioms_def hom_def restrict_def compose_def)
using A_0 A1_3
by (meson data_symm.axioms data_symm_axioms group.inv_closed group_action.element_image)
also have H1_5: "... = (λd ∈ 𝔻. ((π (inv⇘G⇙ g)) ∘ (π h) ∘ (π g)) d)"
by (simp add: compose_def)
have H1_6: "⋀c. c ∈ C ⟹ ((π h) ∘ (π g)) c = (π g) c"
using A1_4
by auto
have H1_7: "⋀c. c ∈ C ⟹ ((π (inv⇘G⇙ g)) ∘ (π h) ∘ (π g)) c = c"
using H1_6 A1_0
apply (simp add: data_symm_def group_action_def BijGroup_def compose_def group_hom_def
group_hom_axioms_def hom_def)
by (meson A_0 data_symm.axioms data_symm_axioms group_action.orbit_sym_aux is_subset subsetD)
have H1_8: "∀c. c ∈ C ⟶ π ((inv⇘G⇙ g) ⊗⇘G⇙ h ⊗⇘G⇙ g) c = c"
using H1_7 H1_5
by (metis calculation is_subset restrict_apply' subsetD)
have H1_9: "φ ((inv⇘G⇙ g) ⊗⇘G⇙ h ⊗⇘G⇙ g) x = x"
using H1_8
by (simp add: H1_1)
hence H1_10: "φ ((inv⇘G⇙ g) ⊗⇘G⇙ h ⊗⇘G⇙ g) x = φ ((inv⇘G⇙ g) ⊗⇘G⇙ (h ⊗⇘G⇙ g)) x"
by (smt (verit, ccfv_SIG) A_0 A1_3 group.inv_closed group.subgroupE(4) group.subgroup_self
group_action.composition_rule group_action.element_image group_action_axioms group_hom
group_hom.axioms(1) is_in_set)
have H1_11: "... = ((φ (inv⇘G⇙ g)) ∘ (φ (h ⊗⇘G⇙ g))) x"
using A_0 A1_3 group.subgroupE(4) group.subgroup_self group_action.composition_rule
group_action_axioms group_hom group_hom.axioms(1) is_in_set
by fastforce
have H1_12: "... = ((the_inv_into X (φ g)) ∘ (φ (h ⊗⇘G⇙ g))) x"
using A1_1
apply (simp add: group_action_def)
by (smt (verit) A_0 A1_3 group.inv_closed group.subgroupE(4) group.subgroup_self
group_action.element_image group_action.inj_prop group_action.orbit_sym_aux
group_action_axioms group_hom.axioms(1) is_in_set the_inv_into_f_f)
have H1_13: "((the_inv_into X (φ g)) ∘ (φ (h ⊗⇘G⇙ g))) x = x"
using H1_9 H1_10 H1_11 H1_12
by auto
hence H1_14: "(φ (h ⊗⇘G⇙ g)) x = φ g x"
using H1_13
by (metis A_0 A1_3 comp_apply composition_rule element_image f_the_inv_into_f inj_prop is_in_set
surj_prop)
show "φ h (φ g x) = φ g x"
using A1_3 A1_2 A_0 H1_14 composition_rule
by (simp add: is_in_set)
qed
show "supports G D π X φ (π g ` C) (g ⊙⇘φ⇙ x)"
using supports_axioms
apply (clarsimp simp add: supports_def supports_axioms_def)
apply (intro conjI)
using element_image is_in_set A_0
apply blast
apply (metis A_0 data_symm_def group_action.surj_prop image_mono is_subset)
apply (rule allI; intro impI)
apply (rename_tac h)
by (simp add: H_0)
qed
end
locale nominal = data_symm G D π + alt_grp_act G X φ
for
G :: "('grp, 'b) monoid_scheme" and
D :: "'D set" ("𝔻") and
π and
X :: "'X set" (structure) and
φ +
assumes
is_nominal:
"⋀g x. g ∈ carrier G ⟹ x ∈ X ⟹ ∃C. C ⊆ 𝔻 ∧ finite C ∧ supports G 𝔻 π X φ C x"
locale nominal_det_G_aut = det_G_aut +
nominal G D π A φ + nominal G D π S ψ
for
D :: "'D set" ("𝔻") and
π
text ‹
The following lemma corresponds to lemma 4.8 from \cite{bojanczyk2014automata}:
›
lemma (in eq_var_func) supp_el_pres:
"supports G D π X φ C x ⟹ supports G D π Y ψ C (f x)"
apply (clarsimp simp add: supports_def supports_axioms_def)
apply (rule conjI)
using eq_var_func_axioms
apply (simp add: eq_var_func_def eq_var_func_axioms_def)
apply (intro conjI)
using is_ext_func_bet
apply blast
apply clarify
by (metis is_eq_var_func')
lemma (in nominal) support_union_lem:
fixes f sup_C col
assumes H_f: "f = (λx. (SOME C. C ⊆ 𝔻 ∧ finite C ∧ supports G 𝔻 π X φ C x))"
and H_col: "col ⊆ X ∧ finite col"
and H_sup_C: "sup_C = ⋃{Cx. Cx ∈ f ` col}"
shows "⋀x. x ∈ col ⟹ sup_C ⊆ 𝔻 ∧ finite sup_C ∧ supports G 𝔻 π X φ sup_C x"
proof -
fix x
assume A_0: "x ∈ col"
have H_0: "⋀x. x ∈ X ⟹ ∃C. C ⊆ 𝔻 ∧ finite C ∧ supports G 𝔻 π X φ C x"
using nominal_axioms
apply (clarsimp simp add: nominal_def nominal_axioms_def)
using stabilizer_one_closed stabilizer_subset
by blast
have H_1: "⋀x. x ∈ col ⟹ f x ⊆ 𝔻 ∧ finite (f x) ∧ supports G 𝔻 π X φ (f x) x"
apply (subst H_f)
using someI_ex H_col H_f H_0
by (metis (no_types, lifting) in_mono)
have H_2: "sup_C ⊆ 𝔻"
using H_1
by (simp add: H_sup_C UN_least)
have H_3: "finite sup_C"
using H_1 H_col H_sup_C
by simp
have H_4: "f x ⊆ sup_C"
using H_1 H_sup_C A_0
by blast
have H_5: "⋀g c. ⟦g ∈ carrier G; (c ∈ sup_C ⟶ π g c = c); c ∈ (f x)⟧ ⟹ π g c = c"
using H_4 H_1 A_0
by (auto simp add: image_def supports_def supports_axioms_def)
have H_6: "supports G 𝔻 π X φ sup_C x"
apply (simp add: supports_def supports_axioms_def)
apply (intro conjI)
apply (simp add: data_symm_axioms)
using A_0 H_1 supports.axioms(2)
apply fastforce
using H_col A_0
apply blast
apply (rule H_2)
apply (clarify)
using supports_axioms_def[of G D π X φ sup_C]
apply (clarsimp)
using H_1 A_0
apply (clarsimp simp add: supports_def supports_axioms_def)
using A_0 H_5
by presburger
show "sup_C ⊆ 𝔻 ∧ finite sup_C ∧ supports G 𝔻 π X φ sup_C x"
using H_2 H_3 H_6 by auto
qed
lemma (in nominal) set_of_list_nom:
"nominal G D π (X⇧⋆) (φ⇧⋆)"
proof-
have H_0: "⋀g x. g ∈ carrier G ⟹ ∀x∈set x. x ∈ X ⟹
∃C⊆𝔻. finite C ∧ supports G 𝔻 π (X⇧⋆) (φ⇧⋆) C x"
proof-
fix g w
assume
A1_0: "g ∈ carrier G" and
A1_1: "∀x∈set w. x ∈ X"
have H1_0: "⋀x. x ∈ X ⟹ ∃C⊆𝔻. finite C ∧ supports G 𝔻 π X φ C x"
using A1_0 is_nominal by force
define f where H1_f: "f = (λx. (SOME C. C ⊆ 𝔻 ∧ finite C ∧ supports G 𝔻 π X φ C x))"
define sup_C :: "'D set " where H1_sup_C: "sup_C = ⋃{Cx. Cx ∈ f ` set w}"
have H1_1: "⋀x. x ∈ set w ⟹ sup_C ⊆ 𝔻 ∧ finite sup_C ∧ supports G 𝔻 π X φ sup_C x"
apply (rule support_union_lem[where f = f and col = "set w"])
apply (rule H1_f)
using A1_0
apply (simp add: A1_1 subset_code(1))
apply (rule H1_sup_C)
by simp
have H1_2: "supports G 𝔻 π (X⇧⋆) (φ⇧⋆) sup_C w"
apply (clarsimp simp add: supports_def supports_axioms_def simp del: GMN_simps)
apply (intro conjI)
apply (simp add: data_symm_axioms)
using lists_a_Gset
apply (auto)[1]
apply (simp add: A1_1 in_listsI)
using H1_1 H1_sup_C
apply blast
apply (rule allI; intro impI)
apply clarsimp
apply (rule conjI)
using H1_1
by (auto simp add: supports_def supports_axioms_def map_idI)
show "∃C⊆𝔻. finite C ∧ supports G 𝔻 π (X⇧⋆) (φ⇧⋆) C w"
using nominal_axioms_def
apply (clarsimp simp add: nominal_def simp del: GMN_simps)
using H1_1 H1_2
by (metis Collect_empty_eq H1_sup_C Union_empty empty_iff image_empty infinite_imp_nonempty
subset_empty subset_emptyI supports.is_subset)
qed
show ?thesis
apply (clarsimp simp add: nominal_def nominal_axioms_def simp del: GMN_simps)
apply (intro conjI)
using group.subgroupE(2) group.subgroup_self group_hom group_hom.axioms(1)
apply (simp add: data_symm_axioms)
apply (rule lists_a_Gset)
apply (clarify)
by (simp add: H_0 del: GMN_simps)
qed
subsection ‹
Proving the Myhill-Nerode Theorem for Nominal $G$-Automata
›
context det_G_aut begin
adhoc_overloading
star labels_a_G_set.induced_star_map
end
lemma (in det_G_aut) input_to_init_eqvar:
"eq_var_func G (A⇧⋆) (φ⇧⋆) S ψ (λw∈A⇧⋆. (δ⇧⋆) i w)"
proof-
have H_0: "⋀a g. ⟦∀x∈set a. x ∈ A; map (φ g) a ∈ A⇧⋆; g ∈ carrier G⟧ ⟹
(δ⇧⋆) i (map (φ g) a) = ψ g ((δ⇧⋆) i a)"
proof-
fix w g
assume
A1_0: "∀x∈set w. x ∈ A" and
A1_1: "map (φ g) w ∈ A⇧⋆" and
A1_2: "g ∈ carrier G"
have H1_0: "(δ⇧⋆) (ψ g i) (map (φ g) w) = ψ g ((δ⇧⋆) i w)"
using give_input_eq_var
apply (clarsimp simp add: eq_var_func_axioms_def eq_var_func_def)
using A1_0 A1_1 A1_2 in_listsI is_aut.init_state_is_a_state states_a_G_set.element_image
by (smt (verit, del_insts))
have H1_1: "(ψ g i) = i"
using A1_2 is_aut.init_state_is_a_state init_is_eq_var.is_equivar
by force
show "(δ⇧⋆) i (map (φ g) w) = ψ g ((δ⇧⋆) i w)"
using H1_0 H1_1
by simp
qed
show ?thesis
apply (clarsimp simp add: eq_var_func_def eq_var_func_axioms_def)
apply (intro conjI)
using labels_a_G_set.lists_a_Gset
apply fastforce
apply (simp add: states_a_G_set.group_action_axioms del: GMN_simps)
apply (simp add: in_listsI is_aut.give_input_closed is_aut.init_state_is_a_state)
apply clarify
apply (rule conjI; intro impI)
apply (simp add: H_0)
using labels_a_G_set.surj_prop
by fastforce
qed
lemma (in reach_det_G_aut) input_to_init_surj:
"(λw∈A⇧⋆. (δ⇧⋆) i w) ` (A⇧⋆) = S"
using reach_det_G_aut_axioms
apply (clarsimp simp add: image_def reach_det_G_aut_def reach_det_aut_def
reach_det_aut_axioms_def)
using is_aut.give_input_closed is_aut.init_state_is_a_state
by blast
context reach_det_G_aut begin
adhoc_overloading
star labels_a_G_set.induced_star_map
end
text ‹
The following lemma corresponds to proposition 5.1 from \cite{bojanczyk2014automata}:
›
proposition (in reach_det_G_aut) alpha_nom_imp_states_nom:
"nominal G D π A φ ⟹ nominal G D π S ψ"
proof-
assume
A_0: "nominal G D π A φ"
have H_0: "⋀g x. ⟦g ∈ carrier G; data_symm G D π; group_action G A φ;
∀x. x ∈ A ⟶ (∃C⊆D. finite C ∧ supports G D π A φ C x); x ∈ S⟧
⟹ ∃C⊆D. finite C ∧ supports G D π S ψ C x"
proof -
fix g s
assume
A1_0: "g ∈ carrier G" and
A1_1: "data_symm G D π" and
A1_2: "group_action G A φ" and
A1_3: "∀x. x ∈ A ⟶ (∃C⊆D. finite C ∧ supports G D π A φ C x)" and
A1_4: "s ∈ S"
have H1_0: "⋀x. x ∈ (A⇧⋆) ⟹ ∃C⊆D. finite C ∧ supports G D π (A⇧⋆) (φ⇧⋆) C x"
using nominal.set_of_list_nom[of G D π A φ] A1_2
apply (clarsimp simp add: nominal_def)
by (metis A1_0 A1_1 A1_3 in_listsI labels_a_G_set.induced_star_map_def nominal_axioms_def)
define f where H1_f: "f = (λw∈A⇧⋆. (δ⇧⋆) i w)"
obtain w where H1_w0: "s = f w" and H1_w1: "w ∈ (A⇧⋆)"
using input_to_init_surj A1_4
apply (simp add: H1_f image_def)
by (metis is_reachable)
obtain C where H1_C: "finite C ∧ supports G D π (A⇧⋆) (labels_a_G_set.induced_star_map φ) C w"
by (meson H1_0 H1_w0 H1_w1)
have H1_2: "supports G D π S ψ C s"
apply (subst H1_w0)
apply (rule eq_var_func.supp_el_pres[where X = "A⇧⋆" and φ = "φ⇧⋆"])
apply (subst H1_f)
apply (rule det_G_aut.input_to_init_eqvar[of A S i F δ G φ ψ])
using reach_det_G_aut_axioms
apply (simp add: reach_det_G_aut_def)
using H1_C
by simp
show "∃C⊆D. finite C ∧ supports G D π S ψ C s"
using H1_2 H1_C
by (meson supports.is_subset)
qed
show ?thesis
apply (rule meta_mp[of "(∃g. g ∈ carrier G)"])
subgoal
using A_0 apply (clarsimp simp add: nominal_def nominal_axioms_def)
apply (rule conjI)
subgoal for g
by (clarsimp simp add: states_a_G_set.group_action_axioms)
apply clarify
by (simp add: H_0)
by (metis bot.extremum_unique ex_in_conv is_aut.init_state_is_a_state
states_a_G_set.stabilizer_one_closed states_a_G_set.stabilizer_subset)
qed
text ‹
The following theorem corresponds to theorem 5.2 from \cite{bojanczyk2014automata}:
›
theorem (in G_lang) Nom_G_Myhill_Nerode:
assumes
orb_fin: "finite (orbits G A φ)" and
nom: "nominal G D π A φ"
shows
Nom_G_Myhill_Nerode_LR: "finite (orbits G MN_equiv ([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙)) ⟹
(∃S F :: 'alpha list set set. ∃i :: 'alpha list set. ∃δ. ∃ψ.
reach_det_G_aut_rec_lang A S i F δ G φ ψ L ∧ finite (orbits G S ψ)
∧ nominal_det_G_aut A S i F δ G φ ψ D π)" and
Nom_G_Myhill_Nerode_RL: "(∃S F :: 's set. ∃i :: 's. ∃δ. ∃ψ.
det_G_aut_rec_lang A S i F δ G φ ψ L ∧ finite (orbits G S ψ)
∧ nominal_det_G_aut A S i F δ G φ ψ D π)
⟹ finite (orbits G MN_equiv ([(φ⇧⋆)]⇩≡⇩M⇩N ⇘A⇧⋆⇙))"
proof-
assume
A_0: "finite (orbits G MN_equiv ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙))"
obtain S F :: "'alpha list set set" and i :: "'alpha list set" and δ ψ
where H_MN: "reach_det_G_aut_rec_lang A S i F δ G φ ψ L ∧ finite (orbits G S ψ)"
using A_0 orb_fin G_Myhill_Nerode_LR
by blast
have H_0: "nominal G D π S ψ"
using H_MN
apply (clarsimp simp del: GMN_simps simp add: reach_det_G_aut_rec_lang_def)
using nom reach_det_G_aut.alpha_nom_imp_states_nom
by metis
show "∃S F :: 'alpha list set set. ∃i :: 'alpha list set. ∃δ. ∃ψ.
reach_det_G_aut_rec_lang A S i F δ G φ ψ L ∧
finite (orbits G S ψ) ∧ nominal_det_G_aut A S i F δ G φ ψ D π"
apply (simp add: nominal_det_G_aut_def reach_det_G_aut_rec_lang_def)
using nom H_MN H_0
apply (clarsimp simp add: reach_det_G_aut_rec_lang_def reach_det_G_aut_def
reach_det_aut_axioms_def)
by blast
next
assume A0: "∃S F i δ ψ. det_G_aut_rec_lang A S i F δ G φ ψ L ∧ finite (orbits G S ψ)
∧ nominal_det_G_aut A S i F δ G φ ψ D π"
show "finite (orbits G MN_equiv ([φ⇧⋆]⇩≡⇩M⇩N⇘A⇧⋆⇙))"
using A0 orb_fin
by (meson G_Myhill_Nerode_RL)
qed
end