Theory StTrans

Up to index of Isabelle/HOL/PI

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

consts
  StFOut :: "(('a::inf_class) procs * 'a * 'a * 'a procs) set"
  StBOut :: "(('a::inf_class) procs * 'a * ('a => 'a procs)) set"
  StIn   :: "(('a::inf_class) procs * 'a * ('a => 'a procs)) set"
  StTau  :: "(('a::inf_class) procs * 'a procs) set"
  StEps  :: "(('a::inf_class) procs * 'a procs) set"

syntax
 "@StFOut" :: "[('a::inf_class) procs, 'a, 'a, 'a procs] => bool"
               ("_ /-_<_>-> /_" [81,0,0,81] 80)
 "@StBOut" :: "[('a::inf_class) procs, 'a, 'a procs] => bool"
               ("_ /-_<>-> /_" [81,0,81] 80)
 "@StIn"   :: "[('a::inf_class) procs, 'a, 'a procs] => bool"
               ("_ /-_[]-> /_" [81,0,81] 80)
 "@StTau"  :: "[('a::inf_class) procs, 'a procs] => bool"
               ("_ /-tau-> /_" [81,81] 80)
 "@StEps"  :: "[('a::inf_class) procs, 'a procs] => bool"
               ("_ /-eps-> /_" [81,81] 80)

translations
 "P -a<b>-> P'" == "(P, a, b, P') : StFOut"
 "P -a<>-> fP'" == "(P, a, fP') : StBOut"
 "P -a[]-> fP'" == "(P, a, fP') : StIn"
 "P -tau->  P'" == "(P, P') : StTau"
 "P -eps->  P'" == "(P, P') : StEps"

inductive "StFOut"
  intrs
    fo0  "rstr P ==> a<b>.P -a<b>-> P"

    fo1  "[| fP c -a<b>-> fP' c ; fresha c fP ; fresha c fP' ; \
           \ c ~: {a, b} ; rstra fP ; rstra fP' |] \
           \ ==> Res fP -a<b>-> Res fP'"

    fo2a "[| P -a<b>-> P' ; rstr Q |] ==> P .+ Q -a<b>-> P'"
    fo2b "[| Q -a<b>-> Q' ; rstr P |] ==> P .+ Q -a<b>-> Q'"

    fo3a "[| P -a<b>-> P' ; rstr Q |] ==> P .| Q -a<b>-> P' .| Q"
    fo3b "[| Q -a<b>-> Q' ; rstr P |] ==> P .| Q -a<b>-> P .| Q'"

    fo4  "P -a<b>-> P' ==> .[c.=c]P -a<b>-> P'"

inductive "StBOut"
  intrs
    bo0  "[| fP c -a<c>-> fP' c ; fresha c fP ; fresha c fP' ; \
           \ a ~= c ; rstra fP ; rstra fP' |] \
           \ ==> Res fP -a<>-> fP'"

    bo1  "[| fP c -a<>-> ffP' c ; fresha c fP ; freshaa c ffP' ; \
           \ a ~= c ; rstra fP ; ALL b. rstra ffP' b ; \
           \ ALL b. rstra (%x. ffP' x b) |] \
           \ ==> Res fP -a<>-> (%x. .#y. ffP' y x)"

    bo2a "[| P -a<>-> fP' ; rstr Q |] ==> P .+ Q -a<>-> fP'"
    bo2b "[| Q -a<>-> fQ' ; rstr P |] ==> P .+ Q -a<>-> fQ'"

    bo3a "[| P -a<>-> fP' ; rstr Q |] ==> \
           \ P .| Q -a<>-> (%x. fP' x .| Q)"
    bo3b "[| Q -a<>-> fQ' ; rstr P |] ==> \
           \ P .| Q -a<>-> (%x. P .| fQ' x)"

    bo4  "P -a<>-> fP' ==> .[c.=c]P -a<>-> fP'"

inductive "StIn"
  intrs
    in0  "rstra fP ==> a[x].(fP x) -a[]-> fP"

    in1  "[| fP c -a[]-> ffP' c ; fresha c fP ; freshaa c ffP' ; \
           \ a ~= c ; rstra fP ; ALL b. rstra ffP' b ; \
           \ ALL b. rstra (%x. ffP' x b) |] \
           \ ==> Res fP -a[]-> (%x. .#y. ffP' y x)"

    in2a "[| P -a[]-> fP' ; rstr Q |] ==> P .+ Q -a[]-> fP'"
    in2b "[| Q -a[]-> fQ' ; rstr P |] ==> P .+ Q -a[]-> fQ'"

    in3a "[| P -a[]-> fP' ; rstr Q |] ==> \
           \ P .| Q -a[]-> (%x. fP' x .| Q)"
    in3b "[| Q -a[]-> fQ' ; rstr P |] ==> \
           \ P .| Q -a[]-> (%x. P .| fQ' x)"

    in4  "P -a[]-> fP' ==> .[c.=c]P -a[]-> fP'"

    in5  "[| P = a[x].fP x ; rstra fP |] ==> .!P -a[]-> (%x. .!P .| fP x)"

inductive "StTau"
  intrs
    ta0  "rstr P ==> .t.P -tau-> P"

    ta1  "[| fP c -tau-> fP' c ; fresha c fP ; fresha c fP' ; \
           \ rstra fP ; rstra fP' |] \
           \ ==> Res fP -tau-> Res fP'"

    ta2a "[| P -tau-> P' ; rstr Q |] ==> P .+ Q -tau-> P'"
    ta2b "[| Q -tau-> Q' ; rstr P |] ==> P .+ Q -tau-> Q'"

    ta3a "[| P -tau-> P' ; rstr Q |] ==> P .| Q -tau-> P' .| Q"
    ta3b "[| Q -tau-> Q' ; rstr P |] ==> P .| Q -tau-> P .| Q'"

    ta4a "[| P -a<b>-> P' ; Q -a[]-> fQ' |] \
           \ ==> P .| Q -tau-> P' .| fQ' b"
    ta4b "[| P -a[]-> fP' ; Q -a<b>-> Q' |] \
           \ ==> P .| Q -tau-> fP' b .| Q'"

    ta5a "[| P -a<>-> fP' ; Q -a[]-> fQ' |] \
           \ ==> P .| Q -tau-> .#x. (fP' x .| fQ' x)"
    ta5b "[| P -a[]-> fP' ; Q -a<>-> fQ' |] \
           \ ==> P .| Q -tau-> .#x. (fP' x .| fQ' x)"

    ta6  "P -tau-> P' ==> .[c.=c]P -tau-> P'"

defs
  StEps_def "StEps == StTau Un RstrId"

end

theorem StFOut_rstr1:

  P -a<b>-> P' ==> rstr P

theorem StFOut_wfp1:

  P -a<b>-> P' ==> wfp P

theorem StFOut_rstr2:

  P -a<b>-> P' ==> rstr P'

theorem StFOut_wfp2:

  P -a<b>-> P' ==> wfp P'

theorem StBOut_rstr1:

  P -a<>-> fP' ==> rstr P

theorem StBOut_wfp1:

  P -a<>-> fP' ==> wfp P

theorem StBOut_rstra2:

  P -a<>-> fP' ==> rstra fP'

theorem StBOut_wfpa2:

  P -a<>-> fP' ==> wfpa fP'

theorem StIn_rstr1:

  P -a[]-> fP' ==> rstr P

theorem StIn_wfp1:

  P -a[]-> fP' ==> wfp P

theorem StIn_rstra2:

  P -a[]-> fP' ==> rstra fP'

theorem StIn_wfpa2:

  P -a[]-> fP' ==> wfpa fP'

theorem StTau_rstr1:

  P -tau-> P' ==> rstr P

theorem StTau_wfp1:

  P -tau-> P' ==> wfp P

theorem StTau_rstr2:

  P -tau-> P' ==> rstr P'

theorem StTau_wfp2:

  P -tau-> P' ==> wfp P'