SSL HAOps.thy

(*  Title:      statecharts/HA/HAOps.thy
    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹Constructing Hierarchical Automata›
theory HAOps
imports HA
begin

subsection "Constructing a Composition Function for a PseudoHA"

definition
  EmptyMap :: "'s set => ('s ⇀ (('s,'e,'d)seqauto) set)" where
  "EmptyMap S = (λ a . if a ∈ S then Some {} else None)"

lemma EmptyMap_dom [simp]:
  "dom (EmptyMap S) = S"
by (unfold dom_def EmptyMap_def,auto)

lemma EmptyMap_ran [simp]:
   "S ≠ {} ==> ran (EmptyMap S) = {{}}"
by (unfold ran_def EmptyMap_def, auto)

lemma EmptyMap_the [simp]:
   "x ∈ S ==> the ((EmptyMap S) x) = {}"
by (unfold ran_def EmptyMap_def, auto)

lemma EmptyMap_ran_override:
  "[ S ≠ {}; (S ∩ (dom G)) = {} ] ==>
  ran (G ++ EmptyMap S) = insert {} (ran G)"
apply (subst ran_override)
apply (simp add: Int_commute)
apply simp
done

lemma EmptyMap_Union_ran_override:
 "[ S ≠ {};
    S ∩ dom G = {} ] ==>
  (Union (ran (G ++ (EmptyMap S)))) = (Union (ran G))"
apply (subst EmptyMap_ran_override)
apply auto
done

lemma EmptyMap_Union_ran_override2:
 "[ S ≠ {}; S ∩ dom G1 = {};
    dom G1 ∩ dom G2 = {} ] ==>
   ∪ (ran (G1 ++ EmptyMap S ++ G2)) = (∪ (ran G1 ∪ ran G2))"
apply (unfold Union_eq UNION_eq EmptyMap_def Int_def ran_def)
apply (simp add: map_add_Some_iff)
apply (unfold dom_def)
apply simp
apply (rule equalityI)
apply (rule subsetI)
apply simp
apply fast
apply (rule subsetI)
apply (rename_tac t)
apply simp
apply (erule bexE)
apply (rename_tac U)
apply simp
apply (erule disjE)
apply (erule exE)
apply (rename_tac v)
apply (rule_tac x=U in exI)
apply simp
apply (rule_tac x=v in exI)
apply auto
done

lemma EmptyMap_Root [simp]:
 "Root {SA} (EmptyMap (States SA)) = SA"
by (unfold Root_def, auto)

lemma EmptyMap_RootEx [simp]:
  "RootEx {SA} (EmptyMap (States SA))"
by (unfold RootEx_def, auto)

lemma EmptyMap_OneAncestor [simp]:
 "OneAncestor {SA} (EmptyMap (States SA))"
by (unfold OneAncestor_def, auto)

lemma EmptyMap_NoCycles [simp]:
  "NoCycles {SA} (EmptyMap (States SA))"
by (unfold NoCycles_def EmptyMap_def , auto)

lemma EmptyMap_IsCompFun [simp]:
 "IsCompFun {SA} (EmptyMap (States SA))"
by (unfold IsCompFun_def, auto)

lemma EmptyMap_hierauto [simp]:
 "(D,{SA}, SAEvents SA, EmptyMap (States SA)) ∈ hierauto"
by (unfold hierauto_def HierAuto_def, auto)

subsection "Extending a Composition Function by a SA"

definition
  FAddSA :: "[('s ⇀ (('s,'e,'d)seqauto) set), 's * ('s,'e,'d)seqauto]
             => ('s ⇀ (('s,'e,'d)seqauto) set)"
           (‹(_ [f+]/ _)› [10,11]10) where
  "FAddSA G SSA = (let (S,SA) = SSA
                   in
                     (if ((S ∈ dom G) ∧ (S ∉ States SA)) then
                        (G ++ (Map.empty(S ↦ (insert SA (the (G S)))))
                         ++ EmptyMap (States SA))
                      else G))"

lemma FAddSA_dom [simp]:
 "(S ∉ (dom (A::('a => ('a,'c,'d)seqauto set option)))) ==>
   ((A [f+] (S,(SA::('a,'c,'d)seqauto))) = A)"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_States [simp]:
 "(S ∈ (States (SA::('a,'c,'d)seqauto))) ==>
   (((A::('a => ('a,'c,'d)seqauto set option)) [f+] (S,SA)) = A)"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_dom_insert [simp]:
 "[ S ∈ (dom A); S ∉ States SA ] ==>
   (((A [f+] (S,SA)) S) = Some (insert SA (the (A S))))"
by (unfold FAddSA_def Let_def restrict_def, auto)

lemma FAddSA_States_neq [simp]:
 "[ S' ∉ States (SA::('a,'c,'d)seqauto); S ≠ S' ] ==>
  ((((A::('a => ('a,'c,'d)seqauto set option)) [f+] (S,SA)) S') = (A S'))"
apply (case_tac "S ∈ dom A")
apply (case_tac "S ∈ States SA")
apply auto
apply (case_tac "S' ∈ dom A")
apply (unfold FAddSA_def Let_def)
apply auto
apply (simp add: dom_None)
done

lemma FAddSA_dom_emptyset [simp]:
 "[ S ∈ (dom A); S ∉ States SA; S' ∈ States (SA::('a,'c,'d)seqauto) ] ==>
    ((((A::('a => ('a,'c,'d)seqauto set option))) [f+] (S,SA)) S') = (Some {})"
apply (unfold FAddSA_def Let_def)
apply auto
apply (unfold EmptyMap_def)
apply auto
done

lemma FAddSA_dom_dom_States [simp]:
  "[ S ∈ (dom F); S ∉ States SA ] ==>
    (dom ((F::('a ⇀ (('a,'b,'d)seqauto) set)) [f+] (S, SA))) =
    ((dom F) ∪ (States (SA::('a,'b,'d)seqauto)))"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_dom_dom [simp]:
  "S ∉ (dom F) ==>
   (dom ((F::('a ⇀ (('a,'b,'d)seqauto) set)) [f+]
       (S,(SA::('a,'b,'d)seqauto)))) = (dom F)"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_States_dom [simp]:
  "S ∈ (States SA) ==>
   (dom ((F::('a ⇀ (('a,'b,'d)seqauto) set)) [f+]
        (S,(SA::('a,'b,'d)seqauto)))) = (dom F)"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_dom_insert_dom_disjunct [simp]:
   "[ S ∈ dom G; States SA ∩ dom G = {} ] ==> ((G [f+] (S,SA)) S) = Some (insert SA (the (G S)))"
apply (rule  FAddSA_dom_insert)
apply auto
done

lemma FAddSA_Union_ran:
 "[ S ∈ dom G; (States SA) ∩ (dom G) = {} ] ==>
   (∪ (ran (G [f+] (S,SA)))) = (insert SA (∪ (ran G)))"
apply (unfold FAddSA_def Let_def)
apply simp
apply (rule conjI)
prefer 2
apply (rule impI)
apply (unfold Int_def)
apply simp
apply (fold Int_def)
apply (rule impI)
apply (subst EmptyMap_Union_ran_override)
apply auto
done

lemma FAddSA_Union_ran2:
 "[ S ∈ dom G1; (States SA) ∩ (dom G1) = {}; (dom G1 ∩ dom G2) = {} ] ==>
   (∪ (ran ((G1 [f+] (S,SA)) ++ G2))) = (insert SA (∪ ((ran G1) ∪ (ran G2))))"
apply (unfold FAddSA_def Let_def)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (rule impI)
apply (subst EmptyMap_Union_ran_override2)
apply simp
apply simp
apply simp
apply fast
apply (subst Union_Un_distrib)
apply (subst Union_ran_override2)
apply auto
done

lemma FAddSA_ran:
  "[ ∀ T ∈ dom G . T ≠ S ⟶ (the (G T) ∩ the (G S)) = {};
     S ∈ dom G; (States SA) ∩ (dom G) = {} ] ==>
    ran (G [f+] (S,SA)) = insert {} (insert (insert SA (the (G S))) (ran G - {the (G S)}))"
apply (unfold FAddSA_def Let_def)
apply simp
apply (rule conjI)
apply (rule impI)+
prefer 2
apply fast
apply (simp add: EmptyMap_ran_override)
apply (unfold ran_def)
apply auto
apply (rename_tac Y X a xa xb)
apply (erule_tac x=a in allE)
apply simp
apply (erule_tac x=a in allE)
apply simp
done

lemma FAddSA_RootEx_def: 
  "[ S ∈ dom G; (States SA) ∩ (dom G) = {} ] ==>
    RootEx F (G [f+] (S,SA)) = (∃! A . A ∈ F ∧ A ∉ insert SA (∪ (ran G)))"
apply (unfold RootEx_def)
apply (simp only: FAddSA_Union_ran Int_commute)
done

lemma FAddSA_RootEx:
  "[ ∪ (ran G) = F - {Root F G};
     dom G = ∪(States ` F);
     (dom G ∩ States SA) = {}; S ∈ dom G;
     RootEx F G ] ==> RootEx (insert SA F) (G [f+] (S,SA))"
apply (simp add: FAddSA_RootEx_def Int_commute cong: rev_conj_cong)
apply (auto cong: conj_cong) 
done

lemma FAddSA_Root_def:
  "[ S ∈ dom G; (States SA) ∩ (dom G) = {} ] ==>
   (Root F (G [f+] (S,SA)) = (@ A . A ∈ F ∧ A ∉ insert SA (∪ (ran G))))" 
apply (unfold Root_def)
apply (simp only: FAddSA_Union_ran Int_commute)
done

lemma FAddSA_RootEx_Root: 
  "[ Union (ran G) = F - {Root F G};
     ∪(States ` F) = dom G;
     (dom G ∩ States SA) = {}; S ∈ dom G;
     RootEx F G ] ==> (Root (insert SA F) (G [f+] (S,SA))) = (Root F G)"
apply (simp add: FAddSA_Root_def Int_commute cong: rev_conj_cong)
apply (simp cong:conj_cong)
done

lemma FAddSA_OneAncestor:
  "[ ∪ (ran G) = F - {Root F G};
     (dom G ∩ States SA) = {}; S ∈ dom G;
     ∪(States ` F) = dom G; RootEx F G;
     OneAncestor F G ] ==> OneAncestor (insert SA F) (G [f+] (S,SA))"
apply (subst OneAncestor_def)
apply simp
apply (rule ballI)
apply (rename_tac SAA)
apply (case_tac "SA = SAA")
apply (rule_tac a=S in ex1I)
apply (rule conjI)
apply simp
apply fast
apply (subst FAddSA_dom_insert)
apply simp
apply (simp add:Int_def)
apply simp
apply (rename_tac T)
apply (erule conjE bexE exE disjE)+
apply (rename_tac SAAA)
apply simp
apply (erule conjE)
apply (subst not_not [THEN sym])
apply (rule notI)
apply (case_tac "T ∈ States SAA")
apply blast
apply (drule_tac A=G and S=S and SA=SAA in FAddSA_States_neq)
apply fast
apply simp
apply (case_tac "SAA ∉ Union (ran G)")
apply (frule ran_dom_the)
prefer 2
apply fast
apply blast
apply simp
apply (erule conjE)
apply (simp add: States_Int_not_mem)
apply (unfold OneAncestor_def)
apply (drule_tac G=G and S=S and SA=SA in FAddSA_RootEx_Root)
apply simp
apply simp
apply simp
apply simp
apply (erule_tac x=SAA in ballE)
prefer 2
apply simp
apply simp
apply (erule conjE bexE ex1E exE disjE)+
apply (rename_tac T SAAA)
apply (rule_tac a=T in ex1I)
apply (rule conjI)
apply fast
apply (case_tac "T = S")
apply simp
apply (case_tac "S ∉ States SA")
apply simp
apply simp
apply (subst FAddSA_States_neq)
apply blast
apply (rule not_sym)
apply simp
apply simp
apply (rename_tac U)
apply simp
apply (erule conjE bexE)+
apply (rename_tac SAAAA)
apply simp
apply (erule conjE disjE)+
apply (frule FAddSA_dom_emptyset)
prefer 2
apply fast
back
back
apply simp
apply blast
apply simp
apply (erule_tac x=U in allE)
apply (erule impE)
prefer 2
apply simp
apply (rule conjI)
apply fast
apply (case_tac "S ≠ U")
apply (subgoal_tac "U ∉ States SA")
apply (drule_tac A=G in FAddSA_States_neq)
apply fast
apply simp
apply blast
apply (drule_tac A=G and SA=SA in FAddSA_dom_insert)
apply simp
apply blast
apply auto
done

lemma FAddSA_NoCycles:
  "[ (States SA ∩ dom G) = {}; S ∈ dom G;
     dom G = ∪(States ` F); NoCycles F G ] ==>
     NoCycles (insert SA F) (G [f+] (S,SA))"
apply (unfold NoCycles_def)
apply (rule ballI impI)+
apply (rename_tac SAA)
apply (case_tac "∃ s ∈ SAA. s ∈ States SA")
apply simp
apply (erule bexE)+
apply (rename_tac SAAA T)
apply (rule_tac x=T in bexI)
apply simp
apply (subst FAddSA_dom_emptyset)
apply simp
apply fast
apply blast
apply simp
apply simp
apply simp
apply simp
apply (erule_tac x=SAA in ballE)
prefer 2
apply simp
apply auto[1]
apply (unfold UNION_eq Pow_def)
apply simp
apply (case_tac "SAA = {}")
apply fast
apply simp
apply (erule bexE)+
apply (rename_tac SAAA T)
apply (rule_tac x=T in bexI)
prefer 2
apply simp
apply (case_tac "T=S")
apply simp
apply (subst FAddSA_dom_insert)
apply auto
done

lemma FAddSA_IsCompFun:
 "[ (States SA ∩ (∪(States ` F))) = {};
     S ∈ (∪(States ` F));
     IsCompFun F G ] ==> IsCompFun (insert SA F) (G [f+] (S,SA))"
apply (unfold IsCompFun_def)
apply (erule conjE)+
apply (simp add: Int_commute FAddSA_RootEx_Root FAddSA_RootEx FAddSA_OneAncestor FAddSA_NoCycles)
apply (rule conjI)
apply (subst FAddSA_dom_dom_States)
apply simp
apply blast
apply (simp add: Un_commute)
apply (simp add: FAddSA_Union_ran)
apply (case_tac "SA = Root F G")
prefer 2
apply blast
apply (subgoal_tac "States (Root F G) ⊆ ∪(States ` F)")
apply simp
apply (frule subset_lemma)
apply auto
done

lemma FAddSA_HierAuto:
  "[ (States SA ∩ (∪(States ` F))) = {};
      S ∈ (∪(States ` F));
      HierAuto D F E G ] ==> HierAuto D (insert SA F) (E ∪ SAEvents SA) (G [f+] (S,SA))"
apply (unfold HierAuto_def)
apply auto
apply (simp add: MutuallyDistinct_Insert)
apply (rule FAddSA_IsCompFun)
apply auto
done

lemma FAddSA_HierAuto_insert [simp]:
  "[ (States SA ∩ HAStates HA) = {};
      S ∈ HAStates HA ] ==>
    HierAuto (HAInitValue HA)
             (insert SA (SAs HA))
             (HAEvents HA ∪ SAEvents SA)
             (CompFun HA [f+] (S,SA))"
apply (unfold HAStates_def)
apply (rule FAddSA_HierAuto)
apply auto
done

subsection "Constructing a PseudoHA" 

definition
  PseudoHA :: "[('s,'e,'d)seqauto,'d data] => ('s,'e,'d)hierauto" where
  "PseudoHA SA D = Abs_hierauto(D,{SA}, SAEvents SA ,EmptyMap (States SA))"

lemma PseudoHA_SAs [simp]:
  "SAs (PseudoHA SA D) = {SA}"
by (unfold PseudoHA_def SAs_def, simp add: Abs_hierauto_inverse)

lemma PseudoHA_Events [simp]:
  "HAEvents (PseudoHA SA D) = SAEvents SA"
by (unfold PseudoHA_def HAEvents_def, simp add: Abs_hierauto_inverse)
 
lemma PseudoHA_CompFun [simp]:
  "CompFun (PseudoHA SA D) = EmptyMap (States SA)"
by (unfold PseudoHA_def CompFun_def, simp add: Abs_hierauto_inverse)

lemma PseudoHA_HAStates [simp]:
  "HAStates (PseudoHA SA D) = (States SA)"
by (unfold HAStates_def, auto)

lemma PseudoHA_HAInitValue [simp]:
  "(HAInitValue (PseudoHA SA D)) = D"
by (unfold PseudoHA_def Let_def HAInitValue_def, simp add: Abs_hierauto_inverse)
 
lemma PseudoHA_CompFun_the [simp]: 
 "S ∈ States A ==> (the (CompFun (PseudoHA A D) S)) = {}"
by simp

lemma PseudoHA_CompFun_ran [simp]:
 "(ran (CompFun (PseudoHA SA D))) = {{}}"
by auto

lemma PseudoHA_HARoot [simp]:
 "(HARoot (PseudoHA SA D)) = SA"
by (unfold HARoot_def, auto)

lemma PseudoHA_HAInitState [simp]:
  "HAInitState (PseudoHA A D) = InitState A"
apply (unfold HAInitState_def)
apply simp
done

lemma PseudoHA_HAInitStates [simp]:
  "HAInitStates (PseudoHA A D) = {InitState A}" 
apply (unfold HAInitStates_def)
apply simp
done

lemma PseudoHA_Chi [simp]:
  "S ∈ States A ==> Chi (PseudoHA A D) S = {}"
apply (unfold Chi_def restrict_def)
apply auto
done

lemma PseudoHA_ChiRel [simp]:
  "ChiRel (PseudoHA A D) = {}"
apply (unfold ChiRel_def)
apply simp
done

lemma PseudoHA_InitConf [simp]:
 "InitConf (PseudoHA A D) = {InitState A}"
apply (unfold InitConf_def)
apply simp
done

subsection ‹Extending a HA by a SA (‹AddSA›)›

definition
  AddSA :: "[('s,'e,'d)hierauto, 's * ('s,'e,'d)seqauto]
             => ('s,'e,'d)hierauto"
           (‹(_ [++]/ _)› [10,11]10) where
  "AddSA HA SSA = (let (S,SA) = SSA;
                        DNew = HAInitValue HA;
                        FNew = insert SA (SAs HA);
                        ENew = HAEvents HA ∪ SAEvents SA;
                        GNew = CompFun HA [f+] (S,SA)
                   in
                       Abs_hierauto(DNew,FNew,ENew,GNew))"

definition
  AddHA :: "[('s,'e,'d)hierauto, 's * ('s,'e,'d)hierauto]
             => ('s,'e,'d)hierauto"
           (‹(_ [**]/ _)› [10,11]10) where
  "AddHA HA1 SHA =
            (let (S,HA2) = SHA;
                 (D1,F1,E1,G1) = Rep_hierauto (HA1 [++] (S,HARoot HA2));
                 (D2,F2,E2,G2) = Rep_hierauto HA2;
                 FNew = F1 ∪ F2;
                 ENew = E1 ∪ E2;
                 GNew = G1 ++ G2
             in
                 Abs_hierauto(D1,FNew,ENew,GNew))"

lemma AddSA_SAs:
  "[ (States SA ∩ HAStates HA) = {};
      S ∈ HAStates HA ] ==> (SAs (HA [++] (S,SA))) = insert SA (SAs HA)"
apply (unfold Let_def AddSA_def)
apply (subst SAs_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_Events:
  "[ (States SA ∩ HAStates HA) = {};
      S ∈ HAStates HA ] ==>
     HAEvents (HA [++] (S,SA)) = (HAEvents HA) ∪ (SAEvents SA)"
apply (unfold Let_def AddSA_def)
apply (subst HAEvents_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_CompFun:
   "[ (States SA ∩ HAStates HA) = {};
      S ∈ HAStates HA ] ==>
     CompFun (HA [++] (S,SA)) = (CompFun HA [f+] (S,SA))"
apply (unfold Let_def AddSA_def)
apply (subst CompFun_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_HAStates:
   "[ (States SA ∩ HAStates HA) = {};
       S ∈ HAStates HA ] ==>
      HAStates (HA [++] (S,SA)) = (HAStates HA) ∪ (States SA)"
apply (unfold HAStates_def)
apply (subst AddSA_SAs)
apply (unfold HAStates_def)
apply auto
done

lemma AddSA_HAInitValue:
   "[ (States SA ∩ HAStates HA) = {};
       S ∈ HAStates HA ] ==>
      (HAInitValue (HA [++] (S,SA))) = (HAInitValue HA)"
apply (unfold Let_def AddSA_def)
apply (subst HAInitValue_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_HARoot:
   "[ (States SA ∩ HAStates HA) = {};
      S ∈ HAStates HA ] ==>
      (HARoot (HA [++] (S,SA))) = (HARoot HA)"
apply (unfold HARoot_def)
apply (simp add: AddSA_CompFun AddSA_SAs)
apply (subst FAddSA_RootEx_Root)
apply auto
apply (simp only: HAStates_SA_mem)
apply (unfold HAStates_def)
apply fast
done

lemma AddSA_CompFun_the: 
 "[ (States SA ∩ HAStates A) = {};
    S ∈ HAStates A ] ==>
  (the ((CompFun (A [++] (S,SA))) S)) = insert SA (the ((CompFun A) S))"
by (simp add: AddSA_CompFun)

lemma AddSA_CompFun_the2:
 "[ S' ∈ States (SA::('a,'c,'d)seqauto);
    (States SA ∩ HAStates A) = {};
    S ∈ HAStates A ] ==>
    the ((CompFun (A [++] (S,SA))) S') = {}"
apply (simp add: AddSA_CompFun)
apply (subst FAddSA_dom_emptyset)
apply auto
done

lemma AddSA_CompFun_the3:
 "[ S' ∉ States (SA::('a,'c,'d)seqauto);
    S ≠ S';
    (States SA ∩ HAStates A) = {};
    S ∈ HAStates A ] ==>
   (the ((CompFun (A [++] (S,SA))) S')) = (the ((CompFun A) S'))"
by (simp add: AddSA_CompFun)

lemma AddSA_CompFun_ran:
 "[ (States SA ∩ HAStates A) = {};
     S ∈ HAStates A ] ==>
   ran (CompFun (A [++] (S,SA))) =
       insert {} (insert (insert SA (the ((CompFun A) S))) (ran (CompFun A) - {the ((CompFun A) S)}))"
apply (simp add: AddSA_CompFun)
apply (subst FAddSA_ran)
apply auto
apply (fast dest: CompFun_Int_disjoint) 
done

lemma AddSA_CompFun_ran2:
 "[ (States SA1 ∩ HAStates A) = {};
    (States SA2 ∩ (HAStates A ∪ States SA1)) = {};
     S ∈ HAStates A;
     T ∈ States SA1 ] ==>
   ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2))) =
       insert {} (insert {SA2} (ran (CompFun (A [++] (S,SA1)))))"
apply (simp add: AddSA_HAStates AddSA_CompFun)
apply (subst FAddSA_ran)
apply (rule ballI)
apply (rule impI)
apply (subst AddSA_CompFun [THEN sym])
apply simp
apply simp
apply (subst AddSA_CompFun [THEN sym])
apply simp
apply simp
apply (rule CompFun_Int_disjoint)
apply simp
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
apply (case_tac "S ∈ States SA1")
apply simp
apply (simp only: dom_CompFun [THEN sym])
apply (frule FAddSA_dom_dom_States)
apply fast
apply simp
apply (case_tac "S ∈ States SA1")
apply simp
apply fast
apply (subst FAddSA_dom_dom_States)
apply simp
apply simp
apply simp
apply (case_tac "S ∈ States SA1")
apply simp
apply fast
apply (subst FAddSA_dom_dom_States)
apply simp
apply simp
apply simp
apply (case_tac "S ∈ States SA1")
apply simp
apply fast
apply simp
apply fast
done

lemma AddSA_CompFun_ran_not_mem:
 "[ States SA2 ∩ (HAStates A ∪ States SA1) = {};
    States SA1 ∩ HAStates A = {};
    S ∈ HAStates A ] ==>
   {SA2} ∉ ran (CompFun A [f+] (S, SA1))"
  apply (cut_tac HA="A [++] (S,SA1)" and Sas="{SA2}" in ran_CompFun_is_not_SA)
  apply (metis AddSA_HAStates SA_States_disjunct2 SAs_States_HAStates insert_subset)
   apply (simp add: AddSA_HAStates AddSA_CompFun)
  done

lemma AddSA_CompFun_ran3:
 "[ (States SA1 ∩ HAStates A) = {};
    (States SA2 ∩ (HAStates A ∪ States SA1)) = {};
    (States SA3 ∩ (HAStates A ∪ States SA1 ∪ States SA2)) = {};
     S ∈ HAStates A;
     T ∈ States SA1 ] ==>
    ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2) [++] (T,SA3))) =
       insert {} (insert {SA3,SA2} (ran (CompFun (A [++] (S,SA1)))))"
  apply (simp add: AddSA_HAStates AddSA_CompFun)
  apply (subst FAddSA_ran)
  apply (metis AddSA_CompFun AddSA_HAStates CompFun_Int_disjoint UnCI dom_CompFun)
  apply (metis AddSA_CompFun AddSA_HAStates UnCI dom_CompFun)
  apply (metis AddSA_CompFun AddSA_HAStates UnCI dom_CompFun)

  apply (subst AddSA_CompFun [THEN sym])
    back
    apply simp
   apply simp

  apply (subst AddSA_CompFun [THEN sym])
    back
    apply (simp add: AddSA_HAStates)
   apply (simp add: AddSA_HAStates)
  apply (subst AddSA_CompFun_ran2)
      apply fast
     apply fast
    apply fast
   apply fast
  apply (simp add: AddSA_CompFun)
  apply (subst  FAddSA_dom_insert)
    apply (subst FAddSA_dom_dom_States)
      apply simp
     apply fast
    apply simp
   apply fast
  apply (subst FAddSA_dom_emptyset)
     apply simp
    apply fast
   apply simp
  apply simp
  apply (subst  FAddSA_dom_insert)
    apply (subst FAddSA_dom_dom_States)
      apply simp
     apply fast
    apply simp
   apply fast
  apply (subst FAddSA_dom_emptyset)
     apply simp
    apply fast
   apply simp
  apply simp
  by (simp add: AddSA_CompFun_ran_not_mem insert_Diff_if insert_commute)

lemma AddSA_CompFun_PseudoHA_ran:
  "[ S ∈ States RootSA;
     States RootSA ∩ States SA = {} ] ==>
     (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA)))) = (insert {} {{SA}})"
apply (subst AddSA_CompFun_ran)
apply auto
done

lemma AddSA_CompFun_PseudoHA_ran2:
  "[ States SA1 ∩ States RootSA = {};
     States SA2 ∩ (States RootSA ∪ States SA1) = {};
     S ∈ States RootSA ] ==>
     (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA1) [++] (S,SA2)))) = (insert {} {{SA2,SA1}})"
apply (subst AddSA_CompFun_ran) 
prefer 3
apply (subst AddSA_CompFun_the)
apply simp
apply simp
apply (subst AddSA_CompFun_PseudoHA_ran)
apply fast
apply fast
apply (subst AddSA_CompFun_the)
apply simp
apply simp
apply simp
apply fast
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
done

lemma AddSA_HAInitStates [simp]:
 "[ States SA ∩ HAStates A = {};
    S ∈ HAStates A ] ==>
   HAInitStates (A [++] (S,SA)) = insert (InitState SA) (HAInitStates A)"
apply (unfold HAInitStates_def)
apply (simp add: AddSA_SAs)
done

lemma AddSA_HAInitState [simp]:
 "[ States SA ∩ HAStates A = {};
    S ∈ HAStates A ] ==>
  HAInitState (A [++] (S,SA)) = (HAInitState A)"
apply (unfold HAInitState_def)
apply (simp add: AddSA_HARoot)
done

lemma AddSA_Chi [simp]:
 "[ States SA ∩ HAStates A = {};
   S ∈ HAStates A ] ==>
  Chi (A [++] (S,SA)) S = (States SA) ∪ (Chi A S)"
apply (unfold Chi_def restrict_def)
apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the)
apply auto
done

lemma AddSA_Chi2 [simp]:
 "[ States SA ∩ HAStates A = {};
    S ∈ HAStates A;
    T ∈ States SA ] ==>
    Chi (A [++] (S,SA)) T = {}"
apply (unfold Chi_def restrict_def)
apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the2)
done

lemma AddSA_Chi3 [simp]:
 "[ States SA ∩ HAStates A = {};
    S ∈ HAStates A;
    T ∉ States SA; T ≠ S ] ==>
    Chi (A [++] (S,SA)) T = Chi A T"
apply (unfold Chi_def restrict_def)
apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the3)
apply auto
done

lemma AddSA_ChiRel [simp]:
 "[ States SA ∩ HAStates A = {};
    S ∈ HAStates A ] ==>
   ChiRel (A [++] (S,SA)) = { (T,T') . T = S ∧ T' ∈ States SA } ∪ (ChiRel A)" 
apply (unfold ChiRel_def)
apply (simp add: AddSA_HAStates)
apply safe
apply (rename_tac T U)
apply (case_tac "T ∈ States SA")
apply simp
apply simp
apply (rename_tac T U)
apply (case_tac "T ≠ S")
apply (case_tac "T ∈ States SA")
apply simp
apply simp
apply simp
apply (rename_tac T U)
apply (case_tac "T ∈ States SA")
apply simp
apply simp
apply (cut_tac A=A and T=T in Chi_HAStates)
apply fast
apply (case_tac "T ∈ States SA")
apply simp
apply simp
apply (cut_tac A=A and T=T in Chi_HAStates)
apply fast
apply fast
apply (rename_tac T U)
apply (case_tac "T ≠ S")
apply (case_tac "T ∈ States SA")
apply simp
apply simp
apply simp
apply (rename_tac T U)
apply (case_tac "T ∈ States SA")
apply auto
apply (metis AddSA_Chi AddSA_Chi3 Int_iff Un_iff empty_iff)
done

lemma help_InitConf:
  "[States SA ∩ HAStates A = {} ] ==> {p. fst p ≠ InitState SA ∧ snd p ≠ InitState SA ∧
       p ∈ insert (InitState SA) (HAInitStates A) × insert (InitState SA) (HAInitStates A) ∧
       (p ∈ {S} × States SA ∨ p ∈ ChiRel A)} =
   (HAInitStates A × HAInitStates A ∩ ChiRel A)"    
apply auto
apply (cut_tac A=SA in InitState_States)
apply (cut_tac A=A in HAInitStates_HAStates, fast)
apply (cut_tac A=SA in InitState_States)
apply (cut_tac A=A in HAInitStates_HAStates, fast)
done
 
lemma AddSA_InitConf [simp]:
 "[ States SA ∩ HAStates A = {};
    S ∈ InitConf A ] ==>
    InitConf (A [++] (S,SA)) = insert (InitState SA) (InitConf A)"
apply (frule InitConf_HAStates2)
apply (unfold InitConf_def)
apply (simp del: insert_Times_insert)
  apply auto
  apply (rename_tac T)
   apply (case_tac "T=S")
  apply auto
  prefer 3
   apply (rule_tac R="(HAInitStates A) × (HAInitStates A) ∩ ChiRel A" in trancl_subseteq)
 apply auto
 apply (rotate_tac 3)
 apply (frule trancl_collect)
   prefer 2
   apply fast
  apply auto
   apply (cut_tac A=SA in InitState_States)
   apply (frule ChiRel_HAStates)
   apply fast
  apply (frule ChiRel_HAStates)
  apply (cut_tac A=SA in InitState_States)
  apply fast
 apply (subst help_InitConf [THEN sym])
  apply fast
 apply auto
apply (rule_tac b=S in rtrancl_into_rtrancl)
 apply auto
  prefer 2
  apply (erule rtranclE)
   apply auto
 prefer 2
 apply (erule rtranclE)
  apply auto
 apply (rule_tac R="(HAInitStates A) × (HAInitStates A) ∩ ChiRel A" in trancl_subseteq)
apply auto
done

lemma AddSA_InitConf2 [simp]:
 "[ States SA ∩ HAStates A = {};
    S ∉ InitConf A;
  S ∈ HAStates A ] ==>
  InitConf (A [++] (S,SA)) = InitConf A"
apply (unfold InitConf_def)
apply simp
apply auto
 apply (rename_tac T)
 prefer 2
 apply (rule_tac R="(HAInitStates A) × (HAInitStates A) ∩ ChiRel A" in trancl_subseteq)
  apply auto
apply (case_tac "T=InitState SA")
 apply auto
 prefer 2
 apply (rotate_tac 3)
 apply (frule trancl_collect)
   prefer 2
   apply fast
  apply auto
   apply (cut_tac A=SA in InitState_States)
   apply (frule ChiRel_HAStates)
   apply fast
  apply (cut_tac A=SA in InitState_States)
  apply (frule ChiRel_HAStates)
 apply fast
 apply (cut_tac A=SA in InitState_States)
 apply (cut_tac A=A in HAInitStates_HAStates)
 apply (subst help_InitConf [THEN sym])
  apply fast
 apply auto
apply (rule_tac b="InitState SA" in rtrancl_induct)
  apply auto
  apply (frule ChiRel_HAStates2)
  apply (cut_tac A=SA in InitState_States)
  apply fast
 prefer 2
 apply (frule ChiRel_HAStates)
 apply (cut_tac A=SA in InitState_States)
 apply fast
apply (rule rtrancl_into_rtrancl)
 apply auto
done

subsection "Theorems for Calculating Wellformedness of HA"

lemma PseudoHA_HAStates_IFF:
 "(States SA) = X ==> (HAStates (PseudoHA SA D)) = X"
apply simp
done

lemma AddSA_SAs_IFF:
 "[ States SA ∩ HAStates HA = {};
    S ∈ HAStates HA;
    (SAs HA) = X ] ==> (SAs (HA [++] (S, SA))) = (insert SA X)"
apply (subst AddSA_SAs)
apply auto
done

lemma AddSA_Events_IFF:
 "[ States SA ∩ HAStates HA = {};
    S ∈ HAStates HA;
    (HAEvents HA) = HAE;
    (SAEvents SA) = SAE;
    (HAE ∪ SAE) = X ] ==> (HAEvents (HA [++] (S, SA))) = X"
apply (subst AddSA_Events)
apply auto
done

lemma AddSA_CompFun_IFF:
 "[ States SA ∩ HAStates HA = {};
    S ∈ HAStates HA;
    (CompFun HA) = HAG;
    (HAG [f+] (S, SA)) = X ] ==> (CompFun (HA [++] (S, SA))) = X"
apply (subst AddSA_CompFun)
apply auto
done

lemma AddSA_HAStates_IFF: 
 "[ States SA ∩ HAStates HA = {};
    S ∈ HAStates HA;
    (HAStates HA) = HAS;
    (States SA) = SAS;
    (HAS ∪ SAS) = X ] ==> (HAStates (HA [++] (S, SA))) = X"
apply (subst AddSA_HAStates)
apply auto
done

lemma AddSA_HAInitValue_IFF:
 "[ States SA ∩ HAStates HA = {};
    S ∈ HAStates HA;
    (HAInitValue HA) = X ] ==> (HAInitValue (HA [++] (S, SA))) = X"
apply (subst AddSA_HAInitValue)
apply auto
done

lemma AddSA_HARoot_IFF:
 "[ States SA ∩ HAStates HA = {};
    S ∈ HAStates HA;
    (HARoot HA) = X ] ==> (HARoot (HA [++] (S, SA))) = X"
apply (subst AddSA_HARoot)
apply auto
done

lemma AddSA_InitConf_IFF:
 "[ InitConf A = Y;
    States SA ∩ HAStates A = {};
    S ∈ HAStates A;
    (if S ∈ Y then insert (InitState SA) Y else Y) = X ] ==>
    InitConf (A [++] (S,SA)) = X" 
apply (case_tac "S ∈ Y")
apply auto
done

lemma AddSA_CompFun_ran_IFF:
  "[ (States SA ∩ HAStates A) = {};
     S ∈ HAStates A;
     (insert {} (insert (insert SA (the ((CompFun A) S))) (ran (CompFun A) - {the ((CompFun A) S)}))) = X ] ==>
     ran (CompFun (A [++] (S,SA))) = X"
apply (subst  AddSA_CompFun_ran)
apply auto
done

lemma AddSA_CompFun_ran2_IFF:
 "[ (States SA1 ∩ HAStates A) = {};
    (States SA2 ∩ (HAStates A ∪ States SA1)) = {};
    S ∈ HAStates A;
    T ∈ States SA1;
    insert {} (insert {SA2} (ran (CompFun (A [++] (S,SA1))))) = X ] ==>
    ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2))) = X"
apply (subst AddSA_CompFun_ran2)
apply auto
done
   
lemma AddSA_CompFun_ran3_IFF:
 "[ (States SA1 ∩ HAStates A) = {};
    (States SA2 ∩ (HAStates A ∪ States SA1)) = {};
    (States SA3 ∩ (HAStates A ∪ States SA1 ∪ States SA2)) = {};
     S ∈ HAStates A;
     T ∈ States SA1;
     insert {} (insert {SA3,SA2} (ran (CompFun (A [++] (S,SA1))))) = X ] ==>
     ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2) [++] (T,SA3))) = X" 
apply (subst AddSA_CompFun_ran3)
apply auto
done

lemma AddSA_CompFun_PseudoHA_ran_IFF:
  "[ S ∈ States RootSA;
     States RootSA ∩ States SA = {};
   (insert {} {{SA}}) = X ] ==>
   (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA)))) = X"
apply (subst AddSA_CompFun_PseudoHA_ran)
apply auto
done

lemma AddSA_CompFun_PseudoHA_ran2_IFF:
  "[ States SA1 ∩ States RootSA = {};
     States SA2 ∩ (States RootSA ∪ States SA1) = {};
     S ∈ States RootSA;
     (insert {} {{SA2,SA1}}) = X ] ==>
     (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA1) [++] (S,SA2)))) = X" 
apply (subst AddSA_CompFun_PseudoHA_ran2)
apply auto
done


ML ‹

  AddSA_SAs_IFF = @{thm AddSA_SAs_IFF};
  AddSA_Events_IFF = @{thm AddSA_Events_IFF};
  AddSA_CompFun_IFF = @{thm AddSA_CompFun_IFF};
  AddSA_HAStates_IFF = @{thm AddSA_HAStates_IFF};
  PseudoHA_HAStates_IFF = @{thm PseudoHA_HAStates_IFF};
  AddSA_HAInitValue_IFF = @{thm AddSA_HAInitValue_IFF};
  AddSA_CompFun_ran_IFF = @{thm AddSA_CompFun_ran_IFF};
  AddSA_HARoot_IFF = @{thm AddSA_HARoot_IFF};
  insert_inter = @{thm insert_inter};
  insert_notmem = @{thm insert_notmem};
  PseudoHA_CompFun = @{thm PseudoHA_CompFun};
  PseudoHA_Events = @{thm PseudoHA_Events};
  PseudoHA_SAs = @{thm PseudoHA_SAs};
  PseudoHA_HARoot = @{thm PseudoHA_HARoot};
  PseudoHA_HAInitValue = @{thm PseudoHA_HAInitValue};
  PseudoHA_CompFun_ran = @{thm PseudoHA_CompFun_ran};
  Un_empty_right = @{thm Un_empty_right};
  insert_union = @{thm insert_union};


  wellformed_tac ctxt L i =
 FIRST[resolve_tac ctxt [AddSA_SAs_IFF] i,
 resolve_tac ctxt [AddSA_Events_IFF] i,
 resolve_tac ctxt [AddSA_CompFun_IFF] i,
 resolve_tac ctxt [AddSA_HAStates_IFF] i,
 resolve_tac ctxt [PseudoHA_HAStates_IFF] i,
 resolve_tac ctxt [AddSA_HAInitValue_IFF] i,
 resolve_tac ctxt [AddSA_HARoot_IFF] i,
 resolve_tac ctxt [AddSA_CompFun_ran_IFF] i,
 resolve_tac ctxt [insert_inter] i,
 resolve_tac ctxt [insert_notmem] i,
 CHANGED (simp_tac (put_simpset HOL_basic_ss ctxt addsimps
 [PseudoHA_HARoot, PseudoHA_CompFun, PseudoHA_CompFun_ran,PseudoHA_Events,PseudoHA_SAs,insert_union,
 PseudoHA_HAInitValue,Un_empty_right]@ L) i),
 fast_tac ctxt i,
 CHANGED (simp_tac ctxt i)];
 ›

method_setup wellformed  = ‹Attrib.thms >> (fn thms => fn ctxt => (METHOD (fn facts =>
 (HEADGOAL (wellformed_tac ctxt (facts @ thms))))))›

end