48 thm multi_recs.perm_bn_alpha |
48 thm multi_recs.perm_bn_alpha |
49 thm multi_recs.perm_bn_simps |
49 thm multi_recs.perm_bn_simps |
50 thm multi_recs.bn_finite |
50 thm multi_recs.bn_finite |
51 |
51 |
52 |
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: |
53 lemma at_set_avoiding5: |
78 assumes "finite xs" |
54 assumes "finite xs" |
79 and "finite (supp c)" |
55 and "finite (supp c)" |
80 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs" |
56 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs" |
81 using assms |
57 using assms |
86 lemma |
62 lemma |
87 fixes c::"'a::fs" |
63 fixes c::"'a::fs" |
88 assumes a: "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P" |
64 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" |
65 shows "y = LetRec lrbs exp \<Longrightarrow> P" |
90 apply - |
66 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))") |
67 apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp))") |
92 apply(erule exE) |
68 apply(erule exE) |
93 apply(simp add: fresh_star_Pair) |
69 apply(simp add: fresh_star_Pair) |
94 apply(erule conjE)+ |
70 apply(erule conjE)+ |
95 apply(simp add: multi_recs.fv_bn_eqvt) |
71 apply(simp add: multi_recs.fv_bn_eqvt) |
96 (* |
72 using Abs_rename_set' |
97 using Abs_rename_set2 |
|
98 apply - |
73 apply - |
99 apply(drule_tac x="p" in meta_spec) |
74 apply(drule_tac x="p" in meta_spec) |
100 apply(drule_tac x="bs lrbs" in meta_spec) |
75 apply(drule_tac x="bs lrbs" in meta_spec) |
101 apply(drule_tac x="lrbs" in meta_spec) |
76 apply(drule_tac x="(lrbs, exp)" in meta_spec) |
102 apply(drule meta_mp) |
77 apply(drule meta_mp) |
103 apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair) |
78 apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair) |
104 apply(drule meta_mp) |
79 apply(drule meta_mp) |
105 apply(simp add: multi_recs.bn_finite) |
80 apply(simp add: multi_recs.bn_finite) |
106 apply(erule exE) |
81 apply(erule exE) |
|
82 apply(erule conjE) |
|
83 apply(rotate_tac 6) |
|
84 apply(drule sym) |
107 apply(simp add: multi_recs.fv_bn_eqvt) |
85 apply(simp add: multi_recs.fv_bn_eqvt) |
108 *) |
|
109 apply(rule a) |
86 apply(rule a) |
110 apply(assumption) |
87 apply(assumption) |
111 apply(clarify) |
88 apply(clarify) |
112 apply(simp (no_asm) only: multi_recs.eq_iff) |
89 apply(simp (no_asm) only: multi_recs.eq_iff) |
113 apply(rule trans) |
90 apply(rule at_set_avoiding1) |
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) |
91 apply(simp add: multi_recs.bn_finite) |
125 apply(simp add: supp_Pair finite_supp) |
92 apply(simp add: supp_Pair finite_supp) |
126 apply(rule finite_sets_supp) |
93 apply(rule finite_sets_supp) |
127 apply(simp add: multi_recs.bn_finite) |
94 apply(simp add: multi_recs.bn_finite) |
128 done |
95 done |
129 |
96 |
130 |
|
131 |
|
132 end |
97 end |
133 |
98 |
134 |
99 |
135 |
100 |