Theory SA

(*  Title:      statecharts/SA/SA.thy

    Author:     Steffen Helke and Florian Kammüller, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Sequential Automata›
theory SA
imports Expr
begin

definition
  SeqAuto :: "['s set,
               's,
               (('s,'e,'d)label) set,
               (('s,'e,'d)trans) set]
              => bool" where
  "SeqAuto S I L D =  (I ∈ S ∧ S ≠ {} ∧  finite S ∧ finite D ∧ 
                       (∀ (s,l,t) ∈ D. s ∈ S ∧ t ∈ S ∧ l ∈ L))"

lemma SeqAuto_EmptySet:
 "({@x .True}, (@x .True), {}, {}) ∈ {(S,I,L,D) | S I L D. SeqAuto S I L D}"
by (unfold SeqAuto_def, auto)

definition
  "seqauto =
    { (S,I,L,D) |
              (S::'s set)
              (I::'s)
              (L::(('s,'e,'d)label) set)
              (D::(('s,'e,'d)trans) set).
             SeqAuto S I L D}"

typedef ('s,'e,'d) seqauto =
    "seqauto :: ('s set * 's * (('s,'e,'d)label) set * (('s,'e,'d)trans) set) set"
  unfolding seqauto_def
  apply (rule exI)
  apply (rule SeqAuto_EmptySet)
  done

definition
 States :: "(('s,'e,'d)seqauto) => 's set" where
 "States = fst o Rep_seqauto"

definition
 InitState :: "(('s,'e,'d)seqauto) => 's" where
 "InitState = fst o snd o Rep_seqauto"

definition
 Labels :: "(('s,'e,'d)seqauto) => (('s,'e,'d)label) set" where
 "Labels = fst o snd o snd o Rep_seqauto"

definition
 Delta :: "(('s,'e,'d)seqauto) => (('s,'e,'d)trans) set" where
 "Delta = snd o snd o snd o Rep_seqauto"

definition
 SAEvents :: "(('s,'e,'d)seqauto) => 'e set" where
 "SAEvents SA = (⋃ l ∈ Label (Delta SA). (fst (action l)) ∪ (ExprEvents (expr l)))"

lemma Rep_seqauto_tuple:
  "Rep_seqauto SA = (States SA, InitState SA, Labels SA, Delta SA)"
by (unfold States_def InitState_def Labels_def Delta_def, auto)

lemma Rep_seqauto_select:
  "(States SA,InitState SA,Labels SA,Delta SA) ∈  seqauto"
by (rule Rep_seqauto_tuple [THEN subst], rule Rep_seqauto)

lemma SeqAuto_select:
  "SeqAuto (States SA) (InitState SA) (Labels SA) (Delta SA)"
by (cut_tac SA=SA in Rep_seqauto_select, unfold seqauto_def, auto)

lemma neq_States [simp]:
  "States SA ≠ {}"
apply (cut_tac Rep_seqauto_select)
apply auto
apply (unfold seqauto_def SeqAuto_def)
apply auto
done

lemma SA_States_disjunct :
 "(States A) ∩ (States A') = {} ⟹ A' ≠ A"
by auto

lemma SA_States_disjunct2 : 
 "⟦ (States A) ∩ C = {}; States B ⊆ C ⟧ ⟹ B ≠ A"
apply (rule SA_States_disjunct)
apply auto
done

lemma SA_States_disjunct3 : 
 "⟦ C ∩ States A = {}; States B ⊆ C ⟧ ⟹  States A ∩ States B = {}"
apply (cut_tac SA=B in neq_States)
apply fast
done

lemma EX_State_SA [simp]:
  "∃ S. S ∈ States SA"
apply (cut_tac Rep_seqauto_select)
apply (unfold seqauto_def SeqAuto_def)
apply auto
done

lemma finite_States [simp]:
  "finite (States A)"
apply (cut_tac Rep_seqauto_select) 
apply (unfold seqauto_def SeqAuto_def)
apply auto
done

lemma finite_Delta [simp]: 
  "finite (Delta A)"
apply (cut_tac Rep_seqauto_select) 
apply (unfold seqauto_def SeqAuto_def)
apply auto
done

lemma InitState_States [simp]:
  "InitState A ∈ States A"
apply (cut_tac Rep_seqauto_select)
apply (unfold seqauto_def SeqAuto_def)
apply auto
done

lemma SeqAuto_EmptySet_States [simp]:
 "(States (Abs_seqauto ({@x. True}, (@x. True), {}, {}))) = {(@x. True)}"
apply (unfold States_def)
apply (simp)
apply (subst Abs_seqauto_inverse)
apply (unfold seqauto_def)
apply (rule SeqAuto_EmptySet)
apply auto
done

lemma SeqAuto_EmptySet_SAEvents [simp]:
 "(SAEvents (Abs_seqauto ({@x. True}, (@x. True), {}, {}))) = {}"
apply (unfold SAEvents_def Delta_def) 
apply simp
apply (subst Abs_seqauto_inverse)
apply (unfold seqauto_def)
apply (rule SeqAuto_EmptySet)
apply auto
done

lemma Label_Delta_subset [simp]:
  "(Label (Delta SA)) ⊆ Labels SA"
apply (unfold Label_def label_def)
apply auto
apply (cut_tac SA=SA in SeqAuto_select)
apply (unfold SeqAuto_def)
apply auto
done

lemma Target_SAs_Delta_States:
  "Target (⋃(Delta ` (SAs HA))) ⊆ ⋃(States ` (SAs HA))"
apply (unfold image_def Target_def target_def)
apply auto
apply (rename_tac SA Source Trigger Guard Action Update Target)
apply (cut_tac SA=SA in SeqAuto_select)
apply (unfold SeqAuto_def)
apply auto
done

lemma States_Int_not_mem:
 "(⋃(States ` F) Int States SA) = {} ⟹ SA ∉ F"
apply (unfold Int_def)
apply auto
apply (subgoal_tac "∃ S. S ∈ States SA")
prefer 2
apply (rule EX_State_SA)
apply (erule exE)
apply (rename_tac T)
apply (erule_tac x=T in allE)
apply auto
done

lemma Delta_target_States [simp]:
  "⟦ T ∈ Delta A⟧ ⟹ target T ∈ States A"
apply (cut_tac SA=A in SeqAuto_select)
apply (unfold SeqAuto_def source_def target_def)
apply auto
done

lemma Delta_source_States [simp]:
  "⟦ T ∈ Delta A ⟧ ⟹ source T ∈ States A"
apply (cut_tac SA=A in SeqAuto_select)
apply (unfold SeqAuto_def source_def target_def)
apply auto
done

end