155 done |
155 done |
156 |
156 |
157 |
157 |
158 lemma strong_exhaust1: |
158 lemma strong_exhaust1: |
159 fixes c::"'a::fs" |
159 fixes c::"'a::fs" |
160 assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" |
160 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
161 and "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P" |
161 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
162 and "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
162 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
163 and "\<And>assn trm ca. \<lbrakk>set (bn1 assn) \<sharp>* ca; c = ca; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
163 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
164 and "\<And>assn trm ca. \<lbrakk>set (bn2 assn) \<sharp>* ca; c = ca; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
164 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
165 and "\<And>assn trm ca. \<lbrakk>set (bn3 assn) \<sharp>* ca; c = ca; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
165 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
166 shows "P" |
166 shows "P" |
167 apply(rule_tac y="y" in foo.exhaust(1)) |
167 apply(rule_tac y="y" in foo.exhaust(1)) |
168 apply(rule assms(1)) |
168 apply(rule assms(1)) |
169 apply(auto)[2] |
169 apply(assumption) |
170 apply(rule assms(2)) |
170 apply(rule assms(2)) |
171 apply(auto)[2] |
171 apply(assumption) |
172 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
172 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
173 apply(erule exE) |
173 apply(erule exE) |
174 apply(erule conjE) |
174 apply(erule conjE) |
175 apply(rule assms(3)) |
175 apply(rule assms(3)) |
176 apply(perm_simp) |
176 apply(perm_simp) |
177 apply(assumption) |
177 apply(assumption) |
178 apply(rule refl) |
178 apply(drule supp_perm_eq[symmetric]) |
179 apply(drule supp_perm_eq[symmetric]) |
179 apply(perm_simp) |
180 apply(simp) |
180 apply(simp) |
181 apply(rule at_set_avoiding2) |
181 apply(rule at_set_avoiding2) |
182 apply(simp add: finite_supp) |
182 apply(simp add: finite_supp) |
183 apply(simp add: finite_supp) |
183 apply(simp add: finite_supp) |
184 apply(simp add: finite_supp) |
184 apply(simp add: finite_supp) |
185 apply(simp add: foo.fresh fresh_star_def) |
185 apply(simp add: foo.fresh fresh_star_def) |
186 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q") |
186 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q") |
187 apply(erule exE) |
187 apply(erule exE) |
188 apply(erule conjE) |
188 apply(erule conjE) |
189 apply(rule assms(4)) |
189 apply(rule assms(4)) |
190 apply(simp add: set_eqvt) |
190 apply(perm_simp add: tt1) |
191 apply(simp add: tt1) |
191 apply(assumption) |
192 apply(rule refl) |
192 apply(drule supp_perm_eq[symmetric]) |
193 apply(simp) |
193 apply(simp add: foo.eq_iff) |
194 apply(simp add: foo.eq_iff) |
|
195 apply(drule supp_perm_eq[symmetric]) |
|
196 apply(simp) |
|
197 apply(simp add: tt1 uu1) |
194 apply(simp add: tt1 uu1) |
198 apply(rule at_set_avoiding2) |
195 apply(rule at_set_avoiding2) |
199 apply(simp add: finite_supp) |
196 apply(simp add: finite_supp) |
200 apply(simp add: finite_supp) |
197 apply(simp add: finite_supp) |
201 apply(simp add: finite_supp) |
198 apply(simp add: finite_supp) |
234 apply(simp add: finite_supp) |
227 apply(simp add: finite_supp) |
235 apply(simp add: finite_supp) |
228 apply(simp add: finite_supp) |
236 apply(simp add: Abs_fresh_star) |
229 apply(simp add: Abs_fresh_star) |
237 done |
230 done |
238 |
231 |
239 thm foo.exhaust |
|
240 |
|
241 lemma strong_exhaust2: |
232 lemma strong_exhaust2: |
242 assumes "\<And>x y t ca. \<lbrakk>c = ca; as = As x y t\<rbrakk> \<Longrightarrow> P" |
233 assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" |
243 shows "P" |
234 shows "P" |
244 apply(rule_tac y="as" in foo.exhaust(2)) |
235 apply(rule_tac y="as" in foo.exhaust(2)) |
245 apply(rule assms(1)) |
236 apply(rule assms(1)) |
246 apply(auto)[2] |
237 apply(assumption) |
247 done |
238 done |
248 |
239 |
249 |
240 |
250 lemma |
241 lemma |
251 fixes t::trm |
242 fixes t::trm |
259 and a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)" |
250 and a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)" |
260 and a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
251 and a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
261 shows "P1 c t" "P2 c as" |
252 shows "P1 c t" "P2 c as" |
262 using assms |
253 using assms |
263 apply(induction_schema) |
254 apply(induction_schema) |
264 apply(rule_tac y="t" in strong_exhaust1) |
255 apply(rule_tac y="t" and c="c" in strong_exhaust1) |
265 apply(blast) |
256 apply(simp_all)[6] |
266 apply(blast) |
|
267 apply(blast) |
|
268 apply(blast) |
|
269 apply(blast) |
|
270 apply(blast) |
|
271 apply(rule_tac as="as" in strong_exhaust2) |
257 apply(rule_tac as="as" in strong_exhaust2) |
272 apply(blast) |
258 apply(simp) |
273 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
259 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
274 apply(auto)[1] |
|
275 apply(simp_all add: foo.size) |
260 apply(simp_all add: foo.size) |
276 done |
261 done |
277 |
262 |
278 end |
263 end |
279 |
264 |