48 thm foo.supports |
45 thm foo.supports |
49 thm foo.fsupp |
46 thm foo.fsupp |
50 thm foo.supp |
47 thm foo.supp |
51 thm foo.fresh |
48 thm foo.fresh |
52 |
49 |
53 lemma at_set_avoiding5: |
|
54 assumes "finite xs" |
|
55 and "finite (supp c)" |
|
56 shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs" |
|
57 using assms |
|
58 apply(erule_tac c="c" in at_set_avoiding) |
|
59 apply(auto) |
|
60 done |
|
61 |
|
62 |
|
63 lemma Abs_rename_lst3: |
|
64 fixes x::"'a::fs" |
|
65 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
|
66 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" |
|
67 proof - |
|
68 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |
|
69 by (simp add: fresh_star_Pair fresh_star_set) |
|
70 with list_renaming_perm |
|
71 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis |
|
72 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
|
73 apply(rule perm_supp_eq[symmetric]) |
|
74 using a ** |
|
75 unfolding fresh_star_Pair |
|
76 unfolding Abs_fresh_star_iff |
|
77 unfolding fresh_star_def |
|
78 by auto |
|
79 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
|
80 also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp |
|
81 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" . |
|
82 then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" |
|
83 using * ** by metis |
|
84 qed |
|
85 |
|
86 |
|
87 lemma |
|
88 fixes c::"'a::fs" |
|
89 assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
90 shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
91 apply - |
|
92 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
93 supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
94 defer |
|
95 apply(rule at_set_avoiding5) |
|
96 apply(simp add: foo.bn_finite) |
|
97 apply(simp add: supp_Pair finite_supp) |
|
98 apply(erule exE) |
|
99 apply(perm_simp add: foo.permute_bn) |
|
100 apply(simp add: fresh_star_Pair) |
|
101 apply(erule conjE)+ |
|
102 thm Abs_rename_lst |
|
103 apply(insert Abs_rename_lst)[1] |
|
104 apply(drule_tac x="p" in meta_spec) |
|
105 apply(drule_tac x="bn assg1" in meta_spec) |
|
106 apply(drule_tac x="trm1" in meta_spec) |
|
107 apply(insert Abs_rename_lst)[1] |
|
108 apply(drule_tac x="p" in meta_spec) |
|
109 apply(drule_tac x="bn assg2" in meta_spec) |
|
110 apply(drule_tac x="trm2" in meta_spec) |
|
111 apply(drule meta_mp) |
|
112 apply(perm_simp add: foo.permute_bn) |
|
113 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
114 apply(drule meta_mp) |
|
115 apply(perm_simp add: foo.permute_bn) |
|
116 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
117 apply(erule exE)+ |
|
118 apply(rule a) |
|
119 apply(assumption) |
|
120 apply(simp only: foo.eq_iff) |
|
121 apply(perm_simp add: foo.permute_bn) |
|
122 apply(rule conjI) |
|
123 apply(rule refl) |
|
124 apply(rule conjI) |
|
125 apply(rule foo.perm_bn_alpha) |
|
126 apply(rule conjI) |
|
127 apply(perm_simp add: foo.permute_bn) |
|
128 apply(rule refl) |
|
129 apply(rule foo.perm_bn_alpha) |
|
130 done |
|
131 |
|
132 lemma |
|
133 fixes c::"'a::fs" |
|
134 assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
135 shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
136 apply - |
|
137 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
138 supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
139 defer |
|
140 apply(rule at_set_avoiding5) |
|
141 apply(simp add: foo.bn_finite) |
|
142 apply(simp add: supp_Pair finite_supp) |
|
143 apply(erule exE) |
|
144 apply(perm_simp add: foo.permute_bn) |
|
145 apply(simp add: fresh_star_Pair) |
|
146 apply(erule conjE)+ |
|
147 apply(insert Abs_rename_lst3)[1] |
|
148 apply(drule_tac x="p" in meta_spec) |
|
149 apply(drule_tac x="bn assg1" in meta_spec) |
|
150 apply(drule_tac x="trm1" in meta_spec) |
|
151 apply(insert Abs_rename_lst3)[1] |
|
152 apply(drule_tac x="p" in meta_spec) |
|
153 apply(drule_tac x="bn assg2" in meta_spec) |
|
154 apply(drule_tac x="trm2" in meta_spec) |
|
155 apply(drule meta_mp) |
|
156 apply(perm_simp add: foo.permute_bn) |
|
157 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
158 apply(drule meta_mp) |
|
159 apply(perm_simp add: foo.permute_bn) |
|
160 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
161 apply(erule exE)+ |
|
162 apply(erule conjE)+ |
|
163 apply(simp add: foo.permute_bn) |
|
164 apply(rule a) |
|
165 apply(assumption) |
|
166 apply(clarify) |
|
167 apply(simp (no_asm) only: foo.eq_iff) |
|
168 apply(rule conjI) |
|
169 apply(assumption) |
|
170 apply(rule conjI) |
|
171 apply(rule foo.perm_bn_alpha) |
|
172 apply(rule conjI) |
|
173 apply(assumption) |
|
174 apply(rule foo.perm_bn_alpha) |
|
175 done |
|
176 |
|
177 |
|
178 lemma |
|
179 fixes c::"'a::fs" |
|
180 assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P" |
|
181 shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P" |
|
182 apply - |
|
183 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and> |
|
184 supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))") |
|
185 defer |
|
186 apply(rule at_set_avoiding5) |
|
187 apply(simp add: foo.bn_finite) |
|
188 apply(simp add: supp_Pair finite_supp) |
|
189 apply(erule exE) |
|
190 apply(simp add: fresh_star_Pair) |
|
191 apply(erule conjE)+ |
|
192 apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt) |
|
193 apply(rule a) |
|
194 apply(assumption) |
|
195 apply(clarify) |
|
196 apply(simp (no_asm) only: foo.eq_iff) |
|
197 apply(rule conjI) |
|
198 apply(rule trans) |
|
199 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
200 apply(rule fresh_star_supp_conv) |
|
201 apply(simp (no_asm_use) add: fresh_star_def) |
|
202 apply(simp (no_asm_use) add: Abs_fresh_iff)[1] |
|
203 apply(rule ballI) |
|
204 apply(auto simp add: fresh_Pair)[1] |
|
205 apply(simp (no_asm_use) only: permute_Abs) |
|
206 apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt) |
|
207 apply(simp) |
|
208 apply(rule at_set_avoiding5) |
|
209 apply(simp add: multi_recs.bn_finite) |
|
210 apply(simp add: supp_Pair finite_supp) |
|
211 apply(rule finite_sets_supp) |
|
212 apply(simp add: multi_recs.bn_finite) |
|
213 done |
|
214 |
|
215 |
|
216 |
|
217 lemma test6: |
|
218 fixes c::"'a::fs" |
|
219 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
220 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
221 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
222 and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P" |
|
223 and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P" |
|
224 shows "P" |
|
225 apply(rule_tac y="y" in foo.exhaust(1)) |
|
226 apply(rule assms(1)) |
|
227 apply(assumption) |
|
228 apply(rule assms(2)) |
|
229 apply(assumption) |
|
230 (* lam case *) |
|
231 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)") |
|
232 apply(erule exE) |
|
233 apply(insert Abs_rename_lst)[1] |
|
234 apply(drule_tac x="p" in meta_spec) |
|
235 apply(drule_tac x="[atom name]" in meta_spec) |
|
236 apply(drule_tac x="trm" in meta_spec) |
|
237 apply(simp only: fresh_star_Pair set.simps) |
|
238 apply(drule meta_mp) |
|
239 apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base) |
|
240 apply(erule exE) |
|
241 apply(rule assms(3)) |
|
242 apply(perm_simp) |
|
243 apply(erule conjE)+ |
|
244 apply(assumption) |
|
245 apply(clarify) |
|
246 apply(simp (no_asm) add: foo.eq_iff) |
|
247 apply(perm_simp) |
|
248 apply(assumption) |
|
249 apply(rule at_set_avoiding1) |
|
250 apply(simp) |
|
251 apply(simp add: finite_supp) |
|
252 (* let1 case *) |
|
253 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
|
254 apply(erule exE) |
|
255 apply(perm_simp add: foo.permute_bn) |
|
256 apply(simp add: fresh_star_Pair) |
|
257 apply(erule conjE)+ |
|
258 apply(insert Abs_rename_lst)[1] |
|
259 apply(drule_tac x="p" in meta_spec) |
|
260 apply(drule_tac x="bn assg1" in meta_spec) |
|
261 apply(drule_tac x="trm1" in meta_spec) |
|
262 apply(insert Abs_rename_lst)[1] |
|
263 apply(drule_tac x="p" in meta_spec) |
|
264 apply(drule_tac x="bn assg2" in meta_spec) |
|
265 apply(drule_tac x="trm2" in meta_spec) |
|
266 apply(drule meta_mp) |
|
267 apply(perm_simp add: foo.permute_bn) |
|
268 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
269 apply(drule meta_mp) |
|
270 apply(perm_simp add: foo.permute_bn) |
|
271 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
272 apply(erule exE)+ |
|
273 apply(rule assms(4)) |
|
274 apply(assumption) |
|
275 apply(simp add: foo.eq_iff refl) |
|
276 apply(rule conjI) |
|
277 apply(perm_simp add: foo.permute_bn) |
|
278 apply(rule refl) |
|
279 apply(rule conjI) |
|
280 apply(rule foo.perm_bn_alpha) |
|
281 apply(rule conjI) |
|
282 apply(perm_simp add: foo.permute_bn) |
|
283 apply(rule refl) |
|
284 apply(rule foo.perm_bn_alpha) |
|
285 apply(rule at_set_avoiding1) |
|
286 apply(simp) |
|
287 apply(simp add: finite_supp) |
|
288 (* let2 case *) |
|
289 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
|
290 apply(erule exE) |
|
291 apply(rule assms(5)) |
|
292 apply(simp only:) |
|
293 apply(simp only: foo.eq_iff) |
|
294 apply(insert Abs_rename_list)[1] |
|
295 apply(drule_tac x="p" in meta_spec) |
|
296 apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec) |
|
297 apply(drule_tac x="trm1" in meta_spec) |
|
298 apply(insert Abs_rename_list)[1] |
|
299 apply(drule_tac x="p" in meta_spec) |
|
300 apply(drule_tac x="[atom name2]" in meta_spec) |
|
301 apply(drule_tac x="trm2" in meta_spec) |
|
302 apply(drule meta_mp) |
|
303 apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp) |
|
304 apply(auto)[1] |
|
305 apply(perm_simp) |
|
306 apply(auto simp add: fresh_star_def)[1] |
|
307 apply(perm_simp) |
|
308 apply(auto simp add: fresh_star_def)[1] |
|
309 apply(perm_simp) |
|
310 apply(auto simp add: fresh_star_def)[1] |
|
311 apply(drule meta_mp) |
|
312 apply(perm_simp) |
|
313 apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1] |
|
314 apply(erule exE)+ |
|
315 apply(rule exI)+ |
|
316 apply(perm_simp add: foo.permute_bn) |
|
317 apply(rule conjI) |
|
318 prefer 2 |
|
319 apply(rule conjI) |
|
320 apply(assumption) |
|
321 apply(assumption) |
|
322 apply(simp add: fresh_star_Pair) |
|
323 apply(simp add: fresh_star_def) |
|
324 apply(rule at_set_avoiding1) |
|
325 apply(simp) |
|
326 apply(simp add: finite_supp) |
|
327 done |
|
328 |
|
329 lemma test5: |
|
330 fixes c::"'a::fs" |
|
331 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
332 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
333 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
334 and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P" |
|
335 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
336 shows "P" |
|
337 apply(rule_tac y="y" in test6) |
|
338 apply(erule exE)+ |
|
339 apply(rule assms(1)) |
|
340 apply(assumption) |
|
341 apply(erule exE)+ |
|
342 apply(rule assms(2)) |
|
343 apply(assumption) |
|
344 apply(rule assms(3)) |
|
345 apply(auto)[2] |
|
346 apply(erule exE)+ |
|
347 apply(rule assms(4)) |
|
348 apply(auto)[2] |
|
349 apply(erule exE)+ |
|
350 apply(rule assms(5)) |
|
351 apply(auto)[2] |
|
352 done |
|
353 |
|
354 |
|
355 lemma strong_induct: |
50 lemma strong_induct: |
356 fixes c :: "'a :: fs" |
51 fixes c :: "'a :: fs" |
357 and assg :: assg and trm :: trm |
52 and assg :: assg and trm :: trm |
358 assumes a0: "\<And>name c. P1 c (Var name)" |
53 assumes a0: "\<And>name c. P1 c (Var name)" |
359 and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)" |
54 and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)" |
360 and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)" |
55 and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)" |
361 and a3: "\<And>a1 t1 a2 t2 c. |
56 and a3: "\<And>a1 t1 a2 t2 c. |
362 \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk> |
57 \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk> |
363 \<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)" |
58 \<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)" |
364 and a4: "\<And>n1 n2 t1 t2 c. |
59 and a4: "\<And>n1 n2 t1 t2 c. |
365 \<lbrakk>{atom n1, atom n2} \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)" |
60 \<lbrakk>({atom n1} \<union> {atom n2}) \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)" |
366 and a5: "\<And>c. P2 c As_Nil" |
61 and a5: "\<And>c. P2 c As_Nil" |
367 and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)" |
62 and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)" |
368 shows "P1 c trm" "P2 c assg" |
63 shows "P1 c trm" "P2 c assg" |
369 using assms |
64 using assms |
370 apply(induction_schema) |
65 apply(induction_schema) |
371 apply(rule_tac y="trm" and c="c" in test5) |
66 apply(rule_tac y="trm" and c="c" in foo.strong_exhaust(1)) |
372 apply(simp_all)[5] |
67 apply(simp_all)[5] |
373 apply(rule_tac y="assg" in foo.exhaust(2)) |
68 apply(rule_tac ya="assg" in foo.strong_exhaust(2)) |
374 apply(simp_all)[2] |
69 apply(simp_all)[2] |
375 apply(relation "measure (sum_case (size o snd) (size o snd))") |
70 apply(relation "measure (sum_case (size o snd) (size o snd))") |
376 apply(simp_all add: foo.size) |
71 apply(simp_all add: foo.size) |
377 done |
72 done |
378 |
73 |