Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover
theory CSP_syntax = Complex_Main:(*-------------------------------------------*
| CSP-Prover |
| December 2004 |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_syntax = Complex_Main:
(*-----------------------------------------------------------*
| |
| Process Type Definitions |
| |
| ('n,'a) proc : type of process expressions |
| 'n : process name |
| 'a : event |
| |
*-----------------------------------------------------------*)
(*********************************************************************
process expression
*********************************************************************)
datatype
('n,'a) proc
= STOP
| SKIP
| DIV
| Act_prefix "'a" "('n,'a) proc" ("(1_ /-> _)" [150,80] 80)
| Ext_pre_choice "'a set" "'a => ('n,'a) proc"
("(1? :_ /-> _)" [90,80] 80)
| Ext_choice "('n,'a) proc" "('n,'a) proc"
("(1_ /[+] _)" [72,73] 72)
| Int_choice "('n,'a) proc" "('n,'a) proc"
("(1_ /|~| _)" [64,65] 64)
| Rep_int_choice "'a set" "'a => ('n,'a) proc"
("(1! :_ .. /_)" [0,68] 68)
| Conditional "bool" "('n,'a) proc" "('n,'a) proc"
("(0IF _ /THEN _ /ELSE _)" [900,60,60] 88)
| Parallel "('n,'a) proc" "'a set" "('n,'a) proc"
("(1_ /|[_]| _)" [76,0,77] 76)
| Hiding "('n,'a) proc" "'a set" ("(1_ /-- _)" [84,85] 84)
| Renaming "('n,'a) proc" "('a * 'a) set"
("(1_ /[[_]])" [84,0] 84)
| Seq_compo "('n,'a) proc" "('n,'a) proc"
("(1_ /;; _)" [79,78] 78)
| Proc_name "'n" ("<_>" [0] 90)
(*--------------------------------------------------------------------*
| |
| (1) binding power: |
| Proc_name > Conditional > {Hiding, Renaming} > |
| {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) DIV is a short notation as follows: DIV = ! {} .. (%x. STOP) |
| |
| (3) About ("(1_ /-> _)" [150,80] 80) |
| The nth operator ! has the power 101. |
| So, 150 > 101 is needed. |
| |
*--------------------------------------------------------------------*)
(*** external prefix ***)
syntax
"@Ext_pre_choice" :: "pttrn => 'a set => ('n,'a) proc
=> ('n,'a) proc" ("(1? _:_ /-> _)" [900,900,80] 80)
translations
"? x:X -> P" == "? :X -> (%x. P)"
(*** internal prefix choice ***)
consts
Int_pre_choice :: "'a set => ('a => ('n,'a) proc) => ('n,'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 => ('n,'a) proc
=> ('n,'a) proc" ("(1! _:_ /-> _)" [900,900,80] 80)
translations
"! x:X -> P" == "! :X -> (%x. P)"
(*** sending and receiving prefixes ***)
consts
Send_prefix :: "('x => 'a) => 'x => ('n,'a) proc => ('n,'a) proc"
("(1_ ! _ /-> _)" [900,1000,80] 80)
Nondet_send_prefix :: "('x => 'a) => 'x set =>
('x => ('n,'a) proc) => ('n,'a) proc"
Rec_prefix :: "('x => 'a) => 'x set =>
('x => ('n,'a) proc) => ('n,'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 => ('n,'a) proc => ('n,'a) proc"
("(1_ !! _:_ /-> _)" [900,900,1000,80] 80)
"@Nondet_send_prefix_UNIV" ::
"('x => 'a) => pttrn => ('n,'a) proc => ('n,'a) proc"
("(1_ !! _ /-> _)" [900,900,80] 80)
"@Rec_prefix" ::
"('x => 'a) => pttrn => 'x set => ('n,'a) proc => ('n,'a) proc"
("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
"@Rec_Prefix_UNIV" ::
"('x => 'a) => pttrn => ('n,'a) proc => ('n,'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"
(*** internal choice ***)
consts
Rep_int_choice_fun ::
"('x => 'a) => 'x set => ('x => ('n,'a) proc) => ('n,'a) proc"
defs
Rep_int_choice_fun_def :
"Rep_int_choice_fun f X Pf == ! :(f ` X) .. (%x. (Pf ((inv f) x)))"
syntax
"@Rep_int_choice"::
"pttrn => 'a set => ('n,'a) proc => ('n,'a) proc"
("(1! _:_ .. /_)" [900,900,68] 68)
"@Rep_int_choice_fun" ::
"('x => 'a) => pttrn => 'x set => ('n,'a) proc => ('n,'a) proc"
("(1_ !! _:_ .. /_)" [900,900,1000,80] 80)
"@Rep_int_choice_fun_UNIV" ::
"('x => 'a) => pttrn => ('n,'a) proc => ('n,'a) proc"
("(1_ !! _ .. /_)" [900,900,80] 80)
translations
"! x:X .. P" == "! :X .. (%x. P)"
"a !! x:X .. P" == "Rep_int_choice_fun a X (%x. P)"
"a !! x .. P" == "a !! x:UNIV .. P"
(*** parallel ***)
syntax
"_Interleave" :: "('n,'a) proc => ('n,'a) proc
=> ('n,'a) proc" ("(1_ ||| _)" [76,77] 76)
"_Synchro" :: "('n,'a) proc => ('n,'a) proc
=> ('n,'a) proc" ("(1_ || _)" [76,77] 76)
translations
"P ||| Q" == "P |[{}]| Q"
"P || Q" == "P |[UNIV]| Q"
consts
Alpha_parallel :: "('n,'a) proc => 'a set => 'a set => ('n,'a) proc
=> ('n,'a) proc" ("(1_ |[_,_]| _)" [76,0,0,77] 76)
defs
Alpha_parallel_def :
"P |[X,Y]| Q == (P |[UNIV - X]| STOP) |[X Int Y]| (Q |[UNIV - Y]| STOP)" (* ? *)
(*** timeout ***)
syntax
"_Timeout" :: "('n,'a) proc => ('n,'a) proc
=> ('n,'a) proc" ("(1_ /[> _)" [73,74] 73)
translations
"P [> Q" == "(P |~| STOP) [+] Q"
(*------------------------------------*
| |
| X-Symbols |
| |
*------------------------------------*)
syntax (output)
"_PrefixX" :: "'a => ('n,'a) proc => ('n,'a) proc"
("(1_ /-> _)" [150,80] 80)
"_Ext_pre_choiceX" :: "pttrn => 'a set => ('n,'a) proc => ('n,'a) proc"
("(1? _:_ /-> _)" [900,900,80] 80)
"_Ext_choiceX" :: "('n,'a) proc => ('n,'a) proc => ('n,'a) proc"
("(1_ /[+] _)" [72,73] 72)
"_Int_choiceX" :: "('n,'a) proc => ('n,'a) proc => ('n,'a) proc"
("(1_ /|~| _)" [64,65] 64)
"_Rep_int_choiceX" :: "pttrn => 'a set => ('n,'a) proc
=> ('n,'a) proc" ("(1! _:_ .. /_)" [900,900,68] 68)
"_Int_pre_choiceX" :: "pttrn => 'a set => ('n,'a) proc => ('n,'a) proc"
("(1! _:_ /-> _)" [900,900,80] 80)
"_Rep_int_choiceX" :: "('x => 'a) => pttrn => 'x set =>
('n,'a) proc => ('n,'a) proc"
("(1_ !! _:_ .. /_)" [900,900,1000,80] 80)
"_Rep_int_choice_UNIVX" :: "('x => 'a) => pttrn =>
('n,'a) proc => ('n,'a) proc"
("(1_ !! _ .. /_)" [900,900,80] 80)
syntax (xsymbols)
"_PrefixX" :: "'a => ('n,'a) proc => ('n,'a) proc"
("(1_ /-> _)" [150,80] 80)
"_Ext_pre_choiceX" :: "pttrn => 'a set => ('n,'a) proc => ('n,'a) proc"
("(1? _:_ /-> _)" [900,900,80] 80)
"_Ext_choiceX" :: "('n,'a) proc => ('n,'a) proc => ('n,'a) proc"
("(1_ /\<box> _)" [72,73] 72)
"_Int_choiceX" :: "('n,'a) proc => ('n,'a) proc => ('n,'a) proc"
("(1_ /\<sqinter> _)" [64,65] 64)
"_Rep_int_choiceX" :: "pttrn => 'a set => ('n,'a) proc
=> ('n,'a) proc" ("(1! _:_ \<bullet> /_)" [900,900,68] 68)
"_Int_pre_choiceX" :: "pttrn => 'a set => ('n,'a) proc => ('n,'a) proc"
("(1! _:_ /-> _)" [900,900,80] 80)
"_Rep_int_choiceX" :: "('x => 'a) => pttrn => 'x set =>
('n,'a) proc => ('n,'a) proc"
("(1_ !! _:_ \<bullet> /_)" [900,900,1000,80] 80)
"_Rep_int_choice_UNIVX" :: "('x => 'a) => pttrn =>
('n,'a) proc => ('n,'a) proc"
("(1_ !! _ \<bullet> /_)" [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 \<bullet> P" == "! x:X .. P"
"! x:X -> P" == "! x:X -> P"
"a !! x:X \<bullet> P" == "a !! x:X .. P"
"a !! x \<bullet> P" == "a !! x:UNIV \<bullet> P"
syntax (output)
"_Nondet_send_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('n,'a) proc => ('n,'a) proc"
("(1_ !! _:_ /-> _)" [900,900,1000,80] 80)
"_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => ('n,'a) proc => ('n,'a) proc"
("(1_ !! _ /-> _)" [900,900,80] 80)
"_Send_prefixX" :: "('x => 'a) => 'x => ('n,'a) proc => ('n,'a) proc"
("(1_ ! _ /-> _)" [900,1000,80] 80)
"_Rec_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('n,'a) proc => ('n,'a) proc"
("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
"_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
('n,'a) proc => ('n,'a) proc"
("(1_ ? _ /-> _)" [900,900,80] 80)
syntax (xsymbols)
"_Nondet_send_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('n,'a) proc => ('n,'a) proc"
("(1_ !! _:_ /-> _)" [900,900,1000,80] 80)
"_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => ('n,'a) proc => ('n,'a) proc"
("(1_ !! _ /-> _)" [900,900,80] 80)
"_Send_prefixX" :: "('x => 'a) => 'x => ('n,'a) proc => ('n,'a) proc"
("(1_ ! _ /-> _)" [900,1000,80] 80)
"_Rec_prefixX" :: "('x => 'a) => pttrn => 'x set =>
('n,'a) proc => ('n,'a) proc"
("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
"_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
('n,'a) proc => ('n,'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" :: "'n => ('n,'a) proc" ("<_>" [0] 90)
"_TimeoutX" :: "('n,'a) proc => ('n,'a) proc
=> ('n,'a) proc" ("(1_ /[> _)" [73,74] 73)
"_HidingX" :: "('n,'a) proc => 'a set => ('n,'a) proc"
("(1_ /-- _)" [84,85] 84)
"_RenamingX" :: "('n,'a) proc => ('a * 'a) set => ('n,'a) proc"
("(1_ /[[_]])" [84,0] 84)
syntax (xsymbols)
"_Proc_nameX" :: "'n => ('n,'a) proc" ("〈_〉" [0] 90)
"_TimeoutX" :: "('n,'a) proc => ('n,'a) proc
=> ('n,'a) proc" ("(1_ /\<rhd> _)" [73,74] 73)
"_HidingX" :: "('n,'a) proc => 'a set => ('n,'a) proc"
("(1_ /\<midarrow> _)" [84,85] 84)
"_RenamingX" :: "('n,'a) proc => ('a * 'a) set => ('n,'a) proc"
("(1_ /[|_|])" [84,0] 84)
translations
"〈C〉" == "<C>"
"P \<rhd> Q" == "(P |~| STOP) [+] Q"
"P \<midarrow> X" == "P -- X"
"P [|r|]" == "P [[r]]"
(*********************************************************************
recursive process
*********************************************************************)
datatype fp_type = Ufp | Lfp
types ('n,'a) procDF = "'n => ('n,'a) proc" (* synonym *)
datatype
('n,'a) procRC
= Letin "fp_type" "('n,'a) procDF" "('n,'a) proc"
("//(2LET:_ /_ )/(2IN /_)/" [53,53,53] 53)
(*
syntax
"_LetinUFP" :: "('n,'a) procDF => ('n,'a) proc => ('n,'a) procRC"
("//(2LET /_ )/(2IN /_)/" [53,53] 53)
translations
"LET df IN P" == "LET:Ufp df IN P" (* default LET _ IN _ *)
*)
(*********************************************************************
name and proc from Letin
*********************************************************************)
consts
LetF :: "('n,'a) procRC => fp_type"
LetD :: "('n,'a) procRC => ('n,'a) procDF"
InP :: "('n,'a) procRC => ('n,'a) proc"
primrec "LetF (LET:fp df IN P) = fp"
primrec "LetD (LET:fp df IN P) = df"
primrec "InP (LET:fp df IN P) = P"
(****************** lemma *****************)
lemma fp_type_is: "((fp::fp_type) = Ufp) | (fp = Lfp)"
apply (induct_tac fp)
by (auto)
lemma LetD_InP: "LET:(LetF R) LetD R IN InP R = R"
apply (induct_tac R)
by (auto)
(*================================================*
| Short notation for non-recursive processes |
*================================================*)
datatype NoRec = NoUse
consts
NoDef :: "(NoRec, 'a) procDF"
primrec
"NoDef (NoUse) = DIV"
syntax
"_LETIN" :: "(NoRec,'a) proc => (NoRec,'a) procRC"
("(2LET-IN /_)" [53] 53)
translations
"LET-IN P" == "LET:Ufp NoDef IN P"
(*************************************************************
Syntactical functions
*************************************************************)
(*** guarded (proc) ***)
consts
guard :: "('n,'a) proc => bool"
primrec
"guard STOP = True"
"guard SKIP = True"
"guard DIV = True"
"guard (a -> P) = True"
"guard (? :X -> Pf) = True"
"guard (P [+] Q) = (guard P & guard Q)"
"guard (P |~| Q) = (guard P & guard Q)"
"guard (! :X .. Pf) = (ALL x. guard (Pf x))"
"guard (IF b THEN P ELSE Q) = (guard P & guard Q)"
"guard (P |[X]| Q) = (guard P & guard Q)"
"guard (P -- X) = guard P"
"guard (P [[r]]) = guard P"
"guard (P ;; Q) = (guard P & guard Q)"
"guard (<C>) = False"
(*** nohide (proc) ***)
consts
nohide :: "('n,'a) proc => bool"
primrec
"nohide STOP = True"
"nohide SKIP = True"
"nohide DIV = True"
"nohide (a -> P) = nohide P"
"nohide (? :X -> Pf) = (ALL x. nohide (Pf x))"
"nohide (P [+] Q) = (nohide P & nohide Q)"
"nohide (P |~| Q) = (nohide P & nohide Q)"
"nohide (! :X .. 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) = False"
"nohide (P [[r]]) = nohide P"
"nohide (P ;; Q) = (nohide P & nohide Q)"
"nohide (<C>) = True"
(*** extending function over processes from process-names ***)
consts
rewrite_by :: "('n,'a) proc => ('n => ('m,'a) proc) => ('m,'a) proc"
("(Rewrite _ By _)" [1000,1000] 100)
primrec
"Rewrite STOP By f = STOP"
"Rewrite SKIP By f = SKIP"
"Rewrite DIV By f = DIV"
"Rewrite (a -> P) By f = a -> (Rewrite P By f)"
"Rewrite (? :X -> Pf) By f = ? :X -> (%x. (Rewrite (Pf x) By f))"
"Rewrite (P [+] Q) By f = (Rewrite P By f) [+] (Rewrite Q By f)"
"Rewrite (P |~| Q) By f = (Rewrite P By f) |~| (Rewrite Q By f)"
"Rewrite (! :X .. Pf) By f = ! :X .. (%x. (Rewrite (Pf x) By f))"
"Rewrite (IF b THEN P ELSE Q) By f
= IF b THEN (Rewrite P By f) ELSE (Rewrite Q By f)"
"Rewrite (P |[X]| Q) By f = (Rewrite P By f) |[X]| (Rewrite Q By f)"
"Rewrite (P -- X) By f = (Rewrite P By f) -- X"
"Rewrite (P [[r]]) By f = (Rewrite P By f) [[r]]"
"Rewrite (P ;; Q) By f = (Rewrite P By f) ;; (Rewrite Q By f)"
"Rewrite (<C>) By f = f C"
(*********************************************************
termination relation for proc
*********************************************************)
consts
procterm :: "(('n,'a) proc * ('n,'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 a, ! :X .. 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"
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)+
done
(****************************************************************
procterm Test
The following guardrec is easily defined by primrec.
This is an example for showing how to use procterm for recdef.
An advantage for using recdef is that matching can be used.
****************************************************************)
(*
consts
guardrec :: "('n,'a) proc => bool"
recdef guardrec "procterm"
"guardrec STOP = True"
"guardrec SKIP = True"
"guardrec DIV = True"
"guardrec (a -> P) = True"
"guardrec (? :X -> Pf) = True"
"guardrec (P [+] Q) = (guardrec P & guardrec Q)"
"guardrec (P |~| Q) = (guardrec P & guardrec Q)"
"guardrec (! :X .. Pf) = (ALL x. guardrec (Pf x))"
"guardrec (IF b THEN P ELSE Q) = (guardrec P & guardrec Q)"
"guardrec (P |[X]| Q) = (guardrec P & guardrec Q)"
"guardrec (P -- X) = guardrec P"
"guardrec (P [[r]]) = guardrec P"
"guardrec (P ;; Q) = (guardrec P & guardrec Q)"
"guardrec (<C>) = False"
(hints recdef_wf add: wf_procterm intro: procterm.intros)
*)
(*********************************************************
Guared Test
*********************************************************)
(*
datatype abcType = a | b |c
datatype testprocNameType = A nat | B nat | C
consts
testSYSdef :: "(testprocNameType, abcType) procDF"
primrec
"testSYSdef (A n) = a -> <B (n+1)>"
"testSYSdef (B n) = b -> <A (n+1)> [+] c -> <C>"
"testSYSdef (C) = (b -> SKIP) ;; a -> <A 0>"
lemma "!! C. guardrec(testSYSdef C)"
apply (induct_tac C)
apply (simp_all)
done
*)
end
lemma fp_type_is:
fp = Ufp ∨ fp = Lfp
lemma LetD_InP:
LET:LetF R LetD R IN InP R = R
lemma wf_procterm:
wf procterm