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 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))")
apply(erule exE)
apply(simp add: fresh_star_Pair)
apply(erule conjE)+
apply(simp add: multi_recs.fv_bn_eqvt)
using Abs_rename_set'
apply -
apply(drule_tac x="p" in meta_spec)
apply(drule_tac x="bs lrbs" in meta_spec)
apply(drule_tac x="(lrbs, exp)" 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(erule conjE)
apply(rotate_tac 6)
apply(drule sym)
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 at_set_avoiding1)
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