Theory Seq_compo_cms (Isabelle2004: April 2004)

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

theory Seq_compo_cms = Seq_compo + 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 ;; Q]]T : non expanding
         2. [[P ;; Q]]F : non expanding
         3. 
         4. 

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

(*********************************************************
                   map Seq_compo T
 *********************************************************)

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

lemma Seq_compo_restT_sub:
   "[| [[P]]T ev1 rest n <= [[P]]T ev2 rest n ;
       [[Q]]T ev1 rest n <= [[Q]]T ev2 rest n |]
    ==> [[P ;; Q]]T ev1 rest n <= [[P ;; Q]]T ev2 rest n"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: in_restT)
apply (simp add: Seq_compo_memT)
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, simp add: not_None_T)
 apply (erule disjE, simp)
 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 add: not_None_T)
 apply (insert trace_last_nil_or_unnil)
 apply (rotate_tac -1)
 apply (drule_tac x="ta" in spec, simp add: not_None_T)
 apply (erule disjE, simp)

  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 (simp add: appt_ass_rev del: appt_ass)

  apply (drule_tac x="s @t [Tick]t" in spec)
  apply (drule_tac x=" sa @t [a]t" in spec)
  apply (simp)
  apply (rule_tac x="s" in exI)
  apply (rule_tac x="sa @t [a]t" in exI)
  apply (simp add: not_None)
done

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

lemma Seq_compo_restT:
   "[| [[P]]T ev1 rest n = [[P]]T ev2 rest n ;
       [[Q]]T ev1 rest n = [[Q]]T ev2 rest n |]
    ==> [[P ;; Q]]T ev1 rest n = [[P ;; Q]]T ev2 rest n"
apply (rule order_antisym)
by (simp_all add: Seq_compo_restT_sub)

(*** distT lemma ***)

lemma Seq_compo_distT:
"TTs = {([[P]]T ev1, [[P]]T ev2), ([[Q]]T ev1, [[Q]]T ev2)}
 ==> (EX TT. TT:TTs & 
             distance([[P ;; Q]]T ev1, [[P ;; Q]]T ev2) 
          <= distance((fst TT), (snd TT)))"
apply (rule rest_to_dist_pair)
by (auto intro: Seq_compo_restT)

(*** map_alpha T lemma ***)

lemma Seq_compo_evalT_map_alpha_lm:
  "[| distance ([[P]]T ev1, [[P]]T ev2) <= alpha * distance (ev1, ev2) ;
      distance ([[Q]]T ev1, [[Q]]T ev2) <= alpha * distance (ev1, ev2) |]
    ==> distance ([[P ;; Q]]T ev1, [[P ;; Q]]T ev2)
     <= alpha * distance (ev1, ev2)"
apply (insert Seq_compo_distT
       [of "{([[P]]T ev1, [[P]]T ev2), ([[Q]]T ev1, [[Q]]T ev2)}" P ev1 ev2 Q])
by (auto)

(*** Seq_compo_evalT_map_alpha ***)

lemma Seq_compo_evalT_map_alpha:
 "[| map_alpha [[P]]T alpha ; map_alpha [[Q]]T alpha |]
  ==> map_alpha [[P ;; Q]]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="x" in spec)
apply (drule_tac x="y" in spec)
apply (drule_tac x="y" in spec)
by (simp add: Seq_compo_evalT_map_alpha_lm)

(*** Seq_compo_evalT_non_expanding ***)

lemma Seq_compo_evalT_non_expanding:
 "[| non_expanding [[P]]T ; non_expanding [[Q]]T |]
  ==> non_expanding [[P ;; Q]]T"
by (simp add: non_expanding_def Seq_compo_evalT_map_alpha)

(*** Seq_compo_evalT_contraction_alpha ***)

lemma Seq_compo_evalT_contraction_alpha:
 "[| contraction_alpha [[P]]T alpha; contraction_alpha [[Q]]T alpha|]
  ==> contraction_alpha [[P ;; Q]]T alpha"
by (simp add: contraction_alpha_def Seq_compo_evalT_map_alpha)

(*********************************************************
                   map Seq_compo F
 *********************************************************)

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

lemma Seq_compo_restF_sub:
   "[| [[P]]T ev1 rest n <= [[P]]T ev2 rest n ;
       [[P]]F ev1 rest n <= [[P]]F ev2 rest n ;
       [[Q]]F ev1 rest n <= [[Q]]F ev2 rest n |]
    ==> [[P ;; Q]]F ev1 rest n <= [[P ;; Q]]F ev2 rest n"
apply (simp add: subsetT_iff subsetF_iff)
apply (intro allI impI)
apply (simp add: in_restT in_restF)
apply (simp add: Seq_compo_memF)
apply (elim conjE)

 (* case 1 *)
 apply (erule disjE)
 apply (rotate_tac 1)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="insert Tick X" in spec, simp)

 (* case 2 *)
 apply (elim conjE exE)
 apply (case_tac "~ notick sa", simp add: not_None_T)
 apply (case_tac "sa @t t = None", simp add: not_None)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)

  (* < n *)
  apply (erule disjE)
  apply (simp)

  (* = n *)
  apply (elim conjE exE, simp)
  apply (insert trace_last_nil_or_unnil)
  apply (rotate_tac -1)
  apply (drule_tac x="t" in spec, simp add: not_None_F)
  apply (erule disjE, simp)
  apply (elim conjE exE, simp)
  apply (simp add: appt_ass_rev del: appt_ass)

  apply (rotate_tac 2)
  apply (drule_tac x="sb @t [Tick]t" in spec)
  apply (drule_tac x="X" in spec, simp)
  apply (force)
done

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

lemma Seq_compo_restF:
   "[| [[P]]T ev1 rest n = [[P]]T ev2 rest n ;
       [[P]]F ev1 rest n = [[P]]F ev2 rest n ;
       [[Q]]F ev1 rest n = [[Q]]F ev2 rest n |]
    ==> [[P ;; Q]]F ev1 rest n = [[P ;; Q]]F ev2 rest n"
apply (rule order_antisym)
by (simp_all add: Seq_compo_restF_sub)

(*** distF lemma ***)

lemma Seq_compo_distF:
"[| TTs = {([[P]]T ev1, [[P]]T ev2)} ;
    FFs = {([[P]]F ev1, [[P]]F ev2), ([[Q]]F ev1, [[Q]]F ev2)} |]
   ==> (EX TT. TT:TTs & 
             distance([[P ;; Q]]F ev1, [[P ;; Q]]F ev2) 
          <= distance((fst TT), (snd TT))) |
       (EX FF. FF:FFs & 
             distance([[P ;; Q]]F ev1, [[P ;; Q]]F ev2) 
          <= distance((fst FF), (snd FF)))"
apply (rule rest_to_dist_pair_two)
by (auto intro: Seq_compo_restF)

(*** map_alpha F lemma ***)

lemma Seq_compo_evalF_map_alpha_lm:
  "[| distance ([[P]]T ev1, [[P]]T ev2) <= alpha * distance (ev1, ev2) ;
      distance ([[P]]F ev1, [[P]]F ev2) <= alpha * distance (ev1, ev2) ;
      distance ([[Q]]F ev1, [[Q]]F ev2) <= alpha * distance (ev1, ev2) |]
    ==> distance ([[P ;; Q]]F ev1, [[P ;; Q]]F ev2)
     <= alpha * distance (ev1, ev2)"
apply (insert Seq_compo_distF
       [of "{([[P]]T ev1, [[P]]T ev2)}" P ev1 ev2
           "{([[P]]F ev1, [[P]]F ev2), ([[Q]]F ev1, [[Q]]F ev2)}" Q])
by (auto)

(*** Seq_compo_evalF_map_alpha ***)

lemma Seq_compo_evalF_map_alpha:
 "[| map_alpha [[P]]T alpha ; map_alpha [[P]]F alpha ; map_alpha [[Q]]F alpha |]
  ==> map_alpha [[P ;; Q]]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)
by (simp add: Seq_compo_evalF_map_alpha_lm)

(*** Seq_compo_evalF_non_expanding ***)

lemma Seq_compo_evalF_non_expanding:
 "[| non_expanding [[P]]T ; non_expanding [[P]]F ; non_expanding [[Q]]F |]
  ==> non_expanding [[P ;; Q]]F"
by (simp add: non_expanding_def Seq_compo_evalF_map_alpha)

(*** Seq_compo_evalF_contraction_alpha ***)

lemma Seq_compo_evalF_contraction_alpha:
 "[| contraction_alpha [[P]]T alpha; 
     contraction_alpha [[P]]F alpha; contraction_alpha [[Q]]F alpha|]
  ==> contraction_alpha [[P ;; Q]]F alpha"
by (simp add: contraction_alpha_def Seq_compo_evalF_map_alpha)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end

lemma Seq_compo_restT_sub:

  [| [[P]]T ev1 rest n ≤ [[P]]T ev2 rest n;
     [[Q]]T ev1 rest n ≤ [[Q]]T ev2 rest n |]
  ==> [[P ;; Q]]T ev1 rest n ≤ [[P ;; Q]]T ev2 rest n

lemma Seq_compo_restT:

  [| [[P]]T ev1 rest n = [[P]]T ev2 rest n;
     [[Q]]T ev1 rest n = [[Q]]T ev2 rest n |]
  ==> [[P ;; Q]]T ev1 rest n = [[P ;; Q]]T ev2 rest n

lemma Seq_compo_distT:

  TTs = {([[P]]T ev1, [[P]]T ev2), ([[Q]]T ev1, [[Q]]T ev2)}
  ==> ∃TT. TT ∈ TTs ∧
           distance ([[P ;; Q]]T ev1, [[P ;; Q]]T ev2) ≤ distance (fst TT, snd TT)

lemma Seq_compo_evalT_map_alpha_lm:

  [| distance ([[P]]T ev1, [[P]]T ev2) ≤ alpha * distance (ev1, ev2);
     distance ([[Q]]T ev1, [[Q]]T ev2) ≤ alpha * distance (ev1, ev2) |]
  ==> distance ([[P ;; Q]]T ev1, [[P ;; Q]]T ev2) ≤ alpha * distance (ev1, ev2)

lemma Seq_compo_evalT_map_alpha:

  [| map_alpha [[P]]T alpha; map_alpha [[Q]]T alpha |]
  ==> map_alpha [[P ;; Q]]T alpha

lemma Seq_compo_evalT_non_expanding:

  [| non_expanding [[P]]T; non_expanding [[Q]]T |] ==> non_expanding [[P ;; Q]]T

lemma Seq_compo_evalT_contraction_alpha:

  [| contraction_alpha [[P]]T alpha; contraction_alpha [[Q]]T alpha |]
  ==> contraction_alpha [[P ;; Q]]T alpha

lemma Seq_compo_restF_sub:

  [| [[P]]T ev1 rest n ≤ [[P]]T ev2 rest n; [[P]]F ev1 rest n ≤ [[P]]F ev2 rest n;
     [[Q]]F ev1 rest n ≤ [[Q]]F ev2 rest n |]
  ==> [[P ;; Q]]F ev1 rest n ≤ [[P ;; Q]]F ev2 rest n

lemma Seq_compo_restF:

  [| [[P]]T ev1 rest n = [[P]]T ev2 rest n; [[P]]F ev1 rest n = [[P]]F ev2 rest n;
     [[Q]]F ev1 rest n = [[Q]]F ev2 rest n |]
  ==> [[P ;; Q]]F ev1 rest n = [[P ;; Q]]F ev2 rest n

lemma Seq_compo_distF:

  [| TTs = {([[P]]T ev1, [[P]]T ev2)};
     FFs = {([[P]]F ev1, [[P]]F ev2), ([[Q]]F ev1, [[Q]]F ev2)} |]
  ==> (∃TT. TT ∈ TTs ∧
            distance ([[P ;; Q]]F ev1, [[P ;; Q]]F ev2)
            ≤ distance (fst TT, snd TT)) ∨
      (∃FF. FF ∈ FFs ∧
            distance ([[P ;; Q]]F ev1, [[P ;; Q]]F ev2)
            ≤ distance (fst FF, snd FF))

lemma Seq_compo_evalF_map_alpha_lm:

  [| distance ([[P]]T ev1, [[P]]T ev2) ≤ alpha * distance (ev1, ev2);
     distance ([[P]]F ev1, [[P]]F ev2) ≤ alpha * distance (ev1, ev2);
     distance ([[Q]]F ev1, [[Q]]F ev2) ≤ alpha * distance (ev1, ev2) |]
  ==> distance ([[P ;; Q]]F ev1, [[P ;; Q]]F ev2) ≤ alpha * distance (ev1, ev2)

lemma Seq_compo_evalF_map_alpha:

  [| map_alpha [[P]]T alpha; map_alpha [[P]]F alpha; map_alpha [[Q]]F alpha |]
  ==> map_alpha [[P ;; Q]]F alpha

lemma Seq_compo_evalF_non_expanding:

  [| non_expanding [[P]]T; non_expanding [[P]]F; non_expanding [[Q]]F |]
  ==> non_expanding [[P ;; Q]]F

lemma Seq_compo_evalF_contraction_alpha:

  [| contraction_alpha [[P]]T alpha; contraction_alpha [[P]]F alpha;
     contraction_alpha [[Q]]F alpha |]
  ==> contraction_alpha [[P ;; Q]]F alpha