theory ExLet
imports "Parser"
begin

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

atom_decl name

ML {* val _ = recursive := false  *}
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[no_vars]
thm trm_lts.inducts[no_vars]
thm trm_lts.distinct
thm trm_lts.fv[simplified trm_lts.supp]

consts
  permute_bn :: "perm \<Rightarrow> lts \<Rightarrow> lts"

lemma test:
  "permute_bn pi (Lnil) = Lnil"
  "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)"
  sorry

lemma permute_bn_add:
  "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
  oops

lemma Lt_subst:
  "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
  sorry

lemma 
  fixes t::trm
  and   l::lts
  and   c::"'a::fs"
  assumes a1: "\<And>name c. P1 c (Vr name)"
  and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
  and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
  and     a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
  and     a5: "\<And>c. P2 c Lnil"
  and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
  shows "P1 c t" and "P2 c l"
proof -
  have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
       "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
    apply(induct rule: trm_lts.inducts)
    apply(simp)
    apply(rule a1)
    apply(simp)
    apply(rule a2)
    apply(simp)
    apply(simp)
    apply(simp)
    apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
    apply(erule exE)
    apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" 
               and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
    apply(rule supp_perm_eq)
    apply(simp)
    apply(simp)
    apply(rule a3)
    apply(simp add: atom_eqvt)
    apply(subst permute_plus[symmetric])
    apply(blast)
    apply(rule at_set_avoiding2_atom)
    apply(simp add: finite_supp)
    apply(simp add: finite_supp)
    apply(simp add: fresh_def)
    apply(simp add: trm_lts.fv[simplified trm_lts.supp])
    apply(simp)
    apply(subgoal_tac "\<exists>q. (bn (permute_bn q (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
    apply(erule exE)
    apply(erule conjE)
    apply(subst Lt_subst)
    apply assumption
    apply(rule a4)
    apply assumption
    apply (simp add: fresh_star_def fresh_def)
    apply(rotate_tac 1)
    apply(drule_tac x="q + p" in meta_spec)
    apply(simp)
    (*apply(rule at_set_avoiding2)
    apply(simp add: finite_supp)
    apply(simp add: supp_Abs)
    apply(rule finite_Diff)
    apply(simp add: finite_supp)
    apply(simp add: fresh_star_def fresh_def supp_Abs)*)
    defer
    apply(simp add: eqvts test)
    apply(rule a5)
    apply(simp add: test)
    apply(rule a6)
    apply simp
    apply simp
    oops
    


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))"
  by (simp add: trm_lts.eq_iff)

lemma lets_ok:
  "(Lt (Lcons x (Vr y) 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: alphas)
  apply (simp add: 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:
  "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
   (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
  apply (simp add: alphas trm_lts.eq_iff)
  apply (rule_tac x="0::perm" in exI)
  apply (simp add: fresh_star_def eqvts)
  apply blast
  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