259 apply(simp) |
257 apply(simp) |
260 apply(simp add: eqvt_at_def perm_supp_eq) |
258 apply(simp add: eqvt_at_def perm_supp_eq) |
261 apply(simp add: eqvt_at_def perm_supp_eq) |
259 apply(simp add: eqvt_at_def perm_supp_eq) |
262 done |
260 done |
263 |
261 |
|
262 termination by lexicographic_order |
264 |
263 |
265 lemma ww1: |
264 lemma ww1: |
266 shows "finite (fv_trm t)" |
265 shows "finite (fv_trm t)" |
267 and "finite (fv_bn as)" |
266 and "finite (fv_bn as)" |
268 apply(induct t and as rule: trm_assn.inducts) |
267 apply(induct t and as rule: trm_assn.inducts) |
322 subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and |
321 subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and |
323 subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90) |
322 subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90) |
324 where |
323 where |
325 "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))" |
324 "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))" |
326 | "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])" |
325 | "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])" |
327 | "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])" |
326 | "(set (bn as)) \<sharp>* (y, s, fv_bn as) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])" |
328 | "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])" |
327 | "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])" |
329 apply(subgoal_tac "\<And>p x r. subst_trm2_subst_assn2_graph x r \<Longrightarrow> subst_trm2_subst_assn2_graph (p \<bullet> x) (p \<bullet> r)") |
328 apply(subgoal_tac "\<And>p x r. subst_trm2_subst_assn2_graph x r \<Longrightarrow> subst_trm2_subst_assn2_graph (p \<bullet> x) (p \<bullet> r)") |
330 apply(simp add: eqvt_def) |
329 apply(simp add: eqvt_def) |
331 apply(rule allI) |
330 apply(rule allI) |
332 apply(simp add: permute_fun_def permute_bool_def) |
331 apply(simp add: permute_fun_def permute_bool_def) |
346 apply(rule TrueI) |
345 apply(rule TrueI) |
347 apply(case_tac x) |
346 apply(case_tac x) |
348 apply(simp) |
347 apply(simp) |
349 apply(case_tac a) |
348 apply(case_tac a) |
350 apply(simp) |
349 apply(simp) |
351 apply(rule_tac y="aa" and c="(b, c)" in trm_assn.strong_exhaust(1)) |
350 apply(rule_tac y="aa" and c="(b, c, aa)" in trm_assn.strong_exhaust(1)) |
352 apply(blast)+ |
351 apply(blast)+ |
|
352 apply(simp) |
|
353 apply(drule_tac x="assn" in meta_spec) |
|
354 apply(drule_tac x="b" in meta_spec) |
|
355 apply(drule_tac x="c" in meta_spec) |
|
356 apply(drule_tac x="trm" in meta_spec) |
|
357 apply(simp add: trm_assn.alpha_refl) |
|
358 apply(rotate_tac 5) |
|
359 apply(drule meta_mp) |
|
360 apply(simp add: fresh_star_Pair) |
|
361 apply(simp add: fresh_star_def trm_assn.fresh) |
|
362 apply(simp add: fresh_def) |
|
363 apply(subst supp_finite_atom_set) |
|
364 apply(simp) |
|
365 apply(simp) |
353 apply(simp) |
366 apply(simp) |
354 apply(case_tac b) |
367 apply(case_tac b) |
355 apply(simp) |
368 apply(simp) |
356 apply(rule_tac y="a" in trm_assn.exhaust(2)) |
369 apply(rule_tac y="a" in trm_assn.exhaust(2)) |
357 apply(simp) |
370 apply(simp) |
360 apply(all_trivials) |
373 apply(all_trivials) |
361 apply(simp) |
374 apply(simp) |
362 apply(simp) |
375 apply(simp) |
363 prefer 2 |
376 prefer 2 |
364 apply(simp) |
377 apply(simp) |
365 thm Inl_inject |
|
366 apply(drule Inl_inject) |
378 apply(drule Inl_inject) |
367 apply(rule arg_cong) |
379 apply(rule arg_cong) |
368 back |
380 back |
369 apply (simp only: meta_eq_to_obj_eq[OF subst_trm2_def, symmetric, unfolded fun_eq_iff]) |
381 apply (simp only: meta_eq_to_obj_eq[OF subst_trm2_def, symmetric, unfolded fun_eq_iff]) |
370 apply (simp only: meta_eq_to_obj_eq[OF subst_assn2_def, symmetric, unfolded fun_eq_iff]) |
382 apply (simp only: meta_eq_to_obj_eq[OF subst_assn2_def, symmetric, unfolded fun_eq_iff]) |
374 apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm2 ta ya sa) ta") |
386 apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm2 ta ya sa) ta") |
375 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (ast, y, s))") |
387 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (ast, y, s))") |
376 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))") |
388 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))") |
377 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))") |
389 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))") |
378 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))") |
390 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))") |
379 defer |
391 apply(simp) |
380 apply(simp add: Abs_eq_iff alphas) |
392 (* HERE *) |
381 apply(clarify) |
393 apply (subgoal_tac "subst_assn2 ast y s= subst_assn2 asta ya sa") |
382 apply(rule eqvt_at_perm) |
394 apply (subgoal_tac "subst_trm2 t y s = subst_trm2 ta ya sa") |
383 apply(simp) |
395 apply(simp) |
384 apply(simp add: subst_trm2_def) |
|
385 apply(simp add: eqvt_at_def) |
|
386 defer |
|
387 defer |
|
388 defer |
|
389 defer |
|
390 defer |
|
391 apply(rule conjI) |
|
392 apply (subgoal_tac "subst_assn2 ast ya sa= subst_assn2 asta ya sa") |
|
393 apply (subgoal_tac "subst_trm2 t ya sa = subst_trm2 ta ya sa") |
|
394 apply(simp) |
396 apply(simp) |
395 apply(erule_tac conjE)+ |
397 apply(erule_tac conjE)+ |
396 apply(erule alpha_bn_cases) |
398 apply(erule alpha_bn_cases) |
397 apply(simp add: trm_assn.bn_defs) |
399 apply(simp add: trm_assn.bn_defs) |
398 apply(rotate_tac 7) |
400 apply(rotate_tac 7) |
399 apply(drule k) |
|
400 apply(erule conjE) |
|
401 apply(subst (asm) Abs1_eq_iff) |
|
402 apply(rule sort_of_atom_eq) |
|
403 apply(rule sort_of_atom_eq) |
|
404 apply(erule disjE) |
|
405 apply(simp) |
|
406 apply(rotate_tac 12) |
|
407 apply(drule sym) |
|
408 apply(rule sym) |
|
409 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
401 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
410 apply(erule fresh_eqvt_at) |
402 apply(erule fresh_eqvt_at) |
|
403 |
411 |
404 |
412 thm fresh_eqvt_at |
405 thm fresh_eqvt_at |
413 apply(simp add: Abs_fresh_iff) |
406 apply(simp add: Abs_fresh_iff) |
414 apply(simp add: fresh_star_def fresh_Pair) |
407 apply(simp add: fresh_star_def fresh_Pair) |
415 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
408 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |