2701
+ − 1
+ − 2
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 3
theory Tutorial5
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
imports Tutorial4
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 5
begin
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 6
2701
+ − 7
section {* Type-Preservation and Progress Lemma*}
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 8
2701
+ − 9
text {*
+ − 10
The point of this tutorial is to prove the
+ − 11
type-preservation and progress lemma. Since
+ − 12
we now know that \<Down>, \<longrightarrow>cbv* and the machine
+ − 13
correspond to each other, we only need to
+ − 14
prove this property for one of them. We chose
+ − 15
\<longrightarrow>cbv.
+ − 16
+ − 17
First we need to establish two elimination
+ − 18
properties and two auxiliary lemmas about contexts.
+ − 19
*}
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 20
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 21
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 22
lemma valid_elim:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 23
assumes a: "valid ((x, T) # \<Gamma>)"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 24
shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 25
using a by (cases) (auto)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 26
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 27
lemma valid_insert:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 28
assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 29
shows "valid (\<Delta> @ \<Gamma>)"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 30
using a
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 31
by (induct \<Delta>)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 32
(auto simp add: fresh_append fresh_Cons dest!: valid_elim)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 33
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 34
lemma fresh_list:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 35
shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 36
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 37
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 38
lemma context_unique:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 39
assumes a1: "valid \<Gamma>"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 40
and a2: "(x, T) \<in> set \<Gamma>"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 41
and a3: "(x, U) \<in> set \<Gamma>"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 42
shows "T = U"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 43
using a1 a2 a3
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 44
by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 45
2701
+ − 46
+ − 47
section {* EXERCISE 16 *}
+ − 48
+ − 49
text {*
+ − 50
Next we want to show the type substitution lemma. Unfortunately,
+ − 51
we have to prove a slightly more general version of it, where
+ − 52
the variable being substituted occurs somewhere inside the
+ − 53
context.
+ − 54
*}
+ − 55
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 56
lemma type_substitution_aux:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 57
assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 58
and b: "\<Gamma> \<turnstile> e' : T'"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 59
shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 60
using a b
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 61
proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 62
case (t_Var y T x e' \<Delta>)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 63
have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 64
have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 65
have a3: "\<Gamma> \<turnstile> e' : T'" by fact
2701
+ − 66
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 67
from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 68
{ assume eq: "x = y"
2701
+ − 69
+ − 70
have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" sorry
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 71
}
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 72
moreover
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 73
{ assume ineq: "x \<noteq> y"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 74
from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 75
then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 76
}
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 77
ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
2701
+ − 78
next
+ − 79
case (t_Lam y T1 t T2 x e' \<Delta>)
+ − 80
have a1: "atom y \<sharp> e'" by fact
+ − 81
have a2: "atom y \<sharp> \<Delta> @ [(x, T')] @ \<Gamma>" by fact
+ − 82
have a3: "\<Gamma> \<turnstile> e' : T'" by fact
+ − 83
have ih: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> ((y, T1) # \<Delta>) @ \<Gamma> \<turnstile> t [x ::= e'] : T2"
+ − 84
using t_Lam(6)[of "(y, T1) # \<Delta>"] by auto
+ − 85
+ − 86
+ − 87
show "\<Delta> @ \<Gamma> \<turnstile> (Lam [y]. t)[x ::= e'] : T1 \<rightarrow> T2" sorry
+ − 88
next
+ − 89
case (t_App t1 T1 T2 t2 x e' \<Delta>)
+ − 90
have ih1: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t1 [x ::= e'] : T1 \<rightarrow> T2" using t_App(2) by auto
+ − 91
have ih2: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t2 [x ::= e'] : T1" using t_App(4) by auto
+ − 92
have a: "\<Gamma> \<turnstile> e' : T'" by fact
+ − 93
+ − 94
show "\<Delta> @ \<Gamma> \<turnstile> App t1 t2 [x ::= e'] : T2" sorry
+ − 95
qed
+ − 96
+ − 97
text {*
+ − 98
From this we can derive the usual version of the substitution
+ − 99
lemma.
+ − 100
*}
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 101
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 102
corollary type_substitution:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 103
assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 104
and b: "\<Gamma> \<turnstile> e' : T'"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 105
shows "\<Gamma> \<turnstile> e[x ::= e'] : T"
2701
+ − 106
using a b type_substitution_aux[of "[]"]
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 107
by auto
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 108
2701
+ − 109
+ − 110
section {* Type Preservation *}
+ − 111
+ − 112
text {*
+ − 113
Finally we are in a position to establish the type preservation
+ − 114
property. We just need the following two inversion rules for
+ − 115
particualr typing instances.
+ − 116
*}
+ − 117
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 118
lemma t_App_elim:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 119
assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 120
obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 121
using a
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 122
by (cases) (auto simp add: lam.eq_iff lam.distinct)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 123
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 124
text {* we have not yet generated strong elimination rules *}
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 125
lemma t_Lam_elim:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 126
assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 127
and fc: "atom x \<sharp> \<Gamma>"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 128
obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 129
using ty fc
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 130
apply(cases)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 131
apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 132
apply(auto simp add: Abs1_eq_iff)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 133
apply(rotate_tac 3)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 134
apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 135
apply(perm_simp)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 136
apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 137
done
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 138
2701
+ − 139
+ − 140
section {* EXERCISE 17 *}
+ − 141
+ − 142
text {*
+ − 143
Fill in the gaps in the t_Lam case. You will need
+ − 144
the type substitution lemma proved above.
+ − 145
*}
+ − 146
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 147
theorem cbv_type_preservation:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 148
assumes a: "t \<longrightarrow>cbv t'"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 149
and b: "\<Gamma> \<turnstile> t : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 150
shows "\<Gamma> \<turnstile> t' : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 151
using a b
2701
+ − 152
proof (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
+ − 153
case (cbv1 v x t \<Gamma> T)
+ − 154
have fc: "atom x \<sharp> \<Gamma>" by fact
+ − 155
have "\<Gamma> \<turnstile> App (Lam [x]. t) v : T" by fact
+ − 156
then obtain T' where
+ − 157
*: "\<Gamma> \<turnstile> Lam [x]. t : T' \<rightarrow> T" and
+ − 158
**: "\<Gamma> \<turnstile> v : T'" by (rule t_App_elim)
+ − 159
have "(x, T') # \<Gamma> \<turnstile> t : T" using * fc by (rule t_Lam_elim) (simp add: ty.eq_iff)
+ − 160
+ − 161
show "\<Gamma> \<turnstile> t [x ::= v] : T " sorry
+ − 162
qed (auto elim!: t_App_elim)
+ − 163
+ − 164
text {*
+ − 165
We can easily extend this to sequences of cbv* reductions.
+ − 166
*}
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 167
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 168
corollary cbvs_type_preservation:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 169
assumes a: "t \<longrightarrow>cbv* t'"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 170
and b: "\<Gamma> \<turnstile> t : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 171
shows "\<Gamma> \<turnstile> t' : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 172
using a b
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 173
by (induct) (auto intro: cbv_type_preservation)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 174
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 175
text {*
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 176
The type-preservation property for the machine and
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 177
evaluation relation.
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 178
*}
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 179
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 180
theorem machine_type_preservation:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 181
assumes a: "<t, []> \<mapsto>* <t', []>"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 182
and b: "\<Gamma> \<turnstile> t : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 183
shows "\<Gamma> \<turnstile> t' : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 184
proof -
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 185
have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 186
then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 187
qed
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 188
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 189
theorem eval_type_preservation:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 190
assumes a: "t \<Down> t'"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 191
and b: "\<Gamma> \<turnstile> t : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 192
shows "\<Gamma> \<turnstile> t' : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 193
proof -
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 194
have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 195
then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 196
qed
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 197
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 198
text {* The Progress Property *}
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 199
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 200
lemma canonical_tArr:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 201
assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 202
and b: "val t"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 203
obtains x t' where "t = Lam [x].t'"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 204
using b a by (induct) (auto)
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 205
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 206
theorem progress:
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 207
assumes a: "[] \<turnstile> t : T"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 208
shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 209
using a
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 210
by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
2698
+ − 211
(auto elim: canonical_tArr simp add: val.simps)
2691
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 212
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 213
text {*
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 214
Done! Congratulations!
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 215
*}
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 216
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 217
end
abb6c3ac2df2
separated type preservation and progress into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 218