# Theory Contrib

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

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
"λx∈A. 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 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 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 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 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"

lemmas PartI = Part_eqI [OF _ refl]

lemma PartE [elim!]: "⟦ a ∈ Part A h;  !!z. ⟦ a ∈ A;  a=h(z) ⟧ ⟹ P ⟧ ⟹ P"

lemma Part_subset: "Part A h ⊆ A"

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"

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
*)

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 (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 (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
*)

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
*)

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
*)

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
*)

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
*)

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 ==
(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 (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 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 (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)
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 (cut_tac A=A in ChiPlus_HAStates)
apply (unfold HAStates_def)
apply auto
apply (frule ChiPlus_ChiRel_NoCycle_2)
apply fast
apply (frule ChiPlus_ChiRel_NoCycle_1)
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 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 safe
apply (erule_tac x=SA in ballE)
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 (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 (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 (rename_tac V W)
apply (fold ChiPlus_def)
apply (case_tac "V=T")
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
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)
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
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)
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")
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
*)

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
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

" ⟦ TS ⊆ ET ST; t ∈ TS ⟧ ⟹ t ∈ HADelta (HA ST)"
apply auto
apply (unfold ET_def EnabledTrans_def Image_def)
apply auto
done

" ⟦ TS ∈ HPT ST; t ∈ TS ⟧ ⟹ t ∈ HADelta (HA ST)"
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 (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 (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
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 (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 (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 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
prefer 2
apply (rename_tac X Y)
apply (case_tac "X=S")
apply simp
prefer 2
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 (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 (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 (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")
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