Theory Congruence

Up to index of Isabelle/HOL/PI

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

consts
  PiCon :: "(('a::inf_class) procs * 'a procs) set"
  AxExp :: "(('a::inf_class) procs * 'a procs) set"

syntax
 "@PiCon" :: "[('a::inf_class) procs, 'a procs] => bool"
              (infixl ".~" 60)
 "@AxExp" :: "[('a::inf_class) procs, 'a procs] => bool"
              (infixl ".>" 60)

translations
  "P .~ Q" == "(P, Q) : PiCon"
  "P .> Q" == "(P, Q) : AxExp"

inductive "PiCon"
  intrs
   (* basic *)
    refl  "rstr P ==> P .~ P"
    symm  "[| P .~ Q |] ==> Q .~ P"
    trans "[| P .~ Q ; Q .~ R |] ==> P .~ R"

    (* congruence *)
    tau   "P .~ Q ==> .t.P .~ .t.Q"
    out    "P .~ Q ==> a<b>.P .~ a<b>.Q"
    inp   "[| fP c .~ fP' c ; rstra fP ; rstra fP' ; fresha c fP ; fresha c fP' |] \
            \ ==> a[x]. fP x .~ a[x]. fP' x"
    ch     "[| P .~ Q ; rstr R |] ==> P .+ R .~ Q .+ R"
    par    "[| P .~ Q ; rstr R |] ==> P .| R .~ Q .| R"
    res    "[| fP c .~ fP' c ; rstra fP ; rstra fP' ; fresha c fP ; fresha c fP' |] \
            \ ==> .#x. fP x .~ .#x. fP' x"
    mt     "P .~ Q ==> .[a.=b]P .~ .[a.=b]Q"
    rep    "[| fP c .~ fP' c ; rstra fP ; rstra fP' ; fresha c fP ; fresha c fP' |] \
            \ ==> .!a[x]. fP x .~ .!a[x]. fP' x"

    (* garbage collection *)
    n_ch   "rstr P ==> P .+ .0 .~ P"
    n_par  "rstr P ==> P .| .0 .~ P"
    n_res  "rstr P ==> .#x. (%x. P) x .~ P"
    n_rs1  "[| rstra fP ; rstr P |] ==> .#x. (%x. fP x .| P) x .~ (.#x. fP x) .| P"
    n_mt1  "rstr P ==> .[a.=a]P .~ P"
    n_mt2  "[| rstr P ; a~=b |] ==> .[a.=b]P .~ .0"

    (* symmetry *)
    c_sym  "[| rstr P ; rstr Q |] ==> P .+ Q .~ Q .+ P"
    p_sym  "[| rstr P ; rstr Q |] ==> P .| Q .~ Q .| P"

  monos
    rstr_mono_res,rstra_mono_res


inductive "AxExp"
  intrs
    (* basic *)
    con    "P .~ Q ==> P .> Q"
    trans  "[| P .> Q ; Q .> R |] ==> P .> R"

    (* precongruence *)
    par    "[| P .> Q ; rstr R |] ==> P .| R .> Q .| R"
    res    "[| fP c .> fP' c ; rstra fP ; rstra fP' ; fresha c fP ; fresha c fP' |] \
            \ ==> .#x. fP x .> .#x. fP' x"

    (* implicit steps *)
    s_tau  "rstr P ==> .t.(.t.P) .> .t.P"
    s_com  "[| ue{m}fP m ; ur{m}fQ m ; ~ rr{m}fP m ; ~ ee{m}fQ m ; \
             \ fP m -m<fa m>-> fP' m ; \
             \ fQ m -m[]-> ffQ' m ; rstra fP ; rstra fP' ; rstra fQ ; \
             \ ALL b. rstra ffQ' b ; ALL b. rstra (%x. ffQ' x b) ; wfna fa ; \
             \ fresha m fP ; fresha m fP' ; fresha m fQ ; freshaa m ffQ' ; \
             \ a ~: fnna fa |] ==> .#x. (fP x .| fQ x) .> .#x. (fP' x .| ffQ' m (fa x))"
  
end

theorem lemma:

  P .~ Q ==> rstr P & rstr Q

theorem PiCon_rstr1:

  P .~ Q ==> rstr P

theorem PiCon_rstr2:

  P .~ Q ==> rstr Q

theorem lemma:

  P .> Q ==> rstr P & rstr Q

theorem AxExp_rstr1:

  P .> Q ==> rstr P

theorem AxExp_rstr2:

  P .> Q ==> rstr Q

theorem n_res_ch_null:

  rstr P ==> .#x. procs.Plus P (.0) .~ P

theorem n_res_par_null:

  rstr P ==> .#x. (P .| .0) .~ P