Theory Alpha

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

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

- Single and transitive-reflexive alpha-reduction.
- Inverse alpha-reduction and notion of alpha-equivalence.

*)


Alpha = SubstLemmas +
  
consts  sq_alpha  :: "(lterm * var * lterm) set"
        i_alpha   :: "(lterm * var * lterm) set"
        alpha     :: "(lterm * lterm) set"
        rev_alpha :: "(lterm * lterm) set"
  
syntax  "->sA", "->iA"  :: [lterm,var,lterm] => bool (infixl 50)
        "->A", "->>A"   :: [lterm,lterm] => bool (infixl 50)
        "A<-", "=A="    :: [lterm,lterm] => bool (infixl 50)
  
translations
  "(s,x) ->sA t"  == "(s,x,t) : sq_alpha"
  "(s,x) ->iA t"  == "(s,x,t) : i_alpha"
  "s ->A t"       == "(s,t) : alpha"
  "s ->>A t"      == "(s,t) : alpha^*"
  "s A<- t"       == "(s,t) : rev_alpha"
  "s =A= t"       == "(s,t) : (alpha Un rev_alpha)^*"

inductive sq_alpha  (* rewriting on an alpha-enabled redex *)
intrs
  alpha  "[|x~=y; y~:(FV(e) Un Capt x e)|] ==>
          ((Abs x e),y) ->sA (Abs y (e[x:=Var y]))"

inductive i_alpha   (* contextual closure of 'squiggly alpha' *)
intrs
  index  "(s,y) ->sA t ==> (s,y) ->iA t"
  aappL  "(s,y) ->iA t ==> (s$u,y) ->iA t$u"
  aappR  "(s,y) ->iA t ==> (u$s,y) ->iA u$t"
  aabs   "(s,y) ->iA t ==> ((Abs x s),y) ->iA (Abs x t)"
  
inductive alpha     (* version of i_alpha without variable indices *)
intrs
  strip  "(s,y) ->iA t ==> s ->A t"  

inductive rev_alpha (* the symmetric of alpha *)
intrs
  rev    "s ->A t ==> t A<- s"
  
end

theorem alphaeq_sym:

  e1 =A= e2 ==> e2 =A= e1

theorem aux_symmetry_lemma_1:

  [| x ~= y; y ~: Capt x e |] ==> x ~: FV (e[x:=Var y])

theorem aux_symmetry_lemma_2:

  x ~= y & y ~: FV e & y ~: Capt x e --> x ~: Capt y (e[x:=Var y])

theorem local_alpha_symmetry_1:

  (Abs x e, y) ->sA Abs y (e[x:=Var y])
  ==> (Abs y (e[x:=Var y]), x) ->sA Abs x (e[x:=Var y][y:=Var x])

theorem renaming4_enabled:

  (Abs x e, y) ->sA Abs y (e[x:=Var y]) ==> e = e[x:=Var y][y:=Var x]

theorem local_alpha_symmetry_2:

  (Abs x e, y) ->sA Abs y (e[x:=Var y]) ==> (Abs y (e[x:=Var y]), x) ->sA Abs x e

theorem local_alpha_symmetry_3:

  [| x ~= y; y ~: FV e; y ~: Capt x e |] ==> (Abs y (e[x:=Var y]), x) ->sA Abs x e

theorem squiggly_alpha_symmetric:

  (e, y) ->sA e' ==> EX x. (e', x) ->sA e

theorem index_alpha_symmetric:

  (e, y) ->iA e' ==> EX x. (e', x) ->iA e

theorem alpha_symmetric:

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

theorem Lemma_D:

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