theory SingleLetFoo
imports "../NewParser"
begin


declare [[STEPS = 5]]

atom_decl name

nominal_datatype trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"  bind_set x in t
| Let a::"assg" t::"trm"  bind_set "bn a" in t
| Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
| Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
and assg =
  As "name" "trm"
binder
  bn::"assg \<Rightarrow> atom set"
where
  "bn (As x t) = {atom x}"

thm trm_assg.distinct
thm trm_assg.eq_iff
thm trm_assg.supp
thm trm_assg.perm

thm permute_trm_raw_permute_assg_raw.simps
thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]

(* there is something wrong with the free variables *)

text {*
thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
*}

inductive 
  alpha_trm_raw and alpha_assg_raw and alpha_bn_raw
where
  "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
| "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk>
  \<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)"
| "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow>
   alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
| "\<lbrakk>\<exists>p. (bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (bn_raw assg_rawa, trm_rawa);
    alpha_bn_raw assg_raw assg_rawa\<rbrakk>
    \<Longrightarrow> alpha_trm_raw (Let_raw assg_raw trm_raw) (Let_raw assg_rawa trm_rawa)"
| "\<lbrakk>\<exists>p. (bn_raw assg_raw1 \<union> bn_raw ass_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p 
        (bn_raw assg_raw1a \<union> bn_raw ass_raw2a, trm_rawa);
   alpha_bn_raw assg_raw1 assg_raw1a; alpha_bn_raw assg_raw2 assg_raw2a\<rbrakk>
   \<Longrightarrow> alpha_trm_raw (Foo1_raw assg_raw1 assg_raw2 trm_raw) (Foo1_raw assg_raw1a assg_raw2a trm_rawa)"
| "\<lbrakk>\<exists>p. ({atom name} \<union> bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p 
        ({atom namea} \<union> bn_raw assg_rawa, trm_rawa);
   alpha_bn_raw assg_raw assg_rawa\<rbrakk>
   \<Longrightarrow> alpha_trm_raw (Foo2_raw name assg_raw trm_raw) (Foo2_raw namea assg_rawa trm_rawa)"

| "\<lbrakk>name = namea; alpha_trm_raw trm_raw trm_rawa\<rbrakk>
  \<Longrightarrow> alpha_assg_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
| "alpha_trm_raw trm_raw trm_rawa \<Longrightarrow> alpha_bn_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"

lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros

lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry

lemma
  assumes "distinct [x,y, z, u]"
  shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z))
                       (Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))"
using assms
apply(rule_tac all)
apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI)
apply(simp only: alphas)
apply(rule conjI)
apply(simp)
apply(simp add: supp_at_base fresh_star_def)
apply(rule conjI)
apply(simp add: supp_at_base fresh_star_def)
apply(rule conjI)
apply(simp)
apply(rule all)
apply(simp)
unfolding flip_def
apply(perm_simp add: test)
unfolding flip_def[symmetric]
apply(simp)
apply(subst flip_at_base_simps(3))
apply(auto)[2]
apply(simp)
apply(rule all)
apply(rule all)
apply(simp)
done

lemma
  assumes "distinct [x,y,z,u]"
  shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}"
using assms
apply(simp add: supp_at_base)


end