Theory CSP_T_law_ref (Isabelle2008: June 2008)

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  March 2007  (modified)   |
            |                 August 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_law_ref
imports CSP_T_law_basic
begin

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

         1. rules for refinement

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

(*-------------------------------------------------------*
 |            refinement and equality                    |
 *-------------------------------------------------------*)

lemma cspT_ref_eq_iff: "(P <=T[M,M] Q) = (P =T[M,M] Q |~| P)"
apply (simp add: cspT_semantics)
apply (rule)

(* <= *)
 apply (rule order_antisym)
 apply (simp add: subdomT_iff)
 apply (simp add: in_traces)
 apply (simp add: subdomT_iff)
 apply (simp add: in_traces)

(* => *)
 apply (erule order_antisymE)
 apply (rule)
 apply (rotate_tac 1)
 apply (erule subdomTE_ALL)
 apply (drule_tac x="t" in spec)
 apply (simp add: in_traces)
done

(*-------------------------------------------------------*
 |             simp STOP [+]                             |
 *-------------------------------------------------------*)

lemma cspT_Ent_choice_left1_ref:"P [+] Q <=T[M,M] P"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
done

lemma cspT_Ent_choice_left2_ref:"P [+] Q <=T[M,M] Q"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
done

lemmas cspT_Ent_choice_left_ref =
       cspT_Ent_choice_left1_ref
       cspT_Ent_choice_left2_ref

(*-------------------------------------------------------*
 |              decompose Internal choice                |
 *-------------------------------------------------------*)

(*** or <= ***)                                         (* unsafe *)

lemma cspT_Int_choice_left1:
  "P1 <=T[M1,M2] Q ==> P1 |~| P2 <=T[M1,M2] Q"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
apply (force)
done

lemma cspT_Int_choice_left2:
  "P2 <=T[M1,M2] Q ==> P1 |~| P2 <=T[M1,M2] Q"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
by (simp add: cspT_Int_choice_left1)

(*** <= and ***)                                          (* safe *)

lemma cspT_Int_choice_right:
  "[| P <=T[M1,M2] Q1 ; P <=T[M1,M2] Q2 |]
      ==> P <=T[M1,M2] Q1 |~| Q2"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
apply (force)
done

(*-------------------------------------------------------*
 |        decompose Replicated internal choice           |
 *-------------------------------------------------------*)

(*** EX <= ***)                                           (* unsafe *)

lemma cspT_Rep_int_choice_sum_left:
  "(EX c. c:sumset C & Pf c <=T[M1,M2] Q)
      ==> !! :C .. Pf <=T[M1,M2] Q"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
apply (force)
done

lemma cspT_Rep_int_choice_sum_left_x:
  "[| c: sumset C ; Pf c <=T[M1,M2] Q |]
  ==> !! :C .. Pf <=T[M1,M2] Q"
by (rule cspT_Rep_int_choice_sum_left, fast)

lemma cspT_Rep_int_choice_nat_left:
  "(EX n. n:N & Pf n <=T[M1,M2] Q)
      ==> !nat :N .. Pf <=T[M1,M2] Q"
apply (simp add: Rep_int_choice_ss_def)
by (rule cspT_Rep_int_choice_sum_left, force)

lemma cspT_Rep_int_choice_nat_left_x:
  "[| n:N ; Pf n <=T[M1,M2] Q |]
  ==> !nat :N .. Pf <=T[M1,M2] Q"
by (rule cspT_Rep_int_choice_nat_left, fast)

lemma cspT_Rep_int_choice_set_left:
  "(EX X. X:Xs & Pf X <=T[M1,M2] Q)
      ==> !set :Xs .. Pf <=T[M1,M2] Q"
apply (simp add: Rep_int_choice_ss_def)
by (rule cspT_Rep_int_choice_sum_left, force)

lemma cspT_Rep_int_choice_set_left_x:
  "[| X:Xs ; Pf X <=T[M1,M2] Q |]
  ==> !set :Xs .. Pf <=T[M1,M2] Q"
by (rule cspT_Rep_int_choice_set_left, fast)

lemma cspT_Rep_int_choice_com_left:
  "(EX a. a:X & Pf a <=T[M1,M2] Q)
      ==> ! :X .. Pf <=T[M1,M2] Q"
apply (simp add: Rep_int_choice_com_def)
by (rule cspT_Rep_int_choice_set_left, force)

lemma cspT_Rep_int_choice_com_left_x:
  "[| a:X ; Pf a <=T[M1,M2] Q |]
  ==> ! :X .. Pf <=T[M1,M2] Q"
by (rule cspT_Rep_int_choice_com_left, fast)

lemma cspT_Rep_int_choice_f_left:
  "[| inj f ; (EX a. a:X & Pf a <=T[M1,M2] Q) |]
      ==> !<f> :X .. Pf <=T[M1,M2] Q"
apply (simp add: Rep_int_choice_f_def)
by (rule cspT_Rep_int_choice_com_left, force)

lemma cspT_Rep_int_choice_f_left_x:
  "[| inj f ; a:X ; Pf a <=T[M1,M2] Q |]
  ==> !<f> :X .. Pf <=T[M1,M2] Q"
by (rule cspT_Rep_int_choice_f_left, simp, fast)

lemmas cspT_Rep_int_choice_left = cspT_Rep_int_choice_sum_left
                                  cspT_Rep_int_choice_nat_left
                                  cspT_Rep_int_choice_set_left
                                  cspT_Rep_int_choice_com_left
                                  cspT_Rep_int_choice_f_left

lemmas cspT_Rep_int_choice_left_x = cspT_Rep_int_choice_sum_left_x
                                  cspT_Rep_int_choice_nat_left_x
                                  cspT_Rep_int_choice_set_left_x
                                  cspT_Rep_int_choice_com_left_x
                                  cspT_Rep_int_choice_f_left_x

(*** <= ALL ***)                                         (* safe *)

lemma cspT_Rep_int_choice_sum_right:
  "[| !!c. c:sumset C ==> P <=T[M1,M2] Qf c |]
               ==> P <=T[M1,M2] !! :C .. Qf"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
apply (force)
done

lemma cspT_Rep_int_choice_nat_right:
  "[| !!n. n:N ==> P <=T[M1,M2] Qf n |]
               ==> P <=T[M1,M2] !nat :N .. Qf"
apply (simp add: Rep_int_choice_ss_def)
by (rule cspT_Rep_int_choice_sum_right, force)

lemma cspT_Rep_int_choice_set_right:
  "[| !!X. X:Xs ==> P <=T[M1,M2] Qf X |]
               ==> P <=T[M1,M2] !set :Xs .. Qf"
apply (simp add: Rep_int_choice_ss_def)
by (rule cspT_Rep_int_choice_sum_right, force)

lemma cspT_Rep_int_choice_com_right:
  "[| !!a. a:X ==> P <=T[M1,M2] Qf a |]
               ==> P <=T[M1,M2] ! :X .. Qf"
apply (simp add: Rep_int_choice_com_def)
by (rule cspT_Rep_int_choice_set_right, force)

lemma cspT_Rep_int_choice_f_right:
  "[| inj f ; !!a. a:X ==> P <=T[M1,M2] Qf a |]
               ==> P <=T[M1,M2] !<f> :X .. Qf"
apply (simp add: Rep_int_choice_f_def)
by (rule cspT_Rep_int_choice_com_right, force)

lemmas cspT_Rep_int_choice_right 
     = cspT_Rep_int_choice_sum_right
       cspT_Rep_int_choice_nat_right
       cspT_Rep_int_choice_set_right
       cspT_Rep_int_choice_com_right
       cspT_Rep_int_choice_f_right

(* 1,2,3,f E *)

lemma cspT_Rep_int_choice_sum_rightE:
  "[| P <=T[M1,M2] !! :C .. Qf ;
      ALL c:sumset C. P <=T[M1,M2] Qf c ==> R
   |] ==> R"
apply (simp add: cspT_semantics)
apply (simp add: subdomT_iff)
apply (simp add: in_traces)
apply (force)
done

lemma cspT_Rep_int_choice_nat_rightE:
  "[| P <=T[M1,M2] !nat :N .. Qf ;
      ALL n:N. P <=T[M1,M2] Qf n ==> R
   |] ==> R"
apply (simp add: Rep_int_choice_ss_def)
by (erule cspT_Rep_int_choice_sum_rightE, force)

lemma cspT_Rep_int_choice_set_rightE:
  "[| P <=T[M1,M2] !set :Xs .. Qf ;
      ALL X:Xs. P <=T[M1,M2] Qf X ==> R
   |] ==> R"
apply (simp add: Rep_int_choice_ss_def)
by (erule cspT_Rep_int_choice_sum_rightE, force)

lemma cspT_Rep_int_choice_com_rightE:
  "[| P <=T[M1,M2] ! :X .. Qf ;
      ALL a:X. P <=T[M1,M2] Qf a ==> R
   |] ==> R"
apply (simp add: Rep_int_choice_com_def)
by (erule cspT_Rep_int_choice_set_rightE, force)

lemma cspT_Rep_int_choice_f_rightE:
  "[| P <=T[M1,M2] !<f> :X .. Qf ; inj f ;
      [| ALL a:X. P <=T[M1,M2] Qf a |] ==> R
   |] ==> R"
apply (simp add: Rep_int_choice_f_def)
by (erule cspT_Rep_int_choice_com_rightE, force)

lemmas cspT_Rep_int_choice_rightE =
       cspT_Rep_int_choice_sum_rightE
       cspT_Rep_int_choice_nat_rightE
       cspT_Rep_int_choice_set_rightE
       cspT_Rep_int_choice_com_rightE
       cspT_Rep_int_choice_f_rightE

(*-------------------------------------------------------*
 |             decomposition with subset                 |
 *-------------------------------------------------------*)

(*** Rep_int_choice ***)                                        (* unsafe *)

lemma cspT_Rep_int_choice_sum_subset:
  "[| sumset C2 <= sumset C1  ; !!c. c:sumset C2 ==> Pf c <=T[M1,M2] Qf c |]
                    ==> !! :C1 .. Pf <=T[M1,M2] !! :C2 .. Qf"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
apply (force)
done

lemma cspT_Rep_int_choice_nat_subset:
  "[| N2 <= N1  ; !!n. n:N2 ==> Pf n <=T[M1,M2] Qf n |]
                    ==> !nat :N1 .. Pf <=T[M1,M2] !nat :N2 .. Qf"
apply (simp add: Rep_int_choice_ss_def)
by (rule cspT_Rep_int_choice_sum_subset, auto)

lemma cspT_Rep_int_choice_set_subset:
  "[| Ys <= Xs  ; !!X. X:Ys ==> Pf X <=T[M1,M2] Qf X |]
                    ==> !set :Xs .. Pf <=T[M1,M2] !set :Ys .. Qf"
apply (simp add: Rep_int_choice_ss_def)
by (rule cspT_Rep_int_choice_sum_subset, auto)

lemma cspT_Rep_int_choice_com_subset:
  "[| Y <= X  ; !!a. a:Y ==> Pf a <=T[M1,M2] Qf a |]
                    ==> ! :X .. Pf <=T[M1,M2] ! :Y .. Qf"
apply (simp add: Rep_int_choice_com_def)
by (rule cspT_Rep_int_choice_set_subset, auto)

lemma cspT_Rep_int_choice_f_subset:
  "[| inj f ; Y <= X  ; !!a. a:Y ==> Pf a <=T[M1,M2] Qf a |]
                    ==> !<f> :X .. Pf <=T[M1,M2] !<f> :Y .. Qf"
apply (simp add: Rep_int_choice_f_def)
by (rule cspT_Rep_int_choice_com_subset, auto)

lemmas cspT_Rep_int_choice_subset 
     = cspT_Rep_int_choice_sum_subset
       cspT_Rep_int_choice_nat_subset
       cspT_Rep_int_choice_set_subset
       cspT_Rep_int_choice_com_subset
       cspT_Rep_int_choice_f_subset

(*** ! x:X .. and ? -> ***)

lemma cspT_Int_Ext_pre_choice_subset:
  "[| Y ~={} ; Y <= X ; !!a. a:Y ==> Pf a <=T[M1,M2] Qf a |]
        ==> ! x:X .. (x -> Pf x) <=T[M1,M2]
            ? :Y -> Qf"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
apply (force)
done

lemmas cspT_decompo_subset = cspT_Rep_int_choice_subset
                             cspT_Int_Ext_pre_choice_subset

(*-------------------------------------------------------*
 |               decompose external choice               |
 *-------------------------------------------------------*)

lemma cspT_Ext_choice_right:
  "[| P <=T[M1,M2] Q1 ;
      P <=T[M1,M2] Q2 |]
      ==> P <=T[M1,M2] Q1 [+] Q2"
apply (simp add: cspT_semantics)
apply (rule, simp add: in_traces)
apply (force)
done

end

lemma cspT_ref_eq_iff:

  (P <=T[M,M] Q) = (P =T[M,M] Q |~| P)

lemma cspT_Ent_choice_left1_ref:

  P [+] Q <=T[M,M] P

lemma cspT_Ent_choice_left2_ref:

  P [+] Q <=T[M,M] Q

lemma cspT_Ent_choice_left_ref:

  P [+] Q <=T[M,M] P

  P [+] Q <=T[M,M] Q

lemma cspT_Int_choice_left1:

  P1.0 <=T[M1.0,M2.0] Q ==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q

lemma cspT_Int_choice_left2:

  P2.0 <=T[M1.0,M2.0] Q ==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q

lemma cspT_Int_choice_right:

  [| P <=T[M1.0,M2.0] Q1.0; P <=T[M1.0,M2.0] Q2.0 |]
  ==> P <=T[M1.0,M2.0] Q1.0 |~| Q2.0

lemma cspT_Rep_int_choice_sum_left:

  ∃c. c ∈ sumset C ∧ Pf c <=T[M1.0,M2.0] Q ==> !! :C .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_sum_left_x:

  [| c ∈ sumset C; Pf c <=T[M1.0,M2.0] Q |] ==> !! :C .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_nat_left:

  ∃n. n ∈ N ∧ Pf n <=T[M1.0,M2.0] Q ==> !nat :N .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_nat_left_x:

  [| n ∈ N; Pf n <=T[M1.0,M2.0] Q |] ==> !nat :N .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_set_left:

  ∃X. X ∈ Xs ∧ Pf X <=T[M1.0,M2.0] Q ==> !set :Xs .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_set_left_x:

  [| X ∈ Xs; Pf X <=T[M1.0,M2.0] Q |] ==> !set :Xs .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_com_left:

  ∃a. a ∈ X ∧ Pf a <=T[M1.0,M2.0] Q ==> ! :X .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_com_left_x:

  [| a ∈ X; Pf a <=T[M1.0,M2.0] Q |] ==> ! :X .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_f_left:

  [| inj f; ∃a. a ∈ X ∧ Pf a <=T[M1.0,M2.0] Q |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_f_left_x:

  [| inj f; a ∈ X; Pf a <=T[M1.0,M2.0] Q |] ==> !<f> :X .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_left:

  ∃c. c ∈ sumset C ∧ Pf c <=T[M1.0,M2.0] Q ==> !! :C .. Pf <=T[M1.0,M2.0] Q

  ∃n. n ∈ N ∧ Pf n <=T[M1.0,M2.0] Q ==> !nat :N .. Pf <=T[M1.0,M2.0] Q

  ∃X. X ∈ Xs ∧ Pf X <=T[M1.0,M2.0] Q ==> !set :Xs .. Pf <=T[M1.0,M2.0] Q

  ∃a. a ∈ X ∧ Pf a <=T[M1.0,M2.0] Q ==> ! :X .. Pf <=T[M1.0,M2.0] Q

  [| inj f; ∃a. a ∈ X ∧ Pf a <=T[M1.0,M2.0] Q |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_left_x:

  [| c ∈ sumset C; Pf c <=T[M1.0,M2.0] Q |] ==> !! :C .. Pf <=T[M1.0,M2.0] Q

  [| n ∈ N; Pf n <=T[M1.0,M2.0] Q |] ==> !nat :N .. Pf <=T[M1.0,M2.0] Q

  [| X ∈ Xs; Pf X <=T[M1.0,M2.0] Q |] ==> !set :Xs .. Pf <=T[M1.0,M2.0] Q

  [| a ∈ X; Pf a <=T[M1.0,M2.0] Q |] ==> ! :X .. Pf <=T[M1.0,M2.0] Q

  [| inj f; a ∈ X; Pf a <=T[M1.0,M2.0] Q |] ==> !<f> :X .. Pf <=T[M1.0,M2.0] Q

lemma cspT_Rep_int_choice_sum_right:

  (!!c. c ∈ sumset C ==> P <=T[M1.0,M2.0] Qf c) ==> P <=T[M1.0,M2.0] !! :C .. Qf

lemma cspT_Rep_int_choice_nat_right:

  (!!n. n ∈ N ==> P <=T[M1.0,M2.0] Qf n) ==> P <=T[M1.0,M2.0] !nat :N .. Qf

lemma cspT_Rep_int_choice_set_right:

  (!!X. X ∈ Xs ==> P <=T[M1.0,M2.0] Qf X) ==> P <=T[M1.0,M2.0] !set :Xs .. Qf

lemma cspT_Rep_int_choice_com_right:

  (!!a. a ∈ X ==> P <=T[M1.0,M2.0] Qf a) ==> P <=T[M1.0,M2.0] ! :X .. Qf

lemma cspT_Rep_int_choice_f_right:

  [| inj f; !!a. a ∈ X ==> P <=T[M1.0,M2.0] Qf a |]
  ==> P <=T[M1.0,M2.0] !<f> :X .. Qf

lemma cspT_Rep_int_choice_right:

  (!!c. c ∈ sumset C ==> P <=T[M1.0,M2.0] Qf c) ==> P <=T[M1.0,M2.0] !! :C .. Qf

  (!!n. n ∈ N ==> P <=T[M1.0,M2.0] Qf n) ==> P <=T[M1.0,M2.0] !nat :N .. Qf

  (!!X. X ∈ Xs ==> P <=T[M1.0,M2.0] Qf X) ==> P <=T[M1.0,M2.0] !set :Xs .. Qf

  (!!a. a ∈ X ==> P <=T[M1.0,M2.0] Qf a) ==> P <=T[M1.0,M2.0] ! :X .. Qf

  [| inj f; !!a. a ∈ X ==> P <=T[M1.0,M2.0] Qf a |]
  ==> P <=T[M1.0,M2.0] !<f> :X .. Qf

lemma cspT_Rep_int_choice_sum_rightE:

  [| P <=T[M1.0,M2.0] !! :C .. Qf; ∀c∈sumset C. P <=T[M1.0,M2.0] Qf c ==> R |]
  ==> R

lemma cspT_Rep_int_choice_nat_rightE:

  [| P <=T[M1.0,M2.0] !nat :N .. Qf; ∀n∈N. P <=T[M1.0,M2.0] Qf n ==> R |] ==> R

lemma cspT_Rep_int_choice_set_rightE:

  [| P <=T[M1.0,M2.0] !set :Xs .. Qf; ∀X∈Xs. P <=T[M1.0,M2.0] Qf X ==> R |] ==> R

lemma cspT_Rep_int_choice_com_rightE:

  [| P <=T[M1.0,M2.0] ! :X .. Qf; ∀a∈X. P <=T[M1.0,M2.0] Qf a ==> R |] ==> R

lemma cspT_Rep_int_choice_f_rightE:

  [| P <=T[M1.0,M2.0] !<f> :X .. Qf; inj f; ∀a∈X. P <=T[M1.0,M2.0] Qf a ==> R |]
  ==> R

lemma cspT_Rep_int_choice_rightE:

  [| P <=T[M1.0,M2.0] !! :C .. Qf; ∀c∈sumset C. P <=T[M1.0,M2.0] Qf c ==> R |]
  ==> R

  [| P <=T[M1.0,M2.0] !nat :N .. Qf; ∀n∈N. P <=T[M1.0,M2.0] Qf n ==> R |] ==> R

  [| P <=T[M1.0,M2.0] !set :Xs .. Qf; ∀X∈Xs. P <=T[M1.0,M2.0] Qf X ==> R |] ==> R

  [| P <=T[M1.0,M2.0] ! :X .. Qf; ∀a∈X. P <=T[M1.0,M2.0] Qf a ==> R |] ==> R

  [| P <=T[M1.0,M2.0] !<f> :X .. Qf; inj f; ∀a∈X. P <=T[M1.0,M2.0] Qf a ==> R |]
  ==> R

lemma cspT_Rep_int_choice_sum_subset:

  [| sumset C2.0 ⊆ sumset C1.0;
     !!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf

lemma cspT_Rep_int_choice_nat_subset:

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf

lemma cspT_Rep_int_choice_set_subset:

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf

lemma cspT_Rep_int_choice_com_subset:

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf

lemma cspT_Rep_int_choice_f_subset:

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf

lemma cspT_Rep_int_choice_subset:

  [| sumset C2.0 ⊆ sumset C1.0;
     !!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf

lemma cspT_Int_Ext_pre_choice_subset:

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf

lemma cspT_decompo_subset:

  [| sumset C2.0 ⊆ sumset C1.0;
     !!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
  ==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
  ==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
  ==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
  ==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf

lemma cspT_Ext_choice_right:

  [| P <=T[M1.0,M2.0] Q1.0; P <=T[M1.0,M2.0] Q2.0 |]
  ==> P <=T[M1.0,M2.0] Q1.0 [+] Q2.0