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