Up to index of Isabelle/HOL/raw-confluence-lambda
theory RawToReal = RawConfluence + AbstractRewrites + AlphaClass(* 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