theory ExLetRec

imports "Parser"

begin

text {* example 3 or example 5 from Terms.thy *}

atom_decl name

ML {* val _ = recursive := true *}

nominal_datatype trm =

  Vr "name"

| Ap "trm" "trm"

| Lm x::"name" t::"trm"  bind x in t

| Lt a::"lts" t::"trm"   bind "bn a" in t

and lts =

  Lnil

| Lcons "name" "trm" "lts"

binder

  bn

where

  "bn Lnil = {}"

| "bn (Lcons x t l) = {atom x} \<union> (bn l)"

thm trm_lts.fv

thm trm_lts.eq_iff

thm trm_lts.bn

thm trm_lts.perm

thm trm_lts.induct

thm trm_lts.distinct

thm trm_lts.fv[simplified trm_lts.supp]

(* why is this not in HOL simpset? *)

lemma set_sub: "{a, b} - {b} = {a} - {b}"

by auto

lemma lets_bla:

  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"

  apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub)

  done

lemma lets_ok:

  "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"

  apply (simp add: trm_lts.eq_iff)

  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

  apply (simp_all add: alpha_gen2 fresh_star_def eqvts)

  done

lemma lets_ok3:

  "x \<noteq> y \<Longrightarrow>

   (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>

   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"

  apply (simp add: alphas trm_lts.eq_iff)

  done

lemma lets_not_ok1:

  "x \<noteq> y \<Longrightarrow>

   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>

   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"

  apply (simp add: alphas trm_lts.eq_iff)

  done

lemma lets_nok:

  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>

   (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>

   (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"

  apply (simp add: alphas trm_lts.eq_iff fresh_star_def)

  done

end