Theory CSP_F_domain

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005 (modified)    |
            |                 August 2005 (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_domain = CSP_T_traces + CSP_F_failures:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*********************************************************
                        domF
 *********************************************************)

(*--------------------------------*
 |             STOP               |
 *--------------------------------*)

(* T2 *)

lemma STOP_T2 : "HC_T2 (traces(STOP), failures(STOP))"
by (simp add: HC_T2_def in_traces in_failures)

(* F3 *)

lemma STOP_F3 : "HC_F3 (traces(STOP), failures(STOP))"
by (simp add: HC_F3_def in_traces in_failures)

(* T3_F4 *)

lemma STOP_T3_F4 : "HC_T3_F4 (traces(STOP), failures(STOP))"
by (auto simp add: HC_T3_F4_def in_traces in_failures)

(*** STOP_domF ***)

lemma STOP_domF : "(traces(STOP), failures(STOP)) : domF"
apply (simp add: domF_iff)
apply (simp add: STOP_T2)
apply (simp add: STOP_F3)
apply (simp add: STOP_T3_F4)
done

(*--------------------------------*
 |             SKIP               |
 *--------------------------------*)

(* T2 *)

lemma SKIP_T2 : "HC_T2 (traces(SKIP), failures(SKIP))"
by (simp add: HC_T2_def in_traces in_failures)

(* F3 *)

lemma SKIP_F3 : "HC_F3 (traces(SKIP), failures(SKIP))"
apply (simp add: HC_F3_def in_traces in_failures)
by (auto simp add: Evset_def)

(* T3_F4 *)

lemma SKIP_T3_F4 : "HC_T3_F4 (traces(SKIP), failures(SKIP))"
by (auto simp add: HC_T3_F4_def in_traces in_failures)

(*** SKIP_domF ***)

lemma SKIP_domF : "(traces(SKIP), failures(SKIP)) : domF"
apply (simp add: domF_iff)
apply (simp add: SKIP_T2)
apply (simp add: SKIP_F3)
apply (simp add: SKIP_T3_F4)
done

(*--------------------------------*
 |              DIV               |
 *--------------------------------*)

(* T2 *)

lemma DIV_T2 : "HC_T2 (traces(DIV), failures(DIV))"
by (simp add: HC_T2_def in_traces in_failures)

(* F3 *)

lemma DIV_F3 : "HC_F3 (traces(DIV), failures(DIV))"
by (simp add: HC_F3_def in_traces in_failures)

(* T3_F4 *)

lemma DIV_T3_F4 : "HC_T3_F4 (traces(DIV), failures(DIV))"
by (auto simp add: HC_T3_F4_def in_traces in_failures)

(*** DIV_domF ***)

lemma DIV_domF : "(traces(DIV), failures(DIV)) : domF"
apply (simp add: domF_iff)
apply (simp add: DIV_T2)
apply (simp add: DIV_F3)
apply (simp add: DIV_T3_F4)
done

(*--------------------------------*
 |          Act_prefix            |
 *--------------------------------*)

(* T2 *)

lemma Act_prefix_T2 :
  "(traces(P), failures(P)) : domF ==> HC_T2 (traces(a -> P), failures(a -> P))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE, simp)

apply (simp add: domF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
by (force)

(* F3 *)

lemma Act_prefix_F3 :
  "(traces(P), failures(P)) : domF ==> HC_F3 (traces(a -> P), failures(a -> P))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)

apply (elim conjE disjE, simp)
apply (case_tac "Ev a ~: Y", simp)  (* show "Ev a : Y --> contradict" *)
apply (drule_tac x="Ev a" in spec, simp)
apply (drule_tac x="<>" in spec, simp)

apply (elim conjE exE, simp)
apply (simp add: domF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="X" in spec)
apply (drule_tac x="Y" in spec)
apply (simp)

apply (drule mp)
 apply (intro allI impI)
 apply (drule_tac x="aa" in spec, simp)
 apply (drule_tac x="sa ^^ <aa>" in spec)
apply (simp add: appt_assoc)
by (simp)

(* T3_F4 *)

lemma Act_prefix_T3_F4 : 
  "(traces(P), failures(P)) : domF ==> HC_T3_F4 (traces(a -> P), failures(a -> P))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="s" in spec)

apply (erule disjE, simp)   (* s ^^ <Tick> = <> --> contradict *)
apply (erule disjE, simp)   (* s = <> --> contradict *)
apply (erule disjE, simp)   (* s = <Tick> --> contradict *)

apply (elim conjE exE)      (* s = [Ev a]t ^^ sb *)

apply (simp add: domF_iff HC_T3_F4_def)
apply (elim conjE exE)
apply (drule_tac x="sb" in spec)
apply (simp add: appt_assoc)
done

(*** Act_prefix_domF ***)

lemma Act_prefix_domF : 
  "(traces(P), failures(P)) : domF ==> (traces(a -> P), failures(a -> P)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Act_prefix_T2)
apply (simp add: Act_prefix_F3)
apply (simp add: Act_prefix_T3_F4)
done

(*--------------------------------*
 |        Ext_pre_choice          |
 *--------------------------------*)

(* T2 *)

lemma Ext_pre_choice_T2 :
  "ALL a. (traces(Pf a), failures(Pf a)) : domF
     ==> HC_T2 (traces(? :X -> Pf), failures(? :X -> Pf))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE, simp)

apply (drule_tac x="a" in spec)
apply (simp add: domF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
by (force)

(* F3 *)

lemma Ext_pre_choice_F3 :
  "ALL a. (traces(Pf a), failures(Pf a)) : domF
     ==> HC_F3 (traces(? :X -> Pf), failures(? :X -> Pf))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)

apply (elim conjE disjE, simp)

(* s = <> *)
apply (case_tac "EX a. Ev a :Ev ` X Int (Xa Un Y)")  (* show contradiction" *)
 apply (elim conjE exE)
 apply (drule_tac x="Ev a" in spec)
 apply (drule mp)
  apply (simp)                      (* show "Ev a : Y" *)
  apply (elim conjE disjE)
  apply (fast)                      (* contradict *)
  apply (simp)

 apply (drule_tac x="a" in spec)
 apply (drule_tac x="a" in spec)
 apply (simp)
 apply (drule_tac x="s" in spec)
 apply (simp)
 apply (fast)                      (* contradict *)
apply (fast)                       (* Ev ` X Int (Xa Un Y) = {} *)

(* s ~= <> *)
apply (elim conjE exE, simp)
apply (drule_tac x="a" in spec)
apply (simp add: domF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="Xa" in spec)
apply (drule_tac x="Y" in spec)
apply (simp)

apply (drule mp)
 apply (intro allI impI)
 apply (drule_tac x="aa" in spec, simp)
 apply (drule_tac x="a" in spec)
 apply (drule_tac x="sa ^^ <aa>" in spec)
 apply (simp add: appt_assoc)
by (simp)

(* T3_F4 *)

lemma Ext_pre_choice_T3_F4 : 
  "ALL a. (traces(Pf a), failures(Pf a)) : domF
     ==> HC_T3_F4 (traces(? :X -> Pf), failures(? :X -> Pf))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="s" in spec)

apply (erule disjE, simp)   (* contradict *)
apply (erule disjE, simp)   (* s = <> --> contradict *)
apply (erule disjE, simp)   (* s = <Tick> --> contradict *)

apply (elim conjE exE)      (* s = [Ev aa]t ^^ sb *)
apply (drule_tac x="a" in spec)
apply (simp add: domF_iff HC_T3_F4_def)
apply (elim conjE exE)
apply (drule_tac x="sb" in spec)
apply (simp add: appt_assoc)
done

(*** Ext_pre_choice_domF ***)

lemma Ext_pre_choice_domF : 
  "ALL a. (traces(Pf a), failures(Pf a)) : domF
     ==> (traces(? :X -> Pf), failures(? :X -> Pf)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Ext_pre_choice_T2)
apply (simp add: Ext_pre_choice_F3)
apply (simp add: Ext_pre_choice_T3_F4)
done

(*--------------------------------*
 |          Ext_choice            |
 *--------------------------------*)

(* T2 *)

lemma Ext_choice_T2 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T2 (traces(P [+] Q), failures(P [+] Q))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)

apply (simp add: domF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="s" in spec)
by (fast)

(* F3 *)

lemma Ext_choice_F3 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_F3 (traces(P [+] Q), failures(P [+] Q))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)

apply (elim conjE disjE)
apply (simp_all add: domF_def HC_F3_def)
apply (auto simp add: Evset_def)
done

(* T3_F4 *)

lemma Ext_choice_T3_F4 : 
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T3_F4 (traces(P [+] Q), failures(P [+] Q))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)

apply (simp add: domF_iff HC_T3_F4_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="s" in spec)
by (auto)

(*** Ext_choice_domF ***)

lemma Ext_choice_domF : 
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> (traces(P [+] Q), failures(P [+] Q)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Ext_choice_T2)
apply (simp add: Ext_choice_F3)
apply (simp add: Ext_choice_T3_F4)
done

(*--------------------------------*
 |          Int_choice            |
 *--------------------------------*)

(* T2 *)

lemma Int_choice_T2 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T2 (traces(P |~| Q), failures(P |~| Q))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (simp add: domF_def HC_T2_def)
by (auto)

(* F3 *)

lemma Int_choice_F3 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_F3 (traces(P |~| Q), failures(P |~| Q))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (simp add: domF_def HC_F3_def)
by (auto)

(* T3_F4 *)

lemma Int_choice_T3_F4 : 
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T3_F4 (traces(P |~| Q), failures(P |~| Q))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (simp add: domF_iff HC_T3_F4_def)
by (auto)

(*** Int_choice_domF ***)

lemma Int_choice_domF : 
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> (traces(P |~| Q), failures(P |~| Q)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Int_choice_T2)
apply (simp add: Int_choice_F3)
apply (simp add: Int_choice_T3_F4)
done

(*--------------------------------*
 |        Rep_int_choice          |
 *--------------------------------*)

(* T2 *)

lemma Union_proc_T2:
  "ALL c. (Tf c, Ff c) : domF
   ==> HC_T2 ({t. t = <> | (EX c:C. t :t Tf c)}t,
                         {f. EX c:C. f :f Ff c}f)"
apply (simp add: HC_T2_def)
apply (simp add: in_traces)
apply (simp add: in_failures)
apply (intro allI impI)
apply (elim conjE bexE exE)
apply (rule disjI2)
apply (drule_tac x="c" in spec)
apply (rule_tac x="c" in bexI)
apply (simp add: domF_def HC_T2_def)
by (auto)

lemma Rep_int_choice_T2 :
  "ALL c. (traces(Pf c), failures(Pf c)) : domF
     ==> HC_T2 (traces(!! :C .. Pf), failures(!! :C .. Pf))"
apply (simp add: traces_def failures_def)
apply (simp add: Union_proc_T2)
done

(* F3 *)

lemma Union_proc_F3:
  "ALL c. (Tf c, Ff c) : domF
   ==>
   HC_F3 ({t. t = <> | (EX c:C. t :t Tf c)}t,
          {f. EX c:C. f :f Ff c}f)"
apply (simp add: HC_F3_def)
apply (simp add: in_traces)
apply (simp add: in_failures)
apply (intro allI)
apply (intro impI)
apply (elim conjE bexE)
apply (rule_tac x="c" in bexI)
apply (drule_tac x="c" in spec)
apply (rule domF_F3)
apply (auto)
done

lemma Rep_int_choice_F3 : 
  "ALL c. (traces(Pf c), failures(Pf c)) : domF
     ==> HC_F3 (traces(!! :C .. Pf), failures(!! :C .. Pf))"
apply (simp add: traces_def failures_def)
apply (simp add: Union_proc_F3)
done

(* T3_F4 *)

lemma Union_proc_T3_F4:
  "ALL c. (Tf c, Ff c) : domF
   ==>
   HC_T3_F4 ({t. t = <> | (EX c:C. t :t Tf c)}t,
             {f. EX c:C. f :f Ff c}f)"
apply (simp add: HC_T3_F4_def)
apply (simp add: in_traces)
apply (simp add: in_failures)
apply (auto)
apply (rule_tac x="c" in bexI)
apply (rule domF_F4)
apply (simp_all)
apply (rule_tac x="c" in bexI)
apply (rule domF_T3)
apply (simp_all)
done

lemma Rep_int_choice_T3_F4 : 
  "ALL c. (traces(Pf c), failures(Pf c)) : domF
     ==> HC_T3_F4 (traces(!! :C .. Pf), failures(!! :C .. Pf))"
apply (simp add: traces_def failures_def)
apply (simp add: Union_proc_T3_F4)
done

(*** F ***)

lemma Union_proc_domF:
  "ALL c. (Tf c, Ff c) : domF
   ==> ({t. t = <> | (EX c:C. t :t Tf c)}t,
        {f. EX c:C. f :f Ff c}f) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Union_proc_T2)
apply (simp add: Union_proc_F3)
apply (simp add: Union_proc_T3_F4)
done

(*** Rep_int_choice_domF ***)

lemma Rep_int_choice_domF : 
  "ALL c. (traces(Pf c), failures(Pf c)) : domF
     ==> (traces(!! :C .. Pf), failures(!! :C .. Pf)) : domF"
apply (simp add: traces_def failures_def)
apply (simp add: Union_proc_domF)
done

(*--------------------------------*
 |               IF               |
 *--------------------------------*)

(* T2 *)

lemma IF_T2 :
  "[| (traces(P), failures(P)) : domF ;
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T2 (traces(IF b THEN P ELSE Q), failures(IF b THEN P ELSE Q))"
by (simp add: HC_T2_def in_traces in_failures domF_def)

(* F3 *)

lemma IF_F3 :
  "[| (traces(P), failures(P)) : domF ;
      (traces(Q), failures(Q)) : domF |]
     ==> HC_F3 (traces(IF b THEN P ELSE Q), failures(IF b THEN P ELSE Q))"
by (simp add: HC_F3_def in_traces in_failures domF_def)

(* T3_F4 *)

lemma IF_T3_F4 : 
  "[| (traces(P), failures(P)) : domF ;
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T3_F4 (traces(IF b THEN P ELSE Q), failures(IF b THEN P ELSE Q))"
by (simp add: HC_T3_F4_def in_traces in_failures domF_iff)

(*** IF_domF ***)

lemma IF_domF :
  "[| (traces(P), failures(P)) : domF ;
      (traces(Q), failures(Q)) : domF |]
     ==> (traces(IF b THEN P ELSE Q), failures(IF b THEN P ELSE Q)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: IF_T2)
apply (simp add: IF_F3)
apply (simp add: IF_T3_F4)
done

(*--------------------------------*
 |           Parallel             |
 *--------------------------------*)

(*** T2 ***)

lemma Parallel_T2 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T2 (traces(P |[X]| Q), failures(P |[X]| Q))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="t" in exI)
apply (simp)
apply (simp add: domF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="t" in spec)

apply (drule mp, rule_tac x="Y" in exI, simp)
apply (drule mp, rule_tac x="Z" in exI, simp)
by (simp)

(*** F3 ***)

lemma Parallel_F3_lm1: "X1 Un (X2 Un X3) - X = (X1 - X) Un (X2 - X) Un (X3 - X)"
by (auto)

lemma Parallel_F3_lm2: "[| X1 = X2 ; Y1 = Y2 |] ==> X1 Un Y1 = X2 Un Y2"
by (auto)

lemma Parallel_F3 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_F3 (traces(P |[X]| Q), failures(P |[X]| Q))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (rename_tac u X12 Y X1 X2 s t)

(* (u, X12) :f [[P |[X]| Q]]F *)
(* (s, X1)  :f [[P]]F         *)
(* (t, X2)  :f [[Q]]F         *)
(*  X12 = X1 Un X2               *)

apply (rule_tac x=
        "X1 Un
         ({a. a : Y & (a = Tick | a : Ev ` X) & s ^^ <a> ~:t traces(P)} Un
          {a. a : Y & a ~= Tick & a ~: Ev ` X})" in exI)       (* Z1 *)
apply (rule_tac x=
        "X2 Un
         ({a. a : Y & (a = Tick | a : Ev ` X) & t ^^ <a> ~:t traces(Q)} Un
          {a. a : Y & a ~= Tick & a ~: Ev ` X})" in exI)       (* Z2 *)

apply (subgoal_tac "noTick s & noTick t", simp)
apply (rule conjI)

(* show X12 Un Y = X1 Un Z1 Un Z2 *)
apply (rule equalityI)

 (* <= *)
 apply (rule subsetI, simp)
 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (simp)

 apply (drule_tac x="x" in spec, simp)
 apply (drule_tac x="s ^^ <x>" in spec)
 apply (drule_tac x="t ^^ <x>" in spec)

  (* no sync *)
  apply (case_tac "x ~= Tick & x ~: Ev ` X", simp)
  (* sync *)
  apply (simp add: par_tr_last)
  apply (erule disjE, simp)
  apply (force)

  apply (rotate_tac -2)
  apply (erule disjE, simp)
  apply (force)
  apply (simp)
  apply (force)

 (* => *)
 apply (force)

apply (rule conjI)

 (* show X1 Un ... = X2 Un ... *)
 apply (simp add: Parallel_F3_lm1)
 apply (rule Parallel_F3_lm2)
 apply (rule Parallel_F3_lm2)
 apply (simp)
 apply (force)
 apply (simp)

 (* condition 2 *)
 apply (rule_tac x="s" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)

 apply (simp add: domF_def HC_F3_def)
 apply (elim conjE)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="t" in spec)
 apply (drule_tac x="X1" in spec)
 apply (drule_tac x="X2" in spec)
 apply (drule_tac x="{a. a : Y & (a = Tick | a : Ev ` X) & s ^^ <a> ~:t traces(P)} Un
                     {a. a : Y & a ~= Tick & a ~: Ev ` X}" in spec)
 apply (drule_tac x="{a. a : Y & (a = Tick | a : Ev ` X) & t ^^ <a> ~:t traces(Q)} Un
                     {a. a : Y & a ~= Tick & a ~: Ev ` X}" in spec)
 apply (simp)

 (* left *)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (drule_tac x="s ^^ <a>" in spec)
  apply (drule_tac x="t" in spec)
  apply (erule disjE)
  apply (simp add: par_tr_last)
  apply (fast)

  apply (erule disjE, simp)
  apply (simp add: HC_T2_def)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="t" in spec)
  apply (force)

 (* right *)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="t ^^ <a>" in spec)
  apply (erule disjE)
  apply (simp add: par_tr_last)
  apply (fast)

  apply (erule disjE)
  apply (simp add: HC_T2_def)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="t" in spec)
  apply (force)
  apply (simp)
 apply (simp)

(* notick s & notick t *)
apply (simp add: par_tr_noTick_decompo)
done

(* T3_F4 *)

lemma Parallel_T3_F4 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T3_F4 (traces(P |[X]| Q), failures(P |[X]| Q))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: par_tr_last)
apply (elim conjE exE)
apply (rule conjI)

 (* F4 *)
 apply (rule_tac x="Evset" in exI)
 apply (rule_tac x="Evset" in exI)
 apply (simp)
 apply (rule_tac x="s'" in exI)
 apply (rule_tac x="t'" in exI)
 apply (simp add: domF_def HC_F4_def)

 (* T3 *)
 apply (rule allI)
 apply (rule_tac x="Xa" in exI)
 apply (rule_tac x="Xa" in exI)
 apply (simp)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp add: domF_def HC_T3_def)
 apply (fast)
done

(*** Parallel_domF ***)

lemma Parallel_domF :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> (traces(P |[X]| Q), failures(P |[X]| Q)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Parallel_T2)
apply (simp add: Parallel_F3)
apply (simp add: Parallel_T3_F4)
done

(*--------------------------------*
 |            Hiding              |
 *--------------------------------*)

(*** T2 ***)

lemma Hiding_T2 :
  "(traces(P), failures(P)) : domF
   ==> HC_T2 (traces(P -- X), failures(P -- X))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (simp add: domF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
by (force)

(*** F3 ***)

lemma Hiding_F3 :
  "(traces(P), failures(P)) : domF
   ==> HC_F3 (traces(P -- X), failures(P -- X))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (rename_tac t Y Z s)
apply (rule_tac x="s" in exI, simp)

apply (simp add: domF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="Ev ` X Un Y" in spec)
apply (drule_tac x="Z - Ev ` X" in spec)
apply (simp)

apply (drule mp)
 apply (intro allI impI)
 apply (drule_tac x="a" in spec)
 apply (simp)

 apply (insert event_Tick_or_Ev)
 apply (drule_tac x="a" in spec)
 apply (erule disjE)
  (* Tick *)
  apply (drule_tac x="s ^^ <Tick>" in spec)
  apply (simp)
  (* Ev *)
  apply (elim conjE exE)
  apply (drule_tac x="s ^^ <Ev aa>" in spec)
  apply (simp)
  apply (subgoal_tac "aa ~: X", simp_all)
  apply (force)

apply (subgoal_tac "Ev ` X Un Y Un (Z - Ev ` X) = Ev ` X Un (Y Un Z)", simp)
by (auto)

(* T3_F4 *)

lemma Hiding_T3_F4 :
  "(traces(P), failures(P)) : domF
   ==> HC_T3_F4 (traces(P -- X), failures(P -- X))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (drule sym)
apply (simp add: hide_tr_decompo)
apply (elim conjE exE)
apply (rotate_tac -1)
apply (drule sym)

apply (subgoal_tac "(EX t''. t' = t'' ^^ <Tick> & sett t'' <= Ev ` X)")
 apply (elim conjE exE)
 apply (simp)

 (* F4 *)
 apply (rule conjI)
  apply (rule_tac x="s' ^^ t''" in exI)
  apply (simp)
  apply (subgoal_tac "t'' --tr X = <>", simp)
   apply (simp add: domF_def HC_F4_def)
   apply (elim conjE)
   apply (drule_tac x="s' ^^ t''" in spec)
   apply (subgoal_tac "noTick t''")
    apply (simp add: appt_assoc)
   apply (simp add: noTick_def)
   apply (force)
  apply (simp add: hide_tr_nilt_sett)

 (* T3 *)
 apply (rule allI)
 apply (rule_tac x="sa" in exI, simp)
 apply (simp add: domF_def HC_T3_def)
 apply (elim conjE)
 apply (drule_tac x="s' ^^ t''" in spec, simp)
 apply (subgoal_tac "noTick t''")
  apply (simp add: appt_assoc)
 apply (simp add: noTick_def)
 apply (force)

apply (auto simp add: hide_tr_Tick_sett)
done

(*** Hiding_domF ***)

lemma Hiding_domF :
  "(traces(P), failures(P)) : domF
   ==> (traces(P -- X), failures(P -- X)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Hiding_T2)
apply (simp add: Hiding_F3)
apply (simp add: Hiding_T3_F4)
done

(*--------------------------------*
 |           Renaming             |
 *--------------------------------*)

(*** T2 ***)

lemma Renaming_T2 :
  "(traces(P), failures(P)) : domF
   ==> HC_T2 (traces(P [[r]]), failures(P [[r]]))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (simp add: domF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
by (force)

(*** F3 ***)

lemma Renaming_F3 :
  "(traces(P), failures(P)) : domF
   ==> HC_F3 (traces(P [[r]]), failures(P [[r]]))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI, simp)

apply (simp add: domF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="[[r]]inv X" in spec)
apply (drule_tac x="[[r]]inv Y" in spec)

apply (drule mp)
 apply (simp add: ren_tr_noTick_right)
 apply (intro allI impI)
 apply (simp add: ren_inv_def)
 apply (erule bexE)
 apply (fold ren_inv_def)
 apply (drule_tac x="eb" in spec, simp)

  (* Tick *)
  apply (erule disjE)
  apply (drule_tac x=" sa ^^ <a>" in spec)
  apply (simp add: ren_tr_noTick_right)
  (* Ev *)
  apply (elim conjE exE)
  apply (drule_tac x=" sa ^^ <Ev aa>" in spec)
  apply (simp add: ren_tr_noTick_right)
by (simp)

(* T3_F4 *)

lemma Renaming_T3_F4 :
  "(traces(P), failures(P)) : domF
   ==> HC_T3_F4 (traces(P [[r]]), failures(P [[r]]))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: ren_tr_appt_decompo)
apply (elim conjE exE)
apply (case_tac "~ noTick s1", simp)
apply (simp)

 (* F4 *)
 apply (rule conjI)
 apply (rule_tac x="s1" in exI, simp)
 apply (simp add: domF_def HC_F4_def)
 apply (elim conjE)
 apply (drule_tac x="s1" in spec, simp)
 apply (rule memF_F2, simp, simp)

 (* T3 *)
 apply (rule allI)
 apply (rule_tac x="s1 ^^ <Tick>" in exI)
 apply (simp add: domF_def HC_T3_def)
 apply (fast)
done

(*** Renaming_domF ***)

lemma Renaming_domF :
  "(traces(P), failures(P)) : domF
   ==> (traces(P [[r]]), failures(P [[r]])) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Renaming_T2)
apply (simp add: Renaming_F3)
apply (simp add: Renaming_T3_F4)
done

(*--------------------------------*
 |           Seq_compo            |
 *--------------------------------*)

(*** T2 ***)

lemma Seq_compo_T2 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T2 (traces(P ;; Q), failures(P ;; Q))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI)
apply (rule conjI)

 (* case 1 *)
 apply (intro impI)
 apply (rule disjI1)
 apply (rule_tac x="s" in exI, simp)
 apply (simp add: domF_def HC_T2_def)
 apply (elim conjE)
 apply (drule_tac x="s" in spec)
 apply (force)

 (* case 2 *)
 apply (intro impI)
 apply (elim conjE exE disjE)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp add: domF_def HC_T2_def)
 apply (elim conjE)
 apply (rotate_tac 4)
 apply (drule_tac x="t" in spec)
 apply (force)
done

(*** F3 ***)

lemma Seq_compo_F3 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_F3 (traces(P ;; Q), failures(P ;; Q))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE disjE)

 (* case 1 *)
 apply (simp add: domF_def HC_F3_def)
 apply (elim conjE)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="insert Tick X" in spec)
 apply (drule_tac x="Y-{Tick}" in spec)
 apply (simp)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (simp add: not_Tick_to_Ev)
  apply (elim conjE exE, simp)
  apply (rotate_tac -3)
  apply (drule_tac x="s ^^ <Ev aa>" in spec, simp)
 apply (subgoal_tac 
   "insert Tick (X Un (Y - {Tick})) = insert Tick (X Un Y)", simp)
 apply (force)

 (* case 2 *)
 apply (simp add: domF_def HC_F3_def)
 apply (elim conjE)
 apply (rotate_tac -2)
 apply (drule_tac x="t" in spec)
 apply (drule_tac x="X" in spec)
 apply (drule_tac x="Y" in spec)
 apply (simp)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (elim conjE)
  apply (rotate_tac -1)
  apply (drule_tac x="sa" in spec)
  apply (rotate_tac -1)
  apply (drule_tac x="t ^^ <a>" in spec)
  apply (simp add: appt_assoc)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)
done

(* T3_F4 *)

lemma Seq_compo_T3_F4 :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> HC_T3_F4 (traces(P ;; Q), failures(P ;; Q))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE disjE)

 (* case 1 *)
 apply (elim conjE exE)
 apply (subgoal_tac "noTick (s ^^ <Tick>) ~= noTick (rmTick sa)", simp)
 apply (simp (no_asm_use))
 apply (drule sym)
 apply (simp)

 (* case 2 *)
 apply (elim conjE exE)
 apply (case_tac "~ noTick sa", simp)
 apply (insert trace_last_nil_or_unnil)
 apply (drule_tac x="t" in spec)
 apply (simp)
  (* <> *)
  apply (erule disjE)
  apply (rotate_tac -5)
  apply (drule_tac sym, simp)   (* contradict *)

  (* ... <Tick> *)
  apply (elim conjE exE, simp)
  apply (simp add: appt_assoc_sym)
  apply (erule conjE)
  apply (rule conjI)

   (* F4 *)
   apply (rule disjI2)
   apply (rule_tac x="sa" in exI)
   apply (rule_tac x="sb" in exI)
   apply (simp add: domF_def HC_F4_def)

   (* T3 *)
   apply (rule allI)
   apply (rule_tac x="sa" in exI)
   apply (rule_tac x="t" in exI)
   apply (simp add: appt_assoc_sym domF_def HC_T3_def)
done

(*** Seq_compo_domF ***)

lemma Seq_compo_domF :
  "[| (traces(P), failures(P)) : domF ; 
      (traces(Q), failures(Q)) : domF |]
     ==> (traces(P ;; Q), failures(P ;; Q)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Seq_compo_T2)
apply (simp add: Seq_compo_F3)
apply (simp add: Seq_compo_T3_F4)
done

(*--------------------------------*
 |          Depth_rest            |
 *--------------------------------*)

(*** T2 ***)

lemma Depth_rest_T2 :
  "(traces(P), failures(P)) : domF
   ==> HC_T2 (traces(P |. n), failures(P |. n))"
apply (simp add: HC_T2_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: domF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
by (force)

(*** F3 ***)

lemma Depth_rest_F3 :
  "(traces(P), failures(P)) : domF
   ==> HC_F3 (traces(P |. n), failures(P |. n))"
apply (simp add: HC_F3_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)

apply (simp add: domF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
apply (drule_tac x="Y" in spec)
apply (simp)
apply (erule disjE)
apply (simp)
apply (simp)
apply (elim conjE exE)
apply (simp)
done

(* T3_F4 *)

lemma Depth_rest_T3_F4 :
  "(traces(P), failures(P)) : domF
   ==> HC_T3_F4 (traces(P |. n), failures(P |. n))"
apply (simp add: HC_T3_F4_def in_traces in_failures)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp)

 (* F4 *)
 apply (rule conjI)
 apply (simp add: domF_def HC_F4_def)

 (* T3 *)
 apply (simp add: domF_def HC_T3_def)
 apply (case_tac "Suc (lengtht s) < n")
 apply (simp)
 apply (simp)
 apply (fast)
done

(*** Depth_rest_domF ***)

lemma Depth_rest_domF :
  "(traces(P), failures(P)) : domF
   ==> (traces(P |. n), failures(P |. n)) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: Depth_rest_T2)
apply (simp add: Depth_rest_F3)
apply (simp add: Depth_rest_T3_F4)
done

(*--------------------------------*
 |             proc               |
 *--------------------------------*)

lemma proc_domF[simp]: "(traces(P), failures(P)) : domF"
apply (induct_tac P)
apply (simp add: STOP_domF)
apply (simp add: SKIP_domF)
apply (simp add: DIV_domF)

apply (simp add: Act_prefix_domF)
apply (simp add: Ext_pre_choice_domF)
apply (simp add: Ext_choice_domF)
apply (simp add: Int_choice_domF)
apply (simp add: Rep_int_choice_domF)
apply (simp add: IF_domF)
apply (simp add: Parallel_domF)
apply (simp add: Hiding_domF)
apply (simp add: Renaming_domF)
apply (simp add: Seq_compo_domF)
apply (simp add: Depth_rest_domF)
done

(*--------------------------------*
 |          fstF sndF             |
 *--------------------------------*)

lemma fstF_proc_domF[simp]: "fstF (traces(P),, failures(P)) = traces(P)"
by (simp add: pairF)

lemma sndF_proc_domF[simp]: "sndF (traces(P),, failures(P)) = failures(P)"
by (simp add: pairF)

lemma fstF_semF[simp]: "fstF [[P]]F = traces(P)"
by (simp add: semF_def)

lemma sndF_semF[simp]: "sndF [[P]]F = failures(P)"
by (simp add: semF_def)

(*--------------------------------*
 |          =F and <=F            |
 *--------------------------------*)

lemma cspF_eqF_semantics:
  "(P =F Q) = ((traces P = traces Q) & (failures P = failures Q))"
apply (simp add: eqF_def)
apply (simp add: eqF_decompo)
done

lemma cspF_eqF_eqT_semantics:
  "(P =F Q) = ((P =T Q) & (failures P = failures Q))"
apply (simp add: eqT_def)
apply (simp add: semT_def)
apply (simp add: cspF_eqF_semantics)
done

lemma cspF_refF_semantics:
  "(P <=F Q) = ((traces Q <= traces P) & (failures Q <= failures P))"
apply (simp add: refF_def)
apply (simp add: subdomF_decompo)
done

lemma cspF_refF_refT_semantics:
  "(P <=F Q) = ((P <=T Q) & (failures Q <= failures P))"
apply (simp add: refT_def)
apply (simp add: semT_def)
apply (simp add: cspF_refF_semantics)
done

lemma cspF_eqF_prod_semantics:
  "(f =F' g) = 
   ((ALL x. traces (f x) = traces(g x)) & 
    (ALL x. failures (f x) = failures (g x)))"
apply (simp add: eqF_prod_def)
apply (simp add: cspF_eqF_semantics)
by (auto)

lemma cspF_eqF_prod_eqT_semantics:
  "(f =F' g) = 
   (f =T' g &
    (ALL x. failures (f x) = failures (g x)))"
apply (simp add: eqT_prod_def)
apply (simp add: eqT_def)
apply (simp add: semT_def)
apply (simp add: cspF_eqF_prod_semantics)
done

lemma cspF_refF_prod_semantics:
  "(f <=F' g) = 
   ((ALL x. traces (g x) <= traces(f x)) & 
    (ALL x. failures (g x) <= failures (f x)))"
apply (simp add: refF_prod_def)
apply (simp add: cspF_refF_semantics)
apply (rule iffI)
by (auto)

lemma cspF_refF_prod_eqT_semantics:
  "(f <=F' g) = 
   (f <=T' g &
    (ALL x. failures (g x) <= failures (f x)))"
apply (simp add: refT_prod_def)
apply (simp add: refT_def)
apply (simp add: semT_def)
apply (simp add: cspF_refF_prod_semantics)
done

lemmas cspF_semantics = cspF_eqF_semantics  cspF_refF_semantics
                        cspF_eqF_prod_semantics cspF_refF_prod_semantics

lemmas cspF_cspT_semantics = cspF_eqF_eqT_semantics  cspF_refF_refT_semantics
                             cspF_eqF_prod_eqT_semantics cspF_refF_prod_eqT_semantics

(*--------------------------------*
 |            Timeout             |
 *--------------------------------*)

lemma in_failures_Timeout1: 
  "(f :f failures(P [> Q)) =
   (f :f failures(Q) |
   (EX s X. f = (s, X) & s ~= <> & (s, X) :f failures(P)) |
   (EX X. f = (<>, X) & X <= Evset & <Tick> :t traces(P)))"
apply (rule)

(* <= *)
 apply (simp add: in_failures)
 apply (elim conjE exE disjE)
 apply (simp_all)
 apply (simp add: in_traces)
 apply (rule disjI1)
 apply (rule domF_F2_F4, simp_all)

 (* <= *)
 apply (simp add: in_failures in_traces)
 apply (elim conjE exE disjE, simp_all)
 apply (auto elim: memF_pairE)
done

lemma in_failures_Timeout2:
  "(f :f failures(P [>def Q)) =
   (f :f failures(Q) |
   (EX s X. f = (s, X) & s ~= <> & (s, X) :f failures(P)) |
   (EX X. f = (<>, X) & X <= Evset & <Tick> :t traces(P)))"
apply (simp add: Timeout_def)
apply (simp add: in_failures_Timeout1)
done

lemmas in_failures_Timeout = in_failures_Timeout1 in_failures_Timeout2

(*--------------------------------*
 |           Depth rest           |
 *--------------------------------*)

lemma semF_Depth_rest: "[[P |. n]]F = [[P]]F .|. n"
apply (simp add: semF_def)
apply (simp add: traces.simps)
apply (simp add: failures.simps)
apply (simp add: rest_domF_def)
apply (simp add: restTF_def)
apply (simp add: pairF_def)
apply (simp add: Abs_domF_inverse)
apply (simp add: pair_restriction_def)
done

(*---------------------------------------------------*
 |         Healthiness conditions for proc           |
 *---------------------------------------------------*)

lemma proc_T2:
    "(s, X) :f failures(P) ==> s :t traces(P)"
apply (insert pairF_domF_T2[of "s" "X" "(traces(P),, failures(P))"])
by (simp)

lemma proc_T3:
  "[| s ^^ <Tick> :t traces(P) ; noTick s |]
   ==> (s ^^ <Tick>, X) :f failures(P)"
apply (insert pairF_domF_T3[of "s" "(traces(P),, failures(P))" "X"])
by (simp)

lemma proc_T3_Tick:
  "<Tick> :t traces(P) ==> (<Tick>, X) :f failures(P)"
apply (insert proc_T3[of "<>" P X])
by (simp)

lemma proc_F4:
  "[| s ^^ <Tick> :t traces(P) ; noTick s |]
   ==> (s, Evset) :f failures(P)"
apply (insert pairF_domF_F4[of "s" "(traces(P),, failures(P))"])
by (simp)

lemma proc_F3:
  "[| (s, X) :f failures(P) ; noTick s ;
      (ALL a. a : Y --> s ^^ <a> ~:t  traces(P)) |]
   ==> (s, X Un Y) :f  failures(P)"
apply (insert pairF_domF_F3[of "s" "X" "(traces(P),, failures(P))" "Y"])
by (simp)

lemma proc_F3I:
  "[| (s, X) :f failures(P) ; noTick s ;
      (ALL a. a : Y --> s ^^ <a> ~:t traces(P)) ;
      Z = X Un Y |]
   ==> (s, Z) :f failures(P)"
by (simp add: proc_F3)

(*** F2_F4 ***)

lemma proc_F2_F4:
  "[| s ^^ <Tick> :t  traces(P) ; noTick s ; X <= Evset|]
   ==> (s, X) :f failures(P)"
apply (insert pairF_domF_F2_F4[of "s" "(traces(P),, failures(P))" "X"])
by (simp)

(*** T2_T3 ***)

lemma proc_T2_T3:
  "[| (s ^^ <Tick>, X) :f failures(P) ; noTick s |] 
  ==> (s ^^ <Tick>, Y) :f failures(P)"
apply (rule proc_T3)
apply (rule proc_T2)
by (simp_all)

(*------------------------------------------------------*
 |   Union in domF  (used for generic internal choice   |
 *------------------------------------------------------*)

lemma non_empty_UnionT_UnionF_T2:
 "Ps ~= {} ==>
  HC_T2 (UnionT {traces P |P. P : Ps} , UnionF {failures P |P. P : Ps})"
apply (simp add: HC_T2_def)
apply (intro allI impI)
apply (subgoal_tac "{traces P |P. P : Ps} ~= {}")
apply (simp)
apply (elim conjE bexE exE)
apply (simp)
apply (rule_tac x="traces Pa" in exI)
apply (rule conjI)
apply (rule_tac x="Pa" in exI)
apply (simp)
apply (simp add: proc_T2)
by (auto)

lemma non_empty_UnionT_UnionF_F3:
 "Ps ~= {} ==>
  HC_F3 (UnionT {traces P |P. P : Ps} , UnionF {failures P |P. P : Ps})"
apply (simp add: HC_F3_def)
apply (intro allI impI)
apply (subgoal_tac "{traces P |P. P : Ps} ~= {}")
apply (simp)
apply (elim conjE exE)
apply (simp)
apply (rule_tac x="failures Pa" in exI)
apply (rule conjI)
apply (rule_tac x="Pa" in exI)
apply (simp)
apply (rule proc_F3)
apply (simp_all)
apply (intro allI impI)
apply (drule_tac x="a" in spec)
apply (simp)
apply (drule_tac x="traces Pa" in spec)
apply (erule disjE)
apply (drule_tac x="Pa" in spec)
apply (simp)
apply (simp)
apply (auto)
done

lemma non_empty_UnionT_UnionF_T3_F4:
 "Ps ~= {} ==>
  HC_T3_F4 (UnionT {traces P |P. P : Ps} , UnionF {failures P |P. P : Ps})"
apply (simp add: HC_T3_F4_def)
apply (intro allI impI)
apply (subgoal_tac "{traces P |P. P : Ps} ~= {}")
apply (simp)
apply (elim conjE bexE exE)
apply (simp)
apply (rule conjI)
 apply (rule_tac x="failures Pa" in exI)
 apply (rule conjI)
 apply (fast)
 apply (rule proc_F4)
 apply (simp_all)

 apply (rule allI)
 apply (rule_tac x="failures Pa" in exI)
 apply (rule conjI)
 apply (fast)
 apply (rule proc_T3)
 apply (simp_all)
by (auto)

lemma non_empty_UnionT_UnionF_domF:
 "Ps ~= {} ==>
  (UnionT {traces P |P. P : Ps} , UnionF {failures P |P. P : Ps}) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: non_empty_UnionT_UnionF_T2)
apply (simp add: non_empty_UnionT_UnionF_F3)
apply (simp add: non_empty_UnionT_UnionF_T3_F4)
done

(*------------------------------------------------------*
 |   Union in domF  (used for generic internal choice   |
 *------------------------------------------------------*)

lemma UnionT_UnionF_T2:
 "HC_T2 ({t. t = <> | (EX P:Ps. t :t traces(P)) }t ,
         {f. EX P:Ps. f :f failures(P)}f )"
apply (simp add: HC_T2_def)
apply (intro allI impI)
apply (simp add: in_traces_Union_proc)
apply (simp add: in_failures_Union_proc)
apply (elim conjE bexE exE)
apply (rule disjI2)
apply (rule_tac x="P" in bexI)
apply (simp add: proc_T2)
apply (simp)
done

lemma UnionT_UnionF_F3:
 "HC_F3 ({t. t = <> | (EX P:Ps. t :t traces(P)) }t ,
         {f. EX P:Ps. f :f failures(P)}f )"
apply (simp add: HC_F3_def)
apply (intro allI impI)
apply (simp add: in_traces_Union_proc)
apply (simp add: in_failures_Union_proc)
apply (elim conjE bexE exE)
apply (simp)
apply (rule_tac x="P" in bexI)
apply (rule proc_F3)
apply (simp_all)
done

lemma UnionT_UnionF_T3_F4:
 "HC_T3_F4 ({t. t = <> | (EX P:Ps. t :t traces(P)) }t ,
            {f. EX P:Ps. f :f failures(P)}f )"
apply (simp add: HC_T3_F4_def)
apply (intro allI impI)
apply (simp add: in_traces_Union_proc)
apply (simp add: in_failures_Union_proc)
apply (elim conjE bexE exE)
apply (simp)
apply (elim bexE)
apply (rule conjI)
 apply (rule_tac x="P" in bexI)
 apply (rule proc_F4)
 apply (simp_all)

 apply (rule allI)
 apply (rule_tac x="P" in bexI)
 apply (rule proc_T3)
 apply (simp_all)
done

lemma UnionT_UnionF_domF:
 "({t. t = <> | (EX P:Ps. t :t traces(P)) }t ,
            {f. EX P:Ps. f :f failures(P)}f) : domF"
apply (simp (no_asm) add: domF_iff)
apply (simp add: UnionT_UnionF_T2)
apply (simp add: UnionT_UnionF_F3)
apply (simp add: UnionT_UnionF_T3_F4)
done

(****************** to add them again ******************)

declare disj_not1   [simp]

end