3 imports Tutorial1 Tutorial2 Tutorial3 |
3 imports Tutorial1 Tutorial2 Tutorial3 |
4 begin |
4 begin |
5 |
5 |
6 section {* The CBV Reduction Relation (Small-Step Semantics) *} |
6 section {* The CBV Reduction Relation (Small-Step Semantics) *} |
7 |
7 |
8 text {* |
|
9 In order to help establishing the property that the CK Machine |
|
10 calculates a nomrmalform that corresponds to the evaluation |
|
11 relation, we introduce the call-by-value small-step semantics. |
|
12 *} |
|
13 |
8 |
14 inductive |
9 inductive |
15 cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) |
10 cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) |
16 where |
11 where |
17 cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" |
12 cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" |
18 | cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2" |
13 | cbv2: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2" |
19 | cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'" |
14 | cbv3: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'" |
|
15 |
|
16 inductive |
|
17 "cbv_star" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60) |
|
18 where |
|
19 cbvs1: "e \<longrightarrow>cbv* e" |
|
20 | cbvs2: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3" |
|
21 |
|
22 declare cbv.intros[intro] cbv_star.intros[intro] |
|
23 |
|
24 subsection {* EXERCISE 3 *} |
|
25 |
|
26 text {* |
|
27 Show that cbv* is transitive, by filling the gaps in the |
|
28 proof below. |
|
29 *} |
|
30 |
|
31 lemma |
|
32 assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3" |
|
33 shows "e1 \<longrightarrow>cbv* e3" |
|
34 using a |
|
35 proof (induct) |
|
36 case (cbvs1 e1) |
|
37 have asm: "e1 \<longrightarrow>cbv* e3" by fact |
|
38 show "e1 \<longrightarrow>cbv* e3" sorry |
|
39 next |
|
40 case (cbvs2 e1 e2 e3') |
|
41 have "e1 \<longrightarrow>cbv e2" by fact |
|
42 have "e2 \<longrightarrow>cbv* e3'" by fact |
|
43 have "e3' \<longrightarrow>cbv* e3 \<Longrightarrow> e2 \<longrightarrow>cbv* e3" by fact |
|
44 have "e3' \<longrightarrow>cbv* e3" by fact |
|
45 |
|
46 show "e1 \<longrightarrow>cbv* e3" sorry |
|
47 qed |
|
48 |
|
49 lemma cbvs3 [intro]: |
|
50 assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3" |
|
51 shows "e1 \<longrightarrow>cbv* e3" |
|
52 using a by (induct) (auto) |
|
53 |
|
54 |
|
55 |
|
56 |
|
57 |
|
58 text {* |
|
59 In order to help establishing the property that the CK Machine |
|
60 calculates a nomrmalform that corresponds to the evaluation |
|
61 relation, we introduce the call-by-value small-step semantics. |
|
62 *} |
|
63 |
20 |
64 |
21 equivariance val |
65 equivariance val |
22 equivariance cbv |
66 equivariance cbv |
23 nominal_inductive cbv |
67 nominal_inductive cbv |
24 avoids cbv1: "x" |
68 avoids cbv1: "x" |
42 (auto simp add: lam.fresh fresh_at_base) |
86 (auto simp add: lam.fresh fresh_at_base) |
43 |
87 |
44 |
88 |
45 lemma better_cbv1 [intro]: |
89 lemma better_cbv1 [intro]: |
46 assumes a: "val v" |
90 assumes a: "val v" |
47 shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]" |
91 shows "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" |
48 proof - |
92 proof - |
49 obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh) |
93 obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh) |
50 have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs |
94 have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs |
51 by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base) |
95 by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base) |
52 also have "\<dots> \<longrightarrow>cbv ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a cbv1 by auto |
96 also have "\<dots> \<longrightarrow>cbv ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a cbv1 by auto |
56 |
100 |
57 text {* |
101 text {* |
58 The transitive closure of the cbv-reduction relation: |
102 The transitive closure of the cbv-reduction relation: |
59 *} |
103 *} |
60 |
104 |
61 inductive |
105 |
62 "cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60) |
106 |
63 where |
|
64 cbvs1[intro]: "e \<longrightarrow>cbv* e" |
|
65 | cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3" |
|
66 |
|
67 lemma cbvs3 [intro]: |
|
68 assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3" |
|
69 shows "e1 \<longrightarrow>cbv* e3" |
|
70 using a by (induct) (auto) |
|
71 |
107 |
72 |
108 |
73 subsection {* EXERCISE 8 *} |
109 subsection {* EXERCISE 8 *} |
74 |
110 |
75 text {* |
111 text {* |