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