author | haftmann |
Wed, 20 May 2009 10:37:37 +0200 | |
changeset 31207 | 7eb05fc49b45 |
parent 25974 | 0cb35fa9c6fa |
child 36319 | 8feb2c4bef1a |
permissions | -rw-r--r-- |
9114
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Lambda/Type.thy |
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer |
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
4 |
Copyright 2000 TU Muenchen |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
5 |
*) |
9114
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
6 |
|
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
7 |
header {* Simply-typed lambda terms *} |
9114
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
8 |
|
16417 | 9 |
theory Type imports ListApplication begin |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
10 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
11 |
|
11946 | 12 |
subsection {* Environments *} |
13 |
||
19086 | 14 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
15 |
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91) where |
19086 | 16 |
"e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))" |
19363 | 17 |
|
21210 | 18 |
notation (xsymbols) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
19 |
shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) |
19363 | 20 |
|
21210 | 21 |
notation (HTML output) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
22 |
shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) |
11946 | 23 |
|
24 |
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T" |
|
25 |
by (simp add: shift_def) |
|
26 |
||
27 |
lemma shift_gt [simp]: "j < i \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e j" |
|
28 |
by (simp add: shift_def) |
|
29 |
||
30 |
lemma shift_lt [simp]: "i < j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e (j - 1)" |
|
31 |
by (simp add: shift_def) |
|
32 |
||
33 |
lemma shift_commute [simp]: "e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>" |
|
34 |
apply (rule ext) |
|
35 |
apply (case_tac x) |
|
36 |
apply simp |
|
37 |
apply (case_tac nat) |
|
38 |
apply (simp_all add: shift_def) |
|
39 |
done |
|
40 |
||
41 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
42 |
subsection {* Types and typing rules *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
43 |
|
9641 | 44 |
datatype type = |
9622 | 45 |
Atom nat |
11945 | 46 |
| Fun type type (infixr "\<Rightarrow>" 200) |
9114
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
47 |
|
23750 | 48 |
inductive typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
22271 | 49 |
where |
50 |
Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T" |
|
51 |
| Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)" |
|
52 |
| App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" |
|
53 |
||
23750 | 54 |
inductive_cases typing_elims [elim!]: |
22271 | 55 |
"e \<turnstile> Var i : T" |
56 |
"e \<turnstile> t \<degree> u : T" |
|
57 |
"e \<turnstile> Abs t : T" |
|
58 |
||
25974 | 59 |
primrec |
11943 | 60 |
typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
25974 | 61 |
where |
62 |
"typings e [] Ts = (Ts = [])" |
|
63 |
| "typings e (t # ts) Ts = |
|
64 |
(case Ts of |
|
65 |
[] \<Rightarrow> False |
|
66 |
| T # Ts \<Rightarrow> e \<turnstile> t : T \<and> typings e ts Ts)" |
|
19086 | 67 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
68 |
abbreviation |
19086 | 69 |
typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
70 |
("_ ||- _ : _" [50, 50, 50] 50) where |
19363 | 71 |
"env ||- ts : Ts == typings env ts Ts" |
19086 | 72 |
|
21210 | 73 |
notation (latex) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
74 |
typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50) |
9114
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
75 |
|
25974 | 76 |
abbreviation |
77 |
funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200) where |
|
78 |
"Ts =>> T == foldr Fun Ts T" |
|
79 |
||
80 |
notation (latex) |
|
81 |
funs (infixr "\<Rrightarrow>" 200) |
|
9114
de99e37effda
Subject reduction and strong normalization of simply-typed lambda terms.
berghofe
parents:
diff
changeset
|
82 |
|
9622 | 83 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
84 |
subsection {* Some examples *} |
9622 | 85 |
|
12011 | 86 |
lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T" |
11935 | 87 |
by force |
9622 | 88 |
|
12011 | 89 |
lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T" |
11935 | 90 |
by force |
9622 | 91 |
|
92 |
||
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
93 |
subsection {* Lists of types *} |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
94 |
|
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
95 |
lemma lists_typings: |
22271 | 96 |
"e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts" |
20503 | 97 |
apply (induct ts arbitrary: Ts) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
98 |
apply (case_tac Ts) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
99 |
apply simp |
22271 | 100 |
apply (rule listsp.Nil) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
101 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
102 |
apply (case_tac Ts) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
103 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
104 |
apply simp |
22271 | 105 |
apply (rule listsp.Cons) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
106 |
apply blast |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
107 |
apply blast |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
108 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
109 |
|
18241 | 110 |
lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]" |
20503 | 111 |
apply (induct ts arbitrary: Ts) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
112 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
113 |
apply (case_tac Ts) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
114 |
apply simp+ |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
115 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
116 |
|
18241 | 117 |
lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] = |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
118 |
(e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" |
20503 | 119 |
apply (induct ts arbitrary: Ts) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
120 |
apply (case_tac Ts) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
121 |
apply simp+ |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
122 |
apply (case_tac Ts) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14565
diff
changeset
|
123 |
apply (case_tac "ts @ [t]") |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
124 |
apply simp+ |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
125 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
126 |
|
25974 | 127 |
lemma rev_exhaust2 [extraction_expand]: |
128 |
obtains (Nil) "xs = []" | (snoc) ys y where "xs = ys @ [y]" |
|
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
129 |
-- {* Cannot use @{text rev_exhaust} from the @{text List} |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
130 |
theory, since it is not constructive *} |
25974 | 131 |
apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> thesis") |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
132 |
apply (erule_tac x="rev xs" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
133 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
134 |
apply (rule allI) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
135 |
apply (rule impI) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
136 |
apply (case_tac ys) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
137 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
138 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
139 |
apply atomize |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
140 |
apply (erule allE)+ |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
141 |
apply (erule mp, rule conjI) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
142 |
apply (rule refl)+ |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
143 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
144 |
|
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
145 |
lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow> |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
146 |
(\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> P" |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
147 |
apply (cases Ts rule: rev_exhaust2) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
148 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
149 |
apply (case_tac "ts @ [t]") |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
150 |
apply (simp add: types_snoc_eq)+ |
17589 | 151 |
apply iprover |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
152 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
153 |
|
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
154 |
|
11950 | 155 |
subsection {* n-ary function types *} |
9622 | 156 |
|
11987 | 157 |
lemma list_app_typeD: |
18241 | 158 |
"e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts" |
20503 | 159 |
apply (induct ts arbitrary: t T) |
9622 | 160 |
apply simp |
11987 | 161 |
apply atomize |
9622 | 162 |
apply simp |
12011 | 163 |
apply (erule_tac x = "t \<degree> a" in allE) |
9622 | 164 |
apply (erule_tac x = T in allE) |
165 |
apply (erule impE) |
|
166 |
apply assumption |
|
167 |
apply (elim exE conjE) |
|
23750 | 168 |
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
9622 | 169 |
apply (rule_tac x = "Ta # Ts" in exI) |
170 |
apply simp |
|
171 |
done |
|
172 |
||
11935 | 173 |
lemma list_app_typeE: |
12011 | 174 |
"e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C" |
11935 | 175 |
by (insert list_app_typeD) fast |
176 |
||
11987 | 177 |
lemma list_app_typeI: |
18241 | 178 |
"e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T" |
20503 | 179 |
apply (induct ts arbitrary: t T Ts) |
9622 | 180 |
apply simp |
11987 | 181 |
apply atomize |
9622 | 182 |
apply (case_tac Ts) |
183 |
apply simp |
|
184 |
apply simp |
|
12011 | 185 |
apply (erule_tac x = "t \<degree> a" in allE) |
9622 | 186 |
apply (erule_tac x = T in allE) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14565
diff
changeset
|
187 |
apply (erule_tac x = list in allE) |
9622 | 188 |
apply (erule impE) |
189 |
apply (erule conjE) |
|
190 |
apply (erule typing.App) |
|
191 |
apply assumption |
|
192 |
apply blast |
|
193 |
done |
|
194 |
||
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
195 |
text {* |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
196 |
For the specific case where the head of the term is a variable, |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
197 |
the following theorems allow to infer the types of the arguments |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
198 |
without analyzing the typing derivation. This is crucial |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
199 |
for program extraction. |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
200 |
*} |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
201 |
|
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
202 |
theorem var_app_type_eq: |
18241 | 203 |
"e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U" |
20503 | 204 |
apply (induct ts arbitrary: T U rule: rev_induct) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
205 |
apply simp |
23750 | 206 |
apply (ind_cases "e \<turnstile> Var i : T" for T) |
207 |
apply (ind_cases "e \<turnstile> Var i : T" for T) |
|
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
208 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
209 |
apply simp |
23750 | 210 |
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
211 |
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
|
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
212 |
apply atomize |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
213 |
apply (erule_tac x="Ta \<Rightarrow> T" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
214 |
apply (erule_tac x="Tb \<Rightarrow> U" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
215 |
apply (erule impE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
216 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
217 |
apply (erule impE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
218 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
219 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
220 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
221 |
|
18241 | 222 |
lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
223 |
e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us" |
20503 | 224 |
apply (induct us arbitrary: ts Ts U) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
225 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
226 |
apply (erule var_app_type_eq) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
227 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
228 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
229 |
apply atomize |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
230 |
apply (case_tac U) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
231 |
apply (rule FalseE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
232 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
233 |
apply (erule list_app_typeE) |
23750 | 234 |
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
235 |
apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
236 |
apply assumption |
9622 | 237 |
apply simp |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
238 |
apply (erule_tac x="ts @ [a]" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
239 |
apply (erule_tac x="Ts @ [type1]" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
240 |
apply (erule_tac x="type2" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
241 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
242 |
apply (erule impE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
243 |
apply (rule types_snoc) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
244 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
245 |
apply (erule list_app_typeE) |
23750 | 246 |
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
247 |
apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
248 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
249 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
250 |
apply (erule impE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
251 |
apply (rule typing.App) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
252 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
253 |
apply (erule list_app_typeE) |
23750 | 254 |
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
255 |
apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
256 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
257 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
258 |
apply (erule exE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
259 |
apply (rule_tac x="type1 # Us" in exI) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
260 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
261 |
apply (erule list_app_typeE) |
23750 | 262 |
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
263 |
apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
264 |
apply assumption |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
265 |
apply simp |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
266 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
267 |
|
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
268 |
lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
269 |
(\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P" |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
270 |
apply (drule var_app_types [of _ _ "[]", simplified]) |
17589 | 271 |
apply (iprover intro: typing.Var)+ |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
272 |
done |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
273 |
|
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
274 |
lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P" |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
275 |
apply (cases T) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
276 |
apply (rule FalseE) |
22271 | 277 |
apply (erule typing.cases) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
278 |
apply simp_all |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
279 |
apply atomize |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
280 |
apply (erule_tac x="type1" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
281 |
apply (erule_tac x="type2" in allE) |
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
282 |
apply (erule mp) |
22271 | 283 |
apply (erule typing.cases) |
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
284 |
apply simp_all |
9622 | 285 |
done |
286 |
||
287 |
||
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
288 |
subsection {* Lifting preserves well-typedness *} |
9622 | 289 |
|
18257 | 290 |
lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T" |
20503 | 291 |
by (induct arbitrary: i U set: typing) auto |
12171 | 292 |
|
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
293 |
lemma lift_types: |
18241 | 294 |
"e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts" |
20503 | 295 |
apply (induct ts arbitrary: Ts) |
9622 | 296 |
apply simp |
297 |
apply (case_tac Ts) |
|
11946 | 298 |
apply auto |
9622 | 299 |
done |
300 |
||
301 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
302 |
subsection {* Substitution lemmas *} |
9622 | 303 |
|
11994 | 304 |
lemma subst_lemma: |
18257 | 305 |
"e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T" |
20503 | 306 |
apply (induct arbitrary: e' i U u set: typing) |
11946 | 307 |
apply (rule_tac x = x and y = i in linorder_cases) |
308 |
apply auto |
|
309 |
apply blast |
|
9622 | 310 |
done |
311 |
||
12011 | 312 |
lemma substs_lemma: |
18241 | 313 |
"e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow> |
11943 | 314 |
e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts" |
20503 | 315 |
apply (induct ts arbitrary: Ts) |
9622 | 316 |
apply (case_tac Ts) |
317 |
apply simp |
|
318 |
apply simp |
|
12011 | 319 |
apply atomize |
9622 | 320 |
apply (case_tac Ts) |
321 |
apply simp |
|
322 |
apply simp |
|
323 |
apply (erule conjE) |
|
12011 | 324 |
apply (erule (1) subst_lemma) |
11994 | 325 |
apply (rule refl) |
326 |
done |
|
327 |
||
9622 | 328 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
329 |
subsection {* Subject reduction *} |
9622 | 330 |
|
22271 | 331 |
lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T" |
20503 | 332 |
apply (induct arbitrary: t' set: typing) |
9622 | 333 |
apply blast |
334 |
apply blast |
|
11994 | 335 |
apply atomize |
23750 | 336 |
apply (ind_cases "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t') |
9622 | 337 |
apply hypsubst |
23750 | 338 |
apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U) |
9622 | 339 |
apply (rule subst_lemma) |
340 |
apply assumption |
|
341 |
apply assumption |
|
342 |
apply (rule ext) |
|
11935 | 343 |
apply (case_tac x) |
11946 | 344 |
apply auto |
9622 | 345 |
done |
346 |
||
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
347 |
theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T" |
23750 | 348 |
by (induct set: rtranclp) (iprover intro: subject_reduction)+ |
9622 | 349 |
|
350 |
||
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset
|
351 |
subsection {* Alternative induction rule for types *} |
9622 | 352 |
|
11935 | 353 |
lemma type_induct [induct type]: |
18241 | 354 |
assumes |
11945 | 355 |
"(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow> |
18241 | 356 |
(\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)" |
357 |
shows "P T" |
|
358 |
proof (induct T) |
|
359 |
case Atom |
|
23464 | 360 |
show ?case by (rule assms) simp_all |
18241 | 361 |
next |
362 |
case Fun |
|
23464 | 363 |
show ?case by (rule assms) (insert Fun, simp_all) |
11935 | 364 |
qed |
365 |
||
11638 | 366 |
end |