Theory FreshAlphaConf

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

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

*)

FreshAlphaConf = AlphaZero + VarList

theorem BV_Un_FV_induct_1:

  y ~: BV (Abs x e) Un FV (Abs x e) ==> y ~: BV e Un FV e

theorem BV_Un_FV_induct_2:

  y ~: BV (e1 $ e2) Un FV (e1 $ e2) ==> y ~: BV e1 Un FV e1 & y ~: BV e2 Un FV e2

theorem FAC_proposition_1:

  y ~: BV e Un FV e --> (e, y) ->iA1 e

theorem FAC_proposition_2:

  (e, y) ->iA1 e' ==> y ~: BV e Un FV e

theorem FAC_lemma_3:

  (e1, z1) ->iA1 e2
  ==> ALL e3.
         (e1, z2) ->iA1 e3 -->
         z1 ~= z2 --> (EX e4. (e2, z2) ->iA1 e4 & (e3, z1) ->iA1 e4)

theorem FAC_lemma_3:

  [| (e1, z1) ->iA1 e2; (e1, z2) ->iA1 e3; z1 ~= z2 |]
  ==> EX e4. (e2, z2) ->iA1 e4 & (e3, z1) ->iA1 e4

theorem FAC_lemma_4:

  (e1, y) ->iA e2
  ==> z ~: FV e1 Un BV e1 Un {y} --> (EX e3. (e1, z) ->iA1 e3 & (e2, z) ->iA1 e3)

theorem FAC_lemma_4:

  [| (e1, y) ->iA e2; z ~: FV e1 Un BV e1 Un {y} |]
  ==> EX e3. (e1, z) ->iA1 e3 & (e2, z) ->iA1 e3

theorem FAC_lemma_6:

  (e1, zs) ->>iA1 e2
  ==> ALL e3.
         (e1, z) ->iA1 e3 -->
         ¬ z mem zs --> (EX e4. (e2, z) ->iA1 e4 & (e3, zs) ->>iA1 e4)

theorem FAC_lemma_6:

  [| (e1, zs) ->>iA1 e2; (e1, z) ->iA1 e3; ¬ z mem zs |]
  ==> EX e4. (e2, z) ->iA1 e4 & (e3, zs) ->>iA1 e4

theorem list_induct_aux:

  [| ALL z. z mem zs --> ¬ z mem xs & z ~: BV e1 & z ~: FV e1; zs = y # ys |]
  ==> ALL z. z mem ys --> ¬ z mem xs & z ~: BV e1 & z ~: FV e1

theorem uniqlist_induct_1:

  [| uniqlist zs; zs = y # ys |] ==> uniqlist ys & ¬ y mem ys

theorem FAC_lemma_5:

  (e1, xs) ->>ciA e2
  ==> ALL zs.
         length zs = length xs -->
         uniqlist zs -->
         (ALL z. z mem zs --> ¬ z mem xs & z ~: BV e1 Un FV e1) -->
         (EX e3. (e1, zs) ->>iA1 e3 & (e2, rev zs) ->>iA1 e3)

theorem FAC_lemma_5:

  [| (e1, xs) ->>ciA e2; uniqlist zs; length zs = length xs;
     ALL z. z mem zs --> ¬ z mem xs & z ~: BV e1 Un FV e1 |]
  ==> EX e3. (e1, zs) ->>iA1 e3 & (e2, rev zs) ->>iA1 e3

theorem FAC_lemma_7:

  e1 ->>A e2 ==> EX e3. e1 ->>A0 e3 & e2 ->>A0 e3

theorem alphaeq_trans:

  [| x =A= y; y =A= z |] ==> x =A= z

theorem rt_alpha_in_alphaeq:

  e ->>A e' ==> e =A= e'

theorem FreshAlphaConf:

  [| e ->>A e1; e ->>A e2 |] ==> EX e3. e1 ->>A0 e3 & e2 ->>A0 e3