author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 56073  29e308b56d23 
child 58273  9f0bfcd15097 
permissions  rwrr 
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 simplytyped lambda terms.
berghofe
parents:
diff
changeset

2 
Author: Stefan Berghofer 
de99e37effda
Subject reduction and strong normalization of simplytyped lambda terms.
berghofe
parents:
diff
changeset

3 
Copyright 2000 TU Muenchen 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

4 
*) 
9114
de99e37effda
Subject reduction and strong normalization of simplytyped lambda terms.
berghofe
parents:
diff
changeset

5 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

6 
header {* Simplytyped lambda terms *} 
9114
de99e37effda
Subject reduction and strong normalization of simplytyped 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 newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

9 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

10 

11946  11 
subsection {* Environments *} 
12 

19086  13 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

14 
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91) where 
19086  15 
"e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j  1))" 
19363  16 

21210  17 
notation (xsymbols) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset

18 
shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) 
19363  19 

21210  20 
notation (HTML output) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset

21 
shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91) 
11946  22 

23 
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T" 

24 
by (simp add: shift_def) 

25 

26 
lemma shift_gt [simp]: "j < i \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e j" 

27 
by (simp add: shift_def) 

28 

29 
lemma shift_lt [simp]: "i < j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e (j  1)" 

30 
by (simp add: shift_def) 

31 

32 
lemma shift_commute [simp]: "e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>" 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
50336
diff
changeset

33 
by (rule ext) (simp_all add: shift_def split: nat.split) 
11946  34 

35 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

36 
subsection {* Types and typing rules *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

37 

9641  38 
datatype type = 
9622  39 
Atom nat 
11945  40 
 Fun type type (infixr "\<Rightarrow>" 200) 
9114
de99e37effda
Subject reduction and strong normalization of simplytyped lambda terms.
berghofe
parents:
diff
changeset

41 

23750  42 
inductive typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) 
22271  43 
where 
44 
Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T" 

45 
 Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)" 

46 
 App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" 

47 

23750  48 
inductive_cases typing_elims [elim!]: 
22271  49 
"e \<turnstile> Var i : T" 
50 
"e \<turnstile> t \<degree> u : T" 

51 
"e \<turnstile> Abs t : T" 

52 

25974  53 
primrec 
11943  54 
typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" 
25974  55 
where 
56 
"typings e [] Ts = (Ts = [])" 

57 
 "typings e (t # ts) Ts = 

58 
(case Ts of 

59 
[] \<Rightarrow> False 

60 
 T # Ts \<Rightarrow> e \<turnstile> t : T \<and> typings e ts Ts)" 

19086  61 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

62 
abbreviation 
19086  63 
typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

64 
("_  _ : _" [50, 50, 50] 50) where 
19363  65 
"env  ts : Ts == typings env ts Ts" 
19086  66 

21210  67 
notation (latex) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset

68 
typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50) 
9114
de99e37effda
Subject reduction and strong normalization of simplytyped lambda terms.
berghofe
parents:
diff
changeset

69 

25974  70 
abbreviation 
71 
funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200) where 

72 
"Ts =>> T == foldr Fun Ts T" 

73 

74 
notation (latex) 

75 
funs (infixr "\<Rrightarrow>" 200) 

9114
de99e37effda
Subject reduction and strong normalization of simplytyped lambda terms.
berghofe
parents:
diff
changeset

76 

9622  77 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

78 
subsection {* Some examples *} 
9622  79 

36319  80 
schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T" 
11935  81 
by force 
9622  82 

36319  83 
schematic_lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T" 
11935  84 
by force 
9622  85 

86 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

87 
subsection {* Lists of types *} 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

88 

35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

89 
lemma lists_typings: 
22271  90 
"e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts" 
20503  91 
apply (induct ts arbitrary: Ts) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

92 
apply (case_tac Ts) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

93 
apply simp 
22271  94 
apply (rule listsp.Nil) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

95 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

96 
apply (case_tac Ts) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

97 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

98 
apply simp 
22271  99 
apply (rule listsp.Cons) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

100 
apply blast 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

101 
apply blast 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

102 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

103 

18241  104 
lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]" 
20503  105 
apply (induct ts arbitrary: Ts) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

106 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

107 
apply (case_tac Ts) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

108 
apply simp+ 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

109 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

110 

18241  111 
lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] = 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

112 
(e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" 
20503  113 
apply (induct ts arbitrary: Ts) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

114 
apply (case_tac Ts) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

115 
apply simp+ 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

116 
apply (case_tac Ts) 
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14565
diff
changeset

117 
apply (case_tac "ts @ [t]") 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

118 
apply simp+ 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

119 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

120 

25974  121 
lemma rev_exhaust2 [extraction_expand]: 
122 
obtains (Nil) "xs = []"  (snoc) ys y where "xs = ys @ [y]" 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

123 
 {* Cannot use @{text rev_exhaust} from the @{text List} 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

124 
theory, since it is not constructive *} 
25974  125 
apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> thesis") 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

126 
apply (erule_tac x="rev xs" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

127 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

128 
apply (rule allI) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

129 
apply (rule impI) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

130 
apply (case_tac ys) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

131 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

132 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

133 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

134 

35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

135 
lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow> 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

136 
(\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> P" 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

137 
apply (cases Ts rule: rev_exhaust2) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

138 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

139 
apply (case_tac "ts @ [t]") 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

140 
apply (simp add: types_snoc_eq)+ 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

141 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

142 

35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

143 

11950  144 
subsection {* nary function types *} 
9622  145 

11987  146 
lemma list_app_typeD: 
18241  147 
"e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts" 
20503  148 
apply (induct ts arbitrary: t T) 
9622  149 
apply simp 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
50336
diff
changeset

150 
apply (rename_tac a b t T) 
11987  151 
apply atomize 
9622  152 
apply simp 
12011  153 
apply (erule_tac x = "t \<degree> a" in allE) 
9622  154 
apply (erule_tac x = T in allE) 
155 
apply (erule impE) 

156 
apply assumption 

157 
apply (elim exE conjE) 

23750  158 
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 
9622  159 
apply (rule_tac x = "Ta # Ts" in exI) 
160 
apply simp 

161 
done 

162 

11935  163 
lemma list_app_typeE: 
12011  164 
"e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C" 
11935  165 
by (insert list_app_typeD) fast 
166 

11987  167 
lemma list_app_typeI: 
18241  168 
"e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T" 
20503  169 
apply (induct ts arbitrary: t T Ts) 
9622  170 
apply simp 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
50336
diff
changeset

171 
apply (rename_tac a b t T Ts) 
11987  172 
apply atomize 
9622  173 
apply (case_tac Ts) 
174 
apply simp 

175 
apply simp 

12011  176 
apply (erule_tac x = "t \<degree> a" in allE) 
9622  177 
apply (erule_tac x = T in allE) 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
50336
diff
changeset

178 
apply (rename_tac list) 
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14565
diff
changeset

179 
apply (erule_tac x = list in allE) 
9622  180 
apply (erule impE) 
181 
apply (erule conjE) 

182 
apply (erule typing.App) 

183 
apply assumption 

184 
apply blast 

185 
done 

186 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

187 
text {* 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

188 
For the specific case where the head of the term is a variable, 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

189 
the following theorems allow to infer the types of the arguments 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

190 
without analyzing the typing derivation. This is crucial 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

191 
for program extraction. 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

192 
*} 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

193 

35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

194 
theorem var_app_type_eq: 
18241  195 
"e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U" 
20503  196 
apply (induct ts arbitrary: T U rule: rev_induct) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

197 
apply simp 
23750  198 
apply (ind_cases "e \<turnstile> Var i : T" for T) 
199 
apply (ind_cases "e \<turnstile> Var i : T" for T) 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

200 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

201 
apply simp 
23750  202 
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 
203 
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

204 
apply atomize 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

205 
apply (erule_tac x="Ta \<Rightarrow> T" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

206 
apply (erule_tac x="Tb \<Rightarrow> U" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

207 
apply (erule impE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

208 
apply assumption 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

209 
apply (erule impE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

210 
apply assumption 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

211 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

212 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

213 

18241  214 
lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

215 
e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us" 
20503  216 
apply (induct us arbitrary: ts Ts U) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

217 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

218 
apply (erule var_app_type_eq) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

219 
apply assumption 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

220 
apply simp 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
50336
diff
changeset

221 
apply (rename_tac a b ts Ts U) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

222 
apply atomize 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

223 
apply (case_tac U) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

224 
apply (rule FalseE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

225 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

226 
apply (erule list_app_typeE) 
23750  227 
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

228 
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

229 
apply assumption 
9622  230 
apply simp 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

231 
apply (erule_tac x="ts @ [a]" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

232 
apply (erule_tac x="Ts @ [type1]" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

233 
apply (erule_tac x="type2" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

234 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

235 
apply (erule impE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

236 
apply (rule types_snoc) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

237 
apply assumption 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

238 
apply (erule list_app_typeE) 
23750  239 
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

240 
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

241 
apply assumption 
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 typing.App) 
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) 
23750  247 
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

248 
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

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 exE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

252 
apply (rule_tac x="type1 # Us" in exI) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

253 
apply simp 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

254 
apply (erule list_app_typeE) 
23750  255 
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

256 
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

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 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

260 

35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

261 
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

262 
(\<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

263 
apply (drule var_app_types [of _ _ "[]", simplified]) 
17589  264 
apply (iprover intro: typing.Var)+ 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

265 
done 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

266 

35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

267 
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

268 
apply (cases T) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

269 
apply (rule FalseE) 
22271  270 
apply (erule typing.cases) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

271 
apply simp_all 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

272 
apply atomize 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

273 
apply (erule_tac x="type1" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

274 
apply (erule_tac x="type2" in allE) 
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

275 
apply (erule mp) 
22271  276 
apply (erule typing.cases) 
14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

277 
apply simp_all 
9622  278 
done 
279 

280 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

281 
subsection {* Lifting preserves welltypedness *} 
9622  282 

18257  283 
lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T" 
20503  284 
by (induct arbitrary: i U set: typing) auto 
12171  285 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

286 
lemma lift_types: 
18241  287 
"e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts" 
20503  288 
apply (induct ts arbitrary: Ts) 
9622  289 
apply simp 
290 
apply (case_tac Ts) 

11946  291 
apply auto 
9622  292 
done 
293 

294 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

295 
subsection {* Substitution lemmas *} 
9622  296 

11994  297 
lemma subst_lemma: 
18257  298 
"e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T" 
20503  299 
apply (induct arbitrary: e' i U u set: typing) 
11946  300 
apply (rule_tac x = x and y = i in linorder_cases) 
301 
apply auto 

302 
apply blast 

9622  303 
done 
304 

12011  305 
lemma substs_lemma: 
18241  306 
"e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow> 
11943  307 
e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts" 
20503  308 
apply (induct ts arbitrary: Ts) 
9622  309 
apply (case_tac Ts) 
310 
apply simp 

311 
apply simp 

12011  312 
apply atomize 
9622  313 
apply (case_tac Ts) 
314 
apply simp 

315 
apply simp 

316 
apply (erule conjE) 

12011  317 
apply (erule (1) subst_lemma) 
11994  318 
apply (rule refl) 
319 
done 

320 

9622  321 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

322 
subsection {* Subject reduction *} 
9622  323 

22271  324 
lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T" 
20503  325 
apply (induct arbitrary: t' set: typing) 
9622  326 
apply blast 
327 
apply blast 

11994  328 
apply atomize 
23750  329 
apply (ind_cases "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t') 
9622  330 
apply hypsubst 
23750  331 
apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U) 
9622  332 
apply (rule subst_lemma) 
333 
apply assumption 

334 
apply assumption 

335 
apply (rule ext) 

11935  336 
apply (case_tac x) 
11946  337 
apply auto 
9622  338 
done 
339 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

340 
theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T" 
23750  341 
by (induct set: rtranclp) (iprover intro: subject_reduction)+ 
9622  342 

343 

14064
35d36f43ba06
Moved strong normalization proof to StrongNorm.thy
berghofe
parents:
13596
diff
changeset

344 
subsection {* Alternative induction rule for types *} 
9622  345 

11935  346 
lemma type_induct [induct type]: 
18241  347 
assumes 
11945  348 
"(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow> 
18241  349 
(\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)" 
350 
shows "P T" 

351 
proof (induct T) 

352 
case Atom 

23464  353 
show ?case by (rule assms) simp_all 
18241  354 
next 
355 
case Fun 

23464  356 
show ?case by (rule assms) (insert Fun, simp_all) 
11935  357 
qed 
358 

11638  359 
end 