420 qed |
420 qed |
421 |
421 |
422 section {* Two proofs for reflexivity of subtyping *} |
422 section {* Two proofs for reflexivity of subtyping *} |
423 |
423 |
424 lemma subtype_reflexivity: |
424 lemma subtype_reflexivity: |
425 shows "\<turnstile> \<Gamma> ok \<longrightarrow> T closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T <: T" |
425 assumes a: "\<turnstile> \<Gamma> ok" |
426 proof(nominal_induct T fresh: \<Gamma> rule: ty.induct_unsafe) |
426 and b: "T closed_in \<Gamma>" |
|
427 shows "\<Gamma> \<turnstile> T <: T" |
|
428 using a b |
|
429 proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe) |
427 case (TAll X T1 T2) |
430 case (TAll X T1 T2) |
428 have i1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<longrightarrow> T1 closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T1 <: T1" by fact |
431 have i1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T1 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T1 <: T1" by fact |
429 have i2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<longrightarrow> T2 closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> T2 <: T2" by fact |
432 have i2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T2 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T2 <: T2" by fact |
430 have f: "X\<sharp>\<Gamma>" by fact |
433 have f: "X\<sharp>\<Gamma>" by fact |
431 show "\<turnstile> \<Gamma> ok \<longrightarrow> (\<forall>[X<:T2].T1) closed_in \<Gamma> \<longrightarrow> \<Gamma> \<turnstile> \<forall>[X<:T2].T1 <: \<forall>[X<:T2].T1" |
434 have "(\<forall>[X<:T2].T1) closed_in \<Gamma>" by fact |
432 proof (intro strip) |
435 hence b1: "T2 closed_in \<Gamma>" and b2: "T1 closed_in ((X,T2)#\<Gamma>)" |
433 assume "(\<forall>[X<:T2].T1) closed_in \<Gamma>" |
|
434 hence b1: "T2 closed_in \<Gamma>" and b2: "T1 closed_in ((X,T2)#\<Gamma>)" |
|
435 by (auto simp add: closed_in_def ty.supp abs_supp) |
436 by (auto simp add: closed_in_def ty.supp abs_supp) |
436 assume c1: "\<turnstile> \<Gamma> ok" |
437 have c1: "\<turnstile> \<Gamma> ok" by fact |
437 hence c2: "\<turnstile> ((X,T2)#\<Gamma>) ok" using b1 f by force |
438 hence c2: "\<turnstile> ((X,T2)#\<Gamma>) ok" using b1 f by force |
438 have "\<Gamma> \<turnstile> T2 <: T2" using i2 b1 c1 by simp |
439 have "\<Gamma> \<turnstile> T2 <: T2" using i2 b1 c1 by simp |
439 moreover |
440 moreover |
440 have "((X,T2)#\<Gamma>) \<turnstile> T1 <: T1" using i1 b2 c2 by simp |
441 have "((X,T2)#\<Gamma>) \<turnstile> T1 <: T1" using i1 b2 c2 by simp |
441 ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T2].T1 <: \<forall>[X<:T2].T1" using f by force |
442 ultimately show "\<Gamma> \<turnstile> \<forall>[X<:T2].T1 <: \<forall>[X<:T2].T1" using f by force |
442 qed |
|
443 qed (auto simp add: closed_in_def ty.supp supp_atm) |
443 qed (auto simp add: closed_in_def ty.supp supp_atm) |
444 |
444 |
445 lemma subtype_reflexivity: |
445 lemma subtype_reflexivity: |
446 assumes a: "\<turnstile> \<Gamma> ok" |
446 assumes a: "\<turnstile> \<Gamma> ok" |
447 and b: "T closed_in \<Gamma>" |
447 and b: "T closed_in \<Gamma>" |
448 shows "\<Gamma> \<turnstile> T <: T" |
448 shows "\<Gamma> \<turnstile> T <: T" |
449 using a b |
449 using a b |
450 apply(nominal_induct T fresh: \<Gamma> rule: ty.induct_unsafe) |
450 apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe) |
451 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm) |
451 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm) |
452 (* too bad that this cannot be found automatically *) |
452 (* too bad that this cannot be found automatically *) |
453 apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec) |
453 apply(drule_tac x="(tyvrs, ty2)#\<Gamma>" in meta_spec) |
454 apply(force simp add: closed_in_def) |
454 apply(force simp add: closed_in_def) |
455 done |
455 done |
591 shows "T closed_in \<Delta>" |
591 shows "T closed_in \<Delta>" |
592 using a1 a2 |
592 using a1 a2 |
593 by (auto dest: extends_domain simp add: closed_in_def) |
593 by (auto dest: extends_domain simp add: closed_in_def) |
594 |
594 |
595 lemma weakening: |
595 lemma weakening: |
596 assumes a1: "\<Gamma> \<turnstile> S <: T" |
596 assumes a: "\<Gamma> \<turnstile> S <: T" |
597 shows "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" |
597 and b: "\<turnstile> \<Delta> ok" |
598 using a1 |
598 and c: "\<Delta> extends \<Gamma>" |
599 proof (nominal_induct \<Gamma> S T fresh: \<Delta> rule: subtype_of_rel_induct) |
599 shows "\<Delta> \<turnstile> S <: T" |
|
600 using a b c |
|
601 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_rel_induct) |
600 case (S_Top \<Gamma> S) |
602 case (S_Top \<Gamma> S) |
601 have lh_drv_prem: "S closed_in \<Gamma>" by fact |
603 have lh_drv_prem: "S closed_in \<Gamma>" by fact |
602 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: Top" |
604 have "\<turnstile> \<Delta> ok" by fact |
603 proof (intro strip) |
605 moreover |
604 assume "\<turnstile> \<Delta> ok" |
606 have "\<Delta> extends \<Gamma>" by fact |
605 moreover |
607 hence "S closed_in \<Delta>" using lh_drv_prem by (rule_tac extends_closed) |
606 assume "\<Delta> extends \<Gamma>" |
608 ultimately show "\<Delta> \<turnstile> S <: Top" by force |
607 hence "S closed_in \<Delta>" using lh_drv_prem by (rule_tac extends_closed) |
|
608 ultimately show "\<Delta> \<turnstile> S <: Top" by force |
|
609 qed |
|
610 next |
609 next |
611 case (S_Var \<Gamma> X S T) |
610 case (S_Var \<Gamma> X S T) |
612 have lh_drv_prem: "(X,S) \<in> set \<Gamma>" by fact |
611 have lh_drv_prem: "(X,S) \<in> set \<Gamma>" by fact |
613 have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" by fact |
612 have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> S <: T" by fact |
614 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> TyVar X <: T" |
613 have ok: "\<turnstile> \<Delta> ok" by fact |
615 proof (intro strip) |
614 have extends: "\<Delta> extends \<Gamma>" by fact |
616 assume ok: "\<turnstile> \<Delta> ok" |
615 have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp add: extends_def) |
617 and extends: "\<Delta> extends \<Gamma>" |
616 moreover |
618 have "(X,S) \<in> set \<Delta>" using lh_drv_prem extends by (simp add: extends_def) |
617 have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp |
619 moreover |
618 ultimately show "\<Delta> \<turnstile> TyVar X <: T" using ok by force |
620 have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp |
|
621 ultimately show "\<Delta> \<turnstile> TyVar X <: T" using ok by force |
|
622 qed |
|
623 next |
619 next |
624 case (S_Refl \<Gamma> X) |
620 case (S_Refl \<Gamma> X) |
625 have lh_drv_prem: "X \<in> domain \<Gamma>" by fact |
621 have lh_drv_prem: "X \<in> domain \<Gamma>" by fact |
626 show ?case |
622 have "\<turnstile> \<Delta> ok" by fact |
627 proof (intro strip) |
623 moreover |
628 assume "\<turnstile> \<Delta> ok" |
624 have "\<Delta> extends \<Gamma>" by fact |
629 moreover |
625 hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain) |
630 assume "\<Delta> extends \<Gamma>" |
626 ultimately show "\<Delta> \<turnstile> TyVar X <: TyVar X" by force |
631 hence "X \<in> domain \<Delta>" using lh_drv_prem by (force dest: extends_domain) |
|
632 ultimately show "\<Delta> \<turnstile> TyVar X <: TyVar X" by force |
|
633 qed |
|
634 next |
627 next |
635 case S_Arrow thus ?case by force |
628 case S_Arrow thus ?case by force |
636 next |
629 next |
637 case (S_All \<Gamma> X S1 S2 T1 T2) |
630 case (S_All \<Gamma> X S1 S2 T1 T2) |
638 have fresh: "X\<sharp>\<Delta>" by fact |
631 have fresh: "X\<sharp>\<Delta>" by fact |
639 have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact |
632 have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact |
640 have ih2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact |
633 have ih2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact |
641 have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact |
634 have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact |
642 hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
635 hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
643 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" |
636 have ok: "\<turnstile> \<Delta> ok" by fact |
644 proof (intro strip) |
637 have extends: "\<Delta> extends \<Gamma>" by fact |
645 assume ok: "\<turnstile> \<Delta> ok" |
638 have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed) |
646 and extends: "\<Delta> extends \<Gamma>" |
639 hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force |
647 have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed) |
640 moreover |
648 hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force |
641 have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def) |
649 moreover |
642 ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp |
650 have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def) |
643 moreover |
651 ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp |
644 have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp |
652 moreover |
645 ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) |
653 have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp |
|
654 ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) |
|
655 qed |
|
656 qed |
646 qed |
657 |
647 |
658 text {* more automated proof *} |
648 text {* more automated proof *} |
659 |
649 |
660 lemma weakening: |
650 lemma weakening: |
661 assumes a1: "\<Gamma> \<turnstile> S <: T" |
651 assumes a: "\<Gamma> \<turnstile> S <: T" |
662 shows "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> S <: T" |
652 and b: "\<turnstile> \<Delta> ok" |
663 using a1 |
653 and c: "\<Delta> extends \<Gamma>" |
664 proof (nominal_induct \<Gamma> S T fresh: \<Delta> rule: subtype_of_rel_induct) |
654 shows "\<Delta> \<turnstile> S <: T" |
|
655 using a b c |
|
656 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of_rel_induct) |
665 case (S_Top \<Gamma> S) thus ?case by (force intro: extends_closed) |
657 case (S_Top \<Gamma> S) thus ?case by (force intro: extends_closed) |
666 next |
658 next |
667 case (S_Var \<Gamma> X S T) thus ?case by (force simp add: extends_def) |
659 case (S_Var \<Gamma> X S T) thus ?case by (force simp add: extends_def) |
668 next |
660 next |
669 case (S_Refl \<Gamma> X) thus ?case by (force dest: extends_domain) |
661 case (S_Refl \<Gamma> X) thus ?case by (force dest: extends_domain) |
670 next |
662 next |
671 case S_Arrow thus ?case by force |
663 case S_Arrow thus ?case by force |
672 next |
664 next |
673 case (S_All \<Gamma> X S1 S2 T1 T2) |
665 case (S_All \<Gamma> X S1 S2 T1 T2) |
674 have fresh: "X\<sharp>\<Delta>" by fact |
666 have fresh: "X\<sharp>\<Delta>" by fact |
675 have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact |
667 have ih1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T1 <: S1" by fact |
676 have ih2: "\<And> \<Delta>. \<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact |
668 have ih2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((X,T1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S2 <: T2" by fact |
677 have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact |
669 have lh_drv_prem: "\<Gamma> \<turnstile> T1 <: S1" by fact |
678 hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
670 hence b5: "T1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) |
679 show "\<turnstile> \<Delta> ok \<longrightarrow> \<Delta> extends \<Gamma> \<longrightarrow> \<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" |
671 have ok: "\<turnstile> \<Delta> ok" by fact |
680 proof (intro strip) |
672 have extends: "\<Delta> extends \<Gamma>" by fact |
681 assume ok: "\<turnstile> \<Delta> ok" |
673 have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed) |
682 and extends: "\<Delta> extends \<Gamma>" |
674 hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force |
683 have "T1 closed_in \<Delta>" using extends b5 by (simp only: extends_closed) |
675 moreover |
684 hence "\<turnstile> ((X,T1)#\<Delta>) ok" using fresh ok by force |
676 have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def) |
685 moreover |
677 ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp |
686 have "((X,T1)#\<Delta>) extends ((X,T1)#\<Gamma>)" using extends by (force simp add: extends_def) |
678 moreover |
687 ultimately have "((X,T1)#\<Delta>) \<turnstile> S2 <: T2" using ih2 by simp |
679 have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp |
688 moreover |
680 ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) |
689 have "\<Delta> \<turnstile> T1 <: S1" using ok extends ih1 by simp |
681 qed |
690 ultimately show "\<Delta> \<turnstile> \<forall> [X<:S1].S2 <: \<forall> [X<:T1].T2" using ok by (force intro: S_All) |
|
691 qed |
|
692 qed |
|
693 |
682 |
694 (* helper lemma to calculate the measure of the induction *) |
683 (* helper lemma to calculate the measure of the induction *) |
695 lemma measure_eq [simp]: "(x, y) \<in> measure f = (f x < f y)" |
684 lemma measure_eq [simp]: "(x, y) \<in> measure f = (f x < f y)" |
696 by (simp add: measure_def inv_image_def) |
685 by (simp add: measure_def inv_image_def) |
697 |
686 |
698 |
|
699 lemma transitivity_and_narrowing: |
687 lemma transitivity_and_narrowing: |
700 "(\<forall>\<Gamma> S T. \<Gamma> \<turnstile> S <: Q \<longrightarrow> \<Gamma> \<turnstile> Q <: T \<longrightarrow> \<Gamma> \<turnstile> S <: T) \<and> |
688 shows "(\<forall>\<Gamma> S T. \<Gamma> \<turnstile> S <: Q \<longrightarrow> \<Gamma> \<turnstile> Q <: T \<longrightarrow> \<Gamma> \<turnstile> S <: T) \<and> |
701 (\<forall>\<Delta> \<Gamma> X P M N. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<longrightarrow> \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
689 (\<forall>\<Delta> \<Gamma> X P M N. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<longrightarrow> \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
702 proof (rule wf_induct [of "measure size_ty" _ Q, rule_format]) |
690 proof (rule wf_induct [of "measure size_ty" _ Q, rule_format]) |
703 show "wf (measure size_ty)" by simp |
691 show "wf (measure size_ty)" by simp |
704 next |
692 next |
705 case (goal2 Q) |
693 case (goal2 Q) |
706 note IH1_outer = goal2[THEN conjunct1] |
694 note IH1_outer = goal2[THEN conjunct1] |
707 and IH2_outer = goal2[THEN conjunct2, THEN spec, of _ "[]", simplified] |
695 and IH2_outer = goal2[THEN conjunct2, THEN spec, of _ "[]", simplified] |
708 (* CHECK: Not clear whether the condition size_ty Q = size_ty Q' is needed, or whether |
696 |
709 just doing it for Q'=Q is enough *) |
697 thm IH1_outer |
|
698 thm IH2_outer |
|
699 |
710 have transitivity: |
700 have transitivity: |
711 "\<And>\<Gamma> S T. \<Gamma> \<turnstile> S <: Q \<Longrightarrow> \<Gamma> \<turnstile> Q <: T \<longrightarrow> \<Gamma> \<turnstile> S <: T" |
701 "\<And>\<Gamma> S T. \<Gamma> \<turnstile> S <: Q \<Longrightarrow> \<Gamma> \<turnstile> Q <: T \<Longrightarrow> \<Gamma> \<turnstile> S <: T" |
712 proof - |
702 proof - |
713 |
703 |
714 (* We first handle the case where T = Top once and for all; this saves some |
704 (* We first handle the case where T = Top once and for all; this saves some |
715 repeated argument below (just like on paper :-). We establish a little lemma |
705 repeated argument below (just like on paper :-). We establish a little lemma |
716 that is invoked where needed in each case of the induction. *) |
706 that is invoked where needed in each case of the induction. *) |
733 ultimately show "\<Gamma> \<turnstile> S <: T'" by blast |
723 ultimately show "\<Gamma> \<turnstile> S <: T'" by blast |
734 qed |
724 qed |
735 |
725 |
736 (* Now proceed by induction on the left-hand derivation *) |
726 (* Now proceed by induction on the left-hand derivation *) |
737 fix \<Gamma> S T |
727 fix \<Gamma> S T |
738 assume a: "\<Gamma> \<turnstile> S <: Q" |
728 assume a: "\<Gamma> \<turnstile> S <: Q" |
739 from a show "\<Gamma> \<turnstile> Q <: T \<longrightarrow> \<Gamma> \<turnstile> S <: T" |
729 assume b: "\<Gamma> \<turnstile> Q <: T" |
740 (* FIXME : nominal induct does not work here because Gamma S and Q are fixed variables *) |
730 from a b show "\<Gamma> \<turnstile> S <: T" |
741 (* FIX: It would be better to use S',\<Gamma>',etc., instead of S1,\<Gamma>1, for consistency, in the cases |
731 proof(nominal_induct \<Gamma> S Q\<equiv>Q avoiding: \<Gamma> S T rule: subtype_of_rel_induct) |
742 where these do not refer to sub-phrases of S, etc. *) |
732 (* Q is immediately instanciated - no way to delay that? *) |
743 proof(nominal_induct \<Gamma> S Q\<equiv>Q fresh: \<Gamma> S T rule: subtype_of_rel_induct) |
733 case (S_Top \<Gamma>1 S1) --"lh drv.: \<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> S1 <: Top" |
744 (* interesting case *) |
734 have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact |
745 |
735 have lh_drv_prem2: "S1 closed_in \<Gamma>1" by fact |
746 case (goal1 \<Gamma>1 S1) --"lh drv.: \<Gamma> \<turnstile> S <: Q' \<equiv> \<Gamma>1 \<turnstile> S1 <: Top" |
736 have Q_inst: "Top=Q" by fact |
747 --"automatic proof: thus ?case proof (auto intro!: S_Top dest: S_TopE)" |
737 have rh_drv: "\<Gamma>1 \<turnstile> Q <: T" --"rh drv." by fact |
748 assume lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" |
738 hence "T = Top" using Q_inst by (simp add: S_TopE) |
749 and lh_drv_prem2: "S1 closed_in \<Gamma>1" |
739 thus "\<Gamma>1 \<turnstile> S1 <: T" using top_case[of "\<Gamma>1" "S1" "False" "T"] lh_drv_prem1 lh_drv_prem2 |
750 and Q_eq: "Top=Q" |
740 by simp |
751 show "\<Gamma>1 \<turnstile> Q <: T \<longrightarrow> \<Gamma>1 \<turnstile> S1 <: T" (* FIXME: why Ta? *) |
|
752 proof (intro strip) |
|
753 assume "\<Gamma>1 \<turnstile> Q <: T" --"rh drv." |
|
754 hence "T = Top" using Q_eq by (simp add: S_TopE) |
|
755 thus "\<Gamma>1 \<turnstile> S1 <: T" using top_case[of "\<Gamma>1" "S1" "False" "T"] lh_drv_prem1 lh_drv_prem2 |
|
756 by simp |
|
757 qed |
|
758 next |
741 next |
759 case (goal2 \<Gamma>1 X1 S1 T1) --"lh drv.: \<Gamma> \<turnstile> S <: Q' \<equiv> \<Gamma>1 \<turnstile> TVar(X1) <: S1" |
742 case (S_Var \<Gamma>1 X1 S1 T1) --"lh drv.: \<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> TVar(X1) <: S1" |
760 --"automatic proof: thus ?case proof (auto intro!: S_Var)" |
|
761 have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact |
743 have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact |
762 have lh_drv_prem2: "(X1,S1)\<in>set \<Gamma>1" by fact |
744 have lh_drv_prem2: "(X1,S1)\<in>set \<Gamma>1" by fact |
763 have IH_inner: "\<And>T. \<Gamma>1 \<turnstile> T1 <: T \<longrightarrow> \<Gamma>1 \<turnstile> S1 <: T" by fact |
745 have IH_inner: "\<And>T. \<Gamma>1 \<turnstile> Q <: T \<Longrightarrow> T1=Q \<Longrightarrow> \<Gamma>1 \<turnstile> S1 <: T" by fact |
764 show "\<Gamma>1 \<turnstile> T1 <: Ta \<longrightarrow> \<Gamma>1 \<turnstile> TyVar X1 <: Ta" |
746 have Q_inst: "T1=Q" by fact |
765 proof (intro strip) |
747 have rh_drv: "\<Gamma>1 \<turnstile> Q <: T" by fact |
766 assume "\<Gamma>1 \<turnstile> T1 <: Ta" --"right-hand drv." |
748 with IH_inner have "\<Gamma>1 \<turnstile> S1 <: T" using Q_inst by simp |
767 with IH_inner have "\<Gamma>1 \<turnstile> S1 <: Ta" by simp |
749 thus "\<Gamma>1 \<turnstile> TyVar X1 <: T" using lh_drv_prem1 lh_drv_prem2 by (simp add: subtype_of_rel.S_Var) |
768 thus "\<Gamma>1 \<turnstile> TyVar X1 <: Ta" using lh_drv_prem1 lh_drv_prem2 by (simp add: S_Var) |
|
769 qed |
|
770 next |
750 next |
771 case goal3 --"S_Refl case" show ?case by simp |
751 case S_Refl --"S_Refl case" thus ?case by simp |
772 next |
752 next |
773 case (goal4 \<Gamma>1 S1 S2 T1 T2) --"lh drv.: \<Gamma> \<turnstile> S <: Q' == \<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T1 \<rightarrow> T2" |
753 case (S_Arrow \<Gamma>1 S1 S2 T1 T2) --"lh drv.: \<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T1 \<rightarrow> T2" |
774 have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact |
754 have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact |
775 have lh_drv_prem2: "\<Gamma>1 \<turnstile> S2 <: T2" by fact |
755 have lh_drv_prem2: "\<Gamma>1 \<turnstile> S2 <: T2" by fact |
776 show "\<Gamma>1 \<turnstile> T1 \<rightarrow> T2 <: T \<longrightarrow> \<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T" |
756 have rh_deriv: "\<Gamma>1 \<turnstile> Q <: T" by fact |
777 proof (intro strip) |
757 have Q_inst: "T1 \<rightarrow> T2 = Q" by fact |
778 (*assume measure: "size_ty Q = size_ty (T1 \<rightarrow> T2)" *) |
758 have measure: "size_ty Q = size_ty (T1 \<rightarrow> T2)" using Q_inst by simp |
779 assume rh_deriv: "\<Gamma>1 \<turnstile> T1 \<rightarrow> T2 <: T'" |
759 have "S1 closed_in \<Gamma>1" and "S2 closed_in \<Gamma>1" |
780 have "S1 closed_in \<Gamma>1" and "S2 closed_in \<Gamma>1" |
760 using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed) |
781 using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed) |
761 hence "(S1 \<rightarrow> S2) closed_in \<Gamma>1" by (simp add: closed_in_def ty.supp) |
782 hence "(S1 \<rightarrow> S2) closed_in \<Gamma>1" by (simp add: closed_in_def ty.supp) |
762 moreover |
783 moreover |
763 have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok) |
784 have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok) |
764 moreover |
785 moreover |
765 have "T = Top \<or> (\<exists>T3 T4. T= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4)" |
786 have "T' = Top \<or> (\<exists>T3 T4. T'= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4)" |
766 using rh_deriv Q_inst by (simp add:S_ArrowE_left) |
787 using rh_deriv by (rule S_ArrowE_left) |
767 moreover |
|
768 { assume "\<exists>T3 T4. T= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4" |
|
769 then obtain T3 T4 |
|
770 where T_inst: "T= T3 \<rightarrow> T4" |
|
771 and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1" |
|
772 and rh_drv_prem2: "\<Gamma>1 \<turnstile> T2 <: T4" by force |
|
773 from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" |
|
774 using measure rh_drv_prem1 lh_drv_prem1 by (force simp add: ty.inject) |
788 moreover |
775 moreover |
789 { assume "\<exists>T3 T4. T'= T3 \<rightarrow> T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> \<Gamma>1 \<turnstile> T2 <: T4" |
776 from IH1_outer[of "T2"] have "\<Gamma>1 \<turnstile> S2 <: T4" |
790 then obtain T3 T4 |
777 using measure rh_drv_prem2 lh_drv_prem2 by (force simp add: ty.inject) |
791 where T'_inst: "T'= T3 \<rightarrow> T4" |
778 ultimately have "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T" using T_inst by force |
792 and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1" |
779 } |
793 and rh_drv_prem2: "\<Gamma>1 \<turnstile> T2 <: T4" by force |
780 ultimately show "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T" using top_case[of "\<Gamma>1" "S1\<rightarrow>S2" _ "T'"] by blast |
794 from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" |
|
795 using measure rh_drv_prem1 lh_drv_prem1 by (force simp add: ty.inject) |
|
796 moreover |
|
797 from IH1_outer[of "T2"] have "\<Gamma>1 \<turnstile> S2 <: T4" |
|
798 using measure rh_drv_prem2 lh_drv_prem2 by (force simp add: ty.inject) |
|
799 ultimately have "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T'" using T'_inst by force |
|
800 } |
|
801 ultimately show "\<Gamma>1 \<turnstile> S1 \<rightarrow> S2 <: T'" using top_case[of "\<Gamma>1" "S1\<rightarrow>S2" _ "T'"] by blast |
|
802 qed |
|
803 next |
781 next |
804 case (goal5 T' \<Gamma>1 X S1 S2 T1 T2) --"lh drv.: \<Gamma> \<turnstile> S <: Q' \<equiv> \<Gamma>1 \<turnstile> \<forall>[X:S1].S2 <: \<forall>[X:T1].T2" |
782 case (S_All \<Gamma>1 X S1 S2 T1 T2) --"lh drv.: \<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> \<forall>[X:S1].S2 <: \<forall>[X:T1].T2" |
805 have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact |
783 have lh_drv_prem1: "\<Gamma>1 \<turnstile> T1 <: S1" by fact |
806 have lh_drv_prem2: "((X,T1)#\<Gamma>1) \<turnstile> S2 <: T2" by fact |
784 have lh_drv_prem2: "((X,T1)#\<Gamma>1) \<turnstile> S2 <: T2" by fact |
807 have fresh_cond: "X\<sharp>(\<Gamma>1,S1,T1)" by fact |
785 have rh_deriv: "\<Gamma>1 \<turnstile> Q <: T" by fact |
808 show "size_ty Q = size_ty (\<forall>[X<:T1].T2) \<longrightarrow> \<Gamma>1 \<turnstile> \<forall>[X<:T1].T2 <: T' \<longrightarrow> \<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T'" |
786 have fresh_cond: "X\<sharp>\<Gamma>1" "X\<sharp>S1" "X\<sharp>T1" by fact |
809 proof (intro strip) |
787 have Q_inst: "\<forall>[X<:T1].T2 = Q" by fact |
810 assume measure: "size_ty Q = size_ty (\<forall>[X<:T1].T2)" |
788 have measure: "size_ty Q = size_ty (\<forall>[X<:T1].T2)" using Q_inst by simp |
811 and rh_deriv: "\<Gamma>1 \<turnstile> \<forall>[X<:T1].T2 <: T'" |
789 have "S1 closed_in \<Gamma>1" and "S2 closed_in ((X,T1)#\<Gamma>1)" |
812 have "S1 closed_in \<Gamma>1" and "S2 closed_in ((X,T1)#\<Gamma>1)" |
790 using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed) |
813 using lh_drv_prem1 lh_drv_prem2 by (simp_all add: subtype_implies_closed) |
791 hence "(\<forall>[X<:S1].S2) closed_in \<Gamma>1" by (force simp add: closed_in_def ty.supp abs_supp) |
814 hence "(\<forall>[X<:S1].S2) closed_in \<Gamma>1" by (force simp add: closed_in_def ty.supp abs_supp) |
792 moreover |
815 moreover |
793 have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok) |
816 have "\<turnstile> \<Gamma>1 ok" using rh_deriv by (rule subtype_implies_ok) |
794 moreover |
817 moreover |
|
818 (* FIX: Maybe T3,T4 could be T1',T2' *) |
795 (* FIX: Maybe T3,T4 could be T1',T2' *) |
819 have "T' = Top \<or> (\<exists>T3 T4. T'=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4)" |
796 have "T = Top \<or> (\<exists>T3 T4. T=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4)" |
820 using rh_deriv fresh_cond by (auto dest: S_AllE_left simp add: fresh_prod) |
797 using rh_deriv fresh_cond Q_inst by (auto dest: S_AllE_left simp add: fresh_prod) |
|
798 moreover |
|
799 { assume "\<exists>T3 T4. T=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" |
|
800 then obtain T3 T4 |
|
801 where T_inst: "T= \<forall>[X<:T3].T4" |
|
802 and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1" |
|
803 and rh_drv_prem2:"((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" by force |
|
804 from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" |
|
805 using lh_drv_prem1 rh_drv_prem1 measure by (force simp add: ty.inject) |
821 moreover |
806 moreover |
822 { assume "\<exists>T3 T4. T'=\<forall>[X<:T3].T4 \<and> \<Gamma>1 \<turnstile> T3 <: T1 \<and> ((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" |
807 from IH2_outer[of "T1"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T2" |
823 then obtain T3 T4 |
808 using measure lh_drv_prem2 rh_drv_prem1 by force |
824 where T'_inst: "T'= \<forall>[X<:T3].T4" |
809 with IH1_outer[of "T2"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T4" |
825 and rh_drv_prem1: "\<Gamma>1 \<turnstile> T3 <: T1" |
810 using measure rh_drv_prem2 by force |
826 and rh_drv_prem2:"((X,T3)#\<Gamma>1) \<turnstile> T2 <: T4" by force |
811 moreover |
827 from IH1_outer[of "T1"] have "\<Gamma>1 \<turnstile> T3 <: S1" |
812 ultimately have "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T" |
828 using lh_drv_prem1 rh_drv_prem1 measure by (force simp add: ty.inject) |
813 using fresh_cond T_inst by (simp add: fresh_prod subtype_of_rel.S_All) |
829 moreover |
814 } |
830 from IH2_outer[of "T1"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T2" |
815 ultimately show "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T" using Q_inst top_case[of "\<Gamma>1" "\<forall>[X<:S1].S2" _ "T'"] |
831 using measure lh_drv_prem2 rh_drv_prem1 by force |
816 by auto |
832 with IH1_outer[of "T2"] have "((X,T3)#\<Gamma>1) \<turnstile> S2 <: T4" |
|
833 using measure rh_drv_prem2 by force |
|
834 moreover |
|
835 ultimately have "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T'" |
|
836 using fresh_cond T'_inst by (simp add: fresh_prod S_All) |
|
837 } |
|
838 ultimately show "\<Gamma>1 \<turnstile> \<forall>[X<:S1].S2 <: T'" using top_case[of "\<Gamma>1" "\<forall>[X<:S1].S2" _ "T'"] by blast |
|
839 qed |
|
840 qed |
817 qed |
841 qed |
818 qed |
842 |
819 |
843 (* test |
820 (* HERE *) |
844 have narrowing: |
821 have narrowing: |
845 "\<And>\<Delta> \<Gamma> X M N. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<Longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P<:Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
822 "\<And>\<Delta> \<Gamma> X M N P. (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N \<Longrightarrow> \<Gamma> \<turnstile> P<:Q \<Longrightarrow> (\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N" |
846 proof - |
823 proof - |
847 fix \<Delta> \<Gamma> X M N |
824 fix \<Delta> \<Gamma> X M N P |
848 assume a: "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N" |
825 assume a: "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N" |
849 thus "\<forall>P. \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N" |
826 assume b: "\<Gamma> \<turnstile> P<:Q" |
850 thm subtype_of_rel_induct |
827 show "(\<Delta>@(X,Q)#\<Gamma>) \<turnstile> M <: N" |
851 thm subtype_of_rel.induct |
828 using a b |
852 using a proof (induct) |
829 proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@(X,Q)#\<Gamma>" M N avoiding: \<Gamma> rule: subtype_of_rel_induct) |
853 using a proof (induct rule: subtype_of_rel_induct[of "\<Delta>@(X,Q)#\<Gamma>" "M" "N" _ "()"]) |
830 case (S_Top \<Gamma>1 S1 \<Gamma>2) |
854 *) |
831 have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact |
855 |
832 have lh_drv_prem2: "S1 closed_in \<Gamma>1" by fact |
856 have narrowing: |
833 have \<Gamma>1_inst: "\<Gamma>1=\<Delta>@(X,Q)#\<Gamma>2" by fact |
857 "\<And>\<Delta> \<Gamma> \<Gamma>' X M N. \<Gamma>' \<turnstile> M <: N \<Longrightarrow> \<Gamma>' = \<Delta>@(X,Q)#\<Gamma> \<longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P<:Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
834 have rh_drv: "\<Gamma>2 \<turnstile> P <: Q" by fact |
858 proof - |
835 hence a1: "P closed_in \<Gamma>2" by (simp add: subtype_implies_closed) |
859 fix \<Delta> \<Gamma> \<Gamma>' X M N |
836 hence a2: "\<turnstile> (\<Delta>@(X,P)#\<Gamma>2) ok" using lh_drv_prem1 a1 \<Gamma>1_inst by (simp add: replace_type) |
860 assume "\<Gamma>' \<turnstile> M <: N" |
837 show ?case |
861 thus "\<Gamma>' = \<Delta>@(X,Q)#\<Gamma> \<longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" |
838 show "(\<Delta>@(X,P)#\<Gamma>2) \<turnstile> S1 <: Top" |
862 (* FIXME : nominal induct does not work here because Gamma' M and N are fixed variables *) |
|
863 (* FIX: Same comment about S1,\<Gamma>1 *) |
|
864 proof (rule subtype_of_rel_induct[of "\<Gamma>'" "M" "N" "\<lambda>\<Gamma>' M N (\<Delta>,\<Gamma>,X). |
|
865 \<Gamma>' = \<Delta>@(X,Q)#\<Gamma> \<longrightarrow> (\<forall>P. \<Gamma> \<turnstile> P <: Q \<longrightarrow> (\<Delta>@(X,P)#\<Gamma>) \<turnstile> M <: N)" "(\<Delta>,\<Gamma>,X)", simplified], |
|
866 simp_all only: split_paired_all split_conv) |
|
867 case (goal1 \<Delta>1 \<Gamma>1 X1 \<Gamma>2 S1) |
|
868 have lh_drv_prem1: "\<turnstile> \<Gamma>2 ok" by fact |
|
869 have lh_drv_prem2: "S1 closed_in \<Gamma>2" by fact |
|
870 show "\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1 \<longrightarrow> (\<forall>P. \<Gamma>1 \<turnstile> P <: Q \<longrightarrow> (\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> S1 <: Top)" |
|
871 proof (intro strip) |
|
872 fix P |
|
873 assume a1: "\<Gamma>2 = \<Delta>1@(X1,Q)#\<Gamma>1" |
|
874 assume a2: "\<Gamma>1 \<turnstile> P <: Q" |
|
875 from a2 have "P closed_in \<Gamma>1" by (simp add: subtype_implies_closed) |
|
876 hence a3: "\<turnstile> (\<Delta>1@(X1,P)#\<Gamma>1) ok" using lh_drv_prem1 a1 by (rule_tac replace_type, simp_all) |
|
877 show "(\<Delta>1@(X1,P)#\<Gamma>1) \<turnstile> S1 <: Top" |
|
878 using a1 a3 lh_drv_prem2 by (force simp add: closed_in_def domain_append) |
839 using a1 a3 lh_drv_prem2 by (force simp add: closed_in_def domain_append) |
879 qed |
840 qed |
880 next |
841 next |
881 case (goal2 \<Delta>1 \<Gamma>1 X1 \<Gamma>2 X2 S1 T1) |
842 case (goal2 \<Delta>1 \<Gamma>1 X1 \<Gamma>2 X2 S1 T1) |
882 have lh_drv_prem1: "\<turnstile> \<Gamma>2 ok" by fact |
843 have lh_drv_prem1: "\<turnstile> \<Gamma>2 ok" by fact |