Theory CSP_tactic

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

theory CSP_tactic = CSP_rule_rw: 
           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_tactic = CSP_rule_rw:

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

         1. tactic
         2.
         3. 
         4. 

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

lemmas csp_ss_def = Int_pre_choice_def Send_prefix_def Nondet_send_prefix_def
                    Rec_prefix_def Rep_int_choice_fun_def

lemmas csp_Conditional_simp_rw_right    = csp_Conditional_rw_right   csp_simp_rw_right
lemmas csp_Conditional_simp_rw_left     = csp_Conditional_rw_left    csp_simp_rw_left
lemmas csp_dist_both_rw_right  = csp_dist_rw_right csp_Rep_dist_rw_right
lemmas csp_dist_both_rw_left   = csp_dist_rw_left  csp_Rep_dist_rw_left

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

ML_setup {*
    val CSP_reflex                    = thms "csp_reflex" ;
    val CSP_rm_head                   = thms "csp_rm_head" ;
    val CSP_ss_def                    = thms "csp_ss_def" ;

    val CSP_rw_flag_left              = thms "csp_rw_flag_left" ;
    val CSP_tr_flag_left              = thms "csp_tr_flag_left" ;
    val CSP_Conditional_simp_rw_left  = thms "csp_Conditional_simp_rw_left" ;
    val CSP_free_decompo_left         = thms "csp_free_decompo_left" ;
    val CSP_free_decompo_flag_left    = thms "csp_free_decompo_flag_left" ;
    val CSP_step_rw_left              = thms "csp_step_rw_left" ;
    val CSP_light_step_rw_left        = thms "csp_light_step_rw_left" ;
    val CSP_SKIP_rw_left              = thms "csp_SKIP_rw_left" ;
    val CSP_dist_both_rw_left         = thms "csp_dist_both_rw_left" ;
    val CSP_unwind_rw_left            = thms "csp_unwind_rw_left" ;

    val CSP_rw_flag_right             = thms "csp_rw_flag_right" ;
    val CSP_tr_flag_right             = thms "csp_tr_flag_right" ;
    val CSP_free_decompo_right        = thms "csp_free_decompo_right" ;
    val CSP_free_decompo_flag_right   = thms "csp_free_decompo_flag_right" ;
    val CSP_unwind_rw_right           = thms "csp_unwind_rw_right" ;

    val RM_Not_Decompo_Flag           = thms "rm_Not_Decompo_Flag";
    val RM_Not_Decompo_Flag_True      = thms "rm_Not_Decompo_Flag_True";
*}

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

(*-----------------------------------------------------*
      apply (tactic {* csp_hnf_left_tac 1 *})
                      is equal to
      apply (rule csp_tr_flag_left ,
             ((simp 
             | simp add: csp_Conditional_simp_rw_left
             | simp add: csp_SKIP_rw_left
             | simp add: csp_step_rw_left
             | simp add: csp_dist_both_rw_left
             | simp add: csp_unwind_rw_left 
             | (rule rm_Not_Decompo_Flag, rule csp_reflex)
             | rule csp_free_decompo_flag_left
             | rule csp_reflex)+)? ,
             (rule rm_Not_Decompo_Flag | rule rm_Not_Decompo_Flag_True))
 *-----------------------------------------------------*)

(*** Head Normal Form ***)

ML_setup {*
fun csp_hnf_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_SKIP_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_step_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_dist_both_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_unwind_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** step ***)

ML_setup {*
fun csp_step_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_SKIP_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_step_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** light step ***)

ML_setup {*
fun csp_light_step_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_SKIP_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_light_step_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** dist ***)

ML_setup {*
fun csp_dist_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_dist_both_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** unwind ***)

ML_setup {*
fun csp_unwind_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_unwind_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** simp ***)

ML_setup {*
fun csp_simp_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** simp add ***)

ML_setup {*
fun csp_simp_add_left_tac add n =
let val ADD = thms add 
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset () addsimps ADD) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** simp del ***)

ML_setup {*
fun csp_simp_del_left_tac del n =
let val DEL = thms del
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset () delsimps DEL) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left 
                                               delsimps DEL) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** simp add del ***)

ML_setup {*
fun csp_simp_add_del_left_tac add del n =
let val ADD = thms add
    val DEL = thms del
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset () addsimps ADD delsimps DEL) n)) ,
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left 
                                               delsimps DEL) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** rule ***)

ML_setup {*
fun csp_rule_left_tac a n =
let val A = thms a
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (resolve_tac A n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** assumption ***)

ML_setup {*
fun csp_asm_left_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_left n,

    REPEAT (
     FIRST 
      [(CHANGED (assume_tac n)) ,
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

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

(*** Head Normal Form ***)

ML_setup {*
fun csp_hnf_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_SKIP_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_step_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_dist_both_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_unwind_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** step ***)

ML_setup {*
fun csp_step_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_SKIP_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_step_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** light step ***)

ML_setup {*
fun csp_light_step_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_SKIP_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_light_step_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** dist ***)

ML_setup {*
fun csp_dist_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_dist_both_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** unwind ***)

ML_setup {*
fun csp_unwind_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_unwind_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** simp ***)

ML_setup {*
fun csp_simp_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (Asm_full_simp_tac n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

(*** simp add ***)

ML_setup {*
fun csp_simp_add_right_tac add n =
let val ADD = thms add 
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset () addsimps ADD) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** simp del ***)

ML_setup {*
fun csp_simp_del_right_tac del n =
let val DEL = thms del
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset () delsimps DEL) n)),
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left 
                                               delsimps DEL) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** simp add del ***)

ML_setup {*
fun csp_simp_add_del_right_tac add del n =
let val ADD = thms add
    val DEL = thms del
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (asm_full_simp_tac (simpset () addsimps ADD delsimps DEL) n)) ,
       (CHANGED (asm_full_simp_tac (simpset () addsimps CSP_Conditional_simp_rw_left 
                                               delsimps DEL) n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** rule ***)

ML_setup {*
fun csp_rule_right_tac a n =
let val A = thms a
in
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (resolve_tac A n)),
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
end
*}

(*** assumption ***)

ML_setup {*
fun csp_asm_right_tac n =
 CHANGED (
  EVERY
   [resolve_tac CSP_rw_flag_right n,

    REPEAT (
     FIRST 
      [(CHANGED (assume_tac n)) ,
       (EVERY [(resolve_tac RM_Not_Decompo_Flag n), (resolve_tac CSP_reflex n)]),
       (resolve_tac CSP_free_decompo_flag_left n) ,
       (resolve_tac CSP_reflex n)]),

    FIRST[resolve_tac RM_Not_Decompo_Flag n, resolve_tac RM_Not_Decompo_Flag_True n] ])
*}

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

(*-----------------------------------------------------*
      apply (tactic {* csp_hnf_tac 1 *})
                      is equal to
      apply ((tactic {* csp_hnf_left_tac 1 *})+)? ,
            ((tactic {* csp_hnf_right_tac 1 *})+)?
 *-----------------------------------------------------*)

ML_setup {*
    fun csp_hnf_tac n = 
      CHANGED (
       EVERY
        [REPEAT (csp_hnf_left_tac n),
         REPEAT (csp_hnf_right_tac n)])
*}

ML_setup {*
    fun csp_step_tac n = 
      CHANGED (
       EVERY
        [REPEAT (csp_step_left_tac n),
         REPEAT (csp_step_right_tac n)])
*}

ML_setup {*
    fun csp_light_step_tac n = 
      CHANGED (
       EVERY
        [REPEAT (csp_light_step_left_tac n),
         REPEAT (csp_light_step_right_tac n)])
*}

ML_setup {*
    fun csp_dist_tac n = 
      CHANGED (
       EVERY
        [REPEAT (csp_dist_left_tac n),
         REPEAT (csp_dist_right_tac n)])
*}

ML_setup {*
    fun csp_unwind_tac n = 
      CHANGED (
       EVERY
        [REPEAT (csp_unwind_left_tac n),
         REPEAT (csp_unwind_right_tac n)])
*}

ML_setup {*
    fun csp_simp_tac n = 
      CHANGED (
       EVERY
        [REPEAT (csp_simp_left_tac n),
         REPEAT (csp_simp_right_tac n)])
*}

ML_setup {*
    fun csp_simp_add_tac add n = 
      CHANGED (
       EVERY
        [REPEAT (csp_simp_add_left_tac add n),
         REPEAT (csp_simp_add_right_tac add n)])
*}

ML_setup {*
    fun csp_simp_del_tac del n = 
      CHANGED (
       EVERY
        [REPEAT (csp_simp_del_left_tac del n),
         REPEAT (csp_simp_del_right_tac del n)])
*}

(*--------------------------------------------------------------------*
      apply (tactic {* csp_simp_add_del_tac add del 1 *})
                      is equal to
      apply ((tactic {* csp_simp_add_del_left_tac add del 1 *})+)? ,
            ((tactic {* csp_simp_add_del_right_tac add del 1 *})+)?
 *--------------------------------------------------------------------*)

ML_setup {*
    fun csp_simp_add_del_tac add del n = 
      CHANGED (
       EVERY
        [REPEAT (csp_simp_add_del_left_tac add del n),
         REPEAT (csp_simp_add_del_right_tac add del n)])
*}

(*-----------------------------------------------------*
      apply (tactic {* csp_rule_tac a 1 *})
                      is equal to
      apply ((tactic {* csp_rule_left_tac a 1 *})+)? ,
            ((tactic {* csp_rule_right_tac a 1 *})+)?
 *-----------------------------------------------------*)

ML_setup {*
    fun csp_rule_tac a n = 
      CHANGED (
       EVERY
        [REPEAT (csp_rule_left_tac a n),
         REPEAT (csp_rule_right_tac a n)])
*}

(*-----------------------------------------------------*
      apply (tactic {* csp_asm_tac 1 *})
                      is equal to
      apply ((tactic {* csp_asm_left_tac 1 *})+)? ,
            ((tactic {* csp_asm_right_tac 1 *})+)?
 *-----------------------------------------------------*)

ML_setup {*
    fun csp_asm_tac n = 
      CHANGED (
       EVERY
        [REPEAT (csp_asm_left_tac n),
         REPEAT (csp_asm_right_tac n)])
*}

end

lemmas csp_ss_def: 

  ! :X -> Pf == ! x:X .. x -> Pf x
  a ! x -> P == a x -> P
  Nondet_send_prefix f X Pf == ! x:(f ` X) -> Pf (inv f x)
  Rec_prefix f X Pf == ? x:(f ` X) -> Pf (inv f x)
  Rep_int_choice_fun f X Pf == ! x:(f ` X) .. Pf (inv f x)

lemmas csp_Conditional_simp_rw_right: 

  (R0 =F 
   LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) =
  (R0 =F 
   LET:fp_1 df_1 IN P_1)
  (R0 =F 
   LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) =
  (R0 =F 
   LET:fp_1 df_1 IN Q_1)
  (R0 <=F 
   LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN P_1)
  (R0 <=F 
   LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN Q_1)
  (R0 =F 
   LET:fp_1 df_1 IN DIV) =
  (R0 =F 
   LET:fp_1 df_1 IN ! x:{} .. DIV)
  (R0 =F 
   LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) =
  (R0 =F 
   LET:fp_1 df_1 IN Pf_1 a_1)
  
  LET:fp_1 df_1 IN P_1 =F 
  LET:fp_1 df_1 IN Q_1
  ==> (R0 =F 
       LET:fp_1 df_1 IN P_1 |~| Q_1) =
      (R0 =F 
       LET:fp_1 df_1 IN P_1)
  (R0 <=F 
   LET:fp_1 df_1 IN DIV) =
  (R0 <=F 
   LET:fp_1 df_1 IN ! x:{} .. DIV)
  (R0 <=F 
   LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN Pf_1 a_1)
  
  LET:fp_1 df_1 IN P_1 =F 
  LET:fp_1 df_1 IN Q_1
  ==> (R0 <=F 
       LET:fp_1 df_1 IN P_1 |~| Q_1) =
      (R0 <=F 
       LET:fp_1 df_1 IN P_1)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (R0 =F 
       LET:fp_1 df_1 IN Q_1 [+] P_1) =
      (R0 =F 
       LET:fp_1 df_1 IN P_1)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (R0 =F 
       LET:fp_1 df_1 IN P_1 [+] Q_1) =
      (R0 =F 
       LET:fp_1 df_1 IN P_1)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (R0 <=F 
       LET:fp_1 df_1 IN Q_1 [+] P_1) =
      (R0 <=F 
       LET:fp_1 df_1 IN P_1)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (R0 <=F 
       LET:fp_1 df_1 IN P_1 [+] Q_1) =
      (R0 <=F 
       LET:fp_1 df_1 IN P_1)
  [| 
     LET:fp_1 df_1 IN P1_1 =F 
     LET:fp_1 df_1 IN STOP;
     
     LET:fp_1 df_1 IN P2_1 =F 
     LET:fp_1 df_1 IN STOP |]
  ==> (R0 =F 
       LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) =
      (R0 =F 
       LET:fp_1 df_1 IN Q_1)
  [| 
     LET:fp_1 df_1 IN P1_1 =F 
     LET:fp_1 df_1 IN STOP;
     
     LET:fp_1 df_1 IN P2_1 =F 
     LET:fp_1 df_1 IN STOP |]
  ==> (R0 <=F 
       LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) =
      (R0 <=F 
       LET:fp_1 df_1 IN Q_1)

lemmas csp_Conditional_simp_rw_left: 

  (
   LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 =F R0) =
  (
   LET:fp_1 df_1 IN P_1 =F R0)
  (
   LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 =F R0) =
  (
   LET:fp_1 df_1 IN Q_1 =F R0)
  (
   LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 <=F R0) =
  (
   LET:fp_1 df_1 IN P_1 <=F R0)
  (
   LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 <=F R0) =
  (
   LET:fp_1 df_1 IN Q_1 <=F R0)
  (
   LET:fp_1 df_1 IN DIV =F R0) =
  (
   LET:fp_1 df_1 IN ! x:{} .. DIV =F R0)
  (
   LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 =F R0) =
  (
   LET:fp_1 df_1 IN Pf_1 a_1 =F R0)
  
  LET:fp_1 df_1 IN P_1 =F 
  LET:fp_1 df_1 IN Q_1
  ==> (
       LET:fp_1 df_1 IN P_1 |~| Q_1 =F R0) =
      (
       LET:fp_1 df_1 IN P_1 =F R0)
  (
   LET:fp_1 df_1 IN DIV <=F R0) =
  (
   LET:fp_1 df_1 IN ! x:{} .. DIV <=F R0)
  (
   LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 <=F R0) =
  (
   LET:fp_1 df_1 IN Pf_1 a_1 <=F R0)
  
  LET:fp_1 df_1 IN P_1 =F 
  LET:fp_1 df_1 IN Q_1
  ==> (
       LET:fp_1 df_1 IN P_1 |~| Q_1 <=F R0) =
      (
       LET:fp_1 df_1 IN P_1 <=F R0)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (
       LET:fp_1 df_1 IN Q_1 [+] P_1 =F R0) =
      (
       LET:fp_1 df_1 IN P_1 =F R0)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (
       LET:fp_1 df_1 IN P_1 [+] Q_1 =F R0) =
      (
       LET:fp_1 df_1 IN P_1 =F R0)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (
       LET:fp_1 df_1 IN Q_1 [+] P_1 <=F R0) =
      (
       LET:fp_1 df_1 IN P_1 <=F R0)
  
  LET:fp_1 df_1 IN Q_1 =F 
  LET:fp_1 df_1 IN STOP
  ==> (
       LET:fp_1 df_1 IN P_1 [+] Q_1 <=F R0) =
      (
       LET:fp_1 df_1 IN P_1 <=F R0)
  [| 
     LET:fp_1 df_1 IN P1_1 =F 
     LET:fp_1 df_1 IN STOP;
     
     LET:fp_1 df_1 IN P2_1 =F 
     LET:fp_1 df_1 IN STOP |]
  ==> (
       LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) =
      (
       LET:fp_1 df_1 IN Q_1 =F R0)
  [| 
     LET:fp_1 df_1 IN P1_1 =F 
     LET:fp_1 df_1 IN STOP;
     
     LET:fp_1 df_1 IN P2_1 =F 
     LET:fp_1 df_1 IN STOP |]
  ==> (
       LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) =
      (
       LET:fp_1 df_1 IN Q_1 <=F R0)

lemmas csp_dist_both_rw_right: 

  (R0 =F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) =
  (R0 =F 
   LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
  (R0 =F 
   LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) =
  (R0 =F 
   LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
  (R0 =F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) =
  (R0 =F 
   LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
  (R0 =F 
   LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) =
  (R0 =F 
   LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
  (R0 =F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) =
  (R0 =F 
   LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
  (R0 =F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) =
  (R0 =F 
   LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
  (R0 =F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) =
  (R0 =F 
   LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
  (R0 <=F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
  (R0 <=F 
   LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) =
  (R0 <=F 
   LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
  (R0 <=F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
  (R0 <=F 
   LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) =
  (R0 <=F 
   LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
  (R0 <=F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
  (R0 <=F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) =
  (R0 <=F 
   LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
  (R0 <=F 
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
  X_1 ≠ {}
  ==> (R0 =F 
       LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) =
      (R0 =F 
       LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
  X_1 ≠ {}
  ==> (R0 =F 
       LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) =
      (R0 =F 
       LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
  Y_1 ≠ {}
  ==> (R0 =F 
       LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) =
      (R0 =F 
       LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
  Y_1 ≠ {}
  ==> (R0 =F 
       LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) =
      (R0 =F 
       LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
  (R0 =F 
   LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) =
  (R0 =F 
   LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
  (R0 =F 
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) =
  (R0 =F 
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
  (R0 =F 
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) =
  (R0 =F 
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)
  X_1 ≠ {}
  ==> (R0 <=F 
       LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) =
      (R0 <=F 
       LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
  X_1 ≠ {}
  ==> (R0 <=F 
       LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) =
      (R0 <=F 
       LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
  Y_1 ≠ {}
  ==> (R0 <=F 
       LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) =
      (R0 <=F 
       LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
  Y_1 ≠ {}
  ==> (R0 <=F 
       LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) =
      (R0 <=F 
       LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
  (R0 <=F 
   LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
  (R0 <=F 
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) =
  (R0 <=F 
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
  (R0 <=F 
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) =
  (R0 <=F 
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)

lemmas csp_dist_both_rw_left: 

  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) =
  (
   LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 =F R0)
  (
   LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) =F R0) =
  (
   LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 =F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 =F R0) =
  (
   LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 =F R0)
  (
   LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) =F R0) =
  (
   LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 =F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 =F R0) =
  (
   LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 =F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] =F R0) =
  (
   LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] =F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 =F R0) =
  (
   LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 =F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) =
  (
   LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 <=F R0)
  (
   LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) <=F R0) =
  (
   LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 <=F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 <=F R0) =
  (
   LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 <=F R0)
  (
   LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) <=F R0) =
  (
   LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 <=F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 <=F R0) =
  (
   LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 <=F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] <=F R0) =
  (
   LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] <=F R0)
  (
   LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 <=F R0) =
  (
   LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 <=F R0)
  X_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 =F R0) =
      (
       LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 =F R0)
  X_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) =F R0) =
      (
       LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x =F R0)
  Y_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 =F R0) =
      (
       LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 =F R0)
  Y_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) =F R0) =
      (
       LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x =F R0)
  (
   LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 =F R0) =
  (
   LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 =F R0)
  (
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] =F R0) =
  (
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] =F R0)
  (
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 =F R0) =
  (
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 =F R0)
  X_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 <=F R0) =
      (
       LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 <=F R0)
  X_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) <=F R0) =
      (
       LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x <=F R0)
  Y_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 <=F R0) =
      (
       LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 <=F R0)
  Y_1 ≠ {}
  ==> (
       LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) <=F R0) =
      (
       LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x <=F R0)
  (
   LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 <=F R0) =
  (
   LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 <=F R0)
  (
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] <=F R0) =
  (
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] <=F R0)
  (
   LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 <=F R0) =
  (
   LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 <=F R0)