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.bn_defs
thm foo.permute_bn
thm foo.perm_bn_alpha
thm foo.perm_bn_simps
thm foo.bn_finite

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

text {*
  tests by cu
*}

lemma set_renaming_perm:
  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
proof (induct)
  case empty
  have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
    by (simp add: permute_set_eq supp_perm)
  then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
next
  case (insert a bs)
  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" 
    by (perm_simp) (auto)
  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast 
  { assume 1: "q \<bullet> a = p \<bullet> a"
    have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)
    moreover 
    have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
      using ** by (auto simp add: insert_eqvt)
    ultimately 
    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
  }
  moreover
  { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
    def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
    { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)
      moreover 
      have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)
      ultimately 
      have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def 
        by (simp add: insert_eqvt  swap_set_not_in) 
    }
    moreover 
    { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
	using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`
	by (auto simp add: supp_perm insert_eqvt)
      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
      moreover
      have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
	using ** by (auto simp add: insert_eqvt)
      ultimately 
      have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
        unfolding q'_def using supp_plus_perm by blast
    }
    ultimately 
    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
  }
  ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
    by blast
qed


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 set_renaming_perm 
  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 set_renaming_perm 
  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 list_renaming_perm:
  fixes bs::"atom list"
  assumes a: "(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 a
proof (induct bs)
  case Nil
  have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
    by (simp add: permute_set_eq supp_perm)
  then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
next
  case (Cons a bs)
  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" 
    by (perm_simp) (auto)
  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast 
  { assume 1: "a \<in> set bs"
    have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
    then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp 
    moreover 
    have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
    ultimately 
    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
  }
  moreover
  { assume 2: "a \<notin> set bs"
    def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
    { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] 
	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
      moreover 
      have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` 
	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
      ultimately 
      have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def 
        by (simp add: swap_fresh_fresh) 
    }
    moreover 
    { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
	using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`
	by (auto simp add: supp_perm insert_eqvt)
      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
      moreover
      have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
	using ** by (auto simp add: insert_eqvt)
      ultimately 
      have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
        unfolding q'_def using supp_plus_perm by blast
    }
    ultimately 
    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
  }
  ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
    by blast
qed


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 list_renaming_perm 
  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

(*
thm at_set_avoiding1[THEN exE]


lemma Let1_rename:
  fixes c::"'a::fs"
  shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and>  Lam name trm = Lam name' trm'"
apply(simp only: foo.eq_iff)
apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE])
apply(simp)
apply(simp add: finite_supp)
apply(perm_simp)
apply(rule Abs_rename_list[THEN exE])
apply(simp only: set_eqvt)
apply
sorry 
*)

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     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<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)
(* lam case *)
(*
apply(rule Let1_rename)
apply(rule assms(3))
apply(assumption)
apply(simp)
*)

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(rule assms(3))
apply(perm_simp)
apply(erule conjE)+
apply(assumption)
apply(clarify)
apply(simp (no_asm) add: foo.eq_iff)
apply(perm_simp)
apply(assumption)
apply(rule at_set_avoiding1)
apply(simp)
apply(simp add: finite_supp)
(* let1 case *)
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: 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: foo.permute_bn)
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 foo.perm_bn_alpha)
apply(rule conjI)
apply(assumption)
apply(rule foo.perm_bn_alpha)
apply(rule at_set_avoiding1)
apply(simp)
apply(simp add: finite_supp)
(* let2 case *)
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: foo.permute_bn)
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(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