Theory RawToReal

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

(*  Title:      RawToReal.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    17th January, 2001

- Definition of the real lambda-calculus in terms of alpha-equivalence classes,
  including a real beta relation

*)

RawToReal = RawConfluence + AbstractRewrites + AlphaClass +

typedef acls = "{y. EX (x::lterm). y = alphaclass x}"

consts  real_beta  :: "(acls * acls) set"
        beta_mod_alpha :: "(lterm * lterm) set"
        mem_ac :: "lterm => acls => bool"
  
syntax  "=>B"     :: [acls set,acls set] => bool (infixl 50)
        "=>>B"    :: [acls set,acls set] => bool (infixl 50)
        "-ABA->"  :: [lterm, lterm] => bool (infixl 50)
        "-ABA->>" :: [lterm, lterm] => bool (infixl 50)
        "in"      :: [lterm,acls] => bool (infixl 50)
  
translations
  "s =>B t"     == "(s,t) : real_beta"
  "s =>>B t"    == "(s,t) : real_beta^*"
  "s -ABA-> t"  == "(s,t) : beta_mod_alpha"
  "s -ABA->> t" == "(s,t) : beta_mod_alpha^*"
  "e in A"      == "mem_ac e A"            

(* The functions Rep_acls and Abs_acls are provided by Isabelle automatically
   from the typedef above.  They can be thought of as the functions which
   explicitly convert an acls (read: alpha equivalence class) to the
   appropriate lterm set, and vice versa. *)
  
defs mem_ac_def "mem_ac e A == (Rep_acls A = alphaclass e)"
  
inductive beta_mod_alpha
intrs
  cons "[|s =A= s'; s' ->B t'; t' =A= t|] ==> s -ABA-> t"

inductive real_beta
intrs
  lift "s ->B t ==> Abs_acls(alphaclass s) =>B Abs_acls(alphaclass t)"

(* This comment has been included to relate the pointwise definition of 
   real beta in the paper to the above, inductive definition.

   We write "[e]" for "Abs_acls(alphaclass e)".

   Definition (Real-Beta)

   [Inductive]: Let =>Bi be the least relation on alpha-equivalence classes 
   containing the (lift) rule:

         e1 ->B e2
      --------------(lift)
      [e1] =>Bi [e2]

   [Pointwise]: Let =>Bp be given pointwise on alpha-equivalence classes thus:
       [e1] =>Bp [e2] <=> e1 =A= ; ->B ; =A= e2

   Lemma: =>Bi = =>Bp

   Proof:
   Assume [e1] =>Bi [e2]. Then, by minimality of =>Bi, there are e1' \in 
   [e1] and e2' \in [e2], such that e1' ->B e2'. By the right-to-left 
   direction of the definition of =>Bp and ei =_a ei', we therefore have 
   [e1] =>Bp [e2].
   Assume [e1] =>Bp [e2]. Then, by definition of relation composition, ";", 
   there are ei' =_a ei, such that, e1' ->B e2'. Thus [e1]=[e1'] =>Bi 
   [e2']=[e2].

   <end of proof>
*)


  

  
end

theorem raw_to_real_beta:

  e -ABA->> e' | e =A= e'
  ==> Abs_acls (alphaclass e) =>>B Abs_acls (alphaclass e')

theorem alphaclass_self_inclusion_2:

  e in Abs_acls (alphaclass e)

theorem alphaclass_mem_elim:

  e in Abs_acls (alphaclass t) ==> e : alphaclass t

theorem real_to_raw_beta_aux:

  ac1 =>>B ac2 ==> ALL e e'. e in ac1 --> e' in ac2 --> e -ABA->> e' | e =A= e'

theorem RawToReal_Lemma8:

  (Abs_acls (alphaclass e) =>>B Abs_acls (alphaclass e')) =
  (e -ABA->> e' | e =A= e')

theorem RawToReal_Prop9:

  beta_mod_alpha^* Un (alpha Un rev_alpha)^* = (alpha Un beta)^*

theorem RawToReal_Lemma7:

  e ->>AB e' ==> Abs_acls (alphaclass e) =>>B Abs_acls (alphaclass e')

theorem RawToReal_Lemma10:

  Abs_acls (alphaclass e) =>>B Abs_acls (alphaclass e') ==> e ->>AB e'

theorem acls_type_lemma_1:

  y : acls ==> EX x. alphaclass x = y

theorem alphaclass_struct_coll:

  struct_coll (Abs_acls o alphaclass) UNIV UNIV ((alpha Un beta)^*) (real_beta^*)

theorem alphaclass_satisfies_preservation_premise:

  ALL x y x' y'.
     x' =>>B y' &
     (Abs_acls o alphaclass) x = x' & (Abs_acls o alphaclass) y = y' -->
     x ->>AB y

theorem real_confluence:

  confluent real_beta