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