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