Theory Act_prefix_cms

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

theory Act_prefix_cms = Act_prefix + 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. [[a -> P]]T : contraction map
         2. [[a -> P]]F : contraction map
         3. 
         4. 

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

(*********************************************************
                     map prefix T
 *********************************************************)

lemma Act_prefix_evalT_contraction_half_lm: 
   "distance ([[a -> P]]T ev1, [[a -> P]]T ev2) * 2
    = distance ([[P]]T ev1, [[P]]T ev2)"
apply (rule sym)
apply (rule rest_Suc_dist_half[simplified])
apply (rule allI)
apply (simp add: restT_eq_iff)
apply (rule iffI)

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

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

 (* <= *)
 apply (rule allI)
 apply (drule_tac x="[Ev a]t @t s" in spec)
 apply (case_tac "s = None", simp)
 apply (simp add: Act_prefix_memT)
done

(*** Act_prefix_evalT_contraction ***)

lemma Act_prefix_evalT_contraction_half: 
 "non_expanding [[P]]T ==> contraction_alpha [[a -> P]]T (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: Act_prefix_evalT_contraction_half_lm)
done

(*** Act_prefix_evalT_contraction ***)

lemma Act_prefix_evalT_contraction:
 "non_expanding [[P]]T ==> contraction [[a -> P]]T"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
by (simp add: Act_prefix_evalT_contraction_half)

(*** Act_prefix_evalT_non_expanding ***)

lemma Act_prefix_evalT_non_expanding: 
 "non_expanding [[P]]T ==> non_expanding [[a -> P]]T"
apply (rule contraction_non_expanding)
by (simp add: Act_prefix_evalT_contraction)

(*********************************************************
                     map prefix F
 *********************************************************)

lemma Act_prefix_evalF_contraction_half_lm: 
   "distance ([[a -> P]]F ev1, [[a -> P]]F ev2) * 2
    = distance ([[P]]F ev1, [[P]]F ev2)"
apply (rule sym)
apply (rule rest_Suc_dist_half[simplified])
apply (rule allI)
apply (simp add: restF_eq_iff)
apply (rule iffI)

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

  (* => *)
  apply (elim conjE exE disjE)
   apply (simp_all)

   apply (simp add: not_None)
   apply (drule_tac x="sa" in spec)
   apply (drule_tac x="X" in spec)
   apply (simp)

   apply (simp add: not_None)
   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 (simp add: not_None)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (simp add: appt_ass_rev del: appt_ass)

  (* <= *)
  apply (elim conjE exE disjE)
   apply (simp_all)

   apply (simp add: not_None)
   apply (drule_tac x="sa" in spec)
   apply (drule_tac x="X" in spec)
   apply (simp)

   apply (simp add: not_None)
   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 (simp add: not_None)
   apply (erule disjE, simp)
   apply (elim conjE exE)
   apply (simp add: appt_ass_rev del: appt_ass)

 (* <= *)
 apply (intro allI)
 apply (drule_tac x="[Ev a]t @t s" in spec)
 apply (drule_tac x="X" in spec)
 apply (case_tac "s = None", simp)
 apply (simp add: Act_prefix_memF)
 apply (rule iffI)

  (* => *)
  apply (elim conjE exE disjE)
   apply (simp)
   apply (subgoal_tac "notick([Ev a]t @t s')")
    apply (simp add: appt_ass_rev del: appt_ass)
   apply (case_tac "~ notick s'", simp, simp)

  (* <= *)
  apply (elim conjE exE disjE)
   apply (simp)
   apply (subgoal_tac "notick([Ev a]t @t s')")
    apply (simp add: appt_ass_rev del: appt_ass)
   apply (case_tac "~ notick s'", simp, simp)
done

(*** Act_prefix_evalF_contraction ***)

lemma Act_prefix_evalF_contraction_half: 
 "non_expanding [[P]]F ==> contraction_alpha [[a -> P]]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: Act_prefix_evalF_contraction_half_lm)
done

(*** Act_prefix_evalF_contraction ***)

lemma Act_prefix_evalF_contraction:
 "non_expanding [[P]]F ==> contraction [[a -> P]]F"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
by (simp add: Act_prefix_evalF_contraction_half)

(*** Act_prefix_evalF_non_expanding ***)

lemma Act_prefix_evalF_non_expanding: 
 "non_expanding [[P]]F ==> non_expanding [[a -> P]]F"
apply (rule contraction_non_expanding)
by (simp add: Act_prefix_evalF_contraction)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end