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