|
1 theory Tutorial5 |
|
2 imports Tutorial4 |
|
3 begin |
|
4 |
|
5 |
|
6 section {* Type Preservation (fixme separate file) *} |
|
7 |
|
8 |
|
9 lemma valid_elim: |
|
10 assumes a: "valid ((x, T) # \<Gamma>)" |
|
11 shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>" |
|
12 using a by (cases) (auto) |
|
13 |
|
14 lemma valid_insert: |
|
15 assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)" |
|
16 shows "valid (\<Delta> @ \<Gamma>)" |
|
17 using a |
|
18 by (induct \<Delta>) |
|
19 (auto simp add: fresh_append fresh_Cons dest!: valid_elim) |
|
20 |
|
21 lemma fresh_list: |
|
22 shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)" |
|
23 by (induct xs) (simp_all add: fresh_Nil fresh_Cons) |
|
24 |
|
25 lemma context_unique: |
|
26 assumes a1: "valid \<Gamma>" |
|
27 and a2: "(x, T) \<in> set \<Gamma>" |
|
28 and a3: "(x, U) \<in> set \<Gamma>" |
|
29 shows "T = U" |
|
30 using a1 a2 a3 |
|
31 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base) |
|
32 |
|
33 lemma type_substitution_aux: |
|
34 assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T" |
|
35 and b: "\<Gamma> \<turnstile> e' : T'" |
|
36 shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T" |
|
37 using a b |
|
38 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
|
39 case (t_Var y T x e' \<Delta>) |
|
40 have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact |
|
41 have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact |
|
42 have a3: "\<Gamma> \<turnstile> e' : T'" by fact |
|
43 from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert) |
|
44 { assume eq: "x = y" |
|
45 from a1 a2 have "T = T'" using eq by (auto intro: context_unique) |
|
46 with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening) |
|
47 } |
|
48 moreover |
|
49 { assume ineq: "x \<noteq> y" |
|
50 from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp |
|
51 then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto |
|
52 } |
|
53 ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast |
|
54 qed (force simp add: fresh_append fresh_Cons)+ |
|
55 |
|
56 corollary type_substitution: |
|
57 assumes a: "(x, T') # \<Gamma> \<turnstile> e : T" |
|
58 and b: "\<Gamma> \<turnstile> e' : T'" |
|
59 shows "\<Gamma> \<turnstile> e[x ::= e'] : T" |
|
60 using a b type_substitution_aux[where \<Delta>="[]"] |
|
61 by auto |
|
62 |
|
63 lemma t_App_elim: |
|
64 assumes a: "\<Gamma> \<turnstile> App t1 t2 : T" |
|
65 obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'" |
|
66 using a |
|
67 by (cases) (auto simp add: lam.eq_iff lam.distinct) |
|
68 |
|
69 text {* we have not yet generated strong elimination rules *} |
|
70 lemma t_Lam_elim: |
|
71 assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" |
|
72 and fc: "atom x \<sharp> \<Gamma>" |
|
73 obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2" |
|
74 using ty fc |
|
75 apply(cases) |
|
76 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff) |
|
77 apply(auto simp add: Abs1_eq_iff) |
|
78 apply(rotate_tac 3) |
|
79 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI) |
|
80 apply(perm_simp) |
|
81 apply(auto simp add: flip_def swap_fresh_fresh ty_fresh) |
|
82 done |
|
83 |
|
84 theorem cbv_type_preservation: |
|
85 assumes a: "t \<longrightarrow>cbv t'" |
|
86 and b: "\<Gamma> \<turnstile> t : T" |
|
87 shows "\<Gamma> \<turnstile> t' : T" |
|
88 using a b |
|
89 by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct) |
|
90 (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff) |
|
91 |
|
92 corollary cbvs_type_preservation: |
|
93 assumes a: "t \<longrightarrow>cbv* t'" |
|
94 and b: "\<Gamma> \<turnstile> t : T" |
|
95 shows "\<Gamma> \<turnstile> t' : T" |
|
96 using a b |
|
97 by (induct) (auto intro: cbv_type_preservation) |
|
98 |
|
99 text {* |
|
100 The type-preservation property for the machine and |
|
101 evaluation relation. |
|
102 *} |
|
103 |
|
104 theorem machine_type_preservation: |
|
105 assumes a: "<t, []> \<mapsto>* <t', []>" |
|
106 and b: "\<Gamma> \<turnstile> t : T" |
|
107 shows "\<Gamma> \<turnstile> t' : T" |
|
108 proof - |
|
109 have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp |
|
110 then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp |
|
111 qed |
|
112 |
|
113 theorem eval_type_preservation: |
|
114 assumes a: "t \<Down> t'" |
|
115 and b: "\<Gamma> \<turnstile> t : T" |
|
116 shows "\<Gamma> \<turnstile> t' : T" |
|
117 proof - |
|
118 have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp |
|
119 then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp |
|
120 qed |
|
121 |
|
122 text {* The Progress Property *} |
|
123 |
|
124 lemma canonical_tArr: |
|
125 assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2" |
|
126 and b: "val t" |
|
127 obtains x t' where "t = Lam [x].t'" |
|
128 using b a by (induct) (auto) |
|
129 |
|
130 theorem progress: |
|
131 assumes a: "[] \<turnstile> t : T" |
|
132 shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)" |
|
133 using a |
|
134 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T) |
|
135 (auto elim: canonical_tArr) |
|
136 |
|
137 text {* |
|
138 Done! Congratulations! |
|
139 *} |
|
140 |
|
141 end |
|
142 |