Theory WkTrans

Up to index of Isabelle/HOL/PI

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

consts
  WkFOut :: "(('a::inf_class) procs * 'a * 'a * 'a procs) set"
  WkBOut :: "(('a::inf_class) procs * 'a * ('a => 'a procs)) set"
  WkIn   :: "(('a::inf_class) procs * 'a * ('a => 'a procs)) set"
  WkTau  :: "(('a::inf_class) procs * 'a procs) set"
  WkEps  :: "(('a::inf_class) procs * 'a procs) set"

syntax
 "@WkFOut" :: "[('a::inf_class) procs, 'a, 'a, 'a procs] => bool"
               ("_ /=_<_>=> /_" [81,0,0,81] 80)
 "@WkBOut" :: "[('a::inf_class) procs, 'a, 'a procs] => bool"
               ("_ /=_<>=> /_" [81,0,81] 80)
 "@WkIn"   :: "[('a::inf_class) procs, 'a, 'a procs] => bool"
               ("_ /=_[]=> /_" [81,0,81] 80)
 "@WkBTau" :: "[('a::inf_class) procs, 'a procs] => bool"
               ("_ /=tau=> /_" [81,81] 80)
 "@WkBEps" :: "[('a::inf_class) procs, 'a procs] => bool"
               ("_ /=eps=> /_" [81,81] 80)

translations
 "P =a<b>=> P'" == "(P, a, b, P') : WkFOut"
 "P =a<>=> fP'" == "(P, a, fP') : WkBOut"
 "P =a[]=> fP'" == "(P, a, fP') : WkIn"
 "P =tau=>  P'" == "(P, P') : WkTau"
 "P =eps=>  P'" == "(P, P') : WkEps"

defs
  WkFOut_def "WkFOut == {(P, a, b, P') . EX Q . \
                \ P =eps=> Q & Q -a<b>-> P'}"
  WkBOut_def "WkBOut == {(P, a, fP') . EX Q . \
                \ P =eps=> Q & Q -a<>-> fP'}"
  WkIn_def   "WkIn == {(P, a, fP') . EX Q . \
                \ P =eps=> Q & Q -a[]-> fP'}"
  WkTau_def  "WkTau == StTau^+"
  WkEps_def  "WkEps == WkTau Un RstrId"

end

theorem lemma:

  P =tau=> P' ==> rstr P & rstr P'

theorem WkTau_rstr1:

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

theorem WkTau_rstr2:

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

theorem WkEps_rstr1:

  P =eps=> P' ==> rstr P

theorem WkEps_rstr2:

  P =eps=> P' ==> rstr P'

theorem WkFOut_rstr1:

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

theorem WkFOut_rstr2:

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

theorem WkBOut_rstr1:

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

theorem WkBOut_rstra2:

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

theorem WkIn_rstr1:

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

theorem WkIn_rstra2:

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

theorem WkTau_wfp1:

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

theorem WkTau_wfp2:

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

theorem WkEps_wfp1:

  P =eps=> P' ==> wfp P

theorem WkTau_wfp2:

  P =eps=> P' ==> wfp P'

theorem WkFOut_wfp1:

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

theorem WkFOut_wfp2:

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

theorem WkBOut_wfp1:

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

theorem WkBOut_wfpa2:

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

theorem WkIn_wfp1:

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

theorem WkIn_wfpa2:

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

theorem WkIn_wfp2:

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

theorem StTau_WkTau:

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

theorem WkTau_trans:

  [| P =tau=> P'; P' =tau=> P'' |] ==> P =tau=> P''

theorem WkTau_induct:

  [| P =tau=> P'; !!P'. P -tau-> P' ==> Pr P';
     !!P' P''. [| P =tau=> P'; P' -tau-> P''; Pr P' |] ==> Pr P'' |]
  ==> Pr P'

theorem WkTau_trans_induct:

  [| P =tau=> P'; !!P P'. P -tau-> P' ==> Pr P P';
     !!P P' P''.
        [| P =tau=> P'; Pr P P'; P' =tau=> P''; Pr P' P'' |] ==> Pr P P'' |]
  ==> Pr P P'

theorem WkEpsD:

  P =eps=> P' ==> (P, P') : RstrId | P =tau=> P'

theorem StTau_WkEps:

  P -tau-> P' ==> P =eps=> P'

theorem WkTau_WkEps:

  P =tau=> P' ==> P =eps=> P'

theorem WkEps_WkTau:

  [| P =eps=> P'; P ~= P' |] ==> P =tau=> P'

theorem StTau_rtrancl_WkEps:

  [| (P, P') : StTau^*; rstr P; rstr P' |] ==> P =eps=> P'

theorem WkEps_refl:

  rstr P ==> P =eps=> P

theorem WkEps_trans:

  [| P =eps=> P'; P' =eps=> P'' |] ==> P =eps=> P''

theorem WkEps_StTau_trans:

  [| P =eps=> P'; P' -tau-> P'' |] ==> P =eps=> P''

theorem lemma:

  [| P =eps=> P'; !!P. rstr P ==> Pr P;
     !!P' P''. [| P =eps=> P'; P' -tau-> P''; Pr P' |] ==> Pr P'' |]
  ==> rstr P' --> Pr P'

theorem WkEps_induct:

  [| P =eps=> P'; !!P. rstr P ==> Pr P;
     !!P' P''. [| P =eps=> P'; P' -tau-> P''; Pr P' |] ==> Pr P'' |]
  ==> Pr P'

theorem lemma:

  [| P =eps=> P'; !!P. rstr P ==> Pr P P;
     !!P P' P''. [| Pr P P'; P =eps=> P'; P' -tau-> P'' |] ==> Pr P P'' |]
  ==> rstr P & rstr P' --> Pr P P'

theorem WkEps_full_induct:

  [| P =eps=> P'; !!P. rstr P ==> Pr P P;
     !!P P' P''. [| Pr P P'; P =eps=> P'; P' -tau-> P'' |] ==> Pr P P'' |]
  ==> Pr P P'

theorem WkEps_trans_induct:

  [| P =eps=> P'; !!P. rstr P ==> rstr f P;
     !!P P'. P -tau-> P' ==> f P -tau-> f P' |]
  ==> f P =eps=> f P'

theorem WkFOutI:

  [| P =eps=> P'; P' -a<b>-> P'' |] ==> P =a<b>=> P''

theorem WkBOutI:

  [| P =eps=> P'; P' -a<>-> P'' |] ==> P =a<>=> P''

theorem WkInI:

  [| P =eps=> P'; P' -a[]-> P'' |] ==> P =a[]=> P''

theorem WkTauI:

  [| P =eps=> P'; P' -tau-> P'' |] ==> P =tau=> P''

theorem WkFOutD:

  P =a<b>=> P' ==> EX P''. P =eps=> P'' & P'' -a<b>-> P'

theorem WkBOutD:

  P =a<>=> fP' ==> EX P''. P =eps=> P'' & P'' -a<>-> fP'

theorem WkInD:

  P =a[]=> fP' ==> EX P''. P =eps=> P'' & P'' -a[]-> fP'

theorem WkTauD:

  P =tau=> P' ==> EX P''. P =eps=> P'' & P'' -tau-> P'

theorem WkEps_ta0:

  rstr P ==> .t.P =eps=> P

theorem lemma:

  P =eps=> P'
  ==> ALL fP fP'.
         P = fP c &
         P' = fP' c & rstra fP & rstra fP' & fresha c fP & fresha c fP' -->
         .#x. fP x =eps=> .#x. fP' x

theorem WkEps_ta1:

  [| P =eps=> P'; fresha c fP; fresha c fP'; rstra fP; rstra fP'; P = fP c;
     P' = fP' c |]
  ==> .#x. fP x =eps=> .#x. fP' x

theorem WkEps_ta3a:

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

theorem WkEps_ta3b:

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

theorem WkEps_ta4a:

  [| P =a<b>=> P'; Q =a[]=> fQ' |] ==> P .| Q =eps=> P' .| fQ' b

theorem WkEps_ta4b:

  [| P =a[]=> fP'; Q =a<b>=> Q' |] ==> P .| Q =eps=> fP' b .| Q'

theorem WkEps_ta5a:

  [| P =a<>=> fP'; Q =a[]=> fQ' |] ==> P .| Q =eps=> .#x. (fP' x .| fQ' x)

theorem WkEps_ta5b:

  [| P =a[]=> fP'; Q =a<>=> fQ' |] ==> P .| Q =eps=> .#x. (fP' x .| fQ' x)

theorem WkEps_par_trans:

  [| P =eps=> P'; Q =eps=> Q' |] ==> P .| Q =eps=> P' .| Q'

theorem StFOut_WkFOut:

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

theorem WkFOut_fo0:

  rstr P ==> a<b>.P =a<b>=> P

theorem WkFOut_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'

theorem WkFOut_fo3a:

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

theorem WkFOut_fo3b:

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

theorem StBOut_WkBOut:

  P -a<>-> P' ==> P =a<>=> P'

theorem WkBOut_bo0:

  [| fP c =a<c>=> fP' c; fresha c fP; fresha c fP'; a ~= c; rstra fP; rstra fP' |]
  ==> Res fP =a<>=> fP'

theorem WkBOut_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) |]
  ==> .#y. fP y =a<>=> (%x. .#y. ffP' y x)

theorem WkBOut_bo3a:

  [| P =a<>=> fP'; rstr Q |] ==> P .| Q =a<>=> (%x. fP' x .| Q)

theorem WkBOut_bo3b:

  [| Q =a<>=> fQ'; rstr P |] ==> P .| Q =a<>=> (%x. P .| fQ' x)

theorem StIn_WkIn:

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

theorem WkIn_in0:

  rstra fP ==> In a fP =a[]=> fP

theorem WkIn_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) |]
  ==> .#y. fP y =a[]=> (%x. .#y. ffP' y x)

theorem WkIn_in3a:

  [| P =a[]=> fP'; rstr Q |] ==> P .| Q =a[]=> (%x. fP' x .| Q)

theorem WkIn_in3b:

  [| Q =a[]=> fQ'; rstr P |] ==> P .| Q =a[]=> (%x. P .| fQ' x)

theorem WkTau_ta0:

  rstr P ==> .t.P =tau=> P

theorem WkTau_ta1:

  [| fP c =tau=> fP' c; fresha c fP; fresha c fP'; rstra fP; rstra fP' |]
  ==> Res fP =tau=> Res fP'

theorem WkTau_ta3a:

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

theorem WkTau_ta3b:

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

theorem WkTau_ta4a:

  [| P =a<b>=> P'; Q =a[]=> fQ' |] ==> P .| Q =tau=> P' .| fQ' b

theorem WkTau_ta4b:

  [| P =a[]=> fP'; Q =a<b>=> Q' |] ==> P .| Q =tau=> fP' b .| Q'

theorem WkTau_ta5a:

  [| P =a<>=> fP'; Q =a[]=> fQ' |] ==> P .| Q =tau=> .#x. (fP' x .| fQ' x)

theorem WkTau_ta5b:

  [| P =a[]=> fP'; Q =a<>=> fQ' |] ==> P .| Q =tau=> .#x. (fP' x .| fQ' x)