Theory CSP_syntax

           (*-------------------------------------------*
            |        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)   |
            |                                           |
            |        CSP-Prover on Isabelle2007         |
            |                January 2008  (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
 *********************************************************************)

types
   'a sets_nats = "('a set set, nat set) sum"
   'a aset_anat = "('a set, nat) sum"

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 "'a sets_nats" "'a aset_anat => ('p,'a) proc"
                                               ("(1!! :_ .. /_)" [900,68] 68) 
    | IF             "bool" "('p,'a) proc" "('p,'a) proc"
                                 ("(0IF _ /THEN _ /ELSE _)" [900,88,88] 88)
(*                               ("(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)
(*                                               ("(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":: 
      "pttrn => 'a sets_nats => ('p,'a) proc => ('p,'a) proc"  
                               ("(1!! _:_ .. /_)" [900,900,68] 68)
  "@Rep_int_choice_UNIV":: 
      "pttrn => ('p,'a) proc => ('p,'a) proc"
                               ("(1!! _ .. /_)" [900,68] 68)

translations
  "!! c:C .. P"    == "!! :C .. (%c. P)"
  "!! c .. P"      == "!! c:UNIV .. P"

(*** set, nat ***)

consts
  Rep_int_choice_set :: 
    "'a set set => ('a set => ('p,'a) proc) => ('p,'a) proc"
                                      ("(1!set :_ .. /_)" [900,68] 68)
  Rep_int_choice_nat ::
    "nat set => (nat => ('p,'a) proc) => ('p,'a) proc"
                                      ("(1!nat :_ .. /_)" [900,68] 68)

defs
  Rep_int_choice_set_def:
        "!set :Xs .. Pf == !! c:(type1 Xs) .. (Pf ((inv type1) c))"
  Rep_int_choice_nat_def:
        "!nat :N .. Pf == !! c:(type2 N) .. (Pf ((inv type2) c))"

(* bound variable *)

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

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

(* UNIV *)

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

translations
      "!set X .. P" == "!set X:UNIV .. P"
      "!nat n .. P" == "!nat n: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"

lemmas Rep_int_choice_ss_def =
       Rep_int_choice_set_def
       Rep_int_choice_nat_def
       Rep_int_choice_com_def
       Rep_int_choice_f_def

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

(*
The sending "a ! v -> P" causes syntactical ambiguity.
So, it is recommended to directly use "a v -> P" instead of "a ! v -> P".
*)

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

abbreviation
   Interleave :: "('p,'a) proc => ('p,'a) proc
                    => ('p,'a) proc"  ("(1_ /||| _)" [76,77] 76)
where "P ||| Q == P |[{}]| Q"

abbreviation
   Synchro   :: "('p,'a) proc => ('p,'a) proc
                    => ('p,'a) proc"  ("(1_ /|| _)" [76,77] 76)
where "P || Q == P |[UNIV]| Q"

(*
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[||] _)" [78] 78)

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,78] 78)

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,78] 78)

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

abbreviation
 Timeout_abb :: "('p,'a) proc => ('p,'a) proc 
             => ('p,'a) proc"  ("(1_ /[> _)" [73,74] 73)
 where "P [> Q == (P |~| STOP) [+] Q"

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


(*===================================================================*

(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)

(*-------*
 | 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"
  "(!! :C .. Qf)<<Pf = !! c:C .. (Qf c)<<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)"

(* lemmas *)

lemma Subst_procfun_Rep_int_choice_set[simp]:
  "(!set :Xs .. Qf)<<Pf      = !set X:Xs .. (Qf X)<<Pf"
by (simp add: Rep_int_choice_ss_def)

lemma Subst_procfun_Rep_int_choice_nat[simp]:
  "(!nat :N .. Qf)<<Pf      = !nat n:N .. (Qf n)<<Pf"
by (simp add: Rep_int_choice_ss_def)

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"   (* no 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 (!! :C .. Pf) = (ALL c. noPN (Pf c))"
  "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 (!! :C .. Pf) = (ALL c. gSKIP (Pf c))"
  "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 (!! :C .. Pf) = (ALL c. noHide (Pf c))"
  "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 (!! :C .. Pf) = (ALL c. guarded (Pf c))"
  "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_set[simp]:
  "noPN (!set :Xs .. Pf) = (ALL X. noPN (Pf X))"
by (simp add: Rep_int_choice_ss_def)

lemma noPN_Rep_int_choice_nat[simp]:
  "noPN (!nat :N .. Pf) = (ALL n. noPN (Pf n))"
by (simp add: Rep_int_choice_ss_def)

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[simp]:
  "[| 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_set[simp]:
  "gSKIP (!set :Xs .. Pf) = (ALL X. gSKIP (Pf X))"
by (simp add: Rep_int_choice_ss_def)

lemma gSKIP_Rep_int_choice_nat[simp]:
  "gSKIP (!nat :N .. Pf) = (ALL n. gSKIP (Pf n))"
by (simp add: Rep_int_choice_ss_def)

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[simp]:
  "[| 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_set[simp]:
  "noHide (!set :Xs .. Pf) = (ALL X. noHide (Pf X))"
by (simp add: Rep_int_choice_ss_def)

lemma noHide_Rep_int_choice_nat[simp]:
  "noHide (!nat :N .. Pf) = (ALL n. noHide (Pf n))"
by (simp add: Rep_int_choice_ss_def)

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_set[simp]:
  "guarded (!set :Xs .. Pf) = (ALL X. guarded (Pf X))"
by (simp add: Rep_int_choice_ss_def)

lemma guarded_Rep_int_choice_nat[simp]:
  "guarded (!nat :N .. Pf) = (ALL n. guarded (Pf n))"
by (simp add: Rep_int_choice_ss_def)

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

(* Isabelle 2005
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 c, !! :C .. 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"
*)

inductive_set
  procterm :: "(('p,'a) proc * ('p,'a) proc) set"
where
  "(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 c, !! :C .. 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.cases,
         simp, simp, simp, simp, simp, simp,
         simp, simp, simp, simp, simp, simp,
         simp, simp, simp, simp)+
done

(* procterm.elims in Isabelle 2005 
   -->  procterm.cases in Isabelle 2007 *)

(*-------------------------------------------------------* 
 |                                                       |
 |      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";
*}
for Isabelle 2007
*)

ML {*
    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