Theory CSP_syntax

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               November 2004               |
            |                   June 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_syntax = Infra:

(*  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         |
 |                       'a : event                          |
 |                                                           |
 *-----------------------------------------------------------*)

(*********************************************************************
                       process expression
 *********************************************************************)

datatype 
 'a proc
    = STOP

    | SKIP

    | DIV

    | Act_prefix     "'a" "'a proc"      ("(1_ /-> _)" [150,80] 80)

    | Ext_pre_choice "'a set" "'a => 'a proc"
                                               ("(1? :_ /-> _)" [900,80] 80)
    | Ext_choice     "'a proc" "'a proc"  
                                               ("(1_ /[+] _)" [72,73] 72)
    | Int_choice     "'a proc" "'a proc"  
                                               ("(1_ /|~| _)" [64,65] 64)
    | Rep_int_choice "'a selector set" "'a selector => 'a proc"
                                               ("(1!! :_ .. /_)" [900,68] 68) 
    | IF             "bool" "'a proc" "'a proc"
                                 ("(0IF _ /THEN _ /ELSE _)" [900,60,60] 88)
    | Parallel       "'a proc" "'a set" "'a proc"  
                                               ("(1_ /|[_]| _)" [76,0,77] 76)
    | Hiding         "'a proc" "'a set"   ("(1_ /-- _)" [84,85] 84)

    | Renaming       "'a proc" "('a * 'a) set"
                                               ("(1_ /[[_]])" [84,0] 84)
    | Seq_compo      "'a proc" "'a proc"  
                                               ("(1_ /;; _)" [79,78] 78)
    | Depth_rest     "'a proc" "nat"  
                                               ("(1_ /|. _)" [84,900] 84)

(*--------------------------------------------------------------------*
 |                                                                    |
 | (1) binding power:                                                 |
 |      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 => 'a proc 
                => 'a proc"  ("(1? _:_ /-> _)" [900,900,80] 80)

translations
  "? x:X -> P"  == "? :X -> (%x. P)"

(*** internal choice ***)

consts
  Rep_int_choice_fun :: "('b => ('a selector))
                         => 'b set => ('b => 'a proc) => 'a proc"
                                      ("(1!!<_> :_ .. /_)" [0,900,68] 68)
defs
  Rep_int_choice_fun_def : 
        "!!<f> :X .. Pf == !! :(f ` X) .. (%x. (Pf ((inv f) x)))"

(********* internal choice *********)

syntax
  "@Rep_int_choice":: 
      "pttrn => ('a selector) set => 'a proc => 'a proc"  
                               ("(1!! _:_ .. /_)" [900,900,68] 68)
  "@Rep_int_choice_UNIV":: 
      "pttrn => 'a proc => 'a proc"  
                               ("(1!! _ .. /_)" [900,68] 68)

  "@Rep_int_choice_fun":: 
  "('b => ('a selector)) => pttrn => 'b set => 'a proc => 'a proc"
                               ("(1!!<_> _:_ .. /_)" [0,900,900,68] 68)

  "@Rep_int_choice_UNIV_fun":: 
  "('b => ('a selector)) => pttrn => 'a proc => 'a proc"
                               ("(1!!<_> _ .. /_)" [0,900,68] 68)

translations
  "!! c:C .. P"    == "!! :C .. (%c. P)"
  "!! c .. P"      == "!! c:UNIV .. P"
  "!!<f> x:X .. P" == "!!<f> :X .. (%x. P)"
  "!!<f> x .. P"   == "!!<f> x:UNIV .. P"

(*** set, nat **)

syntax
  "@Rep_int_choice_fun_set" :: "('a set) set => ('a set => 'a proc) => 'a proc"
                                      ("(1!set :_ .. /_)" [900,68] 68)
  "@Rep_int_choice_fun_nat" :: "nat set => (nat => 'a proc) => 'a proc"
                                      ("(1!nat :_ .. /_)" [900,68] 68)

translations
        "!set :Xs .. Pf" == "!!<sel_set> :Xs .. Pf"
        "!nat :N .. Pf" == "!!<sel_nat> :N .. Pf"

syntax
  "@Rep_int_choice_set" :: "pttrn => ('a set) set => ('a set => 'a proc) => 'a proc"
                                      ("(1!set _:_ .. /_)" [900,900,68] 68)
  "@Rep_int_choice_nat" :: "pttrn => nat set => (nat => 'a proc) => '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)"

syntax
  "@Rep_int_choice_set_UNIV" :: "pttrn => ('a set => 'a proc) => 'a proc"
                                      ("(1!set _ .. /_)" [900,68] 68)
  "@Rep_int_choice_nat_UNIV" :: "pttrn => (nat => 'a proc) => '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 => 'a proc) => '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 => 'a proc) => 'a proc"
                                      ("(1! _:_ .. /_)" [900,900,68] 68)
  "@Rep_int_choice_com_UNIV" :: "pttrn => ('a => 'a proc) => '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 => 'a proc) => '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 => 'a proc => 'a proc"
                                      ("(1!<_> _:_ .. /_)" [0,900,900,68] 68)
  "@Rep_int_choice_f_UNIV":: "('b => 'a) => pttrn => 'a proc => '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 => 'a proc) => '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 => 'a proc 
                         => 'a proc"  ("(1! _:_ /-> _)" [900,900,80] 80)

  "@Int_pre_choice_UNIV" ::  "pttrn => 'a proc => '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 => 'a proc => 'a proc" 
                                      ("(1_ ! _ /-> _)" [900,1000,80] 80)
  Nondet_send_prefix :: "('x => 'a) => 'x set => 
                         ('x => 'a proc) => 'a proc" 
  Rec_prefix  :: "('x => 'a) => 'x set => 
                  ('x => 'a proc) => '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 => 'a proc => 'a proc"
                               ("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)

  "@Nondet_send_prefix_UNIV" :: 
     "('x => 'a) => pttrn => 'a proc => 'a proc"
                               ("(1_ !? _ /-> _)" [900,900,80] 80)

  "@Rec_prefix" :: 
     "('x => 'a) => pttrn => 'x set => 'a proc => 'a proc"
                               ("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
  "@Rec_Prefix_UNIV" :: 
     "('x => 'a) => pttrn => 'a proc => '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"    :: "'a proc => 'a proc
                    => 'a proc"  ("(1_ /||| _)" [76,77] 76)
  "_Synchro"       :: "'a proc => 'a proc
                    => 'a proc"  ("(1_ /|| _)" [76,77] 76)

translations
  "P ||| Q"     == "P |[{}]| Q"
  "P || Q"      == "P |[UNIV]| Q"

consts
  Alpha_parallel :: "'a proc => 'a set => 'a set => 'a proc
                      => '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 :: "('a proc * 'a set) list
                   => 'a proc"  ("(1[||] _)" [77] 77)

primrec
  "[||] [] = SKIP"
  "[||] (PX # PXs) = (fst PX) |[snd PX, Union (snd ` set PXs)]| ([||] PXs)"

consts
  Rep_parallel :: "'i set => ('i => ('a proc * 'a set))
                      => '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 => ('a proc * 'a set)
                      => '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"  :: "'a proc => 'a proc 
               => 'a proc"  ("(1_ /[> _)" [73,74] 73)
translations
  "P [> Q"      == "(P |~| STOP) [+] Q"

(*** it is sometimes useful to prevent automatical unfolding [> ***)

consts
  Timeout  :: "'a proc => 'a proc 
               => 'a proc"  ("(1_ /[>def _)" [73,74] 73)
defs
  Timeout_def : "P [>def Q == P [> Q"

(*------------------------------------*
 |                                    |
 |              X-Symbols             |
 |                                    |
 *------------------------------------*)

syntax (output)
  "_PrefixX"         :: "'a => 'a proc => 'a proc"
                                   ("(1_ /-> _)" [150,80] 80)
  "_Ext_pre_choiceX" :: "pttrn => 'a set => 'a proc => 'a proc"  
                                   ("(1? _:_ /-> _)" [900,900,80] 80)
  "_Ext_choiceX"     :: "'a proc => 'a proc => 'a proc"
                                   ("(1_ /[+] _)" [72,73] 72)
  "_Int_choiceX"     :: "'a proc => 'a proc => 'a proc"
                                   ("(1_ /|~| _)" [64,65] 64)
  "_Int_pre_choiceX" :: "pttrn => 'a set => 'a proc => 'a proc"  
                                   ("(1! _:_ /-> _)" [900,900,80] 80)

syntax (xsymbols)
  "_PrefixX"         :: "'a => 'a proc => 'a proc"
                          ("(1_ /-> _)" [150,80] 80)
  "_Ext_pre_choiceX" :: "pttrn => 'a set => 'a proc => 'a proc"  
                          ("(1? _:_ /-> _)" [900,900,80] 80)
  "_Ext_choiceX"     :: "'a proc => 'a proc => 'a proc"
                          ("(1_ /\<box> _)" [72,73] 72)
  "_Int_choiceX"     :: "'a proc => 'a proc => 'a proc"
                          ("(1_ /\<sqinter> _)" [64,65] 64)

  "_Int_pre_choiceX" :: "pttrn => 'a set => 'a proc => '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 => 
                                  'a proc => 'a proc"
                                  ("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)
  "_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => 'a proc => 'a proc"
                               ("(1_ !? _ /-> _)" [900,900,80] 80)

  "_Send_prefixX"     :: "('x => 'a) => 'x => 'a proc => 'a proc" 
                          ("(1_ ! _ /-> _)" [900,1000,80] 80)

  "_Rec_prefixX"      :: "('x => 'a) => pttrn => 'x set => 
                          'a proc => 'a proc"
                          ("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
  "_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
                          'a proc => 'a proc"
                          ("(1_ ? _ /-> _)" [900,900,80] 80)

syntax (xsymbols)
  "_Nondet_send_prefixX"      :: "('x => 'a) => pttrn => 'x set => 
                                  'a proc => 'a proc"
                               ("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)
  "_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => 'a proc => 'a proc"
                               ("(1_ !? _ /-> _)" [900,900,80] 80)

  "_Send_prefixX"     :: "('x => 'a) => 'x => 'a proc => 'a proc" 
                          ("(1_ ! _ /-> _)" [900,1000,80] 80)

  "_Rec_prefixX"      :: "('x => 'a) => pttrn => 'x set => 
                          'a proc => 'a proc"
                          ("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
  "_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
                          'a proc => '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 => 'a proc" ("<_>" [0] 90)
  "_TimeoutX"   :: "'a proc => 'a proc 
                 => 'a proc"  ("(1_ /[> _)" [73,74] 73)
  "_TimeoutdefX" :: "'a proc => 'a proc 
                 => 'a proc"  ("(1_ /[>def _)" [73,74] 73)
  "_HidingX"    :: "'a proc => 'a set => 'a proc"  
                                        ("(1_ /-- _)" [84,85] 84)
  "_RenamingX"  :: "'a proc => ('a * 'a) set => 'a proc"  
                                        ("(1_ /[[_]])" [84,0] 84)
  "_Depth_rest" :: "'a proc => 'a proc 
                 => 'a proc"   ("(1_ /|. _)" [84,900] 84)

syntax (xsymbols)
  "_Proc_nameX" :: "'n => 'a proc" ("⟨_⟩" [0] 90)
  "_TimeoutX"   :: "'a proc => 'a proc 
                 => 'a proc"  ("(1_ /\<rhd> _)" [73,74] 73)
  "_TimeoutdefX":: "'a proc => 'a proc 
                 => 'a proc"  ("(1_ /\<unrhd> _)" [73,74] 73)
  "_HidingX"    :: "'a proc => 'a set => 'a proc"  
                                   ("(1_ /\<midarrow> _)" [84,85] 84)
  "_RenamingX"  :: "'a proc => ('a * 'a) set => 'a proc"  
                                        ("(1_ /[|_|])" [84,0] 84)
  "_Depth_rest" :: "'a proc => 'a proc 
                 => '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"

(*********************************************************************
             recursive process (fixed point) and
         process expression (process with variable)
 *********************************************************************)

types ('p,'a) procfun = "('p => 'a proc) => 'a proc"
types ('p,'a) procFun = "('p => 'a proc) => ('p => 'a proc)"
types ('p,'a) procDef = "(('p => 'a proc) * 'p) => 'a proc"

(* Tarski's fixed point *)

consts
 FIXn :: "nat => ('p,'a) procFun => ('p => 'a proc)"  ("FIX[_] _" [0,1000] 55)
 FIX  :: "('p,'a) procFun => ('p => 'a proc)"  ("FIX _" [1000] 55)

defs
 FIXn_def :  "FIX[n] PF == (PF^n) (%q. DIV)"
 FIX_def  :     "FIX PF == (%p. (!nat n .. ((FIX[n] PF) p)))"

(* Banach's fixed point *)

consts
 FIX1n :: "nat => ('p,'a) procFun => ('p => 'a proc)"  ("FIX![_] _" [0,1000] 55)
 FIX1  :: "('p,'a) procFun => ('p => 'a proc)"  ("FIX! _" [1000] 55)
 AnyInitProc :: "'a proc"

(*    note: The type of AnyInitProc is declared,     *)
(*    note: but it is not needed to be defined.      *)

defs
 FIX1n_def : "FIX![n] PF == (PF^n) (%q. AnyInitProc)"
 FIX1_def  :    "FIX! PF == (%p. (!nat n .. (((FIX![n] PF) p) |. n)))"

(*** Procx ***)

consts
  Procfun :: "('p,'a) procfun set"
  ProcFun :: "('p,'a) procFun set"

defs
  ProcFun_def: "ProcFun == {PF. (ALL p. (%f. PF f p) : Procfun)}"

inductive "Procfun"
intros
Procfun_p:
  "(%f. f p) : Procfun"
Procfun_STOP: 
  "(%f. STOP) : Procfun"
Procfun_SKIP: 
  "(%f. SKIP) : Procfun"
Procfun_DIV:
  "(%f. DIV) : Procfun"
Procfun_Act_prefix:
  "Pf : Procfun ==> (%f. a -> (Pf f)) : Procfun"
Procfun_Ext_pre_choice:
  "[| ALL a. Pff a : Procfun |] ==> (%f. ? a:X -> (Pff a f)) : Procfun"
Procfun_Ext_choice:
  "[| Pf : Procfun ; Qf : Procfun |] ==> (%f. (Pf f) [+] (Qf f)) : Procfun"
Procfun_Int_choice:
  "[| Pf : Procfun ; Qf : Procfun |] ==> (%f. (Pf f) |~| (Qf f)) : Procfun"
Procfun_Rep_int_choice0:
  "[| ALL c. Pff c : Procfun |] ==> (%f. !! c:C .. (Pff c f)) : Procfun"
Procfun_IF:
  "[| Pf : Procfun ; Qf : Procfun |] ==> (%f. IF b THEN (Pf f) ELSE (Qf f)) : Procfun"
Procfun_Parallel:
  "[| Pf : Procfun ; Qf : Procfun |] ==> (%f. (Pf f) |[X]| (Qf f)) : Procfun"
Procfun_Hiding:
  "Pf : Procfun ==> (%f. (Pf f) -- X) : Procfun"
Procfun_Renaming:
  "Pf : Procfun ==> (%f. (Pf f) [[r]]) : Procfun"
Procfun_Seq_compo:
  "[| Pf : Procfun ; Qf : Procfun |] ==> (%f. (Pf f) ;; (Qf f)) : Procfun"
Procfun_Depth_rest:
  "Pf : Procfun ==> (%f. (Pf f) |. n) : Procfun"

lemma Procfun_Rep_int_choice_fun:
  "[| ALL a. Pff a : Procfun |] 
   ==> (%f. !!<g> a:X .. (Pff a f)) : Procfun"
by (simp add: Rep_int_choice_fun_def Procfun_Rep_int_choice0)

lemma Procfun_Rep_int_choice_com:
  "[| ALL a. Pff a : Procfun |] 
   ==> (%f. ! a:X .. (Pff a f)) : Procfun"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: Procfun_Rep_int_choice_fun)
done

lemma Procfun_Rep_int_choice_f:
  "[| ALL a. Pff a : Procfun |] 
   ==> (%f. !<g> a:X .. (Pff a f)) : Procfun"
apply (simp add: Rep_int_choice_f_def)
apply (rule Procfun_Rep_int_choice_com)
by (auto)

lemmas Procfun_Rep_int_choice = Procfun_Rep_int_choice0
                                Procfun_Rep_int_choice_fun
                                Procfun_Rep_int_choice_com
                                Procfun_Rep_int_choice_f

lemmas Procfun_basic_def = 
  Procfun_p Procfun_STOP  Procfun_SKIP        Procfun_DIV
  Procfun_Act_prefix   Procfun_Ext_pre_choice   Procfun_Ext_choice 
  Procfun_Int_choice   Procfun_Rep_int_choice   Procfun_IF
  Procfun_Parallel     Procfun_Hiding           Procfun_Renaming
  Procfun_Seq_compo    Procfun_Depth_rest

lemma Procfun_const:
  "(%f. P) : Procfun"
apply (induct_tac P)
apply (simp_all add: Procfun_basic_def)
done

(*** simp for Procfun ***)

lemma Procfun_p_iff: "(%f. f p) : Procfun"
by (simp add: Procfun_basic_def)

lemma Procfun_STOP_iff: "(%f. STOP) : Procfun"
by (simp add: Procfun_basic_def)

lemma Procfun_SKIP_iff: "(%f. SKIP) : Procfun"
by (simp add: Procfun_basic_def)

lemma Procfun_DIV_iff: "(%f. DIV) : Procfun"
by (simp add: Procfun_basic_def)

lemma Procfun_Act_prefix_iff: 
  "(%f. a -> (Pf f)) : Procfun = (Pf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Ext_pre_choice_iff:
  "(%f. ? a:X -> (Pff a f)) : Procfun = (ALL a. Pff a : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Ext_choice_iff: 
  "(%f. (Pf f) [+] (Qf f)) : Procfun = (Pf : Procfun & Qf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Int_choice_iff: 
  "(%f. (Pf f) |~| (Qf f)) : Procfun = (Pf : Procfun & Qf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Rep_int_choice0_iff: 
  "(%f. !! c:C .. (Pff c f)) : Procfun = (ALL c. Pff c : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_IF_iff:
  "(%f. IF b THEN (Pf f) ELSE (Qf f)) : Procfun = (Pf : Procfun & Qf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Parallel_iff: 
  "(%f. (Pf f) |[X]| (Qf f)) : Procfun = (Pf : Procfun & Qf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Hiding_iff: "(%f. Pf f -- X) : Procfun = (Pf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (simp add: expand_fun_eq[THEN sym])
by (simp add: Procfun_basic_def)

lemma Procfun_Renaming_iff: 
  "(%f. (Pf f) [[r]]) : Procfun = (Pf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Seq_compo_iff: 
  "(%f. (Pf f) ;; (Qf f)) : Procfun = (Pf : Procfun & Qf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: Procfun_basic_def)

lemma Procfun_Depth_rest_iff: 
  "(%f. (Pf f) |. n) : Procfun = (Pf : Procfun)"
apply (rule)
apply (erule Procfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
apply (simp add: Procfun_basic_def)
done

lemmas Procfun_iff =
  Procfun_p_iff    Procfun_SKIP_iff   Procfun_STOP_iff   Procfun_DIV_iff
  Procfun_Act_prefix_iff   Procfun_Ext_pre_choice_iff       Procfun_Ext_choice_iff 
  Procfun_Int_choice_iff   Procfun_Rep_int_choice0_iff      Procfun_IF_iff
  Procfun_Parallel_iff     Procfun_Hiding_iff
  Procfun_Renaming_iff     Procfun_Seq_compo_iff            Procfun_Depth_rest_iff

declare Procfun_iff [simp]

lemma Procfun_Rep_int_choice_fun_iff[simp]:
  "inj g ==> (%f. !!<g> a:X .. (Pff a f)) : Procfun = (ALL a. Pff a : Procfun)"
apply (auto simp add: Rep_int_choice_fun_def)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma Procfun_Rep_int_choice_com_iff[simp]:
  "(%f. ! a:X .. (Pff a f)) : Procfun = (ALL a. Pff a : Procfun)"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done

lemma Procfun_Rep_int_choice_f_iff[simp]:
  "inj g ==> (%f. !<g> a:X .. (Pff a f)) : Procfun = (ALL a. Pff a : Procfun)"
apply (simp add: Rep_int_choice_f_def)
apply (auto)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma Procfun_Alpha_parallel_iff[simp]:
  "(%f. (Pf f) |[X,Y]| (Qf f)) : Procfun = (Pf : Procfun & Qf : Procfun)"
apply (simp add: Alpha_parallel_def)
done

(*
lemma Procfun_basic_def_test:
  "[| ALL a. Pff a : Procfun |] ==> (%f. ! a:X .. (Pff a f)) : Procfun"
by (simp)
*)

(*------------------------------------------------------*
 |  "Procfun.induct" is available.                      |
 |                                                      |
 |      apply (rule Procfun.induct[of P PR])            |
 |                                                      |
 *------------------------------------------------------*)

lemma compo_in_Procfun1:
  "[| Pf : Procfun ; QF : ProcFun |] ==> (%f. Pf (QF f)) : Procfun"
apply (rule Procfun.induct[of Pf "(%Pf. (%f. Pf (QF f)) : Procfun)"])
apply (simp_all)
apply (simp add: ProcFun_def)
done

lemma compo_in_Procfun2:
  "[| Pf : Procfun ; QF : ProcFun |] ==> Pf o QF : Procfun"
by (simp add: comp_def compo_in_Procfun1)

lemmas compo_in_Procfun = compo_in_Procfun1 compo_in_Procfun2

lemma compo_in_Procfun_ALL:
  "ALL Pf QF. (Pf : Procfun & QF : ProcFun ) --> (%f. Pf (QF f)) : Procfun"
by (simp add: compo_in_Procfun)

lemma compo_in_ProcFun1:
  "[| PF : ProcFun ; QF : ProcFun |] ==> (%f. PF (QF f)): ProcFun"
apply (simp add: ProcFun_def)
apply (intro allI)
apply (drule_tac x="p" in spec)
apply (insert compo_in_Procfun_ALL)
apply (drule_tac x="(%f. PF f p)" in spec)
apply (drule_tac x="QF" in spec)
apply (simp add: ProcFun_def)
done

lemma compo_in_ProcFun2:
  "[| PF : ProcFun ; QF : ProcFun |] ==> PF o QF : ProcFun"
by (simp add: comp_def compo_in_ProcFun1)

lemmas compo_in_ProcFun = compo_in_ProcFun1 compo_in_ProcFun2

lemma iteration_in_ProcFun:
  "PF : ProcFun ==> PF ^ n : ProcFun"
apply (induct_tac n)
apply (simp add: ProcFun_def)
apply (simp add: compo_in_ProcFun)
done

lemma iteration_in_Procfun:
  "PF : ProcFun ==> (%f. (PF ^ n) f p) : Procfun"
apply (insert iteration_in_ProcFun[of PF n])
apply (simp)
apply (simp add: ProcFun_def)
done

(*------------------------------------------------------*
 |                                                      |
 |            single recursion by MU operator           |
 |                                                      |
 *------------------------------------------------------*)

datatype 
 mup = MUp

consts
  MUX :: "('a proc => 'a proc) => 'a proc"
  MUX1 :: "('a proc => 'a proc) => 'a proc"   ("MUX!")

defs
  MUX_def :
   "MUX PX == (FIX (%f. (%p. (PX (f MUp))))) MUp"

  MUX1_def :
   "MUX1 PX == (FIX! (%f. (%p. (PX (f MUp))))) MUp"

syntax
  "@MU"  :: "pttrn => 'a proc => 'a proc"  ("(1MU _ .. _)" [900,62] 62)
  "@MU1" :: "pttrn => 'a proc => 'a proc"  ("(1MU! _ .. _)" [900,62] 62)

translations
  "MU X .. P"  == "MUX (%X. P)"
  "MU! X .. P" == "MUX! (%X. P)"

syntax (output)
  "_MU"  :: "pttrn => 'a proc => 'a proc"  ("(1MU _ .. _)" [900,62] 62)
  "_MU1" :: "pttrn => 'a proc => 'a proc"  ("(1MU! _ .. _)" [900,62] 62)

syntax (xsymbols)
  "_MU"  :: "pttrn => 'a proc => 'a proc"  ("(1μ _ .. _)" [900,62] 62)
  "_MU1" :: "pttrn => 'a proc => 'a proc"  ("(1μ! _ .. _)" [900,62] 62)

translations
  "μ X .. P"  == "MU X .. P"
  "μ! X .. P"  == "MU! X .. P"

consts
  ProcX :: "('a proc => 'a proc) set"

defs
  ProcX_def: "ProcX == {PX. (%X. PX (X MUp)) : Procfun}"

(*** Procfun lemma ***)

lemma Procfun_MU[simp]:
  "(ALL Pf:Procfun. (%f. (PfX f (Pf f))) : Procfun) ==> (%f. MUX (PfX f)) : Procfun"
apply (simp add: MUX_def FIX_def)
apply (rule allI)
apply (simp add: FIXn_def)
apply (induct_tac n)
apply (simp)
apply (simp)
done

lemma Procfun_MU1[simp]:
  "(ALL Pf:Procfun. (%f. (PfX f (Pf f))) : Procfun) ==> (%f. MUX! (PfX f)) : Procfun"
apply (simp add: MUX1_def FIX1_def)
apply (rule allI)
apply (simp add: FIX1n_def)

apply (induct_tac n)
apply (simp add: Procfun_const)
apply (simp)
done

lemmas Procfun_def = Procfun_basic_def Procfun_MU Procfun_MU1

(*** Procfun test ***)

lemma "(%Z. (MU X .. a -> (MU! Y .. b -> X [+] c -> Y |~| d -> Z))) : ProcX"
apply (simp add: ProcX_def)
done

(*************************************************************
                   Syntactical functions
 *************************************************************)

(*** guarded (rec_proc_fun) ***)

consts
  gSKIPfun  :: "('p,'a) procfun set"
  nohidefun :: "('p,'a) procfun set"
  gProcfun  :: "('p,'a) procfun set"

(*** gSKIP ***)

inductive "gSKIPfun"
intros
gSKIPfun_STOP: 
  "(%f. STOP) : gSKIPfun"
gSKIPfun_DIV:
  "(%f. DIV) : gSKIPfun"
gSKIPfun_Act_prefix:
  "Pf : Procfun ==> (%f. a -> (Pf f)) : gSKIPfun"
gSKIPfun_Ext_pre_choice:
  "[| ALL a. Pff a : Procfun |] ==> (%f. ? a:X -> (Pff a f)) : gSKIPfun"
gSKIPfun_Ext_choice:
  "[| Pf : gSKIPfun ; Qf : gSKIPfun |] ==> (%f. (Pf f) [+] (Qf f)) : gSKIPfun"
gSKIPfun_Int_choice:
  "[| Pf : gSKIPfun ; Qf : gSKIPfun |] ==> (%f. (Pf f) |~| (Qf f)) : gSKIPfun"
gSKIPfun_Rep_int_choice0:
  "[| ALL c. Pff c : gSKIPfun |] ==> (%f. !! c:C .. (Pff c f)) : gSKIPfun"
gSKIPfun_IF:
  "[| Pf : gSKIPfun ; Qf : gSKIPfun |] ==> (%f. IF b THEN (Pf f) ELSE (Qf f)) : gSKIPfun"
gSKIPfun_Parallel:
  "[| (Pf : gSKIPfun & Qf : Procfun) |
      (Pf : Procfun & Qf : gSKIPfun) |]
   ==> (%f. (Pf f) |[X]| (Qf f)) : gSKIPfun"
gSKIPfun_Renaming:
  "Pf : gSKIPfun ==> (%f. (Pf f) [[r]]) : gSKIPfun"
gSKIPfun_Seq_compo:
  "[| (Pf : gSKIPfun & Qf : Procfun) |
      (Pf : Procfun & Qf : gSKIPfun) |]
   ==> (%f. (Pf f) ;; (Qf f)) : gSKIPfun"
gSKIPfun_Depth_rest_fun:
  "Pf : gSKIPfun ==> (%f. (Pf f) |. n) : gSKIPfun"
gSKIPfun_Depth_rest_const:
  "(%f. P |. 0) : gSKIPfun"

lemmas gSKIPfun_Depth_rest = gSKIPfun_Depth_rest_fun gSKIPfun_Depth_rest_const

lemma gSKIPfun_Rep_int_choice_fun:
  "[| ALL a. Pff a : gSKIPfun |] 
   ==> (%f. !!<g> a:X .. (Pff a f)) : gSKIPfun"
by (simp add: Rep_int_choice_fun_def gSKIPfun_Rep_int_choice0)

lemma gSKIPfun_Rep_int_choice_com:
  "[| ALL a. Pff a : gSKIPfun |] 
   ==> (%f. ! a:X .. (Pff a f)) : gSKIPfun"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: gSKIPfun_Rep_int_choice_fun)
done

lemma gSKIPfun_Rep_int_choice_f:
  "[| ALL a. Pff a : gSKIPfun |] 
   ==> (%f. !<g> a:X .. (Pff a f)) : gSKIPfun"
apply (simp add: Rep_int_choice_f_def)
apply (rule gSKIPfun_Rep_int_choice_com)
by (auto)

lemmas gSKIPfun_Rep_int_choice = gSKIPfun_Rep_int_choice0
                                 gSKIPfun_Rep_int_choice_fun
                                 gSKIPfun_Rep_int_choice_com
                                 gSKIPfun_Rep_int_choice_f

lemmas gSKIPfun_basic_def = 
  gSKIPfun_STOP         gSKIPfun_DIV
  gSKIPfun_Act_prefix   gSKIPfun_Ext_pre_choice       gSKIPfun_Ext_choice 
  gSKIPfun_Int_choice   gSKIPfun_Rep_int_choice       gSKIPfun_IF
  gSKIPfun_Parallel     gSKIPfun_Renaming             gSKIPfun_Seq_compo
  gSKIPfun_Depth_rest

lemma gSKIPfun_implies_Procfun[simp]:
  "Pf : gSKIPfun ==> Pf : Procfun"
apply (rule gSKIPfun.induct[of Pf])
apply (auto)
apply (simp add: Procfun_const)
done

lemma gSKIPfun_subseteq_Procfun:
  "gSKIPfun <= Procfun"
apply (auto)
done

(*** no hide ***)

inductive "nohidefun"
intros
nohidefun_p:
  "(%f. f p) : nohidefun"
nohidefun_STOP: 
  "(%f. STOP) : nohidefun"
nohidefun_SKIP: 
  "(%f. SKIP) : nohidefun"
nohidefun_DIV:
  "(%f. DIV) : nohidefun"
nohidefun_Act_prefix:
  "[| Pf : nohidefun |] ==>  (%f. a -> (Pf f)) : nohidefun"
nohidefun_Ext_pre_choice:
  "[| ALL a. Pff a : nohidefun |] ==> (%f. ? a:X -> (Pff a f)) : nohidefun"
nohidefun_Ext_choice:
  "[| Pf : nohidefun ; Qf : nohidefun |] ==> (%f. (Pf f) [+] (Qf f)) : nohidefun"
nohidefun_Int_choice:
  "[| Pf : nohidefun ; Qf : nohidefun |] ==> (%f. (Pf f) |~| (Qf f)) : nohidefun"
nohidefun_Rep_int_choice0:
  "[| ALL c. Pff c : nohidefun |] ==> (%f. !! c:C .. (Pff c f)) : nohidefun"
nohidefun_IF:
  "[| Pf : nohidefun ; Qf : nohidefun |] 
   ==> (%f. IF b THEN (Pf f) ELSE (Qf f)) : nohidefun"
nohidefun_Parallel:
  "[| Pf : nohidefun ; Qf : nohidefun |] ==> (%f. (Pf f) |[X]| (Qf f)) : nohidefun"
nohidefun_Hiding:
  "(%f. P -- X) : nohidefun"
nohidefun_Renaming:
  "Pf : nohidefun ==> (%f. (Pf f) [[r]]) : nohidefun"
nohidefun_Seq_compo:
  "[| Pf : nohidefun ; Qf : nohidefun |] ==> (%f. (Pf f) ;; (Qf f)) : nohidefun"
nohidefun_Depth_rest:
  "Pf : nohidefun ==> (%f. (Pf f) |. n) : nohidefun"

lemma nohidefun_Rep_int_choice_fun:
  "[| ALL a. Pff a : nohidefun |] 
   ==> (%f. !!<g> a:X .. (Pff a f)) : nohidefun"
by (simp add: Rep_int_choice_fun_def nohidefun_Rep_int_choice0)

lemma nohidefun_Rep_int_choice_com:
  "[| ALL a. Pff a : nohidefun |] 
   ==> (%f. ! a:X .. (Pff a f)) : nohidefun"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: nohidefun_Rep_int_choice_fun)
done

lemma nohidefun_Rep_int_choice_f:
  "[| ALL a. Pff a : nohidefun |] 
   ==> (%f. !<g> a:X .. (Pff a f)) : nohidefun"
apply (simp add: Rep_int_choice_f_def)
apply (rule nohidefun_Rep_int_choice_com)
by (auto)

lemmas nohidefun_Rep_int_choice = nohidefun_Rep_int_choice0
                                  nohidefun_Rep_int_choice_fun
                                  nohidefun_Rep_int_choice_com
                                  nohidefun_Rep_int_choice_f

lemmas nohidefun_basic_def = 
  nohidefun_p
  nohidefun_STOP         nohidefun_SKIP              nohidefun_DIV
  nohidefun_Act_prefix   nohidefun_Ext_pre_choice    nohidefun_Ext_choice 
  nohidefun_Int_choice   nohidefun_Rep_int_choice    nohidefun_IF
  nohidefun_Parallel     nohidefun_Renaming          nohidefun_Seq_compo
  nohidefun_Depth_rest   nohidefun_Hiding

lemma nohidefun_implies_Procfun[simp]:
  "Pf : nohidefun ==> Pf : Procfun"
apply (rule nohidefun.induct[of Pf])
apply (simp_all)
apply (simp add: Procfun_const)
done

lemma nohidefun_subseteq_Procfun:
  "nohidefun <= Procfun"
by (auto)

lemma nohidefun_const:
  "(%f. P) : nohidefun"
apply (induct_tac P)
apply (simp_all add: nohidefun_basic_def)
done

(*** gProc ***)

inductive "gProcfun"
intros
gProcfun_STOP: 
  "(%f. STOP) : gProcfun"
gProcfun_SKIP: 
  "(%f. SKIP) : gProcfun"
gProcfun_DIV:
  "(%f. DIV) : gProcfun"
gProcfun_Act_prefix:
  "Pf : nohidefun ==> (%f. a -> (Pf f)) : gProcfun"
gProcfun_Ext_pre_choice:
  "[| ALL a. Pff a : nohidefun |] ==> (%f. ? a:X -> (Pff a f)) : gProcfun"
gProcfun_Ext_choice:
  "[| Pf : gProcfun ; Qf : gProcfun |] ==> (%f. (Pf f) [+] (Qf f)) : gProcfun"
gProcfun_Int_choice:
  "[| Pf : gProcfun ; Qf : gProcfun |] ==> (%f. (Pf f) |~| (Qf f)) : gProcfun"
gProcfun_Rep_int_choice0:
  "[| ALL c. Pff c : gProcfun |] ==> (%f. !! c:C .. (Pff c f)) : gProcfun"
gProcfun_IF:
  "[| Pf : gProcfun ; Qf : gProcfun |] ==> (%f. IF b THEN (Pf f) ELSE (Qf f)) : gProcfun"
gProcfun_Parallel:
  "[| Pf : gProcfun ; Qf : gProcfun |] ==> (%f. (Pf f) |[X]| (Qf f)) : gProcfun"
gProcfun_Hiding:
  "(%f. P -- X) : gProcfun"
gProcfun_Renaming:
  "Pf : gProcfun ==> (%f. (Pf f) [[r]]) : gProcfun"
gProcfun_Seq_compo:
  "[| ((Pf : gProcfun & Pf : gSKIPfun & Qf : nohidefun) |
       (Pf : gProcfun & Qf : gProcfun)) |]
   ==> (%f. (Pf f) ;; (Qf f)) : gProcfun"
gProcfun_Depth_rest:
  "Pf : gProcfun ==> (%f. (Pf f) |. n) : gProcfun"

lemma gProcfun_Rep_int_choice_fun:
  "[| ALL a. Pff a : gProcfun |] 
   ==> (%f. !!<g> a:X .. (Pff a f)) : gProcfun"
by (simp add: Rep_int_choice_fun_def gProcfun_Rep_int_choice0)

lemma gProcfun_Rep_int_choice_com:
  "[| ALL a. Pff a : gProcfun |] 
   ==> (%f. ! a:X .. (Pff a f)) : gProcfun"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: gProcfun_Rep_int_choice_fun)
done

lemma gProcfun_Rep_int_choice_f:
  "[| ALL a. Pff a : gProcfun |] 
   ==> (%f. !<g> a:X .. (Pff a f)) : gProcfun"
apply (simp add: Rep_int_choice_f_def)
apply (rule gProcfun_Rep_int_choice_com)
by (auto)

lemmas gProcfun_Rep_int_choice = gProcfun_Rep_int_choice0
                                 gProcfun_Rep_int_choice_fun
                                 gProcfun_Rep_int_choice_com
                                 gProcfun_Rep_int_choice_f

lemmas gProcfun_basic_def = 
  gProcfun_STOP         gProcfun_SKIP              gProcfun_DIV
  gProcfun_Act_prefix   gProcfun_Ext_pre_choice    gProcfun_Ext_choice 
  gProcfun_Int_choice   gProcfun_Rep_int_choice    gProcfun_IF
  gProcfun_Parallel     gProcfun_Renaming          gProcfun_Seq_compo
  gProcfun_Depth_rest   gProcfun_Hiding

lemma gProcfun_implies_nohidefun[simp]:
  "Pf : gProcfun ==> Pf : nohidefun"
apply (rule gProcfun.induct[of Pf])
apply (auto simp add: nohidefun_basic_def)
done

lemma gProcfun_implies_Procfun:
  "Pf : gProcfun ==> Pf : Procfun"
apply (simp)
done

lemma gProcfun_subseteq_Procfun:
  "gProcfun <= Procfun"
by (auto)

lemma gProcfun_const:
  "(%f. P) : gProcfun"
apply (induct_tac P)
apply (simp_all add: gProcfun_basic_def)
done

(*** simp for gSKIPfun ***)

lemma gSKIPfun_p_iff: "(%f. f p) : gSKIPfun = False"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
done

lemma gSKIPfun_STOP_iff: "(%f. STOP) : gSKIPfun"
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_SKIP_iff: "(%f. SKIP) : gSKIPfun = False"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
done

lemma gSKIPfun_DIV_iff: "(%f. DIV) : gSKIPfun"
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Act_prefix_iff: 
  "((%f. a -> (Pf f)) : gSKIPfun) = (Pf : Procfun)"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Ext_pre_choice_iff: 
  "(%f. ? a:X -> (Pff a f)) : gSKIPfun = (ALL a. Pff a : Procfun)"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Ext_choice_iff: 
  "(%f. (Pf f) [+] (Qf f)) : gSKIPfun = (Pf : gSKIPfun & Qf : gSKIPfun)"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Int_choice_iff: 
  "(%f. (Pf f) |~| (Qf f)) : gSKIPfun = (Pf : gSKIPfun & Qf : gSKIPfun)"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Rep_int_choice0_iff: 
  "(%f. !! c:C .. (Pff c f)) : gSKIPfun = (ALL c. Pff c : gSKIPfun)"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_IF_iff:
  "(%f. IF b THEN (Pf f) ELSE (Qf f)) : gSKIPfun = (Pf : gSKIPfun & Qf : gSKIPfun)"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Parallel_iff: 
  "(%f. (Pf f) |[X]| (Qf f)) : gSKIPfun = 
   ((Pf : gSKIPfun & Qf : Procfun) |
    (Pf : Procfun & Qf : gSKIPfun))"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (erule disjE)
apply (simp_all)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Hiding_iff: "(%f. Pf f -- X) : gSKIPfun = False"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
done

lemma gSKIPfun_Renaming_iff: 
  "(%f. (Pf f) [[r]]) : gSKIPfun = (Pf : gSKIPfun)"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Seq_compo_iff: 
  "(%f. (Pf f) ;; (Qf f)) : gSKIPfun = 
   ((Pf : gSKIPfun & Qf : Procfun) |
    (Pf : Procfun & Qf : gSKIPfun))"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (erule disjE)
apply (simp_all)
apply (simp add: expand_fun_eq)
by (simp add: gSKIPfun_basic_def)

lemma gSKIPfun_Depth_rest_iff: 
  "(%f. (Pf f) |. n) : gSKIPfun = ((Pf : gSKIPfun) | (EX P. Pf = (%f. P) & n = 0))"
apply (rule)
apply (erule gSKIPfun.elims)
apply (simp_all add: expand_fun_eq)
apply (simp add: expand_fun_eq[THEN sym])
apply (elim disjE conjE exE)
apply (simp add: gSKIPfun_basic_def)
apply (simp add: gSKIPfun_basic_def)
done

lemmas gSKIPfun_iff =
  gSKIPfun_p_iff  gSKIPfun_SKIP_iff  gSKIPfun_STOP_iff     gSKIPfun_DIV_iff
  gSKIPfun_Act_prefix_iff   gSKIPfun_Ext_pre_choice_iff     gSKIPfun_Ext_choice_iff 
  gSKIPfun_Int_choice_iff   gSKIPfun_Rep_int_choice0_iff    gSKIPfun_IF_iff
  gSKIPfun_Parallel_iff     gSKIPfun_Hiding_iff
  gSKIPfun_Renaming_iff     gSKIPfun_Seq_compo_iff          gSKIPfun_Depth_rest_iff

declare gSKIPfun_iff [simp]

(*** simp for nohidefun ***)

lemma nohidefun_p_iff: "(%f. f p) : nohidefun"
by (simp add: nohidefun_basic_def)

lemma nohidefun_STOP_iff: "(%f. STOP) : nohidefun"
by (simp add: nohidefun_basic_def)

lemma nohidefun_SKIP_iff: "(%f. SKIP) : nohidefun"
by (simp add: nohidefun_basic_def)

lemma nohidefun_DIV_iff: "(%f. DIV) : nohidefun"
by (simp add: nohidefun_basic_def)

lemma nohidefun_Act_prefix_iff: 
  "(%f. a -> (Pf f)) : nohidefun = (Pf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Ext_pre_choice_iff:
  "(%f. ? a:X -> (Pff a f)) : nohidefun = (ALL a. Pff a : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Ext_choice_iff: 
  "(%f. (Pf f) [+] (Qf f)) : nohidefun = (Pf : nohidefun & Qf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Int_choice_iff: 
  "(%f. (Pf f) |~| (Qf f)) : nohidefun = (Pf : nohidefun & Qf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Rep_int_choice0_iff: 
  "(%f. !! c:C .. (Pff c f)) : nohidefun = (ALL c. Pff c : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_IF_iff:
  "(%f. IF b THEN (Pf f) ELSE (Qf f)) : nohidefun = (Pf : nohidefun & Qf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Parallel_iff: 
  "(%f. (Pf f) |[X]| (Qf f)) : nohidefun = (Pf : nohidefun & Qf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Hiding_iff: "(%f. Pf f -- X) : nohidefun = (EX P. Pf = (%f. P))"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (simp add: expand_fun_eq[THEN sym])
apply (elim exE)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Renaming_iff: 
  "(%f. (Pf f) [[r]]) : nohidefun = (Pf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Seq_compo_iff: 
  "(%f. (Pf f) ;; (Qf f)) : nohidefun = (Pf : nohidefun & Qf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: nohidefun_basic_def)

lemma nohidefun_Depth_rest_iff: 
  "(%f. (Pf f) |. n) : nohidefun = (Pf : nohidefun)"
apply (rule)
apply (erule nohidefun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
apply (simp add: nohidefun_basic_def)
done

lemmas nohidefun_iff =
  nohidefun_p_iff    nohidefun_SKIP_iff   nohidefun_STOP_iff   nohidefun_DIV_iff
  nohidefun_Act_prefix_iff   nohidefun_Ext_pre_choice_iff       nohidefun_Ext_choice_iff 
  nohidefun_Int_choice_iff   nohidefun_Rep_int_choice0_iff      nohidefun_IF_iff
  nohidefun_Parallel_iff     nohidefun_Hiding_iff
  nohidefun_Renaming_iff     nohidefun_Seq_compo_iff            nohidefun_Depth_rest_iff

declare nohidefun_iff [simp]

(*** simp for gProcfun ***)

lemma gProcfun_p_iff: "(%f. f p) : gProcfun = False"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. STOP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
apply (drule_tac x="(%f. SKIP)" in spec, simp)
done

lemma gProcfun_STOP_iff: "(%f. STOP) : gProcfun"
by (simp add: gProcfun_basic_def)

lemma gProcfun_SKIP_iff: "(%f. SKIP) : gProcfun"
by (simp add: gProcfun_basic_def)

lemma gProcfun_DIV_iff: "(%f. DIV) : gProcfun"
by (simp add: gProcfun_basic_def)

lemma gProcfun_Act_prefix_iff: 
  "((%f. a -> (Pf f)) : gProcfun) = (Pf : nohidefun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Ext_pre_choice_iff: 
  "(%f. ? a:X -> (Pff a f)) : gProcfun = (ALL a. Pff a : nohidefun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Ext_choice_iff: 
  "(%f. (Pf f) [+] (Qf f)) : gProcfun = (Pf : gProcfun & Qf : gProcfun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Int_choice_iff: 
  "(%f. (Pf f) |~| (Qf f)) : gProcfun = (Pf : gProcfun & Qf : gProcfun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Rep_int_choice0_iff: 
  "(%f. !! c:C .. (Pff c f)) : gProcfun = (ALL c. Pff c : gProcfun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pff = Pffa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_IF_iff:
  "(%f. IF b THEN (Pf f) ELSE (Qf f)) : gProcfun = (Pf : gProcfun & Qf : gProcfun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Parallel_iff: 
  "(%f. (Pf f) |[X]| (Qf f)) : gProcfun = (Pf : gProcfun & Qf : gProcfun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Hiding_iff: "(%f. Pf f -- X) : gProcfun = (EX P. Pf = (%f. P))"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (simp add: expand_fun_eq[THEN sym])
apply (elim exE)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Renaming_iff: 
  "(%f. (Pf f) [[r]]) : gProcfun = (Pf : gProcfun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Seq_compo_iff: 
  "(%f. (Pf f) ;; (Qf f)) : gProcfun
 = ((Pf : gProcfun & Pf : gSKIPfun & Qf : nohidefun) |
    (Pf : gProcfun & Qf : gProcfun))"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa & Qf = Qfa")
apply (simp)
apply (simp add: expand_fun_eq)
by (simp add: gProcfun_basic_def)

lemma gProcfun_Depth_rest_iff: 
  "(%f. (Pf f) |. n) : gProcfun = (Pf : gProcfun)"
apply (rule)
apply (erule gProcfun.elims)
apply (simp_all add: expand_fun_eq)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
apply (simp add: gProcfun_basic_def)
done

lemmas gProcfun_iff =
  gProcfun_p_iff  gProcfun_SKIP_iff  gProcfun_STOP_iff    gProcfun_DIV_iff
  gProcfun_Act_prefix_iff   gProcfun_Ext_pre_choice_iff    gProcfun_Ext_choice_iff 
  gProcfun_Int_choice_iff   gProcfun_Rep_int_choice0_iff   gProcfun_IF_iff
  gProcfun_Parallel_iff     gProcfun_Hiding_iff
  gProcfun_Renaming_iff     gProcfun_Seq_compo_iff         gProcfun_Depth_rest_iff

declare gProcfun_iff [simp]

(****** short notations ******)

(* gSKIP *)

lemma gSKIPfun_Rep_int_choice_fun_iff[simp]:
  "inj g ==> (%f. !!<g> a:X .. (Pff a f)) : gSKIPfun = (ALL a. Pff a : gSKIPfun)"
apply (auto simp add: Rep_int_choice_fun_def)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma gSKIPfun_Rep_int_choice_com_iff[simp]:
  "(%f. ! a:X .. (Pff a f)) : gSKIPfun = (ALL a. Pff a : gSKIPfun)"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done

lemma gSKIPfun_Rep_int_choice_f_iff[simp]:
  "inj g ==> (%f. !<g> a:X .. (Pff a f)) : gSKIPfun = (ALL a. Pff a : gSKIPfun)"
apply (simp add: Rep_int_choice_f_def)
apply (auto)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma gSKIPfun_Alpha_parallel_iff[simp]:
  "(%f. (Pf f) |[X,Y]| (Qf f)) : gSKIPfun = 
   ((Pf : gSKIPfun & Qf : Procfun) |
    (Pf : Procfun & Qf : gSKIPfun))"
apply (simp add: Alpha_parallel_def)
done

lemma gSKIPfun_MU[simp]:
  "(ALL Pf: gSKIPfun. (%f. (PfX f (Pf f))) : gSKIPfun)
    ==> (%f. MUX (PfX f)) : gSKIPfun"
apply (simp add: MUX_def FIX_def)
apply (rule allI)
apply (simp add: FIXn_def)
apply (induct_tac n)
apply (simp)
apply (simp)
done

(* note: forall f *)
lemma gSKIPfun_MU1[simp]:
  "(ALL Pf. (%f. (PfX f (Pf f))) : gSKIPfun)
    ==> (%f. MUX! (PfX f)) : gSKIPfun"
apply (simp add: MUX1_def FIX1_def)
apply (rule allI)
apply (simp add: FIX1n_def)
apply (induct_tac n)
apply (auto)
done

lemmas gSKIPfun_def = gSKIPfun_basic_def 
                      gSKIPfun_MU
                      gSKIPfun_MU1

(*** gSKIPfun test ***)

lemma "(%Z. (MU X .. a -> (MU! Y .. b -> X [+] c -> Y |~| d -> Z i))) : gSKIPfun"
apply (simp)
done

lemma "ALL a. P a : gSKIPfun ==> (%f. (!set X:Xs .. P X f)) : gSKIPfun"
by (simp)

(* nohide *)

lemma nohidefun_Rep_int_choice_fun_iff[simp]:
  "inj g ==> (%f. !!<g> a:X .. (Pff a f)) : nohidefun = (ALL a. Pff a : nohidefun)"
apply (auto simp add: Rep_int_choice_fun_def)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma nohidefun_Rep_int_choice_com_iff[simp]:
  "(%f. ! a:X .. (Pff a f)) : nohidefun = (ALL a. Pff a : nohidefun)"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done

lemma nohidefun_Rep_int_choice_f_iff[simp]:
  "inj g ==> (%f. !<g> a:X .. (Pff a f)) : nohidefun = (ALL a. Pff a : nohidefun)"
apply (simp add: Rep_int_choice_f_def)
apply (auto)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma nohidefun_Alpha_parallel_iff[simp]:
  "(%f. (Pf f) |[X,Y]| (Qf f)) : nohidefun = (Pf : nohidefun & Qf : nohidefun)"
apply (simp add: Alpha_parallel_def)
done

lemma nohidefun_MU[simp]:
  "(ALL Pf: nohidefun. (%f. (PfX f (Pf f))) : nohidefun)
    ==> (%f. MUX (PfX f)) : nohidefun"
apply (simp add: MUX_def FIX_def)
apply (rule allI)
apply (simp add: FIXn_def)
apply (induct_tac n)
apply (simp)
apply (simp)
done

lemma nohidefun_MU1[simp]:
  "(ALL Pf: nohidefun. (%f. (PfX f (Pf f))) : nohidefun)
    ==> (%f. MUX! (PfX f)) : nohidefun"
apply (simp add: MUX1_def FIX1_def)
apply (rule allI)
apply (simp add: FIX1n_def)
apply (induct_tac n)
apply (simp add: nohidefun_const)
apply (simp)
done

lemmas nohidefun_def = nohidefun_basic_def 
                       nohidefun_MU
                       nohidefun_MU1

(*** nohidefun test ***)

lemma "(%Z. (MU X .. a -> (MU! Y .. b -> X [+] c -> Y |~| d -> Z i))) : nohidefun"
apply (simp)
done

(************ gProc ************)

lemma gProcfun_Rep_int_choice_fun_iff[simp]:
  "inj g ==> (%f. !!<g> a:X .. (Pff a f)) : gProcfun = (ALL a. Pff a : gProcfun)"
apply (auto simp add: Rep_int_choice_fun_def)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma gProcfun_Rep_int_choice_com_iff[simp]:
  "(%f. ! a:X .. (Pff a f)) : gProcfun = (ALL a. Pff a : gProcfun)"
apply (auto simp add: Rep_int_choice_com_def)
apply (drule_tac x="{a}" in spec)
apply (simp)
done

lemma gProcfun_Rep_int_choice_f_iff[simp]:
  "inj g ==> (%f. !<g> a:X .. (Pff a f)) : gProcfun = (ALL a. Pff a : gProcfun)"
apply (simp add: Rep_int_choice_f_def)
apply (auto)
apply (drule_tac x="g a" in spec)
apply (simp)
done

lemma gProcfun_Alpha_parallel_iff[simp]:
  "(%f. (Pf f) |[X,Y]| (Qf f)) : gProcfun = (Pf : gProcfun & Qf : gProcfun)"
apply (simp add: Alpha_parallel_def)
done

lemma gProcfun_MU[simp]:
  "(ALL Pf: gProcfun. (%f. (PfX f (Pf f))) : gProcfun)
    ==> (%f. MUX (PfX f)) : gProcfun"
apply (simp add: MUX_def FIX_def)
apply (rule allI)
apply (simp add: FIXn_def)
apply (induct_tac n)
apply (simp)
apply (simp)
done

lemma gProcfun_MU1[simp]:
  "(ALL Pf: gProcfun. (%f. (PfX f (Pf f))) : gProcfun)
    ==> (%f. MUX! (PfX f)) : gProcfun"
apply (simp add: MUX1_def FIX1_def)
apply (rule allI)
apply (simp add: FIX1n_def)
apply (induct_tac n)
apply (simp add: gProcfun_const)
apply (simp)
done

lemmas gProcfun_def = gProcfun_basic_def 
                      gProcfun_MU
                      gProcfun_MU1

(*** gProcfun test ***)

lemma "(%Z. (MU! X .. a -> (MU! Y .. b -> X [+] c -> Y |~| d -> Z i))) : gProcfun"
apply (simp)
done

lemma "(%Z. (MU X .. a -> (MU! Y .. b -> X [+] c -> Y |~| d -> Z i)) |~| Z j) : gProcfun
       = False"
apply (simp)
done

(************ Fun ************)

consts
  gSKIPFun  :: "('p,'a) procFun set"
  nohideFun :: "('p,'a) procFun set"
  gProcFun  :: "('p,'a) procFun set"

defs 
  gSKIPFun_def : 
    "gSKIPFun == {PF. (ALL p. (%f. (PF f p)) : gSKIPfun)}"

  nohideFun_def : 
    "nohideFun == {PF. (ALL p. (%f. (PF f p)) : nohidefun)}"

  gProcFun_def : 
    "gProcFun == {PF. (ALL p. (%f. (PF f p)) : gProcfun)}"

(************ for MU and MU! ************)

consts
  gSKIPX  :: "('a proc => 'a proc) set"
  nohideX :: "('a proc => 'a proc) set"
  gProcX  :: "('a proc => 'a proc) set"

defs
  gSKIPX_def : "gSKIPX  == {PX. (%f. PX (f MUp)) : gSKIPfun}"
  nohideX_def: "nohideX == {PX. (%f. PX (f MUp)) : nohidefun}"
  gProcX_def : "gProcX  == {PX. (%f. PX (f MUp)) : gProcfun}"

(************ implies ************)

lemma gSKIPFun_implies_ProcFun[simp]:
  "PF : gSKIPFun ==> PF : ProcFun"
by (simp add: gSKIPFun_def ProcFun_def)

lemma nohideFun_implies_ProcFun[simp]:
  "PF : nohideFun ==> PF : ProcFun"
by (simp add: nohideFun_def ProcFun_def)

lemma gProcFun_implies_ProcFun[simp]:
  "PF : gProcFun ==> PF : ProcFun"
by (simp add: gProcFun_def ProcFun_def)

(** PX **)

lemma gSKIPX_implies_ProcX[simp]:
  "PX : gSKIPX ==> PX : ProcX"
by (simp add: gSKIPX_def ProcX_def)

lemma nohideX_implies_ProcX[simp]:
  "PX : nohideX ==> PX : ProcX"
by (simp add: nohideX_def ProcX_def)

lemma gProcX_implies_ProcX[simp]:
  "PX : gProcX ==> PX : ProcX"
by (simp add: gProcX_def ProcX_def)

(*********************************************************
             termination relation for proc
 *********************************************************)

consts
  procterm :: "('a proc * '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"


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)+
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";
*}

(*-------------------------------------------------------* 
 |                                                       |
 |                  unfold PF: ***Fun                    |
 |                                                       |
 *-------------------------------------------------------*)

lemmas CSP_Fun_def = ProcFun_def gSKIPFun_def gProcFun_def nohideFun_def

(*------------------------------------------------------------*
 |                    convenient lemmas                       |
 *------------------------------------------------------------*)

lemma Rep_int_choice_fun_SET_eq:
   "(!set :Xs1 .. Pf = !set :Xs2 .. Pf) = (Xs1 = Xs2)"
apply (rule)
apply (simp add: Rep_int_choice_fun_def)
apply (erule equalityE)

 apply (rule)
  apply (rule subsetI)
  apply (elim subsetE)
   apply (drule_tac x="sel_set x" in bspec)
   apply (simp add: image_iff)
   apply (simp add: image_iff)

  apply (rule subsetI)
  apply (elim subsetE)
   apply (rotate_tac -1)
   apply (drule_tac x="sel_set x" in bspec)
   apply (simp add: image_iff)
   apply (simp add: image_iff)
apply (simp)
done

lemma Rep_int_choice_fun_SET_decompo:
   "!set :Xs1 .. Pf1 = !set :Xs2 .. Pf2
    ==> Xs1 = Xs2 & (ALL X:Xs2. Pf1 X = Pf2 X)"
apply (simp add: Rep_int_choice_fun_def)
apply (erule conjE)
apply (erule equalityE)
apply (rule conjI)

 apply (rule)
  apply (rule subsetI)
  apply (elim subsetE)
   apply (drule_tac x="sel_set x" in bspec)
   apply (simp add: image_iff)
   apply (simp add: image_iff)

  apply (rule subsetI)
  apply (elim subsetE)
   apply (rotate_tac -1)
   apply (drule_tac x="sel_set x" in bspec)
   apply (simp add: image_iff)
   apply (simp add: image_iff)

apply (rule ballI)
apply (simp add: expand_fun_eq)
apply (drule_tac x="sel_set X" in spec)
apply (simp)
done

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end