equal
deleted
inserted
replaced
47 qed |
47 qed |
48 |
48 |
49 |
49 |
50 text {* |
50 text {* |
51 In order to help establishing the property that the machine |
51 In order to help establishing the property that the machine |
52 calculates a normal form that corresponds to the evaluation |
52 calculates a nomrmalform that corresponds to the evaluation |
53 relation, we introduce the call-by-value small-step semantics. |
53 relation, we introduce the call-by-value small-step semantics. |
54 *} |
54 *} |
55 |
55 |
56 |
56 |
57 equivariance val |
57 equivariance val |
122 |
122 |
123 section {* EXERCISE 13 *} |
123 section {* EXERCISE 13 *} |
124 |
124 |
125 text {* |
125 text {* |
126 The point of the cbv-reduction was that we can easily relatively |
126 The point of the cbv-reduction was that we can easily relatively |
127 establish the following property: |
127 establish the follwoing property: |
128 *} |
128 *} |
129 |
129 |
130 lemma machine_implies_cbvs_ctx: |
130 lemma machine_implies_cbvs_ctx: |
131 assumes a: "<e, Es> \<mapsto> <e', Es'>" |
131 assumes a: "<e, Es> \<mapsto> <e', Es'>" |
132 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |
132 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |