# Theory SM.LTS

```section ‹Very Basic LTS Formalization›
theory LTS
imports CAVA_Automata.Digraph
begin

(* TODO: transition labeled automata, not supported by CAVA automata library *)

locale LTS =
fixes step :: "'s ⇒ 'l ⇒ 's ⇒ bool"
begin
primrec path :: "'s ⇒ 'l list ⇒ 's ⇒ bool" where
"path s [] s' ⟷ s'=s"
| "path s (l#ls) s' ⟷ (∃sh. step s l sh ∧ path sh ls s')"

lemma path_append[simp]:
"path s (p@p') s' ⟷ (∃sh. path s p sh ∧ path sh p' s')"
by (induction p arbitrary: s) auto

lemma path_trans[trans]:
"step s l sh ⟹ step sh l' s' ⟹ path s [l,l'] s'"
"step s l sh ⟹ path sh p s' ⟹ path s (l#p) s'"
"path s p sh ⟹ step sh l s' ⟹ path s (p@[l]) s'"
"path s p sh ⟹ path sh p' s' ⟹ path s (p@p') s'"
by auto

lemma path_sngI: "step s a s' ⟹ path s [a] s'" by auto
lemma path_emptyI: "path s [] s" by auto

definition "reachable s s' ≡ ∃p. path s p s'"
lemma reachableI: "path s p s' ⟹ reachable s s'"
unfolding reachable_def by auto

lemma reachable_trans[trans]:
"reachable s sh ⟹ step sh l s' ⟹ reachable s s'"
"reachable s sh ⟹ path sh p s' ⟹ reachable s s'"
"path s p sh ⟹ reachable sh s' ⟹ reachable s s'"
"step s l sh ⟹ reachable sh s' ⟹ reachable s s'"
unfolding reachable_def
by (auto dest: path_trans)

end

locale asystem =
lts: LTS astep
for init :: "'c ⇒ bool"
and astep :: "'c ⇒ 'a ⇒ 'c ⇒ bool"
begin

definition step :: "'c digraph"
where "step ≡ {(c, c'). ∃ a. astep c a c'}"

definition G :: "'c graph_rec"
where "G ≡ ⦇ g_V = UNIV, g_E = step, g_V0 = Collect init ⦈"

lemma G_simps[simp]:
"g_V G = UNIV"
"g_E G = step"
"g_V0 G = Collect init"
unfolding G_def by simp+

sublocale graph G by unfold_locales auto

lemma path_is_step: "lts.path c p c' ⟹ (c, c') ∈ step⇧*"
unfolding step_def
apply (induction p arbitrary: c)
apply auto
by (metis (mono_tags, lifting) case_prod_conv converse_rtrancl_into_rtrancl mem_Collect_eq)

lemma step_is_path: "(c, c') ∈ step⇧* ⟹ ∃p. lts.path c p c'"
proof (induction rule: converse_rtrancl_induct, safe)
fix c
show "∃p. lts.path c p c"
apply (rule exI[where x="[]"])
by auto
next
fix c ch p
assume "(c, ch) ∈ step" and 1: "lts.path ch p c'"
then obtain a where "astep c a ch" by (auto simp: step_def)
with 1 show "∃p. lts.path c p c'"
apply (rule_tac exI[where x="a#p"]) by auto
qed

lemma step_path_conv: "(c, c') ∈ step⇧* ⟷ (∃p. lts.path c p c')"
using path_is_step step_is_path by blast

end

end

```