41 thm foo.supports |
43 thm foo.supports |
42 thm foo.fsupp |
44 thm foo.fsupp |
43 thm foo.supp |
45 thm foo.supp |
44 thm foo.fresh |
46 thm foo.fresh |
45 |
47 |
46 lemma tt1: |
|
47 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
|
48 apply(induct as rule: foo.inducts(2)) |
|
49 apply(auto)[5] |
|
50 apply(simp only: foo.perm_bn_simps foo.bn_defs) |
|
51 apply(perm_simp) |
|
52 apply(simp only:) |
|
53 apply(simp only: foo.perm_bn_simps foo.bn_defs) |
|
54 apply(perm_simp add: foo.fv_bn_eqvt) |
|
55 apply(simp only:) |
|
56 done |
|
57 |
|
58 text {* |
48 text {* |
59 tests by cu |
49 tests by cu |
60 *} |
50 *} |
61 |
51 |
62 lemma yy: |
52 lemma set_renaming_perm: |
63 assumes a: "p \<bullet> bs \<inter> bs = {}" |
53 assumes a: "p \<bullet> bs \<inter> bs = {}" |
64 and b: "finite bs" |
54 and b: "finite bs" |
65 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
55 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
66 using b a |
56 using b a |
67 apply(induct) |
57 proof (induct) |
68 apply(simp add: permute_set_eq) |
58 case empty |
69 apply(rule_tac x="0" in exI) |
59 have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}" |
70 apply(simp add: supp_perm) |
60 by (simp add: permute_set_eq supp_perm) |
71 apply(perm_simp) |
61 then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast |
72 apply(drule meta_mp) |
62 next |
73 apply(auto simp add: fresh_star_def fresh_finite_insert)[1] |
63 case (insert a bs) |
74 apply(erule exE) |
64 then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" |
75 apply(simp) |
65 by (perm_simp) (auto) |
76 apply(case_tac "q \<bullet> x = p \<bullet> x") |
66 then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast |
77 apply(rule_tac x="q" in exI) |
67 { assume 1: "q \<bullet> a = p \<bullet> a" |
78 apply(auto)[1] |
68 have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt) |
79 apply(rule_tac x="((q \<bullet> x) \<rightleftharpoons> (p \<bullet> x)) + q" in exI) |
69 moreover |
80 apply(subgoal_tac "p \<bullet> x \<notin> p \<bullet> F") |
70 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
81 apply(subgoal_tac "q \<bullet> x \<notin> p \<bullet> F") |
71 using ** by (auto simp add: insert_eqvt) |
82 apply(simp add: swap_set_not_in) |
72 ultimately |
83 apply(rule subset_trans) |
73 have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast |
84 apply(rule supp_plus_perm) |
74 } |
85 apply(simp) |
75 moreover |
86 apply(rule conjI) |
76 { assume 2: "q \<bullet> a \<noteq> p \<bullet> a" |
87 apply(simp add: supp_swap) |
77 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
88 apply(simp add: supp_perm) |
78 { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff) |
89 apply(auto)[1] |
79 moreover |
90 apply(auto)[1] |
80 have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff) |
91 apply(erule conjE)+ |
81 ultimately |
92 apply(drule sym) |
82 have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def |
93 apply(simp add: mem_permute_iff) |
83 by (simp add: insert_eqvt swap_set_not_in) |
94 apply(simp add: mem_permute_iff) |
84 } |
95 done |
85 moreover |
96 |
86 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
|
87 using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}` |
|
88 by (auto simp add: supp_perm insert_eqvt) |
|
89 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap) |
|
90 moreover |
|
91 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
|
92 using ** by (auto simp add: insert_eqvt) |
|
93 ultimately |
|
94 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
|
95 unfolding q'_def using supp_plus_perm by blast |
|
96 } |
|
97 ultimately |
|
98 have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast |
|
99 } |
|
100 ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
|
101 by blast |
|
102 qed |
97 |
103 |
98 |
104 |
99 lemma Abs_rename_set: |
105 lemma Abs_rename_set: |
100 fixes x::"'a::fs" |
106 fixes x::"'a::fs" |
101 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
107 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
102 and b: "finite bs" |
108 and b: "finite bs" |
103 shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" |
109 shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" |
104 proof - |
110 proof - |
105 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) |
111 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) |
106 with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
112 with set_renaming_perm |
|
113 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
107 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
114 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
108 apply(rule perm_supp_eq[symmetric]) |
115 apply(rule perm_supp_eq[symmetric]) |
109 using a ** |
116 using a ** |
110 unfolding fresh_star_Pair |
117 unfolding fresh_star_Pair |
111 unfolding Abs_fresh_star_iff |
118 unfolding Abs_fresh_star_iff |
122 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
129 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
123 and b: "finite bs" |
130 and b: "finite bs" |
124 shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" |
131 shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" |
125 proof - |
132 proof - |
126 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) |
133 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) |
127 with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
134 with set_renaming_perm |
|
135 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
128 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
136 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
129 apply(rule perm_supp_eq[symmetric]) |
137 apply(rule perm_supp_eq[symmetric]) |
130 using a ** |
138 using a ** |
131 unfolding fresh_star_Pair |
139 unfolding fresh_star_Pair |
132 unfolding Abs_fresh_star_iff |
140 unfolding Abs_fresh_star_iff |
136 also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp |
144 also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp |
137 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" . |
145 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" . |
138 then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast |
146 then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast |
139 qed |
147 qed |
140 |
148 |
141 lemma zz0: |
149 lemma list_renaming_perm: |
142 assumes "p \<bullet> bs = q \<bullet> bs" |
|
143 and a: "a \<in> set bs" |
|
144 shows "p \<bullet> a = q \<bullet> a" |
|
145 using assms |
|
146 by (induct bs) (auto) |
|
147 |
|
148 lemma zz: |
|
149 fixes bs::"atom list" |
150 fixes bs::"atom list" |
150 assumes "(p \<bullet> (set bs)) \<inter> (set bs) = {}" |
151 assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}" |
151 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
152 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
152 using assms |
153 using a |
153 apply(induct bs) |
154 proof (induct bs) |
154 apply(simp add: permute_set_eq) |
155 case Nil |
155 apply(rule_tac x="0" in exI) |
156 have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
156 apply(simp add: supp_perm) |
157 by (simp add: permute_set_eq supp_perm) |
157 apply(drule meta_mp) |
158 then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast |
158 apply(perm_simp) |
159 next |
159 apply(auto)[1] |
160 case (Cons a bs) |
160 apply(erule exE) |
161 then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" |
161 apply(simp) |
162 by (perm_simp) (auto) |
162 apply(case_tac "a \<in> set bs") |
163 then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast |
163 apply(rule_tac x="q" in exI) |
164 { assume 1: "a \<in> set bs" |
164 apply(perm_simp) |
165 have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto) |
165 apply(auto dest: zz0)[1] |
166 then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp |
166 apply(subgoal_tac "q \<bullet> a \<sharp> p \<bullet> bs") |
167 moreover |
167 apply(subgoal_tac "p \<bullet> a \<sharp> p \<bullet> bs") |
168 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt) |
168 apply(rule_tac x="((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" in exI) |
169 ultimately |
169 apply(simp add: swap_fresh_fresh) |
170 have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast |
170 apply(rule subset_trans) |
171 } |
171 apply(rule supp_plus_perm) |
172 moreover |
172 apply(simp) |
173 { assume 2: "a \<notin> set bs" |
173 apply(rule conjI) |
174 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
174 apply(simp add: supp_swap) |
175 { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] |
175 apply(simp add: supp_perm) |
176 by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list) |
176 apply(perm_simp) |
177 moreover |
177 apply(auto simp add: fresh_def supp_of_atom_list)[1] |
178 have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` |
178 apply(perm_simp) |
179 by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list) |
179 apply(auto)[1] |
180 ultimately |
180 apply(simp add: fresh_permute_iff) |
181 have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def |
181 apply(simp add: fresh_def supp_of_atom_list) |
182 by (simp add: swap_fresh_fresh) |
182 apply(erule conjE)+ |
183 } |
183 apply(drule sym) |
184 moreover |
184 apply(drule sym) |
185 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
185 apply(simp) |
186 using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}` |
186 apply(simp add: fresh_permute_iff) |
187 by (auto simp add: supp_perm insert_eqvt) |
187 apply(auto simp add: fresh_def supp_of_atom_list)[1] |
188 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap) |
188 done |
189 moreover |
|
190 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
|
191 using ** by (auto simp add: insert_eqvt) |
|
192 ultimately |
|
193 have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
|
194 unfolding q'_def using supp_plus_perm by blast |
|
195 } |
|
196 ultimately |
|
197 have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast |
|
198 } |
|
199 ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
|
200 by blast |
|
201 qed |
|
202 |
189 |
203 |
190 lemma Abs_rename_list: |
204 lemma Abs_rename_list: |
191 fixes x::"'a::fs" |
205 fixes x::"'a::fs" |
192 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
206 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
193 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
207 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
194 proof - |
208 proof - |
195 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |
209 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |
196 by (simp add: fresh_star_Pair fresh_star_set) |
210 by (simp add: fresh_star_Pair fresh_star_set) |
197 with zz obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis |
211 with list_renaming_perm |
|
212 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis |
198 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
213 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
199 apply(rule perm_supp_eq[symmetric]) |
214 apply(rule perm_supp_eq[symmetric]) |
200 using a ** |
215 using a ** |
201 unfolding fresh_star_Pair |
216 unfolding fresh_star_Pair |
202 unfolding Abs_fresh_star_iff |
217 unfolding Abs_fresh_star_iff |
206 also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp |
221 also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp |
207 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" . |
222 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" . |
208 then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast |
223 then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast |
209 qed |
224 qed |
210 |
225 |
|
226 (* |
|
227 thm at_set_avoiding1[THEN exE] |
|
228 |
|
229 |
|
230 lemma Let1_rename: |
|
231 fixes c::"'a::fs" |
|
232 shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and> Lam name trm = Lam name' trm'" |
|
233 apply(simp only: foo.eq_iff) |
|
234 apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE]) |
|
235 apply(simp) |
|
236 apply(simp add: finite_supp) |
|
237 apply(perm_simp) |
|
238 apply(rule Abs_rename_list[THEN exE]) |
|
239 apply(simp only: set_eqvt) |
|
240 apply |
|
241 sorry |
|
242 *) |
211 |
243 |
212 lemma test6: |
244 lemma test6: |
213 fixes c::"'a::fs" |
245 fixes c::"'a::fs" |
214 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
246 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
215 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
247 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
243 apply(perm_simp) |
283 apply(perm_simp) |
244 apply(assumption) |
284 apply(assumption) |
245 apply(rule at_set_avoiding1) |
285 apply(rule at_set_avoiding1) |
246 apply(simp) |
286 apply(simp) |
247 apply(simp add: finite_supp) |
287 apply(simp add: finite_supp) |
|
288 (* let1 case *) |
248 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
289 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
249 apply(erule exE) |
290 apply(erule exE) |
250 apply(rule assms(4)) |
291 apply(rule assms(4)) |
251 apply(simp only:) |
|
252 apply(simp only: foo.eq_iff) |
292 apply(simp only: foo.eq_iff) |
253 apply(insert Abs_rename_list)[1] |
293 apply(insert Abs_rename_list)[1] |
254 apply(drule_tac x="p" in meta_spec) |
294 apply(drule_tac x="p" in meta_spec) |
255 apply(drule_tac x="bn assg1" in meta_spec) |
295 apply(drule_tac x="bn assg1" in meta_spec) |
256 apply(drule_tac x="trm1" in meta_spec) |
296 apply(drule_tac x="trm1" in meta_spec) |