theory Multi_Recs
imports "../Nominal2"
begin

(* 
  multiple recursive binders

  example 7 from Peter Sewell's bestiary 

*)

atom_decl name

nominal_datatype multi_recs: exp =
  Var name
| Unit
| Pair exp exp
| LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e
and lrb =
  Assign name exp
and lrbs =
  Single lrb
| More lrb lrbs
binder
  b :: "lrb \<Rightarrow> atom set" and
  bs :: "lrbs \<Rightarrow> atom set"
where
  "b (Assign x e) = {atom x}"
| "bs (Single a) = b a"
| "bs (More a as) = (b a) \<union> (bs as)"

thm multi_recs.distinct
thm multi_recs.induct
thm multi_recs.inducts
thm multi_recs.exhaust
thm multi_recs.fv_defs
thm multi_recs.bn_defs
thm multi_recs.perm_simps
thm multi_recs.eq_iff
thm multi_recs.fv_bn_eqvt
thm multi_recs.size_eqvt
thm multi_recs.supports
thm multi_recs.fsupp
thm multi_recs.supp

thm multi_recs.bn_defs
thm multi_recs.permute_bn
thm multi_recs.perm_bn_alpha
thm multi_recs.perm_bn_simps
thm multi_recs.bn_finite


lemma Abs_rename_set2:
  fixes x::"'a::fs"
  assumes a: "(p \<bullet> cs) \<sharp>* (cs, x)" 
  and     b: "finite cs"
  shows "\<exists>q. [cs]set. x = [p \<bullet> cs]set. (q \<bullet> x) \<and> q \<bullet> cs = p \<bullet> cs \<and> supp q \<subseteq> cs \<union> (p \<bullet> cs)"
proof -
  from a b have "p \<bullet> cs \<inter> cs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
  with set_renaming_perm 
  obtain q where *: "q \<bullet> cs = p \<bullet> cs" and **: "supp q \<subseteq> cs \<union> (p \<bullet> cs)" using b by metis
  have "[cs]set. x =  q \<bullet> ([cs]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> cs]set. (q \<bullet> x)" by simp
  also have "\<dots> = [p \<bullet> cs]set. (q \<bullet> x)" using * by simp
  finally have "[cs]set. x = [p \<bullet> cs]set. (q \<bullet> x)" .
  then show "\<exists>q. [cs]set. x = [p \<bullet> cs]set. (q \<bullet> x) \<and> q \<bullet> cs = p \<bullet> cs \<and> supp q \<subseteq> cs \<union> (p \<bullet> cs)"
    using * **
    by (blast)
qed

lemma at_set_avoiding5:
  assumes "finite xs"
  and     "finite (supp c)"
  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
using assms
apply(erule_tac c="c" in at_set_avoiding)
apply(auto)
done

lemma
  fixes c::"'a::fs"
  assumes a:  "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P"
  shows "y = LetRec lrbs exp \<Longrightarrow> P"
apply -
apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp)) \<and> supp p = bs lrbs \<union> (p \<bullet> (bs lrbs))")
apply(erule exE)
apply(simp add: fresh_star_Pair)
apply(erule conjE)+
apply(simp add: multi_recs.fv_bn_eqvt)
(*
using Abs_rename_set2
apply -
apply(drule_tac x="p" in meta_spec)
apply(drule_tac x="bs lrbs" in meta_spec)
apply(drule_tac x="lrbs" in meta_spec)
apply(drule meta_mp)
apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair)
apply(drule meta_mp)
apply(simp add: multi_recs.bn_finite)
apply(erule exE)
apply(simp add: multi_recs.fv_bn_eqvt)
*)
apply(rule a)
apply(assumption)
apply(clarify)
apply(simp (no_asm) only: multi_recs.eq_iff)
apply(rule trans)
apply(rule_tac p="p" in supp_perm_eq[symmetric])
apply(rule fresh_star_supp_conv)
apply(simp (no_asm_use) add: fresh_star_def)
apply(simp (no_asm_use) add: Abs_fresh_iff)[1]
apply(rule ballI)
apply(auto simp add: fresh_Pair)[1]
apply(simp (no_asm_use) only: permute_Abs)
apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt)
apply(simp)
apply(rule at_set_avoiding5)
apply(simp add: multi_recs.bn_finite)
apply(simp add: supp_Pair finite_supp)
apply(rule finite_sets_supp)
apply(simp add: multi_recs.bn_finite)
done



end