Theory CSP_F_law_ref

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F

theory CSP_F_law_ref
imports CSP_F_law_basic CSP_T_law_ref
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_ref = CSP_F_law_basic + CSP_T_law_ref:

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

         1. rules for refinement

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

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

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

lemma cspF_Int_choice_left1:
  "P1 <=F Q ==> P1 |~| P2 <=F Q"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_left1)
apply (rule, simp add: in_failures)
apply (force)
done

lemma cspF_Int_choice_left2:
  "P2 <=F Q ==> P1 |~| P2 <=F Q"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
by (simp add: cspF_Int_choice_left1)

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

lemma cspF_Int_choice_right:
  "[| P <=F Q1 ; P <=F Q2 |]
      ==> P <=F Q1 |~| Q2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_right)
apply (rule, simp add: in_failures)
apply (force)
done

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

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

lemma cspF_Rep_int_choice0_left:
  "(EX c. c:C & Pf c <=F Q)
      ==> !! :C .. Pf <=F Q"
apply (simp add: cspF_cspT_semantics)
apply (rule conjI)

apply (rule cspT_Rep_int_choice0_left)
apply (fast)

apply (rule, simp add: in_failures)
apply (force)
done

lemma cspF_Rep_int_choice0_left_x:
  "[| x:C ; Pf x <=F Q |]
  ==> !! :C .. Pf <=F Q"
apply (rule cspF_Rep_int_choice0_left)
by (fast)

lemma cspF_Rep_int_choice_fun_left:
  "[| inj f ; (EX a. a:X & Pf a <=F Q) |]
      ==> !!<f> :X .. Pf <=F Q"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice0_left)
apply (force)
done

lemma cspF_Rep_int_choice_fun_left_x:
  "[| inj f ; x:X ; Pf x <=F Q |]
  ==> !!<f> :X .. Pf <=F Q"
apply (rule cspF_Rep_int_choice_fun_left)
by (auto)

(* com, set, nat *)

lemma cspF_Rep_int_choice2_left:
  "(EX X. X:Xs & Pf X <=F Q)
      ==> !set :Xs .. Pf <=F Q"
by (simp add: cspF_Rep_int_choice_fun_left)

lemma cspF_Rep_int_choice3_left:
  "(EX n. n:N & Pf n <=F Q)
      ==> !nat :N .. Pf <=F Q"
by (simp add: cspF_Rep_int_choice_fun_left)

lemma cspF_Rep_int_choice1_left:
  "(EX a. a:X & Pf a <=F Q)
      ==> ! :X .. Pf <=F Q"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice2_left)
apply (elim conjE exE)
apply (rule_tac x="{a}" in exI)
apply (simp)
done

lemma cspF_Rep_int_choice_f_left:
  "[| inj f ; (EX a. a:X & Pf a <=F Q) |]
      ==> !<f> :X .. Pf <=F Q"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_Rep_int_choice1_left)
apply (erule exE)
apply (rule_tac x="f a" in exI)
apply (simp)
done

(* x *)

lemma cspF_Rep_int_choice2_left_x:
  "[| x:Xs ; Pf x <=F Q |]
  ==> !set :Xs .. Pf <=F Q"
by (simp add: cspF_Rep_int_choice_fun_left_x)

lemma cspF_Rep_int_choice3_left_x:
  "[| x:N ; Pf x <=F Q |]
  ==> !nat :N .. Pf <=F Q"
by (simp add: cspF_Rep_int_choice_fun_left_x)

lemma cspF_Rep_int_choice1_left_x:
  "[| x:X ; Pf x <=F Q |]
  ==> ! :X .. Pf <=F Q"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice2_left_x[of "{x}"])
apply (simp)
apply (simp)
done

lemma cspF_Rep_int_choice_f_left_x:
  "[| inj f ; x:X ; Pf x <=F Q |]
      ==> !<f> :X .. Pf <=F Q"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_Rep_int_choice1_left)
apply (rule_tac x="f x" in exI)
apply (simp)
done

lemmas cspF_Rep_int_choice_left = cspF_Rep_int_choice0_left
                                  cspF_Rep_int_choice1_left
                                  cspF_Rep_int_choice2_left
                                  cspF_Rep_int_choice3_left
                                  cspF_Rep_int_choice_f_left

lemmas cspF_Rep_int_choice_left_x = cspF_Rep_int_choice0_left_x
                                    cspF_Rep_int_choice1_left_x
                                    cspF_Rep_int_choice2_left_x
                                    cspF_Rep_int_choice3_left_x
                                    cspF_Rep_int_choice_f_left_x

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

lemma cspF_Rep_int_choice0_right:
  "[| !!c. c:C ==> P <=F Qf c |]
               ==> P <=F !! :C .. Qf"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice0_right)
apply (rule, simp add: in_failures)
apply (force)
done

lemma cspF_Rep_int_choice0_rightE:
  "[| P <=F !! :C .. Qf ;
      ALL c:C. P <=F Qf c ==> R
   |] ==> R"
apply (simp add: cspF_cspT_semantics)
apply (elim conjE exE)
apply (erule cspT_Rep_int_choice0_rightE)

apply (simp add: subsetF_iff)
apply (simp add: in_failures)
apply (force)
done

(* f *)

lemma cspF_Rep_int_choice_fun_right:
  "[| inj f ; !!a. a:X ==> P <=F Qf a |]
               ==> P <=F !!<f> :X .. Qf"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice0_right)
apply (force)
done

lemma cspF_Rep_int_choice_fun_rightE:
  "[| P <=F !!<f> :X .. Qf ; inj f ;
      ALL a:X. P <=F Qf a ==> R
   |] ==> R"
apply (simp add: Rep_int_choice_fun_def)
apply (erule cspF_Rep_int_choice0_rightE)
apply (force)
done

(* 1,2,3,f *)

lemma cspF_Rep_int_choice2_right:
  "[| !!X. X:Xs ==> P <=F Qf X |]
               ==> P <=F !set :Xs .. Qf"
by (simp add: cspF_Rep_int_choice_fun_right)

lemma cspF_Rep_int_choice3_right:
  "[| !!n. n:N ==> P <=F Qf n |]
               ==> P <=F !nat :N .. Qf"
by (simp add: cspF_Rep_int_choice_fun_right)

lemma cspF_Rep_int_choice1_right:
  "[| !!a. a:X ==> P <=F Qf a |]
               ==> P <=F ! :X .. Qf"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice2_right)
apply (force)
done

lemma cspF_Rep_int_choice_f_right:
  "[| inj f ; !!a. a:X ==> P <=F Qf a |]
               ==> P <=F !<f> :X .. Qf"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_Rep_int_choice1_right)
apply (simp add: image_iff)
apply (elim bexE)
apply (simp)
done

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

lemma cspF_Rep_int_choice2_rightE:
  "[| P <=F !set :Xs .. Qf ;
      ALL X:Xs. P <=F Qf X ==> R
   |] ==> R"
apply (erule cspF_Rep_int_choice_fun_rightE)
by (auto)

lemma cspF_Rep_int_choice3_rightE:
  "[| P <=F !nat :N .. Qf ;
      ALL n:N. P <=F Qf n ==> R
   |] ==> R"
apply (erule cspF_Rep_int_choice_fun_rightE)
by (auto)

lemma cspF_Rep_int_choice1_rightE:
  "[| P <=F ! :X .. Qf ;
      ALL a:X. P <=F Qf a ==> R
   |] ==> R"
apply (simp add: Rep_int_choice_com_def)
apply (erule cspF_Rep_int_choice2_rightE)
apply (force)
done

lemma cspF_Rep_int_choice_f_rightE:
  "[| P <=F !<f> :X .. Qf ; inj f ;
      [| ALL a:X. P <=F Qf a |] ==> R
   |] ==> R"
apply (simp add: Rep_int_choice_f_def)
apply (erule cspF_Rep_int_choice1_rightE)
apply (simp add: image_iff)
done

lemmas cspF_Rep_int_choice_right 
     = cspF_Rep_int_choice0_right
       cspF_Rep_int_choice1_right
       cspF_Rep_int_choice2_right
       cspF_Rep_int_choice3_right
       cspF_Rep_int_choice_f_right

lemmas cspF_Rep_int_choice_rightE
     = cspF_Rep_int_choice0_rightE
       cspF_Rep_int_choice1_rightE
       cspF_Rep_int_choice2_rightE
       cspF_Rep_int_choice3_rightE
       cspF_Rep_int_choice_f_rightE

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

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

lemma cspF_Rep_int_choice0_subset:
  "[| C2 <= C1  ; !!c. c:C2 ==> Pf c <=F Qf c |]
                    ==> !! :C1 .. Pf <=F !! :C2 .. Qf"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice0_subset)
apply (rule, simp add: in_failures)
apply (force)
done

lemma cspF_Rep_int_choice_fun_subset:
  "[| inj f ; Y <= X  ; !!a. a:Y ==> Pf a <=F Qf a |]
                    ==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice0_subset)
apply (force)
apply (force)
done

lemma cspF_Rep_int_choice2_subset:
  "[| Ys <= Xs  ; !!X. X:Ys ==> Pf X <=F Qf X |]
                    ==> !set :Xs .. Pf <=F !set :Ys .. Qf"
by (simp add: cspF_Rep_int_choice_fun_subset)

lemma cspF_Rep_int_choice3_subset:
  "[| N2 <= N1  ; !!n. n:N2 ==> Pf n <=F Qf n |]
                  ==> !nat :N1 .. Pf <=F !nat :N2 .. Qf"
by (simp add: cspF_Rep_int_choice_fun_subset)

lemma cspF_Rep_int_choice1_subset:
  "[| Y <= X  ; !!a. a:Y ==> Pf a <=F Qf a |]
                    ==> ! :X .. Pf <=F ! :Y .. Qf"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice2_subset)
apply (auto)
done

lemma cspF_Rep_int_choice_f_subset:
  "[| inj f ; Y <= X  ; !!a. a:Y ==> Pf a <=F Qf a |]
                    ==> !<f> :X .. Pf <=F !<f> :Y .. Qf"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_Rep_int_choice1_subset)
apply (auto simp add: image_def)
done

lemmas cspF_Rep_int_choice_subset 
     = cspF_Rep_int_choice0_subset
       cspF_Rep_int_choice1_subset
       cspF_Rep_int_choice2_subset
       cspF_Rep_int_choice3_subset
       cspF_Rep_int_choice_f_subset

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

lemma cspF_Int_Ext_pre_choice_subset:
  "[| Y ~={} ; Y <= X ; !!a. a:Y ==> Pf a <=F Qf a |]
        ==> ! x:X .. (x -> Pf x) <=F
            ? :Y -> Qf"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_Ext_pre_choice_subset)
apply (rule, simp add: in_failures)
apply (force)
done

lemmas cspF_decompo_subset = cspF_Rep_int_choice_subset
                             cspF_Int_Ext_pre_choice_subset

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

lemma cspF_Ext_choice_right:
  "[| P <=F Q1 ;
      P <=F Q2 |]
      ==> P <=F Q1 [+] Q2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_right)
apply (rule)

 apply (simp add: in_failures)
 apply (elim disjE conjE exE, simp)
 apply (force, force, force)
 apply (simp_all)

 apply (subgoal_tac "(<>, X) :f failures(Q1)")
 apply (force)
 apply (rule proc_F2_F4)
 apply (simp_all)
 apply (rule proc_F2_F4)
 apply (simp_all)
 apply (simp add: cspT_semantics)
 apply (auto)
done

end

lemma cspF_Int_choice_left1: 

  P1.0 <=F Q ==> P1.0 |~| P2.0 <=F Q

lemma cspF_Int_choice_left2: 

  P2.0 <=F Q ==> P1.0 |~| P2.0 <=F Q

lemma cspF_Int_choice_right: 

  [| P <=F Q1.0; P <=F Q2.0 |] ==> P <=F Q1.0 |~| Q2.0

lemma cspF_Rep_int_choice0_left: 

  ∃c. c ∈ C ∧ Pf c <=F Q ==> !! :C .. Pf <=F Q

lemma cspF_Rep_int_choice0_left_x: 

  [| x ∈ C; Pf x <=F Q |] ==> !! :C .. Pf <=F Q

lemma cspF_Rep_int_choice_fun_left: 

  [| inj f; ∃a. a ∈ X ∧ Pf a <=F Q |] ==> !!<f> :X .. Pf <=F Q

lemma cspF_Rep_int_choice_fun_left_x: 

  [| inj f; x ∈ X; Pf x <=F Q |] ==> !!<f> :X .. Pf <=F Q

lemma cspF_Rep_int_choice2_left: 

  ∃X. X ∈ Xs ∧ Pf X <=F Q ==> !set :Xs .. Pf <=F Q

lemma cspF_Rep_int_choice3_left: 

  ∃n. n ∈ N ∧ Pf n <=F Q ==> !nat :N .. Pf <=F Q

lemma cspF_Rep_int_choice1_left: 

  ∃a. a ∈ X ∧ Pf a <=F Q ==> ! :X .. Pf <=F Q

lemma cspF_Rep_int_choice_f_left: 

  [| inj f; ∃a. a ∈ X ∧ Pf a <=F Q |] ==> !<f> :X .. Pf <=F Q

lemma cspF_Rep_int_choice2_left_x: 

  [| x ∈ Xs; Pf x <=F Q |] ==> !set :Xs .. Pf <=F Q

lemma cspF_Rep_int_choice3_left_x: 

  [| x ∈ N; Pf x <=F Q |] ==> !nat :N .. Pf <=F Q

lemma cspF_Rep_int_choice1_left_x: 

  [| x ∈ X; Pf x <=F Q |] ==> ! :X .. Pf <=F Q

lemma cspF_Rep_int_choice_f_left_x: 

  [| inj f; x ∈ X; Pf x <=F Q |] ==> !<f> :X .. Pf <=F Q

lemmas cspF_Rep_int_choice_left: 

  ∃c. c ∈ C ∧ Pf c <=F Q ==> !! :C .. Pf <=F Q
  ∃a. a ∈ X ∧ Pf a <=F Q ==> ! :X .. Pf <=F Q
  ∃X. X ∈ Xs ∧ Pf X <=F Q ==> !set :Xs .. Pf <=F Q
  ∃n. n ∈ N ∧ Pf n <=F Q ==> !nat :N .. Pf <=F Q
  [| inj f; ∃a. a ∈ X ∧ Pf a <=F Q |] ==> !<f> :X .. Pf <=F Q

lemmas cspF_Rep_int_choice_left: 

  ∃c. c ∈ C ∧ Pf c <=F Q ==> !! :C .. Pf <=F Q
  ∃a. a ∈ X ∧ Pf a <=F Q ==> ! :X .. Pf <=F Q
  ∃X. X ∈ Xs ∧ Pf X <=F Q ==> !set :Xs .. Pf <=F Q
  ∃n. n ∈ N ∧ Pf n <=F Q ==> !nat :N .. Pf <=F Q
  [| inj f; ∃a. a ∈ X ∧ Pf a <=F Q |] ==> !<f> :X .. Pf <=F Q

lemmas cspF_Rep_int_choice_left_x: 

  [| x ∈ C; Pf x <=F Q |] ==> !! :C .. Pf <=F Q
  [| x ∈ X; Pf x <=F Q |] ==> ! :X .. Pf <=F Q
  [| x ∈ Xs; Pf x <=F Q |] ==> !set :Xs .. Pf <=F Q
  [| x ∈ N; Pf x <=F Q |] ==> !nat :N .. Pf <=F Q
  [| inj f; x ∈ X; Pf x <=F Q |] ==> !<f> :X .. Pf <=F Q

lemmas cspF_Rep_int_choice_left_x: 

  [| x ∈ C; Pf x <=F Q |] ==> !! :C .. Pf <=F Q
  [| x ∈ X; Pf x <=F Q |] ==> ! :X .. Pf <=F Q
  [| x ∈ Xs; Pf x <=F Q |] ==> !set :Xs .. Pf <=F Q
  [| x ∈ N; Pf x <=F Q |] ==> !nat :N .. Pf <=F Q
  [| inj f; x ∈ X; Pf x <=F Q |] ==> !<f> :X .. Pf <=F Q

lemma cspF_Rep_int_choice0_right: 

  (!!c. c ∈ C ==> P <=F Qf c) ==> P <=F !! :C .. Qf

lemma cspF_Rep_int_choice0_rightE: 

  [| P <=F !! :C .. Qf; ∀c∈C. P <=F Qf c ==> R |] ==> R

lemma cspF_Rep_int_choice_fun_right: 

  [| inj f; !!a. a ∈ X ==> P <=F Qf a |] ==> P <=F !!<f> :X .. Qf

lemma cspF_Rep_int_choice_fun_rightE: 

  [| P <=F !!<f> :X .. Qf; inj f; ∀a∈X. P <=F Qf a ==> R |] ==> R

lemma cspF_Rep_int_choice2_right: 

  (!!X. X ∈ Xs ==> P <=F Qf X) ==> P <=F !set :Xs .. Qf

lemma cspF_Rep_int_choice3_right: 

  (!!n. n ∈ N ==> P <=F Qf n) ==> P <=F !nat :N .. Qf

lemma cspF_Rep_int_choice1_right: 

  (!!a. a ∈ X ==> P <=F Qf a) ==> P <=F ! :X .. Qf

lemma cspF_Rep_int_choice_f_right: 

  [| inj f; !!a. a ∈ X ==> P <=F Qf a |] ==> P <=F !<f> :X .. Qf

lemma cspF_Rep_int_choice2_rightE: 

  [| P <=F !set :Xs .. Qf; ∀X∈Xs. P <=F Qf X ==> R |] ==> R

lemma cspF_Rep_int_choice3_rightE: 

  [| P <=F !nat :N .. Qf; ∀n∈N. P <=F Qf n ==> R |] ==> R

lemma cspF_Rep_int_choice1_rightE: 

  [| P <=F ! :X .. Qf; ∀a∈X. P <=F Qf a ==> R |] ==> R

lemma cspF_Rep_int_choice_f_rightE: 

  [| P <=F !<f> :X .. Qf; inj f; ∀a∈X. P <=F Qf a ==> R |] ==> R

lemmas cspF_Rep_int_choice_right: 

  (!!c. c ∈ C ==> P <=F Qf c) ==> P <=F !! :C .. Qf
  (!!a. a ∈ X ==> P <=F Qf a) ==> P <=F ! :X .. Qf
  (!!X. X ∈ Xs ==> P <=F Qf X) ==> P <=F !set :Xs .. Qf
  (!!n. n ∈ N ==> P <=F Qf n) ==> P <=F !nat :N .. Qf
  [| inj f; !!a. a ∈ X ==> P <=F Qf a |] ==> P <=F !<f> :X .. Qf

lemmas cspF_Rep_int_choice_right: 

  (!!c. c ∈ C ==> P <=F Qf c) ==> P <=F !! :C .. Qf
  (!!a. a ∈ X ==> P <=F Qf a) ==> P <=F ! :X .. Qf
  (!!X. X ∈ Xs ==> P <=F Qf X) ==> P <=F !set :Xs .. Qf
  (!!n. n ∈ N ==> P <=F Qf n) ==> P <=F !nat :N .. Qf
  [| inj f; !!a. a ∈ X ==> P <=F Qf a |] ==> P <=F !<f> :X .. Qf

lemmas cspF_Rep_int_choice_rightE: 

  [| P <=F !! :C .. Qf; ∀c∈C. P <=F Qf c ==> R |] ==> R
  [| P <=F ! :X .. Qf; ∀a∈X. P <=F Qf a ==> R |] ==> R
  [| P <=F !set :Xs .. Qf; ∀X∈Xs. P <=F Qf X ==> R |] ==> R
  [| P <=F !nat :N .. Qf; ∀n∈N. P <=F Qf n ==> R |] ==> R
  [| P <=F !<f> :X .. Qf; inj f; ∀a∈X. P <=F Qf a ==> R |] ==> R

lemmas cspF_Rep_int_choice_rightE: 

  [| P <=F !! :C .. Qf; ∀c∈C. P <=F Qf c ==> R |] ==> R
  [| P <=F ! :X .. Qf; ∀a∈X. P <=F Qf a ==> R |] ==> R
  [| P <=F !set :Xs .. Qf; ∀X∈Xs. P <=F Qf X ==> R |] ==> R
  [| P <=F !nat :N .. Qf; ∀n∈N. P <=F Qf n ==> R |] ==> R
  [| P <=F !<f> :X .. Qf; inj f; ∀a∈X. P <=F Qf a ==> R |] ==> R

lemma cspF_Rep_int_choice0_subset: 

  [| C2.0 ⊆ C1.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |]
  ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf

lemma cspF_Rep_int_choice_fun_subset: 

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> !!<f> :X .. Pf <=F !!<f> :Y .. Qf

lemma cspF_Rep_int_choice2_subset: 

  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F Qf X |]
  ==> !set :Xs .. Pf <=F !set :Ys .. Qf

lemma cspF_Rep_int_choice3_subset: 

  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |]
  ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf

lemma cspF_Rep_int_choice1_subset: 

  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf

lemma cspF_Rep_int_choice_f_subset: 

  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> !<f> :X .. Pf <=F !<f> :Y .. Qf

lemmas cspF_Rep_int_choice_subset: 

  [| C2.0 ⊆ C1.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |]
  ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F Qf X |]
  ==> !set :Xs .. Pf <=F !set :Ys .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |]
  ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> !<f> :X .. Pf <=F !<f> :Y .. Qf

lemmas cspF_Rep_int_choice_subset: 

  [| C2.0 ⊆ C1.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |]
  ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F Qf X |]
  ==> !set :Xs .. Pf <=F !set :Ys .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |]
  ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> !<f> :X .. Pf <=F !<f> :Y .. Qf

lemma cspF_Int_Ext_pre_choice_subset: 

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> ! x:X .. x -> Pf x <=F ? :Y -> Qf

lemmas cspF_decompo_subset: 

  [| C2.0 ⊆ C1.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |]
  ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F Qf X |]
  ==> !set :Xs .. Pf <=F !set :Ys .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |]
  ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> ! x:X .. x -> Pf x <=F ? :Y -> Qf

lemmas cspF_decompo_subset: 

  [| C2.0 ⊆ C1.0; !!c. c ∈ C2.0 ==> Pf c <=F Qf c |]
  ==> !! :C1.0 .. Pf <=F !! :C2.0 .. Qf
  [| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |] ==> ! :X .. Pf <=F ! :Y .. Qf
  [| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=F Qf X |]
  ==> !set :Xs .. Pf <=F !set :Ys .. Qf
  [| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=F Qf n |]
  ==> !nat :N1.0 .. Pf <=F !nat :N2.0 .. Qf
  [| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> !<f> :X .. Pf <=F !<f> :Y .. Qf
  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=F Qf a |]
  ==> ! x:X .. x -> Pf x <=F ? :Y -> Qf

lemma cspF_Ext_choice_right: 

  [| P <=F Q1.0; P <=F Q2.0 |] ==> P <=F Q1.0 [+] Q2.0