Theory ExistsBCF

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

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

- Uses same definition of indexed-alpha0 as in the proof of fresh-naming alpha
  confluence, and also introduces the concept of the number of lambda
  abstractions in a term

*)

ExistsBCF = AlphaZero + VarList +

consts
  lambdas :: "lterm => nat"

primrec
  var "lambdas(Var x) = 0"
  app "lambdas(e1 $ e2) = lambdas(e1) + lambdas(e2)"
  abs "lambdas(Abs x e) = 1 + lambdas(e)"

end

theorem cl_ialpha1_FV_lemma:

  (s, ys) ->>iA1 t ==> FV s = FV t

theorem cl_ialpha1_BV_lemma:

  (s, ys) ->>iA1 t ==> BV t <= BV s Un set ys

theorem cl_ialpha1_abs:

  (e, xs) ->>iA1 e' ==> x ~: set xs --> (Abs x e, xs) ->>iA1 Abs x e'

theorem cl_ialpha1_var_subst:

  (e, xs) ->>iA1 e'
  ==> y ~: set xs --> y ~: BV e --> (e[x:=Var y], xs) ->>iA1 e'[x:=Var y]

theorem BV_var_subst:

  BV (e[x:=Var y]) = BV e

theorem UB_var_subst:

  UB e --> UB (e[x:=Var y])

theorem FV_var_subst:

  x ~= y ==> FV (e[x:=Var y]) <= FV e Un {y}

theorem EBCF_aux_1:

  [| ALL z. z mem zs --> z ~: FV (Abs x e1) & z ~: BV (Abs x e1); zs = y # ys |]
  ==> ALL z. z mem ys --> z ~: BV e1 & z ~: FV e1

theorem EBCF_aux_2:

  ALL m xs.
     length xs = n + m -->
     (EX ys zs. xs = ys @ zs & length ys = n & length zs = m)

theorem EBCF_aux_3:

  length xs = n + m ==> EX ys zs. xs = ys @ zs & length ys = n & length zs = m

theorem EBCF_aux_4:

  ALL x. x mem ys @ zs --> P x
  ==> (ALL x. x mem ys --> P x) & (ALL x. x mem zs --> P x)

theorem uniqlist_property_1:

  uniqlist (ys @ zs) --> uniqlist ys & uniqlist zs

theorem uniqlist_property_2:

  uniqlist (ys @ zs) --> set ys Int set zs = {}

theorem EBCF_aux_5:

  (ALL x. x mem ys --> x ~: FV e1 & x ~: FV e2 & P x) -->
  FV e1 Int set ys = {} & FV e2 Int set ys = {}

theorem all_list_induct_1:

  ALL x. x mem y # ys --> P x ==> (ALL x. x mem ys --> P x) & P y

theorem cl_ialpha1_appL:

  (e1, xs) ->>iA1 e1'
  ==> ALL e2.
         (ALL x. x mem xs --> x ~: BV e2 Un FV e2) -->
         (e1 $ e2, xs) ->>iA1 e1' $ e2

theorem cl_ialpha1_appL:

  [| (e1, xs) ->>iA1 e1'; ALL x. x mem xs --> x ~: BV e2 Un FV e2 |]
  ==> (e1 $ e2, xs) ->>iA1 e1' $ e2

theorem cl_ialpha1_appR:

  (e1, xs) ->>iA1 e1'
  ==> ALL e2.
         (ALL x. x mem xs --> x ~: BV e2 Un FV e2) -->
         (e2 $ e1, xs) ->>iA1 e2 $ e1'

theorem cl_ialpha1_appR:

  [| (e1, xs) ->>iA1 e1'; ALL x. x mem xs --> x ~: BV e2 Un FV e2 |]
  ==> (e2 $ e1, xs) ->>iA1 e2 $ e1'

theorem cl_ialpha1_bigtrans:

  (e2, ys) ->>iA1 e3 ==> ALL e1 xs. (e1, xs) ->>iA1 e2 --> (e1, ys @ xs) ->>iA1 e3

theorem cl_ialpha1_bigtrans:

  [| (e1, xs) ->>iA1 e2; (e2, ys) ->>iA1 e3 |] ==> (e1, ys @ xs) ->>iA1 e3

theorem cl_ialpha1_doubleApp:

  [| (e1, xs) ->>iA1 e1'; ALL x. x mem xs --> x ~: BV e2 Un FV e2;
     (e2, ys) ->>iA1 e2'; ALL y. y mem ys --> y ~: BV e1' Un FV e1' |]
  ==> (e1 $ e2, ys @ xs) ->>iA1 e1' $ e2'

theorem key_to_BCF_existence:

  ALL xs.
     lambdas e1 = length xs -->
     uniqlist xs -->
     (ALL x. x mem xs --> x ~: FV e1 Un BV e1) -->
     (EX e2. (e1, rev xs) ->>iA1 e2 & BCF e2 & BV e2 = set xs)

theorem ExistsBCF:

  EX e2. e1 ->>A0 e2 & BCF e2