Theory VarList

Up to index of Isabelle/HOL/raw-confluence-lambda

(*  Title:      VarList.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    30th August, 2000

- Definition of lists of unique names

*)

VarList = Lambda +

consts  uniqlist :: "var list => bool"

primrec
  empty  "uniqlist([]) = True"
  cons   "uniqlist(y#ys) = (~(y mem ys) & uniqlist(ys))"

end

theorem list_theory_1:

  ¬ z mem x # xs --> x ~= z & ¬ z mem xs

theorem list_theory_2:

  ALL z. z mem zs --> ¬ z mem x # xs & Q z
  ==> (ALL z. z mem zs --> ¬ z mem xs & Q z) & (ALL z. z mem zs --> x ~= z)

theorem list_theory_3:

  ¬ y mem ys --> y ~: set ys

theorem list_theory_4:

  zs = y # ys ==> y mem zs

theorem list_theory_5:

  y ~: set ys --> ¬ y mem ys

theorem finite_var_lemma_1:

  length zs = x --> finite (FV e Un BV e Un set ys Un set zs)

theorem exists_suitable_z:

  length zs = x ==> EX z. z ~: FV e Un BV e Un set ys Un set zs

theorem mem_impl_set:

  z mem zs --> z : set zs

theorem set_impl_mem:

  z : set zs --> z mem zs

theorem exists_suitable_list:

  EX zs. length zs = n &
         uniqlist zs & (ALL z. z mem zs --> z ~: FV e Un BV e Un set ys)