theory Let
imports "../Nominal2" 
begin

atom_decl name

nominal_datatype trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"  bind  x in t
| Let as::"assn" t::"trm"   bind "bn as" in t
and assn =
  ANil
| ACons "name" "trm" "assn"
binder
  bn
where
  "bn ANil = []"
| "bn (ACons x t as) = (atom x) # (bn as)"

thm trm_assn.fv_defs
thm trm_assn.eq_iff 
thm trm_assn.bn_defs
thm trm_assn.perm_simps
thm trm_assn.induct
thm trm_assn.inducts
thm trm_assn.distinct
thm trm_assn.supp
thm trm_assn.fresh
thm trm_assn.exhaust
thm trm_assn.strong_exhaust


lemma lets_bla:
  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Let (ACons x (Var y) ANil) (Var x)) \<noteq> (Let (ACons x (Var z) ANil) (Var x))"
  by (simp add: trm_assn.eq_iff)


lemma lets_ok:
  "(Let (ACons x (Var y) ANil) (Var x)) = (Let (ACons y (Var y) ANil) (Var y))"
  apply (simp add: trm_assn.eq_iff Abs_eq_iff )
  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
  apply (simp_all add: alphas atom_eqvt supp_at_base fresh_star_def trm_assn.bn_defs trm_assn.supp)
  done

lemma lets_ok3:
  "x \<noteq> y \<Longrightarrow>
   (Let (ACons x (App (Var y) (Var x)) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
   (Let (ACons y (App (Var x) (Var y)) (ACons x (Var x) ANil)) (App (Var x) (Var y)))"
  apply (simp add: trm_assn.eq_iff)
  done


lemma lets_not_ok1:
  "x \<noteq> y \<Longrightarrow>
   (Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
   (Let (ACons y (Var x) (ACons x (Var y) ANil)) (App (Var x) (Var y)))"
  apply (simp add: alphas trm_assn.eq_iff trm_assn.supp fresh_star_def atom_eqvt Abs_eq_iff trm_assn.bn_defs)
  done

lemma lets_nok:
  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
   (Let (ACons x (App (Var z) (Var z)) (ACons y (Var z) ANil)) (App (Var x) (Var y))) \<noteq>
   (Let (ACons y (Var z) (ACons x (App (Var z) (Var z)) ANil)) (App (Var x) (Var y)))"
  apply (simp add: alphas trm_assn.eq_iff fresh_star_def trm_assn.bn_defs Abs_eq_iff trm_assn.supp trm_assn.distinct)
  done

lemma
  fixes a b c :: name
  assumes x: "a \<noteq> c" and y: "b \<noteq> c"
  shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)"
  apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
  apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt)
  by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y)

lemma
  assumes "atom a \<noteq> atom c \<and> atom b \<noteq> atom c"
  shows "\<exists>p. ([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c) \<and> supp p \<subseteq> (supp (Var c) \<inter> {atom a}) \<union> (supp (Var c) \<inter> {atom b})"
  apply (simp add: alphas trm_assn.supp supp_at_base assms trm_assn.eq_iff atom_eqvt fresh_star_def)
  oops

end