Up to index of Isabelle/HOL/raw-confluence-lambda
theory Alpha = SubstLemmas(* 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