(* Title: HOL/Lambda/Type.thy ID: $Id: Type.thy,v 1.31 2005/09/22 21:56:35 nipkow Exp $ Author: Stefan Berghofer Copyright 2000 TU Muenchen *) header {* Simply-typed lambda terms *} theory Type imports ListApplication begin subsection {* Environments *} constdefs shift :: "(nat => 'a) => nat => 'a => nat => 'a" ("_<_:_>" [90, 0, 0] 91) "e<i:a> ≡ λj. if j < i then e j else if j = i then a else e (j - 1)" syntax (xsymbols) shift :: "(nat => 'a) => nat => 'a => nat => 'a" ("_〈_:_〉" [90, 0, 0] 91) syntax (HTML output) shift :: "(nat => 'a) => nat => 'a => nat => 'a" ("_〈_:_〉" [90, 0, 0] 91) lemma shift_eq [simp]: "i = j ==> (e〈i:T〉) j = T" by (simp add: shift_def) lemma shift_gt [simp]: "j < i ==> (e〈i:T〉) j = e j" by (simp add: shift_def) lemma shift_lt [simp]: "i < j ==> (e〈i:T〉) j = e (j - 1)" by (simp add: shift_def) lemma shift_commute [simp]: "e〈i:U〉〈0:T〉 = e〈0:T〉〈Suc i:U〉" apply (rule ext) apply (case_tac x) apply simp apply (case_tac nat) apply (simp_all add: shift_def) done subsection {* Types and typing rules *} datatype type = Atom nat | Fun type type (infixr "=>" 200) consts typing :: "((nat => type) × dB × type) set" typings :: "(nat => type) => dB list => type list => bool" syntax "_funs" :: "type list => type => type" (infixr "=>>" 200) "_typing" :: "(nat => type) => dB => type => bool" ("_ |- _ : _" [50, 50, 50] 50) "_typings" :: "(nat => type) => dB list => type list => bool" ("_ ||- _ : _" [50, 50, 50] 50) syntax (xsymbols) "_typing" :: "(nat => type) => dB => type => bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) syntax (latex) "_funs" :: "type list => type => type" (infixr "\<Rrightarrow>" 200) "_typings" :: "(nat => type) => dB list => type list => bool" ("_ \<tturnstile> _ : _" [50, 50, 50] 50) translations "Ts \<Rrightarrow> T" \<rightleftharpoons> "foldr Fun Ts T" "env \<turnstile> t : T" \<rightleftharpoons> "(env, t, T) ∈ typing" "env \<tturnstile> ts : Ts" \<rightleftharpoons> "typings env ts Ts" inductive typing intros Var [intro!]: "env x = T ==> env \<turnstile> Var x : T" Abs [intro!]: "env〈0:T〉 \<turnstile> t : U ==> env \<turnstile> Abs t : (T => U)" App [intro!]: "env \<turnstile> s : T => U ==> env \<turnstile> t : T ==> env \<turnstile> (s ° t) : U" inductive_cases typing_elims [elim!]: "e \<turnstile> Var i : T" "e \<turnstile> t ° u : T" "e \<turnstile> Abs t : T" primrec "(e \<tturnstile> [] : Ts) = (Ts = [])" "(e \<tturnstile> (t # ts) : Ts) = (case Ts of [] => False | T # Ts => e \<turnstile> t : T ∧ e \<tturnstile> ts : Ts)" subsection {* Some examples *} lemma "e \<turnstile> Abs (Abs (Abs (Var 1 ° (Var 2 ° Var 1 ° Var 0)))) : ?T" by force lemma "e \<turnstile> Abs (Abs (Abs (Var 2 ° Var 0 ° (Var 1 ° Var 0)))) : ?T" by force subsection {* Lists of types *} lemma lists_typings: "!!Ts. e \<tturnstile> ts : Ts ==> ts ∈ lists {t. ∃T. e \<turnstile> t : T}" apply (induct ts) apply (case_tac Ts) apply simp apply (rule lists.Nil) apply simp apply (case_tac Ts) apply simp apply simp apply (rule lists.Cons) apply blast apply blast done lemma types_snoc: "!!Ts. e \<tturnstile> ts : Ts ==> e \<turnstile> t : T ==> e \<tturnstile> ts @ [t] : Ts @ [T]" apply (induct ts) apply simp apply (case_tac Ts) apply simp+ done lemma types_snoc_eq: "!!Ts. e \<tturnstile> ts @ [t] : Ts @ [T] = (e \<tturnstile> ts : Ts ∧ e \<turnstile> t : T)" apply (induct ts) apply (case_tac Ts) apply simp+ apply (case_tac Ts) apply (case_tac "ts @ [t]") apply simp+ done lemma rev_exhaust2 [case_names Nil snoc, extraction_expand]: "(xs = [] ==> P) ==> (!!ys y. xs = ys @ [y] ==> P) ==> P" -- {* Cannot use @{text rev_exhaust} from the @{text List} theory, since it is not constructive *} apply (subgoal_tac "∀ys. xs = rev ys --> P") apply (erule_tac x="rev xs" in allE) apply simp apply (rule allI) apply (rule impI) apply (case_tac ys) apply simp apply simp apply atomize apply (erule allE)+ apply (erule mp, rule conjI) apply (rule refl)+ done lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts ==> (!!Us U. Ts = Us @ [U] ==> e \<tturnstile> ts : Us ==> e \<turnstile> t : U ==> P) ==> P" apply (cases Ts rule: rev_exhaust2) apply simp apply (case_tac "ts @ [t]") apply (simp add: types_snoc_eq)+ apply iprover done subsection {* n-ary function types *} lemma list_app_typeD: "!!t T. e \<turnstile> t °° ts : T ==> ∃Ts. e \<turnstile> t : Ts \<Rrightarrow> T ∧ e \<tturnstile> ts : Ts" apply (induct ts) apply simp apply atomize apply simp apply (erule_tac x = "t ° a" in allE) apply (erule_tac x = T in allE) apply (erule impE) apply assumption apply (elim exE conjE) apply (ind_cases "e \<turnstile> t ° u : T") apply (rule_tac x = "Ta # Ts" in exI) apply simp done lemma list_app_typeE: "e \<turnstile> t °° ts : T ==> (!!Ts. e \<turnstile> t : Ts \<Rrightarrow> T ==> e \<tturnstile> ts : Ts ==> C) ==> C" by (insert list_app_typeD) fast lemma list_app_typeI: "!!t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T ==> e \<tturnstile> ts : Ts ==> e \<turnstile> t °° ts : T" apply (induct ts) apply simp apply atomize apply (case_tac Ts) apply simp apply simp apply (erule_tac x = "t ° a" in allE) apply (erule_tac x = T in allE) apply (erule_tac x = list in allE) apply (erule impE) apply (erule conjE) apply (erule typing.App) apply assumption apply blast done text {* For the specific case where the head of the term is a variable, the following theorems allow to infer the types of the arguments without analyzing the typing derivation. This is crucial for program extraction. *} theorem var_app_type_eq: "!!T U. e \<turnstile> Var i °° ts : T ==> e \<turnstile> Var i °° ts : U ==> T = U" apply (induct ts rule: rev_induct) apply simp apply (ind_cases "e \<turnstile> Var i : T") apply (ind_cases "e \<turnstile> Var i : T") apply simp apply simp apply (ind_cases "e \<turnstile> t ° u : T") apply (ind_cases "e \<turnstile> t ° u : T") apply atomize apply (erule_tac x="Ta => T" in allE) apply (erule_tac x="Tb => U" in allE) apply (erule impE) apply assumption apply (erule impE) apply assumption apply simp done lemma var_app_types: "!!ts Ts U. e \<turnstile> Var i °° ts °° us : T ==> e \<tturnstile> ts : Ts ==> e \<turnstile> Var i °° ts : U ==> ∃Us. U = Us \<Rrightarrow> T ∧ e \<tturnstile> us : Us" apply (induct us) apply simp apply (erule var_app_type_eq) apply assumption apply simp apply atomize apply (case_tac U) apply (rule FalseE) apply simp apply (erule list_app_typeE) apply (ind_cases "e \<turnstile> t ° u : T") apply (drule_tac T="Atom nat" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq) apply assumption apply simp apply (erule_tac x="ts @ [a]" in allE) apply (erule_tac x="Ts @ [type1]" in allE) apply (erule_tac x="type2" in allE) apply simp apply (erule impE) apply (rule types_snoc) apply assumption apply (erule list_app_typeE) apply (ind_cases "e \<turnstile> t ° u : T") apply (drule_tac T="type1 => type2" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq) apply assumption apply simp apply (erule impE) apply (rule typing.App) apply assumption apply (erule list_app_typeE) apply (ind_cases "e \<turnstile> t ° u : T") apply (frule_tac T="type1 => type2" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq) apply assumption apply simp apply (erule exE) apply (rule_tac x="type1 # Us" in exI) apply simp apply (erule list_app_typeE) apply (ind_cases "e \<turnstile> t ° u : T") apply (frule_tac T="type1 => Us \<Rrightarrow> T" and U="Ta => Tsa \<Rrightarrow> T" in var_app_type_eq) apply assumption apply simp done lemma var_app_typesE: "e \<turnstile> Var i °° ts : T ==> (!!Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T ==> e \<tturnstile> ts : Ts ==> P) ==> P" apply (drule var_app_types [of _ _ "[]", simplified]) apply (iprover intro: typing.Var)+ done lemma abs_typeE: "e \<turnstile> Abs t : T ==> (!!U V. e〈0:U〉 \<turnstile> t : V ==> P) ==> P" apply (cases T) apply (rule FalseE) apply (erule typing.elims) apply simp_all apply atomize apply (erule_tac x="type1" in allE) apply (erule_tac x="type2" in allE) apply (erule mp) apply (erule typing.elims) apply simp_all done subsection {* Lifting preserves well-typedness *} lemma lift_type [intro!]: "e \<turnstile> t : T ==> (!!i U. e〈i:U〉 \<turnstile> lift t i : T)" by (induct set: typing) auto lemma lift_types: "!!Ts. e \<tturnstile> ts : Ts ==> e〈i:U〉 \<tturnstile> (map (λt. lift t i) ts) : Ts" apply (induct ts) apply simp apply (case_tac Ts) apply auto done subsection {* Substitution lemmas *} lemma subst_lemma: "e \<turnstile> t : T ==> (!!e' i U u. e' \<turnstile> u : U ==> e = e'〈i:U〉 ==> e' \<turnstile> t[u/i] : T)" apply (induct set: typing) apply (rule_tac x = x and y = i in linorder_cases) apply auto apply blast done lemma substs_lemma: "!!Ts. e \<turnstile> u : T ==> e〈i:T〉 \<tturnstile> ts : Ts ==> e \<tturnstile> (map (λt. t[u/i]) ts) : Ts" apply (induct ts) apply (case_tac Ts) apply simp apply simp apply atomize apply (case_tac Ts) apply simp apply simp apply (erule conjE) apply (erule (1) subst_lemma) apply (rule refl) done subsection {* Subject reduction *} lemma subject_reduction: "e \<turnstile> t : T ==> (!!t'. t -> t' ==> e \<turnstile> t' : T)" apply (induct set: typing) apply blast apply blast apply atomize apply (ind_cases "s ° t -> t'") apply hypsubst apply (ind_cases "env \<turnstile> Abs t : T => U") apply (rule subst_lemma) apply assumption apply assumption apply (rule ext) apply (case_tac x) apply auto done theorem subject_reduction': "t ->β* t' ==> e \<turnstile> t : T ==> e \<turnstile> t' : T" by (induct set: rtrancl) (iprover intro: subject_reduction)+ subsection {* Alternative induction rule for types *} lemma type_induct [induct type]: "(!!T. (!!T1 T2. T = T1 => T2 ==> P T1) ==> (!!T1 T2. T = T1 => T2 ==> P T2) ==> P T) ==> P T" proof - case rule_context show ?thesis proof (induct T) case Atom show ?case by (rule rule_context) simp_all next case Fun show ?case by (rule rule_context) (insert Fun, simp_all) qed qed end
lemma shift_eq:
i = j ==> (e〈i:T〉) j = T
lemma shift_gt:
j < i ==> (e〈i:T〉) j = e j
lemma shift_lt:
i < j ==> (e〈i:T〉) j = e (j - 1)
lemma shift_commute:
e〈i:U〉〈0:T〉 = e〈0:T〉〈Suc i:U〉
lemmas typing_elims:
[| e |- Var i : T; T = e i ==> P |] ==> P
[| e |- t ° u : T; !!T. [| e |- t : T => T; e |- u : T |] ==> P |] ==> P
[| e |- Abs t : T; !!T U. [| e〈0:T〉 |- t : U; T = T => U |] ==> P |] ==> P
lemma
e |- Abs (Abs (Abs (Var 1 ° (Var 2 ° Var 1 ° Var 0)))) : ((Ta => U) => T => Ta) => (Ta => U) => T => U
lemma
e |- Abs (Abs (Abs (Var 2 ° Var 0 ° (Var 1 ° Var 0)))) : (T => Ta => U) => (T => Ta) => T => U
lemma lists_typings:
e ||- ts : Ts ==> ts ∈ lists {t. ∃T. e |- t : T}
lemma types_snoc:
[| e ||- ts : Ts; e |- t : T |] ==> e ||- ts @ [t] : Ts @ [T]
lemma types_snoc_eq:
(e ||- ts @ [t] : Ts @ [T]) = (e ||- ts : Ts ∧ e |- t : T)
lemma rev_exhaust2:
[| xs = [] ==> P; !!ys y. xs = ys @ [y] ==> P |] ==> P
lemma types_snocE:
[| e ||- ts @ [t] : Ts; !!Us U. [| Ts = Us @ [U]; e ||- ts : Us; e |- t : U |] ==> P |] ==> P
lemma list_app_typeD:
e |- t °° ts : T ==> ∃Ts. e |- t : Ts =>> T ∧ e ||- ts : Ts
lemma list_app_typeE:
[| e |- t °° ts : T; !!Ts. [| e |- t : Ts =>> T; e ||- ts : Ts |] ==> C |] ==> C
lemma list_app_typeI:
[| e |- t : Ts =>> T; e ||- ts : Ts |] ==> e |- t °° ts : T
theorem var_app_type_eq:
[| e |- Var i °° ts : T; e |- Var i °° ts : U |] ==> T = U
lemma var_app_types:
[| e |- Var i °° ts °° us : T; e ||- ts : Ts; e |- Var i °° ts : U |] ==> ∃Us. U = Us =>> T ∧ e ||- us : Us
lemma var_app_typesE:
[| e |- Var i °° ts : T; !!Ts. [| e |- Var i : Ts =>> T; e ||- ts : Ts |] ==> P |] ==> P
lemma abs_typeE:
[| e |- Abs t : T; !!U V. e〈0:U〉 |- t : V ==> P |] ==> P
lemma lift_type:
e |- t : T ==> e〈i:U〉 |- lift t i : T
lemma lift_types:
e ||- ts : Ts ==> e〈i:U〉 ||- map (%t. lift t i) ts : Ts
lemma subst_lemma:
[| e |- t : T; e' |- u : U; e = e'〈i:U〉 |] ==> e' |- t[u/i] : T
lemma substs_lemma:
[| e |- u : T; e〈i:T〉 ||- ts : Ts |] ==> e ||- map (%t. t[u/i]) ts : Ts
lemma subject_reduction:
[| e |- t : T; t -> t' |] ==> e |- t' : T
theorem subject_reduction':
[| t ->> t'; e |- t : T |] ==> e |- t' : T
lemma type_induct:
(!!T. [| !!T1 T2. T = T1 => T2 ==> P T1; !!T1 T2. T = T1 => T2 ==> P T2 |] ==> P T) ==> P T