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