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