--- a/src/HOL/Lambda/Lambda.thy Thu Oct 25 22:59:11 2001 +0200
+++ b/src/HOL/Lambda/Lambda.thy Fri Oct 26 12:24:19 2001 +0200
@@ -16,6 +16,9 @@
| App dB dB (infixl "$" 200)
| Abs dB
+syntax (symbols)
+ App :: "dB => dB => dB" (infixl "\<^sub>\<degree>" 200)
+
consts
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
lift :: "[dB, nat] => dB"
--- a/src/HOL/Lambda/ListApplication.thy Thu Oct 25 22:59:11 2001 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Fri Oct 26 12:24:19 2001 +0200
@@ -9,7 +9,10 @@
theory ListApplication = Lambda:
syntax
- "_list_application" :: "dB => dB list => dB" (infixl "$$" 150)
+ "_list_application" :: "dB => dB list => dB" (infixl "$$" 150)
+syntax (symbols)
+ "_list_application" :: "dB => dB => dB" (infixl "\<^sub>\<degree>\<^sub>\<degree>" 150)
+
translations
"t $$ ts" == "foldl (op $) t ts"
--- a/src/HOL/Lambda/ROOT.ML Thu Oct 25 22:59:11 2001 +0200
+++ b/src/HOL/Lambda/ROOT.ML Fri Oct 26 12:24:19 2001 +0200
@@ -4,6 +4,8 @@
Copyright 1998 TUM
*)
+Syntax.ambiguity_level := 100;
+
time_use_thy "Eta";
time_use_thy "Accessible_Part";
time_use_thy "Type";
--- a/src/HOL/Lambda/Type.thy Thu Oct 25 22:59:11 2001 +0200
+++ b/src/HOL/Lambda/Type.thy Fri Oct 26 12:24:19 2001 +0200
@@ -19,82 +19,90 @@
datatype type =
Atom nat
- | Fun type type (infixr "=>" 200)
+ | Fun type type (infixr "\<rightarrow>" 200)
consts
- typing :: "((nat => type) \<times> dB \<times> type) set"
+ typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
+ typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
syntax
- "_typing" :: "[nat => type, dB, type] => bool" ("_ |- _ : _" [50,50,50] 50)
- "_funs" :: "[type list, type] => type" (infixl "=>>" 150)
+ "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=\<guillemotright>" 200)
+ "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50)
+ "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
+ ("_ ||- _ : _" [50, 50, 50] 50)
+
+syntax (symbols)
+ "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+syntax (latex)
+ "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
+ ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
translations
- "env |- t : T" == "(env, t, T) \<in> typing"
- "Ts =>> T" == "foldr Fun Ts T"
+ "Ts =\<guillemotright> T" \<rightleftharpoons> "foldr Fun Ts T"
+ "env \<turnstile> t : T" \<rightleftharpoons> "(env, t, T) \<in> typing"
+ "env \<tturnstile> ts : Ts" \<rightleftharpoons> "typings env ts Ts"
inductive typing
intros
- Var [intro!]: "env x = T ==> env |- Var x : T"
- 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"
+ Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
+ Abs [intro!]: "(nat_case T env) \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<rightarrow> U)"
+ App [intro!]: "env \<turnstile> s : T \<rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<^sub>\<degree> 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 typing_elims [elim!]:
+ "e \<turnstile> Var i : T"
+ "e \<turnstile> t \<^sub>\<degree> u : T"
+ "e \<turnstile> Abs t : T"
-inductive_cases [elim!]:
- "e |- Var i : T"
- "e |- t $ u : T"
- "e |- Abs t : T"
+primrec
+ "(e \<tturnstile> [] : Ts) = (Ts = [])"
+ "(e \<tturnstile> (t # ts) : Ts) =
+ (case Ts of
+ [] \<Rightarrow> False
+ | T # Ts \<Rightarrow> e \<turnstile> t : T \<and> e \<tturnstile> ts : Ts)"
-consts
- "types" :: "[nat => type, dB list, type list] => bool"
-primrec
- "types e [] Ts = (Ts = [])"
- "types e (t # ts) Ts =
- (case Ts of
- [] => False
- | T # Ts => e |- t : T \<and> types e ts Ts)"
-
-inductive_cases [elim!]:
+inductive_cases lists_elim [elim!]:
"x # xs \<in> lists S"
declare IT.intros [intro!]
+constdefs
+ shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+ "e\<langle>i:a\<rangle> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
+
subsection {* Some examples *}
-lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T"
+lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<^sub>\<degree> (Var 2 \<^sub>\<degree> Var 1 \<^sub>\<degree> Var 0)))) : ?T"
by force
-lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
+lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<^sub>\<degree> Var 0 \<^sub>\<degree> (Var 1 \<^sub>\<degree> Var 0)))) : ?T"
by force
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)"
+ "\<forall>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<longrightarrow> (\<exists>Ts. e \<turnstile> t : Ts =\<guillemotright> T \<and> e \<tturnstile> ts : Ts)"
apply (induct_tac ts)
apply simp
apply (intro strip)
apply simp
- apply (erule_tac x = "t $ a" in allE)
+ apply (erule_tac x = "t \<^sub>\<degree> 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")
+ apply (ind_cases "e \<turnstile> t \<^sub>\<degree> u : T")
apply (rule_tac x = "Ta # Ts" in exI)
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"
+ "e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts =\<guillemotright> T \<Longrightarrow> e \<tturnstile> 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"
+ "\<forall>t T Ts. e \<turnstile> t : Ts =\<guillemotright> T \<longrightarrow> e \<tturnstile> ts : Ts \<longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
apply (induct_tac ts)
apply (intro strip)
apply simp
@@ -102,7 +110,7 @@
apply (case_tac Ts)
apply simp
apply simp
- apply (erule_tac x = "t $ a" in allE)
+ apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
apply (erule_tac x = T in allE)
apply (erule_tac x = lista in allE)
apply (erule impE)
@@ -112,8 +120,8 @@
apply blast
done
-lemma lists_types [rule_format]:
- "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
+lemma lists_typings [rule_format]:
+ "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
apply (induct_tac ts)
apply (intro strip)
apply (case_tac Ts)
@@ -133,15 +141,15 @@
subsection {* Lifting preserves termination and well-typedness *}
lemma lift_map [simp]:
- "\<And>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
+ "\<And>t. lift (t \<^sub>\<degree>\<^sub>\<degree> ts) i = lift t i \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t i) ts"
by (induct ts) simp_all
lemma subst_map [simp]:
- "\<And>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
+ "\<And>t. subst (t \<^sub>\<degree>\<^sub>\<degree> ts) u i = subst t u i \<^sub>\<degree>\<^sub>\<degree> 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"
+ "t \<in> IT \<Longrightarrow> \<forall>i. lift t i \<in> IT"
apply (erule IT.induct)
apply (rule allI)
apply (simp (no_asm))
@@ -177,16 +185,16 @@
done
lemma lift_type':
- "e |- t : T ==> e<i:U> |- lift t i : T"
+ "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
proof -
- assume "e |- t : T"
- thus "\<And>i U. e<i:U> |- lift t i : T"
+ assume "e \<turnstile> t : T"
+ thus "\<And>i U. e\<langle>i:U\<rangle> \<turnstile> 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 = e<0:U>")
+ "e \<turnstile> t : T \<Longrightarrow> nat_case U e \<turnstile> lift t 0 : T"
+ apply (subgoal_tac "nat_case U e = e\<langle>0:U\<rangle>")
apply (erule ssubst)
apply (erule lift_type')
apply (rule ext)
@@ -194,8 +202,8 @@
apply (simp_all add: shift_def)
done
-lemma lift_types [rule_format]:
- "\<forall>Ts. types e ts Ts --> types (e<i:U>) (map (\<lambda>t. lift t i) ts) Ts"
+lemma lift_typings [rule_format]:
+ "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> (e\<langle>i:U\<rangle>) \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
apply (induct_tac ts)
apply simp
apply (intro strip)
@@ -209,8 +217,7 @@
subsection {* Substitution lemmas *}
lemma subst_lemma [rule_format]:
- "e |- t : T ==> \<forall>e' i U u. e' |- u : U -->
- e = e'<i:U> --> e' |- t[u/i] : T"
+ "e \<turnstile> t : T \<Longrightarrow> \<forall>e' i U u. e' \<turnstile> u : U \<longrightarrow> e = e'\<langle>i:U\<rangle> \<longrightarrow> e' \<turnstile> t[u/i] : T"
apply (unfold shift_def)
apply (erule typing.induct)
apply (intro strip)
@@ -230,8 +237,8 @@
done
lemma substs_lemma [rule_format]:
- "e |- u : T ==> \<forall>Ts. types (e<i:T>) ts Ts -->
- types e (map (\<lambda>t. t[u/i]) ts) Ts"
+ "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. (e\<langle>i:T\<rangle>) \<tturnstile> ts : Ts \<longrightarrow>
+ e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
apply (induct_tac ts)
apply (intro strip)
apply (case_tac Ts)
@@ -251,14 +258,14 @@
subsection {* Subject reduction *}
lemma subject_reduction [rule_format]:
- "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
+ "e \<turnstile> t : T \<Longrightarrow> \<forall>t'. t -> t' \<longrightarrow> e \<turnstile> t' : T"
apply (erule typing.induct)
apply blast
apply blast
apply (intro strip)
- apply (ind_cases "s $ t -> t'")
+ apply (ind_cases "s \<^sub>\<degree> t -> t'")
apply hypsubst
- apply (ind_cases "env |- Abs t : T => U")
+ apply (ind_cases "env \<turnstile> Abs t : T \<rightarrow> U")
apply (rule subst_lemma)
apply assumption
apply assumption
@@ -270,10 +277,10 @@
subsection {* Additional lemmas *}
-lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
+lemma app_last: "(t \<^sub>\<degree>\<^sub>\<degree> ts) \<^sub>\<degree> u = t \<^sub>\<degree>\<^sub>\<degree> (ts @ [u])"
by simp
-lemma subst_Var_IT [rule_format]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
+lemma subst_Var_IT [rule_format]: "r \<in> IT \<Longrightarrow> \<forall>i j. r[Var i/j] \<in> IT"
apply (erule IT.induct)
txt {* Case @{term Var}: *}
apply (intro strip)
@@ -303,13 +310,13 @@
done
lemma Var_IT: "Var n \<in> IT"
- apply (subgoal_tac "Var n $$ [] \<in> IT")
+ apply (subgoal_tac "Var n \<^sub>\<degree>\<^sub>\<degree> [] \<in> IT")
apply simp
apply (rule IT.Var)
apply (rule lists.Nil)
done
-lemma app_Var_IT: "t \<in> IT ==> t $ Var i \<in> IT"
+lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<^sub>\<degree> Var i \<in> IT"
apply (erule IT.induct)
apply (subst app_last)
apply (rule IT.Var)
@@ -328,8 +335,8 @@
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"
+ "(\<And>T. (\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
+ (\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> P T"
proof -
case rule_context
show ?thesis
@@ -346,164 +353,164 @@
subsection {* Well-typed substitution preserves termination *}
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"
+ "\<And>t e T u i. t \<in> IT \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
+ u \<in> IT \<Longrightarrow> e \<turnstile> 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 MI1: "\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> PROP ?P T1"
+ assume MI2: "\<And>T1 T2. T = T1 \<rightarrow> 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"
+ assume uIT: "u \<in> IT"
+ assume uT: "e \<turnstile> 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'}"
+ assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree>\<^sub>\<degree> rs : T'"
+ let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> 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"
+ e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
+ show "(Var n \<^sub>\<degree>\<^sub>\<degree> 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
+ 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\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'" by simp
+ then obtain Ts
+ where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a : Ts =\<guillemotright> T'"
+ and argsT: "(e\<langle>i:T\<rangle>) \<tturnstile> as : Ts"
+ by (rule list_app_typeE)
+ from headT obtain T''
+ where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<rightarrow> Ts =\<guillemotright> T'"
+ and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''"
+ by cases simp_all
+ from varT True have T: "T = T'' \<rightarrow> Ts =\<guillemotright> T'"
+ by cases (auto simp add: shift_def)
+ with uT have uT': "e \<turnstile> u : T'' \<rightarrow> Ts =\<guillemotright> T'" by simp
+ from Var have SI: "?R a" by cases (simp_all add: Cons)
+ from T have "(Var 0 \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t 0)
+ (map (\<lambda>t. t[u/i]) as))[(u \<^sub>\<degree> a[u/i])/0] \<in> IT"
+ proof (rule MI2)
+ from T have "(lift u 0 \<^sub>\<degree> Var 0)[a[u/i]/0] \<in> IT"
+ proof (rule MI1)
+ have "lift u 0 \<in> IT" by (rule lift_IT)
+ thus "lift u 0 \<^sub>\<degree> Var 0 \<in> IT" by (rule app_Var_IT)
+ show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<^sub>\<degree> Var 0 : Ts =\<guillemotright> T'"
+ proof (rule typing.App)
+ show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<rightarrow> Ts =\<guillemotright> T'"
+ by (rule lift_type') (rule uT')
+ show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''"
+ by (rule typing.Var) (simp add: shift_def)
+ qed
+ from argT uIT uT show "a[u/i] \<in> IT"
+ by (rule SI[rule_format])
+ from argT uT show "e \<turnstile> a[u/i] : T''"
+ by (rule subst_lemma) (simp add: shift_def)
+ qed
+ thus "u \<^sub>\<degree> a[u/i] \<in> IT" by simp
+ from Var have "as \<in> lists {t. ?R t}"
+ by cases (simp_all add: Cons)
+ moreover from argsT have "as \<in> lists ?ty"
+ by (rule lists_typings)
+ ultimately have "as \<in> 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\<langle>i:T\<rangle> \<turnstile> b : U" by fast
+ with uT uIT I have "b[u/i] \<in> IT" by simp
+ hence "lift (b[u/i]) 0 \<in> 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 \<^sub>\<degree>\<^sub>\<degree> ?ls as \<in> IT" by (rule IT.Var)
+ have "e\<langle>0:Ts =\<guillemotright> T'\<rangle> \<turnstile> Var 0 : Ts =\<guillemotright> T'"
+ by (rule typing.Var) (simp add: shift_def)
+ moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
+ by (rule substs_lemma)
+ hence "(e\<langle>0:Ts =\<guillemotright> T'\<rangle>) \<tturnstile> ?ls as : Ts"
+ by (rule lift_typings)
+ ultimately show "e\<langle>0:Ts =\<guillemotright> T'\<rangle> \<turnstile> Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as : T'"
+ by (rule list_app_typeI)
+ from argT uT have "e \<turnstile> a[u/i] : T''"
+ by (rule subst_lemma) (rule refl)
+ with uT' show "e \<turnstile> u \<^sub>\<degree> a[u/i] : Ts =\<guillemotright> 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)
+ case False
+ from Var have "rs \<in> lists {t. ?R t}" by simp
+ moreover from nT obtain Ts where "(e\<langle>i:T\<rangle>) \<tturnstile> rs : Ts"
+ by (rule list_app_typeE)
+ hence "rs \<in> lists ?ty" by (rule lists_typings)
+ ultimately have "rs \<in> 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\<langle>i:T\<rangle> \<turnstile> a : U" by fast
+ with uT uIT I have "a[u/i] \<in> 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"
+ assume "e\<langle>i:T\<rangle> \<turnstile> 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)
+ 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 T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'"
+ assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<^sub>\<degree>\<^sub>\<degree> 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"
+ have "Abs (r[lift u 0/Suc i]) \<^sub>\<degree> a[u/i] \<^sub>\<degree>\<^sub>\<degree> 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)
+ have "Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as -> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as"
+ by (rule apps_preserves_beta) (rule beta.beta)
+ with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as : T'"
+ by (rule subject_reduction)
+ hence "(r[a/0] \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT"
+ by (rule SI1)
+ thus "r[lift u 0/Suc i][a[u/i]/0] \<^sub>\<degree>\<^sub>\<degree> 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\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a : U"
+ by (rule list_app_typeE) fast
+ then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> 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
+ thus "(Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT" by simp
}
qed
qed
subsection {* Well-typed terms are strongly normalizing *}
-lemma type_implies_IT: "e |- t : T ==> t \<in> IT"
+lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"
proof -
- assume "e |- t : T"
+ assume "e \<turnstile> t : T"
thus ?thesis
proof induct
case Var
@@ -513,27 +520,27 @@
show ?case by (rule IT.Lambda)
next
case (App T U e s t)
- have "(Var 0 $ lift t 0)[s/0] \<in> IT"
+ have "(Var 0 \<^sub>\<degree> 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)
+ have "lift t 0 \<in> IT" by (rule lift_IT)
+ hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
+ hence "Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
+ also have "(Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0]) = (Var 0 \<^sub>\<degree> lift t 0)" by simp
+ finally show "\<dots> \<in> IT" .
+ have "e\<langle>0:T \<rightarrow> U\<rangle> \<turnstile> Var 0 : T \<rightarrow> U"
+ by (rule typing.Var) (simp add: shift_def)
+ moreover have "e\<langle>0:T \<rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
+ by (rule lift_type')
+ ultimately show "e\<langle>0:T \<rightarrow> U\<rangle> \<turnstile> Var 0 \<^sub>\<degree> 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"
+theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
proof -
- assume "e |- t : T"
+ assume "e \<turnstile> t : T"
hence "t \<in> IT" by (rule type_implies_IT)
thus ?thesis by (rule IT_implies_termi)
qed