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) ?
>
>  
>
> Please help me if you have a solution on this problem?
>
>  
>
> Thank you in advance,
>
>  
>
> 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
(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 at 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 at 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 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>
(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> Q A)) \<inter> (Q A \<times> lists
(\<Sigma> A) \<times> Q A))"
  apply (auto dest: trclAD_elems)
  apply (erule trclAD.induct)
  apply (auto simp add: trclAD_elems intro: trcl.cons)
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)
  apply (rule trclAD_by_trcl1)
  apply (rule trclAD_by_trcl2)
  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))"
  by (auto iff add: trclAD_by_trcl elim!: trcl_structE)

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)"
  using trclAD_by_trcl'[of A D] by (simp add: Int_absorb2)

lemma trclAD_subset_trcl: "trclAD A D \<subseteq> trcl (D)" proof -
  have "trclAD A D \<subseteq> (trcl (D \<inter> (Q A \<times> \<Sigma>
A \<times> Q A)))" by (auto simp add: trclAD_by_trcl)
  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
prod_fsm_def, auto dest: trclAD_elems)
  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
(fast dest: trclAD_uncons)
  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
prod_fsm_def, auto dest: trclAD_elems)
  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.