321 apply (induct x rule: inducts(9)) |
321 apply (induct x rule: inducts(9)) |
322 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
322 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
323 apply (simp add: finb1 finb2 finb3) |
323 apply (simp add: finb1 finb2 finb3) |
324 done |
324 done |
325 |
325 |
326 lemma strong_inudction_principle: |
326 thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct |
|
327 |
|
328 lemma strong_induction_principle: |
327 assumes a01: "\<And>b. P1 b KStar" |
329 assumes a01: "\<And>b. P1 b KStar" |
328 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
330 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
329 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
331 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
330 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
332 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
331 and a05: "\<And>string b. P3 b (TC string)" |
333 and a05: "\<And>string b. P3 b (TC string)" |
332 and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)" |
334 and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)" |
333 and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)" |
335 and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)" |
334 and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk> |
336 and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk> |
335 \<Longrightarrow> P3 b (TAll tvar tkind ty)" |
337 \<Longrightarrow> P3 b (TAll tvar tkind ty)" |
336 and a09: "\<And>ty1 ty2 ty3 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2; \<And>c. P3 c ty3\<rbrakk> \<Longrightarrow> P3 b (TEq ty1 ty2 ty3)" |
338 and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)" |
337 and a10: "\<And>b. P4 b TvsNil" |
339 and a10: "\<And>b. P4 b TsNil" |
338 and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TvsCons ty ty_lst)" |
340 and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)" |
339 and a12: "\<And>string b. P5 b (CC string)" |
341 and a12: "\<And>string b. P5 b (CVar string)" |
|
342 and a12a:"\<And>str b. P5 b (CConst str)" |
340 and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)" |
343 and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)" |
341 and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)" |
344 and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)" |
342 and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk> |
345 and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk> |
343 \<Longrightarrow> P5 b (CAll tvar ckind co)" |
346 \<Longrightarrow> P5 b (CAll tvar ckind co)" |
344 and a16: "\<And>co1 co2 co3 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2; \<And>c. P5 c co3\<rbrakk> \<Longrightarrow> P5 b (CEq co1 co2 co3)" |
347 and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)" |
345 and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)" |
348 and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)" |
|
349 and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)" |
346 and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)" |
350 and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)" |
|
351 and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)" |
347 and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)" |
352 and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)" |
348 and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)" |
353 and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)" |
349 and a21: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSim co)" |
354 and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)" |
350 and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)" |
355 and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)" |
351 and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)" |
356 and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)" |
352 and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)" |
357 and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)" |
353 and a25: "\<And>b. P6 b CsNil" |
358 and a25: "\<And>b. P6 b CsNil" |
354 and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)" |
359 and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)" |
355 and a27: "\<And>var b. P7 b (Var var)" |
360 and a27: "\<And>var b. P7 b (Var var)" |
356 and a28: "\<And>string b. P7 b (C string)" |
361 and a28: "\<And>string b. P7 b (K string)" |
357 and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
362 and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
358 \<Longrightarrow> P7 b (LAMT tvar tkind trm)" |
363 \<Longrightarrow> P7 b (LAMT tvar tkind trm)" |
359 and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
364 and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk> |
360 \<Longrightarrow> P7 b (LAMC tvar ckind trm)" |
365 \<Longrightarrow> P7 b (LAMC tvar ckind trm)" |
361 and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)" |
366 and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)" |
|
367 and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)" |
362 and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)" |
368 and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)" |
363 and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)" |
369 and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)" |
364 and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk> |
370 and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk> |
365 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
371 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
366 and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)" |
372 and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)" |
367 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
373 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
368 and a37: "\<And>b. P8 b ANil" |
374 and a37: "\<And>b. P8 b ANil" |
369 and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk> |
375 and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk> |
370 \<Longrightarrow> P8 b (ACons pat trm assoc_lst)" |
376 \<Longrightarrow> P8 b (ACons pat trm assoc_lst)" |
371 and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk> |
377 and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk> |
372 \<Longrightarrow> P9 b (K string tvars cvars vars)" |
378 \<Longrightarrow> P9 b (Kpat string tvars cvars vars)" |
373 and a40: "\<And>b. P10 b VsNil" |
379 and a40: "\<And>b. P10 b VsNil" |
374 and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)" |
380 and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)" |
375 and a42: "\<And>b. P11 b TvsNil" |
381 and a42: "\<And>b. P11 b TvsNil" |
376 and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk> |
382 and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk> |
377 \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)" |
383 \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)" |
435 apply (simp add: fresh_def) |
441 apply (simp add: fresh_def) |
436 apply (simp only: supp_abs eqvts) |
442 apply (simp only: supp_abs eqvts) |
437 apply blast |
443 apply blast |
438 |
444 |
439 (* GOAL2 *) |
445 (* GOAL2 *) |
440 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> e \<and> |
446 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and> |
441 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> co)) \<sharp>* pa)") |
447 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)") |
442 apply clarify |
448 apply clarify |
443 apply (simp only: perm) |
449 apply (simp only: perm) |
444 apply(rule_tac t="CAll (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> co)" |
450 apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)" |
445 and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
451 and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
446 apply (simp only: eq_iff) |
452 apply (simp only: eq_iff) |
447 apply (rule_tac x="-pa" in exI) |
453 apply (rule_tac x="-pa" in exI) |
448 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
454 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
449 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}" |
455 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}" |
450 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst) |
456 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst) |
451 apply (simp add: eqvts) |
457 apply (simp add: eqvts) |
452 apply (simp add: eqvts[symmetric]) |
458 apply (simp add: eqvts[symmetric]) |
453 apply (rule conjI) |
459 apply (rule conjI) |
454 apply (rule supp_perm_eq) |
460 apply (rule supp_perm_eq) |
455 apply (simp add: eqvts) |
461 apply (simp add: eqvts) |
516 apply (simp add: fresh_def) |
522 apply (simp add: fresh_def) |
517 apply (simp only: supp_abs eqvts) |
523 apply (simp only: supp_abs eqvts) |
518 apply blast |
524 apply blast |
519 |
525 |
520 (* GOAL4 a copy-and-paste *) |
526 (* GOAL4 a copy-and-paste *) |
521 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
527 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and> |
522 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
528 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)") |
523 apply clarify |
529 apply clarify |
524 apply (simp only: perm) |
530 apply (simp only: perm) |
525 apply(rule_tac t="LAMC (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> trm)" |
531 apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)" |
526 and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
532 and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
527 apply (simp only: eq_iff) |
533 apply (simp only: eq_iff) |
528 apply (rule_tac x="-pa" in exI) |
534 apply (rule_tac x="-pa" in exI) |
529 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
535 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
530 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
536 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}" |
531 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
537 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst) |
532 apply (simp add: eqvts) |
538 apply (simp add: eqvts) |
533 apply (simp add: eqvts[symmetric]) |
539 apply (simp add: eqvts[symmetric]) |
534 apply (rule conjI) |
540 apply (rule conjI) |
535 apply (rule supp_perm_eq) |
541 apply (rule supp_perm_eq) |
536 apply (simp add: eqvts) |
542 apply (simp add: eqvts) |