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