59 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
59 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
60 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
60 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
61 apply(simp add: atom_eqvt) |
61 apply(simp add: atom_eqvt) |
62 done |
62 done |
63 |
63 |
64 |
64 text {* |
65 lemma Let1_rename: |
65 tests by cu |
66 assumes "supp ([bn assn1]lst. trm1) \<sharp>* p" "supp ([bn assn2]lst. trm2) \<sharp>* p" |
66 *} |
67 shows "Let1 assn1 trm1 assn2 trm2 = Let1 (permute_bn p assn1) (p \<bullet> trm1) (permute_bn p assn2) (p \<bullet> trm2)" |
67 |
|
68 |
|
69 lemma yy: |
|
70 assumes a: "p \<bullet> bs \<inter> bs = {}" |
|
71 and b: "finite bs" |
|
72 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
|
73 using b a |
|
74 apply(induct) |
|
75 apply(simp add: permute_set_eq) |
|
76 apply(rule_tac x="0" in exI) |
|
77 apply(simp add: supp_perm) |
|
78 apply(perm_simp) |
|
79 apply(drule meta_mp) |
|
80 apply(auto simp add: fresh_star_def fresh_finite_insert)[1] |
|
81 apply(erule exE) |
|
82 apply(simp) |
|
83 apply(case_tac "q \<bullet> x = p \<bullet> x") |
|
84 apply(rule_tac x="q" in exI) |
|
85 apply(auto)[1] |
|
86 apply(rule_tac x="((q \<bullet> x) \<rightleftharpoons> (p \<bullet> x)) + q" in exI) |
|
87 apply(subgoal_tac "p \<bullet> x \<notin> p \<bullet> F") |
|
88 apply(subgoal_tac "q \<bullet> x \<notin> p \<bullet> F") |
|
89 apply(simp add: swap_set_not_in) |
|
90 apply(rule subset_trans) |
|
91 apply(rule supp_plus_perm) |
|
92 apply(simp) |
|
93 apply(rule conjI) |
|
94 apply(simp add: supp_swap) |
|
95 apply(simp add: supp_perm) |
|
96 apply(auto)[1] |
|
97 apply(auto)[1] |
|
98 apply(erule conjE)+ |
|
99 apply(drule sym) |
|
100 apply(simp add: mem_permute_iff) |
|
101 apply(simp add: mem_permute_iff) |
|
102 done |
|
103 |
|
104 lemma yy1: |
|
105 assumes "(p \<bullet> bs) \<sharp>* bs" "finite bs" |
|
106 shows "p \<bullet> bs \<inter> bs = {}" |
68 using assms |
107 using assms |
|
108 apply(auto simp add: fresh_star_def) |
|
109 apply(simp add: fresh_def supp_finite_atom_set) |
|
110 done |
|
111 |
|
112 lemma abs_rename_set: |
|
113 fixes x::"'a::fs" |
|
114 assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs" |
|
115 shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" |
|
116 using yy assms |
69 apply - |
117 apply - |
70 apply(drule supp_perm_eq[symmetric]) |
118 apply(drule_tac x="p" in meta_spec) |
71 apply(drule supp_perm_eq[symmetric]) |
119 apply(drule_tac x="bs" in meta_spec) |
72 apply(simp only: permute_Abs) |
120 apply(auto simp add: yy1) |
73 apply(simp only: tt1) |
121 apply(rule_tac x="q \<bullet> x" in exI) |
|
122 apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x") |
|
123 apply(simp) |
|
124 apply(rule supp_perm_eq) |
|
125 apply(rule fresh_star_supp_conv) |
|
126 apply(simp add: fresh_star_def) |
|
127 apply(simp add: Abs_fresh_iff) |
|
128 apply(auto) |
|
129 done |
|
130 |
|
131 lemma zz0: |
|
132 assumes "p \<bullet> bs = q \<bullet> bs" |
|
133 and a: "a \<in> set bs" |
|
134 shows "p \<bullet> a = q \<bullet> a" |
|
135 using assms |
|
136 by (induct bs) (auto) |
|
137 |
|
138 lemma zz: |
|
139 fixes bs::"atom list" |
|
140 assumes "set bs \<inter> (p \<bullet> (set bs)) = {}" |
|
141 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))" |
|
142 using assms |
|
143 apply(induct bs) |
|
144 apply(simp add: permute_set_eq) |
|
145 apply(rule_tac x="0" in exI) |
|
146 apply(simp add: supp_perm) |
|
147 apply(drule meta_mp) |
|
148 apply(perm_simp) |
|
149 apply(auto)[1] |
|
150 apply(erule exE) |
|
151 apply(simp) |
|
152 apply(case_tac "a \<in> set bs") |
|
153 apply(rule_tac x="q" in exI) |
|
154 apply(perm_simp) |
|
155 apply(auto dest: zz0)[1] |
|
156 apply(subgoal_tac "q \<bullet> a \<sharp> p \<bullet> bs") |
|
157 apply(subgoal_tac "p \<bullet> a \<sharp> p \<bullet> bs") |
|
158 apply(rule_tac x="((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" in exI) |
|
159 apply(simp add: swap_fresh_fresh) |
|
160 apply(rule subset_trans) |
|
161 apply(rule supp_plus_perm) |
|
162 apply(simp) |
|
163 apply(rule conjI) |
|
164 apply(simp add: supp_swap) |
|
165 apply(simp add: supp_perm) |
|
166 apply(perm_simp) |
|
167 apply(auto simp add: fresh_def supp_of_atom_list)[1] |
|
168 apply(perm_simp) |
|
169 apply(auto)[1] |
|
170 apply(simp add: fresh_permute_iff) |
|
171 apply(simp add: fresh_def supp_of_atom_list) |
|
172 apply(erule conjE)+ |
|
173 apply(drule sym) |
|
174 apply(drule sym) |
|
175 apply(simp) |
|
176 apply(simp add: fresh_permute_iff) |
|
177 apply(auto simp add: fresh_def supp_of_atom_list)[1] |
|
178 done |
|
179 |
|
180 lemma zz1: |
|
181 assumes "(p \<bullet> (set bs)) \<sharp>* bs" |
|
182 shows "(set bs) \<inter> (p \<bullet> (set bs)) = {}" |
|
183 using assms |
|
184 apply(auto simp add: fresh_star_def) |
|
185 apply(simp add: fresh_def supp_of_atom_list) |
|
186 done |
|
187 |
|
188 lemma abs_rename_list: |
|
189 fixes x::"'a::fs" |
|
190 assumes "(p \<bullet> (set bs)) \<sharp>* x" "(p \<bullet> (set bs)) \<sharp>* bs" |
|
191 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
|
192 using zz assms |
|
193 apply - |
|
194 apply(drule_tac x="bs" in meta_spec) |
|
195 apply(drule_tac x="p" in meta_spec) |
|
196 apply(drule_tac zz1) |
|
197 apply(auto) |
|
198 apply(rule_tac x="q \<bullet> x" in exI) |
|
199 apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x") |
|
200 apply(simp) |
|
201 apply(rule supp_perm_eq) |
|
202 apply(rule fresh_star_supp_conv) |
|
203 apply(simp add: fresh_star_def) |
|
204 apply(simp add: Abs_fresh_iff) |
|
205 apply(auto) |
|
206 done |
|
207 |
|
208 lemma fresh_star_list: |
|
209 shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys" |
|
210 and "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs" |
|
211 and "as \<sharp>* []" |
|
212 by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append) |
|
213 |
|
214 |
|
215 lemma test6: |
|
216 fixes c::"'a::fs" |
|
217 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
|
218 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
219 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
|
220 and "\<exists>a1 trm1 a2 trm2. ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P" |
|
221 and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P" |
|
222 shows "P" |
|
223 apply(rule_tac y="y" in foo.exhaust(1)) |
|
224 apply(rule assms(1)) |
|
225 apply(rule exI)+ |
|
226 apply(assumption) |
|
227 apply(rule assms(2)) |
|
228 apply(rule exI)+ |
|
229 apply(assumption) |
|
230 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)") |
|
231 apply(erule exE) |
|
232 apply(rule assms(3)) |
|
233 apply(insert abs_rename_list)[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_prod set.simps) |
|
238 apply(drule meta_mp) |
|
239 apply(rule TrueI) |
|
240 apply(drule meta_mp) |
|
241 apply(rule TrueI) |
|
242 apply(erule exE) |
|
243 apply(rule exI)+ |
|
244 apply(perm_simp) |
|
245 apply(erule conjE)+ |
|
246 apply(rule conjI) |
|
247 apply(assumption) |
|
248 apply(simp add: foo.eq_iff) |
|
249 defer |
|
250 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
|
251 apply(erule exE) |
|
252 apply(rule assms(4)) |
|
253 apply(simp only:) |
74 apply(simp only: foo.eq_iff) |
254 apply(simp only: foo.eq_iff) |
75 apply(simp add: uu1) |
255 apply(insert abs_rename_list)[1] |
76 done |
256 apply(drule_tac x="p" in meta_spec) |
77 |
257 apply(drule_tac x="bn assg1" in meta_spec) |
78 lemma Let2_rename: |
258 apply(drule_tac x="trm1" in meta_spec) |
79 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(supp ([[atom y]]lst. t2)) \<sharp>* p" |
259 apply(insert abs_rename_list)[1] |
80 shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)" |
260 apply(drule_tac x="p" in meta_spec) |
81 using assms |
261 apply(drule_tac x="bn assg2" in meta_spec) |
82 apply - |
262 apply(drule_tac x="trm2" in meta_spec) |
83 apply(drule supp_perm_eq[symmetric]) |
263 apply(drule meta_mp) |
84 apply(drule supp_perm_eq[symmetric]) |
264 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
85 apply(simp only: foo.eq_iff) |
265 apply(drule meta_mp) |
86 apply(simp only: eqvts) |
266 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
87 apply simp |
267 apply(drule meta_mp) |
88 done |
268 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
89 |
269 apply(drule meta_mp) |
90 lemma Let2_rename2: |
270 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
91 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(atom y) \<sharp> p" |
271 apply(erule exE)+ |
92 shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) y (p \<bullet> t1) t2" |
272 apply(rule exI)+ |
93 using assms |
273 apply(perm_simp add: tt1) |
94 apply - |
274 apply(rule conjI) |
95 apply(drule supp_perm_eq[symmetric]) |
275 apply(simp add: fresh_star_prod fresh_star_union) |
96 apply(simp only: foo.eq_iff) |
276 apply(erule conjE)+ |
97 apply(simp only: eqvts) |
277 apply(rule conjI) |
98 apply simp |
278 apply(assumption) |
99 by (metis assms(2) atom_eqvt fresh_perm) |
279 apply(rotate_tac 4) |
100 |
280 apply(assumption) |
101 lemma Let2_rename3: |
281 apply(rule conjI) |
102 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" |
282 apply(assumption) |
103 and "(supp ([[atom y]]lst. t2)) \<sharp>* p" |
283 apply(rule conjI) |
104 and "(atom x) \<sharp> p" |
284 apply(rule uu1) |
105 shows "Let2 x y t1 t2 = Let2 x (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)" |
285 apply(rule conjI) |
106 using assms |
286 apply(assumption) |
107 apply - |
287 apply(rule uu1) |
108 apply(drule supp_perm_eq[symmetric]) |
288 defer |
109 apply(drule supp_perm_eq[symmetric]) |
289 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
110 apply(simp only: foo.eq_iff) |
290 apply(erule exE) |
111 apply(simp only: eqvts) |
291 apply(rule assms(5)) |
112 apply simp |
292 apply(simp only:) |
113 by (metis assms(2) atom_eqvt fresh_perm) |
293 apply(simp only: foo.eq_iff) |
114 |
294 apply(insert abs_rename_list)[1] |
115 lemma strong_exhaust1_pre: |
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_prod set.simps set_append fresh_star_union, simp) |
|
304 apply(drule meta_mp) |
|
305 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union) |
|
306 apply(drule meta_mp) |
|
307 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp) |
|
308 apply(drule meta_mp) |
|
309 apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp) |
|
310 apply(erule exE)+ |
|
311 apply(rule exI)+ |
|
312 apply(perm_simp add: tt1) |
|
313 apply(rule conjI) |
|
314 prefer 2 |
|
315 apply(rule conjI) |
|
316 apply(assumption) |
|
317 apply(assumption) |
|
318 apply(simp add: fresh_star_prod) |
|
319 apply(simp add: fresh_star_def) |
|
320 sorry |
|
321 |
|
322 |
|
323 |
|
324 lemma test5: |
116 fixes c::"'a::fs" |
325 fixes c::"'a::fs" |
117 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
326 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
118 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
327 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
119 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
328 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
120 and "\<And>assn1 trm1 assn2 trm2. |
329 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" |
121 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
|
122 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
123 shows "P" |
|
124 apply(rule_tac y="y" in foo.exhaust(1)) |
|
125 apply(rule assms(1)) |
|
126 apply(assumption) |
|
127 apply(rule assms(2)) |
|
128 apply(assumption) |
|
129 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
|
130 apply(erule exE) |
|
131 apply(erule conjE) |
|
132 apply(rule assms(3)) |
|
133 apply(perm_simp) |
|
134 apply(assumption) |
|
135 apply(simp) |
|
136 apply(drule supp_perm_eq[symmetric]) |
|
137 apply(perm_simp) |
|
138 apply(simp) |
|
139 apply(rule at_set_avoiding2) |
|
140 apply(simp add: finite_supp) |
|
141 apply(simp add: finite_supp) |
|
142 apply(simp add: finite_supp) |
|
143 apply(simp add: foo.fresh fresh_star_def) |
|
144 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg1))) \<sharp>* c \<and> supp ([bn assg1]lst. trm1) \<sharp>* q") |
|
145 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg2))) \<sharp>* c \<and> supp ([bn assg2]lst. trm2) \<sharp>* q") |
|
146 apply(erule exE)+ |
|
147 apply(erule conjE)+ |
|
148 apply(rule assms(4)) |
|
149 apply(simp add: set_eqvt union_eqvt) |
|
150 apply(simp add: tt1) |
|
151 apply(simp add: fresh_star_union) |
|
152 apply(rule conjI) |
|
153 apply(assumption) |
|
154 apply(rotate_tac 3) |
|
155 apply(assumption) |
|
156 apply(simp add: foo.eq_iff) |
|
157 apply(drule supp_perm_eq[symmetric])+ |
|
158 apply(simp add: tt1 uu1) |
|
159 apply(auto)[1] |
|
160 apply(rule at_set_avoiding2) |
|
161 apply(simp add: finite_supp) |
|
162 apply(simp add: finite_supp) |
|
163 apply(simp add: finite_supp) |
|
164 apply(simp add: Abs_fresh_star) |
|
165 apply(rule at_set_avoiding2) |
|
166 apply(simp add: finite_supp) |
|
167 apply(simp add: finite_supp) |
|
168 apply(simp add: finite_supp) |
|
169 apply(simp add: Abs_fresh_star) |
|
170 apply(case_tac "name1 = name2") |
|
171 apply(subgoal_tac |
|
172 "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* c \<and> (supp (([[atom name1, atom name2]]lst. trm1), ([[atom name2]]lst. trm2))) \<sharp>* q") |
|
173 apply(erule exE)+ |
|
174 apply(erule conjE)+ |
|
175 apply(perm_simp) |
|
176 apply(rule assms(5)) |
|
177 |
|
178 apply (simp add: fresh_star_def eqvts) |
|
179 apply (simp only: supp_Pair) |
|
180 apply (simp only: fresh_star_Un_elim) |
|
181 apply (subst Let2_rename) |
|
182 apply assumption |
|
183 apply assumption |
|
184 apply (rule refl) |
|
185 apply(rule at_set_avoiding2) |
|
186 apply(simp add: finite_supp) |
|
187 apply(simp add: finite_supp) |
|
188 apply(simp add: finite_supp) |
|
189 apply clarify |
|
190 apply (simp add: fresh_star_def) |
|
191 apply (simp add: fresh_def supp_Pair supp_Abs) |
|
192 apply(subgoal_tac |
|
193 "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* c \<and> (supp ((([[atom name1, atom name2]]lst. trm1)), (atom name2))) \<sharp>* q") |
|
194 prefer 2 |
|
195 apply(rule at_set_avoiding2) |
|
196 apply(simp add: finite_supp) |
|
197 apply(simp add: finite_supp) |
|
198 apply(simp add: finite_supp) |
|
199 apply (simp add: fresh_star_def) |
|
200 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
|
201 apply(erule exE)+ |
|
202 apply(erule conjE)+ |
|
203 apply(perm_simp) |
|
204 apply(rule assms(5)) |
|
205 apply assumption |
|
206 apply clarify |
|
207 apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2) |
|
208 apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs) |
|
209 apply (simp add: fresh_star_def supp_atom) |
|
210 done |
|
211 |
|
212 lemma strong_exhaust1: |
|
213 fixes c::"'a::fs" |
|
214 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
215 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
216 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
217 and "\<And>assn1 trm1 assn2 trm2. |
|
218 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
|
219 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
330 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
220 shows "P" |
331 shows "P" |
221 apply (rule strong_exhaust1_pre) |
332 apply(rule_tac y="y" in test6) |
222 apply (erule assms) |
333 apply(erule exE)+ |
223 apply (erule assms) |
334 apply(rule assms(1)) |
224 apply (erule assms) apply assumption |
335 apply(assumption) |
225 apply (erule assms) apply assumption |
336 apply(erule exE)+ |
226 apply(case_tac "x1 = x2") |
337 apply(rule assms(2)) |
227 apply(subgoal_tac |
338 apply(assumption) |
228 "\<exists>q. (q \<bullet> {atom x1, atom x2}) \<sharp>* c \<and> (supp (([[atom x1, atom x2]]lst. trm1), ([[atom x2]]lst. trm2))) \<sharp>* q") |
339 apply(erule exE)+ |
229 apply(erule exE)+ |
340 apply(rule assms(3)) |
230 apply(erule conjE)+ |
341 apply(auto)[2] |
231 apply(perm_simp) |
342 apply(erule exE)+ |
|
343 apply(rule assms(4)) |
|
344 apply(auto)[2] |
|
345 apply(erule exE)+ |
232 apply(rule assms(5)) |
346 apply(rule assms(5)) |
233 apply assumption |
347 apply(auto)[2] |
234 apply simp |
348 done |
235 apply (rule Let2_rename) |
349 |
236 apply (simp only: supp_Pair) |
|
237 apply (simp only: fresh_star_Un_elim) |
|
238 apply (simp only: supp_Pair) |
|
239 apply (simp only: fresh_star_Un_elim) |
|
240 apply(rule at_set_avoiding2) |
|
241 apply(simp add: finite_supp) |
|
242 apply(simp add: finite_supp) |
|
243 apply(simp add: finite_supp) |
|
244 apply clarify |
|
245 apply (simp add: fresh_star_def) |
|
246 apply (simp add: fresh_def supp_Pair supp_Abs) |
|
247 |
|
248 apply(subgoal_tac |
|
249 "\<exists>q. (q \<bullet> {atom x2}) \<sharp>* c \<and> supp (([[atom x2]]lst. trm2), ([[atom x1, atom x2]]lst. trm1), (atom x1)) \<sharp>* q") |
|
250 apply(erule exE)+ |
|
251 apply(erule conjE)+ |
|
252 apply(rule assms(5)) |
|
253 apply(perm_simp) |
|
254 apply(simp (no_asm) add: fresh_star_insert) |
|
255 apply(rule conjI) |
|
256 apply (simp add: fresh_star_def) |
|
257 apply(rotate_tac 2) |
|
258 apply(simp add: fresh_star_def) |
|
259 apply(simp) |
|
260 apply (rule Let2_rename3) |
|
261 apply (simp add: supp_Pair fresh_star_union) |
|
262 apply (simp add: supp_Pair fresh_star_union) |
|
263 apply (simp add: supp_Pair fresh_star_union) |
|
264 apply clarify |
|
265 apply (simp add: fresh_star_def supp_atom) |
|
266 apply(rule at_set_avoiding2) |
|
267 apply(simp add: finite_supp) |
|
268 apply(simp add: finite_supp) |
|
269 apply(simp add: finite_supp) |
|
270 apply(simp add: fresh_star_def) |
|
271 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
|
272 done |
|
273 |
350 |
274 lemma strong_induct: |
351 lemma strong_induct: |
275 fixes c :: "'a :: fs" |
352 fixes c :: "'a :: fs" |
276 and assg :: assg and trm :: trm |
353 and assg :: assg and trm :: trm |
277 assumes a0: "\<And>name c. P1 c (Var name)" |
354 assumes a0: "\<And>name c. P1 c (Var name)" |
278 and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)" |
355 and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)" |
279 and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)" |
356 and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)" |
280 and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; \<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)" |
357 and a3: "\<And>a1 t1 a2 t2 c. |
281 and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>{atom name1, atom name2} \<sharp>* c; \<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)" |
358 \<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> |
|
359 \<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)" |
|
360 and a4: "\<And>n1 n2 t1 t2 c. |
|
361 \<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)" |
282 and a5: "\<And>c. P2 c As_Nil" |
362 and a5: "\<And>c. P2 c As_Nil" |
283 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)" |
363 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)" |
284 shows "P1 c trm" "P2 c assg" |
364 shows "P1 c trm" "P2 c assg" |
285 using assms |
365 using assms |
286 apply(induction_schema) |
366 apply(induction_schema) |
287 apply(rule_tac y="trm" and c="c" in strong_exhaust1) |
367 apply(rule_tac y="trm" and c="c" in test5) |
288 apply(simp_all)[5] |
368 apply(simp_all)[5] |
289 apply(rule_tac y="assg" in foo.exhaust(2)) |
369 apply(rule_tac y="assg" in foo.exhaust(2)) |
290 apply(simp_all)[2] |
370 apply(simp_all)[2] |
291 apply(relation "measure (sum_case (size o snd) (\<lambda>y. size (snd y)))") |
371 apply(relation "measure (sum_case (size o snd) (size o snd))") |
292 apply(simp_all add: foo.size) |
372 apply(simp_all add: foo.size) |
293 done |
373 done |
294 |
|
295 |
|
296 text {* |
|
297 tests by cu |
|
298 *} |
|
299 |
|
300 |
|
301 thm at_set_avoiding2 supp_perm_eq at_set_avoiding |
|
302 |
|
303 lemma abs_rename_set: |
|
304 fixes x::"'a::fs" |
|
305 assumes "b' \<sharp> x" "sort_of b = sort_of b'" |
|
306 shows "\<exists>y. [{b}]set. x = [{b'}]set. y" |
|
307 apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI) |
|
308 apply(subst Abs_swap1[where a="b" and b="b'"]) |
|
309 apply(simp) |
|
310 using assms |
|
311 apply(simp add: fresh_def) |
|
312 apply(perm_simp) |
|
313 using assms |
|
314 apply(simp) |
|
315 done |
|
316 |
|
317 lemma abs_rename_set1: |
|
318 fixes x::"'a::fs" |
|
319 assumes "(p \<bullet> b) \<sharp> x" |
|
320 shows "\<exists>y. [{b}]set. x = [{p \<bullet> b}]set. y" |
|
321 apply(rule_tac x="(b \<rightleftharpoons> (p \<bullet> b)) \<bullet> x" in exI) |
|
322 apply(subst Abs_swap1[where a="b" and b="p \<bullet> b"]) |
|
323 apply(simp) |
|
324 using assms |
|
325 apply(simp add: fresh_def) |
|
326 apply(perm_simp) |
|
327 apply(simp) |
|
328 done |
|
329 |
|
330 lemma yy: |
|
331 assumes "finite bs" |
|
332 and "bs \<inter> p \<bullet> bs = {}" |
|
333 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
|
334 using assms |
|
335 apply(induct) |
|
336 apply(simp add: permute_set_eq) |
|
337 apply(rule_tac x="0" in exI) |
|
338 apply(simp add: supp_perm) |
|
339 apply(perm_simp) |
|
340 apply(drule meta_mp) |
|
341 apply(auto)[1] |
|
342 apply(erule exE) |
|
343 apply(simp) |
|
344 apply(case_tac "q \<bullet> x = p \<bullet> x") |
|
345 apply(rule_tac x="q" in exI) |
|
346 apply(auto)[1] |
|
347 apply(rule_tac x="((q \<bullet> x) \<rightleftharpoons> (p \<bullet> x)) + q" in exI) |
|
348 apply(subgoal_tac "p \<bullet> x \<notin> p \<bullet> F") |
|
349 apply(subgoal_tac "q \<bullet> x \<notin> p \<bullet> F") |
|
350 apply(simp add: swap_set_not_in) |
|
351 apply(rule subset_trans) |
|
352 apply(rule supp_plus_perm) |
|
353 apply(simp) |
|
354 apply(rule conjI) |
|
355 apply(simp add: supp_swap) |
|
356 defer |
|
357 apply(auto)[1] |
|
358 apply(erule conjE)+ |
|
359 apply(drule sym) |
|
360 apply(auto)[1] |
|
361 apply(simp add: mem_permute_iff) |
|
362 apply(simp add: mem_permute_iff) |
|
363 apply(auto)[1] |
|
364 apply(simp add: supp_perm) |
|
365 apply(auto)[1] |
|
366 done |
|
367 |
|
368 lemma zz: |
|
369 fixes bs::"atom list" |
|
370 assumes "set bs \<inter> (set (p \<bullet> bs)) = {}" |
|
371 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (set (p \<bullet> bs))" |
|
372 sorry |
|
373 |
|
374 lemma abs_rename_set2: |
|
375 fixes x::"'a::fs" |
|
376 assumes "(p \<bullet> bs) \<sharp>* x" "bs \<inter> p \<bullet> bs ={}" "finite bs" |
|
377 shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" |
|
378 using yy assms |
|
379 apply - |
|
380 apply(drule_tac x="bs" in meta_spec) |
|
381 apply(drule_tac x="p" in meta_spec) |
|
382 apply(auto) |
|
383 apply(rule_tac x="q \<bullet> x" in exI) |
|
384 apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x") |
|
385 apply(simp add: permute_Abs) |
|
386 apply(rule supp_perm_eq) |
|
387 apply(rule fresh_star_supp_conv) |
|
388 apply(simp add: fresh_star_def) |
|
389 apply(simp add: Abs_fresh_iff) |
|
390 apply(auto) |
|
391 done |
|
392 |
|
393 lemma abs_rename_list: |
|
394 fixes x::"'a::fs" |
|
395 assumes "b' \<sharp> x" "sort_of b = sort_of b'" |
|
396 shows "\<exists>y. [[b]]lst. x = [[b']]lst. y" |
|
397 apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI) |
|
398 apply(subst Abs_swap2[where a="b" and b="b'"]) |
|
399 apply(simp) |
|
400 using assms |
|
401 apply(simp add: fresh_def) |
|
402 apply(perm_simp) |
|
403 using assms |
|
404 apply(simp) |
|
405 done |
|
406 |
|
407 lemma abs_rename_list2: |
|
408 fixes x::"'a::fs" |
|
409 assumes "(set (p \<bullet> bs)) \<sharp>* x" "(set bs) \<inter> (set (p \<bullet> bs)) ={}" |
|
410 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
|
411 using zz assms |
|
412 apply - |
|
413 apply(drule_tac x="bs" in meta_spec) |
|
414 apply(drule_tac x="p" in meta_spec) |
|
415 apply(auto simp add: set_eqvt) |
|
416 apply(rule_tac x="q \<bullet> x" in exI) |
|
417 apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x") |
|
418 apply(simp) |
|
419 apply(rule supp_perm_eq) |
|
420 apply(rule fresh_star_supp_conv) |
|
421 apply(simp add: fresh_star_def) |
|
422 apply(simp add: Abs_fresh_iff) |
|
423 apply(auto) |
|
424 done |
|
425 |
|
426 |
|
427 lemma test3: |
|
428 fixes c::"'a::fs" |
|
429 assumes a: "y = Let2 x1 x2 trm1 trm2" |
|
430 and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P" |
|
431 shows "P" |
|
432 using b[simplified a] |
|
433 apply - |
|
434 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)") |
|
435 apply(erule exE) |
|
436 apply(perm_simp) |
|
437 apply(simp only: foo.eq_iff) |
|
438 apply(drule_tac x="q \<bullet> x1" in spec) |
|
439 apply(drule_tac x="q \<bullet> x2" in spec) |
|
440 apply(simp) |
|
441 apply(erule mp) |
|
442 apply(rule conjI) |
|
443 apply(simp add: fresh_star_prod) |
|
444 apply(rule conjI) |
|
445 apply(simp add: atom_eqvt[symmetric]) |
|
446 apply(subst (2) permute_list.simps(1)[where p="q", symmetric]) |
|
447 apply(subst permute_list.simps(2)[symmetric]) |
|
448 apply(subst permute_list.simps(2)[symmetric]) |
|
449 apply(rule abs_rename_list2) |
|
450 apply(simp add: atom_eqvt fresh_star_prod) |
|
451 apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base) |
|
452 apply(simp add: atom_eqvt[symmetric]) |
|
453 apply(subst (2) permute_list.simps(1)[where p="q", symmetric]) |
|
454 apply(subst permute_list.simps(2)[symmetric]) |
|
455 apply(rule abs_rename_list2) |
|
456 apply(simp add: atom_eqvt fresh_star_prod) |
|
457 apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base) |
|
458 apply(simp add: atom_eqvt[symmetric]) |
|
459 apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base) |
|
460 sorry |
|
461 |
|
462 lemma test4: |
|
463 fixes c::"'a::fs" |
|
464 assumes a: "y = Let2 x1 x2 trm1 trm2" |
|
465 and b: "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
466 shows "P" |
|
467 apply(rule test3) |
|
468 apply(rule a) |
|
469 using b |
|
470 apply(auto) |
|
471 done |
|
472 |
|
473 lemma test5: |
|
474 fixes c::"'a::fs" |
|
475 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
476 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
477 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
478 and "\<And>assn1 trm1 assn2 trm2. |
|
479 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
|
480 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
481 shows "P" |
|
482 apply(rule_tac y="y" in foo.exhaust(1)) |
|
483 apply (erule assms) |
|
484 apply (erule assms) |
|
485 prefer 3 |
|
486 apply(erule test4[where c="c"]) |
|
487 apply (rule assms(5)) |
|
488 apply assumption |
|
489 apply(simp) |
|
490 oops |
|
491 |
|
492 |
374 |
493 end |
375 end |
494 |
376 |
495 |
377 |
496 |
378 |