Theory FNF_F_sf

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

theory FNF_F_sf = FNF_F_sf_hide + FNF_F_sf_par
                + FNF_F_sf_ren  + FNF_F_sf_seq
                + FNF_F_sf_rest :

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

         1. full sequentialisation
         2. 
         3. 

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

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

consts
  fsfF_Act_prefix ::
  "'a => 'a proc => 'a proc"               ("(1_ /->seq _)" [150,80] 80)
  fsfF_Ext_pre_choice ::
  "'a set => ('a => 'a proc) => '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 => 'a proc 
                => '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
 *===============================================================*)

consts
   fsfF :: "'a proc => 'a proc"

primrec 
  "fsfF(STOP)        = SSTOP"
  "fsfF(SKIP)        = SSKIP"
  "fsfF(DIV)         = SDIV"
  "fsfF(a -> P)      = a ->seq (fsfF P)"
  "fsfF(? :A -> Pf)  = ? a:A ->seq (fsfF (Pf a))"
  "fsfF(P [+] Q)     = (fsfF P) [+]seq (fsfF Q)"
  "fsfF(P |~| Q)     = (fsfF P) |~|seq (fsfF Q)"
  "fsfF(!! :C .. Pf) = !! c:C ..seq fsfF (Pf c)"
  "fsfF(IF b THEN P ELSE Q) = (if b then fsfF(P) else fsfF(Q))"
  "fsfF(P |[X]| Q)   = (fsfF P) |[X]|seq (fsfF Q)"
  "fsfF(P -- X)      = (fsfF P) --seq X"
  "fsfF(P [[r]])     = (fsfF P) [[r]]seq"
  "fsfF(P ;; Q)      = (fsfF P) ;;seq (fsfF Q)"
  "fsfF(P |. n)      = (fsfF P) |.seq n"

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

theorem fsfF_in: "fsfF 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_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

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

theorem cspF_fsfF_eqF: "P =F fsfF 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 (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (assumption)
apply (simp add: cspF_fsfF_Act_prefix_eqF)

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

(* Ext_choice *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (assumption)
apply (assumption)
apply (simp add: cspF_fsfF_Ext_choice_eqF)

(* Int_choice *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (assumption)
apply (assumption)
apply (simp add: cspF_fsfF_Int_choice_eqF)

(* Rep_int_choice *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (erule rev_all1E)
apply (drule_tac x="c" in spec)
apply (assumption)
apply (simp add: cspF_fsfF_Rep_int_choice_eqF)

(* IF *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (assumption)
apply (assumption)
apply (simp add: cspF_fsfF_IF_eqF)

(* Parallel *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (assumption)
apply (assumption)
apply (simp add: cspF_fsfF_Parallel_eqF)

(* Hiding *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (assumption)
apply (simp add: cspF_fsfF_Hiding_eqF)

(* Renaming *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (assumption)
apply (simp add: cspF_fsfF_Renaming_eqF)

(* Seq_compo *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (assumption)
apply (assumption)
apply (simp add: cspF_fsfF_Seq_compo_eqF)

(* Depth_rest *)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (assumption)
apply (simp)
apply (simp add: cspF_fsfF_Depth_rest_eqF)
done

end