theory Foo1

imports "../Nominal2" 

begin

text {* 

  Contrived example that has more than one

  binding function

*}

atom_decl name

nominal_datatype foo: trm =

  Var "name"

| App "trm" "trm"

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

| Let1 a::"assg" t::"trm"  bind "bn1 a" in t

| Let2 a::"assg" t::"trm"  bind "bn2 a" in t

| Let3 a::"assg" t::"trm"  bind "bn3 a" in t

| Let4 a::"assg'" t::"trm"  bind (set) "bn4 a" in t

and assg =

  As "name" "name" "trm"

and assg' =

  BNil

| BAs "name" "assg'"

binder

  bn1::"assg \<Rightarrow> atom list" and

  bn2::"assg \<Rightarrow> atom list" and

  bn3::"assg \<Rightarrow> atom list" and

  bn4::"assg' \<Rightarrow> atom set"

where

  "bn1 (As x y t) = [atom x]"

| "bn2 (As x y t) = [atom y]"

| "bn3 (As x y t) = [atom x, atom y]"

| "bn4 (BNil) = {}"

| "bn4 (BAs a as) = {atom a} \<union> bn4 as"

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

thm foo.fv_bn_eqvt

thm foo.size_eqvt

thm foo.supports

thm foo.fsupp

thm foo.supp

thm foo.fresh

thm foo.bn_finite

lemma uu1:

  shows "alpha_bn1 as (permute_bn1 p as)"

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

apply(auto)[7]

apply(simp add: foo.perm_bn_simps)

apply(simp add: foo.eq_iff)

apply(auto)

done

lemma uu2:

  shows "alpha_bn2 as (permute_bn2 p as)"

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

apply(auto)[7]

apply(simp add: foo.perm_bn_simps)

apply(simp add: foo.eq_iff)

apply(auto)

done

lemma uu3:

  shows "alpha_bn3 as (permute_bn3 p as)"

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

apply(auto)[7]

apply(simp add: foo.perm_bn_simps)

apply(simp add: foo.eq_iff)

apply(auto)

done

lemma uu4:

  shows "alpha_bn4 as (permute_bn4 p as)"

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

apply(auto)[8]

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> bn1 as) = bn1 (permute_bn1 p as)"

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

apply(auto)[7]

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

apply(simp add: atom_eqvt)

apply(auto)

done

lemma tt2:

  shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)"

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

apply(auto)[7]

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

apply(simp add: atom_eqvt)

apply(auto)

done

lemma tt3:

  shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)"

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

apply(auto)[7]

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

apply(simp add: atom_eqvt)

apply(auto)

done

lemma tt4:

  shows "(p \<bullet> bn4 as) = bn4 (permute_bn4 p as)"

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

apply(auto)[8]

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

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

apply(simp add: atom_eqvt insert_eqvt)

done

lemma Let1_rename:

  assumes "supp ([bn1 assn]lst. trm) \<sharp>* p"

  shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \<bullet> trm)"

using assms

apply -

apply(drule supp_perm_eq[symmetric])

apply(simp only: permute_Abs)

apply(simp only: tt1)

apply(simp only: foo.eq_iff)

apply(rule conjI)

apply(rule refl)

apply(rule uu1)

done

lemma Let1_rename_a:

  fixes c::"'a::fs"

  assumes "y =  Let1 assn trm"

  shows "\<exists>p. (p \<bullet> (set (bn1 assn))) \<sharp>* c \<and> y = Let1 (permute_bn1 p assn) (p \<bullet> trm)"

using assms

apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric])

apply(simp del: permute_Abs)

sorry

lemma strong_exhaust1:

  fixes c::"'a::fs"

  assumes "\<exists>name. y = Var name \<Longrightarrow> P" 

  and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"

  shows "P"

apply(rule_tac y="y" in foo.exhaust(1))

apply(rule assms(1))

apply(rule exI)

apply(assumption)

apply(rule assms(2))

apply(rule exI)+

apply(assumption)

apply(rule assms(3))

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

apply(erule exE)

apply(erule conjE)

apply(rule assms(4))

apply(simp only: set_eqvt tt1)

apply(assumption)

(*

apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")

apply(erule exE)

apply(erule conjE)

*)

thm assms(5)

apply(rule assms(5))

prefer 2

apply(clarify)

unfolding foo.eq_iff

apply

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>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"

  and     "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"

  and     "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"

  and     "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<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(drule Let1_rename_a)

apply(erule exE)

apply(erule conjE)

apply(rule assms(4))

apply(simp only: set_eqvt tt1)

apply(assumption)

(*

apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")

apply(erule exE)

apply(erule conjE)

*)

thm assms(5)

apply(rule assms(5))

prefer 2

apply(clarify)

unfolding foo.eq_iff

apply(rule conjI)

prefer 2

apply(rule uu2)

apply(simp only: tt2[symmetric])

prefer 2

apply(simp only: tt2[symmetric])

apply(simp_all only:)[2]

apply(simp add: set_eqvt)

apply(simp add: tt2)

apply(simp add: foo.eq_iff)

apply(drule supp_perm_eq[symmetric])

apply(simp)

apply(simp add: tt2 uu2)

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 (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q")

apply(erule exE)

apply(erule conjE)

apply(rule assms(6))

apply(simp add: set_eqvt)

apply(simp add: tt3)

apply(simp add: foo.eq_iff)

apply(drule supp_perm_eq[symmetric])

apply(simp)

apply(simp add: tt3 uu3)

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> (bn4 assg')) \<sharp>* c \<and> supp ([bn4 assg']set.trm) \<sharp>* q")

apply(erule exE)

apply(erule conjE)

apply(rule assms(7))

apply(simp add: tt4)

apply(simp add: foo.eq_iff)

apply(drule supp_perm_eq[symmetric])

apply(simp)

apply(simp add: tt4 uu4)

apply(rule at_set_avoiding2)

apply(simp add: foo.bn_finite)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: Abs_fresh_star)

done

thm strong_exhaust1 foo.exhaust(1)

lemma strong_exhaust2:

  assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 

  shows "P"

apply(rule_tac y="as" in foo.exhaust(2))

apply(rule assms(1))

apply(assumption)

done

lemma strong_exhaust3:

  assumes "as' = BNil \<Longrightarrow> P"

  and "\<And>a as. as' = BAs a as \<Longrightarrow> P" 

  shows "P"

apply(rule_tac y="as'" in foo.exhaust(3))

apply(rule assms(1))

apply(assumption)

apply(rule assms(2))

apply(assumption)

done

lemma 

  fixes t::trm

  and   as::assg

  and   as'::assg'

  and   c::"'a::fs"

  assumes a1: "\<And>x c. P1 c (Var x)"

  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"

  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"

  and     a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)"

  and     a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)"

  and     a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)"

  and     a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" 

  and     a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"

  and     a9: "\<And>c. P3 c (BNil)"

  and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"

  shows "P1 c t" "P2 c as" "P3 c as'"

using assms

apply(induction_schema)

apply(rule_tac y="t" and c="c" in strong_exhaust1)

apply(simp_all)[7]

apply(rule_tac as="as" in strong_exhaust2)

apply(simp)

apply(rule_tac as'="as'" in strong_exhaust3)

apply(simp_all)[2]

apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))")

apply(simp_all add: foo.size)

done

end