Theory SRS

(*  Title:       String rewrite systems
    ID:
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section ‹ String rewrite systems ›

theory SRS
imports DPN_Setup
begin

text ‹
  This formalizes systems of labelled string rewrite rules and the labelled transition systems induced by them. 
  DPNs are special string rewrite systems.
›

subsection ‹ Definitions ›
type_synonym ('c,'l) rewrite_rule = "'c list × 'l × 'c list" 
type_synonym ('c,'l) SRS = "('c,'l) rewrite_rule set"

syntax
  syn_rew_rule :: "'c list ⇒ 'l ⇒ 'c list ⇒ ('c,'l) rewrite_rule" ("_ ↪⇘_⇙ _" [51,51,51] 51)

translations (* FIXME: This translates all triples, regardless of their type. *)
  "s ↪⇘a⇙ s'" => "(s,a,s')" 

text ‹ A (labelled) rewrite rule @{term "s ↪⇘a⇙ s'"} consists of the left side @{text s}, the label @{text a} and the right side @{text s'}. Intuitively, it means that a substring @{text s} can be 
  rewritten to @{text s'} by an @{text a}-step. A string rewrite system is a set of labelled rewrite rules ›


subsection ‹ Induced Labelled Transition System ›
text ‹ A string rewrite systems induces a labelled transition system on strings by rewriting substrings according to the rules ›

inductive_set tr :: "('c,'l) SRS ⇒ ('c list, 'l) LTS" for S 
where
  rewrite: "(s ↪⇘a⇙ s') ∈ S ⟹ (ep@s@es,a,ep@s'@es) ∈ tr S"


subsection ‹ Properties of the induced LTS ›
text ‹ Adding characters at the start or end of a state does not influence the capability of making a transition ›
lemma srs_ext_s: "(s,a,s')∈tr S ⟹ (wp@s@ws,a,wp@s'@ws)∈tr S" proof -
  assume "(s,a,s')∈tr S"
  then obtain ep es r r' where "s=ep@r@es ∧ s'=ep@r'@es ∧ (r,a,r')∈S" by (fast elim: tr.cases)
  moreover hence "((wp@ep)@r@(es@ws),a,(wp@ep)@r'@(es@ws)) ∈ tr S" by (fast intro: tr.rewrite)
  ultimately show ?thesis by auto
qed  

lemma srs_ext_both: "(s,w,s')∈trcl (tr S) ⟹ (wp@s@ws,w,wp@s'@ws)∈trcl (tr S)"
  apply (induct s w s' rule: trcl.induct)
  apply (simp)
  apply (subgoal_tac "wp @ c @ ws ↪⇘a⇙ wp @ c' @ ws ∈ tr S")
  apply (auto intro: srs_ext_s)
  done  
  
corollary srs_ext_cons: "(s,w,s')∈trcl (tr S) ⟹ (e#s,w,e#s')∈trcl (tr S)" by (rule srs_ext_both[where wp="[e]" and ws="[]", simplified])
corollary srs_ext_pre: "(s,w,s')∈trcl (tr S) ⟹ (wp@s,w,wp@s')∈trcl (tr S)" by (rule srs_ext_both[where ws="[]", simplified])
corollary srs_ext_post: "(s,w,s')∈trcl (tr S) ⟹ (s@ws,w,s'@ws)∈trcl (tr S)" by (rule srs_ext_both[where wp="[]", simplified])

lemmas srs_ext = srs_ext_both srs_ext_pre srs_ext_post


end