Theory CSP_T_tactic

           (*-------------------------------------------*
            |        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_tr_flag_left              = thms "cspT_tr_flag_left" ;
    val CSPT_tr_flag_right             = thms "cspT_tr_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
*}

(*** refine_with ***)

(* left *)

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

       (EVERY [ resolve_tac CSPT_tr_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
*}

(* right *)

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

       (EVERY [ resolve_tac CSPT_tr_flag_right 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])
*}

(*** refine_with ***)

ML_setup {*
fun cspT_refine_with_left_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_tr_flag_left n,
    cspT_refine_with_left_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])
*}

(*** refine_with ***)

ML_setup {*
fun cspT_refine_with_right_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPT_tr_flag_right n,
    cspT_refine_with_right_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)])
*}

(*** refine_with ***)

ML_setup {*
    fun cspT_refine_with_tac a n = 
      CHANGED (
       EVERY
        [TRY (cspT_refine_with_left_tac a n),
         TRY (cspT_refine_with_right_tac a 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)])
*}

(*-----------------------------------------------------*
      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_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