1(* Title: HOL/Proofs/Lambda/LambdaType.thy 2 Author: Stefan Berghofer 3 Copyright 2000 TU Muenchen 4*) 5 6section \<open>Simply-typed lambda terms\<close> 7 8theory LambdaType imports ListApplication begin 9 10 11subsection \<open>Environments\<close> 12 13definition 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))" 16 17lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T" 18 by (simp add: shift_def) 19 20lemma shift_gt [simp]: "j < i \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e j" 21 by (simp add: shift_def) 22 23lemma shift_lt [simp]: "i < j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e (j - 1)" 24 by (simp add: shift_def) 25 26lemma shift_commute [simp]: "e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>" 27 by (rule ext) (simp_all add: shift_def split: nat.split) 28 29 30subsection \<open>Types and typing rules\<close> 31 32datatype type = 33 Atom nat 34 | Fun type type (infixr "\<Rightarrow>" 200) 35 36inductive typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) 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 42inductive_cases typing_elims [elim!]: 43 "e \<turnstile> Var i : T" 44 "e \<turnstile> t \<degree> u : T" 45 "e \<turnstile> Abs t : T" 46 47primrec 48 typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" 49where 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)" 55 56abbreviation 57 typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool" 58 ("_ \<tturnstile> _ : _" [50, 50, 50] 50) where 59 "env \<tturnstile> ts : Ts == typings env ts Ts" 60 61abbreviation 62 funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "\<Rrightarrow>" 200) where 63 "Ts \<Rrightarrow> T == foldr Fun Ts T" 64 65 66subsection \<open>Some examples\<close> 67 68schematic_goal "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T" 69 by force 70 71schematic_goal "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T" 72 by force 73 74 75subsection \<open>Lists of types\<close> 76 77lemma lists_typings: 78 "e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts" 79 apply (induct ts arbitrary: Ts) 80 apply (case_tac Ts) 81 apply simp 82 apply (rule listsp.Nil) 83 apply simp 84 apply (case_tac Ts) 85 apply simp 86 apply simp 87 apply (rule listsp.Cons) 88 apply blast 89 apply blast 90 done 91 92lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]" 93 apply (induct ts arbitrary: Ts) 94 apply simp 95 apply (case_tac Ts) 96 apply simp+ 97 done 98 99lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] = 100 (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" 101 apply (induct ts arbitrary: Ts) 102 apply (case_tac Ts) 103 apply simp+ 104 apply (case_tac Ts) 105 apply (case_tac "ts @ [t]") 106 apply simp+ 107 done 108 109lemma rev_exhaust2 [extraction_expand]: 110 obtains (Nil) "xs = []" | (snoc) ys y where "xs = ys @ [y]" 111 \<comment> \<open>Cannot use \<open>rev_exhaust\<close> from the \<open>List\<close> 112 theory, since it is not constructive\<close> 113 apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> thesis") 114 apply (erule_tac x="rev xs" in allE) 115 apply simp 116 apply (rule allI) 117 apply (rule impI) 118 apply (case_tac ys) 119 apply simp 120 apply simp 121 done 122 123lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow> 124 (\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> P" 125 apply (cases Ts rule: rev_exhaust2) 126 apply simp 127 apply (case_tac "ts @ [t]") 128 apply (simp add: types_snoc_eq)+ 129 done 130 131 132subsection \<open>n-ary function types\<close> 133 134lemma list_app_typeD: 135 "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts" 136 apply (induct ts arbitrary: t T) 137 apply simp 138 apply (rename_tac a b t T) 139 apply atomize 140 apply simp 141 apply (erule_tac x = "t \<degree> a" in allE) 142 apply (erule_tac x = T in allE) 143 apply (erule impE) 144 apply assumption 145 apply (elim exE conjE) 146 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 147 apply (rule_tac x = "Ta # Ts" in exI) 148 apply simp 149 done 150 151lemma list_app_typeE: 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" 153 by (insert list_app_typeD) fast 154 155lemma list_app_typeI: 156 "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T" 157 apply (induct ts arbitrary: t T Ts) 158 apply simp 159 apply (rename_tac a b t T Ts) 160 apply atomize 161 apply (case_tac Ts) 162 apply simp 163 apply simp 164 apply (erule_tac x = "t \<degree> a" in allE) 165 apply (erule_tac x = T in allE) 166 apply (rename_tac list) 167 apply (erule_tac x = list in allE) 168 apply (erule impE) 169 apply (erule conjE) 170 apply (erule typing.App) 171 apply assumption 172 apply blast 173 done 174 175text \<open> 176For the specific case where the head of the term is a variable, 177the following theorems allow to infer the types of the arguments 178without analyzing the typing derivation. This is crucial 179for program extraction. 180\<close> 181 182theorem var_app_type_eq: 183 "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U" 184 apply (induct ts arbitrary: T U rule: rev_induct) 185 apply simp 186 apply (ind_cases "e \<turnstile> Var i : T" for T) 187 apply (ind_cases "e \<turnstile> Var i : T" for T) 188 apply simp 189 apply simp 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) 192 apply atomize 193 apply (erule_tac x="Ta \<Rightarrow> T" in allE) 194 apply (erule_tac x="Tb \<Rightarrow> U" in allE) 195 apply (erule impE) 196 apply assumption 197 apply (erule impE) 198 apply assumption 199 apply simp 200 done 201 202lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> 203 e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us" 204 apply (induct us arbitrary: ts Ts U) 205 apply simp 206 apply (erule var_app_type_eq) 207 apply assumption 208 apply simp 209 apply (rename_tac a b ts Ts U) 210 apply atomize 211 apply (case_tac U) 212 apply (rule FalseE) 213 apply simp 214 apply (erule list_app_typeE) 215 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 216 apply (rename_tac nat Tsa Ta) 217 apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) 218 apply assumption 219 apply simp 220 apply (rename_tac nat type1 type2) 221 apply (erule_tac x="ts @ [a]" in allE) 222 apply (erule_tac x="Ts @ [type1]" in allE) 223 apply (erule_tac x="type2" in allE) 224 apply simp 225 apply (erule impE) 226 apply (rule types_snoc) 227 apply assumption 228 apply (erule list_app_typeE) 229 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 230 apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) 231 apply assumption 232 apply simp 233 apply (erule impE) 234 apply (rule typing.App) 235 apply assumption 236 apply (erule list_app_typeE) 237 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 238 apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) 239 apply assumption 240 apply simp 241 apply (erule exE) 242 apply (rule_tac x="type1 # Us" in exI) 243 apply simp 244 apply (erule list_app_typeE) 245 apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T) 246 apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq) 247 apply assumption 248 apply simp 249 done 250 251lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> 252 (\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P" 253 apply (drule var_app_types [of _ _ "[]", simplified]) 254 apply (iprover intro: typing.Var)+ 255 done 256 257lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P" 258 apply (cases T) 259 apply (rule FalseE) 260 apply (erule typing.cases) 261 apply simp_all 262 apply atomize 263 apply (rename_tac type1 type2) 264 apply (erule_tac x="type1" in allE) 265 apply (erule_tac x="type2" in allE) 266 apply (erule mp) 267 apply (erule typing.cases) 268 apply simp_all 269 done 270 271 272subsection \<open>Lifting preserves well-typedness\<close> 273 274lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T" 275 by (induct arbitrary: i U set: typing) auto 276 277lemma lift_types: 278 "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts" 279 apply (induct ts arbitrary: Ts) 280 apply simp 281 apply (case_tac Ts) 282 apply auto 283 done 284 285 286subsection \<open>Substitution lemmas\<close> 287 288lemma subst_lemma: 289 "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T" 290 apply (induct arbitrary: e' i U u set: typing) 291 apply (rule_tac x = x and y = i in linorder_cases) 292 apply auto 293 apply blast 294 done 295 296lemma substs_lemma: 297 "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow> 298 e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts" 299 apply (induct ts arbitrary: Ts) 300 apply (case_tac Ts) 301 apply simp 302 apply simp 303 apply atomize 304 apply (case_tac Ts) 305 apply simp 306 apply simp 307 apply (erule conjE) 308 apply (erule (1) subst_lemma) 309 apply (rule refl) 310 done 311 312 313subsection \<open>Subject reduction\<close> 314 315lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T" 316 apply (induct arbitrary: t' set: typing) 317 apply blast 318 apply blast 319 apply atomize 320 apply (ind_cases "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t') 321 apply hypsubst 322 apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U) 323 apply (rule subst_lemma) 324 apply assumption 325 apply assumption 326 apply (rule ext) 327 apply (case_tac x) 328 apply auto 329 done 330 331theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T" 332 by (induct set: rtranclp) (iprover intro: subject_reduction)+ 333 334 335subsection \<open>Alternative induction rule for types\<close> 336 337lemma type_induct [induct type]: 338 assumes 339 "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow> 340 (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)" 341 shows "P T" 342proof (induct T) 343 case Atom 344 show ?case by (rule assms) simp_all 345next 346 case Fun 347 show ?case by (rule assms) (insert Fun, simp_all) 348qed 349 350end 351