Theory CSP_F_contraction

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

theory CSP_F_contraction = CSP_F_failuresfun + CSP_T_contraction:

(*****************************************************************

         1. contraction failuresfun
         2. contraction failuresFun
         3. contraction [[ ]]Ffun
         4. contraction [[ ]]FFun

 *****************************************************************)

(*=============================================================*
 |                    tracesfun fstF                           |
 *=============================================================*)

lemma non_expanding_tracesfun_fstF:
   "Pf : nohidefun
    ==> non_expanding (%SFf. tracesfun Pf (fstF o SFf))"
apply (subgoal_tac "(%SFf. tracesfun Pf (fstF o SFf)) = (tracesfun Pf) o (op o fstF)")
apply (simp)
apply (rule compo_non_expand)
apply (simp add: non_expanding_tracesfun)
apply (simp add: non_expanding_op_fstF)
apply (simp add: expand_fun_eq)
done

lemma contraction_alpha_tracesfun_fstF:
   "Pf : gProcfun
    ==> contraction_alpha (%SFf. tracesfun Pf (fstF o SFf)) (1/2)"
apply (subgoal_tac "(%SFf. tracesfun Pf (fstF o SFf)) = (tracesfun Pf) o (op o fstF)")
apply (simp)
apply (rule compo_contra_alpha_non_expand)
apply (simp add: contraction_alpha_tracesfun)
apply (simp add: non_expanding_op_fstF)
apply (simp add: expand_fun_eq)
done

(*--------------------------------*
 |        STOP,SKIP,DIV           |
 *--------------------------------*)

(*** STOP ***)

lemma map_alpha_failuresfun_STOP: 
  "0 <= alpha ==> map_alpha (failuresfun (%SFf. STOP)) alpha"
by (simp add: failuresfun_simp map_alpha_Constant)

lemma non_expanding_failuresfun_STOP: 
  "non_expanding (failuresfun (%SFf. STOP))"
by (simp add: non_expanding_def map_alpha_failuresfun_STOP)

lemma contraction_alpha_failuresfun_STOP: 
  "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (failuresfun (%SFf. STOP)) alpha"
by (simp add: failuresfun_simp contraction_alpha_Constant)

(*** SKIP ***)

lemma map_alpha_failuresfun_SKIP: 
  "0 <= alpha ==> map_alpha (failuresfun (%SFf. SKIP)) alpha"
by (simp add: failuresfun_simp map_alpha_Constant)

lemma non_expanding_failuresfun_SKIP: 
  "non_expanding (failuresfun (%SFf. SKIP))"
by (simp add: non_expanding_def map_alpha_failuresfun_SKIP)

lemma contraction_alpha_failuresfun_SKIP: 
  "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (failuresfun (%SFf. SKIP)) alpha"
by (simp add: failuresfun_simp contraction_alpha_Constant)

(*** DIV ***)

lemma map_alpha_failuresfun_DIV: 
  "0 <= alpha ==> map_alpha (failuresfun (%SFf. DIV)) alpha"
by (simp add: failuresfun_simp map_alpha_Constant)

lemma non_expanding_failuresfun_DIV: 
  "non_expanding (failuresfun (%SFf. DIV))"
by (simp add: non_expanding_def map_alpha_failuresfun_DIV)

lemma contraction_alpha_failuresfun_DIV: 
  "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (failuresfun (%SFf. DIV)) alpha"
by (simp add: failuresfun_simp contraction_alpha_Constant)

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

lemma contraction_half_failures_Act_prefix_lm: 
   "distance (failures (a -> P), failures (a -> Q)) * 2
    = distance (failures P, failures Q)"
apply (rule sym)
apply (rule rest_Suc_dist_half[simplified])
apply (rule allI)
apply (simp add: rest_setF_eq_iff)
apply (rule iffI)

 (* => *)
 apply (intro allI)
 apply (simp add: in_failures)
 apply (rule iffI)

  (* => *)
  apply (elim conjE exE disjE)
   apply (simp_all)
   apply (drule_tac x="sa" in spec)
   apply (drule_tac x="X" in spec)
   apply (simp)

   apply (drule_tac x="sa" in spec)
   apply (drule_tac x="X" in spec)
   apply (simp)
   apply (erule iffE, simp)
   apply (insert trace_last_nil_or_unnil)
   apply (drule_tac x="sa" in spec)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (simp add: appt_assoc_sym)
   apply (drule mp, fast)
   apply (simp)
   apply (rule_tac x="<Ev a> ^^ sb" in exI)
   apply (simp)

  (* <= *)
  apply (elim conjE exE disjE)
   apply (simp_all)
   apply (drule_tac x="sa" in spec)
   apply (drule_tac x="X" in spec)
   apply (simp)

   apply (drule_tac x="sa" in spec)
   apply (drule_tac x="X" in spec)
   apply (simp)
   apply (erule iffE, simp)
   apply (drule_tac x="sa" in spec)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (simp add: appt_assoc_sym)
   apply (drule mp, fast)
   apply (simp)

 (* <= *)
 apply (intro allI)
 apply (drule_tac x="<Ev a> ^^ s" in spec)
 apply (drule_tac x="X" in spec)
 apply (simp add: in_failures)
 apply (rule iffI)

  (* => *)
  apply (elim conjE exE disjE)
   apply (simp)
   apply (erule iffE, simp)
   apply (simp add: appt_assoc_sym)
   apply (drule mp, force)
   apply (force)

  (* <= *)
  apply (elim conjE exE disjE)
   apply (simp)
   apply (erule iffE, simp)
   apply (simp add: appt_assoc_sym)
   apply (drule mp, force)
   apply (force)
done

(***  contraction_half ***)

lemma contraction_half_failuresfun_Act_prefix: 
 "non_expanding (failuresfun Pf)
  ==> contraction_alpha (failuresfun (%f. a -> Pf f)) (1 / 2)"
apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def)
apply (intro allI)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
apply (simp add: contraction_half_failures_Act_prefix_lm)
done

(***  contraction ***)

lemma contraction_failuresfun_Act_prefix: 
 "non_expanding (failuresfun Pf)
  ==> contraction (failuresfun (%f. a -> Pf f))"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
by (simp add: contraction_half_failuresfun_Act_prefix)

(*** non_expanding ***)

lemma non_expanding_failuresfun_Act_prefix: 
 "non_expanding (failuresfun Pf)
  ==> non_expanding (failuresfun (%f. a -> Pf f))"
apply (rule contraction_non_expanding)
by (simp add: contraction_failuresfun_Act_prefix)

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

(*** rest_setF (subset) ***)

lemma Ext_pre_choice_Act_prefix_rest_setF_sub:
   "[| ALL a : X.
         failures (a -> Pf a) .|. n <= failures (a -> Qf a) .|. n |]
    ==> failures (? a:X -> Pf a) .|. n <=
        failures (? a:X -> Qf a) .|. n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_failures)
apply (elim conjE exE disjE, simp_all)

 apply (drule_tac x="a" in bspec, simp)
 apply (drule_tac x="<Ev a> ^^ sa" in spec)
 apply (drule_tac x="Xa" in spec)
 apply (simp)

 apply (drule_tac x="a" in bspec, simp)
 apply (drule_tac x="s' ^^ <Tick>" in spec)
 apply (drule_tac x="Xa" in spec)
 apply (auto)
done

(*** rest_setF (equal) ***)

lemma Ext_pre_choice_Act_prefix_rest_setF:
   "[| ALL a : X.
         failures (a -> Pf a) .|. n = failures (a -> Qf a) .|. n |]
    ==> failures (? a:X -> Pf a) .|. n =
        failures (? a:X -> Qf a) .|. n"
apply (rule order_antisym)
by (simp_all add: Ext_pre_choice_Act_prefix_rest_setF_sub)

(*** distF lemma ***)

lemma Ext_pre_choice_Act_prefix_distF_nonempty:
"[| X ~= {} ; PQs = {(failures (a -> Pf a), failures (a -> Qf a))|a. a : X} |]
 ==> (EX PQ. PQ:PQs & 
             distance(failures (? a:X -> Pf a), failures (? a:X -> Qf a))
          <= distance(fst PQ, snd PQ))"
apply (rule rest_to_dist_pair)
apply (force)

apply (intro allI impI)
apply (rule Ext_pre_choice_Act_prefix_rest_setF)
apply (rule ballI)
apply (simp)
apply (drule_tac x="failures (a -> Pf a)" in spec)
apply (drule_tac x="failures (a -> Qf a)" in spec)
by (auto)

(*** contraction lemma ***)

lemma contraction_half_failuresfun_Ext_pre_choice_lm:
  "[| X ~= {} ; ALL a. distance (failures (Pf a), failures (Qf a))
                    <= distance (x1, x2) |]
    ==> distance (failures (? a:X -> Pf a), failures (? a:X -> Qf a)) * 2 
     <= distance (x1, x2)"
apply (insert Ext_pre_choice_Act_prefix_distF_nonempty
       [of X "{(failures (a -> Pf a), failures (a -> Qf a)) |a. a : X}" Pf Qf])
apply (simp)
apply (elim conjE exE)
apply (simp)
apply (subgoal_tac 
    "distance (failures (aa -> Pf aa), failures (aa -> Qf aa)) * 2
   = distance (failures (Pf aa), failures (Qf aa))")
apply (drule_tac x="aa" in spec)
apply (force)
by (simp add: contraction_half_failures_Act_prefix_lm)

(*** contraction_half ***)

lemma contraction_half_failuresfun_Ext_pre_choice:
 "ALL a. non_expanding (failuresfun (Pff a))
  ==> contraction_alpha (failuresfun (%f. ? a:X -> (Pff a f))) (1 / 2)"
apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def)
apply (case_tac "X = {}")
apply (simp add: failuresfun_simp)
apply (simp add: failuresfun_def)
by (simp add: contraction_half_failuresfun_Ext_pre_choice_lm)

(*** Ext_pre_choice_evalT_contraction ***)

lemma contraction_failuresfun_Ext_pre_choice:
 "ALL a. non_expanding (failuresfun (Pff a))
  ==> contraction (failuresfun (%f. ? a:X -> (Pff a f)))"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
by (simp add: contraction_half_failuresfun_Ext_pre_choice)

(*** Ext_pre_choice_evalT_non_expanding ***)

lemma non_expanding_failuresfun_Ext_pre_choice:
 "ALL a. non_expanding (failuresfun (Pff a))
  ==> non_expanding (failuresfun (%f. ? a:X -> (Pff a f)))"
apply (rule contraction_non_expanding)
by (simp add: contraction_failuresfun_Ext_pre_choice)

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

(*** rest_domT (subset) ***)

lemma Ext_choice_rest_setF_sub:
   "[| traces P1 .|. n <= traces P2 .|. n ;
       traces Q1 .|. n <= traces Q2 .|. n ;
       failures P1 .|. n <= failures P2 .|. n ;
       failures Q1 .|. n <= failures Q2 .|. n  |]
    ==> failures (P1 [+] Q1) .|. n <= failures (P2 [+] Q2) .|. n"
apply (simp add: subdomT_iff subsetF_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_rest_setF)
apply (simp add: in_failures)
apply (elim conjE exE disjE, simp_all)

 apply (rotate_tac 2)
 apply (drule_tac x="s' ^^ <Tick>" in spec)
 apply (drule_tac x="X" in spec)
 apply (drule mp, simp, fast)
 apply (simp)

 apply (rotate_tac 3)
 apply (drule_tac x="s' ^^ <Tick>" in spec)
 apply (drule_tac x="X" in spec)
 apply (drule mp, simp, fast)
 apply (simp)
done

(*** rest_setF (equal) ***)

lemma Ext_choice_rest_setF:
   "[| traces P1 .|. n = traces P2 .|. n ;
       traces Q1 .|. n = traces Q2 .|. n ;
       failures P1 .|. n = failures P2 .|. n ;
       failures Q1 .|. n = failures Q2 .|. n  |]
    ==> failures (P1 [+] Q1) .|. n = failures (P2 [+] Q2) .|. n"
apply (rule order_antisym)
by (simp_all add: Ext_choice_rest_setF_sub)

(*** distF lemma ***)

lemma Ext_choice_distF:
"[| PQTs = {(traces P1, traces P2), (traces Q1, traces Q2)} ;
    PQFs = {(failures P1, failures P2), (failures Q1, failures Q2)} |]
 ==> (EX PQ. PQ:PQTs & 
             distance(failures (P1 [+] Q1), failures (P2 [+] Q2))
          <= distance((fst PQ), (snd PQ))) |
     (EX PQ. PQ:PQFs & 
             distance(failures (P1 [+] Q1), failures (P2 [+] Q2))
          <= distance((fst PQ), (snd PQ)))"
apply (rule rest_to_dist_pair_two)
apply (simp_all)
by (auto intro: Ext_choice_rest_setF)

(*** map_alpha F lemma ***)

lemma map_alpha_failuresfun_Ext_choice_lm:
  "[| distance (traces P1, traces P2) <= alpha * distance (x1, x2) ;
      distance (traces Q1, traces Q2) <= alpha * distance (x1, x2) ;
      distance (failures P1, failures P2) <= alpha * distance (x1, x2) ;
      distance (failures Q1, failures Q2) <= alpha * distance (x1, x2) |]
    ==> distance (failures (P1 [+] Q1), failures (P2 [+] Q2))
     <= alpha * distance (x1, x2)"
apply (insert Ext_choice_distF
       [of "{(traces P1, traces P2), (traces Q1, traces Q2)}" P1 P2 Q1 Q2
           "{(failures P1, failures P2), (failures Q1, failures Q2)}"])
by (auto)

(*** map_alpha ***)

lemma map_alpha_failuresfun_Ext_choice:
 "[| Pf : Procfun ; Qf : Procfun ;
     map_alpha (%SFf. tracesfun Pf (fstF o SFf)) alpha ; 
     map_alpha (%SFf. tracesfun Qf (fstF o SFf)) alpha ;
     map_alpha (failuresfun Pf) alpha ; map_alpha (failuresfun Qf) alpha |]
  ==> map_alpha (failuresfun (%f. (Pf f [+] Qf f))) alpha"
apply (simp add: map_alpha_def)
apply (intro allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
apply (simp add: tracesfun_def)
apply (simp add: traces_Pf_Proc_T_F)
by (simp add: map_alpha_failuresfun_Ext_choice_lm)

(*** non_expanding ***)

lemma non_expanding_failuresfun_Ext_choice:
 "[| Pf : Procfun ; Qf : Procfun ;
     non_expanding (%SFf. tracesfun Pf (fstF o SFf)) ;
     non_expanding (%SFf. tracesfun Qf (fstF o SFf)) ;
     non_expanding (failuresfun Pf) ; non_expanding (failuresfun Qf) |]
  ==> non_expanding (failuresfun (%f. (Pf f [+] Qf f)))"
by (simp add: non_expanding_def map_alpha_failuresfun_Ext_choice)

(*** contraction ***)

lemma contraction_alpha_failuresfun_Ext_choice:
 "[| Pf : Procfun ; Qf : Procfun ;
     contraction_alpha (%SFf. tracesfun Pf (fstF o SFf)) alpha ;
     contraction_alpha (%SFf. tracesfun Qf (fstF o SFf)) alpha ;
     contraction_alpha (failuresfun Pf) alpha ; 
     contraction_alpha (failuresfun Qf) alpha|]
  ==> contraction_alpha (failuresfun (%f. (Pf f [+] Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_failuresfun_Ext_choice)

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

(*** rest_domT (subset) ***)

lemma Int_choice_rest_setF_sub:
   "[| failures P1 .|. n <= failures P2 .|. n ;
       failures Q1 .|. n <= failures Q2 .|. n  |]
    ==> failures (P1 |~| Q1) .|. n <= failures (P2 |~| Q2) .|. n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_failures)
apply (elim disjE conjE exE)
by (force)+

(*** rest_setF (equal) ***)

lemma Int_choice_rest_setF:
   "[| failures P1 .|. n = failures P2 .|. n ;
       failures Q1 .|. n = failures Q2 .|. n  |]
    ==> failures (P1 |~| Q1) .|. n = failures (P2 |~| Q2) .|. n"
apply (rule order_antisym)
by (simp_all add: Int_choice_rest_setF_sub)

(*** distF lemma ***)

lemma Int_choice_distF:
"PQs = {(failures P1, failures P2), (failures Q1, failures Q2)}
 ==> (EX PQ. PQ:PQs & 
             distance(failures (P1 |~| Q1), failures (P2 |~| Q2))
          <= distance((fst PQ), (snd PQ)))"
apply (rule rest_to_dist_pair)
by (auto intro: Int_choice_rest_setF)

(*** map_alpha F lemma ***)

lemma map_alpha_failuresfun_Int_choice_lm:
  "[| distance (failures P1, failures P2) <= alpha * distance (x1, x2) ;
      distance (failures Q1, failures Q2) <= alpha * distance (x1, x2) |]
    ==> distance (failures (P1 |~| Q1), failures (P2 |~| Q2))
     <= alpha * distance (x1, x2)"
apply (insert Int_choice_distF
       [of "{(failures P1, failures P2), (failures Q1, failures Q2)}" P1 P2 Q1 Q2])
by (auto)

(*** map_alpha ***)

lemma map_alpha_failuresfun_Int_choice:
 "[| map_alpha (failuresfun Pf) alpha ; map_alpha (failuresfun Qf) alpha |]
  ==> map_alpha (failuresfun (%f. (Pf f |~| Qf f))) alpha"
apply (simp add: map_alpha_def)
apply (intro allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
by (simp add: map_alpha_failuresfun_Int_choice_lm)

(*** non_expanding ***)

lemma non_expanding_failuresfun_Int_choice:
 "[| non_expanding (failuresfun Pf) ; non_expanding (failuresfun Qf) |]
  ==> non_expanding (failuresfun (%f. (Pf f |~| Qf f)))"
by (simp add: non_expanding_def map_alpha_failuresfun_Int_choice)

(*** contraction ***)

lemma contraction_alpha_failuresfun_Int_choice:
 "[| contraction_alpha (failuresfun Pf) alpha ; 
     contraction_alpha (failuresfun Qf) alpha|]
  ==> contraction_alpha (failuresfun (%f. (Pf f |~| Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_failuresfun_Int_choice)

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

(*** rest_setF (subset) ***)

lemma Rep_int_choice_rest_setF_sub:
   "[| ALL c : C.
         failures (Pf c) .|. n <= failures (Qf c) .|. n |]
    ==> failures (!! :C .. Pf) .|. n <=
        failures (!! :C .. Qf) .|. n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_failures)
apply (elim conjE bexE)
apply (rule_tac x="c" in bexI)
by (auto)

(*** rest_setF (equal) ***)

lemma Rep_int_choice_rest_setF:
   "[| ALL c : C.
         failures (Pf c) .|. n = failures (Qf c) .|. n |]
    ==> failures (!! :C .. Pf) .|. n =
        failures (!! :C .. Qf) .|. n"
apply (rule order_antisym)
by (simp_all add: Rep_int_choice_rest_setF_sub)

(*** distF lemma ***)

lemma Rep_int_choice_distF_nonempty:
"[| C ~= {} ; PQs = {(failures (Pf c), failures (Qf c))|c. c : C} |]
 ==> (EX PQ. PQ:PQs & 
             distance(failures (!! :C .. Pf), failures (!! :C .. Qf))
          <= distance(fst PQ, snd PQ))"
apply (rule rest_to_dist_pair)
apply (fast)

apply (intro allI impI)
apply (rule Rep_int_choice_rest_setF)
by (auto)

(*** map_alpha F lemma ***)

lemma map_alpha_failuresfun_Rep_int_choice_lm:
"[| C ~= {} ; ALL c. distance (failures (Pf c), failures (Qf c)) 
                  <= alpha * distance (x1, x2) |]
 ==> distance(failures (!! :C .. Pf), failures (!! :C .. Qf))
  <= alpha * distance(x1, x2)"
apply (insert Rep_int_choice_distF_nonempty
       [of C "{(failures (Pf c), failures (Qf c))|c. c : C}" Pf Qf])
apply (simp)
apply (elim conjE exE, simp)
apply (drule_tac x="c" in spec)
by (force)

(*** map_alpha ***)

lemma map_alpha_failuresfun_Rep_int_choice:
 "ALL c. map_alpha (failuresfun (Pff c)) alpha
  ==> map_alpha (failuresfun (%f. !! c:C .. (Pff c f))) alpha"
apply (simp add: map_alpha_def)
apply (case_tac "C = {}")
 apply (simp add: failuresfun_simp)
 apply (simp add: real_mult_order_eq)
apply (simp add: failuresfun_def)
apply (simp add: map_alpha_failuresfun_Rep_int_choice_lm)
done

(*** non_expanding ***)

lemma non_expanding_failuresfun_Rep_int_choice:
 "ALL c. non_expanding (failuresfun (Pff c))
  ==> non_expanding (failuresfun (%f. !! c:C .. (Pff c f)))"
by (simp add: non_expanding_def map_alpha_failuresfun_Rep_int_choice)

(*** Rep_int_choice_evalT_contraction_alpha ***)

lemma contraction_alpha_failuresfun_Rep_int_choice:
 "ALL c. contraction_alpha (failuresfun (Pff c)) alpha 
     ==> contraction_alpha (failuresfun (%f. !! c:C .. (Pff c f))) alpha"
by (simp add: contraction_alpha_def map_alpha_failuresfun_Rep_int_choice)

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

(*** rest_setF (subset) ***)

lemma IF_rest_setF_sub:
   "[| failures P1 .|. n <= failures P2 .|. n ;
       failures Q1 .|. n <= failures Q2 .|. n  |]
    ==> failures (IF b THEN P1 ELSE Q1) .|. n <= 
        failures (IF b THEN P2 ELSE Q2) .|. n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_failures)
done

(*** rest_setF (equal) ***)

lemma IF_rest_setF:
   "[| failures P1 .|. n = failures P2 .|. n ;
       failures Q1 .|. n = failures Q2 .|. n  |]
    ==> failures (IF b THEN P1 ELSE Q1) .|. n = 
        failures (IF b THEN P2 ELSE Q2) .|. n"
apply (rule order_antisym)
by (simp_all add: IF_rest_setF_sub)

(*** distF lemma ***)

lemma IF_distF:
   "PQs = {(failures P1, failures P2), (failures Q1, failures Q2)}
    ==> (EX PQ. PQ:PQs & 
             distance(failures (IF b THEN P1 ELSE Q1),
                      failures (IF b THEN P2 ELSE Q2))
          <= distance((fst PQ), (snd PQ)))"
apply (rule rest_to_dist_pair)
by (auto intro: IF_rest_setF)

(*** map_alpha F lemma ***)

lemma map_alpha_failuresfun_IF_lm:
  "[| distance (failures P1, failures P2) <= alpha * distance (x1, x2) ;
      distance (failures Q1, failures Q2) <= alpha * distance (x1, x2) |]
    ==> distance(failures (IF b THEN P1 ELSE Q1),
                 failures (IF b THEN P2 ELSE Q2))
     <= alpha * distance (x1, x2)"
apply (insert IF_distF
       [of "{(failures P1, failures P2), (failures Q1, failures Q2)}" P1 P2 Q1 Q2 b])
by (auto)

(*** map_alpha ***)

lemma map_alpha_failuresfun_IF:
 "[| map_alpha (failuresfun Pf) alpha ; map_alpha (failuresfun Qf) alpha |]
  ==> map_alpha (failuresfun (%f. IF b THEN (Pf f) ELSE (Qf f))) alpha"
apply (simp add: map_alpha_def)
apply (intro allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
by (simp add: map_alpha_failuresfun_IF_lm)

(*** non_expanding ***)

lemma non_expanding_failuresfun_IF:
 "[| non_expanding (failuresfun Pf) ; non_expanding (failuresfun Qf) |]
  ==> non_expanding (failuresfun (%f. IF b THEN (Pf f) ELSE (Qf f)))"
by (simp add: non_expanding_def map_alpha_failuresfun_IF)

(*** contraction_alpha ***)

lemma contraction_alpha_failuresfun_IF:
 "[| contraction_alpha (failuresfun Pf) alpha ; contraction_alpha (failuresfun Qf) alpha|]
  ==> contraction_alpha (failuresfun (%f. IF b THEN (Pf f) ELSE (Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_failuresfun_IF)

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

(*** rest_setF (subset) ***)

lemma Parallel_rest_setF_sub:
   "[| failures P1 .|. n <= failures P2 .|. n ;
       failures Q1 .|. n <= failures Q2 .|. n  |]
    ==> failures (P1 |[X]| Q1) .|. n <= failures (P2 |[X]| Q2) .|. n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_failures)
apply (elim conjE exE)

apply (rule_tac x="Y" in exI)
apply (rule_tac x="Z" in exI)
apply (simp)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="t" in exI)
apply (simp)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="t" in spec)
apply (drule_tac x="Y" in spec)
apply (drule_tac x="Z" in spec)

apply (erule disjE, simp)    (* lengtht s < n *)
apply (erule par_tr_lengthtE)
apply (simp)

apply (elim conjE exE, simp) (* lengtht s = n *)
apply (simp add: par_tr_last)
apply (elim conjE exE, simp)
apply (erule par_tr_lengthtE)
apply (case_tac "Suc (lengtht s'a) < n", simp)
 apply (case_tac "Suc (lengtht t') < n", simp)
 apply (case_tac "Suc (lengtht t') = n", simp)
 apply (drule mp, force)
 apply (simp)
 apply (force)  (* contradict *)

 apply (case_tac "Suc (lengtht t') < n", simp)
 apply (drule mp)
  apply (rule_tac x="s'a" in exI, simp)
 apply (simp)

 apply (case_tac "Suc (lengtht t') = n", simp)
 apply (drule mp)
  apply (rule_tac x="s'a" in exI, simp)
 apply (drule mp)
  apply (rule_tac x="t'" in exI, simp)
 apply (simp)
 apply (force)  (* contradict *)
done

(*** rest_setF (equal) ***)

lemma Parallel_rest_setF:
   "[| failures P1 .|. n = failures P2 .|. n ;
       failures Q1 .|. n = failures Q2 .|. n  |]
    ==> failures (P1 |[X]| Q1) .|. n = failures (P2 |[X]| Q2) .|. n"
apply (rule order_antisym)
by (simp_all add: Parallel_rest_setF_sub)

(*** distF lemma ***)

lemma Parallel_distF:
"PQs = {(failures P1, failures P2), (failures Q1, failures Q2)}
 ==> (EX PQ. PQ:PQs & 
             distance(failures (P1 |[X]| Q1), failures (P2 |[X]| Q2))
          <= distance((fst PQ), (snd PQ)))"
apply (rule rest_to_dist_pair)
by (auto intro: Parallel_rest_setF)

(*** map_alpha F lemma ***)

lemma map_alpha_failuresfun_Parallel_lm:
  "[| distance (failures P1, failures P2) <= alpha * distance (x1, x2) ;
      distance (failures Q1, failures Q2) <= alpha * distance (x1, x2) |]
    ==> distance (failures (P1 |[X]| Q1), failures (P2 |[X]| Q2))
     <= alpha * distance (x1, x2)"
apply (insert Parallel_distF
       [of "{(failures P1, failures P2), (failures Q1, failures Q2)}" P1 P2 Q1 Q2 X])
by (auto)

(*** map_alpha ***)

lemma map_alpha_failuresfun_Parallel:
 "[| map_alpha (failuresfun Pf) alpha ; map_alpha (failuresfun Qf) alpha |]
  ==> map_alpha (failuresfun (%f. (Pf f |[X]| Qf f))) alpha"
apply (simp add: map_alpha_def)
apply (intro allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
by (simp add: map_alpha_failuresfun_Parallel_lm)

(*** non_expanding ***)

lemma non_expanding_failuresfun_Parallel:
 "[| non_expanding (failuresfun Pf) ; non_expanding (failuresfun Qf) |]
  ==> non_expanding (failuresfun (%f. (Pf f |[X]| Qf f)))"
by (simp add: non_expanding_def map_alpha_failuresfun_Parallel)

(*** contraction_alpha ***)

lemma contraction_alpha_failuresfun_Parallel:
 "[| contraction_alpha (failuresfun Pf) alpha ; 
     contraction_alpha (failuresfun Qf) alpha |]
  ==> contraction_alpha (failuresfun (%f. (Pf f |[X]| Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_failuresfun_Parallel)

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

(* cms rules for Hiding is not necessary 
   because processes are guarded. *)

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

(*** rest_setF (subset) ***)

lemma Renaming_rest_setF_sub:
   "failures P .|. n <= failures Q .|. n
    ==> failures (P [[r]]) .|. n <= failures (Q [[r]]) .|. n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_failures)
apply (elim conjE exE)

apply (rule_tac x="sa" in exI)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="[[r]]inv X" in spec)
apply (simp)

apply (erule disjE)
apply (simp add: ren_tr_lengtht)

apply (elim conjE exE)
apply (simp add: ren_tr_lengtht)
apply (simp add: ren_tr_appt_decompo_right)
apply (elim conjE exE, simp)
by (fast)

(*** rest_setF (equal) ***)

lemma Renaming_rest_setF:
   "failures P .|. n = failures Q .|. n
    ==> failures (P [[r]]) .|. n = failures (Q [[r]]) .|. n"
apply (rule order_antisym)
by (simp_all add: Renaming_rest_setF_sub)

(*** distF lemma ***)

lemma Renaming_distF:
     "distance(failures (P [[r]]), failures (Q [[r]])) <= 
      distance(failures P, failures Q)"
apply (rule rest_distance_subset)
by (auto intro: Renaming_rest_setF)

(*** map_alphaT lemma ***)

lemma map_alpha_failuresfun_Renaming_lm:
  "distance(failures P, failures Q) <= alpha * distance (x1, x2)
    ==> distance(failures (P [[r]]), failures (Q [[r]]))
     <= alpha * distance(x1, x2)"
apply (insert Renaming_distF[of P r Q])
by (simp)

(*** map_alpha ***)

lemma map_alpha_failuresfun_Renaming:
 "map_alpha (failuresfun Pf) alpha
  ==> map_alpha (failuresfun (%f. (Pf f) [[r]])) alpha"
apply (simp add: map_alpha_def)
apply (intro allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
by (simp add: map_alpha_failuresfun_Renaming_lm)

(*** non_expanding ***)

lemma non_expanding_failuresfun_Renaming:
 "non_expanding (failuresfun Pf)
  ==> non_expanding (failuresfun (%f. (Pf f) [[r]]))"
by (simp add: non_expanding_def map_alpha_failuresfun_Renaming)

(*** contraction_alpha ***)

lemma contraction_alpha_failuresfun_Renaming:
 "contraction_alpha (failuresfun Pf) alpha
  ==> contraction_alpha (failuresfun (%f. (Pf f) [[r]])) alpha"
by (simp add: contraction_alpha_def map_alpha_failuresfun_Renaming)

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

(*** rest_setF (subset) ***)

lemma Seq_compo_rest_setF_sub:
   "[| traces P1 .|. n <= traces P2 .|. n ;
       failures P1 .|. n <= failures P2 .|. n ;
       failures Q1 .|. n <= failures Q2 .|. n  |]
    ==> failures (P1 ;; Q1) .|. n <= failures (P2 ;; Q2) .|. n"
apply (simp add: subsetF_iff)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_rest_domT)
apply (simp add: in_failures)
apply (elim conjE exE disjE)
apply (simp_all)

 (* case 1 *)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)

 (* case 2 *)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)
 apply (drule_tac x=" sa ^^ <Tick>" in spec)
 apply (simp)

 apply (insert trace_last_nil_or_unnil)
 apply (rotate_tac -1)
 apply (drule_tac x="t" in spec)
 apply (erule disjE, simp)
  apply (rotate_tac 2)
  apply (drule sym)
  apply (simp)

  apply (elim conjE exE, simp)
  apply (simp add: appt_assoc_sym)
  apply (rotate_tac 1)
  apply (drule_tac x="sb ^^ <Tick>" in spec)
  apply (drule_tac x="X" in spec, simp)
  apply (elim conjE)

  apply (case_tac "Suc (lengtht sb) < n", simp)
  apply (case_tac "Suc (lengtht sb) = n", simp)
  apply (drule mp, force)
  apply (simp)
  apply (force)
done

(*** rest_setF (equal) ***)

lemma Seq_compo_rest_setF:
   "[| traces P1 .|. n = traces P2 .|. n ;
       failures P1 .|. n = failures P2 .|. n ;
       failures Q1 .|. n = failures Q2 .|. n  |]
    ==> failures (P1 ;; Q1) .|. n = failures (P2 ;; Q2) .|. n"
apply (rule order_antisym)
by (simp_all add: Seq_compo_rest_setF_sub)

(*** distF lemma ***)

lemma Seq_compo_distF:
"[| PQTs = {(traces P1, traces P2)} ;
    PQFs = {(failures P1, failures P2), (failures Q1, failures Q2)} |]
 ==> (EX PQ. PQ:PQTs & 
             distance(failures (P1 ;; Q1), failures (P2 ;; Q2))
          <= distance((fst PQ), (snd PQ))) |
     (EX PQ. PQ:PQFs & 
             distance(failures (P1 ;; Q1), failures (P2 ;; Q2))
          <= distance((fst PQ), (snd PQ)))"
apply (rule rest_to_dist_pair_two)
by (auto intro: Seq_compo_rest_setF)

(*** map_alpha F lemma ***)

lemma map_alpha_transfun_Seq_compo_lm:
  "[| distance (traces P1, traces P2) <= alpha * distance (x1, x2) ;
      distance (failures P1, failures P2) <= alpha * distance (x1, x2) ;
      distance (failures Q1, failures Q2) <= alpha * distance (x1, x2) |]
    ==> distance (failures (P1 ;; Q1), failures (P2 ;; Q2))
     <= alpha * distance (x1, x2)"
apply (insert Seq_compo_distF
       [of "{(traces P1, traces P2)}" P1 P2
           "{(failures P1, failures P2), (failures Q1, failures Q2)}" Q1 Q2])
by (auto)

(*** map_alpha ***)

lemma map_alpha_transfun_Seq_compo:
 "[| Pf : Procfun ; Qf : Procfun ;
     map_alpha (%SFf. tracesfun Pf (fstF o SFf)) alpha ; 
     map_alpha (failuresfun Pf) alpha ; map_alpha (failuresfun Qf) alpha |]
  ==> map_alpha (failuresfun (%f. (Pf f ;; Qf f))) alpha"
apply (simp add: map_alpha_def)
apply (intro allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
apply (simp add: tracesfun_def)
apply (simp add: traces_Pf_Proc_T_F)
by (simp add: map_alpha_transfun_Seq_compo_lm)

(*** non_expanding ***)

lemma non_expanding_failuresfun_Seq_compo:
 "[| Pf : Procfun ; Qf : Procfun ;
     non_expanding (%SFf. tracesfun Pf (fstF o SFf)) ;
     non_expanding (failuresfun Pf) ; non_expanding (failuresfun Qf) |]
  ==> non_expanding (failuresfun (%f. (Pf f ;; Qf f)))"
by (simp add: non_expanding_def map_alpha_transfun_Seq_compo)

(*** contraction_alpha ***)

lemma contraction_alpha_failuresfun_Seq_compo:
 "[| Pf : Procfun ; Qf : Procfun ;
     contraction_alpha (%SFf. tracesfun Pf (fstF o SFf)) alpha ;
     contraction_alpha (failuresfun Pf) alpha ; 
     contraction_alpha (failuresfun Qf) alpha|]
  ==> contraction_alpha (failuresfun (%f. (Pf f ;; Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_transfun_Seq_compo)

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

(*** rest_setF (subset) ***)

lemma gSKIP_Seq_compo_rest_setF_sub:
   "[| traces P1 .|. (Suc n) <= traces P2 .|. (Suc n) ;
       failures P1 .|. (Suc n) <= failures P2 .|. (Suc n) ;
       failures Q1 .|. n <= failures Q2 .|. n ;
       <Tick> ~:t traces P1 ;
       <Tick> ~:t traces P2 |]
    ==> failures (P1 ;; Q1) .|. (Suc n) <= failures (P2 ;; Q2) .|. (Suc n)"
apply (simp add: subsetF_iff)
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_setF)
apply (simp add: in_rest_domT)
apply (simp add: in_failures)
apply (elim conjE exE disjE)
apply (simp_all)

 (* case 1 *)
 apply (insert trace_last_nil_or_unnil)
 apply (rotate_tac -1)
 apply (drule_tac x="sa" in spec)
 apply (erule disjE)
  apply (simp add: gSKIP_to_Tick_notin_traces)   (* sa = []t *)

  apply (rule disjI2)                            (* sa ~= []t *)
  apply (elim conjE exE, simp)
  apply (rule_tac x="(sb ^^ <a>)" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp)

 (* case 2 *)
 apply (rotate_tac -1)
 apply (drule_tac x="t" in spec)
 apply (erule disjE)   
  apply (simp)           (* t = []t *)
  apply (rotate_tac 5)
  apply (drule sym)
  apply (simp)           (* contradict noTick *)

  apply (rule disjI2)    (* t ~= []t *)
  apply (elim conjE exE, simp)
  apply (simp add: appt_assoc_sym)
  apply (rule_tac x="sa" in exI)
  apply (rule_tac x="sb ^^ <Tick>" in exI)
  apply (simp add: appt_assoc)

  apply (insert trace_last_nil_or_unnil)
  apply (rotate_tac -1)
  apply (drule_tac x="sa" in spec)
  apply (erule disjE)
   apply (simp add: gSKIP_to_Tick_notin_traces)   (* sa = []t *)
   apply (elim conjE exE, simp)
                                                  (* i.e. lengtht sb < n *)
   apply (rotate_tac 2)
   apply (drule_tac x="sb ^^ <Tick>" in spec)
   apply (drule_tac x="X" in spec)
   apply (drule mp)
    apply (simp)
    apply (case_tac "Suc (lengtht sb) < n", simp)
    apply (case_tac "Suc (lengtht sb) = n", fast)
    apply (force)
   apply (simp)
done

(*** rest_setF (equal) ***)

lemma gSKIP_Seq_compo_rest_setF:
   "[| traces P1 .|. (Suc n) = traces P2 .|. (Suc n) ;
       failures P1 .|. (Suc n) = failures P2 .|. (Suc n) ;
       failures Q1 .|. n = failures Q2 .|. n ;
       <Tick> ~:t traces P1 ;
       <Tick> ~:t traces P2 |]
    ==> failures (P1 ;; Q1) .|. (Suc n) = failures (P2 ;; Q2) .|. (Suc n)"
apply (rule order_antisym)
by (simp_all add: gSKIP_Seq_compo_rest_setF_sub)

(*** map_alpha F lemma ***)

lemma gSKIP_map_alpha_transfun_Seq_compo_lm:
  "[| distance (traces P1, traces P2) * 2 <= (1/2)^n ;
      distance (failures P1, failures P2) * 2 <= (1/2)^n ;
      distance (failures Q1, failures Q2) <= (1/2)^n ;
       <Tick> ~:t traces P1 ;
       <Tick> ~:t traces P2 |]
    ==> distance (failures (P1 ;; Q1), failures (P2 ;; Q2)) * 2
     <= (1/2)^n"
apply (insert gSKIP_Seq_compo_rest_setF[of P1 n P2 Q1 Q2])
apply (simp add: distance_rs_le_1)
done

(*** map_alpha ***)

lemma gSKIP_contraction_half_transfun_Seq_compo:
 "[| contraction_alpha (%SFf. tracesfun Pf (fstF o SFf)) (1/2) ;
     contraction_alpha (failuresfun Pf) (1/2) ; non_expanding (failuresfun Qf) ;
     Pf : gSKIPfun ; Pf : Procfun |]
  ==> contraction_alpha (failuresfun (%f. (Pf f ;; Qf f))) (1/2)"
apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def)
apply (intro allI)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)

apply (case_tac "x = y", simp)
apply (simp add: distance_iff)
apply (simp add: failuresfun_def)
apply (simp add: tracesfun_def)
apply (simp add: traces_Pf_Proc_T_F)
apply (insert ALL_gSKIP_to_Tick_notin_traces)
apply (frule_tac x="Pf" in spec)
apply (drule_tac x="Pf" in spec)
apply (drule_tac x="(%p. Proc_F(x p))" in spec)
apply (drule_tac x="(%p. Proc_F(y p))" in spec)
apply (simp add: gSKIP_map_alpha_transfun_Seq_compo_lm)
done

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

(*** rest_setF (equal) ***)

lemma Depth_rest_rest_setF:
   "failures P .|. n = failures Q .|. n
    ==> failures (P |. m) .|. n = failures (Q |. m) .|. n"
apply (simp add: failures.simps)
apply (simp add: min_rs)
apply (rule rest_equal_preserve)
apply (simp)
apply (simp add: min_def)
done

(*** distF lemma ***)

lemma Depth_rest_distF:
     "distance(failures (P |. m), failures (Q |. m)) <= 
      distance(failures P, failures Q)"
apply (rule rest_distance_subset)
by (auto intro: Depth_rest_rest_setF)

(*** map_alphaT lemma ***)

lemma map_alpha_failuresfun_Depth_rest_lm:
  "distance(failures P, failures Q) <= alpha * distance (x1, x2)
    ==> distance(failures (P |. m), failures (Q |. m))
     <= alpha * distance(x1, x2)"
apply (insert Depth_rest_distF[of P m Q])
by (simp)

(*** map_alpha ***)

lemma map_alpha_failuresfun_Depth_rest:
 "map_alpha (failuresfun Pf) alpha
  ==> map_alpha (failuresfun (%f. (Pf f) |. n)) alpha"
apply (simp add: map_alpha_def)
apply (intro allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (simp add: failuresfun_def)
by (simp add: map_alpha_failuresfun_Depth_rest_lm)

(*** non_expanding ***)

lemma non_expanding_failuresfun_Depth_rest:
 "non_expanding (failuresfun Pf)
  ==> non_expanding (failuresfun (%f. (Pf f) |. n))"
by (simp add: non_expanding_def map_alpha_failuresfun_Depth_rest)

(*** contraction_alpha ***)

lemma contraction_alpha_failuresfun_Depth_rest:
 "contraction_alpha (failuresfun Pf) alpha
  ==> contraction_alpha (failuresfun (%f. (Pf f) |. n)) alpha"
by (simp add: contraction_alpha_def map_alpha_failuresfun_Depth_rest)

(*--------------------------------*
 |            variable            |
 *--------------------------------*)

(*** non_expanding ***)

lemma non_expanding_failuresfun_variable: 
   "non_expanding (failuresfun (%f. f p))"
apply (subgoal_tac "non_expanding [[%f. f p]]Ffun")
apply (simp add: semF_decompo_fun)
apply (simp add: non_expanding_domF_decompo
                 tracesfun_failuresfun_in_domF)
apply (erule conjE)
apply (simp)

apply (simp add: semFfun_variable)
apply (simp add: non_expanding_prod_variable)
done

(*--------------------------------*
 |            Procfun             |
 *--------------------------------*)

(*****************************************************************
 |                         non_expanding                         |
 *****************************************************************)

lemma non_expanding_failuresfun_lm:
  "Pf : nohidefun ==> non_expanding (failuresfun Pf)"
apply (rule nohidefun.induct[of Pf])
apply (simp)
apply (simp add: non_expanding_failuresfun_variable)
apply (simp add: non_expanding_failuresfun_STOP)
apply (simp add: non_expanding_failuresfun_SKIP)
apply (simp add: non_expanding_failuresfun_DIV)
apply (simp add: non_expanding_failuresfun_Act_prefix)
apply (simp add: non_expanding_failuresfun_Ext_pre_choice)
apply (simp add: non_expanding_failuresfun_Ext_choice non_expanding_tracesfun_fstF)
apply (simp add: non_expanding_failuresfun_Int_choice)
apply (simp add: non_expanding_failuresfun_Rep_int_choice)
apply (simp add: non_expanding_failuresfun_IF)
apply (simp add: non_expanding_failuresfun_Parallel)

(* hiding --> const *)
apply (simp add: failuresfun_def)
apply (simp add: non_expanding_Constant)

apply (simp add: non_expanding_failuresfun_Renaming)
apply (simp add: non_expanding_failuresfun_Seq_compo non_expanding_tracesfun_fstF)
apply (simp add: non_expanding_failuresfun_Depth_rest)
done

lemma non_expanding_failuresfun: 
  "Pf : nohidefun ==> non_expanding (failuresfun Pf)"
by (simp add: non_expanding_failuresfun_lm)

(*=============================================================*
 |                         [[P]]Ffun                           |
 *=============================================================*)

lemma non_expanding_semFfun:
  "Pf : nohidefun ==> non_expanding [[Pf]]Ffun"
apply (simp add: semF_decompo_fun)
apply (simp add: non_expanding_domF_decompo fun_in_domF)
apply (simp add: non_expanding_tracesfun_fstF)
apply (simp add: non_expanding_failuresfun)
done

(*=============================================================*
 |                         failuresFun                         |
 *=============================================================*)

lemma non_expanding_failuresFun:
  "PF : nohideFun ==> non_expanding (failuresFun PF)"
apply (simp add: prod_non_expand)
apply (rule allI)
apply (simp add: proj_failuresFun_failuresfun)
apply (simp add: nohideFun_def)
apply (drule_tac x="i" in spec)
apply (simp add: non_expanding_failuresfun)
done

(*=============================================================*
 |                         [[P]]FFun                           |
 *=============================================================*)

lemma non_expanding_semFFun: 
  "PF : nohideFun ==> non_expanding [[PF]]FFun"
apply (simp add: prod_non_expand)
apply (rule allI)
apply (simp add: proj_semFFun_semFfun)
apply (simp add: nohideFun_def)
apply (drule_tac x="i" in spec)
apply (simp add: non_expanding_semFfun)
done

(*****************************************************************
 |                         contraction                           |
 *****************************************************************)

lemma contraction_alpha_failuresfun: 
  "Pf : gProcfun ==> contraction_alpha (failuresfun Pf) (1/2)"
apply (rule gProcfun.induct[of Pf])
apply (simp)
apply (simp add: contraction_alpha_failuresfun_STOP)
apply (simp add: contraction_alpha_failuresfun_SKIP)
apply (simp add: contraction_alpha_failuresfun_DIV)
apply (simp add: contraction_half_failuresfun_Act_prefix
                 non_expanding_failuresfun)
apply (simp add: contraction_half_failuresfun_Ext_pre_choice
                 non_expanding_failuresfun)
apply (simp add: contraction_alpha_failuresfun_Ext_choice
                 contraction_alpha_tracesfun_fstF)
apply (simp add: contraction_alpha_failuresfun_Int_choice)
apply (simp add: contraction_alpha_failuresfun_Rep_int_choice)
apply (simp add: contraction_alpha_failuresfun_IF)
apply (simp add: contraction_alpha_failuresfun_Parallel)

(* hiding --> const *)
apply (simp add: failuresfun_def)
apply (simp add: contraction_alpha_Constant)

apply (simp add: contraction_alpha_failuresfun_Renaming)

apply (simp)
apply (elim conjE disjE)
apply (simp add: gSKIP_contraction_half_transfun_Seq_compo
                 non_expanding_failuresfun
                 contraction_alpha_tracesfun_fstF)
apply (simp add: contraction_alpha_failuresfun_Seq_compo
                 contraction_alpha_tracesfun_fstF)
apply (simp add: contraction_alpha_failuresfun_Depth_rest)
done

(*=============================================================*
 |                         [[P]]Ffun                           |
 *=============================================================*)

lemma contraction_alpha_semFfun:
  "Pf : gProcfun ==> contraction_alpha [[Pf]]Ffun (1/2)"
apply (simp add: semF_decompo_fun)
apply (simp add: contraction_alpha_domF_decompo fun_in_domF)
apply (simp add: contraction_alpha_tracesfun_fstF)
apply (simp add: contraction_alpha_failuresfun)
done

(*=============================================================*
 |                       failuresfun P                         |
 *=============================================================*)

lemma contraction_alpha_failuresFun: 
  "PF : gProcFun
   ==> contraction_alpha (failuresFun PF) (1/2)"
apply (simp add: prod_contra_alpha)
apply (rule allI)
apply (simp add: proj_failuresFun_failuresfun)
apply (simp add: gProcFun_def)
apply (drule_tac x="i" in spec)
apply (simp add: contraction_alpha_failuresfun)
done

lemma contraction_failuresfun:
  "PF : gProcFun
   ==> contraction (failuresFun PF)"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
apply (simp add: contraction_alpha_failuresFun)
done

(*=============================================================*
 |                         [[P]]FFun                           |
 *=============================================================*)

lemma contraction_alpha_semFFun: 
  "PF : gProcFun
   ==> contraction_alpha [[PF]]FFun (1/2)"
apply (simp add: prod_contra_alpha)
apply (rule allI)
apply (simp add: proj_semFFun_semFfun)
apply (simp add: gProcFun_def)
apply (drule_tac x="i" in spec)
apply (simp add: contraction_alpha_semFfun)
done

lemma contraction_semFFun: 
  "PF : gProcFun
   ==> contraction [[PF]]FFun"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
apply (simp add: contraction_alpha_semFFun)
done

end