Replaced main proof by proper Isar script.
--- 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) \<in> 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 \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [50,0,0] 51)
+ "e<i:a> == \<lambda>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]:
"\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
@@ -86,6 +89,10 @@
apply simp
done
+lemma list_app_typeE:
+ "e |- t $$ ts : T \<Longrightarrow> (\<And>Ts. e |- t : Ts =>> T \<Longrightarrow> types e ts Ts \<Longrightarrow> C) \<Longrightarrow> C"
+ by (insert list_app_typeD) fast
+
lemma list_app_typeI [rule_format]:
"\<forall>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]:
- "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
- apply (induct_tac ts)
- apply simp_all
- done
+lemma lift_map [simp]:
+ "\<And>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
+ by (induct ts) simp_all
-lemma subst_map [rule_format, simp]:
- "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
- apply (induct_tac ts)
- apply simp_all
- done
+lemma subst_map [simp]:
+ "\<And>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
+ by (induct ts) simp_all
lemma lift_IT [rule_format, intro!]:
"t \<in> IT ==> \<forall>i. lift t i \<in> IT"
@@ -157,12 +160,9 @@
apply auto
done
-lemma lifts_IT [rule_format]:
- "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
- apply (induct_tac ts)
- apply auto
- done
-
+lemma lifts_IT:
+ "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> 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 ==> \<forall>i U.
- (\<lambda>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<i:U> |- lift t i : T"
+proof -
+ assume "e |- t : T"
+ thus "\<And>i U. e<i:U> |- 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 =
- (\<lambda>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]:
- "\<forall>Ts. types e ts Ts -->
- types (\<lambda>j. if j < i then e j
- else if j = i then U
- else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts"
+ "\<forall>Ts. types e ts Ts --> types (e<i:U>) (map (\<lambda>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 ==> \<forall>e' i U u.
- e = (\<lambda>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 ==> \<forall>e' i U u. e' |- u : U -->
+ e = e'<i:U> --> 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 ==>
- \<forall>Ts. types (\<lambda>j. if j < i then e j
- else if j = i then T else e (j - 1)) ts Ts -->
- types e (map (\<lambda>t. t[u/i]) ts) Ts"
+ "e |- u : T ==> \<forall>Ts. types (e<i:T>) ts Ts -->
+ types e (map (\<lambda>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 \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
apply (erule IT.induct)
@@ -340,130 +327,215 @@
apply assumption
done
+lemma type_induct [induct type]:
+ "(\<And>T. (\<And>T1 T2. T = T1 => T2 \<Longrightarrow> P T1) \<Longrightarrow>
+ (\<And>T1 T2. T = T1 => T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> 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]:
- "\<forall>t. t \<in> IT --> (\<forall>e T u i.
- (\<lambda>j. if j < i then e j
- else if j = i then U
- else e (j - 1)) |- t : T -->
- u \<in> IT --> e |- u : U --> t[u/i] \<in> 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 \<in> IT")
- prefer 2
- apply (rule app_Var_IT)
- apply (erule lift_IT)
- apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] \<in> IT")
- apply (simp (no_asm_use))
- apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0)
- (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] \<in> 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 (\<lambda>t. lift t 0) (map (\<lambda>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 \<in> 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 (\<lambda>x. x[u/i]) rs \<in> 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:
+ "\<And>t e T u i. t \<in> IT \<Longrightarrow> e<i:U> |- t : T \<Longrightarrow>
+ u \<in> IT \<Longrightarrow> e |- u : U \<Longrightarrow> t[u/i] \<in> IT"
+ (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
+proof (induct U)
+ fix T t
+ assume MI1: "\<And>T1 T2. T = T1 => T2 \<Longrightarrow> PROP ?P T1"
+ assume MI2: "\<And>T1 T2. T = T1 => T2 \<Longrightarrow> PROP ?P T2"
+ assume "t \<in> IT"
+ thus "\<And>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<i:T> |- Var n $$ rs : T'"
+ let ?ty = "{t. \<exists>T'. e<i:T> |- t : T'}"
+ let ?R = "\<lambda>t. \<forall>e T' u i.
+ e<i:T> |- t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e |- u : T \<longrightarrow> t[u/i] \<in> IT"
+ show "(Var n $$ rs)[u/i] \<in> 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<i:T> |- Var n $ a $$ as : T'" by simp
+ then obtain Ts
+ where headT: "e<i:T> |- Var n $ a : Ts =>> T'"
+ and argsT: "types (e<i:T>) as Ts"
+ by (rule list_app_typeE)
+ from headT obtain T''
+ where varT: "e<i:T> |- Var n : T'' => (Ts =>> T')"
+ and argT: "e<i:T> |- 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 (\<lambda>t. lift t 0)
+ (map (\<lambda>t. t[u/i]) as))[(u $ a[u/i])/0] \<in> IT"
+ proof (rule MI2)
+ from T have "(lift u 0 $ Var 0)[a[u/i]/0] \<in> IT"
+ proof (rule MI1)
+ have "lift u 0 : IT" by (rule lift_IT)
+ thus "lift u 0 $ Var 0 \<in> 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] \<in> 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} \<inter> ?ty)"
+ by (rule lists_IntI)
+ hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
+ (is "(?ls as) \<in> _")
+ 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<i:T> |- 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 \<in> lists IT"
+ by (rule lists.Cons) (rule Cons)
+ thus ?case by simp
+ qed
+ thus "Var 0 $$ ?ls as \<in> 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 (\<lambda>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<i:T>) rs Ts"
+ by (rule list_app_typeE)
+ hence "rs : lists ?ty" by (rule lists_types)
+ ultimately have "rs : lists ({t. ?R t} \<inter> ?ty)"
+ by (rule lists_IntI)
+ hence "map (\<lambda>x. x[u/i]) rs \<in> 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<i:T> |- a : U" by fast
+ with uT uIT I have "a[u/i] : IT" by simp
+ hence "a[u/i] # map (\<lambda>t. t[u/i]) as \<in> 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<i:T> |- Abs r : T'"
+ and "\<And>e T' u i. PROP ?Q r e T' u i T"
+ with uIT uT show "Abs r[u/i] \<in> IT"
+ by (fastsimp simp add: shift_def)
+ next
+ case (Beta r a as)
+ assume T: "e<i:T> |- Abs r $ a $$ as : T'"
+ assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] $$ as) e T' u i T"
+ assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
+ have "Abs (r[lift u 0/Suc i]) $ a[u/i] $$ map (\<lambda>t. t[u/i]) as \<in> 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<i:T> |- r[a/0] $$ as : T'"
+ by (rule subject_reduction)
+ hence "(r[a/0] $$ as)[u/i] \<in> IT"
+ by (rule SI1)
+ thus "r[lift u 0/Suc i][a[u/i]/0] $$ map (\<lambda>t. t[u/i]) as \<in> IT"
+ by (simp del: subst_map add: subst_subst subst_map [symmetric])
+ from T obtain U where "e<i:T> |- Abs r $ a : U"
+ by (rule list_app_typeE) fast
+ then obtain T'' where "e<i:T> |- a : T''" by cases simp_all
+ thus "a[u/i] \<in> IT" by (rule SI2)
+ qed
+ thus "(Abs r $ a $$ as)[u/i] \<in> 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 \<in> IT"
- apply (erule typing.induct)
- apply (rule Var_IT)
- apply (erule IT.Lambda)
- apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] \<in> 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] \<in> 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 "\<dots> : 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 \<in> termi beta"
- apply (rule IT_implies_termi)
- apply (erule type_implies_IT)
- done
+proof -
+ assume "e |- t : T"
+ hence "t \<in> IT" by (rule type_implies_IT)
+ thus ?thesis by (rule IT_implies_termi)
+qed
end