458 shows "<e1, Es1> \<mapsto>* <e3, Es3>" |
459 shows "<e1, Es1> \<mapsto>* <e3, Es3>" |
459 using a b |
460 using a b |
460 proof(induct) |
461 proof(induct) |
461 case (ms1 e1 Es1) |
462 case (ms1 e1 Es1) |
462 have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact |
463 have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact |
463 then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp |
464 |
|
465 show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry |
464 next |
466 next |
465 case (ms2 e1 Es1 e2 Es2 e2' Es2') |
467 case (ms2 e1 Es1 e2 Es2 e2' Es2') |
466 have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact |
468 have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact |
467 have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact |
469 have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact |
468 have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact |
470 have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact |
469 show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast |
471 |
|
472 show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry |
470 qed |
473 qed |
471 |
474 |
472 text {* |
475 text {* |
473 Just like gotos in the Basic programming language, labels often reduce |
476 Just like gotos in the Basic programming language, labels often reduce |
474 the readability of proofs. Therefore one can use in Isar the notation |
477 the readability of proofs. Therefore one can use in Isar the notation |
582 -- {* your reasoning *} |
585 -- {* your reasoning *} |
583 show "<App t1 t2, []> \<mapsto>* <v, []>" sorry |
586 show "<App t1 t2, []> \<mapsto>* <v, []>" sorry |
584 qed |
587 qed |
585 |
588 |
586 |
589 |
587 theorem |
|
588 assumes a: "t \<Down> t'" |
|
589 shows "<t, Es> \<mapsto>* <t', Es>" |
|
590 using a |
|
591 proof (induct arbitrary: Es) |
|
592 case (e_Lam x t Es) |
|
593 -- {* no assumptions *} |
|
594 show "<Lam [x].t, Es> \<mapsto>* <Lam [x].t, Es>" by auto |
|
595 next |
|
596 case (e_App t1 x t t2 v' v Es) |
|
597 -- {* all assumptions in this case *} |
|
598 have a1: "t1 \<Down> Lam [x].t" by fact |
|
599 have ih1: "\<And>Es. <t1, Es> \<mapsto>* <Lam [x].t, Es>" by fact |
|
600 have a2: "t2 \<Down> v'" by fact |
|
601 have ih2: "\<And>Es. <t2, Es> \<mapsto>* <v', Es>" by fact |
|
602 have a3: "t[x::=v'] \<Down> v" by fact |
|
603 have ih3: "\<And>Es. <t[x::=v'], Es> \<mapsto>* <v, Es>" by fact |
|
604 -- {* your reasoning *} |
|
605 have "<App t1 t2, Es> \<mapsto>* <t1, CAppL \<box> t2 # Es>" by auto |
|
606 moreover |
|
607 have "<t1, CAppL \<box> t2 # Es> \<mapsto>* <Lam [x].t, CAppL \<box> t2 # Es>" using ih1 by auto |
|
608 moreover |
|
609 have "<Lam [x].t, CAppL \<box> t2 # Es> \<mapsto>* <t2, CAppR (Lam [x].t) \<box> # Es>" by auto |
|
610 moreover |
|
611 have "<t2, CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <v', CAppR (Lam [x].t) \<box> # Es>" |
|
612 using ih2 by auto |
|
613 moreover |
|
614 have "val v'" using a2 eval_to_val by auto |
|
615 then have "<v', CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <t[x::=v'], Es>" by auto |
|
616 moreover |
|
617 have "<t[x::=v'], Es> \<mapsto>* <v, Es>" using ih3 by auto |
|
618 ultimately show "<App t1 t2, Es> \<mapsto>* <v, Es>" by blast |
|
619 qed |
|
620 |
|
621 |
|
622 text {* |
590 text {* |
623 Again the automatic tools in Isabelle can discharge automatically |
591 Again the automatic tools in Isabelle can discharge automatically |
624 of the routine work in these proofs. We can write: |
592 of the routine work in these proofs. We can write: |
625 *} |
593 *} |
626 |
594 |
635 assumes a: "t \<Down> t'" |
603 assumes a: "t \<Down> t'" |
636 shows "<t, []> \<mapsto>* <t', []>" |
604 shows "<t, []> \<mapsto>* <t', []>" |
637 using a eval_implies_machines_ctx by simp |
605 using a eval_implies_machines_ctx by simp |
638 |
606 |
639 |
607 |
640 |
|
641 section {* Function Definitions: Filling a Lambda-Term into a Context *} |
608 section {* Function Definitions: Filling a Lambda-Term into a Context *} |
642 |
609 |
643 text {* |
610 text {* |
644 Many functions over datatypes can be defined by recursion on the |
611 Many functions over datatypes can be defined by recursion on the |
645 structure. For this purpose, Isabelle provides "fun". To use it one needs |
612 structure. For this purpose, Isabelle provides "fun". To use it one needs |
664 lemma |
631 lemma |
665 shows "(CAppL \<box> (Var x))\<lbrakk>Var y\<rbrakk> = App (Var y) (Var x)" |
632 shows "(CAppL \<box> (Var x))\<lbrakk>Var y\<rbrakk> = App (Var y) (Var x)" |
666 by simp |
633 by simp |
667 |
634 |
668 fun |
635 fun |
669 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<odot> _" [99,98] 99) |
636 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" (infixr "\<odot>" 99) |
670 where |
637 where |
671 "\<box> \<odot> E' = E'" |
638 "\<box> \<odot> E' = E'" |
672 | "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'" |
639 | "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'" |
673 | "(CAppR t' E) \<odot> E' = CAppR t' (E \<odot> E')" |
640 | "(CAppR t' E) \<odot> E' = CAppR t' (E \<odot> E')" |
674 |
641 |
713 case (CAppR t' E1) |
680 case (CAppR t' E1) |
714 have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact |
681 have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact |
715 show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry |
682 show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry |
716 qed |
683 qed |
717 |
684 |
|
685 |
|
686 subsection {* EXERCISE 6 *} |
|
687 |
|
688 text {* |
|
689 Remove the sorries in the ctx_append proof below. You can make |
|
690 use of the following two properties. |
|
691 *} |
|
692 |
718 lemma neut_hole: |
693 lemma neut_hole: |
719 shows "E \<odot> \<box> = E" |
694 shows "E \<odot> \<box> = E" |
720 by (induct E) (simp_all) |
695 by (induct E) (simp_all) |
721 |
696 |
722 lemma odot_assoc: (* fixme call compose *) |
697 lemma compose_assoc: |
723 shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)" |
698 shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)" |
724 by (induct E1) (simp_all) |
699 by (induct E1) (simp_all) |
725 |
700 |
726 lemma |
701 lemma |
727 shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)" |
702 shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)" |
733 have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact |
708 have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact |
734 |
709 |
735 show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry |
710 show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry |
736 qed |
711 qed |
737 |
712 |
738 |
|
739 text {* |
713 text {* |
740 The last proof involves several steps of equational reasoning. |
714 The last proof involves several steps of equational reasoning. |
741 Isar provides some convenient means to express such equational |
715 Isar provides some convenient means to express such equational |
742 reasoning in a much cleaner fashion using the "also have" |
716 reasoning in a much cleaner fashion using the "also have" |
743 construction. |
717 construction. |
744 *} |
718 *} |
745 |
|
746 |
719 |
747 lemma |
720 lemma |
748 shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)" |
721 shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)" |
749 proof (induct Es1) |
722 proof (induct Es1) |
750 case Nil |
723 case Nil |
751 show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp |
724 show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp |
752 next |
725 next |
753 case (Cons E Es1) |
726 case (Cons E Es1) |
754 have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact |
727 have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact |
755 have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp |
728 have "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp |
|
729 also have "\<dots> = (Es1 @ Es2)\<down> \<odot> E" by simp |
756 also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp |
730 also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp |
757 also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using odot_assoc by simp |
731 also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp |
758 also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp |
732 also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp |
759 finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp |
733 finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp |
760 qed |
734 qed |
761 |
735 |
762 |
736 |
763 |
|
764 end |
737 end |
765 |
738 |