theory Foo2

imports "../Nominal2" 

begin

(* 

  Contrived example that has more than one

  binding clause

*)

atom_decl name

nominal_datatype foo: trm =

  Var "name"

| App "trm" "trm"

| Lam x::"name" t::"trm"  bind x in t

| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2

| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2

and assg =

  As_Nil

| As "name" x::"name" t::"trm" "assg" 

binder

  bn::"assg \<Rightarrow> atom list"

where

 "bn (As x y t a) = [atom x] @ bn a"

| "bn (As_Nil) = []"

thm foo.perm_bn_simps

thm foo.distinct

thm foo.induct

thm foo.inducts

thm foo.exhaust

thm foo.fv_defs

thm foo.bn_defs

thm foo.perm_simps

thm foo.fv_bn_eqvt

thm foo.size_eqvt

thm foo.supports

thm foo.fsupp

thm foo.supp

thm foo.fresh

lemma uu1:

  shows "alpha_bn as (permute_bn p as)"

apply(induct as rule: foo.inducts(2))

apply(auto)[5]

apply(simp add: foo.perm_bn_simps)

apply(simp add: foo.eq_iff)

apply(simp add: foo.perm_bn_simps)

apply(simp add: foo.eq_iff)

done

lemma tt1:

  shows "(p \<bullet> bn as) = bn (permute_bn p as)"

apply(induct as rule: foo.inducts(2))

apply(auto)[5]

apply(simp add: foo.perm_bn_simps foo.bn_defs)

apply(simp add: foo.perm_bn_simps foo.bn_defs)

apply(simp add: atom_eqvt)

done

lemma Let1_rename:

  assumes "supp ([bn assn1]lst. trm1) \<sharp>* p" "supp ([bn assn2]lst. trm2) \<sharp>* p"

  shows "Let1 assn1 trm1 assn2 trm2 = Let1 (permute_bn p assn1) (p \<bullet> trm1) (permute_bn p assn2) (p \<bullet> trm2)"

using assms

apply -

apply(drule supp_perm_eq[symmetric])

apply(drule supp_perm_eq[symmetric])

apply(simp only: permute_Abs)

apply(simp only: tt1)

apply(simp only: foo.eq_iff)

apply(simp add: uu1)

done

lemma strong_exhaust1:

  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>assn1 trm1 assn2 trm2. 

    \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P"

  and     "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"

  shows "P"

apply(rule_tac y="y" in foo.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 (Lam name trm) \<sharp>* q")

apply(erule exE)

apply(erule conjE)

apply(rule assms(3))

apply(perm_simp)

apply(assumption)

apply(simp)

apply(drule supp_perm_eq[symmetric])

apply(perm_simp)

apply(simp)

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: foo.fresh fresh_star_def)

apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg1))) \<sharp>* c \<and> supp ([bn assg1]lst. trm1) \<sharp>* q")

apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg2))) \<sharp>* c \<and> supp ([bn assg2]lst. trm2) \<sharp>* q")

apply(erule exE)+

apply(erule conjE)+

apply(rule assms(4))

apply(simp add: set_eqvt union_eqvt)

apply(simp add: tt1)

apply(simp add: fresh_star_union)

apply(rule conjI)

apply(assumption)

apply(rotate_tac 3)

apply(assumption)

apply(simp add: foo.eq_iff)

apply(drule supp_perm_eq[symmetric])+

apply(simp add: tt1 uu1)

apply(auto)[1]

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(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)

thm foo.eq_iff

apply(subgoal_tac 

  "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> supp ([[atom name1]]lst. trm1) \<sharp>* q")

apply(subgoal_tac 

  "\<exists>q. (q \<bullet> {atom name2}) \<sharp>* c \<and> supp ([[atom name2]]lst. trm2) \<sharp>* q")

apply(erule exE)+

apply(erule conjE)+

apply(rule assms(5))

apply(perm_simp)

apply(simp (no_asm) add: fresh_star_insert)

apply(rule conjI)

apply(simp add: fresh_star_def)

apply(rotate_tac 3)

apply(simp add: fresh_star_def)

apply(simp)

apply(simp add: foo.eq_iff)

apply(drule supp_perm_eq[symmetric])+

apply(simp add: atom_eqvt)

apply(rule conjI)

oops

end