diff -r e1d4df962ac9 -r 1a3a7b3cd9bb src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/Type.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -18,8 +18,10 @@
 subsection {* Environments *}
 
 constdefs
+  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
+  "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
+syntax (symbols)
   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)"
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   by (simp add: shift_def)
@@ -69,11 +71,11 @@
   intros
     Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
     Abs [intro!]: "env\<langle>0:T\<rangle> \<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"
+    App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
 
 inductive_cases typing_elims [elim!]:
   "e \<turnstile> Var i : T"
-  "e \<turnstile> t \<^sub>\<degree> u : T"
+  "e \<turnstile> t \<degree> u : T"
   "e \<turnstile> Abs t : T"
 
 primrec
@@ -86,44 +88,44 @@
 
 subsection {* Some examples *}
 
-lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<^sub>\<degree> (Var 2 \<^sub>\<degree> Var 1 \<^sub>\<degree> Var 0)))) : ?T"
+lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
   by force
 
-lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<^sub>\<degree> Var 0 \<^sub>\<degree> (Var 1 \<^sub>\<degree> Var 0)))) : ?T"
+lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
   by force
 
 
 subsection {* n-ary function types *}
 
 lemma list_app_typeD:
-    "\<And>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
+    "\<And>t T. e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
   apply (induct ts)
    apply simp
   apply atomize
   apply simp
-  apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
+  apply (erule_tac x = "t \<degree> a" in allE)
   apply (erule_tac x = T in allE)
   apply (erule impE)
    apply assumption
   apply (elim exE conjE)
-  apply (ind_cases "e \<turnstile> t \<^sub>\<degree> u : T")
+  apply (ind_cases "e \<turnstile> t \<degree> u : T")
   apply (rule_tac x = "Ta # Ts" in exI)
   apply simp
   done
 
 lemma list_app_typeE:
-  "e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
+  "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
   by (insert list_app_typeD) fast
 
 lemma list_app_typeI:
-    "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
+    "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
   apply (induct ts)
    apply simp
   apply atomize
   apply (case_tac Ts)
    apply simp
   apply simp
-  apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
+  apply (erule_tac x = "t \<degree> a" in allE)
   apply (erule_tac x = T in allE)
   apply (erule_tac x = lista in allE)
   apply (erule impE)
@@ -152,11 +154,11 @@
 subsection {* Lifting preserves termination and well-typedness *}
 
 lemma lift_map [simp]:
-    "\<And>t. lift (t \<^sub>\<degree>\<^sub>\<degree> ts) i = lift t i \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t i) ts"
+    "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
   by (induct ts) simp_all
 
 lemma subst_map [simp]:
-    "\<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"
+    "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
   by (induct ts) simp_all
 
 lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> (\<And>i. lift t i \<in> IT)"
@@ -206,39 +208,19 @@
   apply blast
   done
 
-lemma substs_lemma [rule_format]:
-  "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<longrightarrow>
+lemma substs_lemma:
+  "\<And>Ts. e \<turnstile> u : T \<Longrightarrow> 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 (induct ts)
    apply (case_tac Ts)
     apply simp
    apply simp
-  apply (intro strip)
+  apply atomize
   apply (case_tac Ts)
    apply simp
   apply simp
   apply (erule conjE)
-  apply (erule subst_lemma)
-   apply assumption
-  apply (rule refl)
-  done
-
-lemma substs_lemma [rule_format]:
-  "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)
-    apply simp
-   apply simp
-  apply (intro strip)
-  apply (case_tac Ts)
-   apply simp
-  apply simp
-  apply (erule conjE)
-  apply (erule subst_lemma)
-   apply assumption
+  apply (erule (1) subst_lemma)
   apply (rule refl)
   done
 
@@ -250,7 +232,7 @@
     apply blast
    apply blast
   apply atomize
-  apply (ind_cases "s \<^sub>\<degree> t -> t'")
+  apply (ind_cases "s \<degree> t -> t'")
     apply hypsubst
     apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
     apply (rule subst_lemma)
@@ -264,13 +246,12 @@
 
 subsection {* Additional lemmas *}
 
-lemma app_last: "(t \<^sub>\<degree>\<^sub>\<degree> ts) \<^sub>\<degree> u = t \<^sub>\<degree>\<^sub>\<degree> (ts @ [u])"
+lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
   by simp
 
 lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> (\<And>i j. r[Var i/j] \<in> IT)"
   apply (induct set: IT)
     txt {* Case @{term Var}: *}
-    apply atomize
     apply (simp (no_asm) add: subst_Var)
     apply
     ((rule conjI impI)+,
@@ -297,13 +278,13 @@
   done
 
 lemma Var_IT: "Var n \<in> IT"
-  apply (subgoal_tac "Var n \<^sub>\<degree>\<^sub>\<degree> [] \<in> IT")
+  apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
    apply simp
   apply (rule IT.Var)
   apply (rule lists.Nil)
   done
 
-lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<^sub>\<degree> Var i \<in> IT"
+lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
   apply (induct set: IT)
     apply (subst app_last)
     apply (rule IT.Var)
@@ -355,11 +336,11 @@
     assume uT: "e \<turnstile> u : T"
     {
       case (Var n rs)
-      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree>\<^sub>\<degree> rs : T'"
+      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<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\<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"
+      show "(Var n \<degree>\<degree> rs)[u/i] \<in> IT"
       proof (cases "n = i")
         case True
         show ?thesis
@@ -368,9 +349,9 @@
           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
+          with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp
           then obtain Ts
-              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a : Ts \<Rrightarrow> T'"
+              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'"
               and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
             by (rule list_app_typeE)
           from headT obtain T''
@@ -380,14 +361,14 @@
           from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
             by cases auto
           with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
-          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"
+          from T have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
+            (map (\<lambda>t. t[u/i]) as))[(u \<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"
+            from T have "(lift u 0 \<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 \<Rrightarrow> T'"
+              thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
+              show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
               proof (rule typing.App)
                 show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
                   by (rule lift_type) (rule uT')
@@ -399,7 +380,7 @@
               from argT uT show "e \<turnstile> a[u/i] : T''"
                 by (rule subst_lemma) simp
             qed
-            thus "u \<^sub>\<degree> a[u/i] \<in> IT" by simp
+            thus "u \<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"
@@ -421,18 +402,18 @@
                 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)
+            thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
             have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
               by (rule typing.Var) simp
             moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
               by (rule substs_lemma)
             hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
               by (rule lift_typings)
-            ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as : T'"
+            ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<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 \<Rrightarrow> T'"
+            with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'"
               by (rule typing.App)
           qed
           with Cons True show ?thesis
@@ -469,25 +450,25 @@
         by fastsimp
     next
       case (Beta r a as)
-      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 T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
+      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<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]) \<^sub>\<degree> a[u/i] \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+      have "Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
       proof (rule IT.Beta)
-        have "Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as -> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as"
+        have "Abs r \<degree> a \<degree>\<degree> as -> r[a/0] \<degree>\<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'"
+        with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
           by (rule subject_reduction)
-        hence "(r[a/0] \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT"
+        hence "(r[a/0] \<degree>\<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"
+        thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<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"
+        from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<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 \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT" by simp
+      thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
     }
   qed
 qed
@@ -506,18 +487,18 @@
     show ?case by (rule IT.Lambda)
   next
     case (App T U e s t)
-    have "(Var 0 \<^sub>\<degree> lift t 0)[s/0] \<in> IT"
+    have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
     proof (rule subst_type_IT)
       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
+      hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
+      also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<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
       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"
+      ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
         by (rule typing.App)
     qed
     thus ?case by simp