Theory Program-Conflict-Analysis.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: "xtrcl (SR)  xtrcl S" "xtrcl (SR)  xtrcl R"
proof -
  assume "xtrcl (SR)"
  with trcl_mono[of "SR" S] show "xtrcl S" by auto
next
  assume "xtrcl (SR)"
  with trcl_mono[of "SR" R] show "xtrcl 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;  
    cDomain S; c'Range (Range S)P 
    P"
  apply (erule_tac trcl_rev_cases)
  apply auto
  apply (erule trcl.cases)
  apply auto
  done


end