Theory CSP_law_decompo

Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover

theory CSP_law_decompo = CSP_proc: 
           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_law_decompo = CSP_proc:

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

declare not_None_eq [simp del]

(*------------------------------------------------*
 |                                                |
 |      laws for monotonicity and congruence      |
 |                                                |
 *------------------------------------------------*)

(*********************************************************
                        Act_prefix mono
 *********************************************************)

lemma domSF_Act_prefix_mono:
  "[| a = b ; [[P]]SF ev1 <= [[Q]]SF ev2 |]
     ==> [[a -> P]]SF ev1 <= [[b -> Q]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Act_prefix_evalT_mono)
apply (simp add: Act_prefix_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Act_prefix_mono:
  "[| a = b ; LET:fp1 df IN P <=F LET:fp2 df IN Q |]
     ==> LET:fp1 df IN a -> P <=F LET:fp2 df IN b -> Q"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Act_prefix_mono)

lemma csp_Act_prefix_cong:
  "[| a = b ; LET:fp1 df IN P =F LET:fp2 df IN Q |]
     ==> LET:fp1 df IN a -> P =F LET:fp2 df IN b -> Q"
by (simp add: csp_eq_ref_iff csp_Act_prefix_mono)

(*********************************************************
                   Ext_pre_choice mono 
 *********************************************************)

lemma domSF_Ext_pre_choice_mono:
  "[|  X = Y ; !! a. a:Y ==> [[Pf a]]SF ev1 <= [[Qf a]]SF ev2 |]
     ==> [[? :X -> Pf]]SF ev1 <= [[? :Y -> Qf]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Ext_pre_choice_evalT_mono)
apply (simp add: Ext_pre_choice_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Ext_pre_choice_mono:
  "[| X = Y ; !! a. a:Y ==> LET:fp1 df IN Pf a <=F LET:fp2 df IN Qf a |]
      ==> LET:fp1 df IN ? :X -> Pf <=F LET:fp2 df IN ? :Y -> Qf"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Ext_pre_choice_mono)

lemma csp_Ext_pre_choice_cong:
  "[| X = Y ; !! a. a:Y ==> LET:fp1 df IN Pf a =F LET:fp2 df IN Qf a |]
      ==> LET:fp1 df IN ? :X -> Pf =F LET:fp2 df IN ? :Y -> Qf"
by (simp add: csp_eq_ref_iff csp_Ext_pre_choice_mono)

(*********************************************************
                      Ext choice mono
 *********************************************************)

lemma domSF_Ext_choice_mono:
  "[| [[P1]]SF ev1 <= [[Q1]]SF ev2 ; [[P2]]SF ev1 <= [[Q2]]SF ev2 |]
     ==> [[P1 [+] P2]]SF ev1 <= [[Q1 [+] Q2]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Ext_choice_evalT_mono)
apply (simp add: Ext_choice_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Ext_choice_mono:
  "[| LET:fp1 df IN P1 <=F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 <=F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 [+] P2 <=F LET:fp2 df IN Q1 [+] Q2"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Ext_choice_mono)

lemma csp_Ext_choice_cong:
  "[| LET:fp1 df IN P1 =F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 =F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 [+] P2 =F LET:fp2 df IN Q1 [+] Q2"
by (simp add: csp_eq_ref_iff csp_Ext_choice_mono)

(*********************************************************
                      Int choice mono
 *********************************************************)

lemma domSF_Int_choice_mono:
  "[| [[P1]]SF ev1 <= [[Q1]]SF ev2 ; [[P2]]SF ev1 <= [[Q2]]SF ev2 |]
     ==> [[P1 |~| P2]]SF ev1 <= [[Q1 |~| Q2]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Int_choice_evalT_mono)
apply (simp add: Int_choice_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Int_choice_mono:
  "[| LET:fp1 df IN P1 <=F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 <=F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 |~| P2 <=F LET:fp2 df IN Q1 |~| Q2"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Int_choice_mono)

lemma csp_Int_choice_cong:
  "[| LET:fp1 df IN P1 =F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 =F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 |~| P2 =F LET:fp2 df IN Q1 |~| Q2"
by (simp add: csp_eq_ref_iff csp_Int_choice_mono)

(*********************************************************
               replicated internal choice
 *********************************************************)

lemma domSF_Rep_int_choice_mono:
  "[|  X = Y ; !! a. a:Y ==> [[Pf a]]SF ev1 <= [[Qf a]]SF ev2 |]
     ==> [[! :X .. Pf]]SF ev1 <= [[! :Y .. Qf]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Rep_int_choice_evalT_mono)
apply (simp add: Rep_int_choice_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Rep_int_choice_mono:
  "[| X = Y ; !! a. a:Y ==> LET:fp1 df IN Pf a <=F LET:fp2 df IN Qf a |]
      ==> LET:fp1 df IN ! :X .. Pf <=F LET:fp2 df IN ! :Y .. Qf"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Rep_int_choice_mono)

lemma csp_Rep_int_choice_cong:
  "[| X = Y ; !! a. a:Y ==> LET:fp1 df IN Pf a =F LET:fp2 df IN Qf a |]
      ==> LET:fp1 df IN ! :X .. Pf =F LET:fp2 df IN ! :Y .. Qf"
by (simp add: csp_eq_ref_iff csp_Rep_int_choice_mono)

(*********************************************************
                   Conditional mono
 *********************************************************)

lemma domSF_Conditional_mono:
  "[| b1 = b2 ; [[P1]]SF ev1 <= [[Q1]]SF ev2 ; [[P2]]SF ev1 <= [[Q2]]SF ev2 |]
     ==> [[IF b1 THEN P1 ELSE P2]]SF ev1 <= 
         [[IF b2 THEN Q1 ELSE Q2]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Conditional_evalT_mono)
apply (simp add: Conditional_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Conditional_mono:
  "[| b1 = b2 ;
      LET:fp1 df IN P1 <=F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 <=F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN IF b1 THEN P1 ELSE P2 <=F
               LET:fp2 df IN IF b2 THEN Q1 ELSE Q2"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Conditional_mono)

lemma csp_Conditional_cong:
  "[| b1 = b2 ;
      LET:fp1 df IN P1 =F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 =F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN IF b1 THEN P1 ELSE P2 =F
               LET:fp2 df IN IF b2 THEN Q1 ELSE Q2"
by (simp add: csp_eq_ref_iff csp_Conditional_mono)

(*********************************************************
                     Parallel mono 
 *********************************************************)

lemma domSF_Parallel_mono:
  "[| X = Y ; [[P1]]SF ev1 <= [[Q1]]SF ev2 ; [[P2]]SF ev1 <= [[Q2]]SF ev2 |]
     ==> [[P1 |[X]| P2]]SF ev1 <= [[Q1 |[X]| Q2]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Parallel_evalT_mono)
apply (simp add: Parallel_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Parallel_mono:
  "[| X = Y ;
      LET:fp1 df IN P1 <=F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 <=F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 |[X]| P2 <=F LET:fp2 df IN Q1 |[Y]| Q2"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Parallel_mono)

lemma csp_Parallel_cong:
  "[| X = Y ;
      LET:fp1 df IN P1 =F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 =F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 |[X]| P2 =F LET:fp2 df IN Q1 |[Y]| Q2"
by (simp add: csp_eq_ref_iff csp_Parallel_mono)

(*********************************************************
                        Hiding mono
 *********************************************************)

lemma domSF_Hiding_mono:
  "[| X = Y ; [[P]]SF ev1 <= [[Q]]SF ev2 |]
     ==> [[P -- X]]SF ev1 <= [[Q -- X]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Hiding_evalT_mono)
apply (simp add: Hiding_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Hiding_mono:
  "[| X = Y ; LET:fp1 df IN P <=F LET:fp2 df IN Q |]
    ==> LET:fp1 df IN P -- X <=F LET:fp2 df IN Q -- Y"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Hiding_mono)

lemma csp_Hiding_cong:
  "[| X = Y ; LET:fp1 df IN P =F LET:fp2 df IN Q |]
    ==> LET:fp1 df IN P -- X =F LET:fp2 df IN Q -- Y"
by (simp add: csp_eq_ref_iff csp_Hiding_mono)

(*********************************************************
                        Renaming mono
 *********************************************************)

lemma domSF_Renaming_mono:
  "[| r1 = r2 ; [[P]]SF ev1 <= [[Q]]SF ev2 |]
     ==> [[P [[r1]]]]SF ev1 <= [[Q [[r2]]]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Renaming_evalT_mono)
apply (simp add: Renaming_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Renaming_mono:
  "[| r1 = r2 ; LET:fp1 df IN P <=F LET:fp2 df IN Q |]
   ==> LET:fp1 df IN P [[r1]] <=F LET:fp2 df IN Q [[r2]]"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Renaming_mono)

lemma csp_Renaming_cong:
  "[| r1 = r2 ; LET:fp1 df IN P =F LET:fp2 df IN Q |]
   ==> LET:fp1 df IN P [[r1]] =F LET:fp2 df IN Q [[r2]]"
by (simp add: csp_eq_ref_iff csp_Renaming_mono)

(*********************************************************
               Sequential composition mono 
 *********************************************************)

lemma domSF_Seq_compo_mono:
  "[| [[P1]]SF ev1 <= [[Q1]]SF ev2 ; [[P2]]SF ev1 <= [[Q2]]SF ev2 |]
     ==> [[P1 ;; P2]]SF ev1 <= [[Q1 ;; Q2]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (simp add: Seq_compo_evalT_mono)
apply (simp add: Seq_compo_evalF_mono)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Seq_compo_mono:
  "[| LET:fp1 df IN P1 <=F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 <=F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 ;; P2 <=F LET:fp2 df IN Q1 ;; Q2"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Seq_compo_mono)

lemma csp_Seq_compo_cong:
  "[| LET:fp1 df IN P1 =F LET:fp2 df IN Q1 ; 
      LET:fp1 df IN P2 =F LET:fp2 df IN Q2 |]
           ==> LET:fp1 df IN P1 ;; P2 =F LET:fp2 df IN Q1 ;; Q2"
by (simp add: csp_eq_ref_iff csp_Seq_compo_mono)

(*********************************************************
                        Timeout mono
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Timeout_mono:
  "[| LET:fp1 df IN P1 <=F LET:fp2 df IN Q1 ;
      LET:fp1 df IN P2 <=F LET:fp2 df IN Q2 |]
      ==> LET:fp1 df IN P1 [> P2 <=F LET:fp2 df IN Q1 [> Q2"
apply (rule csp_Ext_choice_mono)
apply (rule csp_Int_choice_mono)
apply (simp_all)

apply (simp add: refF_def)
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
apply (simp_all add: proc_subsetSF_decompo)
apply (simp_all add: evalT_def evalF_def)
done

lemma csp_Timeout_cong:
  "[| LET:fp1 df IN P1 =F LET:fp2 df IN Q1 ;
      LET:fp1 df IN P2 =F LET:fp2 df IN Q2 |]
      ==> LET:fp1 df IN P1 [> P2 =F LET:fp2 df IN Q1 [> Q2"
by (simp add: csp_eq_ref_iff csp_Timeout_mono)

(*------------------------------------------------------*
 |                       alias                          |
 *------------------------------------------------------*)

lemmas csp_free_mono =
   csp_Ext_choice_mono csp_Int_choice_mono csp_Parallel_mono
   csp_Hiding_mono csp_Renaming_mono csp_Seq_compo_mono

lemmas csp_mono = csp_free_mono
   csp_Act_prefix_mono csp_Ext_pre_choice_mono 
   csp_Rep_int_choice_mono csp_Conditional_mono 

lemmas csp_free_cong =
   csp_Ext_choice_cong csp_Int_choice_cong csp_Parallel_cong
   csp_Hiding_cong csp_Renaming_cong csp_Seq_compo_cong

lemmas csp_cong = csp_free_cong
   csp_Act_prefix_cong csp_Ext_pre_choice_cong 
   csp_Rep_int_choice_cong csp_Conditional_cong 

lemmas csp_free_decompo = csp_free_mono csp_free_cong
lemmas csp_decompo = csp_mono csp_cong

lemmas csp_rm_head_mono = csp_Act_prefix_mono csp_Ext_pre_choice_mono 
lemmas csp_rm_head_cong = csp_Act_prefix_cong csp_Ext_pre_choice_cong
lemmas csp_rm_head      = csp_rm_head_mono csp_rm_head_cong

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

declare not_None_eq    [simp]

end

lemma domSF_Act_prefix_mono: 

  [| a = b; [[P]]SF ev1 ≤ [[Q]]SF ev2 |] ==> [[a -> P]]SF ev1 ≤ [[b -> Q]]SF ev2

lemma csp_Act_prefix_mono: 

  [| a = b; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P <=F 
      LET:fp2 df IN b -> Q

lemma csp_Act_prefix_cong: 

  [| a = b; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P =F 
      LET:fp2 df IN b -> Q

lemma domSF_Ext_pre_choice_mono: 

  [| X = Y; !!a. a ∈ Y ==> [[Pf a]]SF ev1 ≤ [[Qf a]]SF ev2 |]
  ==> [[? :X -> Pf]]SF ev1 ≤ [[? :Y -> Qf]]SF ev2

lemma csp_Ext_pre_choice_mono: 

  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf <=F 
      LET:fp2 df IN ? :Y -> Qf

lemma csp_Ext_pre_choice_cong: 

  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf =F 
      LET:fp2 df IN ? :Y -> Qf

lemma domSF_Ext_choice_mono: 

  [| [[P1]]SF ev1 ≤ [[Q1]]SF ev2; [[P2]]SF ev1 ≤ [[Q2]]SF ev2 |]
  ==> [[P1 [+] P2]]SF ev1 ≤ [[Q1 [+] Q2]]SF ev2

lemma csp_Ext_choice_mono: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 <=F 
      LET:fp2 df IN Q1 [+] Q2

lemma csp_Ext_choice_cong: 

  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 =F 
      LET:fp2 df IN Q1 [+] Q2

lemma domSF_Int_choice_mono: 

  [| [[P1]]SF ev1 ≤ [[Q1]]SF ev2; [[P2]]SF ev1 ≤ [[Q2]]SF ev2 |]
  ==> [[P1 |~| P2]]SF ev1 ≤ [[Q1 |~| Q2]]SF ev2

lemma csp_Int_choice_mono: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 <=F 
      LET:fp2 df IN Q1 |~| Q2

lemma csp_Int_choice_cong: 

  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 =F 
      LET:fp2 df IN Q1 |~| Q2

lemma domSF_Rep_int_choice_mono: 

  [| X = Y; !!a. a ∈ Y ==> [[Pf a]]SF ev1 ≤ [[Qf a]]SF ev2 |]
  ==> [[! :X .. Pf]]SF ev1 ≤ [[! :Y .. Qf]]SF ev2

lemma csp_Rep_int_choice_mono: 

  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf <=F 
      LET:fp2 df IN ! :Y .. Qf

lemma csp_Rep_int_choice_cong: 

  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf =F 
      LET:fp2 df IN ! :Y .. Qf

lemma domSF_Conditional_mono: 

  [| b1 = b2; [[P1]]SF ev1 ≤ [[Q1]]SF ev2; [[P2]]SF ev1 ≤ [[Q2]]SF ev2 |]
  ==> [[IF b1 THEN P1 ELSE P2]]SF ev1 ≤ [[IF b2 THEN Q1 ELSE Q2]]SF ev2

lemma csp_Conditional_mono: 

  [| b1 = b2; 
              LET:fp1 df IN P1 <=F 
              LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN IF b1 THEN P1 ELSE P2 <=F 
      LET:fp2 df IN IF b2 THEN Q1 ELSE Q2

lemma csp_Conditional_cong: 

  [| b1 = b2; 
              LET:fp1 df IN P1 =F 
              LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN IF b1 THEN P1 ELSE P2 =F 
      LET:fp2 df IN IF b2 THEN Q1 ELSE Q2

lemma domSF_Parallel_mono: 

  [| X = Y; [[P1]]SF ev1 ≤ [[Q1]]SF ev2; [[P2]]SF ev1 ≤ [[Q2]]SF ev2 |]
  ==> [[P1 |[X]| P2]]SF ev1 ≤ [[Q1 |[X]| Q2]]SF ev2

lemma csp_Parallel_mono: 

  [| X = Y; 
            LET:fp1 df IN P1 <=F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 <=F 
      LET:fp2 df IN Q1 |[Y]| Q2

lemma csp_Parallel_cong: 

  [| X = Y; 
            LET:fp1 df IN P1 =F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 =F 
      LET:fp2 df IN Q1 |[Y]| Q2

lemma domSF_Hiding_mono: 

  [| X = Y; [[P]]SF ev1 ≤ [[Q]]SF ev2 |] ==> [[P -- X]]SF ev1 ≤ [[Q -- X]]SF ev2

lemma csp_Hiding_mono: 

  [| X = Y; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X <=F 
      LET:fp2 df IN Q -- Y

lemma csp_Hiding_cong: 

  [| X = Y; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X =F 
      LET:fp2 df IN Q -- Y

lemma domSF_Renaming_mono: 

  [| r1 = r2; [[P]]SF ev1 ≤ [[Q]]SF ev2 |]
  ==> [[P [[r1]]]]SF ev1 ≤ [[Q [[r2]]]]SF ev2

lemma csp_Renaming_mono: 

  [| r1 = r2; 
              LET:fp1 df IN P <=F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] <=F 
      LET:fp2 df IN Q [[r2]]

lemma csp_Renaming_cong: 

  [| r1 = r2; 
              LET:fp1 df IN P =F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] =F 
      LET:fp2 df IN Q [[r2]]

lemma domSF_Seq_compo_mono: 

  [| [[P1]]SF ev1 ≤ [[Q1]]SF ev2; [[P2]]SF ev1 ≤ [[Q2]]SF ev2 |]
  ==> [[P1 ;; P2]]SF ev1 ≤ [[Q1 ;; Q2]]SF ev2

lemma csp_Seq_compo_mono: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 <=F 
      LET:fp2 df IN Q1 ;; Q2

lemma csp_Seq_compo_cong: 

  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 =F 
      LET:fp2 df IN Q1 ;; Q2

lemma csp_Timeout_mono: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [> P2 <=F 
      LET:fp2 df IN Q1 [> Q2

lemma csp_Timeout_cong: 

  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [> P2 =F 
      LET:fp2 df IN Q1 [> Q2

lemmas csp_free_mono: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 <=F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 <=F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 <=F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 <=F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X <=F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P <=F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] <=F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 <=F 
      LET:fp2 df IN Q1 ;; Q2

lemmas csp_mono: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 <=F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 <=F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 <=F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 <=F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X <=F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P <=F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] <=F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 <=F 
      LET:fp2 df IN Q1 ;; Q2
  [| a = b; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P <=F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf <=F 
      LET:fp2 df IN ? :Y -> Qf
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf <=F 
      LET:fp2 df IN ! :Y .. Qf
  [| b1 = b2; 
              LET:fp1 df IN P1 <=F 
              LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN IF b1 THEN P1 ELSE P2 <=F 
      LET:fp2 df IN IF b2 THEN Q1 ELSE Q2

lemmas csp_free_cong: 

  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 =F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 =F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 =F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 =F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X =F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P =F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] =F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 =F 
      LET:fp2 df IN Q1 ;; Q2

lemmas csp_cong: 

  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 =F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 =F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 =F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 =F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X =F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P =F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] =F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 =F 
      LET:fp2 df IN Q1 ;; Q2
  [| a = b; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P =F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf =F 
      LET:fp2 df IN ? :Y -> Qf
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf =F 
      LET:fp2 df IN ! :Y .. Qf
  [| b1 = b2; 
              LET:fp1 df IN P1 =F 
              LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN IF b1 THEN P1 ELSE P2 =F 
      LET:fp2 df IN IF b2 THEN Q1 ELSE Q2

lemmas csp_free_decompo: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 <=F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 <=F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 <=F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 <=F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X <=F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P <=F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] <=F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 <=F 
      LET:fp2 df IN Q1 ;; Q2
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 =F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 =F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 =F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 =F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X =F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P =F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] =F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 =F 
      LET:fp2 df IN Q1 ;; Q2

lemmas csp_decompo: 

  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 <=F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 <=F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 <=F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 <=F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X <=F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P <=F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] <=F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 <=F 
      LET:fp2 df IN Q1 ;; Q2
  [| a = b; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P <=F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf <=F 
      LET:fp2 df IN ? :Y -> Qf
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf <=F 
      LET:fp2 df IN ! :Y .. Qf
  [| b1 = b2; 
              LET:fp1 df IN P1 <=F 
              LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN IF b1 THEN P1 ELSE P2 <=F 
      LET:fp2 df IN IF b2 THEN Q1 ELSE Q2
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 [+] P2 =F 
      LET:fp2 df IN Q1 [+] Q2
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |~| P2 =F 
      LET:fp2 df IN Q1 |~| Q2
  [| X = Y; 
            LET:fp1 df IN P1 =F 
            LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 |[X]| P2 =F 
      LET:fp2 df IN Q1 |[Y]| Q2
  [| X = Y; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P -- X =F 
      LET:fp2 df IN Q -- Y
  [| r1 = r2; 
              LET:fp1 df IN P =F 
              LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN P [[r1]] =F 
      LET:fp2 df IN Q [[r2]]
  [| 
     LET:fp1 df IN P1 =F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P1 ;; P2 =F 
      LET:fp2 df IN Q1 ;; Q2
  [| a = b; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P =F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf =F 
      LET:fp2 df IN ? :Y -> Qf
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf =F 
      LET:fp2 df IN ! :Y .. Qf
  [| b1 = b2; 
              LET:fp1 df IN P1 =F 
              LET:fp2 df IN Q1;
     
     LET:fp1 df IN P2 =F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN IF b1 THEN P1 ELSE P2 =F 
      LET:fp2 df IN IF b2 THEN Q1 ELSE Q2

lemmas csp_rm_head_mono: 

  [| a = b; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P <=F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf <=F 
      LET:fp2 df IN ? :Y -> Qf

lemmas csp_rm_head_cong: 

  [| a = b; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P =F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf =F 
      LET:fp2 df IN ? :Y -> Qf

lemmas csp_rm_head: 

  [| a = b; 
            LET:fp1 df IN P <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P <=F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf <=F 
      LET:fp2 df IN ? :Y -> Qf
  [| a = b; 
            LET:fp1 df IN P =F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN a -> P =F 
      LET:fp2 df IN b -> Q
  [| X = Y; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a =F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ? :X -> Pf =F 
      LET:fp2 df IN ? :Y -> Qf