Theory WellFormed

Up to index of Isabelle/HOL/PI

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

Inductive predicates define the sets of well-formed processes and
well-formed process abstractions, and rule out exotic terms.
*)

WellFormed = Procs +

(* well-formedness of names *)
consts
  WFNA  :: (('a::inf_class) => 'a) set
  WFNAA :: (('a::inf_class) => 'a => 'a) set

syntax
  "@WFNA"  :: (('a::inf_class) => 'a) => bool
              ("wfna (_)" [100] 90)
  "@WFNAA" :: (('a::inf_class) => 'a => 'a) => bool
              ("wfnaa (_)" [100] 90)

translations
  "wfna fa" == "fa : WFNA"
  "wfnaa ffa" == "ffa : WFNAA"

inductive WFNA
  intrs
    w1 "wfna (%x. x)"              (* identity *)
    w2 "wfna (%x. a)"              (* constants *)

inductive WFNAA
  intrs
    w1 "wfnaa (%x y. x)"           (* identity *)
    w2 "wfnaa (%x y. y)"           (* identity *)
    w3 "wfnaa (%x y. a)"           (* constants *)


(* well-formedness of processes *)
consts
  WFP   :: (('a::inf_class) procs) set
  WFPA  :: (('a::inf_class) => ('a procs)) set

syntax
  "@WFP"  :: (('a::inf_class) procs) => bool
             ("wfp (_)" [100] 90)
  "@WFPA" :: (('a::inf_class) => ('a procs)) => bool
             ("wfpa (_)" [100] 90)

translations
  "wfp P"  == "P : WFP"
  "wfpa P" == "P : WFPA"

inductive WFP
  intrs
    Null  "wfp (.0)"
    Tau   "wfp P ==> wfp (.t.P)"
    Out   "wfp P ==> wfp (a<b>.P)"
    In    "wfpa fP ==> wfp (a[x].fP x)"
    Res   "wfpa fP ==> wfp (.#x. fP x)"
    Plus  "[| wfp P ; wfp Q |] ==> wfp (P .+ Q)"
    Par   "[| wfp P ; wfp Q |] ==> wfp (P .| Q)"
    Mt    "wfp P ==> wfp (.[a.=b]P)"
    Mmt   "wfp P ==> wfp (.[a.~=b]P)"
    Repl  "wfp P ==> wfp (.!P)"

inductive WFPA
  intrs
    Null  "wfpa (%x. .0)"
    Tau   "wfpa fP ==> wfpa (%x. .t.fP x)"
    Out   "[| wfpa fP ; wfna fa ; wfna fb |] \
            \ ==> wfpa (%x. fa x<fb x>.fP x)"
    In    "[| ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) ; \
            \ wfna fa |] ==> wfpa (%x. fa x[y].ffP y x)"
    Res   "[| ALL b. wfpa (ffP b) ; ALL b. wfpa (%x. ffP x b) |] \
            \ ==> wfpa (%x. .#y. ffP y x)"
    Plus  "[| wfpa fP ; wfpa fQ |] ==> wfpa (%x. fP x .+ fQ x)"
    Par   "[| wfpa fP ; wfpa fQ |] ==> wfpa (%x. fP x .| fQ x)"
    Mt    "[| wfpa fP ; wfna fa ; wfna fb |] \
            \ ==> wfpa (%x. .[fa x.=fb x]fP x)"
    Mmt   "[| wfpa fP ; wfna fa ; wfna fb |] \
            \ ==> wfpa (%x. .[fa x.~=fb x]fP x)"
    Repl  "wfpa fP ==> wfpa (%x. .!fP x)"

end

theorem wfnaa_wfna1:

  wfnaa ffa ==> wfna ffa a

theorem wfnaa_wfna2:

  wfnaa ffa ==> wfna (%x. ffa x a)

theorem fnna_subset:

  [| wfna fa; fnna fa <= A; a : A |] ==> fa a : A

theorem fresh_names_eq:

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

theorem fresh_names_ineq:

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

theorem lemma:

  wfna fa ==> a ~: fnna fa --> nsubst a b (fa a) = fa b

theorem wfna_nsubst:

  [| wfna fa; a ~: fnna fa |] ==> nsubst a b (fa a) = fa b

theorem wfpa_wfp_mono:

  wfpa fP ==> wfp fP a

theorem wfpa_cases0:

  [| .0 = fP a; wfpa fP |] ==> fP = (%x. .0)

theorem wfpa_cases1:

  [| .t.P = fP a; wfpa fP |] ==> EX fP'. wfpa fP' & fP = (%x. .t.fP' x)

theorem wfpa_cases2:

  [| b<c>.P = fP a; wfpa fP |]
  ==> EX fb fc fP'. wfna fb & wfna fc & wfpa fP' & fP = (%x. fb x<fc x>.fP' x)

theorem wfpa_cases3:

  [| In b fP' = fP a; wfpa fP |]
  ==> EX fb ffP.
         wfna fb &
         (ALL b. wfpa ffP b) &
         (ALL b. wfpa (%x. ffP x b)) & fP = (%x. In (fb x) (%y. ffP y x))

theorem wfpa_cases4:

  [| .#y. fP' y = fP a; wfpa fP |]
  ==> EX ffP.
         (ALL b. wfpa ffP b) &
         (ALL b. wfpa (%x. ffP x b)) & fP = (%x. .#y. ffP y x)

theorem wfpa_cases5:

  [| procs.Plus P Q = fP a; wfpa fP |]
  ==> EX fP' fQ. wfpa fP' & wfpa fQ & fP = (%x. procs.Plus (fP' x) (fQ x))

theorem wfpa_cases6:

  [| P .| Q = fP a; wfpa fP |]
  ==> EX fP' fQ. wfpa fP' & wfpa fQ & fP = (%x. fP' x .| fQ x)

theorem wfpa_cases7:

  [| .[b.=c]P = fP a; wfpa fP |]
  ==> EX fb fc fP'. wfna fb & wfna fc & wfpa fP' & fP = (%x. .[fb x.=fc x]fP' x)

theorem wfpa_cases8:

  [| .[b.~=c]P = fP a; wfpa fP |]
  ==> EX fb fc fP'. wfna fb & wfna fc & wfpa fP' & fP = (%x. .[fb x.~=fc x]fP' x)

theorem wfpa_cases9:

  [| .!P = fP a; wfpa fP |] ==> EX fP'. wfpa fP' & fP = (%x. .!fP' x)

theorem lemma:

  wfpa fP ==> a : fn (fP c) & a ~= c --> a : fn (fP b)

theorem fn_fn:

  [| wfpa fP; a : fn (fP c); a ~= c |] ==> a : fn (fP b)

theorem lemma:

  wfpa fP ==> a ~: fn (fP b) & a ~= c --> a ~: fn (fP c)

theorem not_fn_fn:

  [| wfpa fP; a ~: fn (fP b); a ~= c |] ==> a ~: fn (fP c)

theorem fresh_fresh:

  [| wfpa fP; fresh a (fP b); a ~= c |] ==> fresh a (fP c)

theorem fn_fna:

  [| wfpa fP; a : fn (fP c); a ~= c |] ==> a : fna fP

theorem not_fna_fn:

  [| wfpa fP; a ~: fna fP; a ~= c |] ==> a ~: fn (fP c)

theorem fresha_fresh:

  [| wfpa fP; fresha a fP; a ~= c |] ==> fresh a (fP c)

theorem fna_fnaa:

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

theorem not_fnaa_fna:

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

theorem freshaa_fresha:

  [| ALL b. wfpa ffP b; ALL b. wfpa (%x. ffP x b); freshaa a ffP; a ~= c |]
  ==> fresha a (ffP c)

theorem rev_contra_subsetD:

  [| A <= B; x ~: B |] ==> x ~: A

theorem fnaa_fna_subset:

  [| ALL b. wfpa ffP b; ALL b. wfpa (%x. ffP x b); fnaa ffP <= A |]
  ==> fna (ffP a) <= insert a A

theorem fna6:

  [| wfpa fP; wfpa fQ |] ==> fna (%x. fP x .| fQ x) = fna fP Un fna fQ

theorem lemma1:

  [| ALL b a ba c d. dob (ffP b a) ba = dob (ffP b c) d;
     ALL b a ba c d. dob (ffP a b) ba = dob (ffP c b) d |]
  ==> dob (ffP b a) b = dob (ffP d c) d

theorem lemma2:

  [| ALL a b c d. dob (fP a) b = dob (fP c) d;
     ALL a b c d. dob (fQ a) b = dob (fQ c) d |]
  ==> max (dob (fP a) b) (dob (fQ a) b) = max (dob (fP c) d) (dob (fQ c) d)

theorem lemma:

  wfpa fP ==> ALL a b c d. dob (fP a) b = dob (fP c) d

theorem dob_vara:

  wfpa fP ==> dob (fP a) b = dob (fP c) d

theorem doba_vara:

  wfpa fP ==> doba fP a = doba fP b

theorem dob_var:

  wfp P ==> dob P a = dob P b

theorem lemma:

  [| ALL b. wfpa ffP b; ALL b. wfpa (%x. ffP x b) |]
  ==> doba (ffP a) b = doba (ffP c) b

theorem doba_varaa:

  [| ALL b. wfpa ffP b; ALL b. wfpa (%x. ffP x b) |]
  ==> doba (ffP a) b = doba (ffP c) d