(*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| November 2004 |
| June 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| April 2006 (modified) |
| January 2007 (modified) |
| April 2007 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_syntax
imports Infra
begin
(* The following simplification rules are deleted in this theory file *)
(* because they unexpectly rewrite UnionT and InterT. *)
(* Union (B ` A) = (UN x:A. B x) *)
(* Inter (B ` A) = (INT x:A. B x) *)
declare Union_image_eq [simp del]
declare Inter_image_eq [simp del]
(*-----------------------------------------------------------*
| |
| Process Type Definitions |
| |
| 'a proc : type of process expressions |
| 'n : process name |
| 'a : event |
| |
*-----------------------------------------------------------*)
(*********************************************************************
process expression
*********************************************************************)
datatype
('p,'a) proc
= STOP
| SKIP
| DIV
| Act_prefix "'a" "('p,'a) proc" ("(1_ /-> _)" [150,80] 80)
| Ext_pre_choice "'a set" "'a => ('p,'a) proc"
("(1? :_ /-> _)" [900,80] 80)
| Ext_choice "('p,'a) proc" "('p,'a) proc"
("(1_ /[+] _)" [72,73] 72)
| Int_choice "('p,'a) proc" "('p,'a) proc"
("(1_ /|~| _)" [64,65] 64)
| Rep_int_choice_nat "nat set" "nat => ('p,'a) proc"
("(1!nat :_ ../ _)" [900,68] 68)
| Rep_int_choice_set "'a set set" "'a set => ('p,'a) proc"
("(1!set :_ ../ _)" [900,68] 68)
| IF "bool" "('p,'a) proc" "('p,'a) proc"
("(0IF _ /THEN _ /ELSE _)" [900,60,60] 88)
| Parallel "('p,'a) proc" "'a set" "('p,'a) proc"
("(1_ /|[_]| _)" [76,0,77] 76)
| Hiding "('p,'a) proc" "'a set" ("(1_ /-- _)" [84,85] 84)
| Renaming "('p,'a) proc" "('a * 'a) set"
("(1_ /[[_]])" [84,0] 84)
| Seq_compo "('p,'a) proc" "('p,'a) proc"
("(1_ /;; _)" [79,78] 78)
| Depth_rest "('p,'a) proc" "nat"
("(1_ /|. _)" [84,900] 84)
| Proc_name "'p" ("$_" [900] 90)
(*--------------------------------------------------------------------*
| |
| (1) binding power: |
| Proc_Name > IF > {Hiding, Renaming, Restriction} > |
| {Act_prefix, Ext_pre_choice} > Seq_compo > Parallel > |
| Ext_choice > Rep_int_choice > int_choice |
| |
| The binding power 90 is higher than ones of processes ops. |
| |
| (2) About ("(1_ /-> _)" [150,80] 80) |
| The nth operator ! has the power 101. |
| So, 150 > 101 is needed. |
| |
| (3) "selector" is necessary for having our CSP expressive |
| with respect to the domain for stable-failures model F. |
| |
*--------------------------------------------------------------------*)
(*** external prefix ***)
syntax
"@Ext_pre_choice" :: "pttrn => 'a set => ('p,'a) proc
=> ('p,'a) proc" ("(1? _:_ /-> _)" [900,900,80] 80)
translations
"? x:X -> P" == "? :X -> (%x. P)"
(*** replicated internal choice (bound variable, UNIV) ***)
syntax
"@Rep_int_choice_nat" :: "pttrn => nat set => ('p,'a) proc
=> ('p,'a) proc" ("(1!nat _:_ ../ _)" [900,900,68] 68)
"@Rep_int_choice_nat_UNIV" :: "pttrn => ('p,'a) proc
=> ('p,'a) proc" ("(1!nat _ ../ _)" [900,68] 68)
translations
"!nat n:N .. P" == "!nat :N .. (%n. P)"
"!nat n .. P" == "!nat n:UNIV .. P"
syntax
"@Rep_int_choice_set" :: "pttrn => 'a set set => ('p,'a) proc
=> ('p,'a) proc" ("(1!set _:_ ../ _)" [900,900,68] 68)
"@Rep_int_choice_set_UNIV" :: "pttrn => ('p,'a) proc
=> ('p,'a) proc" ("(1!set _ ../ _)" [900,68] 68)
translations
"!set X:Xs .. P" == "!set :Xs .. (%X. P)"
"!set X .. P" == "!set X:UNIV .. P"
(*** com ***)
consts
Rep_int_choice_com :: "'a set => ('a => ('p,'a) proc) => ('p,'a) proc"
("(1! :_ .. /_)" [900,68] 68)
defs
Rep_int_choice_com_def :
"! :A .. Pf == !set X:{{a} |a. a : A} .. Pf (contents(X))"
syntax
"@Rep_int_choice_com" :: "pttrn => 'a set => ('a => ('p,'a) proc) => ('p,'a) proc"
("(1! _:_ .. /_)" [900,900,68] 68)
"@Rep_int_choice_com_UNIV" :: "pttrn => ('a => ('p,'a) proc) => ('p,'a) proc"
("(1! _ .. /_)" [900,68] 68)
translations
"! x:X .. P" == "! :X .. (%x. P)"
"! x .. P" == "! x:UNIV .. P"
(*** f ***)
consts
Rep_int_choice_f :: "('b => 'a) => 'b set => ('b => ('p,'a) proc) => ('p,'a) proc"
("(1!<_> :_ .. /_)" [0,900,68] 68)
defs
Rep_int_choice_f_def :
"!<f> :X .. Pf == ! :(f ` X) .. (%x. (Pf ((inv f) x)))"
syntax
"@Rep_int_choice_f":: "('b => 'a) => pttrn => 'b set => ('p,'a) proc => ('p,'a) proc"
("(1!<_> _:_ .. /_)" [0,900,900,68] 68)
"@Rep_int_choice_f_UNIV":: "('b => 'a) => pttrn => ('p,'a) proc => ('p,'a) proc"
("(1!<_> _ .. /_)" [900,900,68] 68)
translations
"!<f> x:X .. P" == "!<f> :X .. (%x. P)"
"!<f> x .. P" == "!<f> x:UNIV .. P"
(*** internal prefix choice ***)
consts
Int_pre_choice :: "'a set => ('a => ('p,'a) proc) => ('p,'a) proc"
("(1! :_ /-> _)" [900,80] 80)
defs
Int_pre_choice_def : "! :X -> Pf == ! :X .. (%x. x -> (Pf x))"
syntax
"@Int_pre_choice" :: "pttrn => 'a set => ('p,'a) proc
=> ('p,'a) proc" ("(1! _:_ /-> _)" [900,900,80] 80)
"@Int_pre_choice_UNIV" :: "pttrn => ('p,'a) proc => ('p,'a) proc"
("(1! _ /-> _)" [900,80] 80)
translations
"! x:X -> P" == "! :X -> (%x. P)"
"! x -> P" == "! x:UNIV -> P"
(*** sending and receiving prefixes ***)
consts
Send_prefix :: "('x => 'a) => 'x => ('p,'a) proc => ('p,'a) proc"
("(1_ ! _ /-> _)" [900,1000,80] 80)
Nondet_send_prefix :: "('x => 'a) => 'x set =>
('x => ('p,'a) proc) => ('p,'a) proc"
Rec_prefix :: "('x => 'a) => 'x set =>
('x => ('p,'a) proc) => ('p,'a) proc"
defs
Send_prefix_def :
"a ! x -> P == a x -> P"
Nondet_send_prefix_def :
"Nondet_send_prefix f X Pf == ! :(f ` X) -> (%x. (Pf ((inv f) x)))"
Rec_prefix_def :
"Rec_prefix f X Pf == ? :(f ` X) -> (%x. (Pf ((inv f) x)))"
syntax
"@Nondet_send_prefix" ::
"('x => 'a) => pttrn => 'x set => ('p,'a) proc => ('p,'a) proc"
("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)
"@Nondet_send_prefix_UNIV" ::
"('x => 'a) => pttrn => ('p,'a) proc => ('p,'a) proc"
("(1_ !? _ /-> _)" [900,900,80] 80)
"@Rec_prefix" ::
"('x => 'a) => pttrn => 'x set => ('p,'a) proc => ('p,'a) proc"
("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
"@Rec_Prefix_UNIV" ::
"('x => 'a) => pttrn => ('p,'a) proc => ('p,'a) proc"
("(1_ ? _ /-> _)" [900,900,80] 80)
translations
"a !? x:X -> P" == "Nondet_send_prefix a X (%x. P)"
"a !? x -> P" == "a !? x:UNIV -> P"
"a ? x:X -> P" == "Rec_prefix a X (%x. P)"
"a ? x -> P" == "a? x:UNIV -> P"
(*** unfolding syntactic sugar ***)
lemmas csp_prefix_ss_def = Int_pre_choice_def Send_prefix_def Nondet_send_prefix_def
Rec_prefix_def
(*** parallel ***)
syntax
"_Interleave" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /||| _)" [76,77] 76)
"_Synchro" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /|| _)" [76,77] 76)
translations
"P ||| Q" == "P |[{}]| Q"
"P || Q" == "P |[UNIV]| Q"
consts
Alpha_parallel :: "('p,'a) proc => 'a set => 'a set => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /(2|[_,/_]|)/ _)" [76,0,0,77] 76)
defs
Alpha_parallel_def :
"P |[X,Y]| Q == (P |[- X]| SKIP) |[X Int Y]| (Q |[- Y]| SKIP)"
consts
Inductive_parallel :: "(('p,'a) proc * 'a set) list
=> ('p,'a) proc" ("(1[||] _)" [77] 77)
primrec
"[||] [] = SKIP"
"[||] (PX # PXs) = (fst PX) |[snd PX, Union (snd ` set PXs)]| ([||] PXs)"
consts
Rep_parallel :: "'i set => ('i => (('p,'a) proc * 'a set))
=> ('p,'a) proc" ("(1[||]:_ /_)" [90,77] 77)
defs
Rep_parallel_def :
"[||]:I PXf == [||] (map PXf (SOME Is. Is isListOf I))"
syntax
"@Rep_parallel" ::
"pttrn => 'i set => (('p,'a) proc * 'a set)
=> ('p,'a) proc" ("(1[||] _:_ .. /_)" [900,90,77] 77)
translations
"[||] i:I .. PX" == "[||]:I (%i. PX)"
(************************************
| empty Index |
************************************)
lemma Rep_parallel_empty[simp]: "I = {} ==> [||]:I PXf = SKIP"
by (simp add: Rep_parallel_def)
(************************************
| one Index |
************************************)
lemma Rep_parallel_one:
"I = {i} ==> [||]:I PXf = (fst (PXf i)) |[snd (PXf i), {}]| SKIP"
by (simp add: Rep_parallel_def)
(*** timeout ***)
syntax
"_Timeout" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /[> _)" [73,74] 73)
translations
"P [> Q" == "(P |~| STOP) [+] Q"
(*** it is sometimes useful to prevent automatic unfolding [> ***)
consts
Timeout :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /[>def _)" [73,74] 73)
defs
Timeout_def : "P [>def Q == P [> Q"
(*------------------------------------*
| |
| X-Symbols |
| |
*------------------------------------*)
syntax (output)
"_PrefixX" :: "'a => ('p,'a) proc => ('p,'a) proc"
("(1_ /-> _)" [150,80] 80)
"_Ext_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"
("(1? _:_ /-> _)" [900,900,80] 80)
"_Ext_choiceX" :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
("(1_ /[+] _)" [72,73] 72)
"_Int_choiceX" :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
("(1_ /|~| _)" [64,65] 64)
"_Int_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"
("(1! _:_ /-> _)" [900,900,80] 80)
syntax (xsymbols)
"_PrefixX" :: "'a => ('p,'a) proc => ('p,'a) proc"
("(1_ /-> _)" [150,80] 80)
"_Ext_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"
("(1? _:_ /-> _)" [900,900,80] 80)
"_Ext_choiceX" :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
("(1_ /\<box> _)" [72,73] 72)
"_Int_choiceX" :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
("(1_ /\<sqinter> _)" [64,65] 64)
"_Int_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"
("(1! _:_ /-> _)" [900,900,80] 80)
translations
"a -> P" == "a -> P"
"? x:X -> P" == "? x:X -> P"
"P \<box> Q" == "P [+] Q"
"P \<sqinter> Q" == "P |~| Q"
"! x:X -> P" == "! x:X -> P"
syntax (output)
"_Nondet_send_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('p,'a) proc => ('p,'a) proc"
("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)
"_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => ('p,'a) proc => ('p,'a) proc"
("(1_ !? _ /-> _)" [900,900,80] 80)
"_Send_prefixX" :: "('x => 'a) => 'x => ('p,'a) proc => ('p,'a) proc"
("(1_ ! _ /-> _)" [900,1000,80] 80)
"_Rec_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('p,'a) proc => ('p,'a) proc"
("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
"_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
('p,'a) proc => ('p,'a) proc"
("(1_ ? _ /-> _)" [900,900,80] 80)
syntax (xsymbols)
"_Nondet_send_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('p,'a) proc => ('p,'a) proc"
("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)
"_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => ('p,'a) proc => ('p,'a) proc"
("(1_ !? _ /-> _)" [900,900,80] 80)
"_Send_prefixX" :: "('x => 'a) => 'x => ('p,'a) proc => ('p,'a) proc"
("(1_ ! _ /-> _)" [900,1000,80] 80)
"_Rec_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('p,'a) proc => ('p,'a) proc"
("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
"_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
('p,'a) proc => ('p,'a) proc"
("(1_ ? _ /-> _)" [900,900,80] 80)
translations
"a !? x:X -> P" == "a !? x:X -> P"
"a !? x -> P" == "a !? x:UNIV -> P"
"a ! x -> P" == "a ! x -> P"
"a ? x:X -> P" == "a ? x:X -> P"
"a ? x -> P" == "a ? x:UNIV -> P"
syntax (output)
"_Proc_nameX" :: "'p => ('p,'a) proc" ("<_>" [0] 90)
"_TimeoutX" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /[> _)" [73,74] 73)
"_TimeoutdefX" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /[>def _)" [73,74] 73)
"_HidingX" :: "('p,'a) proc => 'a set => ('p,'a) proc"
("(1_ /-- _)" [84,85] 84)
"_RenamingX" :: "('p,'a) proc => ('a * 'a) set => ('p,'a) proc"
("(1_ /[[_]])" [84,0] 84)
"_Depth_rest" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /|. _)" [84,900] 84)
syntax (xsymbols)
"_Proc_nameX" :: "'p => ('p,'a) proc" ("⟨_⟩" [0] 90)
"_TimeoutX" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /\<rhd> _)" [73,74] 73)
"_TimeoutdefX":: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /\<unrhd> _)" [73,74] 73)
"_HidingX" :: "('p,'a) proc => 'a set => ('p,'a) proc"
("(1_ /\<midarrow> _)" [84,85] 84)
"_RenamingX" :: "('p,'a) proc => ('a * 'a) set => ('p,'a) proc"
("(1_ /[|_|])" [84,0] 84)
"_Depth_rest" :: "('p,'a) proc => ('p,'a) proc
=> ('p,'a) proc" ("(1_ /⌊ _)" [84,900] 84)
translations
"P \<rhd> Q" == "(P |~| STOP) [+] Q"
"P \<unrhd> Q" == "P [>def Q"
"P \<midarrow> X" == "P -- X"
"P [|r|]" == "P [[r]]"
"P ⌊ n" == "P |. n"
(*===================================================================*
(1) We assume that a process-name-function PNfun is given for
defining the meaning of each process-name.
When you define a type of process names, you have to define
the function PNfun by "overloaded" as follows:
defs (overloaded)
PNfun_test_def : "PNfun == ..."
(2) There are two kinds of approahes for fixed points, i.e.
cms and cpo approaches. You can defin the mode for fixed
points by
defs FPmode = CPOmode
or
defs FPmode = CMSmode
In addtion, you can use MIXmode as follows
defs FPmode = CMSmode
It means the least fixed point (in subset order) is used for
giving the meaning of process names based on cpo approach, and if
the process function is guarded then cms appoach is also used
because the least fixed point is the unique fixed point in this
case.
*==================================================================*)
consts PNfun :: "'p => ('p,'a) proc" (* Definition of process names *)
datatype fpmode = CPOmode | CMSmode | MIXmode
consts FPmode :: "fpmode"
lemma CPOmode_or_CMSmode_or_MIXmode_lm:
"m = FPmode --> m = CPOmode | m = CMSmode | m = MIXmode"
apply (induct_tac m)
apply (auto)
done
lemma CPOmode_or_CMSmode_or_MIXmode:
"FPmode = CPOmode | FPmode = CMSmode | FPmode = MIXmode"
by (simp add: CPOmode_or_CMSmode_or_MIXmode_lm)
(* ---------------------------------------------- *
| |
| if you do not use process names, you can use |
| the type "nopn" as the type of process names |
| |
| e.g. consts Count :: "(nopn,nat) proc |
| |
* ---------------------------------------------- *)
datatype nopn = UselessName
defs (overloaded)
PNfun_nopn_def : "PNfun == (%p::nopn. STOP)"
(*-------*
| CHAOS |
*-------*)
datatype 'a ChaosName = Chaos "'a set"
consts Chaosfun :: "'a ChaosName => ('a ChaosName, 'a) proc"
primrec "Chaosfun (Chaos A) = (! x:A -> $(Chaos A)) |~| STOP"
defs (overloaded)
Set_Chaosfun_def [simp]: "PNfun == Chaosfun"
consts CHAOS :: "'a set => ('a ChaosName, 'a) proc"
defs CHAOS_def : "CHAOS == (%A. $(Chaos A))"
(* --------------------------------------- *
an example of recursive processes
datatype AB = A | B
consts ABfun :: "AB => (AB,nat) proc"
primrec
"ABfun A = 0 -> $B"
"ABfun B = 1 -> $A"
defs (overloaded)
PNfun_AB_def : "PNfun == ABfun"
* --------------------------------------- *)
(*********************************************************************
substitution by functions : 'p => ('a,'p) proc
*********************************************************************)
consts
Subst_procfun :: "('p,'a) proc => ('p => ('q,'a) proc)
=> ('q,'a) proc" ("_ <<" [1000] 1000)
Subst_procfun_prod ::
"('p => ('q,'a) proc) =>
('q => ('r,'a) proc) => ('p => ('r,'a) proc)"
("_ <<<" [1000] 1000)
primrec
"STOP<<Pf = STOP"
"SKIP<<Pf = SKIP"
"DIV<<Pf = DIV"
"(a -> P)<<Pf = a -> P<<Pf"
"(? :X -> Qf)<<Pf = ? a:X -> (Qf a)<<Pf"
"(P [+] Q)<<Pf = P<<Pf [+] Q<<Pf"
"(P |~| Q)<<Pf = P<<Pf |~| Q<<Pf"
"(!nat :N .. Qf)<<Pf = !nat n:N .. (Qf n)<<Pf"
"(!set :Xs .. Qf)<<Pf = !set X:Xs .. (Qf X)<<Pf"
"(IF b THEN P ELSE Q)<<Pf = IF b THEN P<<Pf ELSE Q<<Pf"
"(P |[X]| Q)<<Pf = P<<Pf |[X]| Q<<Pf"
"(P -- X)<<Pf = P<<Pf -- X"
"(P [[r]])<<Pf = P<<Pf [[r]]"
"(P ;; Q)<<Pf = P<<Pf ;; Q<<Pf"
"(P |. n)<<Pf = P<<Pf |. n"
"($p) <<Pf = Pf p"
defs
Subst_procfun_prod_def: "Pf <<< == (%Qf p. (Pf p)<<Qf)"
lemma Subst_procfun_Rep_int_choice_com[simp]:
"(! :X .. Qf)<<Pf = ! x:X .. (Qf x)<<Pf"
by (simp add: Rep_int_choice_com_def)
lemma Subst_procfun_Rep_int_choice_f[simp]:
"(!<f> :X .. Qf)<<Pf = !<f> x:X .. (Qf x)<<Pf"
by (simp add: Rep_int_choice_f_def)
lemma Subst_procfun_prod_p:
"(Pf <<< Qf) p = (Pf p) << Qf"
by (simp add: Subst_procfun_prod_def)
(*************************************************************
Syntactical functions
*************************************************************)
(*** guarded fun) ***)
consts
noPN :: "('p,'a) proc => bool" (* np Proc_name *)
gSKIP :: "('p,'a) proc => bool" (* guarded SKIP *)
noHide :: "('p,'a) proc => bool" (* no Hide *)
guarded:: "('p,'a) proc => bool" (* guarded proc *)
(*** noPN ***)
primrec
"noPN STOP = True"
"noPN SKIP = True"
"noPN DIV = True"
"noPN (a -> P) = noPN P"
"noPN (? :X -> Pf) = (ALL a. noPN (Pf a))"
"noPN (P [+] Q) = (noPN P & noPN Q)"
"noPN (P |~| Q) = (noPN P & noPN Q)"
"noPN (!nat :N .. Pf) = (ALL n. noPN (Pf n))"
"noPN (!set :Xs .. Pf) = (ALL X. noPN (Pf X))"
"noPN (IF b THEN P ELSE Q) = (noPN P & noPN Q)"
"noPN (P |[X]| Q) = (noPN P & noPN Q)"
"noPN (P -- X) = noPN P"
"noPN (P [[r]]) = noPN P"
"noPN (P ;; Q) = (noPN P & noPN Q)"
"noPN (P |. n) = noPN P"
"noPN ($p) = False"
(*** gSKIP ***)
primrec
"gSKIP STOP = True"
"gSKIP SKIP = False"
"gSKIP DIV = True"
"gSKIP (a -> P) = True"
"gSKIP (? :X -> Pf) = True"
"gSKIP (P [+] Q) = (gSKIP P & gSKIP Q)"
"gSKIP (P |~| Q) = (gSKIP P & gSKIP Q)"
"gSKIP (!nat :N .. Pf) = (ALL n. gSKIP (Pf n))"
"gSKIP (!set :Xs .. Pf) = (ALL X. gSKIP (Pf X))"
"gSKIP (IF b THEN P ELSE Q) = (gSKIP P & gSKIP Q)"
"gSKIP (P |[X]| Q) = (gSKIP P | gSKIP Q)"
"gSKIP (P -- X) = False"
"gSKIP (P [[r]]) = gSKIP P"
"gSKIP (P ;; Q) = (gSKIP P | gSKIP Q)"
"gSKIP (P |. n) = (gSKIP P | n=0)"
"gSKIP ($p) = False"
(*** no hide ***)
primrec
"noHide STOP = True"
"noHide SKIP = True"
"noHide DIV = True"
"noHide (a -> P) = noHide P"
"noHide (? :X -> Pf) = (ALL a. noHide (Pf a))"
"noHide (P [+] Q) = (noHide P & noHide Q)"
"noHide (P |~| Q) = (noHide P & noHide Q)"
"noHide (!nat :N .. Pf) = (ALL n. noHide (Pf n))"
"noHide (!set :Xs .. Pf) = (ALL X. noHide (Pf X))"
"noHide (IF b THEN P ELSE Q) = (noHide P & noHide Q)"
"noHide (P |[X]| Q) = (noHide P & noHide Q)"
"noHide (P -- X) = noPN P"
"noHide (P [[r]]) = noHide P"
"noHide (P ;; Q) = (noHide P & noHide Q)"
"noHide (P |. n) = (noHide P | n=0)"
"noHide ($p) = True"
(*** guarded ***)
primrec
"guarded STOP = True"
"guarded SKIP = True"
"guarded DIV = True"
"guarded (a -> P) = noHide P"
"guarded (? :X -> Pf) = (ALL a. noHide (Pf a))"
"guarded (P [+] Q) = (guarded P & guarded Q)"
"guarded (P |~| Q) = (guarded P & guarded Q)"
"guarded (!nat :N .. Pf) = (ALL n. guarded (Pf n))"
"guarded (!set :Xs .. Pf) = (ALL X. guarded (Pf X))"
"guarded (IF b THEN P ELSE Q) = (guarded P & guarded Q)"
"guarded (P |[X]| Q) = (guarded P & guarded Q)"
"guarded (P -- X) = noPN P"
"guarded (P [[r]]) = guarded P"
"guarded (P ;; Q) = ((guarded P & gSKIP P & noHide Q) |
(guarded P & guarded Q))"
"guarded (P |. n) = (guarded P | n=0)"
"guarded ($p) = False"
(*** for process function ***)
consts
noPNfun :: "('p => ('q,'a) proc) => bool"
gSKIPfun :: "('p => ('q,'a) proc) => bool"
noHidefun :: "('p => ('q,'a) proc) => bool"
guardedfun:: "('p => ('q,'a) proc) => bool"
defs
noPNfun_def : "noPNfun Pf == (ALL p. noPN (Pf p))"
gSKIPfun_def : "gSKIPfun Pf == (ALL p. gSKIP (Pf p))"
noHidefun_def : "noHidefun Pf == (ALL p. noHide (Pf p))"
guardedfun_def: "guardedfun Pf == (ALL p. guarded (Pf p))"
(****** short notations ******)
(* noPN *)
lemma noPN_Rep_int_choice_com[simp]:
"noPN (! :X .. Pf) = (ALL a. noPN (Pf a))"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done
lemma noPN_Rep_int_choice_f:
"[| inj f ; ALL a. noPN (Pf a) |] ==> noPN (!<f> :X .. Pf)"
by (simp add: Rep_int_choice_f_def)
lemma noPN_Alpha_parallel[simp]:
"noPN (P |[X,Y]| Q) = (noPN P & noPN Q)"
by (simp add: Alpha_parallel_def)
(* gSKIP *)
lemma gSKIP_Rep_int_choice_com[simp]:
"gSKIP (! :X .. Pf) = (ALL a. gSKIP (Pf a))"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done
lemma gSKIP_Rep_int_choice_f:
"[| inj f ; ALL a. gSKIP (Pf a) |] ==> gSKIP (!<f> :X .. Pf)"
by (simp add: Rep_int_choice_f_def)
lemma gSKIP_Alpha_parallel[simp]:
"gSKIP (P |[X,Y]| Q) = (gSKIP P | gSKIP Q)"
by (simp add: Alpha_parallel_def)
(* noHide *)
lemma noHide_Rep_int_choice_com[simp]:
"noHide (! :X .. Pf) = (ALL a. noHide (Pf a))"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done
lemma noHide_Rep_int_choice_f[simp]:
"[| inj f ; ALL a. noHide (Pf a) |]
==> noHide (!<f> :X .. Pf)"
by (simp add: Rep_int_choice_f_def)
lemma noHide_Alpha_parallel[simp]:
"noHide (P |[X,Y]| Q) = (noHide P & noHide Q)"
by (simp add: Alpha_parallel_def)
(* guarded *)
lemma guarded_Rep_int_choice_com[simp]:
"guarded (! :X .. Pf) = (ALL a. guarded (Pf a))"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done
lemma guarded_Rep_int_choice_f[simp]:
"[| inj f ; ALL a. guarded (Pf a) |]
==> guarded (!<f> :X .. Pf)"
by (simp add: Rep_int_choice_f_def)
lemma guarded_Alpha_parallel[simp]:
"guarded (P |[X,Y]| Q) = (guarded P & guarded Q)"
by (simp add: Alpha_parallel_def)
(*-----------------------------------------------------*
| Substitution |
*-----------------------------------------------------*)
lemma noPN_Subst_lm: "noPN P --> noPN (P<<Pf)"
apply (induct_tac P)
apply (simp_all)
done
lemma noPN_Subst: "noPN P ==> noPN (P<<Pf)"
by (simp add: noPN_Subst_lm)
lemma noPN_Subst_Pf: "noPNfun Pf ==> noPN (P<<Pf)"
apply (induct_tac P)
apply (simp_all)
apply (simp add: noPNfun_def)
done
lemma noHide_Subst_lm: "(noHide P & noHidefun Pf) --> noHide (P<<Pf)"
apply (induct_tac P)
apply (simp_all)
apply (simp add: noPN_Subst)
apply (force)
apply (simp add: noHidefun_def)
done
lemma noHide_Subst: "[| noHide P ; noHidefun Pf |] ==> noHide (P<<Pf)"
by (simp add: noHide_Subst_lm)
lemma gSKIP_Subst_lm: "(gSKIP P) --> gSKIP (P<<Pf)"
apply (induct_tac P)
apply (simp_all)
done
lemma gSKIP_Subst: "(gSKIP P) ==> gSKIP (P<<Pf)"
by (simp add: gSKIP_Subst_lm)
lemma guarded_Subst_lm: "(guarded P & noHidefun Pf) --> guarded (P<<Pf)"
apply (induct_tac P)
apply (simp_all)
apply (simp add: noHide_Subst)
apply (intro allI impI)
apply (simp add: noHide_Subst)
apply (simp add: noPN_Subst)
apply (intro allI impI)
apply (elim conjE exE disjE)
apply (simp add: gSKIP_Subst noHide_Subst)
apply (simp)
apply (force)
done
lemma guarded_Subst: "[| guarded P ; noHidefun Pf |] ==> guarded (P<<Pf)"
by (simp add: guarded_Subst_lm)
(*********************************************************
termination relation for proc
*********************************************************)
consts
procterm :: "(('p,'a) proc * ('p,'a) proc) set"
inductive procterm
intros
"(P, a -> P) : procterm"
"(Pf a, ? :X -> Pf) : procterm"
"(P, P [+] Q) : procterm"
"(Q, P [+] Q) : procterm"
"(P, P |~| Q) : procterm"
"(Q, P |~| Q) : procterm"
"(Pf n, !nat :N .. Pf) : procterm"
"(Pf X, !set :Xs .. Pf) : procterm"
"(P, IF b THEN P ELSE Q) : procterm"
"(Q, IF b THEN P ELSE Q) : procterm"
"(P, P |[X]| Q) : procterm"
"(Q, P |[X]| Q) : procterm"
"(P, P -- X) : procterm"
"(P, P [[r]]) : procterm"
"(P, P ;; Q) : procterm"
"(Q, P ;; Q) : procterm"
"(P, P |. n) : procterm"
lemma wf_procterm: "wf procterm"
apply (unfold wf_def)
apply (intro strip)
apply (induct_tac x)
apply (erule allE, erule mp, intro strip,
erule procterm.elims,
simp, simp, simp, simp, simp, simp,
simp, simp, simp, simp, simp, simp,
simp, simp, simp, simp, simp)+
done
(*-------------------------------------------------------*
| |
| decompostion controlled by Not_Decompo_Flag |
| |
*-------------------------------------------------------*)
consts Not_Decompo_Flag :: bool
defs Not_Decompo_Flag_def : "Not_Decompo_Flag == True"
lemma on_Not_Decompo_Flag: "Not_Decompo_Flag & R ==> R"
by (simp)
lemma off_Not_Decompo_Flag: "R ==> Not_Decompo_Flag & R"
by (simp add: Not_Decompo_Flag_def)
lemma off_Not_Decompo_Flag_True: "Not_Decompo_Flag"
by (simp add: Not_Decompo_Flag_def)
ML_setup {*
val ON_Not_Decompo_Flag = thms "on_Not_Decompo_Flag";
val OFF_Not_Decompo_Flag = thms "off_Not_Decompo_Flag";
val OFF_Not_Decompo_Flag_True = thms "off_Not_Decompo_Flag_True";
*}
(****************** to add them again ******************)
declare Union_image_eq [simp]
declare Inter_image_eq [simp]
end
lemmas csp_prefix_ss_def:
! :X -> Pf == ! x:X .. x -> Pf x
a ! x -> P == a x -> P
Nondet_send_prefix f X Pf == ! x:(f ` X) -> Pf (inv f x)
Rec_prefix f X Pf == ? x:(f ` X) -> Pf (inv f x)
lemmas csp_prefix_ss_def:
! :X -> Pf == ! x:X .. x -> Pf x
a ! x -> P == a x -> P
Nondet_send_prefix f X Pf == ! x:(f ` X) -> Pf (inv f x)
Rec_prefix f X Pf == ? x:(f ` X) -> Pf (inv f x)
lemma Rep_parallel_empty:
I = {} ==> [||]:I PXf = SKIP
lemma Rep_parallel_one:
I = {i} ==> [||]:I PXf = fst (PXf i) |[snd (PXf i),{}]| SKIP
lemma CPOmode_or_CMSmode_or_MIXmode_lm:
m = FPmode --> m = CPOmode ∨ m = CMSmode ∨ m = MIXmode
lemma CPOmode_or_CMSmode_or_MIXmode:
FPmode = CPOmode ∨ FPmode = CMSmode ∨ FPmode = MIXmode
lemma Subst_procfun_Rep_int_choice_com:
(! :X .. Qf) << Pf = ! x:X .. (Qf x) << Pf
lemma Subst_procfun_Rep_int_choice_f:
(!<f> :X .. Qf) << Pf = !<f> x:X .. (Qf x) << Pf
lemma Subst_procfun_prod_p:
Pf <<< Qf p = (Pf p) << Qf
lemma noPN_Rep_int_choice_com:
noPN (! :X .. Pf) = (∀a. noPN (Pf a))
lemma noPN_Rep_int_choice_f:
[| inj f; ∀a. noPN (Pf a) |] ==> noPN (!<f> :X .. Pf)
lemma noPN_Alpha_parallel:
noPN (P |[X,Y]| Q) = (noPN P ∧ noPN Q)
lemma gSKIP_Rep_int_choice_com:
gSKIP (! :X .. Pf) = (∀a. gSKIP (Pf a))
lemma gSKIP_Rep_int_choice_f:
[| inj f; ∀a. gSKIP (Pf a) |] ==> gSKIP (!<f> :X .. Pf)
lemma gSKIP_Alpha_parallel:
gSKIP (P |[X,Y]| Q) = (gSKIP P ∨ gSKIP Q)
lemma noHide_Rep_int_choice_com:
noHide (! :X .. Pf) = (∀a. noHide (Pf a))
lemma noHide_Rep_int_choice_f:
[| inj f; ∀a. noHide (Pf a) |] ==> noHide (!<f> :X .. Pf)
lemma noHide_Alpha_parallel:
noHide (P |[X,Y]| Q) = (noHide P ∧ noHide Q)
lemma guarded_Rep_int_choice_com:
guarded (! :X .. Pf) = (∀a. guarded (Pf a))
lemma guarded_Rep_int_choice_f:
[| inj f; ∀a. guarded (Pf a) |] ==> guarded (!<f> :X .. Pf)
lemma guarded_Alpha_parallel:
guarded (P |[X,Y]| Q) = (guarded P ∧ guarded Q)
lemma noPN_Subst_lm:
noPN P --> noPN (P << Pf)
lemma noPN_Subst:
noPN P ==> noPN (P << Pf)
lemma noPN_Subst_Pf:
noPNfun Pf ==> noPN (P << Pf)
lemma noHide_Subst_lm:
noHide P ∧ noHidefun Pf --> noHide (P << Pf)
lemma noHide_Subst:
[| noHide P; noHidefun Pf |] ==> noHide (P << Pf)
lemma gSKIP_Subst_lm:
gSKIP P --> gSKIP (P << Pf)
lemma gSKIP_Subst:
gSKIP P ==> gSKIP (P << Pf)
lemma guarded_Subst_lm:
guarded P ∧ noHidefun Pf --> guarded (P << Pf)
lemma guarded_Subst:
[| guarded P; noHidefun Pf |] ==> guarded (P << Pf)
lemma wf_procterm:
wf procterm
lemma on_Not_Decompo_Flag:
Not_Decompo_Flag ∧ R ==> R
lemma off_Not_Decompo_Flag:
R ==> Not_Decompo_Flag ∧ R
lemma off_Not_Decompo_Flag_True:
Not_Decompo_Flag