Theory FNF_F_nf_int

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

theory FNF_F_nf_int = FNF_F_nf_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 sequentialisation for Rep_int_choice
         2. 
         3. 

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

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

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

  fnfF_Rep_int_choice ::
  "nat => 'a selector set => ('a selector => 'a proc) => 'a proc"

defs
  fnfF_Rep_int_choice_step_def:
    "fnfF_Rep_int_choice_step == (%X Af Ysf Pf Qf. 
  ((? :(Union {Af x |x. x:X}) -> Pf)
    [+] (if (EX x:X. Qf x = SKIP) then SKIP else DIV))
   |~| !set Y:(fnfF_set_completion (Union {Af x |x. x:X})
                                   (Union {Ysf x |x. x : X})) .. (? a:Y -> DIV))"

primrec
  "fnfF_Rep_int_choice 0 = (%X SPf. NDIV)"

  "fnfF_Rep_int_choice (Suc n) = (%C SPf. 
   if (ALL c:C. SPf c : fnfF_proc) 
   then
   fnfF_Rep_int_choice_step C 
      (%c. (fnfF_A (SPf c)))
      (%c. (fnfF_Ys (SPf c)))
      (%a. (if a:Union {fnfF_A (SPf c) |c. c : C}
            then fnfF_Rep_int_choice n {c : C. a : (fnfF_A (SPf c))}
                                       (%c. (fnfF_Pf (SPf c) a))
            else DIV))
      (%c. (fnfF_Q (SPf c)))
   else 
      ((!! :C .. SPf) |. Suc n))"

syntax
  "_fnfF_Rep_int_choice" :: 
      "'a selector set => nat => ('a selector => 'a proc) => 'a proc"
                                               ("(1!! :_ ..[_] /_)" [900,0,68] 68) 
  "@fnfF_Rep_int_choice":: 
      "pttrn => ('a selector) set => nat => 'a proc => 'a proc"  
                               ("(1!! _:_ ..[_] /_)" [900,900,0,68] 68)

translations
  "!! :C ..[n] SPf"  == "fnfF_Rep_int_choice n C SPf"
  "!! c:C ..[n] P"   == "!! :C ..[n] (%c. P)"

(*** for convenience ***)

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

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

syntax
  "@fnfF_Rep_int_choice_fun_set" :: "('a set) set => nat => ('a set => 'a proc) => 'a proc"
                                      ("(1!set :_ ..[_] /_)" [900,0,68] 68)
  "@fnfF_Rep_int_choice_fun_nat" :: "nat set => nat => (nat => 'a proc) => 'a proc"
                                      ("(1!nat :_ ..[_] /_)" [900,0,68] 68)

translations
        "!set :Xs ..[n] Pf" == "!!<sel_set> :Xs ..[n] Pf"
        "!nat :N ..[n] Pf" == "!!<sel_nat> :N ..[n] Pf"

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

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

(* com *)

consts
  fnfF_Rep_int_choice_com :: "'a set => nat => ('a => 'a proc) => 'a proc"
                                      ("(1! :_ ..[_] /_)" [900,0,68] 68)
defs
  fnfF_Rep_int_choice_com_def:
     "! :A ..[n] Pf == !set X:{{a} |a. a : A} ..[n] Pf (contents(X))"

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

declare fnfF_Rep_int_choice.simps [simp del]

(*===========================================================*
 |                      in fnfF_rest                         |
 *===========================================================*)

lemma fnfF_Rep_int_choice_in_lm:
  "ALL C SPf.
   (ALL c:C. SPf c : fnfF_proc) -->
    !! :C ..[n] SPf : fnfF_proc"
apply (induct_tac n)
apply (simp add: fnfF_Rep_int_choice.simps)

apply (intro impI allI)
apply (simp add: fnfF_Rep_int_choice.simps)
apply (simp add: fnfF_Rep_int_choice_step_def)
apply (rule fnfF_proc.intros)

(* set *)
apply (rule allI)
apply (simp)
apply (case_tac "EX x. (EX xa. x = fnfF_A (SPf xa) & xa : C) & a : x")
apply (simp)
apply (drule_tac x="{c : C. a : fnfF_A (SPf c)}" in spec)
apply (drule_tac x="(%c. fnfF_Pf (SPf c) a)" in spec)
apply (drule mp)
apply (rule ballI)
apply (simp)
apply (elim conjE exE bexE)
apply (simp)

apply (rule fnfF_Pf_A)
apply (simp)
apply (simp)
apply (simp)

apply (simp (no_asm_simp))
apply (simp)

 apply (rule fnfF_set_completion_Union_subset)
 apply (rule subsetI)
 apply (simp)
 apply (elim conjE exE bexE)
 apply (simp)
 apply (drule_tac x="xa" in bspec, simp)
 apply (erule fnfF_proc.elims)
 apply (simp)
 apply (rule_tac x="fnfF_A (SPf xa)" in exI)
 apply (simp)
 apply (rule conjI)
 apply (rule_tac x="xa" in exI)
 apply (simp)
 apply (auto)
  apply (case_tac "EX x:C. fnfF_Q (SPf x) = SKIP")
  apply (simp_all)
done

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

lemma fnfF_Rep_int_choice_in:
  "(ALL c:C. SPf c : fnfF_proc) ==>
    !! :C ..[n] SPf : fnfF_proc"
apply (simp add: fnfF_Rep_int_choice_in_lm)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)
(*-----------------------------------------*
 |    convenient lemma for subexpresions   |
 *-----------------------------------------*)

lemma fnfF_Rep_int_choice_step_subexp:
  "[| ALL a:(Union {Af2 c |c. c:C}). Pf1 a =F Pf2 a ;
      ALL c:C. Af1 c = Af2 c ; 
      ALL c:C. Ysf1 c = Ysf2 c ; 
      ALL c:C. Qf1 c = Qf2 c ;
      ALL c:C. Union (Ysf2 c) <= (Af2 c) |]
   ==>
      fnfF_Rep_int_choice_step C Af1 Ysf1 Pf1 Qf1
   =F fnfF_Rep_int_choice_step C Af2 Ysf2 Pf2 Qf2"
apply (simp add: fnfF_Rep_int_choice_step_def)

apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_decompo)

(* 1 *)
apply (subgoal_tac
  "{Af1 c |c. c : C} = {Af2 c |c. c : C}", simp)
apply (blast)

(* 2 *)
 apply (simp)
 apply (elim conjE exE)
 apply (simp)
 apply (drule_tac x="Af2 xa" in spec)
 apply (drule mp)
 apply (rule_tac x="xa" in exI)
 apply (simp)
 apply (simp)

(* 3 *)
apply (simp)

(* 4 *)
apply (rule cspF_decompo)
apply (subgoal_tac
  "{Af1 c |c. c : C} = {Af2 c |c. c : C}")
apply (subgoal_tac
  "{Ysf1 c |c. c : C} = {Ysf2 c |c. c : C}")
apply (simp)
apply (erule rem_asmE)
apply (blast)
apply (erule rem_asmE)
apply (blast)
apply (simp)
done

(*------------------------------------*
 |         one step equality          |
 *------------------------------------*)

lemma cspF_fnfF_Rep_int_choice_one_step:
  "[| ALL c:C. Union (Ysf c) <= (Af c) ;
      ALL c:C. Qf c = SKIP | Qf c = DIV |] ==>
   !! c:C .. (? :(Af c) -> Pff c [+] Qf c 
             |~| !set Y:Ysf c .. ? a:Y -> DIV)
   =F
   fnfF_Rep_int_choice_step C Af Ysf 
          (%a. (!! c:{c : C. a : Af c} .. Pff c a)) Qf"
apply (rule cspF_rw_left)
apply (rule cspF_dist)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Rep_int_choice_Ext_Dist)
apply (simp)
apply (rule cspF_Rep_int_choice_set_DIV)

apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_Rep_int_choice_input_set)
apply (rule cspF_SKIP_DIV_Rep_int_choice)
apply (force)
apply (rule cspF_reflex)

apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Rep_int_choice_input_Dist)
apply (simp split: split_if)
apply (rule cspF_reflex)

apply (simp add: fnfF_Rep_int_choice_step_def)
apply (rule cspF_input_Rep_int_choice_set_subset)

 apply (rule fnfF_set_completion_subset)

 apply (rule ballI)
 apply (simp add: fnfF_set_completion_def)
 apply (subgoal_tac 
   "Union (Union {Ysf c |c. c : C}) <= Union {Af c |c. c : C}")
 apply (blast)
 apply (auto)
done

(*------------------------------------*
 |              induction             |
 *------------------------------------*)

lemma cspF_fnfF_Rep_int_choice_eqF_lm:
  "ALL C SPf.
   (!! :C .. SPf) |. n =F !! :C ..[n] SPf"
apply (induct_tac n)

(* base *)
apply (intro allI)
apply (simp add: fnfF_Rep_int_choice.simps)
apply (rule cspF_rw_left)
apply (rule cspF_Depth_rest_Zero)
apply (rule cspF_NDIV_eqF)

(* step *)
apply (intro allI)
apply (case_tac "(ALL c:C. SPf c : fnfF_proc)")
apply (subgoal_tac "(ALL c:C. SPf c : fnfF_proc)")

apply (erule ALL_fnfF_procE)
apply (elim conjE exE)
apply (simp)

apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (subgoal_tac
  "(!! u:C .. 
             (if u : C
              then ? :Af u -> Pff u [+] Qf u 
                    |~| !set Y:Ysf u .. ? a:Y -> DIV
              else SPf u)) 
   =F (!! u:C .. (? :Af u -> Pff u [+] Qf u 
                    |~| !set Y:Ysf u .. ? a:Y -> DIV))")
apply (assumption)
 apply (rule cspF_decompo)
 apply (simp)
 apply (simp)

apply (rule cspF_rw_left)
apply (rule cspF_Dist_nonempty)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_fnfF_Depth_rest_dist)
apply (simp)

apply (rule cspF_rw_left)
apply (rule cspF_fnfF_Rep_int_choice_one_step)
apply (simp)
apply (simp)

apply (simp add: fnfF_Rep_int_choice.simps)
apply (rule fnfF_Rep_int_choice_step_subexp)

(* Pf *)
apply (rule ballI)
apply (drule_tac x=
   "{c : C.
             a : fnfF_A
                  (if c : C
                   then ? :Af c -> Pff c [+] Qf c 
                         |~| !set Y:Ysf c .. ? a:Y -> DIV
                   else SPf c)}" in spec)
apply (drule_tac x=
   "(%c. fnfF_Pf
                  (if c : C
                   then ? :Af c -> Pff c [+] Qf c 
                         |~| !set Y:Ysf c .. ? a:Y -> DIV
                   else SPf c)
                  a)" in spec)

apply (rotate_tac -1)
apply (erule cspF_symE)
apply (rule cspF_rw_right)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_Dist)

apply (rule cspF_decompo)
apply (rule equalityI)

 apply (rule subsetI)
 apply (simp)
 apply (rule subsetI)
 apply (simp)
 apply (elim conjE bexE)
 apply (simp)

apply (simp_all)
apply (subgoal_tac "~(ALL c:C. SPf c : fnfF_proc)")
apply (simp (no_asm_simp) add: fnfF_Rep_int_choice.simps)
apply (simp)
done

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

lemma cspF_fnfF_Rep_int_choice_eqF:
  "(!! :C .. SPf) |. n =F (!! :C ..[n] SPf)"
apply (simp add: cspF_fnfF_Rep_int_choice_eqF_lm)
done

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

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

lemma fnfF_Rep_int_choice_fun_in:
  "[| inj f ; ALL x:X. SPf x : fnfF_proc |] ==>
    !!<f> :X ..[n] SPf : fnfF_proc"
apply (insert fnfF_Rep_int_choice_in[of "(f ` X)" "(%x. SPf (inv f x))" n])
apply (simp add: fnfF_Rep_int_choice_fun_def)
done

lemma fnfF_Rep_int_choice_com_in:
  "ALL x:X. SPf x : fnfF_proc ==>
       ! :X ..[n] SPf : fnfF_proc"
apply (simp add: fnfF_Rep_int_choice_com_def)
apply (rule fnfF_Rep_int_choice_fun_in)
apply (auto)
done

lemma fnfF_Rep_int_choice_set_in:
  "ALL X:Xs. SPf X : fnfF_proc ==>
       !set :Xs ..[n] SPf : fnfF_proc"
by (simp add: fnfF_Rep_int_choice_fun_in)

lemma fnfF_Rep_int_choice_nat_in:
  "ALL m:N. SPf m : fnfF_proc ==>
       !nat :N ..[n] SPf : fnfF_proc"
by (simp add: fnfF_Rep_int_choice_fun_in)

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

lemma cspF_fnfF_Rep_int_choice_fun_eqF:
  "inj f ==>
  (!!<f> :X .. SPf) |. n =F (!!<f> :X ..[n] SPf)"
apply (insert cspF_fnfF_Rep_int_choice_eqF[of "(f ` X)" "(%x. SPf (inv f x))" n])
apply (simp add: Rep_int_choice_fun_def)
apply (simp add: fnfF_Rep_int_choice_fun_def)
done

lemma cspF_fnfF_Rep_int_choice_com_eqF:
  "(! :X .. SPf) |. n =F ! :X ..[n] SPf"
apply (simp add: fnfF_Rep_int_choice_com_def)
apply (simp add: Rep_int_choice_com_def)
apply (simp add: cspF_fnfF_Rep_int_choice_fun_eqF)
done

lemma cspF_fnfF_Rep_int_choice_set_eqF:
  "(!set :Xs .. SPf) |. n =F !set :Xs ..[n] SPf"
by (simp add: cspF_fnfF_Rep_int_choice_fun_eqF)

lemma cspF_fnfF_Rep_int_choice_nat_eqF:
  "(!nat :N .. SPf) |. n =F !nat :N ..[n] SPf"
by (simp add: cspF_fnfF_Rep_int_choice_fun_eqF)

(*------------------------*
 |     auxiliary laws     |
 *------------------------*)

lemma cspF_fnfF_Rep_int_choice_Depth_rest:
  "(!! :C ..[n] SPf) |. n =F (!! :C ..[n] SPf)"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_fnfF_Rep_int_choice_eqF[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_Depth_rest_min)
apply (simp)
apply (rule cspF_fnfF_Rep_int_choice_eqF)
done

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

declare split_if    [split]
declare disj_not1   [simp]

end