tuned notation;
authorwenzelm
Fri Oct 26 12:24:19 2001 +0200 (2001-10-26)
changeset 11943a9672446b45f
parent 11942 06fac365248d
child 11944 0594e63e6057
tuned notation;
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ROOT.ML
src/HOL/Lambda/Type.thy
     1.1 --- a/src/HOL/Lambda/Lambda.thy	Thu Oct 25 22:59:11 2001 +0200
     1.2 +++ b/src/HOL/Lambda/Lambda.thy	Fri Oct 26 12:24:19 2001 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4    | App dB dB (infixl "$" 200)
     1.5    | Abs dB
     1.6  
     1.7 +syntax (symbols)
     1.8 +  App :: "dB => dB => dB"    (infixl "\<^sub>\<degree>" 200)
     1.9 +
    1.10  consts
    1.11    subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
    1.12    lift :: "[dB, nat] => dB"
     2.1 --- a/src/HOL/Lambda/ListApplication.thy	Thu Oct 25 22:59:11 2001 +0200
     2.2 +++ b/src/HOL/Lambda/ListApplication.thy	Fri Oct 26 12:24:19 2001 +0200
     2.3 @@ -9,7 +9,10 @@
     2.4  theory ListApplication = Lambda:
     2.5  
     2.6  syntax
     2.7 -  "_list_application" :: "dB => dB list => dB"   (infixl "$$" 150)
     2.8 +  "_list_application" :: "dB => dB list => dB"    (infixl "$$" 150)
     2.9 +syntax (symbols)
    2.10 +  "_list_application" :: "dB => dB => dB"    (infixl "\<^sub>\<degree>\<^sub>\<degree>" 150)
    2.11 +
    2.12  translations
    2.13    "t $$ ts" == "foldl (op $) t ts"
    2.14  
     3.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Oct 25 22:59:11 2001 +0200
     3.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Oct 26 12:24:19 2001 +0200
     3.3 @@ -4,6 +4,8 @@
     3.4      Copyright   1998 TUM
     3.5  *)
     3.6  
     3.7 +Syntax.ambiguity_level := 100;
     3.8 +
     3.9  time_use_thy "Eta";
    3.10  time_use_thy "Accessible_Part";
    3.11  time_use_thy "Type";
     4.1 --- a/src/HOL/Lambda/Type.thy	Thu Oct 25 22:59:11 2001 +0200
     4.2 +++ b/src/HOL/Lambda/Type.thy	Fri Oct 26 12:24:19 2001 +0200
     4.3 @@ -19,82 +19,90 @@
     4.4  
     4.5  datatype type =
     4.6      Atom nat
     4.7 -  | Fun type type  (infixr "=>" 200)
     4.8 +  | Fun type type    (infixr "\<rightarrow>" 200)
     4.9  
    4.10  consts
    4.11 -  typing :: "((nat => type) \<times> dB \<times> type) set"
    4.12 +  typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
    4.13 +  typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    4.14  
    4.15  syntax
    4.16 -  "_typing" :: "[nat => type, dB, type] => bool"  ("_ |- _ : _" [50,50,50] 50)
    4.17 -  "_funs" :: "[type list, type] => type"  (infixl "=>>" 150)
    4.18 +  "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=\<guillemotright>" 200)
    4.19 +  "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
    4.20 +  "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    4.21 +    ("_ ||- _ : _" [50, 50, 50] 50)
    4.22 +
    4.23 +syntax (symbols)
    4.24 +  "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    4.25 +syntax (latex)
    4.26 +  "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    4.27 +    ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    4.28  
    4.29  translations
    4.30 -  "env |- t : T" == "(env, t, T) \<in> typing"
    4.31 -  "Ts =>> T" == "foldr Fun Ts T"
    4.32 +  "Ts =\<guillemotright> T" \<rightleftharpoons> "foldr Fun Ts T"
    4.33 +  "env \<turnstile> t : T" \<rightleftharpoons> "(env, t, T) \<in> typing"
    4.34 +  "env \<tturnstile> ts : Ts" \<rightleftharpoons> "typings env ts Ts"
    4.35  
    4.36  inductive typing
    4.37    intros
    4.38 -    Var [intro!]: "env x = T ==> env |- Var x : T"
    4.39 -    Abs [intro!]: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
    4.40 -    App [intro!]: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
    4.41 +    Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
    4.42 +    Abs [intro!]: "(nat_case T env) \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<rightarrow> U)"
    4.43 +    App [intro!]: "env \<turnstile> s : T \<rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<^sub>\<degree> t) : U"
    4.44  
    4.45 -constdefs
    4.46 -  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [50,0,0] 51)
    4.47 -  "e<i:a> == \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
    4.48 +inductive_cases typing_elims [elim!]:
    4.49 +  "e \<turnstile> Var i : T"
    4.50 +  "e \<turnstile> t \<^sub>\<degree> u : T"
    4.51 +  "e \<turnstile> Abs t : T"
    4.52  
    4.53 -inductive_cases [elim!]:
    4.54 -  "e |- Var i : T"
    4.55 -  "e |- t $ u : T"
    4.56 -  "e |- Abs t : T"
    4.57 +primrec
    4.58 +  "(e \<tturnstile> [] : Ts) = (Ts = [])"
    4.59 +  "(e \<tturnstile> (t # ts) : Ts) =
    4.60 +    (case Ts of
    4.61 +      [] \<Rightarrow> False
    4.62 +    | T # Ts \<Rightarrow> e \<turnstile> t : T \<and> e \<tturnstile> ts : Ts)"
    4.63  
    4.64 -consts
    4.65 -  "types" :: "[nat => type, dB list, type list] => bool"
    4.66 -primrec
    4.67 -  "types e [] Ts = (Ts = [])"
    4.68 -  "types e (t # ts) Ts =
    4.69 -    (case Ts of
    4.70 -      [] => False
    4.71 -    | T # Ts => e |- t : T \<and> types e ts Ts)"
    4.72 -
    4.73 -inductive_cases [elim!]:
    4.74 +inductive_cases lists_elim [elim!]:
    4.75    "x # xs \<in> lists S"
    4.76  
    4.77  declare IT.intros [intro!]
    4.78  
    4.79 +constdefs
    4.80 +  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    4.81 +  "e\<langle>i:a\<rangle> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
    4.82 +
    4.83  
    4.84  subsection {* Some examples *}
    4.85  
    4.86 -lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T"
    4.87 +lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<^sub>\<degree> (Var 2 \<^sub>\<degree> Var 1 \<^sub>\<degree> Var 0)))) : ?T"
    4.88    by force
    4.89  
    4.90 -lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
    4.91 +lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<^sub>\<degree> Var 0 \<^sub>\<degree> (Var 1 \<^sub>\<degree> Var 0)))) : ?T"
    4.92    by force
    4.93  
    4.94  
    4.95  subsection {* @{text n}-ary function types *}
    4.96  
    4.97  lemma list_app_typeD [rule_format]:
    4.98 -    "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
    4.99 +    "\<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)"
   4.100    apply (induct_tac ts)
   4.101     apply simp
   4.102    apply (intro strip)
   4.103    apply simp
   4.104 -  apply (erule_tac x = "t $ a" in allE)
   4.105 +  apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
   4.106    apply (erule_tac x = T in allE)
   4.107    apply (erule impE)
   4.108     apply assumption
   4.109    apply (elim exE conjE)
   4.110 -  apply (ind_cases "e |- t $ u : T")
   4.111 +  apply (ind_cases "e \<turnstile> t \<^sub>\<degree> u : T")
   4.112    apply (rule_tac x = "Ta # Ts" in exI)
   4.113    apply simp
   4.114    done
   4.115  
   4.116  lemma list_app_typeE:
   4.117 -  "e |- t $$ ts : T \<Longrightarrow> (\<And>Ts. e |- t : Ts =>> T \<Longrightarrow> types e ts Ts \<Longrightarrow> C) \<Longrightarrow> C"
   4.118 +  "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"
   4.119    by (insert list_app_typeD) fast
   4.120  
   4.121  lemma list_app_typeI [rule_format]:
   4.122 -    "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
   4.123 +    "\<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"
   4.124    apply (induct_tac ts)
   4.125     apply (intro strip)
   4.126     apply simp
   4.127 @@ -102,7 +110,7 @@
   4.128    apply (case_tac Ts)
   4.129     apply simp
   4.130    apply simp
   4.131 -  apply (erule_tac x = "t $ a" in allE)
   4.132 +  apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
   4.133    apply (erule_tac x = T in allE)
   4.134    apply (erule_tac x = lista in allE)
   4.135    apply (erule impE)
   4.136 @@ -112,8 +120,8 @@
   4.137    apply blast
   4.138    done
   4.139  
   4.140 -lemma lists_types [rule_format]:
   4.141 -    "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
   4.142 +lemma lists_typings [rule_format]:
   4.143 +    "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
   4.144    apply (induct_tac ts)
   4.145     apply (intro strip)
   4.146     apply (case_tac Ts)
   4.147 @@ -133,15 +141,15 @@
   4.148  subsection {* Lifting preserves termination and well-typedness *}
   4.149  
   4.150  lemma lift_map [simp]:
   4.151 -    "\<And>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
   4.152 +    "\<And>t. lift (t \<^sub>\<degree>\<^sub>\<degree> ts) i = lift t i \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t i) ts"
   4.153    by (induct ts) simp_all
   4.154  
   4.155  lemma subst_map [simp]:
   4.156 -    "\<And>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
   4.157 +    "\<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"
   4.158    by (induct ts) simp_all
   4.159  
   4.160  lemma lift_IT [rule_format, intro!]:
   4.161 -    "t \<in> IT ==> \<forall>i. lift t i \<in> IT"
   4.162 +    "t \<in> IT \<Longrightarrow> \<forall>i. lift t i \<in> IT"
   4.163    apply (erule IT.induct)
   4.164      apply (rule allI)
   4.165      apply (simp (no_asm))
   4.166 @@ -177,16 +185,16 @@
   4.167    done
   4.168  
   4.169  lemma lift_type':
   4.170 -  "e |- t : T ==> e<i:U> |- lift t i : T"
   4.171 +  "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
   4.172  proof -
   4.173 -  assume "e |- t : T"
   4.174 -  thus "\<And>i U. e<i:U> |- lift t i : T"
   4.175 +  assume "e \<turnstile> t : T"
   4.176 +  thus "\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
   4.177      by induct (auto simp add: shift_def)
   4.178  qed
   4.179  
   4.180  lemma lift_type [intro!]:
   4.181 -    "e |- t : T ==> nat_case U e |- lift t 0 : T"
   4.182 -  apply (subgoal_tac "nat_case U e = e<0:U>")
   4.183 +    "e \<turnstile> t : T \<Longrightarrow> nat_case U e \<turnstile> lift t 0 : T"
   4.184 +  apply (subgoal_tac "nat_case U e = e\<langle>0:U\<rangle>")
   4.185     apply (erule ssubst)
   4.186     apply (erule lift_type')
   4.187    apply (rule ext)
   4.188 @@ -194,8 +202,8 @@
   4.189     apply (simp_all add: shift_def)
   4.190    done
   4.191  
   4.192 -lemma lift_types [rule_format]:
   4.193 -  "\<forall>Ts. types e ts Ts --> types (e<i:U>) (map (\<lambda>t. lift t i) ts) Ts"
   4.194 +lemma lift_typings [rule_format]:
   4.195 +  "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> (e\<langle>i:U\<rangle>) \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
   4.196    apply (induct_tac ts)
   4.197     apply simp
   4.198    apply (intro strip)
   4.199 @@ -209,8 +217,7 @@
   4.200  subsection {* Substitution lemmas *}
   4.201  
   4.202  lemma subst_lemma [rule_format]:
   4.203 -  "e |- t : T ==> \<forall>e' i U u. e' |- u : U -->
   4.204 -    e = e'<i:U> --> e' |- t[u/i] : T"
   4.205 +  "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"
   4.206    apply (unfold shift_def)
   4.207    apply (erule typing.induct)
   4.208      apply (intro strip)
   4.209 @@ -230,8 +237,8 @@
   4.210    done
   4.211  
   4.212  lemma substs_lemma [rule_format]:
   4.213 -  "e |- u : T ==> \<forall>Ts. types (e<i:T>) ts Ts -->
   4.214 -     types e (map (\<lambda>t. t[u/i]) ts) Ts"
   4.215 +  "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. (e\<langle>i:T\<rangle>) \<tturnstile> ts : Ts \<longrightarrow>
   4.216 +     e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
   4.217    apply (induct_tac ts)
   4.218     apply (intro strip)
   4.219     apply (case_tac Ts)
   4.220 @@ -251,14 +258,14 @@
   4.221  subsection {* Subject reduction *}
   4.222  
   4.223  lemma subject_reduction [rule_format]:
   4.224 -    "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
   4.225 +    "e \<turnstile> t : T \<Longrightarrow> \<forall>t'. t -> t' \<longrightarrow> e \<turnstile> t' : T"
   4.226    apply (erule typing.induct)
   4.227      apply blast
   4.228     apply blast
   4.229    apply (intro strip)
   4.230 -  apply (ind_cases "s $ t -> t'")
   4.231 +  apply (ind_cases "s \<^sub>\<degree> t -> t'")
   4.232      apply hypsubst
   4.233 -    apply (ind_cases "env |- Abs t : T => U")
   4.234 +    apply (ind_cases "env \<turnstile> Abs t : T \<rightarrow> U")
   4.235      apply (rule subst_lemma)
   4.236        apply assumption
   4.237       apply assumption
   4.238 @@ -270,10 +277,10 @@
   4.239  
   4.240  subsection {* Additional lemmas *}
   4.241  
   4.242 -lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
   4.243 +lemma app_last: "(t \<^sub>\<degree>\<^sub>\<degree> ts) \<^sub>\<degree> u = t \<^sub>\<degree>\<^sub>\<degree> (ts @ [u])"
   4.244    by simp
   4.245  
   4.246 -lemma subst_Var_IT [rule_format]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
   4.247 +lemma subst_Var_IT [rule_format]: "r \<in> IT \<Longrightarrow> \<forall>i j. r[Var i/j] \<in> IT"
   4.248    apply (erule IT.induct)
   4.249      txt {* Case @{term Var}: *}
   4.250      apply (intro strip)
   4.251 @@ -303,13 +310,13 @@
   4.252    done
   4.253  
   4.254  lemma Var_IT: "Var n \<in> IT"
   4.255 -  apply (subgoal_tac "Var n $$ [] \<in> IT")
   4.256 +  apply (subgoal_tac "Var n \<^sub>\<degree>\<^sub>\<degree> [] \<in> IT")
   4.257     apply simp
   4.258    apply (rule IT.Var)
   4.259    apply (rule lists.Nil)
   4.260    done
   4.261  
   4.262 -lemma app_Var_IT: "t \<in> IT ==> t $ Var i \<in> IT"
   4.263 +lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<^sub>\<degree> Var i \<in> IT"
   4.264    apply (erule IT.induct)
   4.265      apply (subst app_last)
   4.266      apply (rule IT.Var)
   4.267 @@ -328,8 +335,8 @@
   4.268    done
   4.269  
   4.270  lemma type_induct [induct type]:
   4.271 -  "(\<And>T. (\<And>T1 T2. T = T1 => T2 \<Longrightarrow> P T1) \<Longrightarrow>
   4.272 -   (\<And>T1 T2. T = T1 => T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> P T"
   4.273 +  "(\<And>T. (\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
   4.274 +   (\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> P T"
   4.275  proof -
   4.276    case rule_context
   4.277    show ?thesis
   4.278 @@ -346,164 +353,164 @@
   4.279  subsection {* Well-typed substitution preserves termination *}
   4.280  
   4.281  lemma subst_type_IT:
   4.282 -  "\<And>t e T u i. t \<in> IT \<Longrightarrow> e<i:U> |- t : T \<Longrightarrow>
   4.283 -    u \<in> IT \<Longrightarrow> e |- u : U \<Longrightarrow> t[u/i] \<in> IT"
   4.284 +  "\<And>t e T u i. t \<in> IT \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
   4.285 +    u \<in> IT \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> t[u/i] \<in> IT"
   4.286    (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
   4.287  proof (induct U)
   4.288    fix T t
   4.289 -  assume MI1: "\<And>T1 T2. T = T1 => T2 \<Longrightarrow> PROP ?P T1"
   4.290 -  assume MI2: "\<And>T1 T2. T = T1 => T2 \<Longrightarrow> PROP ?P T2"
   4.291 +  assume MI1: "\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> PROP ?P T1"
   4.292 +  assume MI2: "\<And>T1 T2. T = T1 \<rightarrow> T2 \<Longrightarrow> PROP ?P T2"
   4.293    assume "t \<in> IT"
   4.294    thus "\<And>e T' u i. PROP ?Q t e T' u i T"
   4.295    proof induct
   4.296      fix e T' u i
   4.297 -    assume uIT: "u : IT"
   4.298 -    assume uT: "e |- u : T"
   4.299 +    assume uIT: "u \<in> IT"
   4.300 +    assume uT: "e \<turnstile> u : T"
   4.301      {
   4.302        case (Var n rs)
   4.303 -      assume nT: "e<i:T> |- Var n $$ rs : T'"
   4.304 -      let ?ty = "{t. \<exists>T'. e<i:T> |- t : T'}"
   4.305 +      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree>\<^sub>\<degree> rs : T'"
   4.306 +      let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
   4.307        let ?R = "\<lambda>t. \<forall>e T' u i.
   4.308 -	e<i:T> |- t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e |- u : T \<longrightarrow> t[u/i] \<in> IT"
   4.309 -      show "(Var n $$ rs)[u/i] \<in> IT"
   4.310 +        e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
   4.311 +      show "(Var n \<^sub>\<degree>\<^sub>\<degree> rs)[u/i] \<in> IT"
   4.312        proof (cases "n = i")
   4.313 -	case True
   4.314 -	show ?thesis
   4.315 -	proof (cases rs)
   4.316 -	  case Nil
   4.317 -	  with uIT True show ?thesis by simp
   4.318 -	next
   4.319 -	  case (Cons a as)
   4.320 -	  with nT have "e<i:T> |- Var n $ a $$ as : T'" by simp
   4.321 -	  then obtain Ts
   4.322 -	    where headT: "e<i:T> |- Var n $ a : Ts =>> T'"
   4.323 -	    and argsT: "types (e<i:T>) as Ts"
   4.324 -	    by (rule list_app_typeE)
   4.325 -	  from headT obtain T''
   4.326 -	    where varT: "e<i:T> |- Var n : T'' => (Ts =>> T')"
   4.327 -	    and argT: "e<i:T> |- a : T''"
   4.328 -	    by cases simp_all
   4.329 -	  from varT True have T: "T = T'' => (Ts =>> T')"
   4.330 -	    by cases (auto simp add: shift_def)
   4.331 -	  with uT have uT': "e |- u : T'' => (Ts =>> T')" by simp
   4.332 -	  from Var have SI: "?R a" by cases (simp_all add: Cons)
   4.333 -	  from T have "(Var 0 $$ map (\<lambda>t. lift t 0)
   4.334 -            (map (\<lambda>t. t[u/i]) as))[(u $ a[u/i])/0] \<in> IT"
   4.335 -	  proof (rule MI2)
   4.336 -	    from T have "(lift u 0 $ Var 0)[a[u/i]/0] \<in> IT"
   4.337 -	    proof (rule MI1)
   4.338 -	      have "lift u 0 : IT" by (rule lift_IT)
   4.339 -	      thus "lift u 0 $ Var 0 \<in> IT" by (rule app_Var_IT)
   4.340 -	      show "e<0:T''> |- lift u 0 $ Var 0 : Ts =>> T'"
   4.341 -	      proof (rule typing.App)
   4.342 -		show "e<0:T''> |- lift u 0 : T'' => (Ts =>> T')"
   4.343 -		  by (rule lift_type') (rule uT')
   4.344 -		show "e<0:T''> |- Var 0 : T''"
   4.345 -		  by (rule typing.Var) (simp add: shift_def)
   4.346 -	      qed
   4.347 -	      from argT uIT uT show "a[u/i] : IT"
   4.348 -		by (rule SI[rule_format])
   4.349 -	      from argT uT show "e |- a[u/i] : T''"
   4.350 -		by (rule subst_lemma) (simp add: shift_def)
   4.351 -	    qed
   4.352 -	    thus "u $ a[u/i] \<in> IT" by simp
   4.353 -	    from Var have "as : lists {t. ?R t}"
   4.354 -	      by cases (simp_all add: Cons)
   4.355 -	    moreover from argsT have "as : lists ?ty"
   4.356 -	      by (rule lists_types)
   4.357 -	    ultimately have "as : lists ({t. ?R t} \<inter> ?ty)"
   4.358 -	      by (rule lists_IntI)
   4.359 -	    hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
   4.360 -	      (is "(?ls as) \<in> _")
   4.361 -	    proof induct
   4.362 -	      case Nil
   4.363 -	      show ?case by fastsimp
   4.364 -	    next
   4.365 -	      case (Cons b bs)
   4.366 -	      hence I: "?R b" by simp
   4.367 -	      from Cons obtain U where "e<i:T> |- b : U" by fast
   4.368 -	      with uT uIT I have "b[u/i] : IT" by simp
   4.369 -	      hence "lift (b[u/i]) 0 : IT" by (rule lift_IT)
   4.370 -	      hence "lift (b[u/i]) 0 # ?ls bs \<in> lists IT"
   4.371 -		by (rule lists.Cons) (rule Cons)
   4.372 -	      thus ?case by simp
   4.373 -	    qed
   4.374 -	    thus "Var 0 $$ ?ls as \<in> IT" by (rule IT.Var)
   4.375 -	    have "e<0:Ts =>> T'> |- Var 0 : Ts =>> T'"
   4.376 -	      by (rule typing.Var) (simp add: shift_def)
   4.377 -	    moreover from uT argsT have "types e (map (\<lambda>t. t[u/i]) as) Ts"
   4.378 -	      by (rule substs_lemma)
   4.379 -	    hence "types (e<0:Ts =>> T'>) (?ls as) Ts"
   4.380 -	      by (rule lift_types)
   4.381 -	    ultimately show "e<0:Ts =>> T'> |- Var 0 $$ ?ls as : T'"
   4.382 -	      by (rule list_app_typeI)
   4.383 -	    from argT uT have "e |- a[u/i] : T''"
   4.384 -	      by (rule subst_lemma) (rule refl)
   4.385 -	    with uT' show "e |- u $ a[u/i] : Ts =>> T'"
   4.386 -	      by (rule typing.App)
   4.387 -	  qed
   4.388 -	  with Cons True show ?thesis
   4.389 -	    by (simp add: map_compose [symmetric] o_def)
   4.390 -	qed
   4.391 +        case True
   4.392 +        show ?thesis
   4.393 +        proof (cases rs)
   4.394 +          case Nil
   4.395 +          with uIT True show ?thesis by simp
   4.396 +        next
   4.397 +          case (Cons a as)
   4.398 +          with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'" by simp
   4.399 +          then obtain Ts
   4.400 +              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a : Ts =\<guillemotright> T'"
   4.401 +              and argsT: "(e\<langle>i:T\<rangle>) \<tturnstile> as : Ts"
   4.402 +            by (rule list_app_typeE)
   4.403 +          from headT obtain T''
   4.404 +              where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<rightarrow> Ts =\<guillemotright> T'"
   4.405 +              and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''"
   4.406 +            by cases simp_all
   4.407 +          from varT True have T: "T = T'' \<rightarrow> Ts =\<guillemotright> T'"
   4.408 +            by cases (auto simp add: shift_def)
   4.409 +          with uT have uT': "e \<turnstile> u : T'' \<rightarrow> Ts =\<guillemotright> T'" by simp
   4.410 +          from Var have SI: "?R a" by cases (simp_all add: Cons)
   4.411 +          from T have "(Var 0 \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t 0)
   4.412 +            (map (\<lambda>t. t[u/i]) as))[(u \<^sub>\<degree> a[u/i])/0] \<in> IT"
   4.413 +          proof (rule MI2)
   4.414 +            from T have "(lift u 0 \<^sub>\<degree> Var 0)[a[u/i]/0] \<in> IT"
   4.415 +            proof (rule MI1)
   4.416 +              have "lift u 0 \<in> IT" by (rule lift_IT)
   4.417 +              thus "lift u 0 \<^sub>\<degree> Var 0 \<in> IT" by (rule app_Var_IT)
   4.418 +              show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<^sub>\<degree> Var 0 : Ts =\<guillemotright> T'"
   4.419 +              proof (rule typing.App)
   4.420 +                show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<rightarrow> Ts =\<guillemotright> T'"
   4.421 +                  by (rule lift_type') (rule uT')
   4.422 +                show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''"
   4.423 +                  by (rule typing.Var) (simp add: shift_def)
   4.424 +              qed
   4.425 +              from argT uIT uT show "a[u/i] \<in> IT"
   4.426 +                by (rule SI[rule_format])
   4.427 +              from argT uT show "e \<turnstile> a[u/i] : T''"
   4.428 +                by (rule subst_lemma) (simp add: shift_def)
   4.429 +            qed
   4.430 +            thus "u \<^sub>\<degree> a[u/i] \<in> IT" by simp
   4.431 +            from Var have "as \<in> lists {t. ?R t}"
   4.432 +              by cases (simp_all add: Cons)
   4.433 +            moreover from argsT have "as \<in> lists ?ty"
   4.434 +              by (rule lists_typings)
   4.435 +            ultimately have "as \<in> lists ({t. ?R t} \<inter> ?ty)"
   4.436 +              by (rule lists_IntI)
   4.437 +            hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
   4.438 +              (is "(?ls as) \<in> _")
   4.439 +            proof induct
   4.440 +              case Nil
   4.441 +              show ?case by fastsimp
   4.442 +            next
   4.443 +              case (Cons b bs)
   4.444 +              hence I: "?R b" by simp
   4.445 +              from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast
   4.446 +              with uT uIT I have "b[u/i] \<in> IT" by simp
   4.447 +              hence "lift (b[u/i]) 0 \<in> IT" by (rule lift_IT)
   4.448 +              hence "lift (b[u/i]) 0 # ?ls bs \<in> lists IT"
   4.449 +                by (rule lists.Cons) (rule Cons)
   4.450 +              thus ?case by simp
   4.451 +            qed
   4.452 +            thus "Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as \<in> IT" by (rule IT.Var)
   4.453 +            have "e\<langle>0:Ts =\<guillemotright> T'\<rangle> \<turnstile> Var 0 : Ts =\<guillemotright> T'"
   4.454 +              by (rule typing.Var) (simp add: shift_def)
   4.455 +            moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
   4.456 +              by (rule substs_lemma)
   4.457 +            hence "(e\<langle>0:Ts =\<guillemotright> T'\<rangle>) \<tturnstile> ?ls as : Ts"
   4.458 +              by (rule lift_typings)
   4.459 +            ultimately show "e\<langle>0:Ts =\<guillemotright> T'\<rangle> \<turnstile> Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as : T'"
   4.460 +              by (rule list_app_typeI)
   4.461 +            from argT uT have "e \<turnstile> a[u/i] : T''"
   4.462 +              by (rule subst_lemma) (rule refl)
   4.463 +            with uT' show "e \<turnstile> u \<^sub>\<degree> a[u/i] : Ts =\<guillemotright> T'"
   4.464 +              by (rule typing.App)
   4.465 +          qed
   4.466 +          with Cons True show ?thesis
   4.467 +            by (simp add: map_compose [symmetric] o_def)
   4.468 +        qed
   4.469        next
   4.470 -	case False
   4.471 -	from Var have "rs : lists {t. ?R t}" by simp
   4.472 -	moreover from nT obtain Ts where "types (e<i:T>) rs Ts"
   4.473 -	  by (rule list_app_typeE)
   4.474 -	hence "rs : lists ?ty" by (rule lists_types)
   4.475 -	ultimately have "rs : lists ({t. ?R t} \<inter> ?ty)"
   4.476 -	  by (rule lists_IntI)
   4.477 -	hence "map (\<lambda>x. x[u/i]) rs \<in> lists IT"
   4.478 -	proof induct
   4.479 -	  case Nil
   4.480 -	  show ?case by fastsimp
   4.481 -	next
   4.482 -	  case (Cons a as)
   4.483 -	  hence I: "?R a" by simp
   4.484 -	  from Cons obtain U where "e<i:T> |- a : U" by fast
   4.485 -	  with uT uIT I have "a[u/i] : IT" by simp
   4.486 -	  hence "a[u/i] # map (\<lambda>t. t[u/i]) as \<in> lists IT"
   4.487 -	    by (rule lists.Cons) (rule Cons)
   4.488 -	  thus ?case by simp
   4.489 -	qed
   4.490 -	with False show ?thesis by (auto simp add: subst_Var)
   4.491 +        case False
   4.492 +        from Var have "rs \<in> lists {t. ?R t}" by simp
   4.493 +        moreover from nT obtain Ts where "(e\<langle>i:T\<rangle>) \<tturnstile> rs : Ts"
   4.494 +          by (rule list_app_typeE)
   4.495 +        hence "rs \<in> lists ?ty" by (rule lists_typings)
   4.496 +        ultimately have "rs \<in> lists ({t. ?R t} \<inter> ?ty)"
   4.497 +          by (rule lists_IntI)
   4.498 +        hence "map (\<lambda>x. x[u/i]) rs \<in> lists IT"
   4.499 +        proof induct
   4.500 +          case Nil
   4.501 +          show ?case by fastsimp
   4.502 +        next
   4.503 +          case (Cons a as)
   4.504 +          hence I: "?R a" by simp
   4.505 +          from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast
   4.506 +          with uT uIT I have "a[u/i] \<in> IT" by simp
   4.507 +          hence "(a[u/i] # map (\<lambda>t. t[u/i]) as) \<in> lists IT"
   4.508 +            by (rule lists.Cons) (rule Cons)
   4.509 +          thus ?case by simp
   4.510 +        qed
   4.511 +        with False show ?thesis by (auto simp add: subst_Var)
   4.512        qed
   4.513      next
   4.514        case (Lambda r)
   4.515 -      assume "e<i:T> |- Abs r : T'"
   4.516 -	and "\<And>e T' u i. PROP ?Q r e T' u i T"
   4.517 +      assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
   4.518 +        and "\<And>e T' u i. PROP ?Q r e T' u i T"
   4.519        with uIT uT show "Abs r[u/i] \<in> IT"
   4.520 -	by (fastsimp simp add: shift_def)
   4.521 +        by (fastsimp simp add: shift_def)
   4.522      next
   4.523        case (Beta r a as)
   4.524 -      assume T: "e<i:T> |- Abs r $ a $$ as : T'"
   4.525 -      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] $$ as) e T' u i T"
   4.526 +      assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'"
   4.527 +      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<^sub>\<degree>\<^sub>\<degree> as) e T' u i T"
   4.528        assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
   4.529 -      have "Abs (r[lift u 0/Suc i]) $ a[u/i] $$ map (\<lambda>t. t[u/i]) as \<in> IT"
   4.530 +      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"
   4.531        proof (rule IT.Beta)
   4.532 -	have "Abs r $ a $$ as -> r[a/0] $$ as"
   4.533 -	  by (rule apps_preserves_beta) (rule beta.beta)
   4.534 -	with T have "e<i:T> |- r[a/0] $$ as : T'"
   4.535 -	  by (rule subject_reduction)
   4.536 -	hence "(r[a/0] $$ as)[u/i] \<in> IT"
   4.537 -	  by (rule SI1)
   4.538 -	thus "r[lift u 0/Suc i][a[u/i]/0] $$ map (\<lambda>t. t[u/i]) as \<in> IT"
   4.539 -	  by (simp del: subst_map add: subst_subst subst_map [symmetric])
   4.540 -	from T obtain U where "e<i:T> |- Abs r $ a : U"
   4.541 -	  by (rule list_app_typeE) fast
   4.542 -	then obtain T'' where "e<i:T> |- a : T''" by cases simp_all
   4.543 -	thus "a[u/i] \<in> IT" by (rule SI2)
   4.544 +        have "Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as -> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as"
   4.545 +          by (rule apps_preserves_beta) (rule beta.beta)
   4.546 +        with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as : T'"
   4.547 +          by (rule subject_reduction)
   4.548 +        hence "(r[a/0] \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT"
   4.549 +          by (rule SI1)
   4.550 +        thus "r[lift u 0/Suc i][a[u/i]/0] \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
   4.551 +          by (simp del: subst_map add: subst_subst subst_map [symmetric])
   4.552 +        from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a : U"
   4.553 +          by (rule list_app_typeE) fast
   4.554 +        then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
   4.555 +        thus "a[u/i] \<in> IT" by (rule SI2)
   4.556        qed
   4.557 -      thus "(Abs r $ a $$ as)[u/i] \<in> IT" by simp
   4.558 +      thus "(Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT" by simp
   4.559      }
   4.560    qed
   4.561  qed
   4.562  
   4.563  subsection {* Well-typed terms are strongly normalizing *}
   4.564  
   4.565 -lemma type_implies_IT: "e |- t : T ==> t \<in> IT"
   4.566 +lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"
   4.567  proof -
   4.568 -  assume "e |- t : T"
   4.569 +  assume "e \<turnstile> t : T"
   4.570    thus ?thesis
   4.571    proof induct
   4.572      case Var
   4.573 @@ -513,27 +520,27 @@
   4.574      show ?case by (rule IT.Lambda)
   4.575    next
   4.576      case (App T U e s t)
   4.577 -    have "(Var 0 $ lift t 0)[s/0] \<in> IT"
   4.578 +    have "(Var 0 \<^sub>\<degree> lift t 0)[s/0] \<in> IT"
   4.579      proof (rule subst_type_IT)
   4.580 -      have "lift t 0 : IT" by (rule lift_IT)
   4.581 -      hence "[lift t 0] : lists IT" by (rule lists.Cons) (rule lists.Nil)
   4.582 -      hence "Var 0 $$ [lift t 0] : IT" by (rule IT.Var)
   4.583 -      also have "(Var 0 $$ [lift t 0]) = (Var 0 $ lift t 0)" by simp
   4.584 -      finally show "\<dots> : IT" .
   4.585 -      have "e<0:T => U> |- Var 0 : T => U"
   4.586 -	by (rule typing.Var) (simp add: shift_def)
   4.587 -      moreover have "e<0:T => U> |- lift t 0 : T"
   4.588 -	by (rule lift_type')
   4.589 -      ultimately show "e<0:T => U> |- Var 0 $ lift t 0 : U"
   4.590 -	by (rule typing.App)
   4.591 +      have "lift t 0 \<in> IT" by (rule lift_IT)
   4.592 +      hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
   4.593 +      hence "Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
   4.594 +      also have "(Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0]) = (Var 0 \<^sub>\<degree> lift t 0)" by simp
   4.595 +      finally show "\<dots> \<in> IT" .
   4.596 +      have "e\<langle>0:T \<rightarrow> U\<rangle> \<turnstile> Var 0 : T \<rightarrow> U"
   4.597 +        by (rule typing.Var) (simp add: shift_def)
   4.598 +      moreover have "e\<langle>0:T \<rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
   4.599 +        by (rule lift_type')
   4.600 +      ultimately show "e\<langle>0:T \<rightarrow> U\<rangle> \<turnstile> Var 0 \<^sub>\<degree> lift t 0 : U"
   4.601 +        by (rule typing.App)
   4.602      qed
   4.603      thus ?case by simp
   4.604    qed
   4.605  qed
   4.606  
   4.607 -theorem type_implies_termi: "e |- t : T ==> t \<in> termi beta"
   4.608 +theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
   4.609  proof -
   4.610 -  assume "e |- t : T"
   4.611 +  assume "e \<turnstile> t : T"
   4.612    hence "t \<in> IT" by (rule type_implies_IT)
   4.613    thus ?thesis by (rule IT_implies_termi)
   4.614  qed