# HG changeset patch # User blanchet # Date 1354574629 -3600 # Node ID 1d9a31b58053cddf19928f193ef3a0b9c599756a # Parent b17b05c8d4a43da80c3de5675f9df6bf02b2bfdc renamed "Type.thy" to something that's less likely to cause conflicts diff -r b17b05c8d4a4 -r 1d9a31b58053 src/HOL/Proofs/Lambda/LambdaType.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy Mon Dec 03 23:43:49 2012 +0100 @@ -0,0 +1,365 @@ +(* Title: HOL/Proofs/Lambda/LambdaType.thy + Author: Stefan Berghofer + Copyright 2000 TU Muenchen +*) + +header {* Simply-typed lambda terms *} + +theory LambdaType imports ListApplication begin + + +subsection {* Environments *} + +definition + shift :: "(nat \ 'a) \ nat \ 'a \ nat \ 'a" ("_<_:_>" [90, 0, 0] 91) where + "e = (\j. if j < i then e j else if j = i then a else e (j - 1))" + +notation (xsymbols) + shift ("_\_:_\" [90, 0, 0] 91) + +notation (HTML output) + shift ("_\_:_\" [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) + +inductive typing :: "(nat \ type) \ dB \ type \ bool" ("_ \ _ : _" [50, 50, 50] 50) + where + Var [intro!]: "env x = T \ env \ Var x : T" + | Abs [intro!]: "env\0:T\ \ t : U \ env \ Abs t : (T \ U)" + | App [intro!]: "env \ s : T \ U \ env \ t : T \ env \ (s \ t) : U" + +inductive_cases typing_elims [elim!]: + "e \ Var i : T" + "e \ t \ u : T" + "e \ Abs t : T" + +primrec + typings :: "(nat \ type) \ dB list \ type list \ bool" +where + "typings e [] Ts = (Ts = [])" + | "typings e (t # ts) Ts = + (case Ts of + [] \ False + | T # Ts \ e \ t : T \ typings e ts Ts)" + +abbreviation + typings_rel :: "(nat \ type) \ dB list \ type list \ bool" + ("_ ||- _ : _" [50, 50, 50] 50) where + "env ||- ts : Ts == typings env ts Ts" + +notation (latex) + typings_rel ("_ \ _ : _" [50, 50, 50] 50) + +abbreviation + funs :: "type list \ type \ type" (infixr "=>>" 200) where + "Ts =>> T == foldr Fun Ts T" + +notation (latex) + funs (infixr "\" 200) + + +subsection {* Some examples *} + +schematic_lemma "e \ Abs (Abs (Abs (Var 1 \ (Var 2 \ Var 1 \ Var 0)))) : ?T" + by force + +schematic_lemma "e \ Abs (Abs (Abs (Var 2 \ Var 0 \ (Var 1 \ Var 0)))) : ?T" + by force + + +subsection {* Lists of types *} + +lemma lists_typings: + "e \ ts : Ts \ listsp (\t. \T. e \ t : T) ts" + apply (induct ts arbitrary: Ts) + apply (case_tac Ts) + apply simp + apply (rule listsp.Nil) + apply simp + apply (case_tac Ts) + apply simp + apply simp + apply (rule listsp.Cons) + apply blast + apply blast + done + +lemma types_snoc: "e \ ts : Ts \ e \ t : T \ e \ ts @ [t] : Ts @ [T]" + apply (induct ts arbitrary: Ts) + apply simp + apply (case_tac Ts) + apply simp+ + done + +lemma types_snoc_eq: "e \ ts @ [t] : Ts @ [T] = + (e \ ts : Ts \ e \ t : T)" + apply (induct ts arbitrary: Ts) + apply (case_tac Ts) + apply simp+ + apply (case_tac Ts) + apply (case_tac "ts @ [t]") + apply simp+ + done + +lemma rev_exhaust2 [extraction_expand]: + obtains (Nil) "xs = []" | (snoc) ys y where "xs = ys @ [y]" + -- {* Cannot use @{text rev_exhaust} from the @{text List} + theory, since it is not constructive *} + apply (subgoal_tac "\ys. xs = rev ys \ thesis") + 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 \ ts @ [t] : Ts \ + (\Us U. Ts = Us @ [U] \ e \ ts : Us \ e \ 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: + "e \ t \\ ts : T \ \Ts. e \ t : Ts \ T \ e \ ts : Ts" + apply (induct ts arbitrary: t T) + 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 \ t \ u : T" for t u T) + apply (rule_tac x = "Ta # Ts" in exI) + apply simp + done + +lemma list_app_typeE: + "e \ t \\ ts : T \ (\Ts. e \ t : Ts \ T \ e \ ts : Ts \ C) \ C" + by (insert list_app_typeD) fast + +lemma list_app_typeI: + "e \ t : Ts \ T \ e \ ts : Ts \ e \ t \\ ts : T" + apply (induct ts arbitrary: t T 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: + "e \ Var i \\ ts : T \ e \ Var i \\ ts : U \ T = U" + apply (induct ts arbitrary: T U rule: rev_induct) + apply simp + apply (ind_cases "e \ Var i : T" for T) + apply (ind_cases "e \ Var i : T" for T) + apply simp + apply simp + apply (ind_cases "e \ t \ u : T" for t u T) + apply (ind_cases "e \ t \ u : T" for 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: "e \ Var i \\ ts \\ us : T \ e \ ts : Ts \ + e \ Var i \\ ts : U \ \Us. U = Us \ T \ e \ us : Us" + apply (induct us arbitrary: ts Ts U) + 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 \ t \ u : T" for t u T) + apply (drule_tac T="Atom nat" and U="Ta \ Tsa \ 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 \ t \ u : T" for t u T) + apply (drule_tac T="type1 \ type2" and U="Ta \ Tsa \ 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 \ t \ u : T" for t u T) + apply (frule_tac T="type1 \ type2" and U="Ta \ Tsa \ 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 \ t \ u : T" for t u T) + apply (frule_tac T="type1 \ Us \ T" and U="Ta \ Tsa \ T" in var_app_type_eq) + apply assumption + apply simp + done + +lemma var_app_typesE: "e \ Var i \\ ts : T \ + (\Ts. e \ Var i : Ts \ T \ e \ ts : Ts \ P) \ P" + apply (drule var_app_types [of _ _ "[]", simplified]) + apply (iprover intro: typing.Var)+ + done + +lemma abs_typeE: "e \ Abs t : T \ (\U V. e\0:U\ \ t : V \ P) \ P" + apply (cases T) + apply (rule FalseE) + apply (erule typing.cases) + 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.cases) + apply simp_all + done + + +subsection {* Lifting preserves well-typedness *} + +lemma lift_type [intro!]: "e \ t : T \ e\i:U\ \ lift t i : T" + by (induct arbitrary: i U set: typing) auto + +lemma lift_types: + "e \ ts : Ts \ e\i:U\ \ (map (\t. lift t i) ts) : Ts" + apply (induct ts arbitrary: Ts) + apply simp + apply (case_tac Ts) + apply auto + done + + +subsection {* Substitution lemmas *} + +lemma subst_lemma: + "e \ t : T \ e' \ u : U \ e = e'\i:U\ \ e' \ t[u/i] : T" + apply (induct arbitrary: e' i U u set: typing) + apply (rule_tac x = x and y = i in linorder_cases) + apply auto + apply blast + done + +lemma substs_lemma: + "e \ u : T \ e\i:T\ \ ts : Ts \ + e \ (map (\t. t[u/i]) ts) : Ts" + apply (induct ts arbitrary: 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 \ t : T \ t \\<^sub>\ t' \ e \ t' : T" + apply (induct arbitrary: t' set: typing) + apply blast + apply blast + apply atomize + apply (ind_cases "s \ t \\<^sub>\ t'" for s t t') + apply hypsubst + apply (ind_cases "env \ Abs t : T \ U" for env 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 \\<^sub>\\<^sup>* t' \ e \ t : T \ e \ t' : T" + by (induct set: rtranclp) (iprover intro: subject_reduction)+ + + +subsection {* Alternative induction rule for types *} + +lemma type_induct [induct type]: + assumes + "(\T. (\T1 T2. T = T1 \ T2 \ P T1) \ + (\T1 T2. T = T1 \ T2 \ P T2) \ P T)" + shows "P T" +proof (induct T) + case Atom + show ?case by (rule assms) simp_all +next + case Fun + show ?case by (rule assms) (insert Fun, simp_all) +qed + +end diff -r b17b05c8d4a4 -r 1d9a31b58053 src/HOL/Proofs/Lambda/StrongNorm.thy --- a/src/HOL/Proofs/Lambda/StrongNorm.thy Mon Dec 03 20:55:34 2012 +0100 +++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Mon Dec 03 23:43:49 2012 +0100 @@ -5,7 +5,7 @@ header {* Strong normalization for simply-typed lambda calculus *} -theory StrongNorm imports Type InductTermi begin +theory StrongNorm imports LambdaType InductTermi begin text {* Formalization by Stefan Berghofer. Partly based on a paper proof by diff -r b17b05c8d4a4 -r 1d9a31b58053 src/HOL/Proofs/Lambda/Type.thy --- a/src/HOL/Proofs/Lambda/Type.thy Mon Dec 03 20:55:34 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,365 +0,0 @@ -(* Title: HOL/Proofs/Lambda/Type.thy - Author: Stefan Berghofer - Copyright 2000 TU Muenchen -*) - -header {* Simply-typed lambda terms *} - -theory Type imports ListApplication begin - - -subsection {* Environments *} - -definition - shift :: "(nat \ 'a) \ nat \ 'a \ nat \ 'a" ("_<_:_>" [90, 0, 0] 91) where - "e = (\j. if j < i then e j else if j = i then a else e (j - 1))" - -notation (xsymbols) - shift ("_\_:_\" [90, 0, 0] 91) - -notation (HTML output) - shift ("_\_:_\" [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) - -inductive typing :: "(nat \ type) \ dB \ type \ bool" ("_ \ _ : _" [50, 50, 50] 50) - where - Var [intro!]: "env x = T \ env \ Var x : T" - | Abs [intro!]: "env\0:T\ \ t : U \ env \ Abs t : (T \ U)" - | App [intro!]: "env \ s : T \ U \ env \ t : T \ env \ (s \ t) : U" - -inductive_cases typing_elims [elim!]: - "e \ Var i : T" - "e \ t \ u : T" - "e \ Abs t : T" - -primrec - typings :: "(nat \ type) \ dB list \ type list \ bool" -where - "typings e [] Ts = (Ts = [])" - | "typings e (t # ts) Ts = - (case Ts of - [] \ False - | T # Ts \ e \ t : T \ typings e ts Ts)" - -abbreviation - typings_rel :: "(nat \ type) \ dB list \ type list \ bool" - ("_ ||- _ : _" [50, 50, 50] 50) where - "env ||- ts : Ts == typings env ts Ts" - -notation (latex) - typings_rel ("_ \ _ : _" [50, 50, 50] 50) - -abbreviation - funs :: "type list \ type \ type" (infixr "=>>" 200) where - "Ts =>> T == foldr Fun Ts T" - -notation (latex) - funs (infixr "\" 200) - - -subsection {* Some examples *} - -schematic_lemma "e \ Abs (Abs (Abs (Var 1 \ (Var 2 \ Var 1 \ Var 0)))) : ?T" - by force - -schematic_lemma "e \ Abs (Abs (Abs (Var 2 \ Var 0 \ (Var 1 \ Var 0)))) : ?T" - by force - - -subsection {* Lists of types *} - -lemma lists_typings: - "e \ ts : Ts \ listsp (\t. \T. e \ t : T) ts" - apply (induct ts arbitrary: Ts) - apply (case_tac Ts) - apply simp - apply (rule listsp.Nil) - apply simp - apply (case_tac Ts) - apply simp - apply simp - apply (rule listsp.Cons) - apply blast - apply blast - done - -lemma types_snoc: "e \ ts : Ts \ e \ t : T \ e \ ts @ [t] : Ts @ [T]" - apply (induct ts arbitrary: Ts) - apply simp - apply (case_tac Ts) - apply simp+ - done - -lemma types_snoc_eq: "e \ ts @ [t] : Ts @ [T] = - (e \ ts : Ts \ e \ t : T)" - apply (induct ts arbitrary: Ts) - apply (case_tac Ts) - apply simp+ - apply (case_tac Ts) - apply (case_tac "ts @ [t]") - apply simp+ - done - -lemma rev_exhaust2 [extraction_expand]: - obtains (Nil) "xs = []" | (snoc) ys y where "xs = ys @ [y]" - -- {* Cannot use @{text rev_exhaust} from the @{text List} - theory, since it is not constructive *} - apply (subgoal_tac "\ys. xs = rev ys \ thesis") - 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 \ ts @ [t] : Ts \ - (\Us U. Ts = Us @ [U] \ e \ ts : Us \ e \ 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: - "e \ t \\ ts : T \ \Ts. e \ t : Ts \ T \ e \ ts : Ts" - apply (induct ts arbitrary: t T) - 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 \ t \ u : T" for t u T) - apply (rule_tac x = "Ta # Ts" in exI) - apply simp - done - -lemma list_app_typeE: - "e \ t \\ ts : T \ (\Ts. e \ t : Ts \ T \ e \ ts : Ts \ C) \ C" - by (insert list_app_typeD) fast - -lemma list_app_typeI: - "e \ t : Ts \ T \ e \ ts : Ts \ e \ t \\ ts : T" - apply (induct ts arbitrary: t T 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: - "e \ Var i \\ ts : T \ e \ Var i \\ ts : U \ T = U" - apply (induct ts arbitrary: T U rule: rev_induct) - apply simp - apply (ind_cases "e \ Var i : T" for T) - apply (ind_cases "e \ Var i : T" for T) - apply simp - apply simp - apply (ind_cases "e \ t \ u : T" for t u T) - apply (ind_cases "e \ t \ u : T" for 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: "e \ Var i \\ ts \\ us : T \ e \ ts : Ts \ - e \ Var i \\ ts : U \ \Us. U = Us \ T \ e \ us : Us" - apply (induct us arbitrary: ts Ts U) - 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 \ t \ u : T" for t u T) - apply (drule_tac T="Atom nat" and U="Ta \ Tsa \ 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 \ t \ u : T" for t u T) - apply (drule_tac T="type1 \ type2" and U="Ta \ Tsa \ 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 \ t \ u : T" for t u T) - apply (frule_tac T="type1 \ type2" and U="Ta \ Tsa \ 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 \ t \ u : T" for t u T) - apply (frule_tac T="type1 \ Us \ T" and U="Ta \ Tsa \ T" in var_app_type_eq) - apply assumption - apply simp - done - -lemma var_app_typesE: "e \ Var i \\ ts : T \ - (\Ts. e \ Var i : Ts \ T \ e \ ts : Ts \ P) \ P" - apply (drule var_app_types [of _ _ "[]", simplified]) - apply (iprover intro: typing.Var)+ - done - -lemma abs_typeE: "e \ Abs t : T \ (\U V. e\0:U\ \ t : V \ P) \ P" - apply (cases T) - apply (rule FalseE) - apply (erule typing.cases) - 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.cases) - apply simp_all - done - - -subsection {* Lifting preserves well-typedness *} - -lemma lift_type [intro!]: "e \ t : T \ e\i:U\ \ lift t i : T" - by (induct arbitrary: i U set: typing) auto - -lemma lift_types: - "e \ ts : Ts \ e\i:U\ \ (map (\t. lift t i) ts) : Ts" - apply (induct ts arbitrary: Ts) - apply simp - apply (case_tac Ts) - apply auto - done - - -subsection {* Substitution lemmas *} - -lemma subst_lemma: - "e \ t : T \ e' \ u : U \ e = e'\i:U\ \ e' \ t[u/i] : T" - apply (induct arbitrary: e' i U u set: typing) - apply (rule_tac x = x and y = i in linorder_cases) - apply auto - apply blast - done - -lemma substs_lemma: - "e \ u : T \ e\i:T\ \ ts : Ts \ - e \ (map (\t. t[u/i]) ts) : Ts" - apply (induct ts arbitrary: 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 \ t : T \ t \\<^sub>\ t' \ e \ t' : T" - apply (induct arbitrary: t' set: typing) - apply blast - apply blast - apply atomize - apply (ind_cases "s \ t \\<^sub>\ t'" for s t t') - apply hypsubst - apply (ind_cases "env \ Abs t : T \ U" for env 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 \\<^sub>\\<^sup>* t' \ e \ t : T \ e \ t' : T" - by (induct set: rtranclp) (iprover intro: subject_reduction)+ - - -subsection {* Alternative induction rule for types *} - -lemma type_induct [induct type]: - assumes - "(\T. (\T1 T2. T = T1 \ T2 \ P T1) \ - (\T1 T2. T = T1 \ T2 \ P T2) \ P T)" - shows "P T" -proof (induct T) - case Atom - show ?case by (rule assms) simp_all -next - case Fun - show ?case by (rule assms) (insert Fun, simp_all) -qed - -end diff -r b17b05c8d4a4 -r 1d9a31b58053 src/HOL/Proofs/Lambda/WeakNorm.thy --- a/src/HOL/Proofs/Lambda/WeakNorm.thy Mon Dec 03 20:55:34 2012 +0100 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Mon Dec 03 23:43:49 2012 +0100 @@ -6,7 +6,7 @@ header {* Weak normalization for simply-typed lambda calculus *} theory WeakNorm -imports Type NormalForm "~~/src/HOL/Library/Code_Integer" +imports LambdaType NormalForm "~~/src/HOL/Library/Code_Integer" begin text {*