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.eq_iff(5)

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 Let2_rename:

  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(supp ([[atom y]]lst. t2)) \<sharp>* p"

  shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"

  using assms

  apply -

  apply(drule supp_perm_eq[symmetric])

  apply(drule supp_perm_eq[symmetric])

  apply(simp only: foo.eq_iff)

  apply(simp only: eqvts)

  apply simp

  done

lemma Let2_rename2:

  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(atom y) \<sharp> p"

  shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) y (p \<bullet> t1) t2"

  using assms

  apply -

  apply(drule supp_perm_eq[symmetric])

  apply(simp only: foo.eq_iff)

  apply(simp only: eqvts)

  apply simp

  by (metis assms(2) atom_eqvt fresh_perm)

lemma Let2_rename3:

  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p"

  and "(supp ([[atom y]]lst. t2)) \<sharp>* p"

  and "(atom x) \<sharp> p"

  shows "Let2 x y t1 t2 = Let2 x (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"

  using assms

  apply -

  apply(drule supp_perm_eq[symmetric])

  apply(drule supp_perm_eq[symmetric])

  apply(simp only: foo.eq_iff)

  apply(simp only: eqvts)

  apply simp

  by (metis assms(2) atom_eqvt fresh_perm)

  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} \<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)

apply(case_tac "name1 = name2")

apply(subgoal_tac 

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

apply(erule exE)+

apply(erule conjE)+

apply(perm_simp)

apply(rule assms(5))

apply (simp add: fresh_star_def eqvts)

apply (simp only: supp_Pair)

apply (simp only: fresh_star_Un_elim)

apply (subst Let2_rename)

apply assumption

apply assumption

apply (rule refl)

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply clarify

apply (simp add: fresh_star_def)

apply (simp add: fresh_def supp_Pair supp_Abs)

apply(subgoal_tac

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

prefer 2

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply (simp add: fresh_star_def)

apply (simp add: fresh_def supp_Pair supp_Abs supp_atom)

apply(erule exE)+

apply(erule conjE)+

apply(perm_simp)

apply(rule assms(5))

apply assumption

apply clarify

apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2)

apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs)

apply (simp add: fresh_star_def supp_atom)

done

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

  apply (erule assms)

  apply (erule assms) apply assumption

  apply (erule assms) apply assumption

apply(case_tac "x1 = x2")

apply(subgoal_tac 

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

apply(erule exE)+

apply(erule conjE)+

apply(perm_simp)

apply(rule assms(5))

apply assumption

apply simp

apply (rule Let2_rename)

apply (simp only: supp_Pair)

apply (simp only: fresh_star_Un_elim)

apply (simp only: supp_Pair)

apply (simp only: fresh_star_Un_elim)

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply clarify

apply (simp add: fresh_star_def)

apply (simp add: fresh_def supp_Pair supp_Abs)

  apply(subgoal_tac 

    "\<exists>q. (q \<bullet> {atom x2}) \<sharp>* c \<and> supp (([[atom x2]]lst. trm2), ([[atom x1, atom x2]]lst. trm1), (atom x1)) \<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 2)

apply(simp add: fresh_star_def)

apply(simp)

apply (rule Let2_rename3)

apply (simp add: supp_Pair fresh_star_union)

apply (simp add: supp_Pair fresh_star_union)

apply (simp add: supp_Pair fresh_star_union)

apply clarify

apply (simp add: fresh_star_def supp_atom)

apply(rule at_set_avoiding2)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: fresh_star_def)

apply (simp add: fresh_def supp_Pair supp_Abs supp_atom)

done

end