Theory CSP_F_tactic

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

theory CSP_F_tactic
imports CSP_F_law CSP_F_law_etc
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |               February 2005  (modified)   |
            |                   June 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |               November 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_tactic = CSP_F_law + CSP_F_law_etc:

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

         1. tactic
         2.
         3. 
         4. 

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

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

lemmas cspF_all_dist = cspF_dist cspF_Dist cspF_Ext_dist
lemmas cspF_choice_IF = cspF_choice_rule cspF_IF

ML_setup {*
    val CSPF_reflex                    = thms "cspF_reflex" ;
    val CSPF_rw_flag_left              = thms "cspF_rw_flag_left" ;
    val CSPF_rw_flag_right             = thms "cspF_rw_flag_right" ;

    val CSPF_choice_IF                 = thms "cspF_choice_IF";
    val CSPF_step                      = thms "cspF_step" ;
    val CSPF_light_step                = thms "cspF_light_step" ;
    val CSPF_SKIP_DIV_resolve          = thms "cspF_SKIP_DIV_resolve" ;
    val CSPF_all_dist                  = thms "cspF_all_dist" ;
    val CSPF_unwind                    = thms "cspF_unwind" ;
    val CSPF_unwind_MU                 = thms "cspF_unwind_MU" ;

    val CSPF_SKIP_DIV_sort             = thms "cspF_SKIP_DIV_sort";

    val CSPF_free_decompo_flag         = thms "cspF_free_decompo_flag" ;
*}

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

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

                      is equal to

      apply (( simp
             | ((rule off_Not_Decompo_Flag)?,
                (  rule cspF_choice_IF
                 | rule cspF_SKIP_DIV_sort
                 | rule cspF_SKIP_DIV_resolve
                 | rule cspF_step
                 | rule cspF_all_dist
                 | rule cspF_unwind
                 | rule cspF_unwind_MU))
             | (rule cspF_rw_flag_left, rule cspF_free_decompo_flag)
             | ((rule off_Not_Decompo_Flag)?, rule cspF_reflex)
             | (rule off_Not_Decompo_Flag_True))+ ,
             (simp_all off_Not_Decompo_Flag_True))

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

(*** Head Sequential Form ***)

ML_setup {*
fun cspF_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 CSPF_choice_IF n,
                        resolve_tac CSPF_SKIP_DIV_sort n,
                        resolve_tac CSPF_SKIP_DIV_resolve n,
                        resolve_tac CSPF_step n,
                        resolve_tac CSPF_all_dist n,
                        resolve_tac CSPF_unwind n,
                        resolve_tac CSPF_unwind_MU n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 {* cspF_simp_with_main_tac "rulename" 1 *})

                      is equal to

      apply (( simp
             | ((rule off_Not_Decompo_Flag)?,
                (  rule cspF_rule_IF
                 | rule rulename))
             | (rule cspF_rw_flag_left, rule cspF_free_decompo_flag)
             | ((rule off_Not_Decompo_Flag)?, rule cspF_reflex),
             | (rule off_Not_Decompo_Flag_True))+ ,
             (simp add: rule off_Not_Decompo_Flag_True)?)

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

ML_setup {*
fun cspF_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 CSPF_choice_IF n,
                        resolve_tac A n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

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

       (resolve_tac OFF_Not_Decompo_Flag_True n)]) ,

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

(*** assumption ***)

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

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 cspF_hsf_main_tac *********)

(*** step ***)

ML_setup {*
fun cspF_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 CSPF_choice_IF n,
                        resolve_tac CSPF_SKIP_DIV_resolve n,
                        resolve_tac CSPF_step n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 cspF_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 CSPF_choice_IF n,
                        resolve_tac CSPF_light_step n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 cspF_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 CSPF_choice_IF n,
                        resolve_tac CSPF_all_dist n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 cspF_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 CSPF_choice_IF n,
                        resolve_tac CSPF_unwind n,
                        resolve_tac CSPF_unwind_MU n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 cspF_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 CSPF_choice_IF n,
                        resolve_tac CSPF_SKIP_DIV_sort n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 cspF_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 CSPF_choice_IF n ]]),

       (EVERY [ resolve_tac CSPF_rw_flag_left n , 
                resolve_tac CSPF_free_decompo_flag n ]),

       (EVERY [ TRY (resolve_tac OFF_Not_Decompo_Flag n), 
                resolve_tac CSPF_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 cspF_hsf_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_hsf_main_tac n])
*}

(*** simp_with ***)

ML_setup {*
fun cspF_simp_with_left_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_simp_with_main_tac a n])
*}

(*** assumption ***)

ML_setup {*
fun cspF_asm_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_asm_main_tac n])
*}

(*** step ***)

ML_setup {*
fun cspF_step_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_step_main_tac n])
*}

(*** light step ***)

ML_setup {*
fun cspF_light_step_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_light_step_main_tac n])
*}

(*** dist ***)

ML_setup {*
fun cspF_dist_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_dist_main_tac n])
*}

(*** unwind ***)

ML_setup {*
fun cspF_unwind_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_unwind_main_tac n])
*}

(*** sort ***)

ML_setup {*
fun cspF_sort_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_sort_main_tac n])
*}

(*** simp ***)

ML_setup {*
fun cspF_simp_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_left n,
    cspF_simp_main_tac n])
*}

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

(*** hsf ***)

ML_setup {*
fun cspF_hsf_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_hsf_main_tac n])
*}

(*** simp_with ***)

ML_setup {*
fun cspF_simp_with_right_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_simp_with_main_tac a n])
*}

(*** assumption ***)

ML_setup {*
fun cspF_asm_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_asm_main_tac n])
*}

(*** step ***)

ML_setup {*
fun cspF_step_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_step_main_tac n])
*}

(*** light step ***)

ML_setup {*
fun cspF_light_step_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_light_step_main_tac n])
*}

(*** dist ***)

ML_setup {*
fun cspF_dist_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_dist_main_tac n])
*}

(*** unwind ***)

ML_setup {*
fun cspF_unwind_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_unwind_main_tac n])
*}

(*** sort ***)

ML_setup {*
fun cspF_sort_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_sort_main_tac n])
*}

(*** simp ***)

ML_setup {*
fun cspF_simp_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_rw_flag_right n,
    cspF_simp_main_tac n])
*}

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

(*-----------------------------------------------------*
      Apply (tactic {* cspF_hnf_tac n *})
                      is equal to
      apply ((tactic {* cspF_hnf_left_tac n *})? ,
             (tactic {* cspF_hnf_right_tac n *})?)
 *-----------------------------------------------------*)

ML_setup {*
    fun cspF_hsf_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_hsf_left_tac n),
         TRY (cspF_hsf_right_tac n)])
*}

(*-----------------------------------------------------*
      apply (tactic {* cspF_simp_with_tac a n *})
                      is equal to
      apply ((tactic {* cspF_simp_with_left_tac a n *})? ,
             (tactic {* cspF_simp_with_right_tac a n *})?)
 *-----------------------------------------------------*)

ML_setup {*
    fun cspF_simp_with_tac a n = 
      CHANGED (
       EVERY
        [TRY (cspF_simp_with_left_tac a n),
         TRY (cspF_simp_with_right_tac a n)])
*}

(*-----------------------------------------------------*
      apply (tactic {* cspF_asm_tac n *})
                      is equal to
      apply ((tactic {* cspF_asm_left_tac n *})? ,
             (tactic {* cspF_asm_right_tac n *})?)
 *-----------------------------------------------------*)

ML_setup {*
    fun cspF_asm_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_asm_left_tac n),
         TRY (cspF_asm_right_tac n)])
*}

ML_setup {*
    fun cspF_step_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_step_left_tac n),
         TRY (cspF_step_right_tac n)])
*}

ML_setup {*
    fun cspF_light_step_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_light_step_left_tac n),
         TRY (cspF_light_step_right_tac n)])
*}

ML_setup {*
    fun cspF_dist_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_dist_left_tac n),
         TRY (cspF_dist_right_tac n)])
*}

ML_setup {*
    fun cspF_unwind_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_unwind_left_tac n),
         TRY (cspF_unwind_right_tac n)])
*}

ML_setup {*
    fun cspF_sort_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_sort_left_tac n),
         TRY (cspF_sort_right_tac n)])
*}

ML_setup {*
    fun cspF_simp_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_simp_left_tac n),
         TRY (cspF_simp_right_tac n)])
*}

end

lemmas cspF_all_dist: 

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

lemmas cspF_all_dist: 

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

lemmas cspF_choice_IF: 

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

lemmas cspF_choice_IF: 

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