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)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_tactic = CSP_T_law + CSP_T_law_etc:

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

         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_unwind_MU                 = thms "cspT_unwind_MU" ;

    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_unwind_MU))
             | (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,
                        resolve_tac CSPT_unwind_MU 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,
                        resolve_tac CSPT_unwind_MU 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 P1.0 [+] Q |~| P2.0 [+] Q
  P [+] (Q1.0 |~| Q2.0) =T P [+] Q1.0 |~| P [+] Q2.0
  (P1.0 |~| P2.0) |[X]| Q =T P1.0 |[X]| Q |~| P2.0 |[X]| Q
  P |[X]| (Q1.0 |~| Q2.0) =T P |[X]| Q1.0 |~| P |[X]| Q2.0
  (P1.0 |~| P2.0) -- X =T P1.0 -- X |~| P2.0 -- X
  (P1.0 |~| P2.0) [[r]] =T P1.0 [[r]] |~| P2.0 [[r]]
  (P1.0 |~| P2.0) ;; Q =T P1.0 ;; Q |~| P2.0 ;; Q
  (P1.0 |~| P2.0) |. n =T P1.0 |. n |~| P2.0 |. n
  !! c:C .. (Pf c |~| Qf c) =T !! :C .. Pf |~| !! :C .. Qf
  (!! :C .. Pf) [+] Q =T IF (C = {}) THEN DIV [+] Q ELSE !! c:C .. Pf c [+] Q
  P [+] (!! :C .. Qf) =T IF (C = {}) THEN P [+] DIV ELSE !! c:C .. P [+] Qf c
  (!! :C .. Pf) |[X]| Q =T 
  IF (C = {}) THEN DIV |[X]| Q ELSE !! c:C .. Pf c |[X]| Q
  P |[X]| (!! :C .. Qf) =T 
  IF (C = {}) THEN P |[X]| DIV ELSE !! c:C .. P |[X]| Qf c
  (!! :C .. Pf) -- X =T !! c:C .. Pf c -- X
  (!! :C .. Pf) [[r]] =T !! c:C .. Pf c [[r]]
  (!! :C .. Pf) ;; Q =T !! c:C .. Pf c ;; Q
  (!! :C .. Pf) |. n =T !! c:C .. Pf c |. n
  (!!<f> :X .. Pf) [+] Q =T 
  IF (X = {}) THEN DIV [+] Q ELSE !!<f> x:X .. Pf x [+] Q
  P [+] (!!<f> :X .. Qf) =T 
  IF (X = {}) THEN P [+] DIV ELSE !!<f> x:X .. P [+] Qf x
  (!!<f> :Y .. Pf) |[X]| Q =T 
  IF (Y = {}) THEN DIV |[X]| Q ELSE !!<f> x:Y .. Pf x |[X]| Q
  P |[X]| (!!<f> :Y .. Qf) =T 
  IF (Y = {}) THEN P |[X]| DIV ELSE !!<f> x:Y .. P |[X]| Qf x
  (!!<f> :Y .. Pf) -- X =T !!<f> x:Y .. Pf x -- X
  (!!<f> :X .. Pf) [[r]] =T !!<f> x:X .. Pf x [[r]]
  (!!<f> :X .. Pf) ;; Q =T !!<f> x:X .. Pf x ;; Q
  (!!<f> :X .. Pf) |. n =T !!<f> x:X .. Pf x |. n
  (! :X .. Pf) [+] Q =T IF (X = {}) THEN DIV [+] Q ELSE ! x:X .. Pf x [+] Q
  P [+] (! :X .. Qf) =T IF (X = {}) THEN P [+] DIV ELSE ! x:X .. P [+] Qf x
  (! :Y .. Pf) |[X]| Q =T IF (Y = {}) THEN DIV |[X]| Q ELSE ! x:Y .. Pf x |[X]| Q
  P |[X]| (! :Y .. Qf) =T IF (Y = {}) THEN P |[X]| DIV ELSE ! x:Y .. P |[X]| Qf x
  (! :Y .. Pf) -- X =T ! x:Y .. Pf x -- X
  (! :X .. Pf) [[r]] =T ! x:X .. Pf x [[r]]
  (! :X .. Pf) ;; Q =T ! x:X .. Pf x ;; Q
  (! :X .. Pf) |. n =T ! x:X .. Pf x |. n
  (P1.0 [+] P2.0) [[r]] =T P1.0 [[r]] [+] P2.0 [[r]]
  (P1.0 [+] P2.0) |. n =T P1.0 |. n [+] P2.0 |. n

lemmas cspT_all_dist: 

  (P1.0 |~| P2.0) [+] Q =T P1.0 [+] Q |~| P2.0 [+] Q
  P [+] (Q1.0 |~| Q2.0) =T P [+] Q1.0 |~| P [+] Q2.0
  (P1.0 |~| P2.0) |[X]| Q =T P1.0 |[X]| Q |~| P2.0 |[X]| Q
  P |[X]| (Q1.0 |~| Q2.0) =T P |[X]| Q1.0 |~| P |[X]| Q2.0
  (P1.0 |~| P2.0) -- X =T P1.0 -- X |~| P2.0 -- X
  (P1.0 |~| P2.0) [[r]] =T P1.0 [[r]] |~| P2.0 [[r]]
  (P1.0 |~| P2.0) ;; Q =T P1.0 ;; Q |~| P2.0 ;; Q
  (P1.0 |~| P2.0) |. n =T P1.0 |. n |~| P2.0 |. n
  !! c:C .. (Pf c |~| Qf c) =T !! :C .. Pf |~| !! :C .. Qf
  (!! :C .. Pf) [+] Q =T IF (C = {}) THEN DIV [+] Q ELSE !! c:C .. Pf c [+] Q
  P [+] (!! :C .. Qf) =T IF (C = {}) THEN P [+] DIV ELSE !! c:C .. P [+] Qf c
  (!! :C .. Pf) |[X]| Q =T 
  IF (C = {}) THEN DIV |[X]| Q ELSE !! c:C .. Pf c |[X]| Q
  P |[X]| (!! :C .. Qf) =T 
  IF (C = {}) THEN P |[X]| DIV ELSE !! c:C .. P |[X]| Qf c
  (!! :C .. Pf) -- X =T !! c:C .. Pf c -- X
  (!! :C .. Pf) [[r]] =T !! c:C .. Pf c [[r]]
  (!! :C .. Pf) ;; Q =T !! c:C .. Pf c ;; Q
  (!! :C .. Pf) |. n =T !! c:C .. Pf c |. n
  (!!<f> :X .. Pf) [+] Q =T 
  IF (X = {}) THEN DIV [+] Q ELSE !!<f> x:X .. Pf x [+] Q
  P [+] (!!<f> :X .. Qf) =T 
  IF (X = {}) THEN P [+] DIV ELSE !!<f> x:X .. P [+] Qf x
  (!!<f> :Y .. Pf) |[X]| Q =T 
  IF (Y = {}) THEN DIV |[X]| Q ELSE !!<f> x:Y .. Pf x |[X]| Q
  P |[X]| (!!<f> :Y .. Qf) =T 
  IF (Y = {}) THEN P |[X]| DIV ELSE !!<f> x:Y .. P |[X]| Qf x
  (!!<f> :Y .. Pf) -- X =T !!<f> x:Y .. Pf x -- X
  (!!<f> :X .. Pf) [[r]] =T !!<f> x:X .. Pf x [[r]]
  (!!<f> :X .. Pf) ;; Q =T !!<f> x:X .. Pf x ;; Q
  (!!<f> :X .. Pf) |. n =T !!<f> x:X .. Pf x |. n
  (! :X .. Pf) [+] Q =T IF (X = {}) THEN DIV [+] Q ELSE ! x:X .. Pf x [+] Q
  P [+] (! :X .. Qf) =T IF (X = {}) THEN P [+] DIV ELSE ! x:X .. P [+] Qf x
  (! :Y .. Pf) |[X]| Q =T IF (Y = {}) THEN DIV |[X]| Q ELSE ! x:Y .. Pf x |[X]| Q
  P |[X]| (! :Y .. Qf) =T IF (Y = {}) THEN P |[X]| DIV ELSE ! x:Y .. P |[X]| Qf x
  (! :Y .. Pf) -- X =T ! x:Y .. Pf x -- X
  (! :X .. Pf) [[r]] =T ! x:X .. Pf x [[r]]
  (! :X .. Pf) ;; Q =T ! x:X .. Pf x ;; Q
  (! :X .. Pf) |. n =T ! x:X .. Pf x |. n
  (P1.0 [+] P2.0) [[r]] =T P1.0 [[r]] [+] P2.0 [[r]]
  (P1.0 [+] P2.0) |. n =T P1.0 |. n [+] P2.0 |. n

lemmas cspT_choice_IF: 

  !! :{} .. Pf =T DIV
  ! :{} .. Pf =T DIV
  !set :{} .. Pf =T DIV
  !nat :{} .. Pf =T DIV
  !! :{c} .. Pf =T Pf c
  ! :{a} .. Pf =T Pf a
  !set :{X} .. Pf =T Pf X
  !nat :{n} .. Pf =T Pf n
  P |~| P =T P
  !! c:C .. P =T IF (C = {}) THEN DIV ELSE P
  ! x:X .. P =T IF (X = {}) THEN DIV ELSE P
  !set X:Xs .. P =T IF (Xs = {}) THEN DIV ELSE P
  !nat n:N .. P =T IF (N = {}) THEN DIV ELSE P
  ? :{} -> Pf =T ? a:{} -> DIV
  STOP [+] P =T P
  ? :{} -> Qf [+] P =T P
  P [+] STOP =T P
  P [+] ? :{} -> Qf =T P
  P [+] P =T P
  IF True THEN P ELSE Q =T P
  IF False THEN P ELSE Q =T Q

lemmas cspT_choice_IF: 

  !! :{} .. Pf =T DIV
  ! :{} .. Pf =T DIV
  !set :{} .. Pf =T DIV
  !nat :{} .. Pf =T DIV
  !! :{c} .. Pf =T Pf c
  ! :{a} .. Pf =T Pf a
  !set :{X} .. Pf =T Pf X
  !nat :{n} .. Pf =T Pf n
  P |~| P =T P
  !! c:C .. P =T IF (C = {}) THEN DIV ELSE P
  ! x:X .. P =T IF (X = {}) THEN DIV ELSE P
  !set X:Xs .. P =T IF (Xs = {}) THEN DIV ELSE P
  !nat n:N .. P =T IF (N = {}) THEN DIV ELSE P
  ? :{} -> Pf =T ? a:{} -> DIV
  STOP [+] P =T P
  ? :{} -> Qf [+] P =T P
  P [+] STOP =T P
  P [+] ? :{} -> Qf =T P
  P [+] P =T P
  IF True THEN P ELSE Q =T P
  IF False THEN P ELSE Q =T Q