Theory FNF_F_nf_def

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F/FNF_F

theory FNF_F_nf_def
imports CSP_F
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |               February 2006               |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory FNF_F_nf_def = CSP_F:

(*  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. definition of full normalisation
         2. 
         3. 

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

(*----------------------------------------------------------------------*
 |                         full normal form                             |
 *----------------------------------------------------------------------*)

consts
  fnfF_set_condition  :: "'a set => 'a set set => bool"
  fnfF_set_completion :: "'a set => 'a set set => 'a set set"
  XfnfF_proc           :: "'a proc set"
  fnfF_proc      :: "'a proc set"

defs
  fnfF_set_condition_def :
   "fnfF_set_condition A Ys == 
    (ALL Y. ((EX Y0:Ys. Y0 <= Y) & Y <= A Un Union Ys) --> Y:Ys)"

  fnfF_set_completion_def :
   "fnfF_set_completion A Ys == {Y. (EX Y0:Ys. Y0 <= Y) & Y <= (A Un Union Ys)}"

defs
  XfnfF_proc_def :
   "XfnfF_proc == {!nat n .. Pf n |Pf.
                  (ALL n. Pf n =F (!nat n .. Pf n) |. n) &
                  (ALL n. Pf n : fnfF_proc) }"

inductive "fnfF_proc"
intros
fnfF_proc_rule:
  "[| (ALL a. if a:A then Pf a : fnfF_proc else Pf a = DIV) ;
      fnfF_set_condition A Ys ; Union Ys <= A ;
      Q = SKIP | Q = DIV |]
   ==> ((? :A -> Pf) [+] Q) |~| (!set Y:Ys .. (? a:Y -> DIV))
        : fnfF_proc"

(*** convenient lemmas ***)

lemma fnfF_set_completion_sat_condition[simp]:
  "fnfF_set_condition A (fnfF_set_completion A Ys)"
apply (simp add: fnfF_set_condition_def)
apply (intro allI impI)
apply (elim conjE bexE)

apply (simp add: fnfF_set_completion_def)
apply (elim conjE bexE)
apply (rule conjI)
apply (rule_tac x="Y0a" in bexI)
apply (simp)
apply (simp)

apply (rule subsetI)
apply (erule subsetE)
apply (drule_tac x="x" in bspec, simp)
apply (simp)
apply (elim disjE conjE exE bexE)
apply (simp)

apply (rotate_tac 5)
apply (erule subsetE)
apply (simp)
done

lemma fnfF_set_completion_subset:
  "Ys <= fnfF_set_completion A Ys"
by (auto simp add: fnfF_set_completion_def)

lemma fnfF_set_completion_Union_subset:
  "Union Ys <= A ==>
   Union (fnfF_set_completion A Ys) <= A"
apply (auto simp add: fnfF_set_completion_def)
apply (subgoal_tac "x : A Un Union Ys")
apply (simp)
apply (erule disjE)
apply (auto)
done

(*----------------------------------------------------------*
 |                   intro, elim, simp                      |
 *----------------------------------------------------------*)

lemma fnfF_proc_iff:
  "(NP : fnfF_proc) = 
     (EX A Ys Pf Q.
      NP = ((? :A -> Pf) [+] Q) |~| (!set Y:Ys .. (? a:Y -> DIV)) &
      (ALL a. if a:A then Pf a : fnfF_proc else Pf a = DIV) &
       fnfF_set_condition A Ys & Union Ys <= A &
       (Q = SKIP | Q = DIV))"
apply (rule iffI)

(* => *)
 apply (erule fnfF_proc.elims)
 apply (simp_all)
 apply (rule_tac x="Ys" in exI)
 apply (simp)

(* <= *)
 apply (elim conjE exE)
 apply (simp add: fnfF_proc.intros)
done

lemma fnfF_proc_EX_I:
     "(EX A Ys Pf Q.
      NP = ((? :A -> Pf) [+] Q) |~| (!set Y:Ys .. (? a:Y -> DIV)) &
      (ALL a. if a:A then Pf a : fnfF_proc else Pf a = DIV) &
       fnfF_set_condition A Ys & Union Ys <= A &
       (Q = SKIP | Q = DIV))
    ==> NP : fnfF_proc"
apply (simp add: fnfF_proc_iff[of NP])
done

lemma fnfF_proc_EX_E:
  "[| NP : fnfF_proc ;
     (EX A Ys Pf Q.
      NP = ((? :A -> Pf) [+] Q) |~| (!set Y:Ys .. (? a:Y -> DIV)) &
      (ALL a. if a:A then Pf a : fnfF_proc else Pf a = DIV) &
       fnfF_set_condition A Ys & Union Ys <= A &
       (Q = SKIP | Q = DIV))
      ==> S |]
    ==> S"
apply (simp add: fnfF_proc_iff[of NP])
done

(*----------------------------------------------------------*
 |                 ALL fnfF_proc_iff                   |
 *----------------------------------------------------------*)

lemma ALL_fnfF_proc_only_if:
  "ALL x:X. NPf x : fnfF_proc
   ==>
     (EX Af Ysf Pff Qf.
      NPf = (%x. if x:X then (((? :(Af x) -> (Pff x)) [+] Qf x) |~| 
                             (!set Y:(Ysf x) .. (? a:Y -> DIV)))
                        else NPf x) &
      (ALL x:X. ALL a. if a:(Af x) then (Pff x a) : fnfF_proc 
                       else (Pff x a) = DIV) &
      (ALL x:X. fnfF_set_condition (Af x) (Ysf x)) &
      (ALL x:X. Union (Ysf x) <= Af x) &
      (ALL x:X. Qf x = SKIP | Qf x = DIV))"
apply (simp add: fnfF_proc_iff)
apply (simp add: choice_BALL_EX)
apply (elim exE)
apply (rule_tac x="f" in exI)
apply (rule_tac x="fa" in exI)
apply (rule_tac x="fb" in exI)
apply (rule_tac x="fc" in exI)

(* NPf *)
apply (rule conjI)
apply (simp add: expand_fun_eq)
apply (rule allI)
apply (case_tac "x:X")
apply (simp_all)

apply (intro allI ballI)
apply (drule_tac x="x" in bspec, simp)
apply (elim conjE)
apply (drule_tac x="a" in spec)
apply (simp)
done

lemma ALL_fnfF_proc_iff:
  "(ALL x:X. NPf x : fnfF_proc)
   =
     (EX Af Ysf Pff Qf.
      NPf = (%x. if x:X then (((? :(Af x) -> (Pff x)) [+] Qf x) |~| 
                             (!set Y:(Ysf x) .. (? a:Y -> DIV)))
                        else NPf x) &
      (ALL x:X. ALL a. if a:(Af x) then (Pff x a) : fnfF_proc 
                       else (Pff x a) = DIV) &
      (ALL x:X. fnfF_set_condition (Af x) (Ysf x)) &
      (ALL x:X. Union (Ysf x) <= Af x) &
      (ALL x:X. Qf x = SKIP | Qf x = DIV))"
apply (rule)
apply (simp add: ALL_fnfF_proc_only_if)

apply (elim conjE exE)
apply (intro ballI)
apply (simp add: expand_fun_eq)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in bspec, simp)+
apply (simp)
apply (simp add: fnfF_proc.intros)
done

lemma ALL_fnfF_procI:
  "(EX Af Ysf Pff Qf.
      NPf = (%x. if x:X then (((? :(Af x) -> (Pff x)) [+] Qf x) |~| 
                             (!set Y:(Ysf x) .. (? a:Y -> DIV)))
                        else NPf x) &
      (ALL x:X. ALL a. if a:(Af x) then (Pff x a) : fnfF_proc 
                       else (Pff x a) = DIV) &
      (ALL x:X. fnfF_set_condition (Af x) (Ysf x)) &
      (ALL x:X. Union (Ysf x) <= Af x) &
      (ALL x:X. Qf x = SKIP | Qf x = DIV))
   ==> ALL x:X. NPf x : fnfF_proc"
apply (simp add: ALL_fnfF_proc_iff)
done

lemma ALL_fnfF_procE:
  "[| ALL x:X. NPf x : fnfF_proc ;
      (EX Af Ysf Pff Qf.
      NPf = (%x. if x:X then (((? :(Af x) -> (Pff x)) [+] Qf x) |~| 
                             (!set Y:(Ysf x) .. (? a:Y -> DIV)))
                        else NPf x) &
      (ALL x:X. ALL a. if a:(Af x) then (Pff x a) : fnfF_proc 
                       else (Pff x a) = DIV) &
      (ALL x:X. fnfF_set_condition (Af x) (Ysf x)) &
      (ALL x:X. Union (Ysf x) <= Af x) &
      (ALL x:X. Qf x = SKIP | Qf x = DIV))
   ==> S |] ==> S"
apply (simp add: ALL_fnfF_proc_iff)
done

(*======================================================*
 |         function to decompose : fnfF_decompo         |
 *======================================================*)

consts
  fnfF_A ::
     "'a proc => ('a set)"
  fnfF_Ys ::
     "'a proc => ('a set set)"
  fnfF_Pf ::
     "'a proc => ('a => 'a proc)"
  fnfF_Q ::
     "'a proc => 'a proc"

(* they are partial functions *)

recdef fnfF_A "{}"
  "fnfF_A (((? :A -> Pf) [+] Q) |~| R) = A"

recdef fnfF_Ys "{}"
  "fnfF_Ys (P |~| !! :Cf .. Pf) = (inv sel_set) ` Cf"

recdef fnfF_Pf "{}"
  "fnfF_Pf (((? :A -> Pf) [+] Q) |~| R) = Pf"

recdef fnfF_Q "{}"
  "fnfF_Q (((? :A -> Pf) [+] Q) |~| R) = Q"

lemma fnfF_Ys_get[simp]:
  "fnfF_Ys (P |~| !set :Ys .. Pf) = Ys"
apply (auto simp add: Rep_int_choice_fun_def)
apply (simp add: image_iff)
done

(*------------------------*
 |     decomposition      |
 *------------------------*)

lemma cspF_fnfF_nat_decompo:
   "P : fnfF_proc ==>
    P =F ((? : (fnfF_A P) -> (fnfF_Pf P)) [+] fnfF_Q P) 
         |~| (!set Y: fnfF_Ys P .. (? a:Y -> DIV))"
apply (erule fnfF_proc.elims)
apply (simp)
done

(*--------------------------------------*
 |   properties of fnfF decomposition   |
 *--------------------------------------*)

lemma fnfF_Pf_A:
   "[| P : fnfF_proc ; a : (fnfF_A P) |]
    ==> (fnfF_Pf P) a : fnfF_proc"
apply (erule fnfF_proc.elims)
apply (simp)
done

lemma fnfF_Pf_DIV:
   "[| P : fnfF_proc ; a ~: (fnfF_A P) |]
    ==> (fnfF_Pf P) a = DIV"
apply (erule fnfF_proc.elims)
apply (simp)
done

lemma fnfF_Q_range:
   "P : fnfF_proc
    ==> (fnfF_Q P) = SKIP | (fnfF_Q P) = DIV"
apply (erule fnfF_proc.elims)
apply (simp)
done

lemma fnfF_condition_A_Ys:
   "P : fnfF_proc ==>
    fnfF_set_condition (fnfF_A P) (fnfF_Ys P)"
apply (erule fnfF_proc.elims)
apply (simp)
done

lemma fnfF_Union_Ys_A:
   "P : fnfF_proc ==>
    Union (fnfF_Ys P)  <= (fnfF_A P)"
apply (erule fnfF_proc.elims)
apply (simp)
done

(*-----------------------*
 |    DIV, SKIP, STOP    |
 *-----------------------*)

consts
  NSKIP     :: "'a proc"
  NDIV      :: "'a proc"
  NSTOP     :: "'a proc"

defs
  NSKIP_def : "NSKIP == ((? a:{} -> DIV) [+] SKIP) |~| (!set Y:{} .. (? a:Y -> DIV))"
  NDIV_def  : "NDIV  == ((? a:{} -> DIV) [+] DIV)  |~| (!set Y:{} .. (? a:Y -> DIV))"
  NSTOP_def : "NSTOP == ((? a:{} -> DIV) [+] DIV)  |~| (!set Y:{{}} .. (? a:Y -> DIV))"

(*** in fnfF ***)

lemma fnfF_NSKIP[simp]: "NSKIP : fnfF_proc"
apply (simp add: NSKIP_def)
apply (rule fnfF_proc.intros)
apply (simp_all add: fnfF_set_condition_def)
done

lemma fnfF_NDIV[simp]: "NDIV : fnfF_proc"
apply (simp add: NDIV_def)
apply (rule fnfF_proc.intros)
apply (simp_all add: fnfF_set_condition_def)
done

lemma fnfF_NSTOP[simp]: "NSTOP : fnfF_proc"
apply (simp add: NSTOP_def)
apply (rule fnfF_proc.intros)
apply (simp_all add: fnfF_set_condition_def)
done

(*** eqF ***)

lemma cspF_NSKIP_eqF: "SKIP =F NSKIP"
apply (simp add: NSKIP_def)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_choice_rule)
apply (rule cspF_Rep_int_choice_DIV)
apply (rule cspF_rw_right)
apply (rule cspF_unit)
apply (rule cspF_reflex)
done

lemma cspF_NDIV_eqF: "DIV =F NDIV"
apply (simp add: NDIV_def)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_choice_rule)
apply (rule cspF_Rep_int_choice_DIV)
apply (rule cspF_rw_right)
apply (rule cspF_unit)
apply (rule cspF_reflex)
done

lemma cspF_NSTOP_eqF: "STOP =F NSTOP"
apply (simp add: NSTOP_def)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_choice_rule)
apply (rule cspF_Rep_int_choice_singleton)
apply (rule cspF_rw_right)
apply (rule cspF_unit)
apply (rule cspF_step)
done

(*==============================================================*
 |               convenient rules for fnfF                      |
 *==============================================================*)

lemma cspF_fnfF_Depth_rest_dist:
  "Q = SKIP | Q = DIV ==>
   (? :A -> Pf [+] Q
   |~| !set Y:Ys .. ? a:Y -> DIV) |. Suc n
  =F 
   (? a:A -> (Pf a |. n) [+] Q
   |~| !set Y:Ys .. ? a:Y -> DIV)"
apply (rule cspF_rw_left)
apply (rule cspF_dist)
apply (rule cspF_decompo)
apply (rule cspF_rw_left)
apply (rule cspF_Ext_dist)
apply (rule cspF_decompo)
apply (rule cspF_rw_left)
apply (rule cspF_step)
apply (rule cspF_reflex)
apply (erule disjE)
apply (simp_all)

apply (rule cspF_rw_left)
apply (rule cspF_Dist)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_step)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_DIV_Depth_rest)
done

(* left DIV *)

lemma cspF_fsfF_left_DIV:
  "(? a:{} -> DIV [+] DIV) |~| P =F P"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Ext_choice_rule)
apply (rule cspF_reflex)
apply (rule cspF_unit)
done

lemma cspF_fsfF_right_DIV:
  "P |~| (!set :{} .. Pf) =F P"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_Rep_int_choice_DIV)
apply (rule cspF_unit)
done

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

declare split_if    [split]
declare disj_not1   [simp]

end

lemma fnfF_set_completion_sat_condition: 

  fnfF_set_condition A (fnfF_set_completion A Ys)

lemma fnfF_set_completion_subset: 

  Ys ⊆ fnfF_set_completion A Ys

lemma fnfF_set_completion_Union_subset: 

  Union Ys ⊆ A ==> Union (fnfF_set_completion A Ys) ⊆ A

lemma fnfF_proc_iff: 

  (NP ∈ fnfF_proc) =
  (∃A Ys Pf Q.
      NP = ? :A -> Pf [+] Q |~| !set Y:Ys .. ? a:Y -> DIV ∧
      (∀a. if a ∈ A then Pf a ∈ fnfF_proc else Pf a = DIV) ∧
      fnfF_set_condition A Ys ∧ Union Ys ⊆ A ∧ (Q = SKIP ∨ Q = DIV))

lemma fnfF_proc_EX_I: 

  ∃A Ys Pf Q.
     NP = ? :A -> Pf [+] Q |~| !set Y:Ys .. ? a:Y -> DIV ∧
     (∀a. if a ∈ A then Pf a ∈ fnfF_proc else Pf a = DIV) ∧
     fnfF_set_condition A Ys ∧ Union Ys ⊆ A ∧ (Q = SKIP ∨ Q = DIV)
  ==> NP ∈ fnfF_proc

lemma fnfF_proc_EX_E: 

  [| NP ∈ fnfF_proc;
     ∃A Ys Pf Q.
        NP = ? :A -> Pf [+] Q |~| !set Y:Ys .. ? a:Y -> DIV ∧
        (∀a. if a ∈ A then Pf a ∈ fnfF_proc else Pf a = DIV) ∧
        fnfF_set_condition A Ys ∧ Union Ys ⊆ A ∧ (Q = SKIP ∨ Q = DIV)
     ==> S |]
  ==> S

lemma ALL_fnfF_proc_only_if: 

  ∀x∈X. NPf x ∈ fnfF_proc
  ==> ∃Af Ysf Pff Qf.
         NPf =
         (%x. if x ∈ X
              then ? :Af x -> Pff x [+] Qf x |~| !set Y:Ysf x .. ? a:Y -> DIV
              else NPf x) ∧
         (∀x∈X. ∀a. if a ∈ Af x then Pff x a ∈ fnfF_proc else Pff x a = DIV) ∧
         (∀x∈X. fnfF_set_condition (Af x) (Ysf x)) ∧
         (∀x∈X. Union (Ysf x) ⊆ Af x) ∧ (∀x∈X. Qf x = SKIP ∨ Qf x = DIV)

lemma ALL_fnfF_proc_iff: 

  (∀x∈X. NPf x ∈ fnfF_proc) =
  (∃Af Ysf Pff Qf.
      NPf =
      (%x. if x ∈ X
           then ? :Af x -> Pff x [+] Qf x |~| !set Y:Ysf x .. ? a:Y -> DIV
           else NPf x) ∧
      (∀x∈X. ∀a. if a ∈ Af x then Pff x a ∈ fnfF_proc else Pff x a = DIV) ∧
      (∀x∈X. fnfF_set_condition (Af x) (Ysf x)) ∧
      (∀x∈X. Union (Ysf x) ⊆ Af x) ∧ (∀x∈X. Qf x = SKIP ∨ Qf x = DIV))

lemma ALL_fnfF_procI: 

  ∃Af Ysf Pff Qf.
     NPf =
     (%x. if x ∈ X then ? :Af x -> Pff x [+] Qf x |~| !set Y:Ysf x .. ? a:Y -> DIV
          else NPf x) ∧
     (∀x∈X. ∀a. if a ∈ Af x then Pff x a ∈ fnfF_proc else Pff x a = DIV) ∧
     (∀x∈X. fnfF_set_condition (Af x) (Ysf x)) ∧
     (∀x∈X. Union (Ysf x) ⊆ Af x) ∧ (∀x∈X. Qf x = SKIP ∨ Qf x = DIV)
  ==> ∀x∈X. NPf x ∈ fnfF_proc

lemma ALL_fnfF_procE: 

  [| ∀x∈X. NPf x ∈ fnfF_proc;
     ∃Af Ysf Pff Qf.
        NPf =
        (%x. if x ∈ X
             then ? :Af x -> Pff x [+] Qf x |~| !set Y:Ysf x .. ? a:Y -> DIV
             else NPf x) ∧
        (∀x∈X. ∀a. if a ∈ Af x then Pff x a ∈ fnfF_proc else Pff x a = DIV) ∧
        (∀x∈X. fnfF_set_condition (Af x) (Ysf x)) ∧
        (∀x∈X. Union (Ysf x) ⊆ Af x) ∧ (∀x∈X. Qf x = SKIP ∨ Qf x = DIV)
     ==> S |]
  ==> S

lemma fnfF_Ys_get: 

  fnfF_Ys (P |~| !set :Ys .. Pf) = Ys

lemma cspF_fnfF_nat_decompo: 

  P ∈ fnfF_proc
  ==> P =F 
      ? :fnfF_A P -> fnfF_Pf P [+] fnfF_Q P |~| !set Y:fnfF_Ys P .. ? a:Y -> DIV

lemma fnfF_Pf_A: 

  [| P ∈ fnfF_proc; a ∈ fnfF_A P |] ==> fnfF_Pf P a ∈ fnfF_proc

lemma fnfF_Pf_DIV: 

  [| P ∈ fnfF_proc; a ∉ fnfF_A P |] ==> fnfF_Pf P a = DIV

lemma fnfF_Q_range: 

  P ∈ fnfF_proc ==> fnfF_Q P = SKIP ∨ fnfF_Q P = DIV

lemma fnfF_condition_A_Ys: 

  P ∈ fnfF_proc ==> fnfF_set_condition (fnfF_A P) (fnfF_Ys P)

lemma fnfF_Union_Ys_A: 

  P ∈ fnfF_proc ==> Union (fnfF_Ys P) ⊆ fnfF_A P

lemma fnfF_NSKIP: 

  NSKIP ∈ fnfF_proc

lemma fnfF_NDIV: 

  NDIV ∈ fnfF_proc

lemma fnfF_NSTOP: 

  NSTOP ∈ fnfF_proc

lemma cspF_NSKIP_eqF: 

  SKIP =F NSKIP

lemma cspF_NDIV_eqF: 

  DIV =F NDIV

lemma cspF_NSTOP_eqF: 

  STOP =F NSTOP

lemma cspF_fnfF_Depth_rest_dist: 

  Q = SKIP ∨ Q = DIV
  ==> (? :A -> Pf [+] Q |~| !set Y:Ys .. ? a:Y -> DIV) |. Suc n =F 
      ? a:A -> Pf a |. n [+] Q |~| !set Y:Ys .. ? a:Y -> DIV

lemma cspF_fsfF_left_DIV: 

  ? a:{} -> DIV [+] DIV |~| P =F P

lemma cspF_fsfF_right_DIV: 

  P |~| !set :{} .. Pf =F P