Theory Restricted

Up to index of Isabelle/HOL/PI

theory Restricted = ProcExp
files [Restricted.ML]:
Restricted = ProcExp +

consts
  RSTR  :: (('a::inf_class) procs) set
  RSTRA :: (('a::inf_class) => ('a procs)) set

syntax
  "@RSTR"  :: (('a::inf_class) procs) => bool
             ("rstr (_)" [100] 90)
  "@RSTRA" :: (('a::inf_class) => ('a procs)) => bool
             ("rstra (_)" [100] 90)

translations
  "rstr P"  == "P : RSTR"
  "rstra P" == "P : RSTRA"

inductive RSTR
  intrs
    Null  "rstr (.0)"
    Tau   "rstr P ==> rstr (.t.P)"
    Out   "rstr P ==> rstr (a<b>.P)"
    In    "rstra fP ==> rstr (a[x].fP x)"
    Res   "rstra fP ==> rstr (.#x. fP x)"
    Plus  "[| rstr P ; rstr Q |] ==> rstr (P .+ Q)"
    Par   "[| rstr P ; rstr Q |] ==> rstr (P .| Q)"
    Mt    "rstr P ==> rstr (.[a.=b]P)"
    Repl  "rstra fP ==> rstr (.!a[x].fP x)"

inductive RSTRA
  intrs
    Null  "rstra (%x. .0)"
    Tau   "rstra fP ==> rstra (%x. .t.fP x)"
    Out   "[| rstra fP ; wfna fa ; wfna fb |] \
            \ ==> rstra (%x. fa x<fb x>.fP x)"
    In    "[| ALL b. rstra (ffP b) ; ALL b. rstra (%x. ffP x b) ; \
            \ wfna fa |] ==> rstra (%x. fa x[y].ffP y x)"
    Res   "[| ALL b. rstra (ffP b) ; ALL b. rstra (%x. ffP x b) |] \
            \ ==> rstra (%x. .#y. ffP y x)"
    Plus  "[| rstra fP ; rstra fQ |] ==> rstra (%x. fP x .+ fQ x)"
    Par   "[| rstra fP ; rstra fQ |] ==> rstra (%x. fP x .| fQ x)"
    Mt    "[| rstra fP ; wfna fa ; wfna fb |] \
            \ ==> rstra (%x. .[fa x.=fb x]fP x)"
    Repl  "[| ALL b. rstra (ffP b) ; ALL b. rstra (%x. ffP x b) ; \
            \ wfna fa |] ==> rstra (%x. .!fa x[y].ffP y x)"

constdefs
  RstrId :: "(('a::inf_class) procs * 'a procs) set"
 "RstrId == {(P, P') . P=P' & rstr P}"
  
end

theorem rstr_cases1:

  [| .t.P' = P; rstr P |] ==> rstr P'

theorem rstr_cases2:

  [| a<b>.P' = P; rstr P |] ==> rstr P'

theorem rstr_cases3:

  [| In a fP' = P; rstr P |] ==> rstra fP'

theorem rstr_cases4:

  [| .#x. fP' x = P; rstr P |] ==> rstra fP'

theorem rstr_cases5:

  [| procs.Plus P' Q' = P; rstr P |] ==> rstr P' & rstr Q'

theorem rstr_cases6:

  [| P' .| Q' = P; rstr P |] ==> rstr P' & rstr Q'

theorem rstr_cases7:

  [| .[a.=b]P' = P; rstr P |] ==> rstr P'

theorem rstr_cases9:

  [| .!In a fP' = P; rstr P |] ==> rstra fP'

theorem rstra_cases0:

  [| .0 = fP a; rstra fP |] ==> fP = (%x. .0)

theorem rstra_cases1:

  [| .t.P = fP a; rstra fP |] ==> EX fP'. rstra fP' & fP = (%x. .t.fP' x)

theorem rstra_cases2:

  [| b<c>.P = fP a; rstra fP |]
  ==> EX fb fc fP'. wfna fb & wfna fc & rstra fP' & fP = (%x. fb x<fc x>.fP' x)

theorem rstra_cases3:

  [| In b fP' = fP a; rstra fP |]
  ==> EX fb ffP.
         wfna fb &
         (ALL b. rstra ffP b) &
         (ALL b. rstra (%x. ffP x b)) & fP = (%x. In (fb x) (%y. ffP y x))

theorem rstra_cases4:

  [| .#y. fP' y = fP a; rstra fP |]
  ==> EX ffP.
         (ALL b. rstra ffP b) &
         (ALL b. rstra (%x. ffP x b)) & fP = (%x. .#y. ffP y x)

theorem rstra_cases5:

  [| procs.Plus P Q = fP a; rstra fP |]
  ==> EX fP' fQ. rstra fP' & rstra fQ & fP = (%x. procs.Plus (fP' x) (fQ x))

theorem rstra_cases6:

  [| P .| Q = fP a; rstra fP |]
  ==> EX fP' fQ. rstra fP' & rstra fQ & fP = (%x. fP' x .| fQ x)

theorem rstra_cases7:

  [| .[b.=c]P = fP a; rstra fP |]
  ==> EX fb fc fP'. wfna fb & wfna fc & rstra fP' & fP = (%x. .[fb x.=fc x]fP' x)

theorem rstra_cases8:

  [| .[b.~=c]P = fP a; rstra fP |] ==> Pr

theorem rstra_cases9:

  [| .!P = fP a; rstra fP |]
  ==> EX fb ffP'.
         (ALL b. rstra ffP' b) &
         (ALL b. rstra (%x. ffP' x b)) & fP = (%x. .!In (fb x) (%y. ffP' y x))

theorem rstr_In_rstra2:

  rstr In (fa c) (%y. ffP y c) ==> rstra (%x. ffP x c)

theorem rstr_Res_rstra2:

  rstr .#y. ffP y c ==> rstra (%x. ffP x c)

theorem rstr_Plus1:

  rstr procs.Plus P Q ==> rstr P

theorem rstr_Plus2:

  rstr procs.Plus P Q ==> rstr Q

theorem rstr_Par1:

  rstr (P .| Q) ==> rstr P

theorem rstr_Par2:

  rstr (P .| Q) ==> rstr Q

theorem rstr_Mmt:

  rstr (.[a.~=b]P) ==> Pr

theorem rstr_Repl:

  rstr .!P ==> EX a fP. P = In a fP & rstra fP

theorem fun_eq_inst:

  f = g ==> f x = g x

theorem fun_eq_ext:

  ALL x. f x = g x ==> f = g

theorem In_eq1:

  (%x. In (fa x) (%y. ffP y x)) = (%x. In (fb x) (%y. ffQ y x)) ==> fa = fb

theorem In_eq2:

  (%x. In (fa x) (%y. ffP y x)) = (%x. In (fb x) (%y. ffQ y x)) ==> ffP = ffQ

theorem rstra_In_rstra1:

  rstra (%x. In (fb x) (%y. ffP y x)) ==> rstra ffP b

theorem rstra_In_rstra2:

  rstra (%x. In (fb x) (%y. ffP y x)) ==> rstra (%x. ffP x b)

theorem rstra_wfpa:

  rstra fP ==> wfpa fP

theorem rstr_wfp:

  rstr P ==> wfp P

theorem rstra_rstra:

  rstra fP ==> rstra (%x. fP b)

theorem rstr_rstra:

  rstr P ==> rstra (%x. P)

theorem rstra_rstr:

  rstra fP ==> rstr fP b

theorem lemma:

  wfpa fP ==> ALL c. rstr fP c --> rstra fP

theorem wfpa_rstra:

  [| wfpa fP; rstr fP c |] ==> rstra fP

theorem ext_pa_rstra:

  [| fP a = fQ a; fresha a fP; fresha a fQ; rstra fP; rstra fQ |] ==> fP = fQ

theorem ext_paa_rstra:

  [| ffP a = ffQ a; freshaa a ffP; freshaa a ffQ; ALL b. rstra ffP b;
     ALL b. rstra (%x. ffP x b); ALL b. rstra ffQ b; ALL b. rstra (%x. ffQ x b) |]
  ==> ffP = ffQ

theorem beta_exp_rstr:

  rstr P ==> EX fP. rstra fP & fresha a fP & P = fP a

theorem beta_expa_rstra:

  rstra fP
  ==> EX ffP.
         (ALL b. rstra ffP b) &
         (ALL b. rstra (%x. ffP x b)) & freshaa a ffP & fP = ffP a

theorem lemma:

  rstra fP ==> ALL P. fP = (%x. P) --> rstr P

theorem simp_rstra_rstr:

  rstra (%x. P) ==> rstr P

theorem res_rstr_rstr:

  rstr .#x. P ==> rstr P

theorem rstr_mono_res:

  rstr P --> rstr Q ==> rstr .#x. P --> rstr .#x. Q

theorem rstra_mono_res:

  rstra fP --> rstra fQ ==> rstr .#x. fP x --> rstr .#x. fQ x