Theory CSP_T_contraction

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

theory CSP_T_contraction = CSP_T_tracesfun + RS_prod:

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

         1. contraction tracesfun
         2. contraction tracesFun
         3. contraction [[ ]]Tfun
         4. contraction [[ ]]TFun

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

(*============================================*
 |                   gSKIP                    |
 *============================================*)

lemma gSKIP_to_Tick_notin_traces:
  "Pf : gSKIPfun ==> <Tick> ~:t traces (Pf f)"
apply (rule gSKIPfun.induct[of Pf])
apply (simp_all add: in_traces)

 apply (rule impI)
 apply (elim conjE disjE)
 apply (simp_all)

 apply (rule conjI)
 apply (intro allI impI)
 apply (erule noTick_rmTickE)
 apply (simp)
 apply (auto)
done

lemma ALL_gSKIP_to_Tick_notin_traces:
  "ALL Pf f. Pf : gSKIPfun --> <Tick> ~:t traces (Pf f)"
by (simp add: gSKIP_to_Tick_notin_traces)

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

(*** Constant_contraction ***)

lemma map_alpha_Constant: "0 <= alpha ==> map_alpha (%f. P) alpha"
apply (simp add: map_alpha_def)
apply (simp add: real_mult_order_eq)
done

(*** non_expanding_Constant ***)

lemma non_expanding_Constant: "non_expanding (%f. P)"
by (simp add: non_expanding_def map_alpha_Constant)

(*** Constant_contraction_alpha ***)

lemma contraction_alpha_Constant:
   "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (%x. P) alpha"
by (simp add: contraction_alpha_def map_alpha_Constant)

(*** STOP ***)

lemma map_alpha_tracesfun_STOP: 
  "0 <= alpha ==> map_alpha (tracesfun (%f. STOP)) alpha"
by (simp add: tracesfun_simp map_alpha_Constant)

lemma non_expanding_tracesfun_STOP: 
  "non_expanding (tracesfun (%f. STOP))"
by (simp add: non_expanding_def map_alpha_tracesfun_STOP)

lemma contraction_alpha_tracesfun_STOP: 
  "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. STOP)) alpha"
by (simp add: tracesfun_simp contraction_alpha_Constant)

(*** SKIP ***)

lemma map_alpha_tracesfun_SKIP: 
  "0 <= alpha ==> map_alpha (tracesfun (%f. SKIP)) alpha"
by (simp add: tracesfun_simp map_alpha_Constant)

lemma non_expanding_tracesfun_SKIP: 
  "non_expanding (tracesfun (%f. SKIP))"
by (simp add: non_expanding_def map_alpha_tracesfun_SKIP)

lemma contraction_alpha_tracesfun_SKIP: 
  "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. SKIP)) alpha"
by (simp add: tracesfun_simp contraction_alpha_Constant)

(*** DIV ***)

lemma map_alpha_tracesfun_DIV: 
  "0 <= alpha ==> map_alpha (tracesfun (%f. DIV)) alpha"
by (simp add: tracesfun_simp map_alpha_Constant)

lemma non_expanding_tracesfun_DIV: 
  "non_expanding (tracesfun (%f. DIV))"
by (simp add: non_expanding_def map_alpha_tracesfun_DIV)

lemma contraction_alpha_tracesfun_DIV: 
  "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. DIV)) alpha"
by (simp add: tracesfun_simp contraction_alpha_Constant)

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

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

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

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

 (* <= *)
 apply (rule allI)
 apply (drule_tac x="<Ev a> ^^ s" in spec)
 apply (simp add: in_traces)
done

(***  contraction_half ***)

lemma contraction_half_tracesfun_Act_prefix: 
 "non_expanding (tracesfun Pf)
  ==> contraction_alpha (tracesfun (%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: tracesfun_def)
apply (simp add: contraction_half_traces_Act_prefix_lm)
done

(***  contraction ***)

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

(*** non_expanding ***)

lemma non_expanding_tracesfun_Act_prefix: 
 "non_expanding (tracesfun Pf)
  ==> non_expanding (tracesfun (%f. a -> Pf f))"
apply (rule contraction_non_expanding)
by (simp add: contraction_tracesfun_Act_prefix)

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

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

lemma Ext_pre_choice_Act_prefix_rest_domT_sub:
   "[| ALL a : X.
         traces (a -> Pf a) .|. n <= traces (a -> Qf a) .|. n |]
    ==> traces (? a:X -> Pf a) .|. n <=
        traces (? a:X -> Qf a) .|. n"
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_traces)
apply (elim conjE exE disjE)
apply (simp_all)

apply (drule_tac x="a" in bspec, simp)
apply (drule_tac x="t" in spec)
apply (simp add: in_traces)
done

(*** rest_domT (equal) ***)

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

(*** distT lemma ***)

lemma Ext_pre_choice_Act_prefix_distT_nonempty:
"[| X ~= {} ; PQs = {(traces (a -> Pf a), traces (a -> Qf a))|a. a : X} |]
 ==> (EX PQ. PQ:PQs & 
             distance(traces (? a:X -> Pf a), traces (? 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_domT)
apply (rule ballI)
apply (simp)
apply (drule_tac x="traces (a -> Pf a)" in spec)
apply (drule_tac x="traces (a -> Qf a)" in spec)
by (auto)

(*** contraction lemma ***)

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

(*** contraction_half ***)

lemma contraction_half_tracesfun_Ext_pre_choice:
 "ALL a. non_expanding (tracesfun (Pff a))
  ==> contraction_alpha (tracesfun (%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: tracesfun_simp)
apply (simp add: tracesfun_def)
by (simp add: contraction_half_tracesfun_Ext_pre_choice_lm)

(*** Ext_pre_choice_evalT_contraction ***)

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

(*** Ext_pre_choice_evalT_non_expanding ***)

lemma non_expanding_tracesfun_Ext_pre_choice:
 "ALL a. non_expanding (tracesfun (Pff a))
  ==> non_expanding (tracesfun (%f. ? a:X -> (Pff a f)))"
apply (rule contraction_non_expanding)
by (simp add: contraction_tracesfun_Ext_pre_choice)

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

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

lemma Ext_choice_rest_domT_sub:
   "[| traces P1 .|. n <= traces P2 .|. n ;
       traces Q1 .|. n <= traces Q2 .|. n  |]
    ==> traces (P1 [+] Q1) .|. n <= traces (P2 [+] Q2) .|. n"
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_traces)
by (auto)

(*** rest_domT (equal) ***)

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

(*** distT lemma ***)

lemma Ext_choice_distT:
"PQs = {(traces P1, traces P2), (traces Q1, traces Q2)}
 ==> (EX PQ. PQ:PQs & 
             distance(traces (P1 [+] Q1), traces (P2 [+] Q2))
          <= distance((fst PQ), (snd PQ)))"
apply (rule rest_to_dist_pair)
by (auto intro: Ext_choice_rest_domT)

(*** map_alpha T lemma ***)

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

(*** map_alpha ***)

lemma map_alpha_tracesfun_Ext_choice:
 "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |]
  ==> map_alpha (tracesfun (%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: tracesfun_def)
by (simp add: map_alpha_tracesfun_Ext_choice_lm)

(*** non_expanding ***)

lemma non_expanding_tracesfun_Ext_choice:
 "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |]
  ==> non_expanding (tracesfun (%f. (Pf f [+] Qf f)))"
by (simp add: non_expanding_def map_alpha_tracesfun_Ext_choice)

(*** contraction ***)

lemma contraction_alpha_tracesfun_Ext_choice:
 "[| contraction_alpha (tracesfun Pf) alpha ; 
     contraction_alpha (tracesfun Qf) alpha|]
  ==> contraction_alpha (tracesfun (%f. (Pf f [+] Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_tracesfun_Ext_choice)

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

(*** map_alpha ***)

lemma map_alpha_tracesfun_Int_choice:
 "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |]
  ==> map_alpha (tracesfun (%f. (Pf f |~| Qf f))) alpha"
by (simp add: map_alpha_tracesfun_Ext_choice tracesfun_Int_choice_Ext_choice)

(*** non_expanding ***)

lemma non_expanding_tracesfun_Int_choice:
 "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |]
  ==> non_expanding (tracesfun (%f. (Pf f |~| Qf f)))"
by (simp add: non_expanding_tracesfun_Ext_choice tracesfun_Int_choice_Ext_choice)

(*** contraction ***)

lemma contraction_alpha_tracesfun_Int_choice:
 "[| contraction_alpha (tracesfun Pf) alpha ; 
     contraction_alpha (tracesfun Qf) alpha|]
  ==> contraction_alpha (tracesfun (%f. (Pf f |~| Qf f))) alpha"
by (simp add: contraction_alpha_tracesfun_Ext_choice tracesfun_Int_choice_Ext_choice)

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

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

lemma Rep_int_choice_rest_domT_sub:
   "[| ALL c : C.
         traces (Pf c) .|. n <= traces (Qf c) .|. n |]
    ==> traces (!! :C .. Pf) .|. n <=
        traces (!! :C .. Qf) .|. n"
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_traces)
by (auto)

(*** rest_domT (equal) ***)

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

(*** distT lemma ***)

lemma Rep_int_choice_distT_nonempty:
"[| C ~= {} ; PQs = {(traces (Pf c), traces (Qf c))|c. c : C} |]
 ==> (EX PQ. PQ:PQs & 
             distance(traces (!! :C .. Pf), traces (!! :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_domT)
by (auto)

(*** map_alpha T lemma ***)

lemma map_alpha_tracesfun_Rep_int_choice_lm:
"[| C ~= {} ; ALL c. distance (traces (Pf c), traces (Qf c)) 
                  <= alpha * distance (x1, x2) |]
 ==> distance(traces (!! :C .. Pf), traces (!! :C .. Qf))
  <= alpha * distance(x1, x2)"
apply (insert Rep_int_choice_distT_nonempty
       [of C "{(traces (Pf c), traces (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_tracesfun_Rep_int_choice:
 "ALL c. map_alpha (tracesfun (Pff c)) alpha
  ==> map_alpha (tracesfun (%f. !! c:C .. (Pff c f))) alpha"
apply (simp add: map_alpha_def)
apply (case_tac "C = {}")
 apply (simp add: tracesfun_simp)
 apply (simp add: real_mult_order_eq)
apply (simp add: tracesfun_def)
apply (simp add: map_alpha_tracesfun_Rep_int_choice_lm)
done

(*** non_expanding ***)

lemma non_expanding_tracesfun_Rep_int_choice:
 "ALL c. non_expanding (tracesfun (Pff c))
  ==> non_expanding (tracesfun (%f. !! c:C .. (Pff c f)))"
by (simp add: non_expanding_def map_alpha_tracesfun_Rep_int_choice)

(*** Rep_int_choice_evalT_contraction_alpha ***)

lemma contraction_alpha_tracesfun_Rep_int_choice:
 "ALL c. contraction_alpha (tracesfun (Pff c)) alpha 
     ==> contraction_alpha (tracesfun (%f. !! c:C .. (Pff c f))) alpha"
by (simp add: contraction_alpha_def map_alpha_tracesfun_Rep_int_choice)

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

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

lemma IF_rest_domT_sub:
   "[| traces P1 .|. n <= traces P2 .|. n ;
       traces Q1 .|. n <= traces Q2 .|. n  |]
    ==> traces (IF b THEN P1 ELSE Q1) .|. n <= 
        traces (IF b THEN P2 ELSE Q2) .|. n"
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_traces)
done

(*** rest_domT (equal) ***)

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

(*** distT lemma ***)

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

(*** map_alpha T lemma ***)

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

(*** map_alpha ***)

lemma map_alpha_tracesfun_IF:
 "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |]
  ==> map_alpha (tracesfun (%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: tracesfun_def)
by (simp add: map_alpha_tracesfun_IF_lm)

(*** non_expanding ***)

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

(*** contraction_alpha ***)

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

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

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

lemma Parallel_rest_domT_sub:
   "[| traces P1 .|. n <= traces P2 .|. n ;
       traces Q1 .|. n <= traces Q2 .|. n  |]
    ==> traces (P1 |[X]| Q1) .|. n <= traces (P2 |[X]| Q2) .|. n"
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_traces)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
apply (rule_tac x="ta" in exI)
apply (simp)

apply (erule par_tr_lengthtE)
by (auto)

(*** rest_domT (equal) ***)

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

(*** distT lemma ***)

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

(*** map_alpha T lemma ***)

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

(*** map_alpha ***)

lemma map_alpha_tracesfun_Parallel:
 "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |]
  ==> map_alpha (tracesfun (%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: tracesfun_def)
by (simp add: map_alpha_tracesfun_Parallel_lm)

(*** non_expanding ***)

lemma non_expanding_tracesfun_Parallel:
 "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |]
  ==> non_expanding (tracesfun (%f. (Pf f |[X]| Qf f)))"
by (simp add: non_expanding_def map_alpha_tracesfun_Parallel)

(*** contraction_alpha ***)

lemma contraction_alpha_tracesfun_Parallel:
 "[| contraction_alpha (tracesfun Pf) alpha ; 
     contraction_alpha (tracesfun Qf) alpha |]
  ==> contraction_alpha (tracesfun (%f. (Pf f |[X]| Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_tracesfun_Parallel)

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

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

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

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

lemma Renaming_rest_domT_sub:
   "traces P .|. n <= traces Q .|. n
    ==> traces (P [[r]]) .|. n <= traces (Q [[r]]) .|. n"
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_traces)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
apply (drule_tac x="s" in spec)
by (simp add: ren_tr_lengtht)

(*** rest_domT (equal) ***)

lemma Renaming_rest_domT:
   "traces P .|. n = traces Q .|. n
    ==> traces (P [[r]]) .|. n = traces (Q [[r]]) .|. n"
apply (rule order_antisym)
by (simp_all add: Renaming_rest_domT_sub)

(*** distT lemma ***)

lemma Renaming_distT:
     "distance(traces (P [[r]]), traces (Q [[r]])) <= 
      distance(traces P, traces Q)"
apply (rule rest_distance_subset)
by (auto intro: Renaming_rest_domT)

(*** map_alphaT lemma ***)

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

(*** map_alpha ***)

lemma map_alpha_tracesfun_Renaming:
 "map_alpha (tracesfun Pf) alpha
  ==> map_alpha (tracesfun (%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: tracesfun_def)
by (simp add: map_alpha_tracesfun_Renaming_lm)

(*** non_expanding ***)

lemma non_expanding_tracesfun_Renaming:
 "non_expanding (tracesfun Pf)
  ==> non_expanding (tracesfun (%f. (Pf f) [[r]]))"
by (simp add: non_expanding_def map_alpha_tracesfun_Renaming)

(*** contraction_alpha ***)

lemma contraction_alpha_tracesfun_Renaming:
 "contraction_alpha (tracesfun Pf) alpha
  ==> contraction_alpha (tracesfun (%f. (Pf f) [[r]])) alpha"
by (simp add: contraction_alpha_def map_alpha_tracesfun_Renaming)

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

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

lemma Seq_compo_rest_domT_sub:
   "[| traces P1 .|. n <= traces P2 .|. n ;
       traces Q1 .|. n <= traces Q2 .|. n  |]
    ==> traces (P1 ;; Q1) .|. n <= traces (P2 ;; Q2) .|. n"
apply (simp add: subdomT_iff)
apply (intro allI impI)
apply (simp add: in_rest_domT)
apply (simp add: in_traces)
apply (elim conjE exE disjE)

 (* case 1 *)
 apply (rule disjI1)
 apply (insert trace_last_noTick_or_Tick)
 apply (rotate_tac -1)
 apply (drule_tac x="s" in spec)
 apply (erule disjE)
 apply (rule_tac x="s" in exI, simp)

 apply (elim conjE exE)
 apply (rule_tac x="sa" in exI, simp)
 apply (drule_tac x="sa" in spec, simp)
 apply (drule mp)
 apply (rule memT_prefix_closed, simp_all, simp)

 (* case 2 *)
 apply (case_tac "~ noTick s", simp)
 apply (insert trace_last_nil_or_unnil)
 apply (rotate_tac -1)
 apply (drule_tac x="ta" in spec)
 apply (erule disjE)

  apply (rule disjI1)                (* ta = []t *)
  apply (rule_tac x="s" in exI, simp)
  apply (drule_tac x="s" in spec, simp)
  apply (drule mp)
  apply (rule memT_prefix_closed, simp_all, simp)

  apply (rule disjI2)                (* ta ~= []t *)
  apply (elim conjE exE, simp)

  apply (drule_tac x="s ^^ <Tick>" in spec)
  apply (drule_tac x=" sa ^^ <a>" in spec)
  apply (simp)
  apply (rule_tac x="s" in exI)
  apply (rule_tac x="sa ^^ <a>" in exI)
  apply (simp)
done

(*** rest_domT (equal) ***)

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

(*** distT lemma ***)

lemma Seq_compo_distT:
"PQs = {(traces P1, traces P2), (traces Q1, traces Q2)}
 ==> (EX PQ. PQ:PQs & 
             distance(traces (P1 ;; Q1), traces (P2 ;; Q2))
          <= distance((fst PQ), (snd PQ)))"
apply (rule rest_to_dist_pair)
by (auto intro: Seq_compo_rest_domT)

(*** map_alpha T lemma ***)

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

(*** map_alpha ***)

lemma map_alpha_transfun_Seq_compo:
 "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |]
  ==> map_alpha (tracesfun (%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: tracesfun_def)
by (simp add: map_alpha_transfun_Seq_compo_lm)

(*** non_expanding ***)

lemma non_expanding_tracesfun_Seq_compo:
 "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |]
  ==> non_expanding (tracesfun (%f. (Pf f ;; Qf f)))"
by (simp add: non_expanding_def map_alpha_transfun_Seq_compo)

(*** contraction_alpha ***)

lemma contraction_alpha_tracesfun_Seq_compo:
 "[| contraction_alpha (tracesfun Pf) alpha ; 
     contraction_alpha (tracesfun Qf) alpha|]
  ==> contraction_alpha (tracesfun (%f. (Pf f ;; Qf f))) alpha"
by (simp add: contraction_alpha_def map_alpha_transfun_Seq_compo)

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

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

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

 (* case 1 *)
 apply (rule disjI1)
 apply (insert trace_last_noTick_or_Tick)
 apply (rotate_tac -1)
 apply (drule_tac x="s" in spec)
 apply (erule disjE)
 apply (rule_tac x="s" in exI, simp)

 apply (elim conjE exE)
 apply (rule_tac x="sa" in exI, simp)
 apply (drule_tac x="sa" in spec, simp)
 apply (drule mp)
 apply (rule memT_prefix_closed, simp_all, simp)

 (* case 2 *)
 apply (case_tac "~ noTick s", simp)
 apply (insert trace_last_nil_or_unnil)
 apply (rotate_tac -1)
 apply (drule_tac x="ta" in spec)
 apply (erule disjE)

  apply (rule disjI1)                (* ta = []t *)
  apply (rule_tac x="s" in exI, simp)
  apply (drule_tac x="s" in spec, simp)
  apply (drule mp)
  apply (rule memT_prefix_closed, simp_all, simp)

  apply (rule disjI2)                (* ta ~= []t *)
  apply (elim conjE exE, simp)

  apply (drule_tac x="s ^^ <Tick>" in spec)
  apply (drule_tac x=" sa ^^ <a>" in spec)
  apply (simp)
  apply (rule_tac x="s" in exI)
  apply (rule_tac x="sa ^^ <a>" in exI)
  apply (simp)

 apply (insert trace_last_nil_or_unnil)
 apply (rotate_tac -1)
 apply (drule_tac x="s" in spec)
 apply (erule disjE)
  apply (auto)
done

(*** rest_domT (equal) ***)

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

(*** map_alpha T lemma ***)

lemma gSKIP_map_alpha_transfun_Seq_compo_lm:
  "[| distance (traces P1, traces P2) * 2 <= (1/2)^n ;
      distance (traces Q1, traces Q2) <= (1/2)^n ;
       <Tick> ~:t traces P1 ;
       <Tick> ~:t traces P2 |]
    ==> distance (traces (P1 ;; Q1), traces (P2 ;; Q2)) * 2
     <= (1/2)^n"
apply (insert gSKIP_Seq_compo_rest_domT[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 (tracesfun Pf) (1/2) ; non_expanding (tracesfun Qf) ;
     Pf : gSKIPfun |]
  ==> contraction_alpha (tracesfun (%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="y" in spec)
apply (drule_tac x="y" in spec)

apply (case_tac "x = y", simp)
apply (simp add: distance_iff)
apply (simp add: tracesfun_def)
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_T (x p))" in spec)
apply (drule_tac x="(%p. Proc_T (y p))" in spec)
apply (simp add: gSKIP_map_alpha_transfun_Seq_compo_lm)
done

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

(*** rest_domT (equal) ***)

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

(*** distT lemma ***)

lemma Depth_rest_distT:
     "distance(traces (P |. m), traces (Q |. m)) <= 
      distance(traces P, traces Q)"
apply (rule rest_distance_subset)
by (auto intro: Depth_rest_rest_domT)

(*** map_alphaT lemma ***)

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

(*** map_alpha ***)

lemma map_alpha_tracesfun_Depth_rest:
 "map_alpha (tracesfun Pf) alpha
  ==> map_alpha (tracesfun (%f. (Pf f) |. m)) 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: tracesfun_def)
by (simp add: map_alpha_tracesfun_Depth_rest_lm)

(*** non_expanding ***)

lemma non_expanding_tracesfun_Depth_rest:
 "non_expanding (tracesfun Pf)
  ==> non_expanding (tracesfun (%f. (Pf f) |. m))"
by (simp add: non_expanding_def map_alpha_tracesfun_Depth_rest)

(*** contraction_alpha ***)

lemma contraction_alpha_tracesfun_Depth_rest:
 "contraction_alpha (tracesfun Pf) alpha
  ==> contraction_alpha (tracesfun (%f. (Pf f) |. m)) alpha"
by (simp add: contraction_alpha_def map_alpha_tracesfun_Depth_rest)

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

(*** non_expanding ***)

lemma non_expanding_tracesfun_variable: 
   "non_expanding (tracesfun (%f. f p))"
apply (simp add: tracesfun_def)
apply (simp add: traces_Proc_T)
apply (simp add: non_expanding_prod_variable)
done

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

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

lemma non_expanding_tracesfun: 
  "Pf : nohidefun ==> non_expanding (tracesfun Pf)"
apply (rule nohidefun.induct[of Pf])
apply (simp)
apply (simp add: non_expanding_tracesfun_variable)
apply (simp add: non_expanding_tracesfun_STOP)
apply (simp add: non_expanding_tracesfun_SKIP)
apply (simp add: non_expanding_tracesfun_DIV)
apply (simp add: non_expanding_tracesfun_Act_prefix)
apply (simp add: non_expanding_tracesfun_Ext_pre_choice)
apply (simp add: non_expanding_tracesfun_Ext_choice)
apply (simp add: non_expanding_tracesfun_Int_choice)
apply (simp add: non_expanding_tracesfun_Rep_int_choice)
apply (simp add: non_expanding_tracesfun_IF)
apply (simp add: non_expanding_tracesfun_Parallel)

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

apply (simp add: non_expanding_tracesfun_Renaming)
apply (simp add: non_expanding_tracesfun_Seq_compo)
apply (simp add: non_expanding_tracesfun_Depth_rest)
done

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

lemma non_expanding_semTfun: 
  "Pf : nohidefun ==> non_expanding [[Pf]]Tfun"
by (simp add: semT_to_traces non_expanding_tracesfun)

(*=============================================================*
 |                         tracesFun                           |
 *=============================================================*)

lemma non_expanding_tracesFun:
  "PF : nohideFun ==> non_expanding (tracesFun PF)"
apply (simp add: prod_non_expand)
apply (rule allI)
apply (simp add: proj_tracesFun_tracesfun)
apply (simp add: nohideFun_def)
apply (drule_tac x="i" in spec)
apply (simp add: non_expanding_tracesfun)
done

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

lemma non_expanding_semTFun: 
  "PF : nohideFun ==> non_expanding [[PF]]TFun"
apply (simp add: semT_to_traces non_expanding_tracesFun)
done

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

lemma contraction_alpha_tracesfun_lm: 
  "Pf : gProcfun ==> contraction_alpha (tracesfun Pf) (1/2)"
apply (rule gProcfun.induct[of Pf])
apply (simp)
apply (simp add: contraction_alpha_tracesfun_STOP)
apply (simp add: contraction_alpha_tracesfun_SKIP)
apply (simp add: contraction_alpha_tracesfun_DIV)
apply (simp add: contraction_half_tracesfun_Act_prefix
                 non_expanding_tracesfun)
apply (simp add: contraction_half_tracesfun_Ext_pre_choice
                 non_expanding_tracesfun)
apply (simp add: contraction_alpha_tracesfun_Ext_choice)
apply (simp add: contraction_alpha_tracesfun_Int_choice)
apply (simp add: contraction_alpha_tracesfun_Rep_int_choice)
apply (simp add: contraction_alpha_tracesfun_IF)
apply (simp add: contraction_alpha_tracesfun_Parallel)

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

apply (simp add: contraction_alpha_tracesfun_Renaming)

apply (simp)
apply (elim conjE disjE)
apply (simp add: gSKIP_contraction_half_transfun_Seq_compo
                 non_expanding_tracesfun)
apply (simp add: contraction_alpha_tracesfun_Seq_compo)
apply (simp add: contraction_alpha_tracesfun_Depth_rest)
done

lemma contraction_alpha_tracesfun: 
  "Pf : gProcfun ==> contraction_alpha (tracesfun Pf) (1/2)"
by (simp add: contraction_alpha_tracesfun_lm)

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

lemma contraction_alpha_semTfun: 
  "Pf : gProcfun ==> contraction_alpha [[Pf]]Tfun (1/2)"
by (simp add: semT_to_traces contraction_alpha_tracesfun)

(*=============================================================*
 |                       tracesfun P                           |
 *=============================================================*)

lemma contraction_alpha_tracesFun: 
  "PF : gProcFun ==> contraction_alpha (tracesFun PF) (1/2)"
apply (simp add: prod_contra_alpha)
apply (rule allI)
apply (simp add: proj_tracesFun_tracesfun)
apply (simp add: nohideFun_def gProcFun_def)
apply (drule_tac x="i" in spec)
apply (simp add: contraction_alpha_tracesfun)
done

lemma contraction_tracesFun:
  "PF : gProcFun ==> contraction (tracesFun PF)"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
apply (simp add: contraction_alpha_tracesFun)
done

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

lemma contraction_alpha_semTFun: 
  "PF : gProcFun ==> contraction_alpha [[PF]]TFun (1/2)"
by (simp add: semT_to_traces contraction_alpha_tracesFun)

lemma contraction_semTFun: 
  "PF : gProcFun ==> contraction [[PF]]TFun"
by (simp add: semT_to_traces contraction_tracesFun)

end