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)

lemma strong_exhaust1_pre:

  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

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

  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

lemma strong_induct:

  fixes c :: "'a :: fs"

  and assg :: assg and trm :: trm

  assumes a0: "\<And>name c. P1 c (Var name)"

  and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"

  and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"

  and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; \<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)"

  and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>{atom name1, atom name2} \<sharp>* c; \<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)"

  and a5: "\<And>c. P2 c As_Nil"

  and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"

  shows "P1 c trm" "P2 c assg"

  using assms

  apply(induction_schema)

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

apply(simp_all)[5]

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

apply(simp_all)[2]

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

apply(simp_all add: foo.size)

done

text {*

  tests by cu

*}

lemma test3:

  fixes c::"'a::fs"

  assumes a: "y = Let2 x1 x2 trm1 trm2"

  and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P"

  shows "P"

using b[simplified a]

apply -

apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)")

apply(erule exE)

apply(perm_simp)

apply(simp only: foo.eq_iff)

apply(simp)

apply(rule conjI)

apply(rule conjI)

prefer 2

apply(simp add: fresh_star_def)

apply(simp)

apply(case_tac "x1=x2")

apply(simp)

apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])

apply(simp)

apply(simp add: fresh_star_def)

apply(simp add: fresh_def supp_Pair)

apply(simp)

apply(rule exI)

apply(rule refl)

apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])

apply(simp)

apply(simp add: fresh_star_def)

apply(simp add: fresh_def supp_Pair)

apply(simp)

apply(simp add: flip_def[symmetric] atom_eqvt)

apply(subgoal_tac "q \<bullet> x2 \<noteq> x1")

apply(simp)

apply(subst Abs_swap2[where a="atom x1" and b="atom (q \<bullet> x1)"])

apply(simp)

apply(subgoal_tac " atom (q \<bullet> x1) \<notin> supp ((x2 \<leftrightarrow> q \<bullet> x2) \<bullet> trm1)")

apply(simp add: fresh_star_def)

apply(simp add: fresh_star_def)

apply(simp add: fresh_def supp_Pair)

apply(erule conjE)+

apply(rule_tac p="(x2 \<leftrightarrow> q \<bullet> x2)" in permute_boolE)

apply(simp add: mem_eqvt Not_eqvt atom_eqvt supp_eqvt)

apply(subgoal_tac "q \<bullet> x2 \<noteq> q \<bullet> x1")

apply(subgoal_tac "x2 \<noteq> q \<bullet> x1")

apply(simp)

apply(simp add: supp_at_base)

apply(simp)

apply(simp)

apply(rule exI)

apply(rule refl)

apply(simp add: fresh_star_def)

apply(simp add: fresh_def supp_Pair)

apply(simp add: supp_at_base)

apply(rule at_set_avoiding3[where x="()", simplified])

apply(simp)

apply(simp add: finite_supp)

apply(simp add: finite_supp)

apply(simp add: fresh_star_def fresh_Unit)

done

lemma test4:

  fixes c::"'a::fs"

  assumes a: "y = Let2 x1 x2 trm1 trm2"

  and b: "\<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 test3)

apply(rule a)

using b

apply(auto)

done

end