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