Theory CSP_F_tactic

           (*-------------------------------------------*
            |        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)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2008         |
            |                   June 2008  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_tactic
imports CSP_F_law CSP_F_law_etc
begin

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

         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 {*
    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_tr_flag_left              = thms "cspF_tr_flag_left" ;
    val CSPF_tr_flag_right             = thms "cspF_tr_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_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 {*
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 ]]),

       (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 {*
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
*}

(*** refine_with ***)

(* left *)

ML {*
    val CSPF_tr_flag_left              = thms "cspF_tr_flag_left" ;
    val CSPF_tr_flag_right             = thms "cspF_tr_flag_right" ;
*}

ML {*
fun cspF_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 CSPF_tr_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
*}

(* right *)

ML {*
fun cspF_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 CSPF_tr_flag_right 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 {*
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 {*
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 {*
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 {*
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 {*
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 ]]),

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

(*** simp_with ***)

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

(*** refine_with ***)

ML {*
fun cspF_refine_with_left_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_tr_flag_left n,
    cspF_refine_with_left_main_tac a n])
*}

(*** assumption ***)

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

(*** step ***)

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

(*** light step ***)

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

(*** dist ***)

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

(*** unwind ***)

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

(*** sort ***)

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

(*** simp ***)

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

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

(*** hsf ***)

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

(*** simp_with ***)

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

(*** refine_with ***)

ML {*
fun cspF_refine_with_right_tac a n =
 CHANGED (
  EVERY
   [resolve_tac CSPF_tr_flag_right n,
    cspF_refine_with_right_main_tac a n])
*}

(*** assumption ***)

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

(*** step ***)

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

(*** light step ***)

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

(*** dist ***)

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

(*** unwind ***)

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

(*** sort ***)

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

(*** simp ***)

ML {*
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 {*
    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 {*
    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)])
*}

(*** refine_with ***)

ML {*
    fun cspF_refine_with_tac a n = 
      CHANGED (
       EVERY
        [TRY (cspF_refine_with_left_tac a n),
         TRY (cspF_refine_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 {*
    fun cspF_asm_tac n = 
      CHANGED (
       EVERY
        [TRY (cspF_asm_left_tac n),
         TRY (cspF_asm_right_tac n)])
*}

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

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

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

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

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

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

end