Theory FSM_ex

(*  Title:       Executable algorithms for finite state machines
    ID:
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section "Executable algorithms for finite state machines"

theory FSM_ex
imports FSM ImplHelper
begin

text ‹ The transition relation of a finite state machine is represented as a list of labeled edges ›
type_synonym ('s,'a) delta = "('s × 'a × 's) list"

subsection ‹ Word lookup operation ›
text ‹
  Operation that finds some state @{term "q'"} that is reachable from state @{term q} with word @{term w} and has additional property @{term P}.
›


primrec lookup :: "('s ⇒ bool) ⇒ ('s,'a) delta ⇒ 's ⇒ 'a list ⇒ 's option" where
  "lookup P d q [] = (if P q then Some q else None)"
| "lookup P d q (e#w) = first_that (λt. let (qs,es,q')=t in if q=qs ∧ e=es then lookup P d q' w else None) d"

lemma lookupE1: "!!q. lookup P d q w = Some q' ⟹ P q' ∧ (q,w,q') ∈ trcl (set d)" proof (induct w)
  case Nil thus ?case by (cases "P q") simp_all
next
  case (Cons e w) note IHP=this
  hence "first_that (λt. let (qs,es,qh)=t in if q=qs ∧ e=es then lookup P d qh w else None) d = Some q'" by simp
  then obtain t where "t∈set d ∧ ((let (qs,es,qh)=t in if q=qs ∧ e=es then lookup P d qh w else None) = Some q')" by (blast dest: first_thatE1)
  then obtain qh where 1: "(q,e,qh)∈set d ∧ lookup P d qh w = Some q'" 
    by (auto split: prod.splits if_splits)
  moreover from 1 IHP have "P q' ∧ (qh,w,q')∈trcl (set d)" by auto
  ultimately show ?case by auto
qed
    
lemma lookupE2: "!!q. lookup P d q w = None ⟹ ¬(∃q'. (P q') ∧ (q,w,q') ∈ trcl (set d))" proof (induct w)
  case Nil thus ?case by (cases "P q") (auto dest: trcl_empty_cons)
next
  case (Cons e w) note IHP=this
  hence "first_that (λt. let (qs,es,qh)=t in if q=qs ∧ e=es then lookup P d qh w else None) d = None" by simp
  hence "∀t∈set d. (let (qs,es,qh)=t in if q=qs ∧ e=es then lookup P d qh w else None) = None" by (blast dest: first_thatE2)
  hence 1: "!! qs es qh.  (qs,es,qh)∈set d ⟹ q≠qs ∨ e≠es ∨ lookup P d qh w = None" by auto
  show ?case proof (rule notI, elim exE conjE)
    fix q'
    assume C: "P q'" "(q,e#w,q')∈trcl (set d)"
    then obtain qh where 2: "(q,e,qh)∈set d ∧ (qh,w,q')∈trcl (set d)" by (blast dest: trcl_uncons)
    with 1 have "lookup P d qh w = None" by auto
    with C 2 IHP show "False" by auto
  qed
qed

lemma lookupI1: "⟦P q'; (q,w,q')∈trcl (set d)⟧ ⟹ ∃q'. lookup P d q w = Some q'" 
  by (cases "lookup P d q w") (auto dest: lookupE2)

lemma lookupI2: "¬(∃q'. P q' ∧ (q,w,q')∈trcl (set d)) ⟹ lookup P d q w = None"
  by (cases "lookup P d q w") (auto dest: lookupE1)

lemmas lookupE = lookupE1 lookupE2
lemmas lookupI = lookupI1 lookupI2


lemma lookup_trclAD_E1:
  assumes map: "set d = D" and start: "q∈Q A" and cons: "D ⊆ Q A × Σ A × Q A"
  assumes A: "lookup P d q w = Some q'"
  shows "P q' ∧ (q,w,q')∈trclAD A D"
proof -
  from A map have 1: "P q' ∧ (q,w,q')∈trcl D" by (blast dest: lookupE1)
  hence "(q,w,q')∈trcl (D ∩ (Q A × Σ A × Q A)) ∩ (Q A × UNIV × UNIV)" using cons start by (subgoal_tac "D = D ∩ (Q A × Σ A × Q A)", auto)
  with 1 trclAD_by_trcl' show ?thesis by auto
qed

lemma lookup_trclAD_E2:
  assumes map: "set d = D"
  assumes A: "lookup P d q w = None"
  shows "¬ (∃q'. P q' ∧ (q,w,q')∈trclAD A D)"
proof -
  from map A have "¬ (∃q'. P q' ∧ (q, w, q') ∈ trcl D)" by (blast dest: lookupE2)
  with trclAD_subset_trcl show ?thesis by auto
qed

lemma lookup_trclAD_I1: "⟦set d = D; (q,w,q')∈trclAD A D; P q'⟧ ⟹ ∃q'. lookup P d q w = Some q'"
  apply (cases "lookup P d q w")
  apply (subgoal_tac "¬(∃q'. P q' ∧ (q,w,q')∈trclAD A D)")
  apply simp
  apply (rule lookup_trclAD_E2)
  apply auto
  done

lemma lookup_trclAD_I2: "⟦set d = D; q∈Q A; D ⊆ Q A × Σ A × Q A; ¬(∃q'. P q' ∧ (q,w,q')∈trclAD A D)⟧ ⟹ lookup P d q w = None"
  apply (cases "lookup P d q w", auto)
  apply (subgoal_tac "P a ∧ (q,w,a)∈trclAD A (set d)")
  apply blast
  apply (rule lookup_trclAD_E1)
  apply auto
  done

lemmas lookup_trclAD_E = lookup_trclAD_E1 lookup_trclAD_E2
lemmas lookup_trclAD_I = lookup_trclAD_I1 lookup_trclAD_I2 

subsection ‹ Reachable states and alphabet inferred from transition relation ›

definition "states d == fst ` (set d) ∪ (snd∘snd) ` (set d)"
definition "alpha d == (fst∘snd) ` (set d)"

lemma statesAlphaI: "(q,a,q')∈set d ⟹ q∈states d ∧ q'∈states d ∧ a∈alpha d" by (unfold states_def alpha_def, force)
lemma statesE: "q∈states d ⟹ ∃a q'. ((q,a,q')∈set d ∨ (q',a,q)∈set d)" by (unfold states_def alpha_def, force)
lemma alphaE: "a∈alpha d ⟹ ∃q q'. (q,a,q')∈set d" by (unfold states_def alpha_def, force)

lemma states_finite: "finite (states d)" by (unfold states_def, auto)
lemma alpha_finite: "finite (alpha d)" by (unfold alpha_def, auto)

lemma statesAlpha_subset: "set d ⊆ states d × alpha d × states d" by (auto dest: statesAlphaI)

lemma states_mono: "set d ⊆ set d' ⟹ states d ⊆ states d'" by (unfold states_def, auto)
lemma alpha_mono: "set d ⊆ set d' ⟹ alpha d ⊆ alpha d'" by (unfold alpha_def, auto)

lemma statesAlpha_insert: "set d' = insert (q,a,q') (set d) ⟹ states d' = states d ∪ {q,q'} ∧ alpha d' = insert a (alpha d)"
  by (unfold states_def alpha_def) (simp, blast)

lemma statesAlpha_inv: "⟦q∈states d; a∈alpha d; q'∈states d; set d'=insert (q,a,q') (set d)⟧ ⟹ states d = states d' ∧ alpha d = alpha d'"
  by (unfold states_def alpha_def) (simp, blast)

export_code lookup checking SML
  

end