110 apply(simp only: foo.eq_iff) |
110 apply(simp only: foo.eq_iff) |
111 apply(simp only: eqvts) |
111 apply(simp only: eqvts) |
112 apply simp |
112 apply simp |
113 by (metis assms(2) atom_eqvt fresh_perm) |
113 by (metis assms(2) atom_eqvt fresh_perm) |
114 |
114 |
115 lemma strong_exhaust1: |
115 lemma strong_exhaust1_pre: |
116 fixes c::"'a::fs" |
116 fixes c::"'a::fs" |
117 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
117 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
118 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
118 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" |
119 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
120 and "\<And>assn1 trm1 assn2 trm2. |
120 and "\<And>assn1 trm1 assn2 trm2. |
207 apply (rule_tac x="name1" and y="name2" and ?t1.0="trm1" and ?t2.0="trm2" in Let2_rename2) |
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) |
208 apply (simp_all add: fresh_star_Un_elim supp_Pair supp_Abs) |
209 apply (simp add: fresh_star_def supp_atom) |
209 apply (simp add: fresh_star_def supp_atom) |
210 done |
210 done |
211 |
211 |
212 lemma strong_exhaust2: |
212 lemma strong_exhaust1: |
213 fixes c::"'a::fs" |
213 fixes c::"'a::fs" |
214 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
214 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
215 and "\<And>trm1 trm2. y = App trm1 trm2 \<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" |
216 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
217 and "\<And>assn1 trm1 assn2 trm2. |
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" |
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" |
219 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" |
220 shows "P" |
221 apply (rule strong_exhaust1) |
221 apply (rule strong_exhaust1_pre) |
222 apply (erule assms) |
222 apply (erule assms) |
223 apply (erule assms) |
223 apply (erule assms) |
224 apply (erule assms) apply assumption |
224 apply (erule assms) apply assumption |
225 apply (erule assms) apply assumption |
225 apply (erule assms) apply assumption |
226 apply(case_tac "x1 = x2") |
226 apply(case_tac "x1 = x2") |
269 apply(simp add: finite_supp) |
269 apply(simp add: finite_supp) |
270 apply(simp add: fresh_star_def) |
270 apply(simp add: fresh_star_def) |
271 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
271 apply (simp add: fresh_def supp_Pair supp_Abs supp_atom) |
272 done |
272 done |
273 |
273 |
|
274 lemma strong_induct: |
|
275 fixes c :: "'a :: fs" |
|
276 and assg :: assg and trm :: trm |
|
277 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)" |
|
279 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)" |
|
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)" |
|
282 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)" |
|
284 shows "P1 c trm" "P2 c assg" |
|
285 using assms |
|
286 apply(induction_schema) |
|
287 apply(rule_tac y="trm" and c="c" in strong_exhaust1) |
|
288 apply(simp_all)[5] |
|
289 apply(rule_tac y="assg" in foo.exhaust(2)) |
|
290 apply(simp_all)[2] |
|
291 apply(relation "measure (sum_case (size o snd) (\<lambda>y. size (snd y)))") |
|
292 apply(simp_all add: foo.size) |
|
293 done |
|
294 |
|
295 |
274 end |
296 end |
275 |
297 |
276 |
298 |
277 |
299 |