# HG changeset patch # User berghofe # Date 1004033083 -7200 # Node ID cbcba2092d6b0e4df55cc11b011ef8d672e2bd31 # Parent 6c1bf72430b6366469ddc22a6d952fe1bafcd9cf Replaced main proof by proper Isar script. diff -r 6c1bf72430b6 -r cbcba2092d6b src/HOL/Lambda/Type.thy --- a/src/HOL/Lambda/Type.thy Thu Oct 25 20:00:11 2001 +0200 +++ b/src/HOL/Lambda/Type.thy Thu Oct 25 20:04:43 2001 +0200 @@ -27,6 +27,7 @@ syntax "_typing" :: "[nat => type, dB, type] => bool" ("_ |- _ : _" [50,50,50] 50) "_funs" :: "[type list, type] => type" (infixl "=>>" 150) + translations "env |- t : T" == "(env, t, T) \ typing" "Ts =>> T" == "foldr Fun Ts T" @@ -37,6 +38,10 @@ Abs [intro!]: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)" App [intro!]: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U" +constdefs + shift :: "(nat \ 'a) \ nat \ 'a \ nat \ 'a" ("_<_:_>" [50,0,0] 51) + "e == \j. if j < i then e j else if j = i then a else e (j - 1)" + inductive_cases [elim!]: "e |- Var i : T" "e |- t $ u : T" @@ -60,15 +65,13 @@ subsection {* Some examples *} lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T" - apply force - done + by force lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T" - apply force - done + by force -text {* Iterated function types *} +subsection {* @{text n}-ary function types *} lemma list_app_typeD [rule_format]: "\t T. e |- t $$ ts : T --> (\Ts. e |- t : Ts =>> T \ types e ts Ts)" @@ -86,6 +89,10 @@ apply simp done +lemma list_app_typeE: + "e |- t $$ ts : T \ (\Ts. e |- t : Ts =>> T \ types e ts Ts \ C) \ C" + by (insert list_app_typeD) fast + lemma list_app_typeI [rule_format]: "\t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T" apply (induct_tac ts) @@ -125,17 +132,13 @@ subsection {* Lifting preserves termination and well-typedness *} -lemma lift_map [rule_format, simp]: - "\t. lift (t $$ ts) i = lift t i $$ map (\t. lift t i) ts" - apply (induct_tac ts) - apply simp_all - done +lemma lift_map [simp]: + "\t. lift (t $$ ts) i = lift t i $$ map (\t. lift t i) ts" + by (induct ts) simp_all -lemma subst_map [rule_format, simp]: - "\t. subst (t $$ ts) u i = subst t u i $$ map (\t. subst t u i) ts" - apply (induct_tac ts) - apply simp_all - done +lemma subst_map [simp]: + "\t. subst (t $$ ts) u i = subst t u i $$ map (\t. subst t u i) ts" + by (induct ts) simp_all lemma lift_IT [rule_format, intro!]: "t \ IT ==> \i. lift t i \ IT" @@ -157,12 +160,9 @@ apply auto done -lemma lifts_IT [rule_format]: - "ts \ lists IT --> map (\t. lift t 0) ts \ lists IT" - apply (induct_tac ts) - apply auto - done - +lemma lifts_IT: + "ts \ lists IT \ map (\t. lift t 0) ts \ lists IT" + by (induct ts) auto lemma shift_env [simp]: "nat_case T @@ -176,33 +176,26 @@ apply simp_all done -lemma lift_type' [rule_format]: - "e |- t : T ==> \i U. - (\j. if j < i then e j - else if j = i then U - else e (j - 1)) |- lift t i : T" - apply (erule typing.induct) - apply auto - done +lemma lift_type': + "e |- t : T ==> e |- lift t i : T" +proof - + assume "e |- t : T" + thus "\i U. e |- lift t i : T" + by induct (auto simp add: shift_def) +qed lemma lift_type [intro!]: "e |- t : T ==> nat_case U e |- lift t 0 : T" - apply (subgoal_tac - "nat_case U e = - (\j. if j < 0 then e j - else if j = 0 then U else e (j - 1))") + apply (subgoal_tac "nat_case U e = e<0:U>") apply (erule ssubst) apply (erule lift_type') apply (rule ext) - apply (case_tac j) - apply simp_all + apply (case_tac x) + apply (simp_all add: shift_def) done lemma lift_types [rule_format]: - "\Ts. types e ts Ts --> - types (\j. if j < i then e j - else if j = i then U - else e (j - 1)) (map (\t. lift t i) ts) Ts" + "\Ts. types e ts Ts --> types (e) (map (\t. lift t i) ts) Ts" apply (induct_tac ts) apply simp apply (intro strip) @@ -216,11 +209,9 @@ subsection {* Substitution lemmas *} lemma subst_lemma [rule_format]: - "e |- t : T ==> \e' i U u. - e = (\j. if j < i then e' j - else if j = i then U - else e' (j - 1)) --> - e' |- u : U --> e' |- t[u/i] : T" + "e |- t : T ==> \e' i U u. e' |- u : U --> + e = e' --> e' |- t[u/i] : T" + apply (unfold shift_def) apply (erule typing.induct) apply (intro strip) apply (case_tac "x = i") @@ -235,14 +226,12 @@ apply (rule typing.Var) apply assumption apply fastsimp - apply fastsimp + apply auto done lemma substs_lemma [rule_format]: - "e |- u : T ==> - \Ts. types (\j. if j < i then e j - else if j = i then T else e (j - 1)) ts Ts --> - types e (map (\t. t[u/i]) ts) Ts" + "e |- u : T ==> \Ts. types (e) ts Ts --> + types e (map (\t. t[u/i]) ts) Ts" apply (induct_tac ts) apply (intro strip) apply (case_tac Ts) @@ -254,8 +243,8 @@ apply simp apply (erule conjE) apply (erule subst_lemma) - apply (rule refl) - apply assumption + apply assumption + apply (rule refl) done @@ -272,19 +261,17 @@ apply (ind_cases "env |- Abs t : T => U") apply (rule subst_lemma) apply assumption - prefer 2 apply assumption apply (rule ext) - apply (case_tac j) - apply auto + apply (case_tac x) + apply (auto simp add: shift_def) done subsection {* Additional lemmas *} lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])" - apply simp - done + by simp lemma subst_Var_IT [rule_format]: "r \ IT ==> \i j. r[Var i/j] \ IT" apply (erule IT.induct) @@ -340,130 +327,215 @@ apply assumption done +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 + subsection {* Well-typed substitution preserves termination *} -lemma subst_type_IT [rule_format]: - "\t. t \ IT --> (\e T u i. - (\j. if j < i then e j - else if j = i then U - else e (j - 1)) |- t : T --> - u \ IT --> e |- u : U --> t[u/i] \ IT)" - apply (rule_tac f = size and a = U in measure_induct) - apply (rule allI) - apply (rule impI) - apply (erule IT.induct) - txt {* Case @{term Var}: *} - apply (intro strip) - apply (case_tac "n = i") - txt {* Case @{term "n = i"}: *} - apply (case_tac rs) - apply simp - apply simp - apply (drule list_app_typeD) - apply (elim exE conjE) - apply (ind_cases "e |- t $ u : T") - apply (ind_cases "e |- Var i : T") - apply (drule_tac s = "(?T::type) => ?U" in sym) - apply simp - apply (subgoal_tac "lift u 0 $ Var 0 \ IT") - prefer 2 - apply (rule app_Var_IT) - apply (erule lift_IT) - apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] \ IT") - apply (simp (no_asm_use)) - apply (subgoal_tac "(Var 0 $$ map (\t. lift t 0) - (map (\t. t[u/i]) list))[(u $ a[u/i])/0] \ IT") - apply (simp (no_asm_use) del: map_compose - add: map_compose [symmetric] o_def) - apply (erule_tac x = "Ts =>> T" in allE) - apply (erule impE) - apply simp - apply (erule_tac x = "Var 0 $$ - map (\t. lift t 0) (map (\t. t[u/i]) list)" in allE) - apply (erule impE) - apply (rule IT.Var) - apply (rule lifts_IT) - apply (drule lists_types) - apply - (ind_cases "x # xs \ lists (Collect P)", - erule lists_IntI [THEN lists.induct], - assumption) - apply fastsimp - apply fastsimp - apply (erule_tac x = e in allE) - apply (erule_tac x = T in allE) - apply (erule_tac x = "u $ a[u/i]" in allE) - apply (erule_tac x = 0 in allE) - apply (fastsimp intro!: list_app_typeI lift_types subst_lemma substs_lemma) - apply (erule_tac x = Ta in allE) - apply (erule impE) - apply simp - apply (erule_tac x = "lift u 0 $ Var 0" in allE) - apply (erule impE) - apply assumption - apply (erule_tac x = e in allE) - apply (erule_tac x = "Ts =>> T" in allE) - apply (erule_tac x = "a[u/i]" in allE) - apply (erule_tac x = 0 in allE) - apply (erule impE) - apply (rule typing.App) - apply (erule lift_type') - apply (rule typing.Var) - apply simp - apply (fast intro!: subst_lemma) - txt {* Case @{term "n ~= i"}: *} - apply (drule list_app_typeD) - apply (erule exE) - apply (erule conjE) - apply (drule lists_types) - apply (subgoal_tac "map (\x. x[u/i]) rs \ lists IT") - apply (simp add: subst_Var) - apply fast - apply (erule lists_IntI [THEN lists.induct]) - apply assumption - apply fastsimp - apply fastsimp - txt {* Case @{term Lambda}: *} - apply fastsimp - txt {* Case @{term Beta}: *} - apply (intro strip) - apply (simp (no_asm)) - apply (rule IT.Beta) - apply (simp (no_asm) del: subst_map add: subst_subst subst_map [symmetric]) - apply (drule subject_reduction) - apply (rule apps_preserves_beta) - apply (rule beta.beta) - apply fast - apply (drule list_app_typeD) - apply fast - done +lemma subst_type_IT: + "\t e T u i. t \ IT \ e |- t : T \ + u \ IT \ e |- u : U \ t[u/i] \ IT" + (is "PROP ?P U" is "\t e T u i. _ \ PROP ?Q t e T u i U") +proof (induct U) + fix T t + assume MI1: "\T1 T2. T = T1 => T2 \ PROP ?P T1" + assume MI2: "\T1 T2. T = T1 => T2 \ PROP ?P T2" + assume "t \ IT" + thus "\e T' u i. PROP ?Q t e T' u i T" + proof induct + fix e T' u i + assume uIT: "u : IT" + assume uT: "e |- u : T" + { + case (Var n rs) + assume nT: "e |- Var n $$ rs : T'" + let ?ty = "{t. \T'. e |- t : T'}" + let ?R = "\t. \e T' u i. + e |- t : T' \ u \ IT \ e |- u : T \ t[u/i] \ IT" + show "(Var n $$ rs)[u/i] \ IT" + proof (cases "n = i") + case True + show ?thesis + proof (cases rs) + case Nil + with uIT True show ?thesis by simp + next + case (Cons a as) + with nT have "e |- Var n $ a $$ as : T'" by simp + then obtain Ts + where headT: "e |- Var n $ a : Ts =>> T'" + and argsT: "types (e) as Ts" + by (rule list_app_typeE) + from headT obtain T'' + where varT: "e |- Var n : T'' => (Ts =>> T')" + and argT: "e |- a : T''" + by cases simp_all + from varT True have T: "T = T'' => (Ts =>> T')" + by cases (auto simp add: shift_def) + with uT have uT': "e |- u : T'' => (Ts =>> T')" by simp + from Var have SI: "?R a" by cases (simp_all add: Cons) + from T have "(Var 0 $$ map (\t. lift t 0) + (map (\t. t[u/i]) as))[(u $ a[u/i])/0] \ IT" + proof (rule MI2) + from T have "(lift u 0 $ Var 0)[a[u/i]/0] \ IT" + proof (rule MI1) + have "lift u 0 : IT" by (rule lift_IT) + thus "lift u 0 $ Var 0 \ IT" by (rule app_Var_IT) + show "e<0:T''> |- lift u 0 $ Var 0 : Ts =>> T'" + proof (rule typing.App) + show "e<0:T''> |- lift u 0 : T'' => (Ts =>> T')" + by (rule lift_type') (rule uT') + show "e<0:T''> |- Var 0 : T''" + by (rule typing.Var) (simp add: shift_def) + qed + from argT uIT uT show "a[u/i] : IT" + by (rule SI[rule_format]) + from argT uT show "e |- a[u/i] : T''" + by (rule subst_lemma) (simp add: shift_def) + qed + thus "u $ a[u/i] \ IT" by simp + from Var have "as : lists {t. ?R t}" + by cases (simp_all add: Cons) + moreover from argsT have "as : lists ?ty" + by (rule lists_types) + ultimately have "as : lists ({t. ?R t} \ ?ty)" + by (rule lists_IntI) + hence "map (\t. lift t 0) (map (\t. t[u/i]) as) \ lists IT" + (is "(?ls as) \ _") + proof induct + case Nil + show ?case by fastsimp + next + case (Cons b bs) + hence I: "?R b" by simp + from Cons obtain U where "e |- b : U" by fast + with uT uIT I have "b[u/i] : IT" by simp + hence "lift (b[u/i]) 0 : IT" by (rule lift_IT) + hence "lift (b[u/i]) 0 # ?ls bs \ lists IT" + by (rule lists.Cons) (rule Cons) + thus ?case by simp + qed + thus "Var 0 $$ ?ls as \ IT" by (rule IT.Var) + have "e<0:Ts =>> T'> |- Var 0 : Ts =>> T'" + by (rule typing.Var) (simp add: shift_def) + moreover from uT argsT have "types e (map (\t. t[u/i]) as) Ts" + by (rule substs_lemma) + hence "types (e<0:Ts =>> T'>) (?ls as) Ts" + by (rule lift_types) + ultimately show "e<0:Ts =>> T'> |- Var 0 $$ ?ls as : T'" + by (rule list_app_typeI) + from argT uT have "e |- a[u/i] : T''" + by (rule subst_lemma) (rule refl) + with uT' show "e |- u $ a[u/i] : Ts =>> T'" + by (rule typing.App) + qed + with Cons True show ?thesis + by (simp add: map_compose [symmetric] o_def) + qed + next + case False + from Var have "rs : lists {t. ?R t}" by simp + moreover from nT obtain Ts where "types (e) rs Ts" + by (rule list_app_typeE) + hence "rs : lists ?ty" by (rule lists_types) + ultimately have "rs : lists ({t. ?R t} \ ?ty)" + by (rule lists_IntI) + hence "map (\x. x[u/i]) rs \ lists IT" + proof induct + case Nil + show ?case by fastsimp + next + case (Cons a as) + hence I: "?R a" by simp + from Cons obtain U where "e |- a : U" by fast + with uT uIT I have "a[u/i] : IT" by simp + hence "a[u/i] # map (\t. t[u/i]) as \ lists IT" + by (rule lists.Cons) (rule Cons) + thus ?case by simp + qed + with False show ?thesis by (auto simp add: subst_Var) + qed + next + case (Lambda r) + assume "e |- Abs r : T'" + and "\e T' u i. PROP ?Q r e T' u i T" + with uIT uT show "Abs r[u/i] \ IT" + by (fastsimp simp add: shift_def) + next + case (Beta r a as) + assume T: "e |- Abs r $ a $$ as : T'" + assume SI1: "\e T' u i. PROP ?Q (r[a/0] $$ as) e T' u i T" + assume SI2: "\e T' u i. PROP ?Q a e T' u i T" + have "Abs (r[lift u 0/Suc i]) $ a[u/i] $$ map (\t. t[u/i]) as \ IT" + proof (rule IT.Beta) + have "Abs r $ a $$ as -> r[a/0] $$ as" + by (rule apps_preserves_beta) (rule beta.beta) + with T have "e |- r[a/0] $$ as : T'" + by (rule subject_reduction) + hence "(r[a/0] $$ as)[u/i] \ IT" + by (rule SI1) + thus "r[lift u 0/Suc i][a[u/i]/0] $$ map (\t. t[u/i]) as \ IT" + by (simp del: subst_map add: subst_subst subst_map [symmetric]) + from T obtain U where "e |- Abs r $ a : U" + by (rule list_app_typeE) fast + then obtain T'' where "e |- a : T''" by cases simp_all + thus "a[u/i] \ IT" by (rule SI2) + qed + thus "(Abs r $ a $$ as)[u/i] \ IT" by simp + } + qed +qed - -subsection {* Main theorem: well-typed terms are strongly normalizing *} +subsection {* Well-typed terms are strongly normalizing *} lemma type_implies_IT: "e |- t : T ==> t \ IT" - apply (erule typing.induct) - apply (rule Var_IT) - apply (erule IT.Lambda) - apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] \ IT") - apply simp - apply (rule subst_type_IT) - apply (rule lists.Nil - [THEN [2] lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection] - foldl_Cons [THEN eq_reflection]]) - apply (erule lift_IT) - apply (rule typing.App) - apply (rule typing.Var) - apply simp - apply (erule lift_type') - apply assumption - apply assumption - done +proof - + assume "e |- t : T" + thus ?thesis + proof induct + case Var + show ?case by (rule Var_IT) + next + case Abs + show ?case by (rule IT.Lambda) + next + case (App T U e s t) + have "(Var 0 $ lift t 0)[s/0] \ IT" + proof (rule subst_type_IT) + have "lift t 0 : IT" by (rule lift_IT) + hence "[lift t 0] : lists IT" by (rule lists.Cons) (rule lists.Nil) + hence "Var 0 $$ [lift t 0] : IT" by (rule IT.Var) + also have "(Var 0 $$ [lift t 0]) = (Var 0 $ lift t 0)" by simp + finally show "\ : IT" . + have "e<0:T => U> |- Var 0 : T => U" + by (rule typing.Var) (simp add: shift_def) + moreover have "e<0:T => U> |- lift t 0 : T" + by (rule lift_type') + ultimately show "e<0:T => U> |- Var 0 $ lift t 0 : U" + by (rule typing.App) + qed + thus ?case by simp + qed +qed theorem type_implies_termi: "e |- t : T ==> t \ termi beta" - apply (rule IT_implies_termi) - apply (erule type_implies_IT) - done +proof - + assume "e |- t : T" + hence "t \ IT" by (rule type_implies_IT) + thus ?thesis by (rule IT_implies_termi) +qed end