378 lemma rfv_trm_rsp[quot_respect]: |
378 lemma rfv_trm_rsp[quot_respect]: |
379 "(atrm ===> op =) rfv_trm rfv_trm" |
379 "(atrm ===> op =) rfv_trm rfv_trm" |
380 by (simp add: alpha_rfv) |
380 by (simp add: alpha_rfv) |
381 |
381 |
382 thm kind_ty_trm.induct |
382 thm kind_ty_trm.induct |
383 |
383 lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted] |
384 lemma KIND_TY_TRM_induct: |
|
385 fixes P10 :: "KIND \<Rightarrow> bool" and P20 :: "TY \<Rightarrow> bool" and P30 :: "TRM \<Rightarrow> bool" |
|
386 shows |
|
387 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
|
388 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
|
389 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
|
390 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
|
391 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
|
392 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm" |
|
393 by (lifting kind_ty_trm.induct) |
|
394 |
384 |
395 thm kind_ty_trm.inducts |
385 thm kind_ty_trm.inducts |
396 |
386 lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted] |
397 lemma KIND_TY_TRM_inducts: |
|
398 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
|
399 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
|
400 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
|
401 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
|
402 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
|
403 \<Longrightarrow> P10 kind" |
|
404 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
|
405 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
|
406 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
|
407 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
|
408 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
|
409 \<Longrightarrow> P20 ty" |
|
410 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident); |
|
411 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm); |
|
412 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident); |
|
413 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2); |
|
414 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk> |
|
415 \<Longrightarrow> P30 trm" |
|
416 by (lifting kind_ty_trm.inducts) |
|
417 |
387 |
418 instantiation KIND and TY and TRM :: pt |
388 instantiation KIND and TY and TRM :: pt |
419 begin |
389 begin |
420 |
390 |
421 quotient_definition |
391 quotient_definition |
431 quotient_definition |
401 quotient_definition |
432 "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM" |
402 "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM" |
433 as |
403 as |
434 "permute :: perm \<Rightarrow> trm \<Rightarrow> trm" |
404 "permute :: perm \<Rightarrow> trm \<Rightarrow> trm" |
435 |
405 |
436 lemma permute_ktt[simp]: |
|
437 shows "pi \<bullet> TYP = TYP" |
|
438 and "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)" |
|
439 and "pi \<bullet> (TCONST i) = TCONST (pi \<bullet> i)" |
|
440 and "pi \<bullet> (TAPP A M) = TAPP (pi \<bullet> A) (pi \<bullet> M)" |
|
441 and "pi \<bullet> (TPI A x B) = TPI (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> B)" |
|
442 and "pi \<bullet> (CONS i) = CONS (pi \<bullet> i)" |
|
443 and "pi \<bullet> (VAR x) = VAR (pi \<bullet> x)" |
|
444 and "pi \<bullet> (APP M N) = APP (pi \<bullet> M) (pi \<bullet> N)" |
|
445 and "pi \<bullet> (LAM A x M) = LAM (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> M)" |
|
446 apply (lifting permute_kind_permute_ty_permute_trm.simps) |
|
447 done |
|
448 |
|
449 lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z" |
406 lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z" |
450 apply (induct rule: KIND_TY_TRM_induct) |
407 apply (induct rule: KIND_TY_TRM_induct) |
451 apply simp_all |
408 apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted]) |
452 done |
409 done |
453 |
410 |
454 lemma perm_add_ok: |
411 lemma perm_add_ok: |
455 "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))" |
412 "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))" |
456 "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)" |
413 "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)" |
457 "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)" |
414 "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)" |
458 apply(induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts) |
415 apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts) |
459 apply (simp_all) |
416 apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted]) |
460 done |
417 done |
461 |
418 |
462 instance |
419 instance |
463 apply default |
420 apply default |
464 apply (simp_all add: perm_zero_ok perm_add_ok) |
421 apply (simp_all add: perm_zero_ok perm_add_ok) |
465 done |
422 done |
466 |
423 |
467 end |
424 end |
468 |
425 |
469 lemma AKIND_ATY_ATRM_inducts: |
426 lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted] |
470 "\<lbrakk>z1 = z2; P1 TYP TYP; |
427 |
471 \<And>A A' a K b K'. |
428 lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
472 \<lbrakk>A = A'; P2 A A'; |
429 |
473 \<exists>pi. ({atom a}, |
430 lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
474 K) \<approx>gen (\<lambda>x1 x2. |
431 |
475 x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk> |
432 lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.simps[quot_lifted] |
476 \<Longrightarrow> P1 (KPI A a K) (KPI A' b K'); |
433 |
477 \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j); |
434 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
478 \<And>A A' M M'. |
|
479 \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk> |
|
480 \<Longrightarrow> P2 (TAPP A M) (TAPP A' M'); |
|
481 \<And>A A' a B b B'. |
|
482 \<lbrakk>A = A'; P2 A A'; |
|
483 \<exists>pi. ({atom a}, |
|
484 B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk> |
|
485 \<Longrightarrow> P2 (TPI A a B) (TPI A' b B'); |
|
486 \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j); |
|
487 \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y); |
|
488 \<And>M M' N N'. |
|
489 \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk> |
|
490 \<Longrightarrow> P3 (APP M N) (APP M' N'); |
|
491 \<And>A A' a M b M'. |
|
492 \<lbrakk>A = A'; P2 A A'; |
|
493 \<exists>pi. ({atom a}, |
|
494 M) \<approx>gen (\<lambda>x1 x2. |
|
495 x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk> |
|
496 \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk> |
|
497 \<Longrightarrow> P1 z1 z2" |
|
498 "\<lbrakk>z3 = z4; P1 TYP TYP; |
|
499 \<And>A A' a K b K'. |
|
500 \<lbrakk>A = A'; P2 A A'; |
|
501 \<exists>pi. ({atom a}, |
|
502 K) \<approx>gen (\<lambda>x1 x2. |
|
503 x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk> |
|
504 \<Longrightarrow> P1 (KPI A a K) (KPI A' b K'); |
|
505 \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j); |
|
506 \<And>A A' M M'. |
|
507 \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk> |
|
508 \<Longrightarrow> P2 (TAPP A M) (TAPP A' M'); |
|
509 \<And>A A' a B b B'. |
|
510 \<lbrakk>A = A'; P2 A A'; |
|
511 \<exists>pi. ({atom a}, |
|
512 B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk> |
|
513 \<Longrightarrow> P2 (TPI A a B) (TPI A' b B'); |
|
514 \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j); |
|
515 \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y); |
|
516 \<And>M M' N N'. |
|
517 \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk> |
|
518 \<Longrightarrow> P3 (APP M N) (APP M' N'); |
|
519 \<And>A A' a M b M'. |
|
520 \<lbrakk>A = A'; P2 A A'; |
|
521 \<exists>pi. ({atom a}, |
|
522 M) \<approx>gen (\<lambda>x1 x2. |
|
523 x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk> |
|
524 \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk> |
|
525 \<Longrightarrow> P2 z3 z4" |
|
526 "\<lbrakk>z5 = z6; P1 TYP TYP; |
|
527 \<And>A A' a K b K'. |
|
528 \<lbrakk>A = A'; P2 A A'; |
|
529 \<exists>pi. ({atom a}, |
|
530 K) \<approx>gen (\<lambda>x1 x2. |
|
531 x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk> |
|
532 \<Longrightarrow> P1 (KPI A a K) (KPI A' b K'); |
|
533 \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j); |
|
534 \<And>A A' M M'. |
|
535 \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk> |
|
536 \<Longrightarrow> P2 (TAPP A M) (TAPP A' M'); |
|
537 \<And>A A' a B b B'. |
|
538 \<lbrakk>A = A'; P2 A A'; |
|
539 \<exists>pi. ({atom a}, |
|
540 B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk> |
|
541 \<Longrightarrow> P2 (TPI A a B) (TPI A' b B'); |
|
542 \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j); |
|
543 \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y); |
|
544 \<And>M M' N N'. |
|
545 \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk> |
|
546 \<Longrightarrow> P3 (APP M N) (APP M' N'); |
|
547 \<And>A A' a M b M'. |
|
548 \<lbrakk>A = A'; P2 A A'; |
|
549 \<exists>pi. ({atom a}, |
|
550 M) \<approx>gen (\<lambda>x1 x2. |
|
551 x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk> |
|
552 \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk> |
|
553 \<Longrightarrow> P3 z5 z6" |
|
554 unfolding alpha_gen |
|
555 apply (lifting akind_aty_atrm.inducts[unfolded alpha_gen]) |
|
556 done |
|
557 |
|
558 thm akind_aty_atrm_inj |
|
559 lemma KIND_TY_TRM_INJECT: |
|
560 "(TYP) = (TYP) = True" |
|
561 "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. ({atom x}, K) \<approx>gen (op =) fv_kind pi ({atom x'}, K')))" |
|
562 "(TCONST i) = (TCONST j) = (i = j)" |
|
563 "(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = M')" |
|
564 "(TPI A x B) = (TPI A' x' B') = (A = A' \<and> (\<exists>pi. ({atom x}, B) \<approx>gen (op =) fv_ty pi ({atom x'}, B')))" |
|
565 "(CONS i) = (CONS j) = (i = j)" |
|
566 "(VAR x) = (VAR y) = (x = y)" |
|
567 "(APP M N) = (APP M' N') = (M = M' \<and> N = N')" |
|
568 "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. ({atom x}, M) \<approx>gen (op =) fv_trm pi ({atom x'}, M')))" |
|
569 unfolding alpha_gen |
|
570 by (lifting akind_aty_atrm_inj[unfolded alpha_gen]) |
|
571 |
|
572 lemma fv_kind_ty_trm: |
|
573 "fv_kind TYP = {}" |
|
574 "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})" |
|
575 "fv_ty (TCONST i) = {atom i}" |
|
576 "fv_ty (TAPP A M) = fv_ty A \<union> fv_trm M" |
|
577 "fv_ty (TPI A x B) = fv_ty A \<union> (fv_ty B - {atom x})" |
|
578 "fv_trm (CONS i) = {atom i}" |
|
579 "fv_trm (VAR x) = {atom x}" |
|
580 "fv_trm (APP M N) = fv_trm M \<union> fv_trm N" |
|
581 "fv_trm (LAM A x M) = fv_ty A \<union> (fv_trm M - {atom x})" |
|
582 by(lifting rfv_kind_rfv_ty_rfv_trm.simps) |
|
583 |
|
584 lemma fv_eqvt: |
|
585 "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)" |
|
586 "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)" |
|
587 "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)" |
|
588 by(lifting rfv_eqvt) |
|
589 |
435 |
590 lemma supp_kind_ty_trm_easy: |
436 lemma supp_kind_ty_trm_easy: |
591 "supp TYP = {}" |
437 "supp TYP = {}" |
592 "supp (TCONST i) = {atom i}" |
438 "supp (TCONST i) = {atom i}" |
593 "supp (TAPP A M) = supp A \<union> supp M" |
439 "supp (TAPP A M) = supp A \<union> supp M" |