theory Term5
imports "Parser"
begin

atom_decl name

ML {* restricted_nominal := 2 *}

nominal_datatype trm5 =
  Vr5 "name"
| Ap5 "trm5" "trm5"
| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
and lts =
  Lnil
| Lcons "name" "trm5" "lts"
binder
  bv5
where
  "bv5 Lnil = {}"
| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"

lemma lets_ok:
  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
apply (simp add: trm5_lts_inject)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
apply (simp_all add: alpha_gen)
apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn)
done

lemma lets_nok:
  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))"
apply (simp only: trm5_lts_inject not_ex)
apply (rule allI)
apply (simp add: alpha_gen)
apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject)
done

end