Theory AlphaZero

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

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

- We first present two different reflexive/transitive closures of the indexed
  alpha relation.  The first insists that the same name be chosen for each
  alpha reduction; the second allows the use of different names and accumulates
  them in a list.  Both versions are essential in proving key lemmas later.

- We also present two versions of the alpha-0 relation.  The first is simply
  indexed alpha with an additional fresh-naming requirement.  The second (which
  for simplicity we call alpha-1) is defined independently and is reflexive.
  However, the reflexive/transitive closures of alpha-0 and alpha-1 are
  completely equivalent.

*)


AlphaZero = Lambda + Alpha +
  
consts  rt_ialpha  :: "(lterm * var * lterm) set"
        cl_ialpha  :: "(lterm * var list * lterm) set"
        i_alpha0   :: "(lterm * var * lterm) set"
        alpha0     :: "(lterm * lterm) set"
        i_alpha1   :: "(lterm * var * lterm) set"
        cl_ialpha1 :: "(lterm * var list * lterm) set"
  
syntax  "->>iA"         :: [lterm,var,lterm] => bool (infixl 50)
        "->>ciA"        :: [lterm,var list,lterm] => bool (infixl 50)
        "->iA0","->iA1" :: [lterm,var,lterm] => bool (infixl 50)
        "->A0", "->>A0" :: [lterm,lterm] => bool (infixl 50)
        "->>iA1"        :: [lterm,var list,lterm] => bool (infixl 50)
  
translations
  "(s,x) ->>iA t" == "(s,x,t) : rt_ialpha"
  "(s,x) ->iA0 t" == "(s,x,t) : i_alpha0"
  "s ->A0 t"      == "(s,t) : alpha0"
  "s ->>A0 t"     == "(s,t) : alpha0^*"
  "(s,x) ->iA1 t"   == "(s,x,t) : i_alpha1"
  "(s,xs) ->>iA1 t" == "(s,xs,t) : cl_ialpha1"
  "(s,xs) ->>ciA t"  == "(s,xs,t) : cl_ialpha"

inductive rt_ialpha (* requires we use the same alpha-name each time *)
intrs
  refl   "(s,y) ->>iA s"
  trans  "[|(s,y) ->>iA t; (t,y) ->iA u|] ==> (s,y) ->>iA u"

inductive cl_ialpha (* accumulates list of used alpha-names *)
intrs
  refl   "(e,[]) ->>ciA e"
  trans  "[|(e1,xs) ->>ciA e2; (e2,x) ->iA e3|] ==> (e1,x#xs) ->>ciA e3"
 
inductive i_alpha0  (* i_alpha with a variable fresh-naming requirement *)
intrs
  ialpha0 "[|(s,y) ->iA t; y~:(FV(s) Un BV(s))|] ==> (s,y) ->iA0 t" 
  
inductive alpha0    
intrs
  strip   "(s,y) ->iA0 t ==> s ->A0 t"

inductive i_alpha1  (* essentially the same as i_alpha0, but reflexive  *)
intrs
  var    "x~=y ==> (Var x,y) ->iA1 Var x"
  contr  "y~:(BV(Abs x e) Un FV(Abs x e)) ==>
          (Abs x e,y) ->iA1 Abs y (e[x:=Var y])"
  abs    "[|(e,y) ->iA1 e'; x~=y|] ==> (Abs x e,y) ->iA1 Abs x e'"
  appL   "[|(e1,y) ->iA1 e1'; y~:(BV(e2) Un FV(e2))|] ==>
          (e1 $ e2,y) ->iA1 e1' $ e2"
  appR   "[|(e2,y) ->iA1 e2'; y~:(BV(e1) Un FV(e1))|] ==>
          (e1 $ e2,y) ->iA1 e1 $ e2'"

inductive cl_ialpha1 (* equivalent to (alpha0)^* *)
intrs
  refl   "(e,[]) ->>iA1 e"
  trans  "[|(e1,xs) ->>iA1 e2; (e2,x) ->iA1 e3|] ==> (e1,x#xs) ->>iA1 e3"


end

theorem rt_ialpha_base:

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

theorem rt_ialpha_in_alpha:

  (s, y) ->>iA t ==> s ->>A t

theorem rt_ialpha_abs:

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

theorem rt_ialpha_appL:

  (s, y) ->>iA t ==> (s $ u, y) ->>iA t $ u

theorem rt_ialpha_appR:

  (s, y) ->>iA t ==> (u $ s, y) ->>iA u $ t

theorem rt_ialpha_bigtrans:

  (t, y) ->>iA u ==> ALL s. (s, y) ->>iA t --> (s, y) ->>iA u

theorem rt_ialpha_bigtrans:

  [| (s, y) ->>iA t; (t, y) ->>iA u |] ==> (s, y) ->>iA u

theorem rt_ialpha_doubleApp:

  (s1, y) ->>iA t1 ==> (s2, y) ->>iA t2 --> (s1 $ s2, y) ->>iA t1 $ t2

theorem ialpha_FV_lemma:

  (s, y) ->iA t ==> FV t = FV s

theorem rt_ialpha_FV_lemma:

  (s, y) ->>iA t ==> FV s = FV t

theorem BV_subst_lemma_2:

  Capt x e Int FV e' = {} -->
  BV (e[x:=e']) = (if x : FV e then BV e Un BV e' else BV e)

theorem i_alpha_BV_lemma_1:

  (s, y) ->iA t ==> BV t <= BV s Un {y}

theorem ialpha1_in_rt_ialpha:

  (s, y) ->iA1 t ==> (s, y) ->>iA t

theorem ialpha1_FV_lemma:

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

theorem ialpha1_BV_lemma:

  (s, y) ->iA1 t ==> BV t <= BV s Un {y}

theorem cl_ialpha_FV_lemma:

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

theorem cl_ialpha_BV_lemma:

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

theorem cl_ialpha1_trans2:

  (t, ys) ->>iA1 u ==> ALL s y. (s, y) ->iA1 t --> (s, ys @ [y]) ->>iA1 u

theorem cl_ialpha1_trans2:

  [| (s, y) ->iA1 t; (t, ys) ->>iA1 u |] ==> (s, ys @ [y]) ->>iA1 u

theorem ialpha1_to_ialpha0:

  (e1, y) ->iA1 e2 ==> e1 ~= e2 --> (e1, y) ->iA0 e2

theorem rt_ialpha1_to_rt_ialpha0:

  (e, xs) ->>iA1 e' ==> e ->>A0 e'

theorem rt_alpha_to_rt_ialpha:

  e ->>A e' ==> EX xs. (e, xs) ->>ciA e'

theorem ialpha1_var_subst:

  (e, z) ->iA1 e'
  ==> y ~= z --> y ~: Capt x e --> (e[x:=Var y], z) ->iA1 e'[x:=Var y]