46 thm multi_recs.bn_defs

    47 thm multi_recs.permute_bn

    48 thm multi_recs.perm_bn_alpha

    49 thm multi_recs.perm_bn_simps

    50 thm multi_recs.bn_finite

    51 

    52 

    53 lemma Abs_rename_set2:

    54   fixes x::"'a::fs"

    55   assumes a: "(p \<bullet> cs) \<sharp>* (cs, x)" 

    56   and     b: "finite cs"

    57   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)"

    58 proof -

    59   from a b have "p \<bullet> cs \<inter> cs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   

    60   with set_renaming_perm 

    61   obtain q where *: "q \<bullet> cs = p \<bullet> cs" and **: "supp q \<subseteq> cs \<union> (p \<bullet> cs)" using b by metis

    62   have "[cs]set. x =  q \<bullet> ([cs]set. x)"

    63     apply(rule perm_supp_eq[symmetric])

    64     using a **

    65     unfolding fresh_star_Pair

    66     unfolding Abs_fresh_star_iff

    67     unfolding fresh_star_def

    68     by auto

    69   also have "\<dots> = [q \<bullet> cs]set. (q \<bullet> x)" by simp

    70   also have "\<dots> = [p \<bullet> cs]set. (q \<bullet> x)" using * by simp

    71   finally have "[cs]set. x = [p \<bullet> cs]set. (q \<bullet> x)" .

    72   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)"

    73     using * **

    74     by (blast)

    75 qed

    76 

    77 lemma at_set_avoiding5:

    78   assumes "finite xs"

    79   and     "finite (supp c)"

    80   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"

    81 using assms

    82 apply(erule_tac c="c" in at_set_avoiding)

    83 apply(auto)

    84 done

    85 

    86 lemma

    87   fixes c::"'a::fs"

    88   assumes a:  "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P"

    89   shows "y = LetRec lrbs exp \<Longrightarrow> P"

    90 apply -

    91 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))")

    92 apply(erule exE)

    93 apply(simp add: fresh_star_Pair)

    94 apply(erule conjE)+

    95 apply(simp add: multi_recs.fv_bn_eqvt)

    96 (*

    97 using Abs_rename_set2

    98 apply -

    99 apply(drule_tac x="p" in meta_spec)

   100 apply(drule_tac x="bs lrbs" in meta_spec)

   101 apply(drule_tac x="lrbs" in meta_spec)

   102 apply(drule meta_mp)

   103 apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair)

   104 apply(drule meta_mp)

   105 apply(simp add: multi_recs.bn_finite)

   106 apply(erule exE)

   107 apply(simp add: multi_recs.fv_bn_eqvt)

   108 *)

   109 apply(rule a)

   110 apply(assumption)

   111 apply(clarify)

   112 apply(simp (no_asm) only: multi_recs.eq_iff)

   113 apply(rule trans)

   114 apply(rule_tac p="p" in supp_perm_eq[symmetric])

   115 apply(rule fresh_star_supp_conv)

   116 apply(simp (no_asm_use) add: fresh_star_def)

   117 apply(simp (no_asm_use) add: Abs_fresh_iff)[1]

   118 apply(rule ballI)

   119 apply(auto simp add: fresh_Pair)[1]

   120 apply(simp (no_asm_use) only: permute_Abs)

   121 apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt)

   122 apply(simp)

   123 apply(rule at_set_avoiding5)

   124 apply(simp add: multi_recs.bn_finite)

   125 apply(simp add: supp_Pair finite_supp)

   126 apply(rule finite_sets_supp)

   127 apply(simp add: multi_recs.bn_finite)

   128 done

   129 

   130 

   131