Theory FNF_F_nf_def

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

theory FNF_F_nf_def
imports CSP_F_Main

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

theory FNF_F_nf_def
imports CSP_F_Main
begin

(*  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           :: "('p,'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)}"

(* Isabelle 2005
consts
fnfF_proc      :: "('p,'a) proc set"

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"
*)

inductive_set
fnfF_proc      :: "('p,'a) proc set"
where
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"

(* .elims ---> .cases *)

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) }"

(*** convenient lemmas ***)

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

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"

lemma fnfF_set_completion_Union_subset:
"Union Ys <= A ==>
Union (fnfF_set_completion A Ys) <= A"
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 (erule fnfF_proc.cases)
apply (force)

(* <= *)
apply (elim conjE exE)
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"
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"
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 (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 (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 (elim conjE exE)
apply (intro ballI)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in bspec, simp)+
apply (simp)
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"
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"
done

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

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

(* they are partial functions *)

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

recdef fnfF_Ys "{}"
"fnfF_Ys (P |~| !! : type1 Ys .. Pf) = Ys"

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"

(*------------------------*
|     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 (erule fnfF_proc.cases)
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.cases)
apply (simp)
done

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

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

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

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

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

consts
NSKIP     :: "('p,'a) proc"
NDIV      :: "('p,'a) proc"
NSTOP     :: "('p,'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 (rule fnfF_proc.intros)
done

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

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

(*** eqF ***)

lemma cspF_NSKIP_eqF: "SKIP =F NSKIP"
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 (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 (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 (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
```