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
*}


thm at_set_avoiding2 supp_perm_eq at_set_avoiding

lemma abs_rename_set:
  fixes x::"'a::fs"
  assumes "b' \<sharp> x" "sort_of b = sort_of b'"
  shows "\<exists>y. [{b}]set. x = [{b'}]set. y"
apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI)
apply(subst Abs_swap1[where a="b" and b="b'"])
apply(simp)
using assms
apply(simp add: fresh_def)
apply(perm_simp)
using assms
apply(simp)
done

lemma abs_rename_set1:
  fixes x::"'a::fs"
  assumes "(p \<bullet> b) \<sharp> x" 
  shows "\<exists>y. [{b}]set. x = [{p \<bullet> b}]set. y"
apply(rule_tac x="(b \<rightleftharpoons> (p \<bullet> b)) \<bullet> x" in exI)
apply(subst Abs_swap1[where a="b" and b="p \<bullet> b"])
apply(simp)
using assms
apply(simp add: fresh_def)
apply(perm_simp)
apply(simp)
done

lemma yy:
  assumes "finite bs"
  and "bs \<inter> p \<bullet> bs = {}"
  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
using assms
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)[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)
defer
apply(auto)[1]
apply(erule conjE)+
apply(drule sym)
apply(auto)[1]
apply(simp add: mem_permute_iff)
apply(simp add: mem_permute_iff)
apply(auto)[1]
apply(simp add: supp_perm)
apply(auto)[1]
done

lemma zz:
  fixes bs::"atom list"
  assumes "set bs \<inter> (set (p \<bullet> bs)) = {}"
  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (set (p \<bullet> bs))"
sorry

lemma abs_rename_set2:
  fixes x::"'a::fs"
  assumes "(p \<bullet> bs) \<sharp>* x" "bs \<inter> p \<bullet> bs ={}" "finite bs"
  shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
using yy assms
apply -
apply(drule_tac x="bs" in meta_spec)
apply(drule_tac x="p" in meta_spec)
apply(auto)
apply(rule_tac x="q \<bullet> x" in exI)
apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x")
apply(simp add: permute_Abs)
apply(rule supp_perm_eq)
apply(rule fresh_star_supp_conv)
apply(simp add: fresh_star_def)
apply(simp add: Abs_fresh_iff)
apply(auto)
done

lemma abs_rename_list:
  fixes x::"'a::fs"
  assumes "b' \<sharp> x" "sort_of b = sort_of b'"
  shows "\<exists>y. [[b]]lst. x = [[b']]lst. y"
apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI)
apply(subst Abs_swap2[where a="b" and b="b'"])
apply(simp)
using assms
apply(simp add: fresh_def)
apply(perm_simp)
using assms
apply(simp)
done

lemma abs_rename_list2:
  fixes x::"'a::fs"
  assumes "(set (p \<bullet> bs)) \<sharp>* x" "(set bs) \<inter> (set (p \<bullet> bs)) ={}" 
  shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
using zz assms
apply -
apply(drule_tac x="bs" in meta_spec)
apply(drule_tac x="p" in meta_spec)
apply(auto simp add: set_eqvt)
apply(rule_tac x="q \<bullet> x" in exI)
apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x")
apply(simp)
apply(rule supp_perm_eq)
apply(rule fresh_star_supp_conv)
apply(simp add: fresh_star_def)
apply(simp add: Abs_fresh_iff)
apply(auto)
done


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(drule_tac x="q \<bullet> x1" in spec)
apply(drule_tac x="q \<bullet> x2" in spec)
apply(simp)
apply(erule mp)
apply(rule conjI)
apply(simp add: fresh_star_prod)
apply(rule conjI)
apply(simp add: atom_eqvt[symmetric])
apply(subst (2) permute_list.simps(1)[where p="q", symmetric])
apply(subst permute_list.simps(2)[symmetric])
apply(subst permute_list.simps(2)[symmetric])
apply(rule abs_rename_list2)
apply(simp add: atom_eqvt fresh_star_prod)
apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
apply(simp add: atom_eqvt[symmetric])
apply(subst (2) permute_list.simps(1)[where p="q", symmetric])
apply(subst permute_list.simps(2)[symmetric])
apply(rule abs_rename_list2)
apply(simp add: atom_eqvt fresh_star_prod)
apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
apply(simp add: atom_eqvt[symmetric])
apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
sorry

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

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>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_tac y="y" in foo.exhaust(1))
apply (erule assms)
apply (erule assms)
prefer 3
apply(erule test4[where c="c"])
apply (rule assms(5)) 
apply assumption
apply(simp)
oops


end