# HG changeset patch
# User wenzelm
# Date 1004562337 -3600
# Node ID 1a3a7b3cd9bb28501d62f90c02fd6a2c4143818a
# Parent  e1d4df962ac973798dbd7074912cf7251fdb184a
tuned notation (degree instead of dollar);

diff -r e1d4df962ac9 -r 1a3a7b3cd9bb src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/Eta.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -15,7 +15,7 @@
   free :: "dB => nat => bool"
 primrec
   "free (Var j) i = (j = i)"
-  "free (s $ t) i = (free s i \<or> free t i)"
+  "free (s \<degree> t) i = (free s i \<or> free t i)"
   "free (Abs s) i = free s (i + 1)"
 
 consts
@@ -32,14 +32,14 @@
 
 inductive eta
   intros
-    eta [simp, intro]: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
-    appL [simp, intro]: "s -e> t ==> s $ u -e> t $ u"
-    appR [simp, intro]: "s -e> t ==> u $ s -e> u $ t"
+    eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) -e> s[dummy/0]"
+    appL [simp, intro]: "s -e> t ==> s \<degree> u -e> t \<degree> u"
+    appR [simp, intro]: "s -e> t ==> u \<degree> s -e> u \<degree> t"
     abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"
 
 inductive_cases eta_cases [elim!]:
   "Abs s -e> z"
-  "s $ t -e> u"
+  "s \<degree> t -e> u"
   "Var i -e> t"
 
 
@@ -118,18 +118,18 @@
    apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   done
 
-lemma rtrancl_eta_AppL: "s -e>> s' ==> s $ t -e>> s' $ t"
+lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
   apply (erule rtrancl_induct)
    apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   done
 
-lemma rtrancl_eta_AppR: "t -e>> t' ==> s $ t -e>> s $ t'"
+lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
   apply (erule rtrancl_induct)
    apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   done
 
 lemma rtrancl_eta_App:
-    "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"
+    "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
   apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
   done
 
@@ -189,7 +189,7 @@
 
 subsection "Implicit definition of eta"
 
-text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
+text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
 
 lemma not_free_iff_lifted [rule_format]:
     "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
@@ -218,7 +218,7 @@
    apply (rule iffI)
     apply (elim conjE exE)
     apply (rename_tac u1 u2)
-    apply (rule_tac x = "u1 $ u2" in exI)
+    apply (rule_tac x = "u1 \<degree> u2" in exI)
     apply simp
    apply (erule exE)
    apply (erule rev_mp)
@@ -244,8 +244,8 @@
   done
 
 theorem explicit_is_implicit:
-  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) =
-    (\<forall>s. R (Abs (lift s 0 $ Var 0)) s)"
+  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
+    (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
   apply (auto simp add: not_free_iff_lifted)
   done
 
diff -r e1d4df962ac9 -r 1a3a7b3cd9bb src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/InductTermi.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -19,16 +19,16 @@
 
 inductive IT
   intros
-    Var [intro]: "rs : lists IT ==> Var n $$ rs : IT"
+    Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT"
     Lambda [intro]: "r : IT ==> Abs r : IT"
-    Beta [intro]: "(r[s/0]) $$ ss : IT ==> s : IT ==> (Abs r $ s) $$ ss : IT"
+    Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> ss : IT"
 
 
 subsection {* Every term in IT terminates *}
 
 lemma double_induction_lemma [rule_format]:
   "s : termi beta ==> \<forall>t. t : termi beta -->
-    (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
+    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)"
   apply (erule acc_induct)
   apply (erule thin_rl)
   apply (rule allI)
@@ -65,19 +65,19 @@
 
 declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
 
-lemma [simp, THEN not_sym, simp]: "Var n $$ ss \<noteq> Abs r $ s $$ ts"
+lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
   apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
   done
 
 lemma [simp]:
-  "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \<and> s = s' \<and> ss = ss')"
+  "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
   apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
   done
 
 inductive_cases [elim!]:
-  "Var n $$ ss : IT"
+  "Var n \<degree>\<degree> ss : IT"
   "Abs t : IT"
-  "Abs r $ s $$ ts : IT"
+  "Abs r \<degree> s \<degree>\<degree> ts : IT"
 
 theorem termi_implies_IT: "r : termi beta ==> r : IT"
   apply (erule acc_induct)
@@ -96,7 +96,7 @@
    apply (drule ex_step1I, assumption)
    apply clarify
    apply (rename_tac us)
-   apply (erule_tac x = "Var n $$ us" in allE)
+   apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
    apply force
    apply (rename_tac u ts)
    apply (case_tac ts)
@@ -110,7 +110,7 @@
    apply (erule mp)
    apply clarify
    apply (rename_tac t)
-   apply (erule_tac x = "Abs u $ t $$ ss" in allE)
+   apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE)
    apply force
    done
 
diff -r e1d4df962ac9 -r 1a3a7b3cd9bb src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -13,25 +13,22 @@
 
 datatype dB =
     Var nat
-  | App dB dB (infixl "$" 200)
+  | App dB dB (infixl "\<degree>" 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"
 
 primrec
   "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
-  "lift (s $ t) k = lift s k $ lift t k"
+  "lift (s \<degree> t) k = lift s k \<degree> lift t k"
   "lift (Abs s) k = Abs (lift s (k + 1))"
 
 primrec  (* FIXME base names *)
   subst_Var: "(Var i)[s/k] =
     (if k < i then Var (i - 1) else if i = k then s else Var i)"
-  subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]"
+  subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
   subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
 
 declare subst_Var [simp del]
@@ -44,13 +41,13 @@
 
 primrec
   "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
-  "liftn n (s $ t) k = liftn n s k $ liftn n t k"
+  "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
   "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
 
 primrec
   "substn (Var i) s k =
     (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
-  "substn (t $ u) s k = substn t s k $ substn u s k"
+  "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
   "substn (Abs t) s k = Abs (substn t s (k + 1))"
 
 
@@ -68,15 +65,15 @@
 
 inductive beta
   intros
-    beta [simp, intro!]: "Abs s $ t -> s[t/0]"
-    appL [simp, intro!]: "s -> t ==> s $ u -> t $ u"
-    appR [simp, intro!]: "s -> t ==> u $ s -> u $ t"
+    beta [simp, intro!]: "Abs s \<degree> t -> s[t/0]"
+    appL [simp, intro!]: "s -> t ==> s \<degree> u -> t \<degree> u"
+    appR [simp, intro!]: "s -> t ==> u \<degree> s -> u \<degree> t"
     abs [simp, intro!]: "s -> t ==> Abs s -> Abs t"
 
 inductive_cases beta_cases [elim!]:
   "Var i -> t"
   "Abs r -> s"
-  "s $ t -> u"
+  "s \<degree> t -> u"
 
 declare if_not_P [simp] not_less_eq [simp]
   -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
@@ -91,19 +88,19 @@
   done
 
 lemma rtrancl_beta_AppL:
-    "s ->> s' ==> s $ t ->> s' $ t"
+    "s ->> s' ==> s \<degree> t ->> s' \<degree> t"
   apply (erule rtrancl_induct)
    apply (blast intro: rtrancl_into_rtrancl)+
   done
 
 lemma rtrancl_beta_AppR:
-    "t ->> t' ==> s $ t ->> s $ t'"
+    "t ->> t' ==> s \<degree> t ->> s \<degree> t'"
   apply (erule rtrancl_induct)
    apply (blast intro: rtrancl_into_rtrancl)+
   done
 
 lemma rtrancl_beta_App [intro]:
-    "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'"
+    "[| s ->> s'; t ->> t' |] ==> s \<degree> t ->> s' \<degree> t'"
   apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
     intro: rtrancl_trans)
   done
diff -r e1d4df962ac9 -r 1a3a7b3cd9bb src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/ListApplication.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -9,26 +9,23 @@
 theory ListApplication = Lambda:
 
 syntax
-  "_list_application" :: "dB => dB list => dB"    (infixl "$$" 150)
-syntax (symbols)
-  "_list_application" :: "dB => dB list => dB"    (infixl "\<^sub>\<degree>\<^sub>\<degree>" 150)
+  "_list_application" :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
+translations
+  "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
 
-translations
-  "t $$ ts" == "foldl (op $) t ts"
-
-lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
+lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
   apply (induct_tac ts rule: rev_induct)
    apply auto
   done
 
 lemma Var_eq_apps_conv [rule_format, iff]:
-    "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
+    "\<forall>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
   apply (induct_tac ss)
    apply auto
   done
 
 lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
-    "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
+    "\<forall>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
   apply (induct_tac rs rule: rev_induct)
    apply simp
    apply blast
@@ -38,26 +35,26 @@
   done
 
 lemma App_eq_foldl_conv:
-  "(r $ s = t $$ ts) =
-    (if ts = [] then r $ s = t
-    else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
+  "(r \<degree> s = t \<degree>\<degree> ts) =
+    (if ts = [] then r \<degree> s = t
+    else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
   apply (rule_tac xs = ts in rev_exhaust)
    apply auto
   done
 
 lemma Abs_eq_apps_conv [iff]:
-    "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
+    "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
   apply (induct_tac ss rule: rev_induct)
    apply auto
   done
 
-lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
+lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
   apply (induct_tac ss rule: rev_induct)
    apply auto
   done
 
 lemma Abs_apps_eq_Abs_apps_conv [iff]:
-    "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
+    "\<forall>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
   apply (induct_tac rs rule: rev_induct)
    apply simp
    apply blast
@@ -67,13 +64,13 @@
   done
 
 lemma Abs_App_neq_Var_apps [iff]:
-    "\<forall>s t. Abs s $ t ~= Var n $$ ss"
+    "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
   apply (induct_tac ss rule: rev_induct)
    apply auto
   done
 
 lemma Var_apps_neq_Abs_apps [rule_format, iff]:
-    "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
+    "\<forall>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
   apply (induct_tac ss rule: rev_induct)
    apply simp
   apply (rule allI)
@@ -82,19 +79,19 @@
   done
 
 lemma ex_head_tail:
-  "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
+  "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
   apply (induct_tac t)
     apply (rule_tac x = "[]" in exI)
     apply simp
    apply clarify
    apply (rename_tac ts1 ts2 h1 h2)
-   apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
+   apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI)
    apply simp
   apply simp
   done
 
 lemma size_apps [simp]:
-  "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
+  "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
   apply (induct_tac rs rule: rev_induct)
    apply auto
   done
@@ -104,11 +101,11 @@
   done
 
 
-text {* \medskip A customized induction schema for @{text "$$"}. *}
+text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
 
 lemma lem [rule_format (no_asm)]:
-  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
-    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
+    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
   |] ==> \<forall>t. size t = n --> P t"
 proof -
   case rule_context
@@ -149,8 +146,8 @@
 qed
 
 theorem Apps_dB_induct:
-  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
-    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
+    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
   |] ==> P t"
 proof -
   case rule_context
diff -r e1d4df962ac9 -r 1a3a7b3cd9bb src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -18,7 +18,7 @@
   "rs => ss" == "(rs, ss) : step1 beta"
 
 lemma head_Var_reduction_aux:
-  "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
+  "v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)"
   apply (erule beta.induct)
      apply simp
     apply (rule allI)
@@ -32,16 +32,16 @@
   done
 
 lemma head_Var_reduction:
-  "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
+  "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
   apply (drule head_Var_reduction_aux)
   apply blast
   done
 
 lemma apps_betasE_aux:
-  "u -> u' ==> \<forall>r rs. u = r $$ rs -->
-    ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
-     (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
-     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
+  "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
+    ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
+     (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
+     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
   apply (erule beta.induct)
      apply (clarify del: disjCI)
      apply (case_tac r)
@@ -70,12 +70,12 @@
   done
 
 lemma apps_betasE [elim!]:
-  "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
-    !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
-    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
+  "[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R;
+    !!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R;
+    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |]
   ==> R"
 proof -
-  assume major: "r $$ rs -> s"
+  assume major: "r \<degree>\<degree> rs -> s"
   case rule_context
   show ?thesis
     apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
@@ -84,20 +84,20 @@
 qed
 
 lemma apps_preserves_beta [simp]:
-    "r -> s ==> r $$ ss -> s $$ ss"
+    "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
   apply (induct_tac ss rule: rev_induct)
   apply auto
   done
 
 lemma apps_preserves_beta2 [simp]:
-    "r ->> s ==> r $$ ss ->> s $$ ss"
+    "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
   apply (erule rtrancl_induct)
    apply blast
   apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
   done
 
 lemma apps_preserves_betas [rule_format, simp]:
-    "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
+    "\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
   apply (induct_tac rs rule: rev_induct)
    apply simp
   apply simp
diff -r e1d4df962ac9 -r 1a3a7b3cd9bb src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -26,14 +26,14 @@
   intros
     var [simp, intro!]: "Var n => Var n"
     abs [simp, intro!]: "s => t ==> Abs s => Abs t"
-    app [simp, intro!]: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
-    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
+    app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
+    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
 
 inductive_cases par_beta_cases [elim!]:
   "Var n => t"
   "Abs s => Abs t"
-  "(Abs s) $ t => u"
-  "s $ t => u"
+  "(Abs s) \<degree> t => u"
+  "s \<degree> t => u"
   "Abs s => t"
 
 
@@ -105,9 +105,9 @@
   "cd" :: "dB => dB"
 recdef "cd" "measure size"
   "cd (Var n) = Var n"
-  "cd (Var n $ t) = Var n $ cd t"
-  "cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t"
-  "cd (Abs u $ t) = (cd u)[cd t/0]"
+  "cd (Var n \<degree> t) = Var n \<degree> cd t"
+  "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
+  "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
   "cd (Abs s) = Abs (cd s)"
 
 lemma par_beta_cd [rule_format]:
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