Email Gateway (Aug 18 2022 at 10:46): Email Gateway (Aug 18 2022 at 10:46):From: Nguyen Van Tang <tang_nguyen@jaist.ac.jp>
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) ?
Please help me if you have a solution on this problem?
Thank you in advance,
Bests,
Tang.
Email Gateway (Aug 18 2022 at 10:46):From: Peter Lammich <peter.lammich@uni-muenster.de>
Nguyen Van Tang wrote:
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@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@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@w2),c')\<in>trcl t" by simp (* Auto/fast/blast do not
get the point _#(_@_) = (_#_)@_ in next step, so making it explicit *)
with trcl_uncons obtain chh where "(c,a,chh)\<in>t \<and>
(chh,w1@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@[e],c')\<in>trcl T" by
(auto dest: trcl_concat iff add: trcl_single)
lemma trcl_rev_uncons: "(c,w@[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@[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@uni-muenster.de>
Maintainer: Peter Lammich <peter.lammich@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
(auto simp add: delta_cons)
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"
inductive "trclAD A D"
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;
(s',w,s'')\<in>trclAD A D\<rbrakk> \<Longrightarrow>
(s,e#w,s'')\<in>trclAD A D"
syntax trclA :: "('s,'a,'c) FSM_rec_scheme \<Rightarrow> ('s,'a list) LTS"
translations "trclA A" => "trclAD A (\<delta> A)"
lemma trclAD_empty_cons[simp]: "(c,[],c')\<in>trclAD A D
\<Longrightarrow> c=c'" by (auto elim: trclAD.cases)
lemma trclAD_single: "(c,[a],c') \<in> trclAD A D \<Longrightarrow>
(c,a,c') \<in> D" by (auto elim: trclAD.cases)
lemma trclAD_elems: "(c,w,c')\<in>trclAD A D \<Longrightarrow> c\<in>Q A
\<and> w\<in>lists (\<Sigma> A) \<and> c'\<in>Q A" by (erule
trclAD.induct, auto)
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
lemma trclAD_uncons: "(c,a#w,c')\<in>trclAD A D \<Longrightarrow>
\<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"
by (auto elim: trclAD.elims)
lemma trclAD_concat: "!! c . \<lbrakk> (c,w1,c')\<in>trclAD A D;
(c',w2,c'')\<in>trclAD A D \<rbrakk> \<Longrightarrow>
(c,w1@w2,c'')\<in>trclAD A D"
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
lemma trclAD_unconcat: "!! c . (c,w1@w2,c')\<in>trclAD A D
\<Longrightarrow> \<exists>ch . (c,w1,ch)\<in>trclAD A D \<and>
(ch,w2,c')\<in>trclAD A D" proof (induct w1)
case Nil hence "(c,[],c)\<in>trclAD A D \<and> (c,w2,c')\<in>trclAD A
D" by (auto dest: trclAD_elems)
thus ?case by fast
next
case (Cons a w1) note IHP = this
hence "(c,a#(w1@w2),c')\<in>trclAD A D" by simp (* Auto/fast/blast do
not get the point _#(_@_) = (_#_)@_ in next step, so making it explicit *)
with trclAD_uncons obtain chh where "(c,a,chh)\<in>D \<and>
(chh,w1@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>
(ch,w2,c')\<in>trclAD A D" by fast
ultimately have "(c,a#w1,ch)\<in>trclAD A D \<and>
(ch,w2,c')\<in>trclAD A D" by auto
thus ?case by fast
qed
lemma trclAD_eq: "\<lbrakk>Q A = Q A'; \<Sigma> A = \<Sigma> A'\<rbrakk>
\<Longrightarrow> trclAD A D = trclAD A' D" by (unfold trclAD.defs) simp
lemma trclAD_mono[mono]: "D\<subseteq>D' \<Longrightarrow> trclAD A D
\<subseteq> trclAD A D'"
apply (clarsimp)
apply (erule trclAD.induct)
apply auto
done
lemma trclAD_mono_adv: "\<lbrakk>D\<subseteq>D'; Q A = Q A'; \<Sigma> A
= \<Sigma> A'\<rbrakk> \<Longrightarrow> trclAD A D \<subseteq> trclAD
A' D'" by (subgoal_tac "trclAD A D = trclAD A' D") (auto dest: trclAD_eq
trclAD_mono)
subsubsection {* Relation of @{term trclAD} and @{term LTS.trcl} *}
lemma trclAD_by_trcl1: "trclAD A D \<subseteq> (trcl (D \<inter> (Q A
\<times> \<Sigma> A \<times>
[message truncated]
Email Gateway (Aug 18 2022 at 10:46):From: Cristiano Longo <cristiano.longo@tvblob.com>
Hi, I used the definition of Non Deterministic Finite State Automaton to build
a "model" for Automaton with a not finite state set. Such automaton can be
defined by
(1) a data type for states
(2) a data type for symbols + a special simbol Epsilon
(3) a transition function (state, symbol Un Epsilon) => state set
The run function in NonDeterministicAutomata.thy compute the final state set
of a such defined machine given the initial state, transition function and a
list of symbols.
Note the use of option datatype to extends the symbol set with epsilon(None).
ExampleNA.thy implements the automata shown in
http://en.wikipedia.org/wiki/Nondeterministic_finite_state_machine.
The transition function is defined as an inductive set. Using this technique
is simpler and clearer that using primrec. But probably is not correct,
because it is not an inductive set.
I have done some experiment. I am not able to understand if a string is
recognized by this automata using quicksearch, and blast loops on some tryng
to chek some string, for example 001010.
I would be happy to receive suggestions about transition function definitions.
Please my english,
Cristiano Longo
Alle 07:25, venerdì 24 agosto 2007, Nguyen Van Tang ha scritto:
NonDeterministicAutomata.thy
ExampleNA.thy
Email Gateway (Aug 18 2022 at 10:46):From: Tobias Nipkow <nipkow@in.tum.de>
Now that we have got on to the subject of (finite) automata, the
following theories from the Archive of Formal Proofs may be of interest:
http://afp.sourceforge.net/entries/Functional-Automata.shtml
Tobias
Cristiano Longo schrieb:
Last updated: May 03 2024 at 04:19 UTC