# Re: [isabelle] please, help me !

```Nguyen Van Tang wrote:
> Hi all,
>
>
>
> I am studying Isabelle/HOL. I would like to have one question. Can we use
> Isabelle to formalize "finite paths" of a transition system (or formalize
> finite run of a finite automaton) ?
>
>
>
>
>
>
>
>
>
> Bests,
>
> Tang.
>

This is, how I handle labeled transition systems of all kinds, maybe it
helps

I think on AFP (archive of formal proofs, afp.sf.net) there is also
another example how to formalize FSMs:

theory LTS
imports Main
begin

section {* Labeled transition systems *}
text {*
Labeled transition systems (LTS) provide a model of a state transition
system with named transitions.
*}

subsection {* Definitions *}
text {*  A LTS is modelled as a relation, that relates triples of start
configuration, transition label and end configuration *}
types ('c,'a) LTS = "('c \<times> 'a \<times> 'c) set"

text {* Transitive closure of LTS *}
consts trcl :: "('c,'a) LTS \<Rightarrow> ('c,'a list) LTS"

inductive "trcl t"
intros
empty[simp]: "(c,[],c) \<in> trcl t"
cons[simp, trans]: "\<lbrakk> (c,a,c') \<in> t; (c',w,c'') \<in> trcl
t \<rbrakk> \<Longrightarrow> (c,a#w,c'') \<in> trcl t"

subsection {* Basic properties of transitive closure *}
lemma trcl_empty_cons: "(c,[],c')\<in>trcl t \<Longrightarrow> (c=c')"
by (auto elim: trcl.cases)
lemma trcl_empty_simp[simp]: "(c,[],c')\<in>trcl t = (c=c')" by (auto
elim: trcl.cases intro: trcl.intros)

lemma trcl_single[simp]: "((c,[a],c') \<in> trcl t) = ((c,a,c') \<in>
t)" by (auto elim: trcl.cases)
lemma trcl_uncons: "(c,a#w,c')\<in>trcl t \<Longrightarrow> \<exists>ch
. (c,a,ch)\<in>t \<and> (ch,w,c') \<in> trcl t" by (auto elim: trcl.cases)
lemma trcl_one_elem: "(c,e,c')\<in>t \<Longrightarrow>
(c,[e],c')\<in>trcl t" by auto

lemma trcl_concat[trans]: "!! c . \<lbrakk> (c,w1,c')\<in>trcl t;
(c',w2,c'')\<in>trcl t \<rbrakk> \<Longrightarrow>
(c,w1 at w2,c'')\<in>trcl t"
proof (induct w1)
case Nil thus ?case by (subgoal_tac "c=c'") auto
next
case (Cons a w) thus ?case by (auto dest: trcl_uncons)
qed

lemma trcl_unconcat: "!! c . (c,w1 at w2,c')\<in>trcl t \<Longrightarrow>
\<exists>ch . (c,w1,ch)\<in>trcl t \<and> (ch,w2,c')\<in>trcl t" proof
(induct w1)
case Nil hence "(c,[],c)\<in>trcl t \<and> (c,w2,c')\<in>trcl t" by auto
thus ?case by fast
next
case (Cons a w1) note IHP = this
hence "(c,a#(w1 at w2),c')\<in>trcl t" by simp (* Auto/fast/blast do not
get the point _#(_ at _) = (_#_)@_ in next step, so making it explicit *)
with trcl_uncons obtain chh where "(c,a,chh)\<in>t \<and>
(chh,w1 at w2,c')\<in>trcl t" by fast
moreover with IHP obtain ch where "(chh,w1,ch)\<in>trcl t \<and>
(ch,w2,c')\<in>trcl t" by fast
ultimately have "(c,a#w1,ch)\<in>trcl t \<and> (ch,w2,c')\<in>trcl t"
by auto
thus ?case by fast
qed

lemma trcl_rev_cons[trans]: "\<lbrakk> (c,w,ch)\<in>trcl T;
(ch,e,c')\<in>T \<rbrakk> \<Longrightarrow> (c,w at [e],c')\<in>trcl T" by
(auto dest: trcl_concat iff add: trcl_single)
lemma trcl_rev_uncons: "(c,w at [e],c')\<in>trcl T \<Longrightarrow>
\<exists>ch. (c,w,ch)\<in>trcl T \<and> (ch,e,c')\<in>T" by (force dest:
trcl_unconcat)

lemma trcl_cons2[trans]: "\<lbrakk> (c,e,ch)\<in>T; (ch,f,c')\<in>T
\<rbrakk> \<Longrightarrow> (c,[e,f],c')\<in>trcl T" by auto

lemma trcl_mono[mono]: "A \<subseteq> B \<Longrightarrow> trcl A
\<subseteq> trcl B"
apply (clarsimp)
apply (erule trcl.induct)
apply auto
done

(* TODO: What's this good for ?*)
lemma trcl_pair_simple_induct:
assumes NIL: "!!s c. P s c [] s c"
assumes STEP: "!!s c sh ch e w s' c'.
\<lbrakk>((s,c),e,(sh,ch))\<in>T; P sh ch w s' c'\<rbrakk>
\<Longrightarrow> P s c (e#w) s' c'"
shows "!!s c. ((s,c),w,(s',c'))\<in>trcl T \<Longrightarrow> P s c w
s' c'"
proof (induct w)
case Nil thus ?case using NIL by (auto dest: trcl_empty_cons)
next
case (Cons e w) note IHP=this
then obtain sh ch where SPLIT1: "((s,c),e,(sh,ch))\<in>T" and SPLIT2:
"((sh,ch),w,(s',c'))\<in>trcl T" by (fast dest: trcl_uncons)
with IHP show ?case using STEP by (auto)
qed

lemma trcl_inter_mono: "x\<in>trcl (S\<inter>R) \<Longrightarrow>
x\<in>trcl S" "x\<in>trcl (S\<inter>R) \<Longrightarrow> x\<in>trcl R"
proof -
assume "x\<in>trcl (S\<inter>R)"
with trcl_mono[of "S\<inter>R" S] show "x\<in>trcl S" by auto
next
assume "x\<in>trcl (S\<inter>R)"
with trcl_mono[of "S\<inter>R" R] show "x\<in>trcl R" by auto
qed

lemma trcl_rev_cases: "!!c c'. \<lbrakk> (c,w,c')\<in>trcl S;
\<lbrakk>w=[]; c=c'\<rbrakk>\<Longrightarrow>P; !!ch e wh. \<lbrakk>
w=wh at [e]; (c,wh,ch)\<in>trcl S; (ch,e,c')\<in>S
\<rbrakk>\<Longrightarrow>P \<rbrakk> \<Longrightarrow> P"
by (induct w rule: rev_induct) (simp, blast dest: trcl_rev_uncons)

lemma trcl_prop_trans: "\<lbrakk>(c,w,c')\<in>trcl S; \<lbrakk>c=c';
w=[]\<rbrakk> \<Longrightarrow> P;  \<lbrakk>c\<in>Domain S;
c'\<in>Range (Range S)\<rbrakk>\<Longrightarrow>P \<rbrakk>
\<Longrightarrow> P"
apply (erule_tac trcl_rev_cases)
apply auto
apply (erule trcl.cases)
apply auto
done

lemma trcl_mono_e: "x\<in>trcl (T\<inter>M) \<Longrightarrow> x\<in>trcl
T" using trcl_mono[of "T\<inter>M" T] by auto

end

Finite automata can be done (for example) like this:
(*  Title:       Finite state machines
ID:
Author:      Peter Lammich <peter.lammich at uni-muenster.de>
Maintainer:  Peter Lammich <peter.lammich at uni-muenster.de>
*)

header {* Finite state machines *}
theory FSM
imports Main LTS
begin

text {*
This theory models nondeterministic finite state machines with
explicit set of states and alphabet. @{text \<epsilon>}-transitions are
not supported.
*}

subsection {* Definitions *}

record ('s,'a) FSM_rec =
Q :: "'s set" -- "The set of states"
\<Sigma> :: "'a set" -- "The alphabet"
\<delta> :: "('s, 'a) LTS" -- "The transition relation"
s0 :: "'s" -- "The initial state"
F :: "'s set" -- "The set of final states"

locale FSM = struct A +
assumes delta_cons: "(q,l,q')\<in>\<delta> A \<Longrightarrow> q\<in>Q
A \<and> l\<in>\<Sigma> A \<and> q'\<in>Q A" -- "The transition relation
is consistent with the set of states and the alphabet"
assumes s0_cons: "s0 A \<in> Q A" -- "The initial state is a state"
assumes F_cons: "F A \<subseteq> Q A" -- "The final states are states"
assumes finite_states: "finite (Q A)" -- "The set of states is finite"
assumes finite_alphabet: "finite (\<Sigma> A)" -- "The alphabet is finite"

subsection {* Basic properties *}
lemma (in FSM) finite_delta_dom: "finite (Q A \<times> \<Sigma> A
\<times> Q A)" proof -
from finite_states finite_alphabet finite_cartesian_product[of
"\<Sigma> A" "Q A"] have "finite (\<Sigma> A \<times> Q A)" by fast
with finite_states finite_cartesian_product[of "Q A" "\<Sigma> A
\<times> Q A"] show "finite (Q A \<times> \<Sigma> A \<times> Q A)" by fast
qed

lemma (in FSM) finite_delta: "finite (\<delta> A)" proof -
have "\<delta> A \<subseteq> Q A \<times> \<Sigma> A \<times> Q A" by
with finite_delta_dom show ?thesis by (simp add: finite_subset)
qed

subsection {* Reflexive, transitive closure of transition relation *}

text {* Reflexive transitive closure on restricted domain *}

consts trclAD :: "('s,'a,'c) FSM_rec_scheme \<Rightarrow> ('s,'a) LTS
\<Rightarrow> ('s,'a list) LTS"
intros
empty[simp]: "s\<in>Q A \<Longrightarrow> (s,[],s)\<in>trclAD A D"
cons[simp]: "\<lbrakk>(s,e,s')\<in>D; s\<in>Q A; e\<in>\<Sigma> A;

syntax trclA :: "('s,'a,'c) FSM_rec_scheme \<Rightarrow> ('s,'a list) LTS"
translations "trclA A" => "trclAD A (\<delta> A)"

\<Longrightarrow> c=c'" by (auto elim: trclAD.cases)
(c,a,c') \<in> D" by (auto elim: trclAD.cases)
\<and> w\<in>lists (\<Sigma> A) \<and> c'\<in>Q A" by (erule
lemma trclAD_one_elem: "\<lbrakk>c\<in>Q A; e\<in>\<Sigma> A; c'\<in>Q
A; (c,e,c')\<in>D\<rbrakk> \<Longrightarrow> (c,[e],c')\<in>trclAD A D"
by auto

\<exists>ch . (c,a,ch)\<in>D \<and> (ch,w,c') \<in> trclAD A D \<and>
c\<in>Q A \<and> a\<in>\<Sigma> A"

proof (induct w1)
case Nil thus ?case by (subgoal_tac "c=c'") auto
next
case (Cons a w) thus ?case by (auto dest: trclAD_uncons)
qed

\<Longrightarrow> \<exists>ch . (c,w1,ch)\<in>trclAD A D \<and>
(ch,w2,c')\<in>trclAD A D" proof (induct w1)
thus ?case by fast
next
case (Cons a w1) note IHP = this
hence "(c,a#(w1 at w2),c')\<in>trclAD A D" by simp (* Auto/fast/blast do
not get the point _#(_ at _) = (_#_)@_ in next step, so making it explicit *)
with trclAD_uncons obtain chh where "(c,a,chh)\<in>D \<and>
(chh,w1 at w2,c')\<in>trclAD A D \<and> c\<in>Q A \<and> a\<in>\<Sigma> A"
by fast
moreover with IHP obtain ch where "(chh,w1,ch)\<in>trclAD A D \<and>
ultimately have "(c,a#w1,ch)\<in>trclAD A D \<and>
thus ?case by fast
qed

lemma trclAD_eq: "\<lbrakk>Q A = Q A'; \<Sigma> A = \<Sigma> A'\<rbrakk>

apply (clarsimp)
apply auto
done

subsubsection {* Relation of @{term trclAD} and @{term LTS.trcl} *}
\<times> \<Sigma> A \<times> Q A)) \<inter> (Q A \<times> lists
(\<Sigma> A) \<times> Q A))"
done

lemma trclAD_by_trcl2: "(trcl (D \<inter> (Q A \<times> \<Sigma> A
\<times> Q A)) \<inter> (Q A \<times> lists (\<Sigma> A) \<times> Q A))
\<subseteq> trclAD A D " proof -
{ fix c
have "!! s s' . \<lbrakk>(s, c, s') \<in> trcl (D \<inter> Q A
\<times> \<Sigma> A \<times> Q A); s\<in>Q A; s'\<in>Q A; c\<in>lists
(\<Sigma> A)\<rbrakk> \<Longrightarrow> (s,c,s')\<in>trclAD A D" proof
(induct c)
case Nil thus ?case by (auto dest: trcl_empty_cons)
next
case (Cons e w) note IHP=this
then obtain sh where SPLIT: "(s,e,sh)\<in>(D \<inter> Q A \<times>
\<Sigma> A \<times> Q A) \<and> (sh,w,s')\<in>trcl (D \<inter> Q A
\<times> \<Sigma> A \<times> Q A)" by (fast dest: trcl_uncons)
hence "(sh,w,s')\<in>trcl (D \<inter> Q A \<times> \<Sigma> A
\<times> Q A) \<inter> (Q A \<times> lists (\<Sigma> A) \<times> Q A)"
by (auto elim!: trcl_structE)
hence "(sh,w,s')\<in>trclAD A D" by (blast dest: IHP)
with SPLIT show ?case by auto
qed
}
thus ?thesis by (auto)
qed

lemma trclAD_by_trcl: "trclAD A D = (trcl (D \<inter> (Q A \<times>
\<Sigma> A \<times> Q A)) \<inter> (Q A \<times> lists (\<Sigma> A)
\<times> Q A))"
apply (rule equalityI)
done

lemma trclAD_by_trcl': "trclAD A D = (trcl (D \<inter> (Q A \<times>
\<Sigma> A \<times> Q A)) \<inter> (Q A \<times> UNIV \<times> UNIV))"

lemma trclAD_by_trcl'': "\<lbrakk> D\<subseteq>Q A \<times> \<Sigma> A
\<times> Q A \<rbrakk> \<Longrightarrow> trclAD A D = trcl D \<inter> (Q
A \<times> UNIV \<times> UNIV)"

have "trclAD A D \<subseteq> (trcl (D \<inter> (Q A \<times> \<Sigma>
also with trcl_mono[of "D \<inter> (Q A \<times> \<Sigma> A \<times> Q
A)" D] have "\<dots> \<subseteq> trcl D" by auto
finally show ?thesis .
qed

subsection {* Language of a FSM *}

constdefs
(*langs :: "('s,'a) FSM_rec \<Rightarrow> 's \<Rightarrow> ('a list)
set"*)
"langs A s == { w . (\<exists> f\<in>(F A) . (s,w,f) \<in> trclA A) }"
"lang A == langs A (s0 A)"

lemma langs_alt_def: "(w\<in>langs A s) == (\<exists>f . f\<in>F A &
(s,w,f) \<in> trclA A)" by (intro eq_reflection, unfold langs_def, auto)

subsection {* Example: Product automaton *}

constdefs
(*prod_fsm :: "('s,'a,'c) FSM_rec_scheme \<Rightarrow> ('t,'a,'d)
FSM_rec_scheme \<Rightarrow> ('s*'t,'a,'e) FSM_rec_scheme"*)
"prod_fsm A1 A2 == \<lparr> Q=Q A1 \<times> Q A2, \<Sigma>=\<Sigma> A1
\<inter> \<Sigma> A2, \<delta> = { ((s,t),a,(s',t')) .
(s,a,s')\<in>\<delta> A1 \<and> (t,a,t')\<in>\<delta> A2 }, s0=(s0 A1,s0
A2), F = {(s,t) . s\<in>F A1 \<and> t\<in>F A2} \<rparr>"

lemma prod_inter_1: "!! s s' f f' . ((s,s'),w,(f,f')) \<in> trclA
(prod_fsm A A') \<Longrightarrow> (s,w,f) \<in> trclA A \<and> (s',w,f')
\<in> trclA A'" proof (induct w)
case Nil note P=this
moreover hence "s=f \<and> s'=f'" by (fast dest: trclAD_empty_cons)
moreover from P have "s\<in>Q A \<and> s'\<in>Q A'" by (unfold
ultimately show ?case by (auto)
next
case (Cons e w)
note IHP=this
then obtain m m' where I: "((s,s'),e,(m,m')) \<in> \<delta> (prod_fsm
A A') \<and> (s,s')\<in>Q (prod_fsm A A') \<and> e\<in>\<Sigma>
(prod_fsm A A') \<and> ((m,m'),w,(f,f'))\<in>trclA (prod_fsm A A')" by
hence "(s,e,m)\<in>\<delta> A \<and> (s',e,m')\<in>\<delta> A' \<and>
s\<in>Q A \<and> s'\<in>Q A' \<and> e\<in>\<Sigma> A \<and>
e\<in>\<Sigma> A'" by (unfold prod_fsm_def, simp)
moreover from I IHP have "(m,w,f)\<in>trclA A \<and>
(m',w,f')\<in>trclA A'" by auto
ultimately show ?case by auto
qed

lemma prod_inter_2: "!! s s' f f' . (s,w,f) \<in> trclA A \<and>
(s',w,f') \<in> trclA A' \<Longrightarrow> ((s,s'),w,(f,f')) \<in> trclA
(prod_fsm A A')" proof (induct w)
case Nil note P=this
moreover hence "s=f \<and> s'=f'" by (fast dest: trclAD_empty_cons)
moreover from P have "(s,s')\<in>Q (prod_fsm A A')" by (unfold
ultimately show ?case by simp
next
case (Cons e w)
note IHP=this
then obtain m m' where I: "(s,e,m)\<in>\<delta> A \<and>
(m,w,f)\<in>trclA A \<and> (s',e,m')\<in>\<delta> A' \<and>
(m',w,f')\<in>trclA A' \<and> s\<in>Q A \<and> s'\<in>Q A' \<and>
e\<in>\<Sigma> A \<and> e\<in>\<Sigma> A'" by (fast dest: trclAD_uncons)
hence "((s,s'),e,(m,m')) \<in> \<delta> (prod_fsm A A') \<and>
(s,s')\<in>Q (prod_fsm A A') \<and> e\<in>\<Sigma> (prod_fsm A A')" by
(unfold prod_fsm_def, simp)
moreover from I IHP have "((m,m'),w,(f,f')) \<in> trclA (prod_fsm A
A')" by auto
ultimately show ?case by auto
qed

lemma prod_F: "(a,b)\<in>F (prod_fsm A B) = (a\<in>F A \<and> b\<in>F
B)" by (unfold prod_fsm_def, auto)
lemma prod_FI: "\<lbrakk>a\<in>F A; b\<in>F B\<rbrakk> \<Longrightarrow>
(a,b)\<in>F (prod_fsm A B)" by (unfold prod_fsm_def, auto)

lemma prod_fsm_langs: "langs (prod_fsm A B) (s,t) = langs A s \<inter>
langs B t"
apply (unfold langs_def)
apply (insert prod_inter_1 prod_F)
apply (fast intro: prod_inter_2 prod_FI)
done

lemma prod_FSM_intro: "FSM A1 \<Longrightarrow> FSM A2 \<Longrightarrow>
FSM (prod_fsm A1 A2)" by (rule FSM.intro) (auto simp add: FSM_def
prod_fsm_def)

end

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.