32 thm single_let.fv_bn_eqvt |
32 thm single_let.fv_bn_eqvt |
33 thm single_let.size_eqvt |
33 thm single_let.size_eqvt |
34 thm single_let.supports |
34 thm single_let.supports |
35 thm single_let.fsupp |
35 thm single_let.fsupp |
36 |
36 |
37 lemma supp_abs_sum: |
|
38 fixes a b::"'a::fs" |
|
39 shows "supp (Abs x a) \<union> supp (Abs x b) = supp (Abs x (a, b))" |
|
40 and "supp (Abs_res x a) \<union> supp (Abs_res x b) = supp (Abs_res x (a, b))" |
|
41 and "supp (Abs_lst y a) \<union> supp (Abs_lst y b) = supp (Abs_lst y (a, b))" |
|
42 apply (simp_all add: supp_abs supp_Pair) |
|
43 apply blast+ |
|
44 done |
|
45 |
|
46 |
|
47 lemma test: |
|
48 "(\<exists>p. (bs, x) \<approx>gen (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
|
49 sorry |
|
50 |
|
51 lemma Abs_eq_iff: |
37 lemma Abs_eq_iff: |
52 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
38 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
53 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
39 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
54 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
40 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
55 by (lifting alphas_abs) |
41 by (lifting alphas_abs) |
56 |
42 |
57 lemma test2: |
43 lemma test2: |
58 assumes "fv_trm t = supp t" |
44 assumes "fv_trm t = supp t" |
59 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
45 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
60 sorry |
46 apply(rule allI) |
61 |
47 apply(rule_tac p="-p" in permute_boolE) |
62 lemma yy: |
48 apply(perm_simp add: single_let.fv_bn_eqvt permute_minus_cancel) |
63 "X = Y \<Longrightarrow> finite X = finite Y" by simp |
49 apply(rule assms) |
|
50 done |
64 |
51 |
65 |
52 |
66 lemma supp_fv: |
53 lemma supp_fv: |
67 "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}}" |
54 "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}}" |
68 apply(rule single_let.induct) |
55 apply(rule single_let.induct) |
69 apply(simp_all only: single_let.fv_defs)[2] |
56 apply(simp_all (no_asm_use) only: single_let.fv_defs)[2] |
70 apply(simp_all only: supp_def)[2] |
57 apply(simp_all (no_asm_use) only: supp_def)[2] |
71 apply(simp_all only: single_let.perm_simps)[2] |
58 apply(simp_all (no_asm_use) only: single_let.perm_simps)[2] |
72 apply(simp_all only: single_let.eq_iff)[2] |
59 apply(simp_all (no_asm_use) only: single_let.eq_iff)[2] |
73 apply(simp_all only: de_Morgan_conj)[2] |
60 apply(simp_all (no_asm_use) only: de_Morgan_conj)[2] |
74 apply(simp_all only: Collect_disj_eq)[2] |
61 apply(simp_all (no_asm_use) only: Collect_disj_eq)[2] |
75 apply(simp_all only: finite_Un)[2] |
62 apply(simp_all (no_asm_use) only: finite_Un)[2] |
76 apply(simp_all only: de_Morgan_conj)[2] |
63 apply(simp_all (no_asm_use) only: de_Morgan_conj)[2] |
77 apply(simp_all only: Collect_disj_eq)[2] |
64 apply(simp_all (no_asm_use) only: Collect_disj_eq)[2] |
|
65 apply(simp) |
78 --" 1 " |
66 --" 1 " |
79 apply(simp only: single_let.fv_defs) |
67 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
80 apply(simp add: supp_abs(1)[symmetric]) |
68 apply(simp only: supp_abs(3)[symmetric]) |
81 apply(simp (no_asm) only: supp_def) |
69 apply(simp (no_asm) only: supp_def) |
82 apply(simp only: single_let.perm_simps) |
70 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
83 apply(simp only: single_let.eq_iff) |
71 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
84 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
72 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
85 apply(perm_simp) |
|
86 apply(simp only: Abs_eq_iff) |
|
87 apply(simp add: alphas) |
|
88 apply(drule test2) |
73 apply(drule test2) |
89 apply(simp) |
74 apply(simp only:) |
90 -- " 2 " |
75 -- " 2 " |
91 apply(erule conjE)+ |
76 apply(erule conjE)+ |
92 apply(simp only: single_let.fv_defs) |
77 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
93 apply(simp add: supp_abs(1)[symmetric]) |
78 apply(simp only: supp_abs(3)[symmetric]) |
94 apply(simp (no_asm) only: supp_def) |
79 apply(simp (no_asm) only: supp_def) |
95 apply(simp only: single_let.perm_simps) |
80 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
96 apply(simp only: single_let.eq_iff) |
81 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
97 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
82 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
98 apply(perm_simp add: single_let.fv_bn_eqvt) |
83 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
99 apply(simp only: de_Morgan_conj) |
|
100 apply(simp only: Collect_disj_eq) |
|
101 apply(simp only: Abs_eq_iff) |
|
102 apply(simp only: finite_Un) |
|
103 apply(simp only: de_Morgan_conj) |
|
104 apply(simp only: Collect_disj_eq) |
|
105 apply(simp add: alphas) |
|
106 apply(drule test2) |
84 apply(drule test2) |
107 apply(simp) |
85 apply(simp only:) |
108 -- " 3 " |
86 -- " 3 " |
109 apply(simp only: single_let.fv_defs) |
87 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
110 apply(simp only: supp_Pair[symmetric]) |
88 apply(simp only: supp_abs(1)[symmetric]) |
111 apply(simp add: supp_abs(1)[symmetric]) |
|
112 apply(simp (no_asm) only: supp_def) |
89 apply(simp (no_asm) only: supp_def) |
113 apply(simp only: single_let.perm_simps) |
90 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
114 apply(simp only: single_let.eq_iff) |
91 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
115 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
92 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
116 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
117 apply(simp only: Abs_eq_iff) |
|
118 apply(simp add: alphas) |
|
119 apply(simp add: supp_Pair) |
|
120 apply(drule test2)+ |
93 apply(drule test2)+ |
121 apply(simp) |
94 apply(simp only: supp_Pair Un_assoc conj_assoc) |
122 apply(simp add: prod_alpha_def) |
|
123 apply(simp add: Un_assoc) |
|
124 apply(rule Collect_cong) |
|
125 apply(rule arg_cong) |
|
126 back |
|
127 apply(rule yy) |
|
128 apply(rule Collect_cong) |
|
129 apply(auto)[1] |
|
130 -- " Bar " |
95 -- " Bar " |
131 apply(simp only: single_let.fv_defs) |
96 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
132 apply(simp only: supp_Pair[symmetric]) |
97 apply(simp only: supp_abs(3)[symmetric]) |
133 apply(simp add: supp_abs(1)[symmetric]) |
|
134 apply(simp (no_asm) only: supp_def) |
98 apply(simp (no_asm) only: supp_def) |
135 apply(simp only: single_let.perm_simps) |
99 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
136 apply(simp only: single_let.eq_iff) |
100 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
137 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
101 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
138 apply(perm_simp add: single_let.fv_bn_eqvt) |
102 apply(drule test2)+ |
139 apply(simp only: Abs_eq_iff) |
103 apply(simp only: supp_Pair Un_assoc conj_assoc) |
140 apply(simp add: alphas prod_alpha_def) |
104 -- " Baz " |
141 apply(drule test2) |
105 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
142 apply(simp add: supp_Pair) |
106 apply(simp only: supp_abs(3)[symmetric]) |
143 apply(subst atom_eqvt) |
107 apply(simp (no_asm) only: supp_def) |
144 apply(simp) |
108 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
145 apply(simp add: Un_assoc) |
109 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
146 apply(rule Collect_cong) |
110 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
147 apply(rule arg_cong) |
111 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
148 back |
112 apply(drule test2)+ |
149 apply(rule yy) |
113 apply(simp only: supp_Pair Un_assoc conj_assoc) |
150 apply(rule Collect_cong) |
|
151 -- "last" |
114 -- "last" |
152 prefer 3 |
|
153 apply(rule conjI) |
115 apply(rule conjI) |
154 apply(simp only: single_let.fv_defs) |
116 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
155 apply(perm_simp add: single_let.fv_bn_eqvt) |
117 apply(simp only: supp_abs(3)[symmetric]) |
156 apply(simp add: supp_abs(1)[symmetric]) |
|
157 apply(simp (no_asm) only: supp_def) |
118 apply(simp (no_asm) only: supp_def) |
158 apply(simp only: single_let.perm_simps) |
119 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
159 apply(simp only: single_let.eq_iff) |
120 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
160 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
121 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
161 apply(perm_simp add: single_let.fv_bn_eqvt) |
122 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
162 apply(simp only: Abs_eq_iff) |
123 apply(drule test2)+ |
163 apply(simp only: de_Morgan_conj) |
124 apply(simp only: supp_Pair Un_assoc conj_assoc) |
164 apply(simp only: Collect_disj_eq) |
125 -- "other case" |
165 apply(simp only: finite_Un) |
126 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
166 apply(simp only: de_Morgan_conj) |
127 apply(simp only: supp_abs(3)[symmetric]) |
167 apply(simp only: Collect_disj_eq) |
|
168 apply(simp add: alphas prod_alpha_def) |
|
169 apply(drule test2) |
|
170 apply(simp add: supp_Pair) |
|
171 apply(simp only: permute_set_eq) |
|
172 apply(simp) |
|
173 apply(perm_simp add: single_let.fv_bn_eqvt) |
|
174 apply(simp only: single_let.eq_iff) |
|
175 apply(simp only: single_let.fv_defs) |
|
176 apply(simp add: supp_abs(1)[symmetric]) |
|
177 apply(simp (no_asm) only: supp_def) |
128 apply(simp (no_asm) only: supp_def) |
178 apply(perm_simp) |
129 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
179 oops |
130 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
|
131 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
|
132 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)? |
|
133 apply(drule test2)+ |
|
134 apply(simp only: supp_Pair Un_assoc conj_assoc) |
|
135 done |
180 |
136 |
181 |
137 |
182 |
138 |
183 |
139 |
184 |
140 |