43 apply(rule assms) |
43 apply(rule assms) |
44 done |
44 done |
45 |
45 |
46 |
46 |
47 lemma supp_fv: |
47 lemma supp_fv: |
48 "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = {a. infinite {b. \<not>alpha_bn ((a \<rightleftharpoons> b) \<bullet> as) as}}" |
48 "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = supp_rel alpha_bn as" |
49 apply(rule single_let.induct) |
49 apply(rule single_let.induct) |
50 apply(simp_all (no_asm_use) only: single_let.fv_defs)[2] |
50 -- " 0A " |
51 apply(simp_all (no_asm_use) only: supp_def)[2] |
51 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
52 apply(simp_all (no_asm_use) only: single_let.perm_simps)[2] |
52 apply(simp only: supp_abs(3)[symmetric])? |
53 apply(simp_all (no_asm_use) only: single_let.eq_iff)[2] |
53 apply(simp (no_asm) only: supp_def) |
54 apply(simp_all (no_asm_use) only: de_Morgan_conj)[2] |
54 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
55 apply(simp_all (no_asm_use) only: Collect_disj_eq)[2] |
55 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
56 apply(simp_all (no_asm_use) only: finite_Un)[2] |
56 -- " 0B" |
57 apply(simp_all (no_asm_use) only: de_Morgan_conj)[2] |
57 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
58 apply(simp_all (no_asm_use) only: Collect_disj_eq)[2] |
58 apply(simp only: supp_abs(3)[symmetric])? |
59 apply(simp) |
59 apply(simp (no_asm) only: supp_def) |
|
60 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
|
61 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
|
62 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
60 --" 1 " |
63 --" 1 " |
61 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
64 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
62 apply(simp only: supp_abs(3)[symmetric]) |
65 apply(simp only: supp_abs(3)[symmetric]) |
63 apply(simp (no_asm) only: supp_def) |
66 apply(simp (no_asm) only: supp_def) |
64 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
67 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
68 apply(simp only:) |
71 apply(simp only:) |
69 -- " 2 " |
72 -- " 2 " |
70 apply(erule conjE)+ |
73 apply(erule conjE)+ |
71 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
74 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
72 apply(simp only: supp_abs(3)[symmetric]) |
75 apply(simp only: supp_abs(3)[symmetric]) |
73 apply(simp (no_asm) only: supp_def) |
76 apply(simp (no_asm) only: supp_def supp_rel_def) |
74 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
77 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
75 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
78 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
76 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
79 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
77 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
80 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
78 apply(drule test2) |
81 apply(drule test2) |
79 apply(simp only:) |
82 apply(simp only:) |
80 -- " 3 " |
83 -- " 3 " |
81 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
84 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
82 apply(simp only: supp_abs(1)[symmetric]) |
85 apply(simp only: supp_abs(1)[symmetric]) |
83 apply(simp (no_asm) only: supp_def) |
86 apply(simp (no_asm) only: supp_def supp_rel_def) |
84 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
87 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
85 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
88 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
86 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
89 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
87 apply(drule test2)+ |
90 apply(drule test2)+ |
88 apply(simp only: supp_Pair Un_assoc conj_assoc) |
91 apply(simp only: supp_Pair Un_assoc conj_assoc) |
107 apply(simp only: supp_Pair Un_assoc conj_assoc) |
110 apply(simp only: supp_Pair Un_assoc conj_assoc) |
108 -- "last" |
111 -- "last" |
109 apply(rule conjI) |
112 apply(rule conjI) |
110 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
113 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
111 apply(simp only: supp_abs(3)[symmetric]) |
114 apply(simp only: supp_abs(3)[symmetric]) |
112 apply(simp (no_asm) only: supp_def) |
115 apply(simp (no_asm) only: supp_def supp_rel_def) |
113 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
116 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
114 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
117 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
115 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
118 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
116 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
119 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
117 apply(drule test2)+ |
120 apply(drule test2)+ |
118 apply(simp only: supp_Pair Un_assoc conj_assoc) |
121 apply(simp only: supp_Pair Un_assoc conj_assoc) |
119 -- "other case" |
122 -- "other case" |
120 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
123 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
121 apply(simp only: supp_abs(3)[symmetric]) |
124 apply(simp only: supp_abs(3)[symmetric]) |
122 apply(simp (no_asm) only: supp_def) |
125 apply(simp (no_asm) only: supp_def supp_rel_def) |
123 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
126 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
124 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
127 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
125 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
128 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
126 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)? |
129 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)? |
127 apply(drule test2)+ |
130 apply(drule test2)+ |