Theory CSP_T_tactic

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

theory CSP_T_tactic
imports CSP_T_law CSP_T_law_etc
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |               February 2005  (modified)   |
            |                   June 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_tactic
imports CSP_T_law CSP_T_law_etc
begin

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

         1. tactic
         2.
         3. 
         4. 

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

(*================================================*
 |                                                |
 |                  Tacticals                     |
 |                                                |
 *================================================*)

lemmas cspT_all_dist = cspT_dist cspT_Dist cspT_Ext_dist
lemmas cspT_choice_IF = cspT_choice_rule cspT_IF

ML_setup {*
    val CSPT_reflex                    = thms "cspT_reflex" ;
    val CSPT_rw_flag_left              = thms "cspT_rw_flag_left" ;
    val CSPT_rw_flag_right             = thms "cspT_rw_flag_right" ;

    val CSPT_choice_IF                 = thms "cspT_choice_IF";
    val CSPT_step                      = thms "cspT_step" ;
    val CSPT_light_step                = thms "cspT_light_step" ;
    val CSPT_SKIP_DIV_resolve          = thms "cspT_SKIP_DIV_resolve" ;
    val CSPT_all_dist                  = thms "cspT_all_dist" ;
    val CSPT_unwind                    = thms "cspT_unwind" ;

    val CSPT_SKIP_DIV_sort      = thms "cspT_SKIP_DIV_sort";

    val CSPT_Ext_Int                   = thms "cspT_Ext_Int" ;

    val CSPT_free_decompo_flag         = thms "cspT_free_decompo_flag" ;
*}

(************************************************
             sequentialising
 ************************************************)

(*-----------------------------------------------------*
      apply (tactic {* cspT_hsf_main_tac 1 *})

                      is equal to

      apply (( simp
             | ((rule off_Not_Decompo_Flag)?,
                (  rule cspT_choice_IF
                 | rule cspT_SKIP_DIV_sort
                 | rule cspT_SKIP_DIV_resolve
                 | rule cspT_step
                 | rule cspT_all_dist
                 | rule cspT_unwind))
             | (rule cspT_rw_flag_left, rule cspT_free_decompo_flag)
             | ((rule off_Not_Decompo_Flag)?, rule cspT_reflex)
             | (rule off_Not_Decompo_Flag_True))+ ,
             (simp_all off_Not_Decompo_Flag_True))

 *-----------------------------------------------------*)

(*** Head Sequential Form ***)

ML_setup {*
fun cspT_hsf_main_tac n =
 CHANGED (
  EVERY
   [
    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n,
                        resolve_tac CSPT_SKIP_DIV_sort n,
                        resolve_tac CSPT_SKIP_DIV_resolve n,
                        resolve_tac CSPT_step n,
                        resolve_tac CSPT_all_dist n,
                        resolve_tac CSPT_unwind n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(*** simp_with ***)

(*-----------------------------------------------------*
      apply (tactic {* cspT_simp_with_main_tac "rulename" 1 *})

                      is equal to

      apply (( simp
             | ((rule off_Not_Decompo_Flag)?,
                (  rule cspT_rule_IF
                 | rule rulename))
             | (rule cspT_rw_flag_left, rule cspT_free_decompo_flag)
             | ((rule off_Not_Decompo_Flag)?, rule cspT_reflex),
             | (rule off_Not_Decompo_Flag_True))+ ,
             (simp add: rule off_Not_Decompo_Flag_True)?)

 *-----------------------------------------------------*)

ML_setup {*
fun cspT_simp_with_main_tac a n =
let val A = thms a
in
 CHANGED (
  EVERY
   [REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n,
                        resolve_tac A n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
end
*}

(*** trace ***)

ML_setup {*
fun cspT_trace_eq_main_tac n =
 CHANGED (
  EVERY
   [REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_Ext_Int n ]) ,

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(*** assumption ***)

ML_setup {*
fun cspT_asm_main_tac n =
 CHANGED (
  EVERY
   [REPEAT (
     FIRST 
      [(EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                (CHANGED (assume_tac n)) ]) ,

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    TRY (FIRST[ resolve_tac OFF_Not_Decompo_Flag n,
                resolve_tac OFF_Not_Decompo_Flag_True n])])
*}

(********* sub tactic of cspT_hsf_main_tac *********)

(*** step ***)

ML_setup {*
fun cspT_step_main_tac n =
 CHANGED (
  EVERY
   [
    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n,
                        resolve_tac CSPT_SKIP_DIV_resolve n,
                        resolve_tac CSPT_step n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(*** light step ***)

ML_setup {*
fun cspT_light_step_main_tac n =
 CHANGED (
  EVERY
   [
    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n,
                        resolve_tac CSPT_light_step n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(*** dist ***)

ML_setup {*
fun cspT_dist_main_tac n =
 CHANGED (
  EVERY
   [
    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n,
                        resolve_tac CSPT_all_dist n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(*** unwind ***)

ML_setup {*
fun cspT_unwind_main_tac n =
 CHANGED (
  EVERY
   [
    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n,
                        resolve_tac CSPT_unwind n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(*** sort ***)

ML_setup {*
fun cspT_sort_main_tac n =
 CHANGED (
  EVERY
   [
    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n,
                        resolve_tac CSPT_SKIP_DIV_sort n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(*** simp ***)

ML_setup {*
fun cspT_simp_main_tac n =
 CHANGED (
  EVERY
   [
    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset ()) n)),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                FIRST [ resolve_tac CSPT_choice_IF n ]]),

       (EVERY [ resolve_tac CSPT_rw_flag_left n , 
                resolve_tac CSPT_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPT_reflex n ]),

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

    (ALLGOALS (asm_full_simp_tac (simpset () addsimps OFF_Not_Decompo_Flag_True)))])
*}

(************************************************
                  rewrite left
 ************************************************)

(*** hsf ***)

ML_setup {*
fun cspT_hsf_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_hsf_main_tac n])
*}

(*** simp_with ***)

ML_setup {*
fun cspT_simp_with_left_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_simp_with_main_tac a n])
*}

(*** trace ***)

ML_setup {*
fun cspT_trace_eq_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_trace_eq_main_tac n])
*}

(*** assumption ***)

ML_setup {*
fun cspT_asm_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_asm_main_tac n])
*}

(*** step ***)

ML_setup {*
fun cspT_step_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_step_main_tac n])
*}

(*** light step ***)

ML_setup {*
fun cspT_light_step_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_light_step_main_tac n])
*}

(*** dist ***)

ML_setup {*
fun cspT_dist_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_dist_main_tac n])
*}

(*** unwind ***)

ML_setup {*
fun cspT_unwind_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_unwind_main_tac n])
*}

(*** sort ***)

ML_setup {*
fun cspT_sort_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_sort_main_tac n])
*}

(*** simp ***)

ML_setup {*
fun cspT_simp_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_left n,
    cspT_simp_main_tac n])
*}

(************************************************
                  rewrite right
 ************************************************)

(*** hsf ***)

ML_setup {*
fun cspT_hsf_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_hsf_main_tac n])
*}

(*** simp_with ***)

ML_setup {*
fun cspT_simp_with_right_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_simp_with_main_tac a n])
*}

(*** trace ***)

ML_setup {*
fun cspT_trace_eq_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_trace_eq_main_tac n])
*}

(*** assumption ***)

ML_setup {*
fun cspT_asm_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_asm_main_tac n])
*}

(*** step ***)

ML_setup {*
fun cspT_step_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_step_main_tac n])
*}

(*** light step ***)

ML_setup {*
fun cspT_light_step_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_light_step_main_tac n])
*}

(*** dist ***)

ML_setup {*
fun cspT_dist_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_dist_main_tac n])
*}

(*** unwind ***)

ML_setup {*
fun cspT_unwind_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_unwind_main_tac n])
*}

(*** sort ***)

ML_setup {*
fun cspT_sort_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_sort_main_tac n])
*}

(*** simp ***)

ML_setup {*
fun cspT_simp_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_rw_flag_right n,
    cspT_simp_main_tac n])
*}

(************************************************
                 rewrite both
 ************************************************)

(*-----------------------------------------------------*
      Apply (tactic {* cspT_hnf_tac n *})
                      is equal to
      apply ((tactic {* cspT_hnf_left_tac n *})? ,
             (tactic {* cspT_hnf_right_tac n *})?)
 *-----------------------------------------------------*)

ML_setup {*
    fun cspT_hsf_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_hsf_left_tac n),
         TRY (cspT_hsf_right_tac n)])
*}

(*-----------------------------------------------------*
      apply (tactic {* cspT_simp_with_tac a n *})
                      is equal to
      apply ((tactic {* cspT_simp_with_left_tac a n *})? ,
             (tactic {* cspT_simp_with_right_tac a n *})?)
 *-----------------------------------------------------*)

ML_setup {*
    fun cspT_simp_with_tac a n = 
      CHANGED (
       EVERY
        [TRY (cspT_simp_with_left_tac a n),
         TRY (cspT_simp_with_right_tac a n)])
*}

(*-----------------------------------------------------*
      apply (tactic {* cspT_asm_tac n *})
                      is equal to
      apply ((tactic {* cspT_asm_left_tac n *})? ,
             (tactic {* cspT_asm_right_tac n *})?)
 *-----------------------------------------------------*)

ML_setup {*
    fun cspT_trace_eq_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_trace_eq_left_tac n),
         TRY (cspT_trace_eq_right_tac n)])
*}

ML_setup {*
    fun cspT_asm_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_asm_left_tac n),
         TRY (cspT_asm_right_tac n)])
*}

ML_setup {*
    fun cspT_step_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_step_left_tac n),
         TRY (cspT_step_right_tac n)])
*}

ML_setup {*
    fun cspT_light_step_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_light_step_left_tac n),
         TRY (cspT_light_step_right_tac n)])
*}

ML_setup {*
    fun cspT_dist_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_dist_left_tac n),
         TRY (cspT_dist_right_tac n)])
*}

ML_setup {*
    fun cspT_unwind_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_unwind_left_tac n),
         TRY (cspT_unwind_right_tac n)])
*}

ML_setup {*
    fun cspT_sort_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_sort_left_tac n),
         TRY (cspT_sort_right_tac n)])
*}

ML_setup {*
    fun cspT_simp_tac n = 
      CHANGED (
       EVERY
        [TRY (cspT_simp_left_tac n),
         TRY (cspT_simp_right_tac n)])
*}

end

lemmas cspT_all_dist: 

  (P1.0 |~| P2.0) [+] Q =T[M,M] P1.0 [+] Q |~| P2.0 [+] Q
  P [+] (Q1.0 |~| Q2.0) =T[M,M] P [+] Q1.0 |~| P [+] Q2.0
  (P1.0 |~| P2.0) |[X]| Q =T[M,M] P1.0 |[X]| Q |~| P2.0 |[X]| Q
  P |[X]| (Q1.0 |~| Q2.0) =T[M,M] P |[X]| Q1.0 |~| P |[X]| Q2.0
  (P1.0 |~| P2.0) -- X =T[M,M] P1.0 -- X |~| P2.0 -- X
  (P1.0 |~| P2.0) [[r]] =T[M,M] P1.0 [[r]] |~| P2.0 [[r]]
  (P1.0 |~| P2.0) ;; Q =T[M,M] P1.0 ;; Q |~| P2.0 ;; Q
  (P1.0 |~| P2.0) |. n =T[M,M] P1.0 |. n |~| P2.0 |. n
  !nat n:N .. (Pf n |~| Qf n) =T[M,M] !nat :N .. Pf |~| !nat :N .. Qf
  !set X:Xs .. (Pf X |~| Qf X) =T[M,M] !set :Xs .. Pf |~| !set :Xs .. Qf
  ! a:X .. (Pf a |~| Qf a) =T[M,M] ! :X .. Pf |~| ! :X .. Qf
  inj f ==> !<f> a:X .. (Pf a |~| Qf a) =T[M,M] !<f> :X .. Pf |~| !<f> :X .. Qf
  (!nat :N .. Pf) [+] Q =T[M,M] 
  IF (N = {}) THEN DIV [+] Q ELSE !nat n:N .. Pf n [+] Q
  P [+] (!nat :N .. Qf) =T[M,M] 
  IF (N = {}) THEN P [+] DIV ELSE !nat n:N .. P [+] Qf n
  (!nat :N .. Pf) |[X]| Q =T[M,M] 
  IF (N = {}) THEN DIV |[X]| Q ELSE !nat n:N .. Pf n |[X]| Q
  P |[X]| (!nat :N .. Qf) =T[M,M] 
  IF (N = {}) THEN P |[X]| DIV ELSE !nat n:N .. P |[X]| Qf n
  (!nat :N .. Pf) -- X =T[M,M] !nat n:N .. Pf n -- X
  (!nat :N .. Pf) [[r]] =T[M,M] !nat n:N .. Pf n [[r]]
  (!nat :N .. Pf) ;; Q =T[M,M] !nat n:N .. Pf n ;; Q
  (!nat :N .. Pf) |. m =T[M,M] !nat n:N .. Pf n |. m
  (!set :Xs .. Pf) [+] Q =T[M,M] 
  IF (Xs = {}) THEN DIV [+] Q ELSE !set X:Xs .. Pf X [+] Q
  P [+] (!set :Xs .. Qf) =T[M,M] 
  IF (Xs = {}) THEN P [+] DIV ELSE !set X:Xs .. P [+] Qf X
  (!set :Xs .. Pf) |[Y]| Q =T[M,M] 
  IF (Xs = {}) THEN DIV |[Y]| Q ELSE !set X:Xs .. Pf X |[Y]| Q
  P |[Y]| (!set :Xs .. Qf) =T[M,M] 
  IF (Xs = {}) THEN P |[Y]| DIV ELSE !set X:Xs .. P |[Y]| Qf X
  (!set :Xs .. Pf) -- Y =T[M,M] !set X:Xs .. Pf X -- Y
  (!set :Xs .. Pf) [[r]] =T[M,M] !set X:Xs .. Pf X [[r]]
  (!set :Xs .. Pf) ;; Q =T[M,M] !set X:Xs .. Pf X ;; Q
  (!set :Xs .. Pf) |. m =T[M,M] !set X:Xs .. Pf X |. m
  (! :X .. Pf) [+] Q =T[M,M] IF (X = {}) THEN DIV [+] Q ELSE ! x:X .. Pf x [+] Q
  P [+] (! :X .. Qf) =T[M,M] IF (X = {}) THEN P [+] DIV ELSE ! x:X .. P [+] Qf x
  (! :Y .. Pf) |[X]| Q =T[M,M] 
  IF (Y = {}) THEN DIV |[X]| Q ELSE ! x:Y .. Pf x |[X]| Q
  P |[X]| (! :Y .. Qf) =T[M,M] 
  IF (Y = {}) THEN P |[X]| DIV ELSE ! x:Y .. P |[X]| Qf x
  (! :Y .. Pf) -- X =T[M,M] ! x:Y .. Pf x -- X
  (! :X .. Pf) [[r]] =T[M,M] ! x:X .. Pf x [[r]]
  (! :X .. Pf) ;; Q =T[M,M] ! x:X .. Pf x ;; Q
  (! :X .. Pf) |. n =T[M,M] ! x:X .. Pf x |. n
  (!<f> :X .. Pf) [+] Q =T[M,M] 
  IF (X = {}) THEN DIV [+] Q ELSE !<f> x:X .. Pf x [+] Q
  P [+] (!<f> :X .. Qf) =T[M,M] 
  IF (X = {}) THEN P [+] DIV ELSE !<f> x:X .. P [+] Qf x
  (!<f> :Y .. Pf) |[X]| Q =T[M,M] 
  IF (Y = {}) THEN DIV |[X]| Q ELSE !<f> x:Y .. Pf x |[X]| Q
  P |[X]| (!<f> :Y .. Qf) =T[M,M] 
  IF (Y = {}) THEN P |[X]| DIV ELSE !<f> x:Y .. P |[X]| Qf x
  (!<f> :Y .. Pf) -- X =T[M,M] !<f> x:Y .. Pf x -- X
  (!<f> :X .. Pf) [[r]] =T[M,M] !<f> x:X .. Pf x [[r]]
  (!<f> :X .. Pf) ;; Q =T[M,M] !<f> x:X .. Pf x ;; Q
  (!<f> :X .. Pf) |. n =T[M,M] !<f> x:X .. Pf x |. n
  (P1.0 [+] P2.0) [[r]] =T[M,M] P1.0 [[r]] [+] P2.0 [[r]]
  (P1.0 [+] P2.0) |. n =T[M,M] P1.0 |. n [+] P2.0 |. n

lemmas cspT_all_dist: 

  (P1.0 |~| P2.0) [+] Q =T[M,M] P1.0 [+] Q |~| P2.0 [+] Q
  P [+] (Q1.0 |~| Q2.0) =T[M,M] P [+] Q1.0 |~| P [+] Q2.0
  (P1.0 |~| P2.0) |[X]| Q =T[M,M] P1.0 |[X]| Q |~| P2.0 |[X]| Q
  P |[X]| (Q1.0 |~| Q2.0) =T[M,M] P |[X]| Q1.0 |~| P |[X]| Q2.0
  (P1.0 |~| P2.0) -- X =T[M,M] P1.0 -- X |~| P2.0 -- X
  (P1.0 |~| P2.0) [[r]] =T[M,M] P1.0 [[r]] |~| P2.0 [[r]]
  (P1.0 |~| P2.0) ;; Q =T[M,M] P1.0 ;; Q |~| P2.0 ;; Q
  (P1.0 |~| P2.0) |. n =T[M,M] P1.0 |. n |~| P2.0 |. n
  !nat n:N .. (Pf n |~| Qf n) =T[M,M] !nat :N .. Pf |~| !nat :N .. Qf
  !set X:Xs .. (Pf X |~| Qf X) =T[M,M] !set :Xs .. Pf |~| !set :Xs .. Qf
  ! a:X .. (Pf a |~| Qf a) =T[M,M] ! :X .. Pf |~| ! :X .. Qf
  inj f ==> !<f> a:X .. (Pf a |~| Qf a) =T[M,M] !<f> :X .. Pf |~| !<f> :X .. Qf
  (!nat :N .. Pf) [+] Q =T[M,M] 
  IF (N = {}) THEN DIV [+] Q ELSE !nat n:N .. Pf n [+] Q
  P [+] (!nat :N .. Qf) =T[M,M] 
  IF (N = {}) THEN P [+] DIV ELSE !nat n:N .. P [+] Qf n
  (!nat :N .. Pf) |[X]| Q =T[M,M] 
  IF (N = {}) THEN DIV |[X]| Q ELSE !nat n:N .. Pf n |[X]| Q
  P |[X]| (!nat :N .. Qf) =T[M,M] 
  IF (N = {}) THEN P |[X]| DIV ELSE !nat n:N .. P |[X]| Qf n
  (!nat :N .. Pf) -- X =T[M,M] !nat n:N .. Pf n -- X
  (!nat :N .. Pf) [[r]] =T[M,M] !nat n:N .. Pf n [[r]]
  (!nat :N .. Pf) ;; Q =T[M,M] !nat n:N .. Pf n ;; Q
  (!nat :N .. Pf) |. m =T[M,M] !nat n:N .. Pf n |. m
  (!set :Xs .. Pf) [+] Q =T[M,M] 
  IF (Xs = {}) THEN DIV [+] Q ELSE !set X:Xs .. Pf X [+] Q
  P [+] (!set :Xs .. Qf) =T[M,M] 
  IF (Xs = {}) THEN P [+] DIV ELSE !set X:Xs .. P [+] Qf X
  (!set :Xs .. Pf) |[Y]| Q =T[M,M] 
  IF (Xs = {}) THEN DIV |[Y]| Q ELSE !set X:Xs .. Pf X |[Y]| Q
  P |[Y]| (!set :Xs .. Qf) =T[M,M] 
  IF (Xs = {}) THEN P |[Y]| DIV ELSE !set X:Xs .. P |[Y]| Qf X
  (!set :Xs .. Pf) -- Y =T[M,M] !set X:Xs .. Pf X -- Y
  (!set :Xs .. Pf) [[r]] =T[M,M] !set X:Xs .. Pf X [[r]]
  (!set :Xs .. Pf) ;; Q =T[M,M] !set X:Xs .. Pf X ;; Q
  (!set :Xs .. Pf) |. m =T[M,M] !set X:Xs .. Pf X |. m
  (! :X .. Pf) [+] Q =T[M,M] IF (X = {}) THEN DIV [+] Q ELSE ! x:X .. Pf x [+] Q
  P [+] (! :X .. Qf) =T[M,M] IF (X = {}) THEN P [+] DIV ELSE ! x:X .. P [+] Qf x
  (! :Y .. Pf) |[X]| Q =T[M,M] 
  IF (Y = {}) THEN DIV |[X]| Q ELSE ! x:Y .. Pf x |[X]| Q
  P |[X]| (! :Y .. Qf) =T[M,M] 
  IF (Y = {}) THEN P |[X]| DIV ELSE ! x:Y .. P |[X]| Qf x
  (! :Y .. Pf) -- X =T[M,M] ! x:Y .. Pf x -- X
  (! :X .. Pf) [[r]] =T[M,M] ! x:X .. Pf x [[r]]
  (! :X .. Pf) ;; Q =T[M,M] ! x:X .. Pf x ;; Q
  (! :X .. Pf) |. n =T[M,M] ! x:X .. Pf x |. n
  (!<f> :X .. Pf) [+] Q =T[M,M] 
  IF (X = {}) THEN DIV [+] Q ELSE !<f> x:X .. Pf x [+] Q
  P [+] (!<f> :X .. Qf) =T[M,M] 
  IF (X = {}) THEN P [+] DIV ELSE !<f> x:X .. P [+] Qf x
  (!<f> :Y .. Pf) |[X]| Q =T[M,M] 
  IF (Y = {}) THEN DIV |[X]| Q ELSE !<f> x:Y .. Pf x |[X]| Q
  P |[X]| (!<f> :Y .. Qf) =T[M,M] 
  IF (Y = {}) THEN P |[X]| DIV ELSE !<f> x:Y .. P |[X]| Qf x
  (!<f> :Y .. Pf) -- X =T[M,M] !<f> x:Y .. Pf x -- X
  (!<f> :X .. Pf) [[r]] =T[M,M] !<f> x:X .. Pf x [[r]]
  (!<f> :X .. Pf) ;; Q =T[M,M] !<f> x:X .. Pf x ;; Q
  (!<f> :X .. Pf) |. n =T[M,M] !<f> x:X .. Pf x |. n
  (P1.0 [+] P2.0) [[r]] =T[M,M] P1.0 [[r]] [+] P2.0 [[r]]
  (P1.0 [+] P2.0) |. n =T[M,M] P1.0 |. n [+] P2.0 |. n

lemmas cspT_choice_IF: 

  !nat :{} .. Pf =T[M1.0,M2.0] DIV
  !set :{} .. Pf =T[M1.0,M2.0] DIV
  ! :{} .. Pf =T[M1.0,M2.0] DIV
  inj f ==> !<f> :{} .. Pf =T[M1.0,M2.0] DIV
  !nat :{n} .. Pf =T[M,M] Pf n
  !set :{X} .. Pf =T[M,M] Pf X
  ! :{a} .. Pf =T[M,M] Pf a
  inj f ==> !<f> :{x} .. Pf =T[M,M] Pf x
  P |~| P =T[M,M] P
  !nat n:N .. P =T[M,M] IF (N = {}) THEN DIV ELSE P
  !set X:Xs .. P =T[M,M] IF (Xs = {}) THEN DIV ELSE P
  ! x:X .. P =T[M,M] IF (X = {}) THEN DIV ELSE P
  !<f> x:X .. P =T[M,M] IF (X = {}) THEN DIV ELSE P
  ? :{} -> Pf =T[M1.0,M2.0] ? a:{} -> DIV
  STOP [+] P =T[M,M] P
  ? :{} -> Qf [+] P =T[M,M] P
  P [+] STOP =T[M,M] P
  P [+] ? :{} -> Qf =T[M,M] P
  P [+] P =T[M,M] P
  IF True THEN P ELSE Q =T[M,M] P
  IF False THEN P ELSE Q =T[M,M] Q

lemmas cspT_choice_IF: 

  !nat :{} .. Pf =T[M1.0,M2.0] DIV
  !set :{} .. Pf =T[M1.0,M2.0] DIV
  ! :{} .. Pf =T[M1.0,M2.0] DIV
  inj f ==> !<f> :{} .. Pf =T[M1.0,M2.0] DIV
  !nat :{n} .. Pf =T[M,M] Pf n
  !set :{X} .. Pf =T[M,M] Pf X
  ! :{a} .. Pf =T[M,M] Pf a
  inj f ==> !<f> :{x} .. Pf =T[M,M] Pf x
  P |~| P =T[M,M] P
  !nat n:N .. P =T[M,M] IF (N = {}) THEN DIV ELSE P
  !set X:Xs .. P =T[M,M] IF (Xs = {}) THEN DIV ELSE P
  ! x:X .. P =T[M,M] IF (X = {}) THEN DIV ELSE P
  !<f> x:X .. P =T[M,M] IF (X = {}) THEN DIV ELSE P
  ? :{} -> Pf =T[M1.0,M2.0] ? a:{} -> DIV
  STOP [+] P =T[M,M] P
  ? :{} -> Qf [+] P =T[M,M] P
  P [+] STOP =T[M,M] P
  P [+] ? :{} -> Qf =T[M,M] P
  P [+] P =T[M,M] P
  IF True THEN P ELSE Q =T[M,M] P
  IF False THEN P ELSE Q =T[M,M] Q