Theory LTS

(*  Title:       Conflict analysis/Labelled transition systems
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)
section ‹Labeled transition systems›
theory LTS
imports Main
begin
text_raw ‹\label{thy:LTS}›

text ‹
  Labeled transition systems (LTS) provide a model of a state transition system with named transitions.
›

subsection ‹Definitions›
text ‹An LTS is modeled as a ternary relation between start configuration, transition label and end configuration›
type_synonym ('c,'a) LTS = "('c × 'a × 'c) set"

text ‹Transitive reflexive closure›

inductive_set 
  trcl :: "('c,'a) LTS ⇒ ('c,'a list) LTS"
  for t
  where
  empty[simp]: "(c,[],c) ∈ trcl t"
  | cons[simp]: "⟦ (c,a,c') ∈ t; (c',w,c'') ∈ trcl t ⟧ ⟹ (c,a#w,c'') ∈ trcl t"

subsection ‹Basic properties of transitive reflexive closure›
lemma trcl_empty_cons: "(c,[],c')∈trcl t ⟹ (c=c')"
  by (auto elim: trcl.cases)
lemma trcl_empty_simp[simp]: "(c,[],c')∈trcl t = (c=c')"
  by (auto elim: trcl.cases intro: trcl.intros)

lemma trcl_single[simp]: "((c,[a],c') ∈ trcl t) = ((c,a,c') ∈ t)"
  by (auto elim: trcl.cases)
lemma trcl_uncons: "(c,a#w,c')∈trcl t ⟹ ∃ch . (c,a,ch)∈t ∧ (ch,w,c') ∈ trcl t"
  by (auto elim: trcl.cases)
lemma trcl_uncons_cases: "⟦
    (c,e#w,c')∈trcl S; 
    !!ch. ⟦ (c,e,ch)∈S; (ch,w,c')∈trcl S ⟧ ⟹ P 
  ⟧ ⟹ P"
  by (blast dest: trcl_uncons)
lemma trcl_one_elem: "(c,e,c')∈t ⟹ (c,[e],c')∈trcl t"
  by auto

lemma trcl_unconsE[cases set, case_names split]: "⟦ 
    (c,e#w,c')∈trcl S; 
    !!ch. ⟦(c,e,ch)∈S; (ch,w,c')∈trcl S⟧ ⟹ P
  ⟧ ⟹ P"
  by (blast dest: trcl_uncons)
lemma trcl_pair_unconsE[cases set, case_names split]: "⟦ 
    ((s,c),e#w,(s',c'))∈trcl S; 
    !!sh ch. ⟦((s,c),e,(sh,ch))∈S; ((sh,ch),w,(s',c'))∈trcl S⟧ ⟹ P
  ⟧ ⟹ P"
  by (fast dest: trcl_uncons)

lemma trcl_concat: "!! c . ⟦ (c,w1,c')∈trcl t; (c',w2,c'')∈trcl t ⟧ 
  ⟹ (c,w1@w2,c'')∈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')∈trcl t 
  ⟹ ∃ch . (c,w1,ch)∈trcl t ∧ (ch,w2,c')∈trcl t" 
proof (induct w1)
  case Nil hence "(c,[],c)∈trcl t ∧ (c,w2,c')∈trcl t" by auto
  thus ?case by fast
next
  case (Cons a w1) note IHP = this
  hence "(c,a#(w1@w2),c')∈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)∈t ∧ (chh,w1@w2,c')∈trcl t" by fast
  moreover with IHP obtain ch where "(chh,w1,ch)∈trcl t ∧ (ch,w2,c')∈trcl t" by fast
  ultimately have "(c,a#w1,ch)∈trcl t ∧ (ch,w2,c')∈trcl t" by auto
  thus ?case by fast
qed

subsubsection "Appending of elements to paths"
lemma trcl_rev_cons: "⟦ (c,w,ch)∈trcl T; (ch,e,c')∈T ⟧ ⟹ (c,w@[e],c')∈trcl T"
  by (auto dest: trcl_concat iff add: trcl_single)
lemma trcl_rev_uncons: "(c,w@[e],c')∈trcl T 
  ⟹ ∃ch. (c,w,ch)∈trcl T ∧ (ch,e,c')∈T"
  by (force dest: trcl_unconcat)
lemma trcl_rev_induct[induct set, consumes 1, case_names empty snoc]: "!! c'. ⟦ 
    (c,w,c')∈trcl S; 
    !!c. P c [] c; 
    !!c w c' e c''. ⟦ (c,w,c')∈trcl S; (c',e,c'')∈S; P c w c' ⟧ ⟹ P c (w@[e]) c'' 
  ⟧ ⟹ P c w c'"
  by (induct w rule: rev_induct) (auto dest: trcl_rev_uncons)
lemma trcl_rev_cases: "!!c c'. ⟦ 
    (c,w,c')∈trcl S; 
    ⟦w=[]; c=c'⟧⟹P; 
    !!ch e wh. ⟦ w=wh@[e]; (c,wh,ch)∈trcl S; (ch,e,c')∈S ⟧⟹P 
  ⟧ ⟹ P"
  by (induct w rule: rev_induct) (auto dest: trcl_rev_uncons)

lemma trcl_cons2: "⟦ (c,e,ch)∈T; (ch,f,c')∈T ⟧ ⟹ (c,[e,f],c')∈trcl T"
  by auto

subsubsection "Transitivity reasoning setup"
declare trcl_cons2[trans]    ― ‹It's important that this is declared before @{thm [source] trcl_concat}, because we want @{thm [source] trcl_concat} to be tried first by the transitivity reasoner›
declare cons[trans]
declare trcl_concat[trans]
declare trcl_rev_cons[trans]

subsubsection "Monotonicity"
lemma trcl_mono: "!!A B. A ⊆ B ⟹ trcl A ⊆ trcl B" (* FIXME: Why can't this be declared as [mono] or [mono_set] ? *) 
  apply (clarsimp)
  apply (erule trcl.induct)
  apply auto
done

lemma trcl_inter_mono: "x∈trcl (S∩R) ⟹ x∈trcl S" "x∈trcl (S∩R) ⟹ x∈trcl R"
proof -
  assume "x∈trcl (S∩R)"
  with trcl_mono[of "S∩R" S] show "x∈trcl S" by auto
next
  assume "x∈trcl (S∩R)"
  with trcl_mono[of "S∩R" R] show "x∈trcl R" by auto
qed


subsubsection "Special lemmas for reasoning about states that are pairs"
lemmas trcl_pair_induct = trcl.induct[of "(xc1,xc2)" "xb" "(xa1,xa2)", split_format (complete), consumes 1, case_names empty cons]
lemmas trcl_rev_pair_induct = trcl_rev_induct[of "(xc1,xc2)" "xb" "(xa1,xa2)", split_format (complete), consumes 1, case_names empty snoc]

(*lemma trcl_pair_induct[induct set]: 
  "⟦((xc1,xc2), xb, (xa1,xa2)) ∈ trcl t; ⋀c1 c2. P c1 c2 [] c1 c2; ⋀a c1 c2 c1' c2' c1'' c2'' w. ⟦((c1,c2), a, (c1',c2')) ∈ t; ((c1',c2'), w, (c1'',c2'')) ∈ trcl t; P c1' c2' w c1'' c2''⟧ ⟹ P c1 c2 (a # w) c1'' c2''⟧ 
  ⟹ P xc1 xc2 xb xa1 xa2" 
  using trcl.induct[of "(xc1,xc2)" xb "(xa1,xa2)" t "λc w c'. let (c1,c2)=c in let (c1',c2')=c' in P c1 c2 w c1' c2'"] by auto
*)

subsubsection "Invariants"
(* TODO: Do we really need this ? Is this formulation usable ? *)
lemma trcl_prop_trans[cases set, consumes 1, case_names empty steps]: "⟦
    (c,w,c')∈trcl S; 
    ⟦c=c'; w=[]⟧ ⟹ P;  
    ⟦c∈Domain S; c'∈Range (Range S)⟧⟹P 
  ⟧ ⟹ P"
  apply (erule_tac trcl_rev_cases)
  apply auto
  apply (erule trcl.cases)
  apply auto
  done


end