# 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`