Session Statecharts

Theory Contrib

(*  Title:      statecharts/DataSpace/Contrib.thy
    Author:     Steffen Helke and Florian Kammüller, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Contributions to the Standard Library of HOL›

theory Contrib
imports Main
begin

subsection ‹Basic definitions and lemmas›

subsubsection ‹Lambda expressions›                  

definition restrict :: "['a => 'b, 'a set] => ('a => 'b)" where
 "restrict f A = (%x. if x : A then f x else (@ y. True))"

syntax (ASCII)
  "_lambda_in" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
syntax
  "_lambda_in" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3λ__./ _)" [0, 0, 3] 3)
translations 
  "λxA. f"  == "CONST restrict (%x. f) A"


subsubsection ‹Maps›                  

definition chg_map :: "('b => 'b) => 'a => ('a  'b) => ('a  'b)" where  
 "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))"

lemma map_some_list [simp]:
   "map the (map Some L) = L"
apply (induct_tac L)
apply auto
done

lemma dom_ran_the:
  " ran G = {y}; x  (dom G)   (the (G x)) = y"
apply (unfold ran_def dom_def)
apply auto
done

lemma dom_None:
  "(S  dom F)  (F S = None)"
by (unfold dom_def, auto)

lemma ran_dom_the:
  " y  Union (ran G); x  dom G   y  the (G x)"
by (unfold ran_def dom_def, auto)

lemma dom_map_upd: "dom(m(a|->b)) = insert a (dom m)"
apply auto
done

subsubsection rtrancl›

lemma rtrancl_Int:
 " (a,b)  A; (a,b)  B   (a,b)  (A   B)^*"
by auto

lemma rtrancl_mem_Sigma:
 " a  b; (a, b)  (A × A)^*   b  A"
apply (frule rtranclD)
apply (cut_tac r="A × A" and A=A in trancl_subset_Sigma)
apply auto
done

lemma help_rtrancl_Range:
 " a  b; (a,b)  R ^*   b  Range R"
apply (erule rtranclE)
apply auto
done

lemma rtrancl_Int_help:
  "(a,b)  (A  B) ^*  ==> (a,b)  A^*  (a,b)  B^*"
apply (unfold Int_def)
apply auto
apply (rule_tac b=b in rtrancl_induct)
apply auto
apply (rule_tac b=b in rtrancl_induct)
apply auto
done

lemmas rtrancl_Int1 = rtrancl_Int_help [THEN conjunct1]
lemmas rtrancl_Int2 = rtrancl_Int_help [THEN conjunct2]

lemma tranclD3 [rule_format]:
  "(S,T)  R^+  (S,T)  R  ( U. (S,U)  R  (U,T)  R^+)"
apply (rule_tac a="S" and b="T" and r=R in trancl_induct)
apply auto
done

lemma tranclD4 [rule_format]:
  "(S,T)  R^+  (S,T)  R  ( U. (S,U)  R^+  (U,T)  R)"
apply (rule_tac a="S" and b="T" and r=R in trancl_induct)
apply auto
done

lemma trancl_collect [rule_format]:
  " (x,y)  R^*; S  Domain R   y  S  (x,y)  {p. fst p  S  snd p  S  p  R}^*"
apply (rule_tac b=y in rtrancl_induct)
apply auto
apply (rule rtrancl_into_rtrancl)
apply fast
apply auto
done

lemma trancl_subseteq:
  " R  Q; S  R^*   S  Q^*"
apply (frule rtrancl_mono)
apply fast
done

lemma trancl_Int_subset:
   "(R  (A × A))+  R+  (A × A)"
apply (rule subsetI) 
apply (rename_tac S)
apply (case_tac "S")
apply (rename_tac T V)
apply auto
apply (rule_tac a=T and b=V and r="(R   A × A)" in converse_trancl_induct, auto)+
done

lemma trancl_Int_mem:
   "(S,T)  (R  (A × A))+  (S,T)   R+  A × A"
by (rule trancl_Int_subset [THEN subsetD], assumption)

lemma Int_expand: 
  "{(S,S'). P S S'   Q S S'} = ({(S,S'). P S S'}  {(S,S'). Q S S'})"
by auto

subsubsection finite›

lemma finite_conj:  
 "finite ({(S,S'). P S S'}::(('a*'b)set))   
     finite {(S,S'). P (S::'a) (S'::'b)  Q (S::'a) (S'::'b)}"
apply (rule impI)
apply (subst Int_expand)
apply (rule finite_Int)
apply auto
done

lemma finite_conj2:
  " finite A; finite B   finite ({(S,S'). S: A  S' : B})"
by auto

subsubsection override›

lemma dom_override_the:
  "(x  (dom G2))  ((G1 ++ G2) x) = (G2 x)"
by (auto)

lemma dom_override_the2 [simp]:
  " dom G1  dom G2 = {}; x  (dom G1)   ((G1 ++ G2) x) = (G1 x)"
apply (unfold dom_def map_add_def)
apply auto
apply (drule sym)
apply (erule equalityE)
apply (unfold Int_def)
apply auto
apply (erule_tac x=x in allE)
apply auto
done 

lemma dom_override_the3 [simp]:
  " x  dom G2; x  dom G1   ((G1 ++ G2) x) = (G1 x)"
apply (unfold dom_def map_add_def)
apply auto
done

lemma Union_ran_override [simp]:
  "S  dom G   (ran (G ++ Map.empty(S  insert SA (the(G S))))) = 
   (insert SA (Union (ran G)))"
apply (unfold dom_def ran_def)
apply auto
apply (rename_tac T)
apply (case_tac "T = S")
apply auto
done

lemma Union_ran_override2 [simp]:
  "S  dom G   (ran (G(S  insert SA (the(G S))))) = (insert SA (Union (ran G)))"
apply (unfold dom_def ran_def)
apply auto
apply (rename_tac T)
apply (case_tac "T = S")
apply auto
done

lemma ran_override [simp]:
  "(dom A  dom B) = {}  ran (A ++ B) = (ran A)  (ran B)"
apply (unfold Int_def ran_def)
apply (simp add: map_add_Some_iff)
apply auto
done

lemma chg_map_new [simp]:
  "m a = None  chg_map f a m = m"
by (unfold chg_map_def, auto)

lemma chg_map_upd [simp]:
  "m a = Some b  chg_map f a m = m(a|->f b)"
by (unfold chg_map_def, auto)

lemma ran_override_chg_map:
  "A  dom G  ran (G ++ Map.empty(A|->B)) = (ran (chg_map (λ x. B) A G))"
apply (unfold dom_def ran_def)
apply (subst map_add_Some_iff [THEN ext])
apply auto
apply (rename_tac T)
apply (case_tac "T = A")
apply auto
done

subsubsection Part›

definition  Part :: "['a set, 'b => 'a] => 'a set" where
            "Part A h = A  {x.  z. x = h(z)}"
 

lemma Part_UNIV_Inl_comp: 
 "((Part UNIV (Inl o f)) = (Part UNIV (Inl o g))) = ((Part UNIV f) = (Part UNIV g))"
apply (unfold Part_def)
apply auto
apply (erule equalityE)
apply (erule subsetCE)
apply auto
apply (erule equalityE)
apply (erule subsetCE)
apply auto
done

lemma Part_eqI [intro]: " a  A; a=h(b)   a  Part A h"
by (auto simp add: Part_def)

lemmas PartI = Part_eqI [OF _ refl]

lemma PartE [elim!]: " a  Part A h;  !!z.  a  A;  a=h(z)   P   P"
by (auto simp add: Part_def)

lemma Part_subset: "Part A h  A"
by (auto simp add: Part_def)

lemma Part_mono: "A  B  Part A h  Part B h"
by blast

lemmas basic_monos = basic_monos Part_mono

lemma PartD1: "a  Part A h  a  A"
by (simp add: Part_def)

lemma Part_id: "Part A (λ x. x) = A"
by blast

lemma Part_Int: "Part (A  B) h = (Part A h)  (Part B h)"
by blast

lemma Part_Collect: "Part (A  {x. P x}) h = (Part A h)  {x. P x}"
by blast

subsubsection ‹Set operators›

lemma subset_lemma:
  " A  B = {}; A  B   A = {}"
by auto

lemma subset_lemma2:
 " B  A = {}; C  A   C  B = {}"
by auto

lemma insert_inter:
  " a  A; (A  B) = {}   (A  (insert a B)) = {}"
by auto

lemma insert_notmem:
  " a  b; a  B   a  (insert b B)"
by auto

lemma insert_union:
 "A  (insert a B) = insert a A  B"
by auto

lemma insert_or:
     "{s. s = t1   (P s)} = insert t1 {s. P s }"
by auto

lemma Collect_subset: 
  "{x . x  A  P x} = {x  Pow A. P x}"
by auto

lemma OneElement_Card [simp]:
  " finite M; card M <= Suc 0; t  M   M = {t}"
apply auto
apply (rename_tac s)
apply (rule_tac P="finite M" in mp)
apply (rule_tac P="card M <= Suc 0" in mp)
apply (rule_tac P="t  M" in mp)
apply (rule_tac F="M" in finite_induct)
apply auto
apply (rule_tac P="finite M" in mp)
apply (rule_tac P="card M <= Suc 0" in mp)
apply (rule_tac P="s  M" in mp)
apply (rule_tac P="t  M" in mp)
apply (rule_tac F="M" in finite_induct)
apply auto
done 
  
subsubsection ‹One point rule›

lemma Ex1_one_point [simp]: 
  "(∃! x. P x  x = a) = P a"
by auto

lemma Ex1_one_point2 [simp]:
  "(∃! x. P x  Q x  x = a) = (P a  Q a)"
by auto

lemma Some_one_point [simp]:
 "P a  (SOME x. P x  x = a) = a"
by auto

lemma Some_one_point2 [simp]:
 " Q a; P a   (SOME x. P x  Q x  x = a) = a"
by auto

end

Theory DataSpace

(*  Title:      statecharts/DataSpace/DataSpace.thy

    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Partitoned Data Spaces for Statecharts›
theory DataSpace
imports Contrib
begin

subsection ‹Definitions›

definition
  DataSpace :: "('d set) list
                => bool" where
  "DataSpace L = ((distinct L)  
                  ( D1(set L).  D2(set L).
                             D1  D2  ((D1  D2) = {})) 
                  (( (set L)) = UNIV))"

lemma DataSpace_EmptySet:
 "[UNIV]  { L | L. DataSpace L }"
by (unfold DataSpace_def, auto)

definition "dataspace = { L | (L::('d set) list). DataSpace L}"

typedef 'd dataspace = "dataspace :: 'd set list set"
  unfolding dataspace_def
  apply (rule exI)
  apply (rule DataSpace_EmptySet)
  done

definition
 PartNum :: "('d)dataspace => nat" where
 "PartNum = length o Rep_dataspace"

definition
 PartDom :: "['d dataspace, nat] => ('d set)" (infixl "!D!" 101) where
 "PartDom d n = (Rep_dataspace d) ! n" 

subsection ‹Lemmas›

subsubsection DataSpace›

lemma DataSpace_UNIV [simp]:
 "DataSpace [UNIV]"
by (unfold DataSpace_def, auto)

lemma DataSpace_select: 
 "DataSpace (Rep_dataspace L)"
apply (cut_tac x=L in  Rep_dataspace) 
apply (unfold dataspace_def)
apply auto
done

lemma UNIV_dataspace [simp]: 
  "[UNIV]  dataspace"
by (unfold dataspace_def, auto)

lemma Inl_Inr_DataSpace [simp]:
  "DataSpace [Part UNIV Inl, Part UNIV Inr]"
apply (unfold DataSpace_def)
apply auto
apply (rename_tac d)
apply (rule_tac b="(inv Inl) d" in Part_eqI)
apply auto
apply (rule sym)
apply (case_tac d)
apply auto
done

lemma Inl_Inr_dataspace [simp]:
  "[Part UNIV Inl, Part UNIV Inr]  dataspace"
by (unfold dataspace_def, auto)

lemma InlInr_InlInl_Inr_DataSpace [simp]:
  "DataSpace [Part UNIV (Inl o Inr), Part UNIV (Inl o Inl), Part UNIV Inr]"
apply (unfold DataSpace_def)
apply auto
apply (unfold Part_def)
apply auto
apply (rename_tac x)
apply (case_tac x)
apply auto
apply (rename_tac a)
apply (case_tac a)
apply auto
done

lemma InlInr_InlInl_Inr_dataspace [simp]:
  "[Part UNIV (Inl o Inr), Part UNIV (Inl o Inl), Part UNIV Inr] : dataspace"
by (unfold dataspace_def, auto)

subsubsection PartNum›

lemma PartDom_PartNum_distinct: 
      " i < PartNum d; j < PartNum d;        
         i  j; p   (d !D! i)  
         p  (d !D! j)"
apply auto
apply (cut_tac L=d in DataSpace_select)
apply (unfold DataSpace_def) 
apply auto
apply (erule_tac x="Rep_dataspace d ! i" in ballE)
apply (erule_tac x="Rep_dataspace d ! j" in ballE)
apply auto
apply (simp add:distinct_conv_nth PartNum_def)
apply (unfold PartDom_def PartNum_def)
apply auto
done

lemma PartDom_PartNum_distinct2: 
      " i < PartNum d; j < PartNum d;       
         i  j; p   (d !D! j)  
        p  (d !D! i)"
apply auto
apply (cut_tac L=d in DataSpace_select)
apply (unfold DataSpace_def) 
apply auto
apply (erule_tac x="Rep_dataspace d ! i" in ballE)
apply (erule_tac x="Rep_dataspace d ! j" in ballE)
apply auto
apply (simp add:distinct_conv_nth PartNum_def)
apply (unfold PartDom_def PartNum_def)
apply auto
done

lemma PartNum_length [simp]: 
  "(DataSpace L)  (PartNum (Abs_dataspace L) = (length L))"
apply (unfold PartNum_def)
apply auto
apply (subst Abs_dataspace_inverse)
apply (unfold dataspace_def)
apply auto
done

end

Theory Data

(*  Title:      statecharts/DataSpace/Data.thy

    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Data Space Assignments›
theory Data
imports DataSpace
begin

subsection ‹Total data space assignments›

definition
  Data :: "['d list, 'd dataspace]
                => bool" where
  "Data L D = (((length L) = (PartNum D)) 
               ( i  {n. n < (PartNum D)}. (L!i)  (PartDom D i)))"

lemma Data_EmptySet: 
    "([@ t. True], Abs_dataspace [UNIV]) { (L,D) | L D. Data L D }"
apply (unfold Data_def PartDom_def)
apply auto
apply (subst Abs_dataspace_inverse)
apply auto
done

definition
  "data =
    { (L,D) |
             (L::('d list))
             (D::('d dataspace)).
              Data L D }"

typedef 'd data = "data :: ('d list * 'd dataspace) set"
  unfolding data_def
  apply (rule exI)
  apply (rule Data_EmptySet)
  done

definition
 DataValue :: "('d data) => ('d list)" where
 "DataValue = fst o Rep_data"

definition
 DataSpace :: "('d data) => ('d dataspace)" where
 "DataSpace = snd o Rep_data"

definition
 DataPart :: "['d data, nat] => 'd" ("(_ !P!/ _)" [10,11]10) where
 "DataPart d n = (DataValue d) ! n"

lemma Rep_data_tuple:
  "Rep_data D = (DataValue D, DataSpace D)"
by (unfold DataValue_def DataSpace_def, simp)

lemma Rep_data_select: 
  "(DataValue D, DataSpace D)  data"
apply (subst Rep_data_tuple [THEN sym])
apply (rule Rep_data)
done

lemma Data_select:
  "Data (DataValue D) (DataSpace D)"
apply (cut_tac D=D in Rep_data_select)
apply (unfold data_def)
apply auto
done

lemma length_DataValue_PartNum [simp]: 
  "length (DataValue D) = PartNum (Data.DataSpace D)"
apply (cut_tac D=D in Data_select)
apply (unfold Data_def)
apply auto
done

lemma DataValue_PartDom [simp]:
  "i < PartNum (Data.DataSpace D) 
   DataValue D ! i  PartDom (Data.DataSpace D) i"
apply (cut_tac D=D in Data_select)
apply (unfold Data_def)
apply auto
done 

lemma DataPart_PartDom [simp]:
  "i < PartNum (Data.DataSpace d)  (d !P! i)  ((Data.DataSpace d) !D! i)"
apply (unfold DataPart_def)
apply auto
done

subsection ‹Partial data space assignments›

definition
  PData :: "['d option list, 'd dataspace] => bool" where
  "PData L D == ((length L) = (PartNum D))  
                ( i  {n. n < (PartNum D)}.
                    (L!i)  None  the (L!i)  (PartDom D i))"

lemma PData_EmptySet:
    "([Some (@ t. True)], Abs_dataspace [UNIV])  { (L,D) | L D. PData L D }"
apply (unfold PData_def PartDom_def)
apply auto
apply (subst Abs_dataspace_inverse)
apply auto
done

definition
  "pdata =
    { (L,D) |
             (L::('d option list))
             (D::('d dataspace)).
              PData L D }"

typedef 'd pdata = "pdata :: ('d option list * 'd dataspace) set"
  unfolding pdata_def
  apply (rule exI)
  apply (rule PData_EmptySet)
  done

definition
  PDataValue :: "('d pdata) => ('d option list)" where
 "PDataValue = fst o Rep_pdata"

definition
  PDataSpace :: "('d pdata) => ('d dataspace)" where
 "PDataSpace = snd o Rep_pdata"

definition
  Data2PData :: "('d data) => ('d pdata)" where
 "Data2PData D = (let
                      (L,DP) = Rep_data D;
                      OL     = map Some L
                  in
                      Abs_pdata (OL,DP))"

definition
  PData2Data :: "('d pdata) => ('d data)" where
 "PData2Data D = (let
                      (OL,DP) = Rep_pdata D;
                       L      = map the OL
                  in
                      Abs_data (L,DP))"

definition
  DefaultPData :: "('d dataspace) => ('d pdata)" where
 "DefaultPData D = Abs_pdata (replicate (PartNum D) None, D)"

definition
  OptionOverride :: "('d option * 'd) => 'd" where
 "OptionOverride P = (if (fst P) = None then (snd P) else (the (fst P)))"

definition
  DataOverride :: "['d pdata, 'd data] => 'd data" ("(_ [D+]/ _)" [10,11]10) where
 "DataOverride D1 D2 =
                (let
                    (L1,DP1) = Rep_pdata D1;
                    (L2,DP2) = Rep_data D2;
                    L        = map OptionOverride (zip L1 L2)
                 in
                    Abs_data (L,DP2))"

lemma Rep_pdata_tuple:
  "Rep_pdata D = (PDataValue D, PDataSpace D)"
apply (unfold PDataValue_def PDataSpace_def)
apply (simp)
done

lemma Rep_pdata_select:
  "(PDataValue D, PDataSpace D)  pdata"
apply (subst Rep_pdata_tuple [THEN sym])
apply (rule Rep_pdata)
done

lemma PData_select: 
  "PData (PDataValue D) (PDataSpace D)"
apply (cut_tac D=D in Rep_pdata_select)
apply (unfold pdata_def)
apply auto
done

subsubsection DefaultPData›

lemma PData_DefaultPData [simp]:
   "PData (replicate (PartNum D) None) D"
apply (unfold PData_def)
apply auto
done

lemma pdata_DefaultPData [simp]:
   "(replicate (PartNum D) None, D)  pdata "
apply (unfold pdata_def)
apply auto
done

lemma PDataSpace_DefaultPData [simp]:
   "PDataSpace (DefaultPData D) = D"
apply (unfold DataSpace_def PDataSpace_def DefaultPData_def)
apply auto
apply (subst Abs_pdata_inverse)
apply auto
done

lemma length_PartNum_PData [simp]:
  "length (PDataValue P) = PartNum (PDataSpace P)"
apply (cut_tac D=P in Rep_pdata_select)
apply (unfold pdata_def PData_def)
apply auto
done

subsubsection Data2PData›

lemma PData_Data2PData [simp]:
  "PData (map Some (DataValue D)) (Data.DataSpace D)"
apply (unfold PData_def)
apply auto
done

lemma pdata_Data2PData [simp]:
  "(map Some (DataValue D), Data.DataSpace D)  pdata"
apply (unfold pdata_def)
apply auto
done

lemma DataSpace_Data2PData [simp]:
  "(PDataSpace (Data2PData D)) = (Data.DataSpace D)"
apply (unfold DataSpace_def PDataSpace_def Data2PData_def Let_def)
apply auto
apply (cut_tac D=D in Rep_data_tuple)
apply auto
apply (subst Abs_pdata_inverse)
apply auto
done

lemma PDataValue_Data2PData_DataValue [simp]:
     "(map the (PDataValue (Data2PData D))) = DataValue D"
apply (unfold DataValue_def PDataValue_def Data2PData_def Let_def)
apply auto
apply (cut_tac D=D in Rep_data_tuple)
apply auto
apply (subst Abs_pdata_inverse)
apply simp
apply (simp del: map_map)
done

lemma DataSpace_PData2Data:  
   "Data (map the (PDataValue D)) (PDataSpace D) 
   (Data.DataSpace (PData2Data D) = (PDataSpace D))"
apply (unfold DataSpace_def PDataSpace_def PData2Data_def Let_def)
apply auto
apply (cut_tac D=D in Rep_pdata_tuple)
apply auto
apply (subst Abs_data_inverse)
apply (unfold data_def)
apply auto
done

lemma PartNum_PDataValue_PartDom [simp]:
   " i < PartNum (PDataSpace Q);
      PDataValue Q ! i = Some y  
      y  PartDom (PDataSpace Q) i"
apply (cut_tac D=Q in Rep_pdata_select)
apply (unfold pdata_def PData_def)
apply auto
done

subsubsection DataOverride›

lemma Data_DataOverride:
 "((PDataSpace P) = (Data.DataSpace Q)) 
  Data (map OptionOverride (zip (PDataValue P) (Data.DataValue Q))) (Data.DataSpace Q)"
apply (unfold Data_def)
apply auto
apply (unfold OptionOverride_def)
apply auto
apply (rename_tac i D)
apply (case_tac "PDataValue P ! i = None")
apply auto
apply (drule sym)
apply auto
done

lemma data_DataOverride:
 "((PDataSpace P) = (Data.DataSpace Q)) 
   (map OptionOverride (zip (PDataValue P) (Data.DataValue Q)), Data.DataSpace Q)  data"
apply (unfold data_def)
apply auto
apply (rule Data_DataOverride)
apply fast
done

lemma DataSpace_DataOverride [simp]:
 "((Data.DataSpace D) = (PDataSpace E)) 
   Data.DataSpace (E [D+] D) = (Data.DataSpace D)"
apply (unfold DataSpace_def DataOverride_def Let_def)
apply auto
apply (cut_tac D=D in Rep_data_tuple)
apply (cut_tac D=E in Rep_pdata_tuple)
apply auto
apply (subst Abs_data_inverse)
apply auto
apply (drule sym)
apply simp
apply (rule data_DataOverride)
apply auto
done

lemma DataValue_DataOverride [simp]:
 "((PDataSpace P) = (Data.DataSpace Q)) 
  (DataValue (P [D+] Q)) = (map OptionOverride (zip (PDataValue P) (Data.DataValue Q)))"
apply (unfold DataValue_def DataOverride_def Let_def)
apply auto
apply (cut_tac D=P in Rep_pdata_tuple)
apply (cut_tac D=Q in Rep_data_tuple)
apply auto
apply (subst Abs_data_inverse)
apply auto
apply (rule data_DataOverride)
apply auto
done

subsubsection OptionOverride›

lemma DataValue_OptionOverride_nth:
 " ((PDataSpace P) = (DataSpace Q));
    i < PartNum (DataSpace Q)  
    (DataValue (P [D+] Q) ! i) = 
    OptionOverride (PDataValue P ! i, DataValue Q ! i)"
apply auto
done

lemma None_OptionOverride [simp]:
   "(fst P) = None  OptionOverride P = (snd P)"
apply (unfold OptionOverride_def)
apply auto
done

lemma Some_OptionOverride [simp]:
   "(fst P)  None  OptionOverride P = the (fst P)"
apply (unfold OptionOverride_def)
apply auto
done

end

Theory Update

(*  Title:      statecharts/DataSpace/Update.thy

    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Update-Functions on Data Spaces›
theory Update
imports Data
begin

subsection ‹Total update-functions›

definition
  Update :: "(('d data) => ('d data)) => bool" where 
  "Update U = ( d. Data.DataSpace d = DataSpace (U d))"

lemma Update_EmptySet: 
 "(% d. d)  { L | L. Update L}" 
by (unfold Update_def, auto)

definition
  "update = { L | (L::(('d data) => ('d data))). Update L}"

typedef 'd update = "update :: ('d data => 'd data) set"
  unfolding update_def
  apply (rule exI)
  apply (rule Update_EmptySet)
  done
 
definition
 UpdateApply :: "['d update, 'd data] => 'd data" ("(_ !!!/ _)" [10,11]10) where
 "UpdateApply U D == Rep_update U D" 

definition
  DefaultUpdate :: "('d update)" where
 "DefaultUpdate ==  Abs_update (λ D. D)"

subsubsection ‹Basic lemmas›

lemma Update_select:
   "Update (Rep_update U)"
apply (cut_tac x=U in Rep_update)
apply (unfold update_def)
apply auto
done

lemma DataSpace_DataSpace_Update [simp]:
   "Data.DataSpace (Rep_update U DP) = Data.DataSpace DP"
apply (cut_tac U=U in Update_select)
apply (unfold Update_def)
apply auto
done

subsubsection DefaultUpdate›

lemma Update_DefaultUpdate [simp]:
   "Update (λ D. D)"
by (unfold Update_def, auto)

lemma update_DefaultUpdate [simp]:
   "(λ D. D)  update"
by (unfold update_def, auto)

lemma DataSpace_UpdateApply [simp]:
   "Data.DataSpace (U !!! D) = Data.DataSpace D"
by (unfold UpdateApply_def, auto)

subsection ‹Partial update-functions›

definition
  PUpdate :: "(('d data) => ('d pdata)) => bool" where
  "PUpdate U = ( d. Data.DataSpace d = PDataSpace (U d))"

lemma PUpdate_EmptySet:
 "(% d. Data2PData d)  { L | L. PUpdate L}" 
by (unfold PUpdate_def, auto)

definition "pupdate = { L | (L::(('d data) => ('d pdata))). PUpdate L}"

typedef 'd pupdate = "pupdate :: ('d data => 'd pdata) set" 
  unfolding pupdate_def
  apply (rule exI)
  apply (rule PUpdate_EmptySet)
  done
 
definition
 PUpdateApply :: "['d pupdate, 'd data] => 'd pdata" ("(_ !!/ _)" [10,11]10) where
 "PUpdateApply U D = Rep_pupdate U D" 

definition
  DefaultPUpdate :: "('d pupdate)" where
 "DefaultPUpdate = Abs_pupdate (λ D. DefaultPData (Data.DataSpace D))"
                      
subsubsection ‹Basic lemmas›

lemma PUpdate_select:
   "PUpdate (Rep_pupdate U)"
apply (cut_tac x=U in Rep_pupdate)
apply (unfold pupdate_def)
apply auto
done

lemma DataSpace_PDataSpace_PUpdate [simp]:
   "PDataSpace (Rep_pupdate U DP) = Data.DataSpace DP"
apply (cut_tac U=U in PUpdate_select)
apply (unfold PUpdate_def)
apply auto
done

subsubsection Data2PData›

lemma  PUpdate_Data2PData [simp]: 
   "PUpdate Data2PData"
by (unfold PUpdate_def, auto)

lemma pupdate_Data2PData  [simp]:
   "Data2PData  pupdate"
by (unfold pupdate_def, auto)

subsubsection PUpdate›

lemma PUpdate_DefaultPUpdate [simp]:
   "PUpdate (λ D. DefaultPData (Data.DataSpace D))"
apply (unfold PUpdate_def)
apply auto
done

lemma pupdate_DefaultPUpdate [simp]:
   "(λ D. DefaultPData (Data.DataSpace D))  pupdate"
apply (unfold pupdate_def)
apply auto
done

lemma DefaultPUpdate_None [simp]:
    "(DefaultPUpdate !! D) = DefaultPData (DataSpace D)"
apply (unfold DefaultPUpdate_def PUpdateApply_def)
apply (subst Abs_pupdate_inverse)
apply auto
done

subsubsection SequentialRacing›

definition
 UpdateOverride :: "['d pupdate, 'd update] => 
                     'd update" ("(_ [U+]/ _)" [10,11]10) where
 "UpdateOverride U P = Abs_update (λ DA . (U !! DA) [D+] (P !!! DA))"
 

(* -------------------------------------------------------------- *)
(* We use our own FoldSet operator simular to the definition      *)
(* of Isabelle 2002. Note, it is different to the definition      *)
(* in Isabelle 2009. Basically we express "f (g x)" by "h x"      *)
(* -------------------------------------------------------------- *)

inductive
  FoldSet :: "('b => 'a => 'a) => 'a => 'b set => 'a => bool"
  for h ::  "'b => 'a => 'a"
  and z :: 'a
where
  emptyI [intro]: "FoldSet h z {} z"
| insertI [intro]:
     " x  A; FoldSet h z A y 
       FoldSet h z (insert x A) (h x y)"

definition
SequentialRacing :: "('d pupdate set) => ('d update set)" where
 "SequentialRacing U = 
     {u. FoldSet UpdateOverride DefaultUpdate U u}"

lemma FoldSet_imp_finite:
  "FoldSet h z A x  finite A"
by (induct set: FoldSet) auto

lemma finite_imp_FoldSet:
  "finite A   x. FoldSet h z A x"
by (induct set: finite) auto

lemma finite_SequentialRacing:
   "finite US  (SOME u. u  SequentialRacing US)  SequentialRacing US"
apply (unfold SequentialRacing_def)
apply auto
apply (drule_tac h=UpdateOverride and z=DefaultUpdate in finite_imp_FoldSet)
apply auto
apply (rule someI)
apply auto
done


end

Theory Expr

(*  Title:      statecharts/SA/Expr.thy

    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Label Expressions›
theory Expr
imports Update
begin

datatype ('s,'e)expr = true
                        | In 's
                        | En 'e
                        | NOT "('s,'e)expr"
                        | And "('s,'e)expr" "('s,'e)expr"
                        | Or  "('s,'e)expr" "('s,'e)expr"
 
type_synonym 'd guard = "('d data) => bool"
type_synonym ('e,'d)action = "('e set * 'd pupdate)"
type_synonym ('s,'e,'d)label = "(('s,'e)expr * 'd guard * ('e,'d)action)"
type_synonym ('s,'e,'d)trans = "('s * ('s,'e,'d)label * 's)"

primrec
   eval_expr :: "[('s set * 'e set), ('s,'e)expr]  bool" where 
     "eval_expr sc true          = True"
   | "eval_expr sc (En ev)       = (ev  snd sc)"
   | "eval_expr sc (In st)       = (st  fst sc)"
   | "eval_expr sc (NOT e1)      = (¬ (eval_expr sc e1))"
   | "eval_expr sc (And e1 e2)   = ((eval_expr sc e1)  (eval_expr sc e2))"
   | "eval_expr sc (Or  e1 e2)   = ((eval_expr sc e1)  (eval_expr sc e2))"

primrec
   ExprEvents :: "('s,'e)expr  'e set" where
      "ExprEvents true        = {}"
   |  "ExprEvents (En ev)     = {ev}"
   |  "ExprEvents (In st)     = {}"
   |  "ExprEvents (NOT e)     = (ExprEvents e)"
   |  "ExprEvents (And e1 e2) = ((ExprEvents e1)  (ExprEvents e2))"
   |  "ExprEvents (Or  e1 e2) = ((ExprEvents e1)  (ExprEvents e2))"

(* atomar propositions for Sequential Automata, will be necessary for CTL-interpretation *)

datatype ('s, 'e, dead 'd)atomar =
                          TRUE
                          | FALSE
                          | IN 's
                          | EN 'e
                          | VAL "'d data => bool"

definition
  source     :: "('s,'e,'d)trans => 's" where
  "source t  = fst t"

definition
   Source     :: "('s,'e,'d)trans set => 's set" where
  "Source T == source ` T"

definition
   target     :: "('s,'e,'d)trans => 's" where
  "target t  = snd(snd t)"

definition
   Target     :: "('s,'e,'d)trans set => 's set" where
  "Target T = target ` T"

definition
   label      :: "('s,'e,'d)trans => ('s,'e,'d)label" where
  "label t  = fst (snd t)"

definition
   Label      :: "('s,'e,'d)trans set => ('s,'e,'d)label set" where
  "Label T = label ` T"

definition
   expr       :: "('s,'e,'d)label => ('s,'e)expr" where
  "expr  = fst"

definition
   action     :: "('s,'e,'d)label  => ('e,'d)action" where
  "action = snd o snd"

definition
   Action     :: "('s,'e,'d)label set => ('e,'d)action set" where
  "Action L = action ` L"

definition
   pupdate     :: "('s,'e,'d)label => 'd pupdate" where
  "pupdate   = snd o action"

definition
  PUpdate     :: "('s,'e,'d)label set => ('d pupdate) set" where
  "PUpdate L = pupdate ` L"

definition
   actevent   :: "('s,'e,'d)label => 'e set" where
  "actevent  = fst o action"

definition
   Actevent   :: "('s,'e,'d)label set => ('e set) set" where
  "Actevent L = actevent ` L"

definition
   guard      :: "('s,'e,'d)label  => 'd guard" where  
  "guard = fst o snd"

definition
   Guard      :: "('s,'e,'d)label set => ('d guard) set" where
  "Guard L = guard ` L"

definition
   defaultexpr :: "('s,'e)expr" where 
  "defaultexpr = true"

definition
   defaultaction :: "('e,'d)action" where
  "defaultaction = ({},DefaultPUpdate)"

definition
   defaultguard :: "('d guard)" where
  "defaultguard = (λ d. True)"

definition
   defaultlabel :: "('s,'e,'d)label" where
  "defaultlabel = (defaultexpr, defaultguard, defaultaction)"

definition
   eval :: "[('s set * 'e set * 'd data), ('s,'e,'d)label] => bool"
                                                       ("_ |= _" [91,90]90) where
  "eval scd l = (let (s,e,d) = scd
                 in
                    ((eval_expr (s,e) (expr l))  ((guard l) d)))"

lemma Source_EmptySet [simp]:
 "Source {} = {}"
by (unfold Source_def, auto)

lemma Target_EmptySet [simp]:
 "Target {} = {}"
by (unfold Target_def, auto)

lemma Label_EmptySet [simp]:
 "Label {} = {}"
by (unfold Label_def, auto)

lemma Action_EmptySet [simp]:
 "Action {} = {}"
by (unfold Action_def, auto)

lemma PUpdate_EmptySet [simp]:
 "PUpdate {} = {}"
by (unfold PUpdate_def, auto)

lemma Actevent_EmptySet [simp]:
 "Actevent {} = {}"
by (unfold Actevent_def, auto)

lemma Union_Actevent_subset:
  " m  M; (( (Actevent (Label (Union M))))  (N::'a set))  
   (( (Actevent (Label m)))  N)"
by (unfold Actevent_def Label_def, auto)

lemma action_select [simp]:
 "action (a,b,c) = c"
by (unfold action_def, auto)

lemma label_select [simp]:
 "label (a,b,c) = b"
by (unfold label_def, auto)

lemma target_select [simp]:
 "target (a,b,c) = c"
by (unfold target_def, auto)

lemma actevent_select [simp]:
 "actevent (a,b,(c,d)) = c"
by (unfold actevent_def, auto)

lemma pupdate_select [simp]:
 "pupdate (a,b,c,d) = d"
by (unfold pupdate_def, auto)

lemma source_select [simp]:
 "source (a,b) = a"
by (unfold source_def, auto)

lemma finite_PUpdate [simp]:
 "finite S  finite(PUpdate S)"
by (unfold PUpdate_def, auto)

lemma finite_Label [simp]:
 "finite S  finite(Label S)"
by (unfold Label_def, auto)

lemma fst_defaultaction [simp]:
 "fst defaultaction = {}" 
by (unfold defaultaction_def, auto)

lemma action_defaultlabel [simp]:
 "(action defaultlabel) = defaultaction" 
by (unfold defaultlabel_def action_def, auto)

lemma fst_defaultlabel [simp]:
 "(fst defaultlabel) = defaultexpr" 
by (unfold defaultlabel_def, auto)

lemma ExprEvents_defaultexpr [simp]:
 "(ExprEvents defaultexpr) = {}" 
by (unfold defaultexpr_def, auto)

lemma defaultlabel_defaultexpr [simp]:
 "expr defaultlabel = defaultexpr"
by (unfold defaultlabel_def expr_def, auto)

lemma target_Target [simp]:
  "t  T  target t  Target T"
by (unfold Target_def, auto)

lemma Source_union : "Source s  Source t = Source (s  t)"
apply (unfold Source_def)
apply auto
done

lemma Target_union : "Target s  Target t = Target (s  t)"
apply (unfold Target_def)
apply auto
done

end

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

Theory HA

(*  Title:      statecharts/HA/HA.thy

    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Syntax of Hierarchical Automata›
theory HA
imports SA
begin

subsection ‹Definitions›

(* unique root automaton *)

definition
  RootEx :: "[(('s,'e,'d)seqauto) set,
              's   ('s,'e,'d) seqauto set] => bool" where
  "RootEx F G = (∃! A. A  F  A   (ran G))"

definition
  Root :: "[(('s,'e,'d)seqauto) set,
            's  ('s,'e,'d) seqauto set]
           => ('s,'e,'d) seqauto" where
  "Root F G = (@ A. A  F   A   (ran G))"

(* mutually distinct state spaces *)

definition
  MutuallyDistinct :: "(('s,'e,'d)seqauto) set => bool" where
  "MutuallyDistinct F =
        ( a  F.  b  F. a  b  (States a)  (States b) = {})"

(* exactly one ancestor for every non root automaton *)

definition
 OneAncestor :: "[(('s,'e,'d)seqauto) set,
                   's  ('s,'e,'d) seqauto set] => bool" where
 "OneAncestor F G =
                ( A  F - {Root F G} .
                    ∃! s. s  ( A'  F - {A} . States A')  
                         A  the (G s))"

(* composition function contains no cycles *)

definition
  NoCycles :: "[(('s,'e,'d)seqauto) set,
                   's  ('s,'e,'d) seqauto set] => bool" where
  "NoCycles F G =
       ( S  Pow ( A  F. States A).
           S  {}   ( s  S. S  ( A  the (G s). States A) = {}))"
 
(* properties of composition functions *)

definition
  IsCompFun :: "[(('s,'e,'d)seqauto) set,
                    's  ('s,'e,'d) seqauto set] => bool" where
  "IsCompFun F G = ((dom G = ( A  F. States A))  
                    ( (ran G) = (F - {Root F G}))  
                    (RootEx F G)  
                    (OneAncestor F G)  
                    (NoCycles F G))"

subsubsection ‹Well-formedness for the syntax of HA›

definition
  HierAuto :: "['d data,
                 (('s,'e,'d)seqauto) set,
                'e set,
                's  (('s,'e,'d)seqauto) set]
                => bool" where
  "HierAuto D F E G = (( A  F. SAEvents A)  E  
                       MutuallyDistinct F  
                       finite F  
                       IsCompFun F G)"

lemma HierAuto_EmptySet:
 "((@x. True),{Abs_seqauto ({@x. True}, (@x. True), {}, {})}, {}, 
  Map.empty ( @x. True  {}))  {(D,F,E,G) | D F E G. HierAuto D F E G}"
apply (unfold HierAuto_def IsCompFun_def Root_def RootEx_def MutuallyDistinct_def
           OneAncestor_def NoCycles_def)
apply auto
done

definition
  "hierauto =
    {(D,F,E,G) |
        (D::'d data)
        (F::(('s,'e,'d) seqauto) set)
        (E::('e set))
        (G::('s  (('s,'e,'d) seqauto) set)).
                                HierAuto D F E G}"

typedef ('s,'e,'d) hierauto =
    "hierauto :: ('d data * ('s,'e,'d) seqauto set * 'e set * ('s  ('s,'e,'d) seqauto set)) set"
  unfolding hierauto_def
  apply (rule exI)
  apply (rule HierAuto_EmptySet)
  done

definition
  SAs :: "(('s,'e,'d) hierauto)  => (('s,'e,'d) seqauto) set" where
  "SAs = fst o snd o Rep_hierauto"

definition
  HAEvents :: "(('s,'e,'d) hierauto) => ('e set)" where
  "HAEvents = fst o snd o snd o Rep_hierauto"

definition
  CompFun :: "(('s,'e,'d) hierauto) => ('s  ('s,'e,'d) seqauto set)" where
  "CompFun = (snd o snd o snd o Rep_hierauto)"

definition
  HAStates :: "(('s,'e,'d) hierauto) => ('s set)" where
  "HAStates HA = (  A  (SAs HA). States A)"

definition
  HADelta :: "(('s,'e,'d) hierauto) => (('s,'e,'d)trans)set" where
  "HADelta HA = ( F  (SAs HA). Delta F)"

definition
  HAInitValue :: "(('s,'e,'d) hierauto) => 'd data" where
  "HAInitValue == fst o Rep_hierauto"

definition
  HAInitStates :: "(('s,'e,'d) hierauto) => 's set" where
  "HAInitStates HA ==  A  (SAs HA). { InitState A }"

definition
  HARoot :: "(('s,'e,'d) hierauto) => ('s,'e,'d)seqauto" where
  "HARoot HA == Root (SAs HA) (CompFun HA)"

definition
  HAInitState :: "(('s,'e,'d) hierauto) => 's" where
  "HAInitState HA == InitState (HARoot HA)"

subsubsection ‹State successor function›

(* state successor function Chi *)
  
definition
  Chi   :: "('s,'e,'d)hierauto => 's => 's set" where
  "Chi A ==  (λ  S   (HAStates A) .
                 {S'.  SA  (SAs A) . SA  the ((CompFun A) S)  S'  States SA })"

(* direct state successor relation ChiRel *)

definition
  ChiRel :: "('s,'e,'d)hierauto => ('s *'s) set" where
  "ChiRel A == { (S,S'). S  HAStates A  S'  HAStates A  S'  (Chi A) S }"

(* indirect state successor relation ChiPlus *)

definition
  ChiPlus :: "('s,'e,'d)hierauto => ('s *'s) set" where
  "ChiPlus A == (ChiRel A) ^+"

definition
  ChiStar :: "('s,'e,'d)hierauto => ('s *'s) set" where
  "ChiStar A == (ChiRel A) ^*"

(* priority on transitions that are successors *)

definition
  HigherPriority :: "[('s,'e,'d)hierauto,
                      ('s,'e,'d)trans * ('s,'e,'d)trans] => bool" where
  "HigherPriority A ==
             λ (t,t')  (HADelta A) × (HADelta A).
                          (source t',source t)   ChiPlus A"

subsubsection ‹Configurations›

(* initial configuration *)

definition
  InitConf :: "('s,'e,'d)hierauto => 's set" where
  "InitConf A == (((((HAInitStates A) × (HAInitStates A))  (ChiRel A))^* )
                     `` {HAInitState A})"

(*  -------------------------------------------------------------- *)
(*  First, the original definition calculating a step on           *)
(*  configurations given by                                        *)
(*                                                                 *)
(*  E. Mikk, Y. Lakhnech, and M. Siegel. Hierarchical automata as  *)
(*  model for statecharts. In Asian Computing Science Conference   *)
(*  (ASIAN~97), Springer LNCS, 1345, 1997.                         *)
(*                                                                
    "StepConf A C TS ==                                           
       (C - ((ChiStar A) `` (Source TS))) ∪                       
        (Target TS) ∪ (((ChiPlus A) `` (Target TS)) 
                    ∩ (HAInitStates A))"           
                                                                   *)
(*                                                                 *)
(* Note, that this semantic definition not preserves the           *)
(* well-formedness of a Statecharts. Hence we use our definition.  *)
(*  -------------------------------------------------------------- *)

(* step on configurations *)

definition
  StepConf  :: "[('s,'e,'d)hierauto, 's set,
                 ('s,'e,'d)trans set] => 's set" where

  "StepConf A C TS ==
               (C - ((ChiStar A) `` (Source TS)))  
               (Target TS) 
               ((ChiRel A) `` (Target TS))  (HAInitStates A) 
               ((((ChiRel A)  ((HAInitStates A) × (HAInitStates A)))+) 
                   `` (((ChiRel A)`` (Target TS))  (HAInitStates A)))"

subsection ‹Lemmas›

lemma Rep_hierauto_tuple:
"Rep_hierauto HA = (HAInitValue HA, SAs HA, HAEvents HA, CompFun HA)"
by (unfold SAs_def HAEvents_def CompFun_def HAInitValue_def, simp)

lemma Rep_hierauto_select: 
  "(HAInitValue HA, SAs HA, HAEvents HA, CompFun HA): hierauto"
by (rule Rep_hierauto_tuple [THEN subst], rule Rep_hierauto)

lemma HierAuto_select [simp]: 
  "HierAuto (HAInitValue HA) (SAs HA) (HAEvents HA) (CompFun HA)"
by (cut_tac Rep_hierauto_select, unfold hierauto_def, simp)

subsubsection HAStates›

lemma finite_HAStates [simp]:
  "finite (HAStates HA)"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def)
apply auto
apply (simp add: HAStates_def)
apply (rule finite_UN_I)
apply fast
apply (rule finite_States)
done

lemma HAStates_SA_mem:
 " SA  SAs A; S  States SA   S  HAStates A"
by (unfold HAStates_def, auto)

lemma ChiRel_HAStates [simp]:
 "(a,b)  ChiRel A  a  HAStates A"
apply (unfold ChiRel_def)
apply auto
done

lemma ChiRel_HAStates2 [simp]:
 "(a,b)   ChiRel A  b  HAStates A"
apply (unfold ChiRel_def)
apply auto
done

subsubsection HAEvents›

lemma HAEvents_SAEvents_SAs:
  "(SAEvents ` (SAs HA))  HAEvents HA"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def)
apply fast
done

subsubsection NoCycles›

lemma NoCycles_EmptySet [simp]:
  "NoCycles {} S"
by (unfold NoCycles_def, auto)

lemma NoCycles_HA [simp]: 
  "NoCycles (SAs HA) (CompFun HA)"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def IsCompFun_def)
apply auto
done

subsubsection OneAncestor›

lemma OneAncestor_HA [simp]:
  "OneAncestor (SAs HA) (CompFun HA)"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def IsCompFun_def)
apply auto
done

subsubsection MutuallyDistinct›

lemma MutuallyDistinct_Single [simp]:
  "MutuallyDistinct {SA}"
by (unfold MutuallyDistinct_def, auto)

lemma MutuallyDistinct_EmptySet [simp]:
  "MutuallyDistinct {}"
by (unfold MutuallyDistinct_def, auto)

lemma MutuallyDistinct_Insert:
  " MutuallyDistinct S; (States A)   ( B  S. States B) = {} 
   MutuallyDistinct (insert A S)"
by (unfold MutuallyDistinct_def, safe, fast+)

lemma MutuallyDistinct_Union:
  " MutuallyDistinct A; MutuallyDistinct B;
  ( C  A. States C)  ( C  B. States C) = {} 
   MutuallyDistinct (A  B)"
by (unfold MutuallyDistinct_def, safe, blast+)

lemma MutuallyDistinct_HA [simp]:
  "MutuallyDistinct (SAs HA)"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def IsCompFun_def)
apply auto
done

subsubsection RootEx›

lemma RootEx_Root [simp]:
  "RootEx F G  Root F G  F"
apply (unfold RootEx_def Root_def)
apply (erule ex1E)
apply (erule conjE)
apply (rule someI2)
apply blast+
done

lemma RootEx_Root_ran [simp]:
  "RootEx F G  Root F G   (ran G)"
apply (unfold RootEx_def Root_def)
apply (erule ex1E)
apply (erule conjE)
apply (rule someI2)
apply blast+
done

lemma RootEx_States_Subset [simp]:
  "(RootEx F G)  States (Root F G)  ( x  F . States x)"
apply (unfold RootEx_def Root_def)
apply (erule ex1E)
apply (erule conjE)
apply (rule someI2)
apply fast
apply (unfold UNION_eq)
apply (simp add: subset_eq)
apply auto
done

lemma RootEx_States_notdisjunct [simp]:
  "RootEx F G  States (Root F G)  ( x  F . States x)  {}"
apply (frule RootEx_States_Subset)
apply (case_tac "States (Root F G)={}")
prefer 2
apply fast
apply simp
done

lemma Root_neq_SA [simp]:
  " RootEx F G; ( x  F . States x)  States SA = {}   Root F G  SA"
apply (rule  SA_States_disjunct)
apply (frule RootEx_States_Subset)
apply fast
done

lemma RootEx_HA [simp]:
  "RootEx (SAs HA) (CompFun HA)"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def IsCompFun_def)
apply fast
done

subsubsection HARoot›

lemma HARoot_SAs [simp]:  
  "(HARoot HA)  SAs HA"
apply (unfold HARoot_def)
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def)
apply auto
done

lemma States_HARoot_HAStates:
  "States (HARoot HA)   HAStates HA"
apply (unfold HAStates_def)
apply auto
apply (rule_tac x="HARoot HA" in bexI)
apply auto
done

lemma SAEvents_HARoot_HAEvents:
  "SAEvents (HARoot HA)  HAEvents HA"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def)
apply auto
apply (rename_tac S)
apply (unfold UNION_eq)
apply (simp add: subset_eq)
apply (erule_tac x=S in allE)
apply auto
done

lemma HARoot_ran_CompFun:
  "HARoot HA  Union (ran (CompFun HA))"
apply (unfold HARoot_def)
apply (cut_tac Rep_hierauto_select)
apply (unfold IsCompFun_def hierauto_def HierAuto_def)
apply fast
done

lemma HARoot_ran_CompFun2:
  "S  ran (CompFun HA)  HARoot HA  S"
apply (unfold HARoot_def)
apply (cut_tac Rep_hierauto_select)
apply (unfold IsCompFun_def hierauto_def HierAuto_def)
apply fast
done

subsubsection CompFun›

lemma IsCompFun_HA [simp]:
  "IsCompFun (SAs HA) (CompFun HA)"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def)
apply auto
done

lemma dom_CompFun [simp]:
  "dom (CompFun HA) = HAStates HA"
apply (cut_tac HA=HA in IsCompFun_HA)
apply (unfold IsCompFun_def HAStates_def)
apply auto
done

lemma ran_CompFun [simp]:
  "Union (ran (CompFun HA)) = ((SAs HA) - {Root  (SAs HA)(CompFun HA)})"
apply (cut_tac HA=HA in IsCompFun_HA)
apply (unfold IsCompFun_def)
apply fast
done

lemma ran_CompFun_subseteq:
  "Union (ran (CompFun HA))  (SAs HA)"
apply (cut_tac HA=HA in IsCompFun_HA)
apply (unfold IsCompFun_def)
apply fast
done

lemma ran_CompFun_is_not_SA:
  "¬ Sas  (SAs HA)  Sas  (ran (CompFun HA))"
apply (cut_tac HA=HA in IsCompFun_HA)
apply (unfold IsCompFun_def)
apply fast
done

lemma HAStates_HARoot_CompFun [simp]:
  "S  HAStates HA  HARoot HA  the (CompFun HA S)"
apply (rule ran_dom_the)
back
apply (simp add: HARoot_ran_CompFun2 HARoot_def HAStates_def)+
done

lemma HAStates_CompFun_SAs:
 "S  HAStates A  the (CompFun A S)  SAs A"
apply auto
apply (rename_tac T)
apply (cut_tac HA=A in ran_CompFun)
apply (erule equalityE)
apply (erule_tac c=T in subsetCE)
apply (drule ran_dom_the)
apply auto
done

lemma HAStates_CompFun_notmem [simp]:
  " S  HAStates A; SA  the (CompFun A S)   S  States SA"
apply (unfold HAStates_def)
apply auto
apply (rename_tac T)
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x=SA in ballE)
apply (erule_tac x=T in ballE)
apply auto
prefer 2
apply (cut_tac A=A and S=S in  HAStates_CompFun_SAs)
apply (unfold HAStates_def)
apply simp
apply fast
apply fast
apply (cut_tac HA=A in NoCycles_HA)
apply (unfold NoCycles_def)
apply (erule_tac x="{S}" in ballE)
apply auto
done

lemma CompFun_Int_disjoint: 
  " S  T; S   HAStates A; T   HAStates A   the (CompFun A T)  the (CompFun A S) = {}" 
apply auto
apply (rename_tac U)
apply (cut_tac HA=A in OneAncestor_HA)
apply (unfold OneAncestor_def)
apply (erule_tac x=U in ballE)
prefer 2
apply simp
apply (fold HARoot_def)
apply (frule HAStates_HARoot_CompFun)
apply simp
apply (frule HAStates_CompFun_SAs)
apply auto
apply (erule_tac x=S in allE)
apply (erule_tac x=T in allE)
apply auto
apply (cut_tac HA=A in NoCycles_HA)
apply (unfold NoCycles_def)
apply (simp only: HAStates_def)
apply safe
apply (erule_tac x="{S}" in ballE)
apply simp
apply fast
apply simp
apply (cut_tac HA=A in NoCycles_HA)
apply (unfold NoCycles_def)
apply (simp only: HAStates_def)
apply safe
apply (erule_tac x="{T}" in ballE)
apply simp
apply fast
apply simp
done

subsubsection SAs›

lemma finite_SAs [simp]:
  "finite (SAs HA)"
apply (cut_tac Rep_hierauto_select)
apply (unfold hierauto_def HierAuto_def)
apply fast
done

lemma HAStates_SAs_disjunct:
  "HAStates HA1  HAStates HA2 = {}  SAs HA1  SAs HA2 = {}"
apply (unfold UNION_eq HAStates_def Int_def)
apply auto
apply (rename_tac SA)
apply (cut_tac SA=SA in EX_State_SA)
apply (erule exE)
apply auto
done

lemma HAStates_CompFun_SAs_mem [simp]:
 " S  HAStates A; T  the (CompFun A S)   T  SAs A" 
apply (cut_tac A=A and S=S in HAStates_CompFun_SAs)
apply auto
done 

lemma SAs_States_HAStates:
 "SA  SAs A  States SA  HAStates A"
by (unfold HAStates_def, auto)

subsubsection HAInitState›

lemma HAInitState_HARoot [simp]:
  "HAInitState A  States (HARoot A)"
by (unfold HAInitState_def, auto)

lemma HAInitState_HARoot2 [simp]:
  "HAInitState A  States (Root (SAs A) (CompFun A))"
by (fold HARoot_def, simp)

lemma HAInitStates_HAStates [simp]:
  "HAInitStates A  HAStates A"
apply (unfold HAInitStates_def HAStates_def)
apply auto
done

lemma HAInitStates_HAStates2 [simp]:
  "S  HAInitStates A  S  HAStates A"
apply (cut_tac A=A in HAInitStates_HAStates)
apply fast
done

lemma HAInitState_HAStates [simp]:
  "HAInitState A  HAStates A"
apply (unfold HAStates_def)
apply auto
apply (rule_tac x="HARoot A" in bexI)
apply auto
done

lemma HAInitState_HAInitStates [simp]:
  "HAInitState A  HAInitStates A"
by (unfold HAInitStates_def HAInitState_def, auto)


lemma CompFun_HAInitStates_HAStates [simp]:
 " S  HAStates A; SA  the (CompFun A S)   (InitState SA)  HAInitStates A"
apply (unfold HAInitStates_def)
apply auto
done

lemma CompFun_HAInitState_HAInitStates [simp]:
 " SA  the (CompFun A (HAInitState A))   (InitState SA)  HAInitStates A"
apply (unfold HAInitStates_def)
apply auto
apply (rule_tac x=SA in bexI)
apply auto
apply (cut_tac A=A and S="HAInitState A" in HAStates_CompFun_SAs)
apply auto
done

lemma HAInitState_notmem_States [simp]: 
  " S  HAStates A; SA  the (CompFun A S)   HAInitState A  States SA"
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x=SA in ballE)
apply (erule_tac x="HARoot A" in ballE)
apply auto
done

lemma InitState_notmem_States [simp]: 
  " S  HAStates A; SA  the (CompFun A S); 
     T  HAInitStates A; T  InitState SA  
      T  States SA"
apply (unfold HAInitStates_def)
apply auto
apply (rename_tac SAA)
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x=SA in ballE)
apply (erule_tac x=SAA in ballE)
apply auto
done

lemma InitState_States_notmem [simp]:
    " B  SAs A; C  SAs A; B  C   InitState B  States C"
apply auto
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply force
done

lemma OneHAInitState_SAStates:
   " S  HAInitStates A; T  HAInitStates A;
      S  States SA; T  States SA; SA  SAs A   
      S = T" 
apply (unfold HAInitStates_def)
apply auto
apply (rename_tac AA AAA)
apply (case_tac "AA = SA")
apply auto
apply (case_tac "AAA = SA")
apply auto
done

subsubsection Chi›

lemma HARootStates_notmem_Chi [simp]:
  " S  HAStates A;  T  States (HARoot A)   T   Chi A S"
apply (unfold Chi_def restrict_def, auto)
apply (rename_tac SA)
apply (cut_tac HA="A" in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x="HARoot A" in ballE) 
apply (erule_tac x="SA" in ballE)
apply auto
done

lemma SAStates_notmem_Chi [simp]:
  " S  States SA; T  States SA;
     SA  SAs A   T  Chi A S"
apply (unfold Chi_def restrict_def, auto)
apply (rename_tac SAA)
apply (cut_tac HA="A" in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x="SAA" in ballE) 
apply (erule_tac x="SA" in ballE)
apply auto
apply (unfold HAStates_def)
apply auto
done

lemma HAInitState_notmem_Chi [simp]:
  "S  HAStates A  HAInitState A  Chi A S"
by (unfold Chi_def restrict_def, auto)

lemma Chi_HAStates [simp]:
  "T  HAStates A  (Chi A T)  HAStates A"
apply (unfold Chi_def restrict_def)
apply (auto)
apply (cut_tac A=A and S=T in HAStates_CompFun_SAs)
apply (unfold HAStates_def)
apply auto
done

lemma Chi_HAStates_Self [simp]:
  "s   HAStates a  s  (Chi a s)"
by (unfold Chi_def restrict_def, auto)

lemma ChiRel_HAStates_Self [simp]:
  "(s,s)  (ChiRel a)"
by( unfold ChiRel_def, auto)

lemma HAStates_Chi_NoCycles:
  " s  HAStates a; t  HAStates a; s  Chi a t   t  Chi a s"
apply (unfold Chi_def restrict_def)
apply auto
apply (cut_tac HA=a in NoCycles_HA)
apply (unfold NoCycles_def)
apply (erule_tac x="{s,t}" in ballE)
apply auto
done

lemma HAStates_Chi_NoCycles_trans:
 " s  HAStates a; t  HAStates a; u  HAStates a;
    t  Chi a s; u  Chi a t   s  Chi a u"
apply (unfold Chi_def restrict_def)
apply auto
apply (cut_tac HA=a in NoCycles_HA)
apply (unfold NoCycles_def)
apply (erule_tac x="{s,t,u}" in ballE)
prefer 2
apply simp
apply (unfold HAStates_def)
apply auto
done

lemma Chi_range_disjoint:
  " S  T; T  HAStates A; S  HAStates A; U  Chi A S   U  Chi A T"  
apply (frule CompFun_Int_disjoint)
apply auto
apply (unfold Chi_def restrict_def)
apply auto
apply (rename_tac SA SAA)
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x=SA in ballE)
apply (erule_tac x=SAA in ballE)
apply auto
done

lemma SAStates_Chi_trans [rule_format]:
  " U  Chi A T; S  Chi A U; T  States SA; 
     SA  SAs A; U  HAStates A   S  States SA"
apply (frule HAStates_SA_mem)
apply auto
apply (unfold Chi_def restrict_def)
apply auto
apply (rename_tac SAA SAAA)
apply (cut_tac HA=A in NoCycles_HA)
apply (unfold NoCycles_def)
apply (erule_tac x="{U,T}" in ballE)
prefer 2
apply (simp only: HAStates_def) 
apply auto
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (rotate_tac -1)
apply (erule_tac x=SA in ballE)
apply (rotate_tac -1)
apply (erule_tac x=SAAA in ballE)
apply auto
done

subsubsection ChiRel›

lemma finite_ChiRel [simp]:
  "finite (ChiRel A)"
apply (rule_tac B="HAStates A × HAStates A" in finite_subset)
apply auto
done

lemma ChiRel_HAStates_subseteq [simp]:
  "(ChiRel A)  (HAStates A × HAStates A)"  
apply (unfold ChiRel_def Chi_def restrict_def)
apply auto
done

lemma ChiRel_CompFun:
  "s  HAStates a  ChiRel a `` {s} = ( x  the (CompFun a s). States x)"
apply (unfold ChiRel_def Chi_def restrict_def Image_def)
apply simp
apply auto
apply (frule HAStates_CompFun_SAs_mem)
apply fast
apply (unfold HAStates_def)
apply fast
done

lemma ChiRel_HARoot:
 " (x,y)  ChiRel A   y  States (HARoot A)"
apply (unfold ChiRel_def Chi_def)
apply auto 
apply (unfold restrict_def)
apply auto
apply (rename_tac SA)
apply (frule HAStates_HARoot_CompFun)
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply auto
apply (erule_tac x=SA in ballE)
apply (erule_tac x="HARoot A" in ballE)
apply auto
done

lemma HAStates_CompFun_States_ChiRel:
 "S  HAStates A   (States ` the (CompFun A S)) = ChiRel A `` {S}"
apply (unfold ChiRel_def Chi_def restrict_def)
apply auto
apply (drule HAStates_CompFun_SAs)
apply (subst HAStates_def)
apply fast
done

lemma HAInitState_notmem_Range_ChiRel [simp]: 
  "HAInitState A  Range (ChiRel A)"
by (unfold ChiRel_def, auto)

lemma HAInitState_notmem_Range_ChiRel2 [simp]: 
  "(S,HAInitState A)   (ChiRel A)"
by (unfold ChiRel_def, auto)

lemma ChiRel_OneAncestor_notmem:
  " S  T; (S,U)  ChiRel A  (T,U)  ChiRel A"
apply (unfold ChiRel_def)
apply auto
apply (simp only: Chi_range_disjoint)
done

lemma ChiRel_OneAncestor:
  " (S1,U)  ChiRel A; (S2,U)  ChiRel A   S1 = S2"
apply (rule notnotD, rule notI)
apply (simp add: ChiRel_OneAncestor_notmem)
done

lemma CompFun_ChiRel:
  " S1  HAStates A; SA  the (CompFun A S1); 
     S2  States SA   (S1,S2)  ChiRel A"
apply (unfold ChiRel_def Chi_def restrict_def)
apply auto
apply (cut_tac A=A and S=S1 in HAStates_CompFun_SAs)
apply (unfold HAStates_def)
apply auto
done

lemma CompFun_ChiRel2:
 " (S,T)  ChiRel A; T  States SA; SA  SAs A   SA  the (CompFun A S)"
apply (unfold ChiRel_def Chi_def restrict_def)
apply auto
apply (rename_tac SAA)
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x=SA in ballE)
apply (rotate_tac -1)
apply (erule_tac x=SAA in ballE) 
apply auto
done

lemma ChiRel_HAStates_NoCycles:
  "(s,t)  (ChiRel a)  (t,s)  (ChiRel a)"
apply (unfold ChiRel_def)
apply auto
apply (frule HAStates_Chi_NoCycles)
apply auto
done

lemma HAStates_ChiRel_NoCycles_trans:
  " (s,t)  (ChiRel a); (t,u)  (ChiRel a)   (u,s)  (ChiRel a)"
apply (unfold ChiRel_def)
apply auto
apply (frule HAStates_Chi_NoCycles_trans)
apply fast
back
back
prefer 3
apply fast
apply auto
done

lemma SAStates_ChiRel:
  " S  States SA; T  States SA;
     SA  SAs A   (S,T)  (ChiRel A)"
by (unfold ChiRel_def, auto)

lemma ChiRel_SA_OneAncestor: 
   " (S,T)  ChiRel A; T  States SA; 
      U  States SA; SA  SAs A   
      (S,U)  ChiRel A"
apply (frule CompFun_ChiRel2)
apply auto
apply (rule CompFun_ChiRel)
apply auto
done

lemma ChiRel_OneAncestor2: 
  " S  HAStates A; S  States (HARoot A)   
     ∃! T. (T,S)  ChiRel A"
apply (unfold ChiRel_def)
apply auto
prefer 2
apply (rename_tac T U)
prefer 2
apply (unfold Chi_def restrict_def)
apply auto
prefer 2
apply (rename_tac SA SAA)
prefer 2
apply (cut_tac HA=A in OneAncestor_HA)
apply (unfold OneAncestor_def)
apply (fold HARoot_def)
apply auto
apply (simp cong: rev_conj_cong)
apply (unfold HAStates_def)
apply auto
apply (rename_tac SA)
apply (erule_tac x=SA in ballE)
apply auto
apply (case_tac "T = U")
apply auto
apply (frule CompFun_Int_disjoint)
apply (unfold HAStates_def)
apply auto
apply (case_tac "SA=SAA")
apply auto
apply (cut_tac HA=A in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x=SAA in ballE)
apply (erule_tac x=SA in ballE)
apply auto
apply (cut_tac S=T and A=A in HAStates_CompFun_SAs)
apply (unfold HAStates_def)
apply fast
apply fast
apply (cut_tac S=U and A=A in HAStates_CompFun_SAs)
apply (unfold HAStates_def)
apply fast
apply fast
done

lemma HARootStates_notmem_Range_ChiRel [simp]:
  "S  States (HARoot A)  S  Range (ChiRel A)"
by (unfold ChiRel_def, auto)

lemma ChiRel_int_disjoint:
  "S  T  (ChiRel A `` {S})  (ChiRel A `` {T}) = {}"  
apply (unfold ChiRel_def)
apply auto
apply (simp only: Chi_range_disjoint)
done

lemma SAStates_ChiRel_trans [rule_format]:
  " (S,U)  (ChiRel A); (U,T)  ChiRel A; 
     S  States SA; SA  SAs A    T  States SA"
apply auto
apply (unfold ChiRel_def)
apply auto
apply (frule SAStates_Chi_trans)
back
apply fast+
done

lemma HAInitStates_InitState_trancl: 
  "  S  HAInitStates (HA ST); A  the (CompFun (HA ST) S)   
       (S, InitState A)  (ChiRel (HA ST)  HAInitStates (HA ST) × HAInitStates (HA ST))+"
apply (case_tac "S  HAStates (HA ST)") 
apply (frule CompFun_ChiRel)
apply fast+
apply (rule InitState_States)
apply auto
apply (rule r_into_trancl')
apply auto
apply (rule CompFun_HAInitStates_HAStates)
apply auto
done

lemma HAInitStates_InitState_trancl2:
 " S  HAStates (HA ST); A  the (CompFun (HA ST) S); 
   (x, S)  (ChiRel (HA ST)  HAInitStates (HA ST) × HAInitStates (HA ST))+ 
   (x, InitState A)  (ChiRel (HA ST)  HAInitStates (HA ST) × HAInitStates (HA ST))+"
apply (rule_tac a="x" and b="S" and r="ChiRel (HA ST)  HAInitStates (HA ST) × HAInitStates (HA ST)" in converse_trancl_induct)
apply auto
prefer 2
apply (rename_tac T U)
prefer 2
apply (case_tac "S  HAStates (HA ST)") 
apply (frule CompFun_ChiRel)
apply fast
apply (rule InitState_States)
apply simp
apply (rule trancl_trans [of _ S])
apply (rule r_into_trancl')
apply auto
apply (rule r_into_trancl')
apply auto
apply (rule CompFun_HAInitStates_HAStates)
prefer 2
apply fast
apply (cut_tac A="HA ST" in HAInitStates_HAStates, fast)
apply (rule_tac y = U in trancl_trans)
apply (rule r_into_trancl')
apply auto
done

subsubsection ChiPlus›

lemma ChiPlus_ChiRel [simp]:
  "(S,T)  ChiRel A  (S,T)  ChiPlus A"
apply (unfold ChiPlus_def)
apply (frule r_into_trancl)
apply auto
done

lemma ChiPlus_HAStates [simp]:
  "(ChiPlus A)  (HAStates A × HAStates A)"  
apply (unfold ChiPlus_def)
apply (rule trancl_subset_Sigma)
apply auto
done

lemma ChiPlus_subset_States:
  "ChiPlus a `` {t}   (States ` (SAs a))"
apply (cut_tac A=a in ChiPlus_HAStates) 
apply (unfold HAStates_def)
apply auto
done

lemma finite_ChiPlus [simp]: 
  "finite (ChiPlus A)"
apply (rule_tac B="HAStates A × HAStates A" in finite_subset)
apply auto
done

lemma ChiPlus_OneAncestor: 
  " S  HAStates A; S  States (HARoot A)   
      T. (T,S)  ChiPlus A"
apply (unfold ChiPlus_def)
apply (frule ChiRel_OneAncestor2)
apply auto
done

lemma ChiPlus_HAStates_Left:
 "(S,T)  ChiPlus A  S  HAStates A"
apply (cut_tac A=A in ChiPlus_HAStates) 
apply (unfold HAStates_def)
apply auto
done

lemma ChiPlus_HAStates_Right:
 "(S,T)  ChiPlus A  T   HAStates A"
apply (cut_tac A=A in ChiPlus_HAStates) 
apply (unfold HAStates_def)
apply auto
done

lemma ChiPlus_ChiRel_int [rule_format]:
  " (T,S)  (ChiPlus A)  (ChiPlus A `` {T})  (ChiRel A `` {S}) = (ChiRel A `` {S})"  
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="S" and r="(ChiRel A)" in converse_trancl_induct)
apply auto
done

lemma ChiPlus_ChiPlus_int [rule_format]:
  " (T,S)  (ChiPlus A)  (ChiPlus A `` {T})  (ChiPlus A `` {S}) = (ChiPlus A `` {S})"  
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="S" and r="(ChiRel A)" in converse_trancl_induct)
apply auto
done

lemma ChiPlus_ChiRel_NoCycle_1 [rule_format]:
 " (T,S)  ChiPlus A     
   (insert S (insert T ({U. (T,U)  ChiPlus A  (U,S)  ChiPlus A})))   (ChiRel A `` {T})  {}"
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="S" and r="(ChiRel A)" in converse_trancl_induct)
apply (unfold Image_def Int_def)
apply auto
done

lemma ChiPlus_ChiRel_NoCycle_2 [rule_format]:
 " (T,S)  ChiPlus A   (S,T)  (ChiRel A)  
   (insert S (insert T ({U. (T,U)  ChiPlus A  (U,S)  ChiPlus A})))   (ChiRel A `` {S})  {}"
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="S" and r="(ChiRel A)" in converse_trancl_induct)
apply (unfold Image_def Int_def)
apply auto
done

lemma ChiPlus_ChiRel_NoCycle_3 [rule_format]:
 " (T,S)  ChiPlus A   (S,T)  (ChiRel A)  (T,U)   ChiPlus A  (U, S)  ChiPlus A  
   (insert S (insert T ({U. (T,U)  ChiPlus A  (U,S)  ChiPlus A})))   (ChiRel A `` {U})  {}"
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="S" and r="(ChiRel A)" in trancl_induct)
apply (unfold Image_def Int_def, simp)
apply (rename_tac V)
prefer 2
apply (rename_tac V W)
prefer 2
apply (simp, safe)
apply (simp only: ChiRel_HAStates_NoCycles)
apply simp
apply (case_tac "(U,W)  (ChiRel A)", fast, rotate_tac 5, frule tranclD3, fast, blast intro: trancl_into_trancl)+
done

lemma ChiPlus_ChiRel_NoCycle_4 [rule_format]:
 " (T,S)  ChiPlus A   (S,T)   (ChiRel A)  ((ChiPlus A ``{T})  (ChiRel A `` {S}))  {}"
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="S" and r="(ChiRel A)" in trancl_induct)
apply (unfold Image_def Int_def)
apply auto
apply (simp only: ChiRel_HAStates_NoCycles)
apply (rule_tac x=T in exI)
apply simp
apply (rule_tac x=T in exI)
apply simp
done

lemma ChiRel_ChiPlus_NoCycles:
 "(S,T)  (ChiRel A)  (T,S)  (ChiPlus A)"
apply (cut_tac HA=A in NoCycles_HA)
apply (unfold NoCycles_def)
apply (erule_tac x="insert S (insert T ({U. (T,U)  ChiPlus A  (U,S)  ChiPlus A}))" in ballE)
prefer 2
apply (simp add: ChiPlus_subset_States)
apply (cut_tac A=A in ChiPlus_HAStates) 
apply (unfold HAStates_def)
apply auto
apply (frule ChiPlus_ChiRel_NoCycle_2)
apply fast
apply (simp add:ChiRel_CompFun)
apply (frule ChiPlus_ChiRel_NoCycle_1)
apply (simp add:ChiRel_CompFun)
apply (frule ChiPlus_ChiRel_NoCycle_3)
apply fast
apply fast
back
apply fast
apply (rename_tac V)
apply (case_tac "V  HAStates A") 
apply (simp add: ChiRel_CompFun)
apply (simp only: ChiPlus_HAStates_Right)
apply fast
done

lemma ChiPlus_ChiPlus_NoCycles:
 "(S,T)  (ChiPlus A)  (T,S)  (ChiPlus A)"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="T" and r="(ChiRel A)" in trancl_induct)
apply fast
apply (frule ChiRel_ChiPlus_NoCycles)
apply (auto intro: trancl_into_trancl2 simp add:ChiPlus_def)
done

lemma ChiPlus_NoCycles [rule_format]:
 "(S,T)  (ChiPlus A)  S  T"
apply (frule ChiPlus_ChiPlus_NoCycles)
apply auto
done

lemma ChiPlus_NoCycles_2 [simp]:
 "(S,S)  (ChiPlus A)"
apply (rule notI)
apply (frule ChiPlus_NoCycles)
apply fast
done

lemma ChiPlus_ChiPlus_NoCycles_2:
  " (S,U)  ChiPlus A; (U,T)  ChiPlus A   (T,S)   ChiPlus A"
apply (rule ChiPlus_ChiPlus_NoCycles)
apply (auto intro: trancl_trans simp add: ChiPlus_def)
done

lemma ChiRel_ChiPlus_trans:
   " (U,S)  ChiPlus A; (S,T)  ChiRel A  (U,T)  ChiPlus A"
apply (unfold ChiPlus_def)
apply auto
done

lemma ChiRel_ChiPlus_trans2:
   " (U,S)  ChiRel A; (S,T)  ChiPlus A   (U,T)  ChiPlus A"
apply (unfold ChiPlus_def)
apply auto
done

lemma ChiPlus_ChiRel_Ex [rule_format]:
  " (S,T)  ChiPlus A   (S,T)  ChiRel A  
    ( U. (S,U)  ChiPlus A  (U,T)  ChiRel A)"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="T" and r="(ChiRel A)" in converse_trancl_induct)
apply auto
apply (rename_tac U)
apply (rule_tac x=U in exI)
apply auto
done

lemma ChiPlus_ChiRel_Ex2 [rule_format]:
  " (S,T)  ChiPlus A   (S,T)  ChiRel A  
    ( U. (S,U)  ChiRel A  (U,T)  ChiPlus A)"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="T" and r="(ChiRel A)" in converse_trancl_induct)
apply auto
done

lemma HARootStates_Range_ChiPlus [simp]:
  " S  States (HARoot A)   S  Range (ChiPlus A)" 
by (unfold ChiPlus_def, auto)

lemma HARootStates_Range_ChiPlus2 [simp]:
  " S  States (HARoot A)   (x,S)  (ChiPlus A)" 
by (frule HARootStates_Range_ChiPlus, unfold Domain_converse [symmetric], fast)

lemma SAStates_ChiPlus_ChiRel_NoCycle_1 [rule_format]:
 " (S,U)  ChiPlus A; SA  SAs A   (U,T)  (ChiRel A)  S  States SA  T  States SA  
   (insert S (insert U ({V. (S,V)  ChiPlus A  (V,U)  ChiPlus A})))  (ChiRel A `` {U})  {}"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="U" and r="(ChiRel A)" in converse_trancl_induct)
apply (simp, safe) 
apply (simp only: SAStates_ChiRel_trans)
apply (simp add:ChiRel_CompFun)
apply safe
apply (erule_tac x=SA in ballE)
apply (simp add: CompFun_ChiRel2)+
apply (simp add:Int_def, fast)
apply auto
apply (fold ChiPlus_def)
apply (rename_tac W)
apply (frule_tac U=U and T=U and S=W in ChiRel_ChiPlus_trans2)
apply auto
done

lemma SAStates_ChiPlus_ChiRel_NoCycle_2 [rule_format]:
 " (S,U)   ChiPlus A    (U,T)  (ChiRel A)  
   (insert S (insert U ({V. (S,V)  ChiPlus A  (V,U)  ChiPlus A})))   (ChiRel A `` {S})  {}"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="U" and r="(ChiRel A)" in converse_trancl_induct)
apply (unfold Image_def Int_def)
apply auto
done

(* TO DO *)

lemma SAStates_ChiPlus_ChiRel_NoCycle_3 [rule_format]:
 " (S,U)   ChiPlus A    (U,T)  (ChiRel A)  (S,s)  ChiPlus A  (s,U)  ChiPlus A 
   (insert S (insert U ({V. (S,V)  ChiPlus A  (V,U)  ChiPlus A})))   (ChiRel A `` {s})  {}"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="U" and r="(ChiRel A)" in trancl_induct)
apply fast
apply (rename_tac W)
prefer 2
apply (rename_tac W X)
prefer 2
apply (unfold Image_def Int_def)
apply (simp, safe)
apply (fold ChiPlus_def)
apply (case_tac "(s,W)  ChiRel A")
apply fast
apply (frule_tac S=s and T=W in ChiPlus_ChiRel_Ex2)
apply simp
apply safe
apply (rename_tac X)
apply (rule_tac x=X in exI)
apply (fast intro: ChiRel_ChiPlus_trans)
apply simp
apply (case_tac "(s,X)  ChiRel A")
apply force
apply (frule_tac S=s and T=X in ChiPlus_ChiRel_Ex2)
apply simp
apply safe
apply (rename_tac Y)
apply (erule_tac x=Y in allE)
apply simp
apply (fast intro: ChiRel_ChiPlus_trans)
apply simp
apply (case_tac "(s,X)  ChiRel A")
apply force
apply (frule_tac S=s and T=X in ChiPlus_ChiRel_Ex2)
apply simp
apply safe
apply (rename_tac Y)
apply (erule_tac x=Y in allE)
apply simp
apply (fast intro: ChiRel_ChiPlus_trans)
apply fastforce
apply simp
apply (erule_tac x=W in allE)
apply simp
apply simp
apply (rename_tac Y)
apply (erule_tac x=Y in allE)
apply simp
apply (fast intro: ChiRel_ChiPlus_trans)
done

lemma SAStates_ChiPlus_ChiRel_trans [rule_format]:
  " (S,U)  (ChiPlus A); (U,T)  (ChiRel A); S  States SA; SA  SAs A   T  States SA"
apply (cut_tac HA=A in NoCycles_HA)
apply (unfold NoCycles_def)
apply (erule_tac x="insert S (insert U ({V. (S,V)  ChiPlus A  (V,U)  ChiPlus A}))" in ballE)
prefer 2
apply (simp add: ChiPlus_subset_States)
apply (cut_tac A=A in ChiPlus_HAStates) 
apply (unfold HAStates_def)
apply auto[1]
apply safe
apply fast
apply (frule SAStates_ChiPlus_ChiRel_NoCycle_2)
apply fast
apply (frule HAStates_SA_mem)
apply fast
apply (simp only:ChiRel_CompFun)
apply (frule SAStates_ChiPlus_ChiRel_NoCycle_1)
apply auto[3]
apply fast
apply (simp add:ChiRel_CompFun)
apply (frule SAStates_ChiPlus_ChiRel_NoCycle_3)
apply fast
apply fast
back
apply fast
apply (simp only:ChiPlus_HAStates_Left ChiRel_CompFun)
done

lemma SAStates_ChiPlus2 [rule_format]:
  " (S,T)  ChiPlus A; SA  SAs A    S  States SA  T  States SA"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="T" and r="(ChiRel A)" in trancl_induct)
apply auto
apply (rename_tac U)
apply (frule_tac S=S and T=U in SAStates_ChiRel) 
apply auto
apply (fold ChiPlus_def)
apply (simp only: SAStates_ChiPlus_ChiRel_trans)
done

lemma SAStates_ChiPlus [rule_format]:
 " S  States SA; T  States SA; SA  SAs A   (S,T)  ChiPlus A"
apply auto
apply (simp only: SAStates_ChiPlus2)
done

lemma SAStates_ChiPlus_ChiRel_OneAncestor [rule_format]:
  " T  States SA; SA  SAs A; (S,U)  ChiPlus A   S  T  S  States SA  (T,U)  ChiRel A"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="U" and r="(ChiRel A)" in trancl_induct)
apply auto
apply (simp add: ChiRel_OneAncestor_notmem)
apply (rename_tac V W)
apply (fold ChiPlus_def)
apply (case_tac "V=T")
apply (simp add: ChiRel_OneAncestor_notmem SAStates_ChiPlus)+
done

lemma SAStates_ChiPlus_OneAncestor [rule_format]:
  " T  States SA; SA  SAs A; (S,U)  ChiPlus A    S  T   
     S  States SA  (T,U)  ChiPlus A"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="U" and r="(ChiRel A)" in trancl_induct)
apply auto
apply (fold ChiPlus_def)
apply (rename_tac V)
apply (frule_tac T=S and S=T and U=V in SAStates_ChiPlus_ChiRel_OneAncestor)
apply auto
apply (rename_tac V W)
apply (frule_tac S=T and T=W in ChiPlus_ChiRel_Ex)
apply auto
apply (frule_tac T=T and S=S and U=W in SAStates_ChiPlus_ChiRel_OneAncestor)
apply auto
apply (rule ChiRel_ChiPlus_trans)
apply auto
apply (rename_tac X)
apply (case_tac "V=X")
apply simp
apply (simp add: ChiRel_OneAncestor_notmem)
done

lemma ChiRel_ChiPlus_OneAncestor [rule_format]:
  " (T,U)  ChiPlus A   T  S  (S,U)  ChiRel A  (T,S)  ChiPlus A"
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="U" and r="(ChiRel A)" in trancl_induct)
apply auto
apply (fast intro:ChiRel_OneAncestor)
apply (rename_tac V W)
apply (case_tac "S=V")
apply auto
apply (fast intro:ChiRel_OneAncestor)
done

lemma ChiPlus_SA_OneAncestor [rule_format]: 
   " (S,T)  ChiPlus A; 
      U  States SA; SA  SAs A   T  States SA 
      (S,U)  ChiPlus A"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="T" and r="(ChiRel A)" in converse_trancl_induct)
apply auto
apply (frule ChiRel_SA_OneAncestor)
apply fast+
done

subsubsection ChiStar›

lemma ChiPlus_ChiStar [simp]:
  " (S,T)  ChiPlus A    (S,T)  ChiStar A"
by (unfold ChiPlus_def ChiStar_def, auto)

lemma HARootState_Range_ChiStar [simp]:
  " x  S; S  States (HARoot A)   (x,S)  (ChiStar A)" 
apply (unfold ChiStar_def)
apply (subst rtrancl_eq_or_trancl)
apply (fold ChiPlus_def)
apply auto
done

lemma ChiStar_Self [simp]:
 "(S,S)  ChiStar A"
apply (unfold ChiStar_def)
apply simp
done

lemma ChiStar_Image [simp]:  
  "S  M  S  (ChiStar A `` M)"
apply (unfold Image_def)
apply (auto intro: ChiStar_Self)
done

lemma ChiStar_ChiPlus_noteq: 
  " S  T; (S,T)  ChiStar A   (S,T)  ChiPlus A"
apply (unfold ChiPlus_def ChiStar_def)
apply (simp add: rtrancl_eq_or_trancl)
done

lemma ChiRel_ChiStar_trans:
  " (S,U)  ChiStar A; (U,T)  ChiRel A   (S,T)  ChiStar A"
apply (unfold ChiStar_def)
apply auto
done

subsubsection InitConf›

lemma InitConf_HAStates [simp]:
  "InitConf A  HAStates A"
apply (unfold InitConf_def HAStates_def)
apply auto
apply (rule rtrancl_induct)
back
apply auto
apply (rule_tac x="HARoot A" in bexI)
apply auto
apply (unfold HAStates_def ChiRel_def)
apply auto
done

lemma InitConf_HAStates2 [simp]:
 "S  InitConf A  S  HAStates A"
apply (cut_tac A=A in InitConf_HAStates)
apply fast
done

lemma HAInitState_InitConf [simp]:
  "HAInitState A  InitConf A"
by (unfold HAInitState_def InitConf_def, auto)

lemma InitConf_HAInitState_HARoot:
 "[| S  InitConf A; S  HAInitState A |] ==> S  States (HARoot A)"
apply (unfold InitConf_def)
apply auto
apply (rule mp)
prefer 2 
apply fast
back
apply (rule mp)
prefer 2
apply fast
back
back
apply (rule_tac b=S in rtrancl_induct)
apply auto
apply (simp add: ChiRel_HARoot)+
done

lemma InitConf_HARoot_HAInitState [simp]:
 " S  InitConf A; S  States (HARoot A)   S = HAInitState A"
apply (subst not_not [THEN sym])
apply (rule notI)
apply (simp add:InitConf_HAInitState_HARoot)
done

lemma HAInitState_CompFun_InitConf [simp]:
 "[|SA  the (CompFun A  (HAInitState A)) |] ==> (InitState SA)  InitConf A"
apply (unfold InitConf_def HAStates_def)
apply auto
apply (rule rtrancl_Int)
apply auto
apply (cut_tac A=A and S="HAInitState A" in HAStates_CompFun_States_ChiRel)
apply auto
apply (rule Image_singleton_iff [THEN subst])
apply (rotate_tac -1)
apply (drule sym)
apply simp
apply (rule_tac x=SA in bexI)
apply auto
done

lemma InitState_CompFun_InitConf:
 "[| S  HAStates A; SA  the (CompFun A S); S  InitConf A |] ==> (InitState SA)  InitConf A"
apply (unfold InitConf_def)
apply auto
apply (rule_tac b=S in rtrancl_into_rtrancl)
apply fast
apply (frule rtrancl_Int1)
apply auto
apply (case_tac "S = HAInitState A")
apply simp
apply (rule rtrancl_mem_Sigma)
apply auto
apply (cut_tac A=A and S=S in HAStates_CompFun_States_ChiRel)
apply auto
apply (rule Image_singleton_iff [THEN subst])
apply (rotate_tac -1)
apply (drule sym)
apply simp 
apply (rule_tac x=SA in bexI)
apply auto
done

lemma InitConf_HAInitStates:
  "InitConf A  HAInitStates A"
apply (unfold InitConf_def)
apply (rule subsetI)
apply auto
apply (frule rtrancl_Int1)
apply (case_tac "x = HAInitState A")
apply simp
apply (rule rtrancl_mem_Sigma)
apply auto
done

lemma InitState_notmem_InitConf:
 "[| SA  the (CompFun A S); S  InitConf A; T  States SA;
     T  InitState SA |] ==>  T  InitConf A"
apply (frule InitConf_HAStates2)
apply (unfold InitConf_def)
apply auto
apply (rule mp)
prefer 2
apply fast
apply (rule mp)
prefer 2
apply fast
back
apply (rule mp)
prefer 2
apply fast
back
back
apply (rule mp)
prefer 2
apply fast
back
back 
back
apply (rule mp)
prefer 2
apply fast
back
back 
back
back
apply (rule mp)
prefer 2
apply fast
back
back 
back
back
back
apply (rule_tac b=T in rtrancl_induct)
apply auto
done

lemma InitConf_CompFun_InitState [simp]:
 " SA  the (CompFun A S); S  InitConf A; T  States SA;
    T  InitConf A   T = InitState SA"
apply (subst not_not [THEN sym])
apply (rule notI)
apply (frule InitState_notmem_InitConf)
apply auto
done

lemma InitConf_ChiRel_Ancestor:
  " T  InitConf A; (S,T)  ChiRel A   S  InitConf A"
apply (unfold InitConf_def)
apply auto
apply (erule rtranclE)
apply auto
apply (rename_tac U)
apply (cut_tac A=A  in HAInitState_notmem_Range_ChiRel)
apply auto
apply (case_tac "U = S")
apply (auto simp add: ChiRel_OneAncestor)
done

lemma InitConf_CompFun_Ancestor:
  " S  HAStates A; SA  the (CompFun A S); T  InitConf A; T  States SA 
      S  InitConf A"
apply (rule InitConf_ChiRel_Ancestor)
apply auto
apply (rule CompFun_ChiRel)
apply auto
done

subsubsection StepConf›

lemma StepConf_EmptySet [simp]:
  "StepConf A C {} = C"
by (unfold StepConf_def, auto)

end

Theory HASem

(*  Title:      statecharts/HA/HASem.thy

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

section ‹Semantics of Hierarchical Automata›
theory HASem
imports HA
begin

subsection ‹Definitions›

definition
  RootExSem :: "[(('s,'e,'d)seqauto) set, 's  ('s,'e,'d)seqauto set,
                 's set] => bool" where
  "RootExSem F G C == (∃! S. S  States (Root F G)  S  C)"

definition
  UniqueSucStates ::  "[(('s,'e,'d)seqauto) set, 's  ('s,'e,'d)seqauto set,
                        's set]  bool" where
  "UniqueSucStates F G C  ==  S  ((States ` F)).
                                    A  the (G S).
                                      if (S  C) then
                                       ∃! S' . S'   States A  S'  C
                                     else
                                        S  States A. S  C"

definition
  IsConfSet :: "[(('s,'e,'d)seqauto) set, 's  ('s,'e,'d)seqauto set,
                 's set] => bool" where
  "IsConfSet F G C ==
                C  ((States ` F)) &
                RootExSem F G C &
                UniqueSucStates F G C" 

definition
  Status :: "[('s,'e,'d)hierauto,
              's set,
              'e set,
              'd data] => bool" where
  "Status HA C E D == E  HAEvents HA  
                      IsConfSet (SAs HA) (CompFun HA) C  
                      Data.DataSpace (HAInitValue HA) = Data.DataSpace D"

subsubsection Status›

lemma Status_EmptySet:
 "(Abs_hierauto ((@ x . True),
    {Abs_seqauto ({ @ x . True}, (@ x . True), {}, {})}, {}, Map.empty(@ x . True  {})), 
  {@x. True},{}, @x. True)  
  {(HA,C,E,D) | HA C E D. Status HA C E D}"
apply (unfold Status_def CompFun_def SAs_def)
apply auto
apply (subst Abs_hierauto_inverse)
apply (subst hierauto_def)
apply (rule HierAuto_EmptySet)
apply (subst Abs_hierauto_inverse)
apply (subst hierauto_def)
apply (rule HierAuto_EmptySet)
apply auto
apply (unfold IsConfSet_def UniqueSucStates_def RootExSem_def)
apply auto
apply (unfold States_def)
apply auto
apply (unfold Root_def)
apply (rule someI2)
apply (rule conjI)
apply fast
apply (simp add: ran_def) 
apply simp
apply (subst Abs_seqauto_inverse)
apply (subst seqauto_def)
apply (rule SeqAuto_EmptySet)
apply simp
apply (unfold HAInitValue_def)
apply auto
apply (subst Abs_hierauto_inverse)
apply (subst hierauto_def)
apply (rule HierAuto_EmptySet)
apply simp
done

definition
  "status =
    {(HA,C,E,D) |
        (HA::('s,'e,'d)hierauto)
        (C::('s set))
        (E::('e set))
        (D::'d data). Status HA C E D}"

typedef ('s,'e,'d) status =
    "status :: (('s,'e,'d)hierauto * 's set * 'e set * 'd data) set"
  unfolding status_def
  apply (rule exI)
  apply (rule Status_EmptySet)
  done


definition
  HA :: "('s,'e,'d) status  => ('s,'e,'d) hierauto" where
  "HA == fst o Rep_status"

definition
  Conf :: "('s,'e,'d) status  => 's set" where
  "Conf == fst o snd o Rep_status"

definition
  Events :: "('s,'e,'d) status  => 'e set" where
  "Events == fst o snd o snd o Rep_status"

definition
  Value :: "('s,'e,'d) status  => 'd data" where
  "Value == snd o snd o snd o Rep_status"

definition
  RootState :: "('s,'e,'d) status  => 's" where
  "RootState ST == @ S. S  Conf ST  S  States (HARoot (HA ST))"

(* -------------------------------------------------------------- *)
(* enabled transitions                                            *)
(* -------------------------------------------------------------- *)

definition
  EnabledTrans :: "(('s,'e,'d)status * ('s,'e,'d)seqauto *
                    ('s,'e,'d)trans) set" where
  "EnabledTrans == {(ST,SA,T) .
                       SA  SAs (HA ST)  
                       T  Delta SA  
                       source T  Conf ST  
                       (Conf ST, Events ST, Value ST) |= (label T) }"

definition
  ET :: "('s,'e,'d) status => (('s,'e,'d) trans) set" where
  "ET ST ==  SA  SAs (HA ST). (EnabledTrans `` {ST}) `` {SA}"

(* -------------------------------------------------------------- *)
(* maximal non conflicting set of transitions                     *)
(* -------------------------------------------------------------- *)

definition
  MaxNonConflict :: "[('s,'e,'d)status,
                      ('s,'e,'d)trans set] => bool" where
  "MaxNonConflict ST T ==
        (T  ET ST)  
        ( A  SAs (HA ST). card (T Int Delta A)  1)   
        ( t  (ET ST). (t  T) =  (¬ ( t'  ET ST. HigherPriority (HA ST) (t',t))))"

(* -------------------------------------------------------------- *)
(* resolving the occurrence of racing with interleaving semantic  *)
(* for one set of transitions                                     *)
(* -------------------------------------------------------------- *)

definition
 ResolveRacing :: "('s,'e,'d)trans set
                   => ('d update set)" where
 "ResolveRacing TS ==
            let
                U = PUpdate (Label TS)
            in
                SequentialRacing U"

(* -------------------------------------------------------------- *)
(* HPT is a set, there can be more than one! If there are         *)
(* nondeterministic transitions t1, t2 in one SA : SAs A, then    *)
(* they are not in conflict wt higher priority. We have to chose  *)
(* one and get different sets.                                    *)
(* -------------------------------------------------------------- *)

definition
 HPT :: "('s,'e,'d)status => (('s,'e,'d)trans set) set" where
 "HPT ST == { T. MaxNonConflict ST T}"

(* -------------------------------------------------------------- *)
(* The initials status can be defined now for a given automaton.  *)
(* -------------------------------------------------------------- *)

definition
 InitStatus :: "('s,'e,'d)hierauto => ('s,'e,'d)status" where
 "InitStatus A ==
    Abs_status (A,InitConf A,{}, HAInitValue A)"

(* -------------------------------------------------------------- *)
(* The next status for a given status can be defined now by a     *)
(* step.                                                          *)
(* -------------------------------------------------------------- *)

definition
  StepActEvent :: "('s,'e,'d)trans set => 'e set" where
  "StepActEvent TS == Union (Actevent (Label TS))"

definition
  StepStatus :: "[('s,'e,'d)status, ('s,'e,'d)trans set, 'd update]
                 => ('s,'e,'d)status" where
  "StepStatus ST TS U =
                (let
                   (A,C,E,D) = Rep_status ST;
                   C'        = StepConf A C TS;
                   E'        = StepActEvent TS;
                   D'        = U !!! D
                 in
                   Abs_status (A,C',E',D'))"

(* --------------------------------------------------------------- *)
(* The Relation StepRel defines semantic transitions on statuses   *)
(* for given hierarchical automaton.                               *)
(* --------------------------------------------------------------- *)

definition
  StepRelSem :: "('s,'e,'d)hierauto
              => (('s,'e,'d)status * ('s,'e,'d)status) set" where
  "StepRelSem A == {(ST,ST'). (HA ST) = A 
                    ((HPT ST  {}) 
                       (TS  HPT ST.
                           U  ResolveRacing TS.
                                  ST' = StepStatus ST TS U)) &
                    ((HPT ST = {}) 
                       (ST' = StepStatus ST {} DefaultUpdate))}"

(* --------------------------------------------------------------- *)
(* The Relation StepRel defines semantic transitions on statuses   *)
(* The set of all reachable stati can now be defined inductively   *)
(* as the set of statuses derived through applications of          *)
(* transitions starting from the initial status TInitStatus 0.     *)
(* --------------------------------------------------------------- *)

inductive_set
  ReachStati  :: "('s,'e,'d)hierauto => ('s,'e,'d) status set"
  for A ::  "('s,'e,'d)hierauto"
where
  Status0 : "InitStatus A  ReachStati A"
| StatusStep :
     " ST  ReachStati A;  TS  HPT ST; U  ResolveRacing TS 
       StepStatus ST TS U  ReachStati A"

subsection ‹Lemmas›

lemma Rep_status_tuple: 
 "Rep_status ST = (HA ST, Conf ST, Events ST, Value ST)"
by (unfold HA_def Conf_def Events_def Value_def, simp) 

lemma Rep_status_select:
 "(HA ST, Conf ST, Events ST, Value ST)  status"
by (rule Rep_status_tuple [THEN subst], rule Rep_status)

lemma Status_select [simp]:
  "Status (HA ST) (Conf ST) (Events ST) (Value ST)"
apply (cut_tac Rep_status_select)
apply (unfold status_def)
apply simp
done

subsubsection IsConfSet›

lemma IsConfSet_Status [simp]: 
 "IsConfSet (SAs (HA ST)) (CompFun (HA ST)) (Conf ST)"
apply (cut_tac Rep_status_select)
apply (unfold status_def Status_def)
apply auto
done

subsubsection InitStatus›

lemma IsConfSet_InitConf [simp]:
  "IsConfSet (SAs A) (CompFun A) (InitConf A)"
apply (unfold IsConfSet_def RootExSem_def UniqueSucStates_def, fold HARoot_def)
apply (rule conjI)
apply (fold HAStates_def, simp)
apply (rule conjI)
apply (rule_tac a="HAInitState A" in ex1I)
apply auto
apply (rename_tac S SA)
apply (case_tac "S  InitConf A")
apply auto
apply (rule_tac x="InitState SA" in exI)
apply auto
apply (rule InitState_CompFun_InitConf)
apply auto
apply (rename_tac S SA T U)
apply (case_tac "U = InitState SA")
apply auto
apply (simp only:InitConf_CompFun_Ancestor HAStates_SA_mem, simp)+
done

lemma InitConf_status [simp]:
  "(A, InitConf A, {}, HAInitValue A)   status"
apply (cut_tac Rep_status_select)
apply (unfold status_def Status_def)
apply auto
done

lemma Conf_InitStatus_InitConf [simp]:
 "Conf (InitStatus A) = InitConf A"
apply (unfold Conf_def InitStatus_def)
apply simp
apply (subst Abs_status_inverse)
apply auto
done

lemma HAInitValue_Value_DataSpace_Status [simp]:
  "Data.DataSpace (HAInitValue (HA ST)) = Data.DataSpace (Value ST)"
apply (cut_tac Rep_status_select)
apply (unfold status_def Status_def)
apply fast
done

lemma Value_InitStatus_HAInitValue [simp]:
 "Value (InitStatus A) = HAInitValue A"
apply (unfold Value_def InitStatus_def)
apply simp
apply (subst Abs_status_inverse)
apply auto
done

lemma HA_InitStatus [simp]:
 "HA (InitStatus A) = A"
apply (unfold InitStatus_def HA_def)
apply auto
apply (subst Abs_status_inverse)
apply auto
done

subsubsection Events›

lemma Events_HAEvents_Status: 
  "(Events ST)  HAEvents (HA ST)"
apply (cut_tac Rep_status_select)
apply (unfold status_def Status_def)
apply fast
done

lemma TS_EventSet:
    "TS   ET ST   (Actevent (Label TS))  HAEvents (HA ST)"
apply (unfold Actevent_def actevent_def ET_def EnabledTrans_def Action_def Label_def)
apply (cut_tac HA="HA ST" in HAEvents_SAEvents_SAs)
apply auto
apply (rename_tac Event Source Trigger Guard Action Update Target)
apply (unfold SAEvents_def)
apply (erule subsetCE)
apply auto
apply (rename_tac SA)
apply (erule subsetCE)
apply auto
apply (erule_tac x=SA in ballE)
apply auto
apply (erule_tac x="(Trigger, Guard, Action, Update)" in ballE)
apply auto
apply (cut_tac SA=SA in Label_Delta_subset)
apply (erule subsetCE)
apply (unfold Label_def image_def)
apply auto
done

subsubsection StepStatus›

lemma StepStatus_empty:
   "Abs_status (HA ST, Conf ST, {}, U !!! (Value ST)) = StepStatus ST {} U"
apply (unfold StepStatus_def Let_def)
apply auto
apply (subst Rep_status_tuple)
apply auto
apply (unfold StepActEvent_def)
apply auto
done

lemma status_empty_eventset [simp]:
      "(HA ST, Conf ST, {}, U !!! (Value ST))  status"
apply (unfold status_def Status_def)
apply auto
done

lemma HA_StepStatus_emptyTS [simp]:
  "HA (StepStatus ST {} U) = HA ST"
apply (subst StepStatus_empty [THEN sym])
apply (unfold HA_def)
apply auto
apply (subst Abs_status_inverse)
apply auto
apply (subst Rep_status_tuple)
apply auto
done

subsubsection ‹Enabled Transitions ET›

lemma HPT_ETI: 
    "TS  HPT ST  TS  ET ST"
by (unfold HPT_def MaxNonConflict_def, auto)

lemma finite_ET [simp]:
 "finite (ET ST)"
by (unfold ET_def Image_def EnabledTrans_def, auto)

subsubsection ‹Finite Transition Set›

lemma finite_MaxNonConflict [simp]:
 "MaxNonConflict ST TS  finite TS"
apply (unfold MaxNonConflict_def)
apply auto
apply (subst finite_subset)
apply auto
done

lemma finite_HPT [simp]:
  "TS  HPT ST  finite TS"
by (unfold HPT_def, auto)

subsubsection PUpdate›

lemma finite_Update:
 "finite TS  finite ((λ F. (Rep_pupdate F) (Value ST)) ` (PUpdate (Label TS)))"
by (rule finite_imageI, auto)

lemma finite_PUpdate:
 "TS  HPT S  finite (Expr.PUpdate (Label TS))"
apply auto
done

lemma HPT_ResolveRacing_Some [simp]:
  "TS  HPT S  (SOME u. u  ResolveRacing TS)  ResolveRacing TS"
apply (unfold ResolveRacing_def Let_def)
apply (rule finite_SequentialRacing)
apply auto
done

subsubsection ‹Higher Priority Transitions HPT›

lemma finite_HPT2 [simp]:
  "finite (HPT ST)"
apply (cut_tac ST=ST in finite_ET)
apply (unfold HPT_def MaxNonConflict_def)
apply (subst Collect_subset)
apply (frule finite_Collect_subsets)
apply auto
done

lemma HPT_target_StepConf [simp]: 
  " TS  HPT ST; T  TS   target T  StepConf (HA ST) (Conf ST) TS"
apply (unfold StepConf_def)
apply auto
done

lemma HPT_target_StepConf2 [simp]: 
  " TS  HPT ST; (S,L,T)  TS   T  StepConf (HA ST) (Conf ST) TS"
apply (unfold StepConf_def Target_def Source_def source_def target_def image_def)
apply auto
apply auto
done

subsubsection ‹Delta Transition Set›

lemma ET_Delta: 
  " TS  ET ST; t  TS; source t  States A; A  SAs (HA ST)  t  Delta A"
apply (unfold ET_def EnabledTrans_def)
apply simp
apply (erule subsetCE)
apply auto
apply (rename_tac SA)
apply (case_tac "A = SA")
apply auto
apply (cut_tac HA="HA ST" in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply force
done

lemma ET_Delta_target: 
  " TS  ET ST; t  TS; target t  States A; A  SAs (HA ST)   t  Delta A"
apply (unfold ET_def EnabledTrans_def)
apply simp
apply (erule subsetCE)
apply auto
apply (rename_tac SA)
apply (case_tac "A = SA")
apply auto
apply (cut_tac HA="HA ST" in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply force
done

lemma ET_HADelta:
   "  TS  ET ST; t  TS   t  HADelta (HA ST)"
apply (unfold HADelta_def) 
apply auto
apply (unfold ET_def EnabledTrans_def Image_def)
apply auto
done

lemma HPT_HADelta:
   "  TS  HPT ST; t  TS   t  HADelta (HA ST)"
apply (rule ET_HADelta)
apply (unfold HPT_def MaxNonConflict_def)
apply auto
done

lemma HPT_Delta: 
  " TS  HPT ST; t  TS; source t  States A; A  SAs (HA ST)  t  Delta A"
apply (rule ET_Delta)
apply auto
apply (unfold HPT_def MaxNonConflict_def)
apply fast
done

lemma HPT_Delta_target: 
  " TS  HPT ST; t  TS; target t  States A; A  SAs (HA ST)  t  Delta A"
apply (rule ET_Delta_target)
apply auto
apply (unfold HPT_def MaxNonConflict_def)
apply fast
done

lemma OneTrans_HPT_SA:
  " TS  HPT ST; T  TS; source T  States SA;
     U  TS; source U  States SA; SA  SAs (HA ST)   T = U"
apply (unfold HPT_def MaxNonConflict_def Source_def)
apply auto
apply (erule_tac x=SA in ballE)
apply (case_tac "finite (TS  Delta SA)") 
apply (frule_tac t=T in OneElement_Card)
apply fast
apply (frule_tac t=T and A=SA in ET_Delta)
apply assumption+
apply fast
apply (frule_tac t=U in OneElement_Card)
apply fast
apply (frule_tac t=U and A=SA in ET_Delta)
apply auto
done

lemma OneTrans_HPT_SA2:
  " TS  HPT ST; T  TS; target T  States SA;
     U  TS; target U  States SA; SA  SAs (HA ST)   T = U"
apply (unfold HPT_def MaxNonConflict_def Target_def)
apply auto
apply (erule_tac x=SA in ballE)
apply (case_tac "finite (TS  Delta SA)") 
apply (frule_tac t=T in OneElement_Card)
apply fast
apply (frule_tac t=T and A=SA in ET_Delta_target)
apply assumption+
apply fast
apply (frule_tac t=U in OneElement_Card)
apply fast
apply (frule_tac t=U and A=SA in ET_Delta_target)
apply auto
done

subsubsection ‹Target Transition Set›

lemma ET_Target_HAStates:
    "TS  ET ST  Target TS  HAStates (HA ST)"
apply (unfold HAStates_def Target_def target_def ET_def EnabledTrans_def Action_def Label_def) 
apply (cut_tac HA="HA ST" in Target_SAs_Delta_States)
apply auto
apply (rename_tac Source Trigger Guard Action Update Target)
apply (unfold Target_def)
apply (erule subsetCE)
apply auto
apply (rename_tac SA)
apply (erule subsetCE)
apply auto
apply (unfold image_def)
apply auto
apply (metis target_select)
done

lemma HPT_Target_HAStates:
 "TS  HPT ST  Target TS  HAStates (HA ST)"
apply (rule HPT_ETI [THEN ET_Target_HAStates])
apply assumption
done

lemma HPT_Target_HAStates2 [simp]:
  "TS  HPT ST; S  Target TS  S  HAStates (HA ST)"
apply (cut_tac HPT_Target_HAStates)
apply fast+
done

lemma OneState_HPT_Target:
  " TS  HPT ST; S  Target TS; 
     T  Target TS; S  States SA;
     T  States SA; SA  SAs (HA ST) 
    S = T"
apply (unfold Target_def)
apply (auto dest: OneTrans_HPT_SA2[rotated -1])
done

subsubsection ‹Source Transition Set›

lemma ET_Source_Conf:
  "TS  ET ST  (Source TS)  Conf ST"
apply (unfold Source_def ET_def EnabledTrans_def)
apply auto
done

lemma HPT_Source_Conf [simp]:
  "TS  HPT ST  (Source TS)  Conf ST"
apply (unfold HPT_def MaxNonConflict_def)
apply (rule ET_Source_Conf)
apply auto
done

lemma ET_Source_Target [simp]:
  " SA  SAs (HA ST); TS  ET ST; States SA  Source TS = {}   States SA  Target TS = {}"
apply (unfold ET_def EnabledTrans_def Source_def Target_def)
apply auto
apply (rename_tac Source Trigger Guard Action Update Target)
apply (erule subsetCE)
apply auto
apply (rename_tac SAA)
apply (unfold image_def source_def Int_def)
apply auto
apply (erule_tac x=Source in allE)
apply auto
apply (frule Delta_source_States)
apply (unfold source_def)
apply auto
apply (case_tac "SA=SAA")
apply auto
apply (cut_tac HA="HA ST" in MutuallyDistinct_HA)
apply (unfold MutuallyDistinct_def)
apply (erule_tac x=SA in ballE)
apply (erule_tac x=SAA in ballE)
apply auto
apply (frule Delta_target_States)
apply (unfold target_def)
apply force
done

lemma HPT_Source_Target [simp]:
  " TS  HPT ST; States SA  Source TS = {}; SA  SAs (HA ST)   States SA  Target TS = {}"
apply (unfold HPT_def MaxNonConflict_def)
apply auto
done

lemma ET_target_source:
  " TS  ET ST; t  TS; target t  States A; A  SAs (HA ST)   source t  States A"
apply (frule ET_Delta_target)
apply auto
done

lemma ET_source_target:
  " TS  ET ST; t  TS; source t  States A; A  SAs (HA ST)   target t  States A"
apply (frule ET_Delta)
apply auto
done

lemma HPT_target_source:
  " TS  HPT ST; t  TS; target t  States A; A  SAs (HA ST)  source t  States A"
apply (rule ET_target_source)
apply auto
apply (unfold HPT_def MaxNonConflict_def)
apply fast
done

lemma HPT_source_target:
  " TS  HPT ST; t  TS; source t  States A; A  SAs (HA ST)   target t  States A"
apply (rule ET_source_target)
apply auto
apply (unfold HPT_def MaxNonConflict_def)
apply fast
done

lemma HPT_source_target2 [simp]:
  " TS HPT ST; (s,l,t)  TS; s  States A; A  SAs (HA ST)   t States A" 
apply (cut_tac ST=ST and TS=TS and t="(s,l,t)" in HPT_source_target)
apply auto
done

lemma ChiRel_ChiStar_Source_notmem:
   " TS  HPT ST; (S, T)  ChiRel (HA ST); S  Conf ST; 
      T  ChiStar (HA ST) `` Source TS   
      S  ChiStar (HA ST) `` Source TS"
apply auto
apply (rename_tac U)
apply (simp only: Image_def)
apply auto
apply (erule_tac x=U in ballE)
apply (fast intro: ChiRel_ChiStar_trans)+
done

lemma ChiRel_ChiStar_notmem:
  " TS  HPT ST; (S,T)  ChiRel (HA ST); 
     S  ChiStar (HA ST) `` Source TS   T  Source TS"
using [[hypsubst_thin = true]]
apply (unfold HPT_def MaxNonConflict_def HigherPriority_def restrict_def)
apply auto
apply (rename_tac U)
apply (unfold Source_def image_def)
apply auto
apply (rename_tac SSource STrigger SGuard SAction SUpdate STarget 
                  TSource TTrigger TGuard TAction TUpdate TTarget)
apply (erule_tac x="(SSource, (STrigger, SGuard, SAction, SUpdate), STarget)" in ballE)
apply auto
apply (erule_tac x="(TSource, (TTrigger, TGuard, TAction, TUpdate), TTarget)" in ballE)
apply auto
apply (simp add: ET_HADelta)
apply (case_tac "SSource=S") 
apply auto
apply (frule ChiStar_ChiPlus_noteq)
apply fast
apply (fast intro: ChiRel_ChiPlus_trans)
done

subsubsection StepActEvents›

lemma StepActEvent_empty [simp]:
  "StepActEvent {} = {}"
by (unfold StepActEvent_def, auto)

lemma StepActEvent_HAEvents:
 "TS  HPT ST  StepActEvent TS  HAEvents (HA ST)"
apply (unfold StepActEvent_def image_def)
apply (rule HPT_ETI [THEN TS_EventSet])
apply assumption
done

subsubsection UniqueSucStates›

lemma UniqueSucStates_Status [simp]:
  "UniqueSucStates (SAs (HA ST)) (CompFun (HA ST)) (Conf ST)"
apply (cut_tac Rep_status_select)
apply (unfold status_def Status_def IsConfSet_def)
apply auto
done

subsubsection RootState›

lemma RootExSem_Status [simp]:
  "RootExSem (SAs (HA ST)) (CompFun (HA ST)) (Conf ST)"
apply (cut_tac Rep_status_select)
apply (unfold status_def Status_def IsConfSet_def)
apply auto
done

lemma RootState_HARootState [simp]:
  "(RootState ST)  States (HARoot (HA ST))"
apply (unfold RootState_def)
apply (cut_tac ST=ST in RootExSem_Status)
apply (unfold RootExSem_def HARoot_def HAStates_def)
apply auto
apply (subst some1_equality)
apply auto
done

lemma RootState_Conf [simp]:
  "(RootState ST)  (Conf ST)"
apply (unfold RootState_def)
apply (cut_tac ST=ST in RootExSem_Status)
apply (unfold RootExSem_def HARoot_def HAStates_def)
apply auto
apply (subst some1_equality)
apply auto
done

lemma RootState_notmem_Chi [simp]:
  "S  HAStates (HA ST)  (RootState ST)  Chi (HA ST) S"
by auto

lemma RootState_notmem_Range_ChiRel [simp]:
  "RootState ST  Range (ChiRel (HA ST))"
by auto

lemma RootState_Range_ChiPlus [simp]:
  "RootState ST  Range (ChiPlus (HA ST))" 
by auto

lemma RootState_Range_ChiStar [simp]:
  " x  RootState ST   (x,RootState ST)  (ChiStar (HA ST))" 
by auto

lemma RootState_notmem_ChiRel [simp]:
  "(x,RootState ST)  (ChiRel (HA ST))" 
by (unfold ChiRel_def, auto)

lemma RootState_notmem_ChiRel2 [simp]:
  " S  States (HARoot (HA ST))    (x,S)  (ChiRel (HA ST))" 
by (unfold ChiRel_def, auto)

lemma RootState_Conf_StepConf [simp]:
  " RootState ST  Source TS   RootState ST  StepConf (HA ST) (Conf ST) TS"
apply (unfold StepConf_def)
apply auto
apply (rename_tac S)
apply (case_tac "S=RootState ST")
apply fast
apply auto
apply (rename_tac S)
apply (case_tac "S=RootState ST")
apply fast
apply auto
done

lemma OneRootState_Conf [simp]:
  " S  States (HARoot (HA ST)); S  Conf ST   S = RootState ST"
apply (cut_tac ST=ST in IsConfSet_Status)
apply (unfold IsConfSet_def RootExSem_def)
apply (fold HARoot_def)
apply auto
done

lemma OneRootState_Source:
  " TS  HPT ST; S  Source TS; S  States (HARoot (HA ST))   S = RootState ST"
apply (cut_tac ST=ST and TS=TS in HPT_Source_Conf, assumption)
apply (cut_tac ST=ST in OneRootState_Conf)
apply fast+
done

lemma OneState_HPT_Target_Source:
  " TS  HPT ST; S  States SA; SA  SAs (HA ST);
     States SA  Source TS = {}  
    S  Target TS"
apply (unfold Target_def)
apply auto
apply (unfold Source_def Image_def Int_def)
apply auto
apply (frule HPT_target_source)
apply auto
done

lemma RootState_notmem_Target [simp]:
  " TS  HPT ST; S  States (HARoot (HA ST)); RootState ST  Source TS   S  Target TS" 
apply auto
apply (frule OneState_HPT_Target_Source)
prefer 4
apply fast+
apply simp
apply (unfold Int_def)
apply auto
apply (frule OneRootState_Source)
apply fast+
done

subsubsection ‹Configuration Conf›

lemma Conf_HAStates:
 "Conf ST  HAStates (HA ST)"
apply (cut_tac Rep_status_select)
apply (unfold IsConfSet_def status_def Status_def HAStates_def)
apply fast
done

lemma Conf_HAStates2 [simp]:
  "S  Conf ST  S  HAStates (HA ST)"
apply (cut_tac ST="ST" in Conf_HAStates)
apply fast
done

lemma OneState_Conf [intro]:
  " S  Conf ST; T  Conf ST; S  States SA; T  States SA;
     SA  SAs (HA ST)  T = S"
apply (cut_tac ST=ST in IsConfSet_Status)
apply (unfold IsConfSet_def UniqueSucStates_def)
apply (case_tac "SA = HARoot (HA ST)")
apply (cut_tac ST=ST and S=S in OneRootState_Conf)
apply fast+
apply (simp only:OneRootState_Conf)
apply (erule conjE)+
apply (cut_tac HA="HA ST" in OneAncestor_HA)
apply (unfold OneAncestor_def)
apply (fold HARoot_def)
apply (erule_tac x=SA in ballE)
apply (drule ex1_implies_ex)
apply (erule exE)
apply (rename_tac U)
apply (erule_tac x=U in ballE)
apply (erule_tac x=SA in ballE)
apply (case_tac "U  Conf ST")
apply simp
apply safe
apply fast+
apply simp
apply fast
done

lemma OneState_HPT_SA:
  " TS  HPT ST; S  Source TS; T  Source TS;
     S  States SA; T  States SA; 
     SA  SAs (HA ST)   S = T"
apply (rule OneState_Conf)
apply auto
apply (frule HPT_Source_Conf, fast)+
done

lemma HPT_SAStates_Target_Source:
   "TS  HPT ST; A  SAs (HA ST); S  States A; T  States A; S  Conf ST;
     T  Target TS   S  Source TS"
apply (case_tac "States A  Source TS ={}")
apply (frule OneState_HPT_Target_Source)
apply fast
back
apply simp+
apply auto
apply (rename_tac U)
apply (cut_tac ST=ST in HPT_Source_Conf)
apply fast
apply (frule_tac S=S and T=U in OneState_Conf)
apply fast+
done

lemma HPT_Conf_Target_Source:
   "TS  HPT ST; S  Conf ST;
     S  Target TS   S  Source TS"
apply (frule Conf_HAStates2)
apply (unfold HAStates_def)
apply auto
apply (simp only:HPT_SAStates_Target_Source)
done

lemma Conf_SA:
  "S  Conf ST   A  SAs (HA ST). S  States A"
apply (cut_tac ST=ST in IsConfSet_Status)
apply (unfold IsConfSet_def)
apply fast
done

lemma HPT_Source_HAStates [simp]:
   " TS  HPT ST; S  Source TS   S  HAStates (HA ST)"
apply (frule HPT_Source_Conf)
apply (rule Conf_HAStates2)
apply fast
done

lemma Conf_Ancestor: 
  " S  Conf ST;  A  the (CompFun (HA ST) S)   ∃! T  States A. T  Conf ST"
apply (cut_tac ST=ST in IsConfSet_Status)
apply (unfold IsConfSet_def UniqueSucStates_def)
apply safe
apply (erule_tac x=S in ballE)
prefer 2
apply blast
apply (erule_tac x=A in ballE)
prefer 2
apply fast
apply simp
apply (fast intro: HAStates_CompFun_SAs_mem Conf_HAStates2)+
done


lemma Conf_ChiRel: 
   " (S,T)  ChiRel (HA ST); T  Conf ST   S  Conf ST"
apply (unfold ChiRel_def Chi_def restrict_def)
apply simp
apply safe
apply simp
apply safe
apply (rename_tac SA)
apply (unfold HAStates_def)
apply simp
apply safe
apply (rename_tac U)
apply (cut_tac ST=ST in UniqueSucStates_Status) 
apply (unfold UniqueSucStates_def)
apply (erule_tac x=S in ballE)
apply (erule_tac x=SA in ballE)
apply auto
apply (case_tac "S  Conf ST")
apply simp+
done

lemma Conf_ChiPlus:
   " (T,S)  ChiPlus (HA ST)    S  Conf ST  T  Conf ST"
apply (unfold ChiPlus_def)
apply (rule_tac a="T" and b="S" and r="(ChiRel (HA ST))" in trancl_induct)
apply (fast intro: Conf_ChiRel)+
done

lemma HPT_Conf_Target_Source_ChiPlus:
  " TS  HPT ST; S  Conf ST; S  ChiPlus (HA ST) `` Target TS 
      S  ChiStar (HA ST) `` Source TS"
apply auto
apply (rename_tac T)
apply (simp add: Image_def)
apply (frule HPT_Target_HAStates2) 
apply fast
apply (unfold HAStates_def)
apply auto
apply (rename_tac SA)
apply (case_tac "States SA  Source TS = {}")
apply (simp only:OneState_HPT_Target_Source)
apply auto
apply (rename_tac U)
apply (erule_tac x=U in ballE)
apply auto
apply (case_tac "U=T")
apply auto
apply (frule Conf_ChiPlus)
apply simp
apply (frule HPT_Conf_Target_Source)
apply fast
back
apply fast
apply (simp add:OneState_HPT_SA)
done

lemma OneState_HPT_Target_ChiRel:
   " TS  HPT ST; (U,T)  ChiRel (HA ST);
      U  Target TS; A  SAs (HA ST); T  States A;
      S  States A   S  Target TS"
using [[hypsubst_thin = true]]
apply auto
apply (unfold HigherPriority_def restrict_def HPT_def MaxNonConflict_def Target_def)
apply auto
apply (rename_tac SSource STrigger SGuard SAction SUpdate STarget 
                  TSource TTrigger TGuard TAction TUpdate TTarget)
apply (cut_tac t="(TSource, (TTrigger, TGuard, TAction, TUpdate), TTarget)" and TS=TS and ST=ST and A=A in ET_target_source)
apply assumption+
apply simp
apply assumption
apply (frule ChiRel_HAStates)
apply (unfold HAStates_def)
apply safe
apply (cut_tac t="(SSource, (STrigger, SGuard, SAction, SUpdate), STarget)" and A=x and ST=ST and TS=TS in ET_target_source)
apply assumption+ 
apply simp
apply assumption
apply simp
apply (erule_tac x="(SSource, (STrigger, SGuard, SAction, SUpdate), STarget)" in ballE)
apply simp
apply (erule_tac x="(TSource, (TTrigger, TGuard, TAction, TUpdate), TTarget)" in ballE)
apply (simp add: ET_HADelta)
apply (cut_tac A="HA ST" and S=STarget and T=T and U=TSource in ChiRel_SA_OneAncestor)
apply fast+
apply (frule ET_Source_Conf)
apply (unfold Source_def image_def)
apply (case_tac "SSource Conf ST") 
prefer 2
apply (erule subsetCE)
back
apply fast
back
apply simp
apply (case_tac "TSource Conf ST") 
prefer 2
apply (erule subsetCE)
back
apply fast
apply simp
apply (case_tac "STarget=SSource") 
apply simp
apply (fast intro:Conf_ChiRel)+ 
done

lemma OneState_HPT_Target_ChiPlus [rule_format]:
   " TS  HPT ST; (U,T)  ChiPlus (HA ST);
      S  Target TS; A  SAs (HA ST); 
      S  States A   T  States A  U  Target TS"
using [[hypsubst_thin = true]]
apply (unfold ChiPlus_def)
apply (rule_tac a="U" and b="T" and r="(ChiRel (HA ST))" in converse_trancl_induct)
apply auto
apply (simp only:OneState_HPT_Target_ChiRel)
apply (rename_tac V W)
apply (fold ChiPlus_def)
apply (unfold HPT_def MaxNonConflict_def Target_def HigherPriority_def restrict_def)
apply auto
apply (rename_tac SSource STrigger SGuard SAction SUpdate STarget 
                  TSource TTrigger TGuard TAction TUpdate TTarget)
apply (cut_tac t="(SSource, (STrigger, SGuard, SAction, SUpdate), STarget)" and ST=ST and TS=TS and A=A in ET_target_source)
apply assumption+ 
apply simp
apply assumption
apply simp
apply (frule ChiRel_HAStates)
apply (unfold HAStates_def)
apply safe
apply (cut_tac t="(TSource, (TTrigger, TGuard, TAction, TUpdate), TTarget)" and A=x and TS=TS and ST=ST in ET_target_source)
apply assumption+ 
apply simp
apply assumption
apply simp
apply (erule_tac x="(TSource, (TTrigger, TGuard, TAction, TUpdate), TTarget)" in ballE)
apply simp
apply (erule_tac x="(SSource, (STrigger, SGuard, SAction, SUpdate), STarget)" in ballE)
apply (simp add: ET_HADelta)
apply (cut_tac A="HA ST" and S=TTarget and T=T and U=SSource in ChiPlus_SA_OneAncestor)
apply (fast intro: ChiRel_ChiPlus_trans2)
apply fast+
apply (frule ET_Source_Conf)
apply (unfold Source_def image_def)
apply (case_tac "SSource Conf ST") 
prefer 2
apply (erule subsetCE)
back
apply fast
apply simp
apply (case_tac "TSource Conf ST") 
prefer 2
apply (erule subsetCE)
back
apply fast
back
apply simp
apply (case_tac "TTarget=SSource") 
apply simp
apply (frule_tac T=TTarget and S=SSource in Conf_ChiPlus)
apply simp
apply (frule_tac T=TSource and S=TTarget in OneState_Conf)
apply fast+
done

subsubsection RootExSem›

lemma RootExSem_StepConf: 
   " TS  HPT ST   
      RootExSem (SAs (HA ST)) (CompFun (HA ST)) (StepConf (HA ST) (Conf ST) TS)"
apply (unfold RootExSem_def)
apply (fold HARoot_def)
apply auto
apply (case_tac "RootState ST  Source TS") 
apply (rule_tac x="RootState ST" in exI)
apply simp
apply simp
apply (unfold Source_def image_def)
apply simp
apply (erule bexE)
apply (rename_tac T)
apply (rule_tac x="target T" in exI)
apply simp
apply (rule HPT_source_target)
apply auto
apply (rename_tac S T)
apply (case_tac "S  Conf ST") 
apply (case_tac "T  Conf ST")
apply (frule OneRootState_Conf) 
apply auto
apply (frule OneRootState_Conf) 
apply auto
apply (frule OneRootState_Conf) 
apply auto
apply (case_tac "RootState ST  Source TS")
apply (case_tac "T  Source TS")
apply (frule HPT_Source_Conf)
apply fast
apply (unfold StepConf_def)
apply auto
apply (frule OneState_HPT_Target)
apply (frule_tac SA="HARoot (HA ST)" and TS=TS and S=T and T="RootState ST" in OneState_HPT_Target)
apply fast+
apply simp+
apply (frule trancl_Int_mem, fold ChiPlus_def, force)+
prefer 2
apply (frule OneState_HPT_Target)
apply fast+
back
apply simp+
apply (case_tac "RootState ST  Source TS") 
apply (case_tac "T = RootState ST")
apply auto
apply (frule trancl_Int_mem, fold ChiPlus_def, force)+
done

subsubsection StepConf›

lemma Target_StepConf:
   "S  Target TS  S  StepConf (HA ST) (Conf ST) TS"
apply (unfold StepConf_def)
apply auto
done

lemma Target_ChiRel_HAInit_StepConf:
   " S  Target TS; (S,T)  ChiRel A; 
      T  HAInitStates A   T  StepConf A C TS" 
apply (unfold StepConf_def)
apply auto
done

lemma StepConf_HAStates: 
 "TS  HPT ST  StepConf (HA ST) (Conf ST) TS  HAStates (HA ST)"
apply (unfold StepConf_def)
apply auto
apply (frule tranclD2)
apply auto
done

lemma RootState_Conf_StepConf2 [simp]:
  " source T = RootState ST; T  TS   target T  StepConf (HA ST) (Conf ST) TS"
apply (unfold StepConf_def)
apply auto
done

lemma HPT_StepConf_HAStates [simp]: 
   " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS   S  HAStates (HA ST)"
apply (unfold StepConf_def)
apply auto
apply (frule tranclD2)
apply auto
done

lemma StepConf_Target_HAInitStates: 
  " S  StepConf (HA ST) (Conf ST) TS; S  Target TS; S  Conf ST  S  HAInitStates (HA ST)"
apply (unfold StepConf_def)
apply auto
apply (frule tranclD2)
apply auto
done

lemma InitSucState_StepConf:
   " TS  HPT ST; S  Target TS; A  the (CompFun (HA ST) S);
      S  Conf ST; S  StepConf (HA ST) (Conf ST) TS  
      InitState A  StepConf (HA ST) (Conf ST) TS"
apply (frule StepConf_HAStates [THEN subsetD, THEN CompFun_HAInitStates_HAStates])
apply fast+
apply (subst (asm) StepConf_def)
apply safe
apply (unfold StepConf_def)
apply (fast intro: HAInitStates_InitState_trancl)
apply (frule trancl_Int_mem, fold ChiPlus_def)
apply (fast intro:ChiPlus_HAStates_Right [THEN HAInitStates_InitState_trancl2]) 
done

lemma InitSucState_Target_StepConf:
   " TS  HPT ST; S  Target TS; A  the (CompFun (HA ST) S) 
      InitState A  StepConf (HA ST) (Conf ST) TS"
apply (frule HPT_Target_HAStates2 [THEN CompFun_HAInitStates_HAStates])
apply fast+
apply (frule HPT_Target_HAStates2 [THEN CompFun_ChiRel])
apply (fast intro:InitState_States)+
apply (unfold StepConf_def)
apply auto
done

lemma InitSucState_Conf_StepConf:
  " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS; 
     S  Target TS; A  the (CompFun (HA ST) S);
     S  Conf ST; S  ChiStar (HA ST) `` (Source TS)   
     InitState A  StepConf (HA ST) (Conf ST) TS"
apply (frule Conf_HAStates2 [THEN CompFun_HAInitStates_HAStates])
apply fast
apply (subst (asm) StepConf_def)
apply safe
apply fast
apply (unfold StepConf_def)
apply (fast intro:HAInitStates_InitState_trancl)
apply (rename_tac T U V)
apply (frule trancl_Int_mem, fold ChiPlus_def, safe)
apply (subst (asm) Image_def, safe)
apply (rule_tac x=U in bexI)
apply (simp only: ChiPlus_HAStates_Right [THEN HAInitStates_InitState_trancl2])
apply fast
apply (subst (asm) Image_def, safe)
apply (rule_tac x=U in bexI)
apply (simp only: ChiPlus_HAStates_Right [THEN HAInitStates_InitState_trancl2])
apply fast
done

lemma SucState_Conf_StepConf:
  " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS;
     S  Target TS; A  the (CompFun (HA ST) S);
     S  Conf ST; States A  ChiStar (HA ST) `` (Source TS) = {}   
      x. x  States A  x  StepConf (HA ST) (Conf ST) TS" 
apply (unfold StepConf_def)
apply (cut_tac ST=ST in UniqueSucStates_Status)
apply (unfold UniqueSucStates_def)
apply (cut_tac ST=ST in Conf_HAStates2)
apply fast
apply (fold HAStates_def)
apply (erule_tac x=S in ballE)
apply (erule_tac x=A in ballE)
apply simp
apply fast+ 
done

lemma SucState_Conf_Source_StepConf:
  " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS; 
     S  Target TS; A  the (CompFun (HA ST) S);
     S  Conf ST; States A  ChiStar (HA ST) `` (Source TS)  {}; 
     S  ChiStar (HA ST) `` (Source TS)  
      x. x  States A  x  StepConf (HA ST) (Conf ST) TS"
apply safe
apply (rename_tac T U)
apply (frule Conf_HAStates2 [THEN CompFun_ChiRel])
apply fast+
apply simp
apply (case_tac "U=T")
apply simp
apply (rotate_tac -5)
apply (simp only:Source_def Target_def image_def)
apply safe
apply (rename_tac Source Trigger Guard Action Update Target)
apply (erule_tac x=Target in allE)
apply simp
apply (frule HPT_source_target2)
apply fast+
apply (rule HAStates_CompFun_SAs_mem)
apply (rule Conf_HAStates2)
apply fast+
apply (frule ChiStar_ChiPlus_noteq)
apply fast
apply (case_tac "U=S")
apply (fast intro:ChiStar_Self ChiRel_ChiPlus_OneAncestor ChiPlus_ChiStar)+
done

lemma SucState_StepConf:
  " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS; 
     A  the (CompFun (HA ST) S)   
      x. x  States A  x  StepConf (HA ST) (Conf ST) TS" 
apply (case_tac "S  Target TS")
apply (fast intro: InitSucState_Target_StepConf InitState_States)
apply (case_tac "S  Conf ST")
prefer 2
apply (fast intro: InitSucState_StepConf InitState_States)
apply (case_tac "S  ChiStar (HA ST) `` (Source TS)")
apply (fast intro: InitSucState_Conf_StepConf InitState_States)
apply (case_tac "States A  ChiStar (HA ST) `` (Source TS) = {}")
apply (fast intro: SucState_Conf_StepConf SucState_Conf_Source_StepConf)+
done

subsubsection StepStatus›

lemma StepStatus_expand:
   "Abs_status (HA ST, StepConf (HA ST) (Conf ST) TS, 
                StepActEvent TS, U !!! (Value ST)) 
    = (StepStatus ST TS U)"
apply (unfold StepStatus_def Let_def)
apply (subst Rep_status_tuple)
apply auto
done

lemma UniqueSucState_Conf_Source_StepConf:
   " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS; A  SAs (HA ST);
      A  the (CompFun (HA ST) S); T  States A; U  States A;
      T  StepConf (HA ST) (Conf ST) TS; T  U; U  Conf ST   
      U  ChiStar (HA ST) `` Source TS"
apply (frule_tac ?S2.0=T in StepConf_HAStates [THEN subsetD, THEN CompFun_ChiRel])
apply fast+
apply (frule_tac ?S2.0=U in StepConf_HAStates [THEN subsetD, THEN CompFun_ChiRel])
apply fast+
apply (frule_tac S=S and T=U in Conf_ChiRel, fast)
apply (case_tac "S  ChiStar (HA ST) `` Source TS")
apply (fast intro: ChiRel_ChiStar_trans)
apply (case_tac "U  Source TS")
apply force
apply (unfold StepConf_def)
apply simp
apply safe
apply (fast intro: HPT_SAStates_Target_Source)+
apply (rename_tac V)
apply (case_tac "V=S")
apply (frule_tac S=S in HPT_Conf_Target_Source, fast+)
apply (fast intro: ChiStar_Image ChiRel_OneAncestor)+
apply (rename_tac V W) 
apply (frule trancl_Int_mem, fold ChiPlus_def, safe)
apply (cut_tac ST=ST and S=S in HPT_Conf_Target_Source_ChiPlus)
apply fast+
apply (simp only:Image_def, safe)
apply (case_tac "(V, T)  ChiRel (HA ST)")
apply (frule_tac S=V and T=T in ChiPlus_ChiRel_Ex)
apply (fast, safe)
apply (rename_tac X)
apply (case_tac "X=S")
apply (rule_tac x=W in bexI)
prefer 4
apply (case_tac "V=S")
prefer 2
apply simp
apply (fast intro: ChiPlus_ChiRel ChiRel_ChiPlus_trans2 ChiRel_OneAncestor)+
done

lemma UniqueSucState_Target_StepConf:
   " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS; A  SAs (HA ST);
      A  the (CompFun (HA ST) S); T  States A; U  States A;
      T  StepConf (HA ST) (Conf ST) TS; T  U   
      U  Target TS"
apply auto
apply (frule_tac ST=ST in Target_StepConf)
apply (subst (asm) (2) StepConf_def)
apply simp
apply safe
apply (cut_tac TS=TS and ST=ST and S=S and T=U in UniqueSucState_Conf_Source_StepConf)
apply fast+
apply (simp add: OneState_HPT_Target)
apply (simp only:OneState_HPT_Target_ChiRel)
apply (rename_tac V W)
apply (frule_tac U=W and S=V and T=T in ChiRel_ChiPlus_trans2)
apply (frule trancl_Int_mem, fold ChiPlus_def, force)
apply (simp only:OneState_HPT_Target_ChiPlus)
done

lemma UniqueSucState_Target_ChiRel_StepConf: 
   " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS; A  SAs (HA ST);
      A  the (CompFun (HA ST) S); T  States A; U  States A;
      T  StepConf (HA ST) (Conf ST) TS; T  U; (V,U)  ChiRel (HA ST); 
      U  HAInitStates (HA ST) 
     V  Target TS" 
apply auto
apply (frule_tac A="HA ST" and C="Conf ST" in Target_ChiRel_HAInit_StepConf)
apply fast+
apply (subst (asm) (2) StepConf_def, safe)
apply (fast intro:UniqueSucState_Conf_Source_StepConf) 
apply (simp only:OneState_HPT_Target_ChiRel) 
apply (fast intro:OneHAInitState_SAStates)
apply (frule trancl_Int_mem, fold ChiPlus_def)
apply (fast intro:OneHAInitState_SAStates) 
done

lemma UniqueSucState_Target_ChiPlus_StepConf [rule_format]:
  " TS  HPT ST; (S,T)  ChiRel (HA ST); (S,U)  ChiRel (HA ST); 
     V  Target TS; (V,W)  ChiRel (HA ST); T  ChiStar (HA ST) `` Source TS;
     (W,U)  (ChiRel (HA ST)  HAInitStates (HA ST) × HAInitStates (HA ST))+;
     T  Conf ST   (S,U)  ChiRel (HA ST)  T=U"    
apply (frule_tac S=S and T=T in Conf_ChiRel)
apply fast
apply (rule_tac a="W" and b="U" and r="ChiRel (HA ST)  HAInitStates (HA ST) × HAInitStates (HA ST)" in trancl_induct)
apply safe
apply (rename_tac X)
apply (case_tac "W=S")
apply simp
prefer 2
apply (simp add: ChiRel_OneAncestor)
prefer 2
apply (rename_tac X Y)
apply (case_tac "X=S")
apply simp
prefer 2
apply (simp add: ChiRel_OneAncestor)
prefer 2
apply (frule_tac a=V in ChiRel_HAStates)
apply (unfold HAStates_def)
apply (simp,safe)
apply (rename_tac Y)
apply (case_tac "States Y  Source TS = {}")
apply (simp add:OneState_HPT_Target_Source)
apply (subst (asm) Int_def, safe)
apply (rename_tac Z)
apply (frule_tac S=V and T=S in Conf_ChiRel)
apply fast
apply (frule HPT_Conf_Target_Source)
prefer 2
apply fast
apply fast
apply (frule_tac S=Z and T=V in  OneState_HPT_SA)
apply fast+
apply simp
apply (fast intro: ChiPlus_ChiRel ChiRel_ChiPlus_trans ChiPlus_ChiStar)
apply (simp add: Image_def)
apply (frule trancl_Int_mem, fold ChiPlus_def, simp, safe)
back
apply (frule_tac T=W and S=S in Conf_ChiPlus)
apply simp
apply (frule_tac S=V and T=W in Conf_ChiRel)
apply fast
apply (frule_tac a=V in ChiRel_HAStates)
apply (unfold HAStates_def)
apply (simp, safe)
apply (rename_tac Z)
apply (case_tac "States Z  Source TS = {}")
apply (simp add:OneState_HPT_Target_Source)
apply (subst (asm) Int_def, safe)
apply (frule_tac S=V in HPT_Conf_Target_Source)
apply fast+
apply (rename_tac P)
apply (frule_tac S=P and T=V in  OneState_HPT_SA)
apply fast+
apply (frule_tac U=V and S=W and T=S in ChiRel_ChiPlus_trans2)
apply fast+
apply (fast intro: ChiPlus_ChiRel ChiRel_ChiPlus_trans ChiPlus_ChiStar)
apply (case_tac "T=S")
apply (simp add: ChiRel_OneAncestor)+
done

lemma UniqueSucStates_SAStates_StepConf:
   " TS  HPT ST; S  StepConf (HA ST) (Conf ST) TS; A  SAs (HA ST);
      A  the (CompFun (HA ST) S); T  States A; U  States A;
      T  StepConf (HA ST) (Conf ST) TS; T  U   
      U  StepConf (HA ST) (Conf ST) TS"
apply (subst StepConf_def)
apply (simp, safe)
apply (rule UniqueSucState_Conf_Source_StepConf)
apply fast+
apply (frule_tac U=U in UniqueSucState_Target_StepConf)
apply fast+
apply (frule_tac U=U in UniqueSucState_Target_ChiRel_StepConf