Theory FNF_F_sf_int

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

theory FNF_F_sf_int = FNF_F_sf_def:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification rules are deleted in this theory file *)
(*       P (if Q then x else y) = ((Q --> P x) & (~ Q --> P y))        *)

declare split_if  [split del]

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

         1. full sequentialization for Rep_int_choice
         2. full sequentialization for Int_choice
         3. 

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

(*============================================================*
 |                                                            |
 |                      Rep_int_choice                        |
 |                                                            |
 *============================================================*)

consts
  fsfF_Rep_int_choice ::
  "'a selector set => ('a selector => 'a proc) => 'a proc"

defs
  fsfF_Rep_int_choice_def :
    "fsfF_Rep_int_choice C SPf == if (C = {}) then SDIV else !! :C .. SPf"

syntax
  "_fsfF_Rep_int_choice" :: 
      "'a selector set => ('a selector => 'a proc) => 'a proc"
                                     ("(1!! :_ ..seq /_)" [900,68] 68) 
  "@fsfF_Rep_int_choice":: 
      "pttrn => ('a selector) set => 'a proc => 'a proc"  
                               ("(1!! _:_ ..seq /_)" [900,900,68] 68)

translations
  "!! :C ..seq SPf"  == "fsfF_Rep_int_choice C SPf"
  "!! c:C ..seq SP"  == "!! :C ..seq (%c. SP)"

(*** for convenience ***)

consts
  fsfF_Rep_int_choice_fun :: "('b => ('a selector))
                               => 'b set => ('b => 'a proc) => 'a proc"
                                        ("(1!!<_> :_ ..seq /_)" [0,900,68] 68)
defs
  fsfF_Rep_int_choice_fun_def : 
        "!!<f> :X ..seq Pf == !! :(f ` X) ..seq (%x. (Pf ((inv f) x)))"

syntax
  "@fsfF_Rep_int_choice_fun":: 
  "('b => ('a selector)) => pttrn => 'b set => 'a proc => 'a proc"
                               ("(1!!<_> _:_ ..seq /_)" [0,900,900,68] 68)
translations
  "!!<f> x:X ..seq P"   == "!!<f> :X ..seq (%x. P)"

syntax
  "@fsfF_Rep_int_choice_fun_set" :: "('a set) set => ('a set => 'a proc) => 'a proc"
                                      ("(1!set :_ ..seq /_)" [900,68] 68)
  "@fsfF_Rep_int_choice_fun_nat" :: "nat set => (nat => 'a proc) => 'a proc"
                                      ("(1!nat :_ ..seq /_)" [900,68] 68)

translations
        "!set :Xs ..seq Pf" == "!!<sel_set> :Xs ..seq Pf"
        "!nat :N ..seq Pf" == "!!<sel_nat> :N ..seq Pf"

syntax
  "@fsfF_Rep_int_choice_set" :: 
       "pttrn => ('a set) set => ('a set => 'a proc) => 'a proc"
                                      ("(1!set _:_ ..seq /_)" [900,900,68] 68)
  "@fsfF_Rep_int_choice_nat" :: 
       "pttrn => nat set => (nat => 'a proc) => 'a proc"
                                      ("(1!nat _:_ ..seq /_)" [900,900,68] 68)

translations
    "!set X:Xs ..seq P" == "!set :Xs ..seq (%X. P)"
    "!nat n:N ..seq P"  == "!nat :N ..seq (%n. P)"

(* com *)

consts
  fsfF_Rep_int_choice_com :: "'a set => ('a => 'a proc) => 'a proc"
                                      ("(1! :_ ..seq /_)" [900,68] 68)
defs
  fsfF_Rep_int_choice_com_def:
     "! :A ..seq Pf == !set X:{{a} |a. a : A} ..seq Pf (contents(X))"

syntax
  "@fsfF_Rep_int_choice_com" :: 
      "pttrn => 'a set => ('a => 'a proc) => 'a proc"
                                      ("(1! _:_ ..seq /_)" [900,900,68] 68)
translations
    "! x:X ..seq P"    == "! :X ..seq (%x. P)"

(*------------------------------------------------------------*
 |                        in fsfF_proc                        |
 *------------------------------------------------------------*)

lemma fsfF_Rep_int_choice_in:
  "ALL c:C. SPf c : fsfF_proc ==> !! :C ..seq SPf : fsfF_proc"
apply (simp add: fsfF_Rep_int_choice_def)

 apply (simp split: split_if)
 apply (intro impI)

 apply (rule fsfF_procI)
 apply (simp)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)

lemma cspF_fsfF_Rep_int_choice_eqF:
  "!! :C .. SPf =F !! :C ..seq SPf"
apply (simp add: fsfF_Rep_int_choice_def)
apply (case_tac "C={}")
apply (tactic {* cspF_hsf_tac 1 *})
apply (rule cspF_SDIV_eqF)
done

(* =F also can be manually proven without using tactics. *)
(* we give the proof to show which laws are applied.     *)

lemma "!! :C .. SPf =F !! :C ..seq SPf"
apply (simp add: fsfF_Rep_int_choice_def)
apply (case_tac "C={}")
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice0_DIV)
apply (rule cspF_SDIV_eqF)

      (* C~={} *)
apply (simp)
done

lemmas cspF_fsfF_Rep_int_choice_eqF_sym = cspF_fsfF_Rep_int_choice_eqF[THEN cspF_sym]

(*============================================================*
 |                                                            |
 |                 convenient expressions                     |
 |                                                            |
 *============================================================*)

(*------------------------------------*
 |                 in                 |
 *------------------------------------*)

lemma fsfF_Rep_int_choice_fun_in:
  "[| inj f ; ALL x:X. SPf x : fsfF_proc |] ==>
    !!<f> :X ..seq SPf : fsfF_proc"
apply (insert fsfF_Rep_int_choice_in[of "(f ` X)" "(%x. SPf (inv f x))"])
apply (simp add: fsfF_Rep_int_choice_fun_def)
done

lemma fsfF_Rep_int_choice_com_in:
  "ALL x:X. SPf x : fsfF_proc ==>
       ! :X ..seq SPf : fsfF_proc"
apply (simp add: fsfF_Rep_int_choice_com_def)
apply (rule fsfF_Rep_int_choice_fun_in)
apply (auto)
done

lemma fsfF_Rep_int_choice_set_in:
  "ALL X:Xs. SPf X : fsfF_proc ==>
       !set :Xs ..seq SPf : fsfF_proc"
by (simp add: fsfF_Rep_int_choice_fun_in)

lemma fsfF_Rep_int_choice_nat_in:
  "ALL n:N. SPf n : fsfF_proc ==>
       !nat :N ..seq SPf : fsfF_proc"
by (simp add: fsfF_Rep_int_choice_fun_in)

(*------------------------------------*
 |                 eqF                |
 *------------------------------------*)

lemma cspF_fsfF_Rep_int_choice_fun_eqF:
  "inj f ==>
   !!<f> :X .. SPf =F !!<f> :X ..seq SPf"
apply (insert cspF_fsfF_Rep_int_choice_eqF[of "(f ` X)" "(%x. SPf (inv f x))"])
apply (simp add: Rep_int_choice_fun_def)
apply (simp add: fsfF_Rep_int_choice_fun_def)
done

lemma cspF_fsfF_Rep_int_choice_com_eqF:
  "! :X .. SPf =F ! :X ..seq SPf"
apply (simp add: fsfF_Rep_int_choice_com_def)
apply (simp add: Rep_int_choice_com_def)
apply (simp add: cspF_fsfF_Rep_int_choice_fun_eqF)
done

lemma cspF_fsfF_Rep_int_choice_set_eqF:
  "!set :Xs .. SPf =F !set :Xs ..seq SPf"
by (simp add: cspF_fsfF_Rep_int_choice_fun_eqF)

lemma cspF_fsfF_Rep_int_choice_nat_eqF:
  "!nat :N .. SPf =F !nat :N ..seq SPf"
by (simp add: cspF_fsfF_Rep_int_choice_fun_eqF)

(*============================================================*
 |                                                            |
 |                        Int_choice                          |
 |                                                            |
 *============================================================*)

consts
  fsfF_Int_choice ::
  "'a proc => 'a proc => 'a proc"    ("(1_ /|~|seq _)" [64,65] 64)

defs
  fsfF_Int_choice_def :
    "P |~|seq Q ==
           !! :{sel_nat 0, sel_nat (Suc 0)} ..
               (%x. if (x = sel_nat 0) then P else Q)"

(*------------------------------------------------------------*
 |                        in fsfF_proc                        |
 *------------------------------------------------------------*)

lemma fsfF_Int_choice_in:
  "[| P : fsfF_proc ; Q : fsfF_proc |] ==>
   P |~|seq Q : fsfF_proc"
apply (simp add: fsfF_Int_choice_def)
apply (rule fsfF_proc_int)
apply (auto)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)

lemma cspF_fsfF_Int_choice_eqF:
  "P |~| Q =F P |~|seq Q"
apply (simp add: fsfF_Int_choice_def)
apply (rule cspF_rw_left)
apply (rule cspF_Int_choice_to_Rep)
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_IF_split)
apply (auto)
done

(****************** to add them again ******************)

declare split_if    [split]
declare disj_not1   [simp]

end