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

text {*

  tests by cu

*}

lemma yy:

  assumes a: "p \<bullet> bs \<inter> bs = {}" 

  and     b: "finite bs"

  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"

using b a

apply(induct)

apply(simp add: permute_set_eq)

apply(rule_tac x="0" in exI)

apply(simp add: supp_perm)

apply(perm_simp)

apply(drule meta_mp)

apply(auto simp add: fresh_star_def fresh_finite_insert)[1]

apply(erule exE)

apply(simp)

apply(case_tac "q \<bullet> x = p \<bullet> x")

apply(rule_tac x="q" in exI)

apply(auto)[1]

apply(rule_tac x="((q \<bullet> x) \<rightleftharpoons> (p \<bullet> x)) + q" in exI)

apply(subgoal_tac "p \<bullet> x \<notin> p \<bullet> F")

apply(subgoal_tac "q \<bullet> x \<notin> p \<bullet> F")

apply(simp add: swap_set_not_in)

apply(rule subset_trans)

apply(rule supp_plus_perm)

apply(simp)

apply(rule conjI)

apply(simp add: supp_swap)

apply(simp add: supp_perm)

apply(auto)[1]

apply(auto)[1]

apply(erule conjE)+

apply(drule sym)

apply(simp add: mem_permute_iff)

apply(simp add: mem_permute_iff)

done

lemma Abs_rename_set:

  fixes x::"'a::fs"

  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 

  and     b: "finite bs"

  shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"

proof -

  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   

  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis

  have "[bs]set. x =  q \<bullet> ([bs]set. x)"

    apply(rule perm_supp_eq[symmetric])

    using a **

    unfolding fresh_star_Pair

    unfolding Abs_fresh_star_iff

    unfolding fresh_star_def

    by auto

  also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp

  also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp

  finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" .

  then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast

qed

lemma Abs_rename_res:

  fixes x::"'a::fs"

  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 

  and     b: "finite bs"

  shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"

proof -

  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 

  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis

  have "[bs]res. x =  q \<bullet> ([bs]res. x)"

    apply(rule perm_supp_eq[symmetric])

    using a **

    unfolding fresh_star_Pair

    unfolding Abs_fresh_star_iff

    unfolding fresh_star_def

    by auto

  also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp

  also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp

  finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" .

  then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast

qed

lemma zz0:

  assumes "p \<bullet> bs = q \<bullet> bs"

  and a: "a \<in> set bs"

  shows "p \<bullet> a = q \<bullet> a"

using assms

by (induct bs) (auto)

lemma zz:

  fixes bs::"atom list"

  assumes "(p \<bullet> (set bs)) \<inter> (set bs) = {}"

  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"

using assms

apply(induct bs)

apply(simp add: permute_set_eq)

apply(rule_tac x="0" in exI)

apply(simp add: supp_perm)

apply(drule meta_mp)

apply(perm_simp)

apply(auto)[1]

apply(erule exE)

apply(simp)

apply(case_tac "a \<in> set bs")

apply(rule_tac x="q" in exI)

apply(perm_simp)

apply(auto dest: zz0)[1]

apply(subgoal_tac "q \<bullet> a \<sharp> p \<bullet> bs")

apply(subgoal_tac "p \<bullet> a \<sharp> p \<bullet> bs")

apply(rule_tac x="((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" in exI)

apply(simp add: swap_fresh_fresh)

apply(rule subset_trans)

apply(rule supp_plus_perm)

apply(simp)

apply(rule conjI)

apply(simp add: supp_swap)

apply(simp add: supp_perm)

apply(perm_simp)

apply(auto simp add: fresh_def supp_of_atom_list)[1]

apply(perm_simp)

apply(auto)[1]

apply(simp add: fresh_permute_iff)

apply(simp add: fresh_def supp_of_atom_list)

apply(erule conjE)+

apply(drule sym)

apply(drule sym)

apply(simp)

apply(simp add: fresh_permute_iff)

apply(auto simp add: fresh_def supp_of_atom_list)[1]

done

lemma Abs_rename_list:

  fixes x::"'a::fs"

  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 

  shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"

proof -

  from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 

    by (simp add: fresh_star_Pair fresh_star_set)

  with zz obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 

  have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"

    apply(rule perm_supp_eq[symmetric])

    using a **

    unfolding fresh_star_Pair

    unfolding Abs_fresh_star_iff

    unfolding fresh_star_def

    by auto

  also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp

  also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp

  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .

  then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast

qed

lemma test6:

  fixes c::"'a::fs"

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

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

  and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"

  and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 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(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")

apply(erule exE)

apply(insert Abs_rename_list)[1]

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="[atom name]" in meta_spec)

apply(drule_tac x="trm" in meta_spec)

apply(simp only: fresh_star_Pair set.simps)

apply(drule meta_mp)

apply(simp)

apply(erule exE)

apply(perm_simp)

apply(erule conjE)+

apply(assumption)

apply(rule at_set_avoiding1)

apply(simp)

apply(simp add: finite_supp)

apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")

apply(erule exE)

apply(rule assms(4))

apply(simp only:)

apply(simp only: foo.eq_iff)

apply(insert Abs_rename_list)[1]

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="bn assg1" in meta_spec)

apply(drule_tac x="trm1" in meta_spec)

apply(insert Abs_rename_list)[1]

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="bn assg2" in meta_spec)

apply(drule_tac x="trm2" in meta_spec)

apply(drule meta_mp)

apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)

apply(drule meta_mp)

apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)

apply(erule exE)+

apply(rule exI)+

apply(perm_simp add: tt1)

apply(rule conjI)

apply(simp add: fresh_star_Pair fresh_star_Un)

apply(erule conjE)+

apply(rule conjI)

apply(assumption)

apply(rotate_tac 4)

apply(assumption)

apply(rule conjI)

apply(assumption)

apply(rule conjI)

apply(rule uu1)

apply(rule conjI)

apply(assumption)

apply(rule uu1)

apply(rule at_set_avoiding1)

apply(simp)

apply(simp add: finite_supp)

apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")

apply(erule exE)

apply(rule assms(5))

apply(simp only:)

apply(simp only: foo.eq_iff)

apply(insert Abs_rename_list)[1]

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec)

apply(drule_tac x="trm1" in meta_spec)

apply(insert Abs_rename_list)[1]

apply(drule_tac x="p" in meta_spec)

apply(drule_tac x="[atom name2]" in meta_spec)

apply(drule_tac x="trm2" in meta_spec)

apply(drule meta_mp)

apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp)

apply(auto)[1]

apply(perm_simp)

apply(auto simp add: fresh_star_def)[1]

apply(perm_simp)

apply(auto simp add: fresh_star_def)[1]

apply(perm_simp)

apply(auto simp add: fresh_star_def)[1]

apply(drule meta_mp)

apply(perm_simp)

apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]

apply(erule exE)+

apply(rule exI)+

apply(perm_simp add: tt1)

apply(rule conjI)

prefer 2

apply(rule conjI)

apply(assumption)

apply(assumption)

apply(simp add: fresh_star_Pair)

apply(simp add: fresh_star_def)

apply(rule at_set_avoiding1)

apply(simp)

apply(simp add: finite_supp)

done

lemma test5:

  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>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 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 test6)

apply(erule exE)+

apply(rule assms(1))

apply(assumption)

apply(erule exE)+

apply(rule assms(2))

apply(assumption)

apply(erule exE)+

apply(rule assms(3))

apply(auto)[2]

apply(erule exE)+

apply(rule assms(4))

apply(auto)[2]

apply(erule exE)+

apply(rule assms(5))

apply(auto)[2]

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>a1 t1 a2 t2 c. 

    \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk> 

    \<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)"

  and a4: "\<And>n1 n2 t1 t2 c. 

    \<lbrakk>{atom n1, atom n2} \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)"

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

  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) (size o snd))")

  apply(simp_all add: foo.size)

  done

end