theory SingleLet
imports "../Nominal2" 
begin

atom_decl name

declare [[STEPS = 100]]

nominal_datatype single_let: trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"  bind x in t
| Let a::"assg" t::"trm"  bind "bn a" in t
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2 
and assg =
  As "name" x::"name" t::"trm" bind x in t
binder
  bn::"assg \<Rightarrow> atom list"
where
  "bn (As x y t) = [atom x]"

thm single_let.distinct
thm single_let.induct
thm single_let.inducts
thm single_let.exhaust[no_vars]
thm single_let.fv_defs
thm single_let.bn_defs
thm single_let.perm_simps
thm single_let.eq_iff
thm single_let.fv_bn_eqvt
thm single_let.size_eqvt
thm single_let.supports
thm single_let.fsupp
thm single_let.supp
thm single_let.fresh

primrec
  permute_bn_raw
where
  "permute_bn_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"

quotient_definition
  "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
is
  "permute_bn_raw"

lemma [quot_respect]:
  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"
  apply simp
  apply clarify
  apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
  apply (rule TrueI)+
  apply simp_all
  apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
  apply simp_all
  done

lemmas permute_bn = permute_bn_raw.simps[quot_lifted]

lemma uu:
  shows "alpha_bn as (permute_bn p as)"
apply(induct as rule: single_let.inducts(2))
apply(auto)[7]
apply(simp add: permute_bn)
apply(simp add: single_let.eq_iff)
done

lemma tt:
  shows "(p \<bullet> bn as) = bn (permute_bn p as)"
apply(induct as rule: single_let.inducts(2))
apply(auto)[7]
apply(simp add: permute_bn single_let.bn_defs)
apply(simp add: atom_eqvt)
done

lemma Abs_fresh_star':
  fixes x::"'a::fs"
  shows  "set bs = as \<Longrightarrow> as \<sharp>* Abs_lst bs x"
  unfolding fresh_star_def
  by(simp_all add: Abs_fresh_iff)

lemma strong_exhaust:
  fixes c::"'a::fs"
  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
  and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" 
  and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
  and "\<And>assg trm. \<lbrakk>set (bn assg) \<sharp>* c; y = Let assg trm\<rbrakk> \<Longrightarrow> P"
  and "\<And>name1 name2 trm1 trm2 trm3. \<lbrakk>{atom name1} \<sharp>* c; y = Foo name1 name2 trm1 trm2 trm3\<rbrakk> \<Longrightarrow> P"
  and "\<And>name1 name2 trm. \<lbrakk>{atom name1, atom name2} \<sharp>* c; y = Bar name1 name2 trm\<rbrakk> \<Longrightarrow> P" 
  and "\<And>name trm1 trm2. \<lbrakk>{atom name} \<sharp>* c; y = Baz name trm1 trm2\<rbrakk> \<Longrightarrow> P"
  shows "P"
  apply(rule_tac y="y" in single_let.exhaust(1))
  apply(rule assms(1))
  apply(assumption)
  apply(rule assms(2))
  apply(assumption)
  apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp ([[atom name]]lst.trm) \<sharp>* q")
  apply(erule exE)
  apply(erule conjE)
  apply(perm_simp)
  apply(rule assms(3))
  apply(assumption)
  apply(drule supp_perm_eq[symmetric])
  apply(simp add: single_let.eq_iff)
  apply(perm_simp)
  apply(rule refl)
  apply(rule at_set_avoiding2)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  apply(simp add: Abs_fresh_star')
  apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg))) \<sharp>* (c::'a::fs) \<and> supp ([bn assg]lst.trm) \<sharp>* q")
  apply(erule exE)
  apply(erule conjE)
  apply(perm_simp add: tt)
  apply(rule_tac assms(4))
  apply(assumption)
  apply(drule supp_perm_eq[symmetric])
  apply(simp add: single_let.eq_iff)
  apply(simp add: tt uu)
  apply(rule at_set_avoiding2)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  apply(simp add: Abs_fresh_star)
  apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* (c::'a::fs) \<and> 
    supp ([{atom name1}]set.(((name2, trm1), trm2), trm3)) \<sharp>* q")
  apply(erule exE)
  apply(erule conjE)
  apply(perm_simp add: tt)
  apply(rule_tac assms(5))
  apply(assumption)
  apply(drule supp_perm_eq[symmetric])
  apply(simp add: single_let.eq_iff)
  apply(perm_simp)
  apply(rule refl)
  apply(rule at_set_avoiding2)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  apply(simp add: Abs_fresh_star)
  apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* (c::'a::fs) \<and> 
    supp ([[atom name2, atom name1]]lst.((trm, name1), name2)) \<sharp>* q")
  apply(erule exE)
  apply(erule conjE)
  apply(perm_simp add: tt)
  apply(rule_tac assms(6))
  apply(assumption)
  apply(drule supp_perm_eq[symmetric])
  apply(simp add: single_let.eq_iff)
  apply(perm_simp)
  apply(rule refl)
  apply(rule at_set_avoiding2)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  apply(simp add: finite_supp)
  oops


end