Theory Stuttering_Extension

```theory Stuttering_Extension
imports Simulation Step_Conv
begin

definition stutter_extend_edges :: "'v set ⇒ 'v digraph ⇒ 'v digraph"
where "stutter_extend_edges V E ≡ E ∪ {(v, v) |v. v ∈ V ∧ v ∉ Domain E}"

lemma stutter_extend_edgesI_edge:
assumes "(u, v) ∈ E"
shows "(u, v) ∈ stutter_extend_edges V E"
using assms unfolding stutter_extend_edges_def by auto
lemma stutter_extend_edgesI_stutter:
assumes "v ∈ V" "v ∉ Domain E"
shows "(v, v) ∈ stutter_extend_edges V E"
using assms unfolding stutter_extend_edges_def by auto
lemma stutter_extend_edgesE:
assumes "(u, v) ∈ stutter_extend_edges V E"
obtains (edge) "(u, v) ∈ E" | (stutter) "u ∈ V" "u ∉ Domain E" "u = v"
using assms unfolding stutter_extend_edges_def by auto

lemma stutter_extend_wf: "E ⊆ V × V ⟹ stutter_extend_edges V E ⊆ V × V"
unfolding stutter_extend_edges_def by auto

lemma stutter_extend_edges_rtrancl[simp]: "(stutter_extend_edges V E)⇧* = E⇧*"
unfolding stutter_extend_edges_def by (auto intro: in_rtrancl_UnI elim: rtrancl_induct)

lemma stutter_extend_domain: "V ⊆ Domain (stutter_extend_edges V E)"
unfolding stutter_extend_edges_def by auto

definition stutter_extend :: "('v, _) graph_rec_scheme ⇒ ('v, _) graph_rec_scheme"
where "stutter_extend G ≡
⦇
g_V = g_V G,
g_E = stutter_extend_edges (g_V G) (g_E G),
g_V0 = g_V0 G,
… = graph_rec.more G
⦈"

lemma stutter_extend_simps[simp]:
"g_V (stutter_extend G) = g_V G"
"g_E (stutter_extend G) = stutter_extend_edges (g_V G) (g_E G)"
"g_V0 (stutter_extend G) = g_V0 G"
unfolding stutter_extend_def by auto

lemma stutter_extend_simps_sa[simp]:
"sa_L (stutter_extend G) = sa_L G"
unfolding stutter_extend_def
by (metis graph_rec.select_convs(4) sa_rec.select_convs(1) sa_rec.surjective)

lemma (in graph) stutter_extend_graph: "graph (stutter_extend G)"
using V0_ss E_ss by (unfold_locales, auto intro!: stutter_extend_wf)
lemma (in sa) stutter_extend_sa: "sa (stutter_extend G)"
proof -
interpret graph "stutter_extend G" using stutter_extend_graph by this
show ?thesis by unfold_locales
qed

lemma (in bisimulation) stutter_extend: "bisimulation R (stutter_extend A) (stutter_extend B)"
proof -
interpret ea: graph "stutter_extend A" by (rule a.stutter_extend_graph)
interpret eb: graph "stutter_extend B" by (rule b.stutter_extend_graph)
show ?thesis
proof
fix a b
assume "a ∈ g_V (stutter_extend A)" "(a, b) ∈ R"
thus "b ∈ g_V (stutter_extend B)" using s1.nodes_sim by simp
next
fix a
assume "a ∈ g_V0 (stutter_extend A)"
thus "∃ b. b ∈ g_V0 (stutter_extend B) ∧ (a, b) ∈ R" using s1.init_sim by simp
next
fix a a' b
assume "(a, a') ∈ g_E (stutter_extend A)" "(a, b) ∈ R"
thus "∃ b'. (b, b') ∈ g_E (stutter_extend B) ∧ (a', b') ∈ R"
apply simp
using s1.nodes_sim s1.step_sim s2.stuck_sim
by (blast
intro: stutter_extend_edgesI_edge stutter_extend_edgesI_stutter
elim: stutter_extend_edgesE)
next
fix b a
assume "b ∈ g_V (stutter_extend B)" "(b, a) ∈ R¯"
thus "a ∈ g_V (stutter_extend A)" using s2.nodes_sim by simp
next
fix b
assume "b ∈ g_V0 (stutter_extend B)"
thus "∃ a. a ∈ g_V0 (stutter_extend A) ∧ (b, a) ∈ R¯" using s2.init_sim by simp
next
fix b b' a
assume "(b, b') ∈ g_E (stutter_extend B)" "(b, a) ∈ R¯"
thus "∃ a'. (a, a') ∈ g_E (stutter_extend A) ∧ (b', a') ∈ R¯"
apply simp
using s2.nodes_sim s2.step_sim s1.stuck_sim
by (blast
intro: stutter_extend_edgesI_edge stutter_extend_edgesI_stutter
elim: stutter_extend_edgesE)
qed
qed

lemma (in lbisimulation) lstutter_extend: "lbisimulation R (stutter_extend A) (stutter_extend B)"
proof -
interpret se: bisimulation R "stutter_extend A" "stutter_extend B" by (rule stutter_extend)
show ?thesis by (unfold_locales, auto simp: s1.labeling_consistent)
qed

definition stutter_extend_en :: "('s⇒'a set) ⇒ ('s ⇒ 'a option set)" where
"stutter_extend_en en ≡ λs. let as = en s in if as={} then {None} else Some`as"

definition stutter_extend_ex :: "('a ⇒ 's ⇒ 's) ⇒ ('a option ⇒ 's ⇒ 's)" where
"stutter_extend_ex ex ≡ λNone ⇒ id | Some a ⇒ ex a"

abbreviation stutter_extend_enex
:: "('s⇒'a set) × ('a ⇒ 's ⇒ 's) ⇒ ('s ⇒ 'a option set) × ('a option ⇒ 's ⇒ 's)"
where
"stutter_extend_enex ≡ map_prod stutter_extend_en stutter_extend_ex"

lemma stutter_extend_pred_of_enex_conv:
"stutter_extend_edges UNIV (rel_of_enex enex) = rel_of_enex (stutter_extend_enex enex)"
unfolding rel_of_enex_def stutter_extend_edges_def
apply (auto simp: stutter_extend_en_def stutter_extend_ex_def split: prod.splits)
apply force
apply blast
done

lemma stutter_extend_en_Some_eq[simp]:
"Some a ∈ stutter_extend_en en gc ⟷ a ∈ en gc"
"stutter_extend_ex ex (Some a) gc = ex a gc"
unfolding stutter_extend_en_def stutter_extend_ex_def by auto

lemma stutter_extend_ex_None_eq[simp]:
"stutter_extend_ex ex None = id"
unfolding stutter_extend_ex_def by auto

end
```