Theory ProcExt

Up to index of Isabelle/HOL/PI

theory ProcExt = WellFormed
files [ProcExt.ML]:
```(* Title:    ProcExt.thy
Author:   Christine Roeckl

Deriving a proof technique for the equality of process abstractions:
In order to show that two well-formed process abstractions are equal,
it suffices to prove equality for their instantiations with one fresh
name.
*)

ProcExt = WellFormed
```

theorem ext_na:

`  [| wfna fa; wfna fb; fa a = fb a; a ~: fnna fa; a ~: fnna fb |] ==> fa = fb`

theorem lemma:

`  finite ({a, c} Un fnaa ffP Un fnaa ffQ)`

theorem fresh_ext:

`  EX d. d ~= a & d ~= c & d ~: fnaa ffP & d ~: fnaa ffQ`

theorem inst_hyp:

```  [| ALL b fQ a.
wfpa fQ & ffP b a = fQ a & a ~: fna (ffP b) & a ~: fna fQ --> ffP b = fQ;
ALL b fQ a.
wfpa fQ & ffP a b = fQ a & a ~: fna (%x. ffP x b) & a ~: fna fQ -->
(%x. ffP x b) = fQ;
ALL b. wfpa ffP b; ALL b. wfpa (%x. ffP x b); ALL b. wfpa ffQ b;
ALL b. wfpa (%x. ffQ x b); a ~: fnaa ffP; a ~: fnaa ffQ;
(%x. ffP x a) = (%x. ffQ x a) |]
==> (%x. ffP x c) = (%x. ffQ x c)```

theorem lemma:

```  wfpa fP
==> ALL fQ a. wfpa fQ & fP a = fQ a & a ~: fna fP & a ~: fna fQ --> fP = fQ```

theorem ext_pa:

`  [| wfpa fP; wfpa fQ; fP a = fQ a; fresha a fP; fresha a fQ |] ==> fP = fQ`

theorem ext_paa:

```  [| ALL b. wfpa ffP b; ALL b. wfpa (%x. ffP x b); ALL b. wfpa ffQ b;
ALL b. wfpa (%x. ffQ x b); ffP a = ffQ a; freshaa a ffP; freshaa a ffQ |]
==> ffP = ffQ```