# HG changeset patch
# User wenzelm
# Date 1004091859 -7200
# Node ID a9672446b45fd0e3102f232357cc5994230c31c9
# Parent  06fac365248dc08fc5bd04b6c59184bcc40b3e3e
tuned notation;

diff -r 06fac365248d -r a9672446b45f src/HOL/Lambda/Lambda.thy
--- 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"
diff -r 06fac365248d -r a9672446b45f src/HOL/Lambda/ListApplication.thy
--- 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"
 
diff -r 06fac365248d -r a9672446b45f src/HOL/Lambda/ROOT.ML
--- 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";
diff -r 06fac365248d -r a9672446b45f src/HOL/Lambda/Type.thy
--- 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