Theory FNF_F_sf

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |               February 2006               |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory FNF_F_sf
imports FNF_F_sf_hide FNF_F_sf_par
        FNF_F_sf_ren  FNF_F_sf_seq
        FNF_F_sf_rest 
begin

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

         1. full sequentialisation
         2. 
         3. 

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

(*****************************************************************
                      small transformation
 *****************************************************************)

consts
  fsfF_Act_prefix ::
  "'a => ('p,'a) proc => ('p,'a) proc"               ("(1_ /->seq _)" [150,80] 80)
  fsfF_Ext_pre_choice ::
  "'a set => ('a => ('p,'a) proc) => ('p,'a) proc"   ("(1? :_ /->seq _)" [900,80] 80)

defs
  fsfF_Act_prefix_def :
    "a ->seq P == (? y:{a} -> P) [+] STOP"
  fsfF_Ext_pre_choice_def :
    "? :A ->seq Pf == (? :A -> Pf) [+] STOP"

syntax
  "@fsfF_Ext_pre_choice"  :: "pttrn => 'a set => ('p,'a) proc 
                => ('p,'a) proc"  ("(1? _:_ /->seq _)" [900,900,80] 80)
translations
  "? a:A ->seq P"  == "? :A ->seq (%a. P)"

(* a -> P *)

lemma fsfF_Act_prefix_in:
  "P : fsfF_proc ==> a ->seq P : fsfF_proc"
by (simp add: fsfF_Act_prefix_def fsfF_proc.intros)

lemma cspF_fsfF_Act_prefix_eqF:
  "a -> P =F a ->seq P"
apply (simp add: fsfF_Act_prefix_def)
apply (rule cspF_rw_right)
apply (rule cspF_Ext_choice_unit)
apply (rule cspF_Act_prefix_step)
done

(* ? :A -> Pf *)

lemma fsfF_Ext_pre_choice_in:
  "ALL a. Pf a : fsfF_proc ==> ? :A ->seq Pf : fsfF_proc"
by (simp add: fsfF_Ext_pre_choice_def fsfF_proc.intros)

lemma cspF_fsfF_Ext_pre_choice_eqF:
  "? :A -> Pf =F ? :A ->seq Pf"
apply (simp add: fsfF_Ext_pre_choice_def)
apply (rule cspF_rw_right)
apply (rule cspF_Ext_choice_unit)
apply (rule cspF_reflex)
done

(* IF b THEN P ELSE Q *)

lemma fsfF_IF_in:
  "[| P : fsfF_proc ; Q : fsfF_proc |]
   ==> (if b then P else Q) : fsfF_proc"
by (auto)

lemmas cspF_fsfF_IF_eqF = cspF_IF_split

(*===============================================================*
 |                                                               |
 |      definition of a function for full sequentialization      |
 |                     (no process name)                         |
 |                                                               |
 *===============================================================*)

consts
   prefsfF :: "('p,'a) proc => ('p,'a) proc"

primrec 
  "prefsfF(STOP)        = SSTOP"
  "prefsfF(SKIP)        = SSKIP"
  "prefsfF(DIV)         = SDIV"
  "prefsfF(a -> P)      = a ->seq (prefsfF P)"
  "prefsfF(? :A -> Pf)  = ? a:A ->seq (prefsfF (Pf a))"
  "prefsfF(P [+] Q)     = (prefsfF P) [+]seq (prefsfF Q)"
  "prefsfF(P |~| Q)     = (prefsfF P) |~|seq (prefsfF Q)"
  "prefsfF(!nat :N .. Pf) = !nat n:N ..seq prefsfF (Pf n)"
  "prefsfF(!set :Xs .. Pf) = !set X:Xs ..seq prefsfF (Pf X)"
  "prefsfF(IF b THEN P ELSE Q) = (if b then prefsfF(P) else prefsfF(Q))"
  "prefsfF(P |[X]| Q)   = (prefsfF P) |[X]|seq (prefsfF Q)"
  "prefsfF(P -- X)      = (prefsfF P) --seq X"
  "prefsfF(P [[r]])     = (prefsfF P) [[r]]seq"
  "prefsfF(P ;; Q)      = (prefsfF P) ;;seq (prefsfF Q)"
  "prefsfF(P |. n)      = (prefsfF P) |.seq n"
  "prefsfF($p)          = $p"

(*===============================================================*
            --- prefsfF P is fullly sequentialized ---
 *===============================================================*)

lemma prefsfF_in_lm: 
  "noPN P --> prefsfF P : fsfF_proc"
apply (induct_tac P)
apply (simp_all)
apply (simp add: fsfF_Act_prefix_in)
apply (simp add: fsfF_Ext_pre_choice_in)
apply (simp add: fsfF_Ext_choice_in)
apply (simp add: fsfF_Int_choice_in)
apply (simp add: fsfF_Rep_int_choice_nat_in)
apply (simp add: fsfF_Rep_int_choice_set_in)
apply (simp add: fsfF_Parallel_in)
apply (simp add: fsfF_Hiding_in)
apply (simp add: fsfF_Renaming_in)
apply (simp add: fsfF_Seq_compo_in)
apply (simp add: fsfF_Depth_rest_in)
done

lemma prefsfF_in: 
  "noPN P ==> prefsfF P : fsfF_proc"
by (simp add: prefsfF_in_lm)

(*===============================================================*
           --- prefsfF P is equal to P based on F ---
 *===============================================================*)

lemma cspF_prefsfF_eqF_lm:
  "noPN P --> P =F prefsfF P"
apply (induct_tac P)
apply (simp add: cspF_SSTOP_eqF)
apply (simp add: cspF_SSKIP_eqF)
apply (simp add: cspF_SDIV_eqF)

(* Act_prefix *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (simp add: cspF_fsfF_Act_prefix_eqF)

(* Ext_pre_choice *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (erule rev_all1E)
apply (drule_tac x="a" in spec)+
apply (simp_all)
apply (simp add: cspF_fsfF_Ext_pre_choice_eqF)

(* Ext_choice *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (simp add: cspF_fsfF_Ext_choice_eqF)

(* Int_choice *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (simp add: cspF_fsfF_Int_choice_eqF)

(* Rep_int_choice nat *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (erule rev_all1E)
apply (drule_tac x="n" in spec)+
apply (simp_all)
apply (simp add: cspF_fsfF_Rep_int_choice_eqF)

(* Rep_int_choice set *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (erule rev_all1E)
apply (drule_tac x="X" in spec)+
apply (simp_all)
apply (simp add: cspF_fsfF_Rep_int_choice_eqF)

(* IF *)
apply (intro conjI impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (rule cspF_IF)
apply (rule cspF_rw_left)
apply (rule cspF_IF)
apply (simp_all)

(* Parallel *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)

apply (simp add: cspF_fsfF_Parallel_eqF)

(* Hiding *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (simp add: cspF_fsfF_Hiding_eqF)

(* Renaming *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (simp add: cspF_fsfF_Renaming_eqF)

(* Seq_compo *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (simp add: cspF_fsfF_Seq_compo_eqF)

(* Depth_rest *)
apply (intro impI)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (simp add: cspF_fsfF_Depth_rest_eqF)
done

lemma cspF_prefsfF_eqF:
  "noPN P ==> P =F prefsfF P"
by (simp add: cspF_prefsfF_eqF_lm)

(*===============================================================*
 |                                                               |
 |      definition of a function for full sequentialization      |
 |                                                               |
 *===============================================================*)

consts
   fsfF :: "('p,'a) proc => ('p,'a) proc"

defs
   fsfF_def : "fsfF == (%P. prefsfF(rmPN(P)))"

(*===============================================================*
           theorem --- fsfF P is fullly sequentialized ---
 *===============================================================*)

theorem fsfF_in: 
  "fsfF P : fsfF_proc"
apply (simp add: fsfF_def)
apply (rule prefsfF_in)
apply (simp add: noPN_rmPN)
done

(*===============================================================*
           theorem --- fsfF P is equal to P based on F ---
 *===============================================================*)

lemma cspF_fsfF_eqF:
  "FPmode = CPOmode | FPmode = MIXmode ==>  P =F fsfF P"
apply (simp add: fsfF_def)
apply (rule cspF_rw_right)
apply (rule cspF_prefsfF_eqF[THEN cspF_sym])
apply (simp add: noPN_rmPN)
apply (rule cspF_rmPN_eqF)
apply (force)
done

end