Theory HA

(*  Title:      statecharts/HA/HA.thy

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

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

subsection ‹Definitions›

(* unique root automaton *)

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

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

(* mutually distinct state spaces *)

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

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

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

(* composition function contains no cycles *)

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

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

subsubsection ‹Well-formedness for the syntax of HA›

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

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

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

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

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

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

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

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

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

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

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

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

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

subsubsection ‹State successor function›

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

(* direct state successor relation ChiRel *)

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

(* indirect state successor relation ChiPlus *)

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

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

(* priority on transitions that are successors *)

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

subsubsection ‹Configurations›

(* initial configuration *)

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

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

(* step on configurations *)

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

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

subsection ‹Lemmas›

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

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

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

subsubsection ‹‹HAStates››

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

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

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

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

subsubsection ‹‹HAEvents››

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

subsubsection ‹‹NoCycles››

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

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

subsubsection ‹‹OneAncestor››

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

subsubsection ‹‹MutuallyDistinct››

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

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

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

lemma MutuallyDistinct_Union:
  "⟦ MutuallyDistinct A; MutuallyDistinct B;
  (⋃ C ∈ A. States C) ∩ (⋃ C ∈ B. States C) = {} ⟧
  ⟹ MutuallyDistinct (A ∪ B)"
by (unfold MutuallyDistinct_def, safe, blast+)

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

subsubsection ‹‹RootEx››

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

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

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

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

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

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

subsubsection ‹‹HARoot››

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

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

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

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

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

subsubsection ‹‹CompFun››

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

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

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

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

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

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

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

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

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

subsubsection ‹‹SAs››

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

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

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

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

subsubsection ‹‹HAInitState››

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

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

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

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

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

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


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

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

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

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

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

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

subsubsection ‹‹Chi››

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

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

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

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

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

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

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

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

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

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

subsubsection ‹‹ChiRel››

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

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

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

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

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

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

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

lemma ChiRel_OneAncestor_notmem:
  "⟦ S ≠ T; (S,U) ∈ ChiRel A⟧ ⟹ (T,U) ∉ ChiRel A"
apply (unfold ChiRel_def)
apply auto
apply (simp only: Chi_range_disjoint)
done

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

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

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

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

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

lemma SAStates_ChiRel:
  "⟦ S ∈ States SA; T ∈ States SA;
     SA ∈ SAs A ⟧ ⟹ (S,T) ∉ (ChiRel A)"
by (unfold ChiRel_def, auto)

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

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

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

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

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

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

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

subsubsection ‹‹ChiPlus››

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

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

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

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

lemma ChiPlus_OneAncestor: 
  "⟦ S ∈ HAStates A; S ∉ States (HARoot A) ⟧ ⟹ 
     ∃ T. (T,S) ∈ ChiPlus A"
apply (unfold ChiPlus_def)
apply (frule ChiRel_OneAncestor2)
apply auto
done

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma ChiPlus_ChiRel_Ex2 [rule_format]:
  "⟦ (S,T) ∈ ChiPlus A ⟧ ⟹ (S,T) ∉ ChiRel A ⟶ 
    (∃ U. (S,U) ∈ ChiRel A ∧ (U,T) ∈ ChiPlus A)"
apply (unfold ChiPlus_def)
apply (rule_tac a="S" and b="T" and r="(ChiRel A)" in converse_trancl_induct)
apply auto
done

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

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

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

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

(* TO DO *)

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

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

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

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

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

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

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

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

subsubsection ‹‹ChiStar››

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

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

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

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

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

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

subsubsection ‹‹InitConf››

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

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

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

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

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

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

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

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

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

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

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

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

subsubsection ‹‹StepConf››

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

end