Theory Renaming_cms

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Renaming_cms = Renaming + Domain_SF_prod_cms:

(*  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]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

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

         1. [[P [[r]]]]T : non expanding
         2. [[P [[r]]]]F : non expanding
         3. 
         4. 

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

(*********************************************************
                   map Renaming T
 *********************************************************)

(*** restT (subset) ***)

lemma Renaming_restT_sub:
   "[[P]]T ev1 rest n <= [[P]]T ev2 rest n
    ==> [[P [[r]]]]T ev1 rest n <= [[P [[r]]]]T ev2 rest n"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: in_restT)
apply (simp add: Renaming_memT)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
apply (drule_tac x="s" in spec)
by (simp add: ren_tr_lengtht)

(*** restT (equal) ***)

lemma Renaming_restT:
   "[[P]]T ev1 rest n = [[P]]T ev2 rest n
    ==> [[P [[r]]]]T ev1 rest n = [[P [[r]]]]T ev2 rest n"
apply (rule order_antisym)
by (simp_all add: Renaming_restT_sub)

(*** distT lemma ***)

lemma Renaming_distT:
     "distance([[P [[r]]]]T ev1, [[P [[r]]]]T ev2) 
   <= distance([[P]]T ev1, [[P]]T ev2)"
apply (rule rest_distance_subset)
by (auto intro: Renaming_restT)

(*** map_alphaT lemma ***)

lemma Renaming_evalT_map_alpha_lm:
  "distance ([[P]]T ev1, [[P]]T ev2) <= alpha * distance (ev1, ev2)
    ==> distance ([[P [[r]]]]T ev1, [[P [[r]]]]T ev2)
     <= alpha * distance (ev1, ev2)"
apply (insert Renaming_distT[of P r ev1 ev2])
by (simp)

(*** Renaming_evalT_map_alpha ***)

lemma Renaming_evalT_map_alpha:
 "map_alpha [[P]]T alpha ==> map_alpha [[P [[r]]]]T 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)
by (simp add: Renaming_evalT_map_alpha_lm)

(*** Renaming_evalT_non_expanding ***)

lemma Renaming_evalT_non_expanding:
 "non_expanding [[P]]T ==> non_expanding [[P [[r]]]]T"
by (simp add: non_expanding_def Renaming_evalT_map_alpha)

(*** Renaming_evalT_contraction_alpha ***)

lemma Renaming_evalT_contraction_alpha:
 "contraction_alpha [[P]]T alpha ==> contraction_alpha [[P [[r]]]]T alpha"
by (simp add: contraction_alpha_def Renaming_evalT_map_alpha)

(*********************************************************
                   map Renaming F
 *********************************************************)

(*** restF (subset) ***)

lemma Renaming_restF_sub:
   "[[P]]F ev1 rest n <= [[P]]F ev2 rest n
    ==> [[P [[r]]]]F ev1 rest n <= [[P [[r]]]]F ev2 rest n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_restF)
apply (simp add: Renaming_memF)
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: not_None_F ren_tr_appt_decompo_right)
apply (elim conjE exE, simp)
by (fast)

(*** restF (equal) ***)

lemma Renaming_restF:
   "[[P]]F ev1 rest n = [[P]]F ev2 rest n
    ==> [[P [[r]]]]F ev1 rest n = [[P [[r]]]]F ev2 rest n"
apply (rule order_antisym)
by (simp_all add: Renaming_restF_sub)

(*** distF lemma ***)

lemma Renaming_distF:
     "distance([[P [[r]]]]F ev1, [[P [[r]]]]F ev2) 
   <= distance([[P]]F ev1, [[P]]F ev2)"
apply (rule rest_distance_subset)
by (auto intro: Renaming_restF)

(*** map_alphaF lemma ***)

lemma Renaming_evalF_map_alpha_lm:
  "distance ([[P]]F ev1, [[P]]F ev2) <= alpha * distance (ev1, ev2)
    ==> distance ([[P [[r]]]]F ev1, [[P [[r]]]]F ev2)
     <= alpha * distance (ev1, ev2)"
apply (insert Renaming_distF[of P r ev1 ev2])
by (simp)

(*** Renaming_evalF_map_alpha ***)

lemma Renaming_evalF_map_alpha:
 "map_alpha [[P]]F alpha ==> map_alpha [[P [[r]]]]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="y" in spec)
by (simp add: Renaming_evalF_map_alpha_lm)

(*** Renaming_evalF_non_expanding ***)

lemma Renaming_evalF_non_expanding:
 "non_expanding [[P]]F ==> non_expanding [[P [[r]]]]F"
by (simp add: non_expanding_def Renaming_evalF_map_alpha)

(*** Renaming_evalF_contraction_alpha ***)

lemma Renaming_evalF_contraction_alpha:
 "contraction_alpha [[P]]F alpha ==> contraction_alpha [[P [[r]]]]F alpha"
by (simp add: contraction_alpha_def Renaming_evalF_map_alpha)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end