Theory WeakABComm

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

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

- Proof of weak commutativity of parallel-beta and alpha-0 
*)

WeakABComm = AlphaZero + ParBeta

theorem lemmaA_aux_1:

  [| e -|>B e'; y ~: FV e; y ~: BV e; x ~= y |]
  ==> (Abs x e', y) ->>iA Abs y (e'[x:=Var y])

theorem lemmaA_aux_2:

  [| e -|>B e'; y ~: FV e; y ~: BV e |] ==> e[x:=Var y] -|>B e'[x:=Var y]

theorem FV_Un_BV_induct_1:

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

theorem lemmaA_aux_3:

  [| Capt x e' Int A = {}; e -|>B e'; y ~: FV e; y ~: BV e; x ~= y |]
  ==> Capt y (e'[x:=Var y]) Int A = {}

theorem i_alpha_Capt_lemma_1:

  (s, y) ->iA t ==> x ~= y --> Capt x t <= Capt x s Un {y}

theorem rt_ialpha_Capt_lemma_1:

  (s, y) ->>iA t ==> x ~= y --> Capt x t <= Capt x s Un {y}

theorem ialpha_abs_elim:

  (Abs x s, y) ->iA Abs x t ==> (s, y) ->iA t

theorem rt_ialpha_abs_elim_aux:

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

theorem rt_ialpha_abs_elim:

  (s, y) ->>iA t
  ==> ALL s' t'. s = Abs x s' & t = Abs x t' --> x ~= y --> (s', y) ->>iA t'

theorem rt_ialpha_abs_elim:

  (Abs x s, y) ->>iA Abs x t ==> x ~= y --> (s, y) ->>iA t

theorem sq_alpha_substitutivity:

  (s, y) ->sA t
  ==> Capt x s Int FV u = {} -->
      Capt x t Int FV u = {} --> x ~= y --> (s[x:=u], y) ->sA t[x:=u]

theorem i_alpha_substitutivity:

  (s, y) ->iA t
  ==> Capt x s Int FV u = {} -->
      Capt x t Int FV u = {} --> x ~= y --> (s[x:=u], y) ->iA t[x:=u]

theorem subset_lemma_3:

  [| A Int B = {}; C <= A Un {x}; x ~: B |] ==> C Int B = {}

theorem rt_ialpha_substitutivity:

  (s, y) ->>iA t
  ==> x ~= y -->
      y ~: FV u -->
      Capt x s Int FV u = {} -->
      Capt x t Int FV u = {} --> (s[x:=u], y) ->>iA t[x:=u]

theorem rt_ialpha_easy_substitutivity:

  [| (s, y) ->>iA t; x ~= y |] ==> (e[x:=s], y) ->>iA e[x:=t]

theorem key_to_WeakABComm:

  (s, y) ->iA0 t ==> ALL t'. s -|>B t' --> (EX s'. t -|>B s' & (t', y) ->>iA s')

theorem real_key_to_WeakABComm:

  [| s ->A0 t; s -|>B t' |] ==> EX s'. t -|>B s' & t' ->>A s'

theorem WeakABComm:

  [| s ->>A0 t; s -|>B t' |] ==> EX s'. t -|>B s' & t' ->>A s'