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