Theory Receptive

Up to index of Isabelle/HOL/PI

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

consts
  RR :: "('a::inf_class) => ('a procs) set"
  EE :: "('a::inf_class) => ('a procs) set"
  UR :: "('a::inf_class) => ('a procs) set"
  UE :: "('a::inf_class) => ('a procs) set"

syntax
 "@RR" :: "[('a::inf_class), 'a procs] => bool"
           ("rr{_}(_)" [0,100] 90)
 "@EE" :: "[('a::inf_class), 'a procs] => bool"
           ("ee{_}(_)" [0,100] 90)
 "@UR" :: "[('a::inf_class), 'a procs] => bool"
           ("ur{_}(_)" [0,100] 90)
 "@UE" :: "[('a::inf_class), 'a procs] => bool"
           ("ue{_}(_)" [0,100] 90)

translations
  "rr{m}P" == "P : RR m"
  "ee{m}P" == "P : EE m"
  "ur{m}P" == "P : UR m"
  "ue{m}P" == "P : UE m"

inductive "RR m"
  intrs
    rr0  "rstra fP ==> rr{m}m[x].fP x"

    rr1a "[| rr{m}P ; rstr Q |] ==> rr{m}(P .+ Q)"
    rr1b "[| rr{m}Q ; rstr P |] ==> rr{m}(P .+ Q)"

    rr2a "[| rr{m}P ; rstr Q |] ==> rr{m}(P .| Q)"
    rr2b "[| rr{m}Q ; rstr P |] ==> rr{m}(P .| Q)"

    rr3  "[| rr{m}(fP n) ; m ~= n ; fresha n fP ; rstra fP |] \
          \ ==> rr{m}(.#x. fP x)"

    rr4  "[| rr{m}P ; a=b |] ==> rr{m}(.[a.=b]P)"

    rr5  "rstra fP ==> rr{m}(.!m[x].fP x)"

inductive "EE m"
  intrs
    ee0  "rstr P ==> ee{m}m<b>.P"

    ee1a "[| ee{m}P ; rstr Q |] ==> ee{m}(P .+ Q)"
    ee1b "[| ee{m}Q ; rstr P |] ==> ee{m}(P .+ Q)"

    ee2a "[| ee{m}P ; rstr Q |] ==> ee{m}(P .| Q)"
    ee2b "[| ee{m}Q ; rstr P |] ==> ee{m}(P .| Q)"

    ee3  "[| ee{m}(fP n) ; m ~= n ; fresha n fP ; rstra fP |] \
          \  ==> ee{m}(.#x. fP x)"

    ee4  "[| ee{m}P ; a=b |] ==> ee{m}(.[a.=b]P)"

inductive "UR m"
  intrs
    ur0  "rstra fP ==> ur{m}m[x].fP x"

    ur1a "[| ur{m}P ; rstr Q ; ~ rr{m}Q |] ==> ur{m}(P .+ Q)"
    ur1b "[| ur{m}Q ; rstr P ; ~ rr{m}P |] ==> ur{m}(P .+ Q)"

    ur2a "[| ur{m}P ; rstr Q ; ~ rr{m}Q |] ==> ur{m}(P .| Q)"
    ur2b "[| ur{m}Q ; rstr P ; ~ rr{m}P |] ==> ur{m}(P .| Q)"

    ur5  "rstra fP ==> ur{m}(.!m[x].fP x)"

inductive "UE m"
  intrs
    ue0  "rstr P ==> ue{m}m<b>.P"

    ue1a "[| ue{m}P ; rstr Q ; ~ ee{m}Q |] ==> ue{m}(P .+ Q)"
    ue1b "[| ue{m}Q ; rstr P ; ~ ee{m}P |] ==> ue{m}(P .+ Q)"

    ue2a "[| ue{m}P ; rstr Q ; ~ ee{m}Q |] ==> ue{m}(P .| Q)"
    ue2b "[| ue{m}Q ; rstr P ; ~ ee{m}P |] ==> ue{m}(P .| Q)"

(*
inductive "UR m"
  intrs
    ur0  "rstra fP ==> ur{m}m[x].fP x"

    ur1a "[| ur{m}P ; rstr Q ; ~ rr{m}Q |] ==> ur{m}(P .+ Q)"
    ur1b "[| ur{m}Q ; rstr P ; ~ rr{m}P |] ==> ur{m}(P .+ Q)"

    ur2a "[| ur{m}P ; rstr Q ; ~ rr{m}Q |] ==> ur{m}(P .| Q)"
    ur2b "[| ur{m}Q ; rstr P ; ~ rr{m}P |] ==> ur{m}(P .| Q)"

    ur3  "[| ur{m}(fP n) ; m ~= n ; fresha n fP ; rstra fP |] \
          \ ==> ur{m}(.#x. fP x)"

    ur4  "[| ur{m}P ; a=b |] ==> ur{m}(.[a.=b]P)"

    ur5  "rstra fP ==> ur{m}(.!m[x].fP x)"

inductive "UE m"
  intrs
    ue0  "rstr P ==> ue{m}m<b>.P"

    ue1a "[| ue{m}P ; rstr Q ; ~ re{m}Q |] ==> ue{m}(P .+ Q)"
    ue1b "[| ue{m}Q ; rstr P ; ~ re{m}P |] ==> ue{m}(P .+ Q)"

    ue2a "[| ue{m}P ; rstr Q ; ~ re{m}Q |] ==> ue{m}(P .| Q)"
    ue2b "[| ue{m}Q ; rstr P ; ~ re{m}P |] ==> ue{m}(P .| Q)"

    ue3  "[| ue{m}(fP n) ; m ~= n ; fresha n fP ; rstra fP |] \
          \ ==> ue{m}(.#x. fP x)"

    ue4  "[| ue{m}P ; a=b |] ==> ue{m}(.[a.=b]P)"
*)
end

theorem rr_rstr:

  rr{m}P ==> rstr P

theorem ee_rstr:

  ee{m}P ==> rstr P

theorem ur_rstr:

  ur{m}P ==> rstr P

theorem ue_rstr:

  ue{m}P ==> rstr P

theorem ur_rr:

  ur{m}P ==> rr{m}P

theorem ue_ee:

  ue{m}P ==> ee{m}P

theorem rr_StIn:

  rr{m}P ==> EX fP. P -m[]-> fP

theorem ee_StOut:

  ee{m}P ==> (EX b P'. P -m<b>-> P') | (EX fP. P -m<>-> fP)

theorem ur_StIn:

  ur{m}P ==> EX fP. P -m[]-> fP

theorem ue_StOut:

  ue{m}P ==> (EX b P'. P -m<b>-> P') | (EX fP. P -m<>-> fP)

theorem StIn_rr:

  P -m[]-> fP ==> rr{m}P

theorem StFOut_ee:

  P -m<b>-> P' ==> ee{m}P

theorem StBOut_ee:

  P -m<>-> fP ==> ee{m}P

theorem not_rr_not_StIn:

  [| P ~: RR m; P -m[]-> fP |] ==> Pr

theorem not_ee_not_StFOut:

  [| P ~: EE m; P -m<b>-> P' |] ==> Pr

theorem not_ee_not_StBOut:

  [| P ~: EE m; P -m<>-> fP |] ==> Pr

theorem lemma:

  ur{m}P ==> ALL fP fP'. P -m[]-> fP & P -m[]-> fP' --> fP = fP'

theorem ur_unique:

  [| ur{m}P; P -m[]-> fP; P -m[]-> fP' |] ==> fP = fP'

theorem lemma:

  ue{m}P ==> ALL a b P' P''. P -m<a>-> P' & P -m<b>-> P'' --> a = b & P' = P''

theorem ue_unique_FOut_FOut:

  [| ue{m}P; P -m<a>-> P'; P -m<b>-> P'' |] ==> a = b & P' = P''

theorem lemma:

  ue{m}P ==> ALL a b fP fP'. P -m<>-> fP & P -m<>-> fP' --> fP = fP'

theorem ue_unique_BOut_BOut:

  [| ue{m}P; P -m<>-> fP; P -m<>-> fP' |] ==> fP = fP'

theorem lemma:

  ue{m}P ==> ALL a P' fP'. P -m<a>-> P' & P -m<>-> fP' --> Pr

theorem ue_unique_FOut_BOut:

  [| ue{m}P; P -m<a>-> P'; P -m<>-> fP' |] ==> Pr