tuned notation (degree instead of dollar);
authorwenzelm
Wed Oct 31 22:05:37 2001 +0100 (2001-10-31)
changeset 120111a3a7b3cd9bb
parent 12010 e1d4df962ac9
child 12012 1d534baa2827
tuned notation (degree instead of dollar);
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/Type.thy
     1.1 --- a/src/HOL/Lambda/Eta.thy	Wed Oct 31 22:04:29 2001 +0100
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Wed Oct 31 22:05:37 2001 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    free :: "dB => nat => bool"
     1.5  primrec
     1.6    "free (Var j) i = (j = i)"
     1.7 -  "free (s $ t) i = (free s i \<or> free t i)"
     1.8 +  "free (s \<degree> t) i = (free s i \<or> free t i)"
     1.9    "free (Abs s) i = free s (i + 1)"
    1.10  
    1.11  consts
    1.12 @@ -32,14 +32,14 @@
    1.13  
    1.14  inductive eta
    1.15    intros
    1.16 -    eta [simp, intro]: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
    1.17 -    appL [simp, intro]: "s -e> t ==> s $ u -e> t $ u"
    1.18 -    appR [simp, intro]: "s -e> t ==> u $ s -e> u $ t"
    1.19 +    eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) -e> s[dummy/0]"
    1.20 +    appL [simp, intro]: "s -e> t ==> s \<degree> u -e> t \<degree> u"
    1.21 +    appR [simp, intro]: "s -e> t ==> u \<degree> s -e> u \<degree> t"
    1.22      abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"
    1.23  
    1.24  inductive_cases eta_cases [elim!]:
    1.25    "Abs s -e> z"
    1.26 -  "s $ t -e> u"
    1.27 +  "s \<degree> t -e> u"
    1.28    "Var i -e> t"
    1.29  
    1.30  
    1.31 @@ -118,18 +118,18 @@
    1.32     apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    1.33    done
    1.34  
    1.35 -lemma rtrancl_eta_AppL: "s -e>> s' ==> s $ t -e>> s' $ t"
    1.36 +lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
    1.37    apply (erule rtrancl_induct)
    1.38     apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    1.39    done
    1.40  
    1.41 -lemma rtrancl_eta_AppR: "t -e>> t' ==> s $ t -e>> s $ t'"
    1.42 +lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
    1.43    apply (erule rtrancl_induct)
    1.44     apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
    1.45    done
    1.46  
    1.47  lemma rtrancl_eta_App:
    1.48 -    "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"
    1.49 +    "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
    1.50    apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
    1.51    done
    1.52  
    1.53 @@ -189,7 +189,7 @@
    1.54  
    1.55  subsection "Implicit definition of eta"
    1.56  
    1.57 -text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
    1.58 +text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
    1.59  
    1.60  lemma not_free_iff_lifted [rule_format]:
    1.61      "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
    1.62 @@ -218,7 +218,7 @@
    1.63     apply (rule iffI)
    1.64      apply (elim conjE exE)
    1.65      apply (rename_tac u1 u2)
    1.66 -    apply (rule_tac x = "u1 $ u2" in exI)
    1.67 +    apply (rule_tac x = "u1 \<degree> u2" in exI)
    1.68      apply simp
    1.69     apply (erule exE)
    1.70     apply (erule rev_mp)
    1.71 @@ -244,8 +244,8 @@
    1.72    done
    1.73  
    1.74  theorem explicit_is_implicit:
    1.75 -  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) =
    1.76 -    (\<forall>s. R (Abs (lift s 0 $ Var 0)) s)"
    1.77 +  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
    1.78 +    (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
    1.79    apply (auto simp add: not_free_iff_lifted)
    1.80    done
    1.81  
     2.1 --- a/src/HOL/Lambda/InductTermi.thy	Wed Oct 31 22:04:29 2001 +0100
     2.2 +++ b/src/HOL/Lambda/InductTermi.thy	Wed Oct 31 22:05:37 2001 +0100
     2.3 @@ -19,16 +19,16 @@
     2.4  
     2.5  inductive IT
     2.6    intros
     2.7 -    Var [intro]: "rs : lists IT ==> Var n $$ rs : IT"
     2.8 +    Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT"
     2.9      Lambda [intro]: "r : IT ==> Abs r : IT"
    2.10 -    Beta [intro]: "(r[s/0]) $$ ss : IT ==> s : IT ==> (Abs r $ s) $$ ss : IT"
    2.11 +    Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> ss : IT"
    2.12  
    2.13  
    2.14  subsection {* Every term in IT terminates *}
    2.15  
    2.16  lemma double_induction_lemma [rule_format]:
    2.17    "s : termi beta ==> \<forall>t. t : termi beta -->
    2.18 -    (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
    2.19 +    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)"
    2.20    apply (erule acc_induct)
    2.21    apply (erule thin_rl)
    2.22    apply (rule allI)
    2.23 @@ -65,19 +65,19 @@
    2.24  
    2.25  declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
    2.26  
    2.27 -lemma [simp, THEN not_sym, simp]: "Var n $$ ss \<noteq> Abs r $ s $$ ts"
    2.28 +lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
    2.29    apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    2.30    done
    2.31  
    2.32  lemma [simp]:
    2.33 -  "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \<and> s = s' \<and> ss = ss')"
    2.34 +  "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
    2.35    apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    2.36    done
    2.37  
    2.38  inductive_cases [elim!]:
    2.39 -  "Var n $$ ss : IT"
    2.40 +  "Var n \<degree>\<degree> ss : IT"
    2.41    "Abs t : IT"
    2.42 -  "Abs r $ s $$ ts : IT"
    2.43 +  "Abs r \<degree> s \<degree>\<degree> ts : IT"
    2.44  
    2.45  theorem termi_implies_IT: "r : termi beta ==> r : IT"
    2.46    apply (erule acc_induct)
    2.47 @@ -96,7 +96,7 @@
    2.48     apply (drule ex_step1I, assumption)
    2.49     apply clarify
    2.50     apply (rename_tac us)
    2.51 -   apply (erule_tac x = "Var n $$ us" in allE)
    2.52 +   apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
    2.53     apply force
    2.54     apply (rename_tac u ts)
    2.55     apply (case_tac ts)
    2.56 @@ -110,7 +110,7 @@
    2.57     apply (erule mp)
    2.58     apply clarify
    2.59     apply (rename_tac t)
    2.60 -   apply (erule_tac x = "Abs u $ t $$ ss" in allE)
    2.61 +   apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE)
    2.62     apply force
    2.63     done
    2.64  
     3.1 --- a/src/HOL/Lambda/Lambda.thy	Wed Oct 31 22:04:29 2001 +0100
     3.2 +++ b/src/HOL/Lambda/Lambda.thy	Wed Oct 31 22:05:37 2001 +0100
     3.3 @@ -13,25 +13,22 @@
     3.4  
     3.5  datatype dB =
     3.6      Var nat
     3.7 -  | App dB dB (infixl "$" 200)
     3.8 +  | App dB dB (infixl "\<degree>" 200)
     3.9    | Abs dB
    3.10  
    3.11 -syntax (symbols)
    3.12 -  App :: "dB => dB => dB"    (infixl "\<^sub>\<degree>" 200)
    3.13 -
    3.14  consts
    3.15    subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
    3.16    lift :: "[dB, nat] => dB"
    3.17  
    3.18  primrec
    3.19    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
    3.20 -  "lift (s $ t) k = lift s k $ lift t k"
    3.21 +  "lift (s \<degree> t) k = lift s k \<degree> lift t k"
    3.22    "lift (Abs s) k = Abs (lift s (k + 1))"
    3.23  
    3.24  primrec  (* FIXME base names *)
    3.25    subst_Var: "(Var i)[s/k] =
    3.26      (if k < i then Var (i - 1) else if i = k then s else Var i)"
    3.27 -  subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]"
    3.28 +  subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
    3.29    subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
    3.30  
    3.31  declare subst_Var [simp del]
    3.32 @@ -44,13 +41,13 @@
    3.33  
    3.34  primrec
    3.35    "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
    3.36 -  "liftn n (s $ t) k = liftn n s k $ liftn n t k"
    3.37 +  "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
    3.38    "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
    3.39  
    3.40  primrec
    3.41    "substn (Var i) s k =
    3.42      (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
    3.43 -  "substn (t $ u) s k = substn t s k $ substn u s k"
    3.44 +  "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
    3.45    "substn (Abs t) s k = Abs (substn t s (k + 1))"
    3.46  
    3.47  
    3.48 @@ -68,15 +65,15 @@
    3.49  
    3.50  inductive beta
    3.51    intros
    3.52 -    beta [simp, intro!]: "Abs s $ t -> s[t/0]"
    3.53 -    appL [simp, intro!]: "s -> t ==> s $ u -> t $ u"
    3.54 -    appR [simp, intro!]: "s -> t ==> u $ s -> u $ t"
    3.55 +    beta [simp, intro!]: "Abs s \<degree> t -> s[t/0]"
    3.56 +    appL [simp, intro!]: "s -> t ==> s \<degree> u -> t \<degree> u"
    3.57 +    appR [simp, intro!]: "s -> t ==> u \<degree> s -> u \<degree> t"
    3.58      abs [simp, intro!]: "s -> t ==> Abs s -> Abs t"
    3.59  
    3.60  inductive_cases beta_cases [elim!]:
    3.61    "Var i -> t"
    3.62    "Abs r -> s"
    3.63 -  "s $ t -> u"
    3.64 +  "s \<degree> t -> u"
    3.65  
    3.66  declare if_not_P [simp] not_less_eq [simp]
    3.67    -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
    3.68 @@ -91,19 +88,19 @@
    3.69    done
    3.70  
    3.71  lemma rtrancl_beta_AppL:
    3.72 -    "s ->> s' ==> s $ t ->> s' $ t"
    3.73 +    "s ->> s' ==> s \<degree> t ->> s' \<degree> t"
    3.74    apply (erule rtrancl_induct)
    3.75     apply (blast intro: rtrancl_into_rtrancl)+
    3.76    done
    3.77  
    3.78  lemma rtrancl_beta_AppR:
    3.79 -    "t ->> t' ==> s $ t ->> s $ t'"
    3.80 +    "t ->> t' ==> s \<degree> t ->> s \<degree> t'"
    3.81    apply (erule rtrancl_induct)
    3.82     apply (blast intro: rtrancl_into_rtrancl)+
    3.83    done
    3.84  
    3.85  lemma rtrancl_beta_App [intro]:
    3.86 -    "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'"
    3.87 +    "[| s ->> s'; t ->> t' |] ==> s \<degree> t ->> s' \<degree> t'"
    3.88    apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
    3.89      intro: rtrancl_trans)
    3.90    done
     4.1 --- a/src/HOL/Lambda/ListApplication.thy	Wed Oct 31 22:04:29 2001 +0100
     4.2 +++ b/src/HOL/Lambda/ListApplication.thy	Wed Oct 31 22:05:37 2001 +0100
     4.3 @@ -9,26 +9,23 @@
     4.4  theory ListApplication = Lambda:
     4.5  
     4.6  syntax
     4.7 -  "_list_application" :: "dB => dB list => dB"    (infixl "$$" 150)
     4.8 -syntax (symbols)
     4.9 -  "_list_application" :: "dB => dB list => dB"    (infixl "\<^sub>\<degree>\<^sub>\<degree>" 150)
    4.10 +  "_list_application" :: "dB => dB list => dB"    (infixl "\<degree>\<degree>" 150)
    4.11 +translations
    4.12 +  "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
    4.13  
    4.14 -translations
    4.15 -  "t $$ ts" == "foldl (op $) t ts"
    4.16 -
    4.17 -lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
    4.18 +lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
    4.19    apply (induct_tac ts rule: rev_induct)
    4.20     apply auto
    4.21    done
    4.22  
    4.23  lemma Var_eq_apps_conv [rule_format, iff]:
    4.24 -    "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
    4.25 +    "\<forall>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
    4.26    apply (induct_tac ss)
    4.27     apply auto
    4.28    done
    4.29  
    4.30  lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
    4.31 -    "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
    4.32 +    "\<forall>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
    4.33    apply (induct_tac rs rule: rev_induct)
    4.34     apply simp
    4.35     apply blast
    4.36 @@ -38,26 +35,26 @@
    4.37    done
    4.38  
    4.39  lemma App_eq_foldl_conv:
    4.40 -  "(r $ s = t $$ ts) =
    4.41 -    (if ts = [] then r $ s = t
    4.42 -    else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
    4.43 +  "(r \<degree> s = t \<degree>\<degree> ts) =
    4.44 +    (if ts = [] then r \<degree> s = t
    4.45 +    else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
    4.46    apply (rule_tac xs = ts in rev_exhaust)
    4.47     apply auto
    4.48    done
    4.49  
    4.50  lemma Abs_eq_apps_conv [iff]:
    4.51 -    "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
    4.52 +    "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
    4.53    apply (induct_tac ss rule: rev_induct)
    4.54     apply auto
    4.55    done
    4.56  
    4.57 -lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
    4.58 +lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
    4.59    apply (induct_tac ss rule: rev_induct)
    4.60     apply auto
    4.61    done
    4.62  
    4.63  lemma Abs_apps_eq_Abs_apps_conv [iff]:
    4.64 -    "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
    4.65 +    "\<forall>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
    4.66    apply (induct_tac rs rule: rev_induct)
    4.67     apply simp
    4.68     apply blast
    4.69 @@ -67,13 +64,13 @@
    4.70    done
    4.71  
    4.72  lemma Abs_App_neq_Var_apps [iff]:
    4.73 -    "\<forall>s t. Abs s $ t ~= Var n $$ ss"
    4.74 +    "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
    4.75    apply (induct_tac ss rule: rev_induct)
    4.76     apply auto
    4.77    done
    4.78  
    4.79  lemma Var_apps_neq_Abs_apps [rule_format, iff]:
    4.80 -    "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
    4.81 +    "\<forall>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
    4.82    apply (induct_tac ss rule: rev_induct)
    4.83     apply simp
    4.84    apply (rule allI)
    4.85 @@ -82,19 +79,19 @@
    4.86    done
    4.87  
    4.88  lemma ex_head_tail:
    4.89 -  "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
    4.90 +  "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
    4.91    apply (induct_tac t)
    4.92      apply (rule_tac x = "[]" in exI)
    4.93      apply simp
    4.94     apply clarify
    4.95     apply (rename_tac ts1 ts2 h1 h2)
    4.96 -   apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
    4.97 +   apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI)
    4.98     apply simp
    4.99    apply simp
   4.100    done
   4.101  
   4.102  lemma size_apps [simp]:
   4.103 -  "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
   4.104 +  "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
   4.105    apply (induct_tac rs rule: rev_induct)
   4.106     apply auto
   4.107    done
   4.108 @@ -104,11 +101,11 @@
   4.109    done
   4.110  
   4.111  
   4.112 -text {* \medskip A customized induction schema for @{text "$$"}. *}
   4.113 +text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
   4.114  
   4.115  lemma lem [rule_format (no_asm)]:
   4.116 -  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   4.117 -    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   4.118 +  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
   4.119 +    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
   4.120    |] ==> \<forall>t. size t = n --> P t"
   4.121  proof -
   4.122    case rule_context
   4.123 @@ -149,8 +146,8 @@
   4.124  qed
   4.125  
   4.126  theorem Apps_dB_induct:
   4.127 -  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   4.128 -    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   4.129 +  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
   4.130 +    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
   4.131    |] ==> P t"
   4.132  proof -
   4.133    case rule_context
     5.1 --- a/src/HOL/Lambda/ListBeta.thy	Wed Oct 31 22:04:29 2001 +0100
     5.2 +++ b/src/HOL/Lambda/ListBeta.thy	Wed Oct 31 22:05:37 2001 +0100
     5.3 @@ -18,7 +18,7 @@
     5.4    "rs => ss" == "(rs, ss) : step1 beta"
     5.5  
     5.6  lemma head_Var_reduction_aux:
     5.7 -  "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
     5.8 +  "v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)"
     5.9    apply (erule beta.induct)
    5.10       apply simp
    5.11      apply (rule allI)
    5.12 @@ -32,16 +32,16 @@
    5.13    done
    5.14  
    5.15  lemma head_Var_reduction:
    5.16 -  "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
    5.17 +  "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
    5.18    apply (drule head_Var_reduction_aux)
    5.19    apply blast
    5.20    done
    5.21  
    5.22  lemma apps_betasE_aux:
    5.23 -  "u -> u' ==> \<forall>r rs. u = r $$ rs -->
    5.24 -    ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
    5.25 -     (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
    5.26 -     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
    5.27 +  "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
    5.28 +    ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
    5.29 +     (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
    5.30 +     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
    5.31    apply (erule beta.induct)
    5.32       apply (clarify del: disjCI)
    5.33       apply (case_tac r)
    5.34 @@ -70,12 +70,12 @@
    5.35    done
    5.36  
    5.37  lemma apps_betasE [elim!]:
    5.38 -  "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
    5.39 -    !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
    5.40 -    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
    5.41 +  "[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R;
    5.42 +    !!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R;
    5.43 +    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |]
    5.44    ==> R"
    5.45  proof -
    5.46 -  assume major: "r $$ rs -> s"
    5.47 +  assume major: "r \<degree>\<degree> rs -> s"
    5.48    case rule_context
    5.49    show ?thesis
    5.50      apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
    5.51 @@ -84,20 +84,20 @@
    5.52  qed
    5.53  
    5.54  lemma apps_preserves_beta [simp]:
    5.55 -    "r -> s ==> r $$ ss -> s $$ ss"
    5.56 +    "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
    5.57    apply (induct_tac ss rule: rev_induct)
    5.58    apply auto
    5.59    done
    5.60  
    5.61  lemma apps_preserves_beta2 [simp]:
    5.62 -    "r ->> s ==> r $$ ss ->> s $$ ss"
    5.63 +    "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
    5.64    apply (erule rtrancl_induct)
    5.65     apply blast
    5.66    apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
    5.67    done
    5.68  
    5.69  lemma apps_preserves_betas [rule_format, simp]:
    5.70 -    "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
    5.71 +    "\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
    5.72    apply (induct_tac rs rule: rev_induct)
    5.73     apply simp
    5.74    apply simp
     6.1 --- a/src/HOL/Lambda/ParRed.thy	Wed Oct 31 22:04:29 2001 +0100
     6.2 +++ b/src/HOL/Lambda/ParRed.thy	Wed Oct 31 22:05:37 2001 +0100
     6.3 @@ -26,14 +26,14 @@
     6.4    intros
     6.5      var [simp, intro!]: "Var n => Var n"
     6.6      abs [simp, intro!]: "s => t ==> Abs s => Abs t"
     6.7 -    app [simp, intro!]: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
     6.8 -    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
     6.9 +    app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
    6.10 +    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
    6.11  
    6.12  inductive_cases par_beta_cases [elim!]:
    6.13    "Var n => t"
    6.14    "Abs s => Abs t"
    6.15 -  "(Abs s) $ t => u"
    6.16 -  "s $ t => u"
    6.17 +  "(Abs s) \<degree> t => u"
    6.18 +  "s \<degree> t => u"
    6.19    "Abs s => t"
    6.20  
    6.21  
    6.22 @@ -105,9 +105,9 @@
    6.23    "cd" :: "dB => dB"
    6.24  recdef "cd" "measure size"
    6.25    "cd (Var n) = Var n"
    6.26 -  "cd (Var n $ t) = Var n $ cd t"
    6.27 -  "cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t"
    6.28 -  "cd (Abs u $ t) = (cd u)[cd t/0]"
    6.29 +  "cd (Var n \<degree> t) = Var n \<degree> cd t"
    6.30 +  "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
    6.31 +  "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
    6.32    "cd (Abs s) = Abs (cd s)"
    6.33  
    6.34  lemma par_beta_cd [rule_format]:
     7.1 --- a/src/HOL/Lambda/Type.thy	Wed Oct 31 22:04:29 2001 +0100
     7.2 +++ b/src/HOL/Lambda/Type.thy	Wed Oct 31 22:05:37 2001 +0100
     7.3 @@ -18,8 +18,10 @@
     7.4  subsection {* Environments *}
     7.5  
     7.6  constdefs
     7.7 +  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
     7.8 +  "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
     7.9 +syntax (symbols)
    7.10    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    7.11 -  "e\<langle>i:a\<rangle> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
    7.12  
    7.13  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
    7.14    by (simp add: shift_def)
    7.15 @@ -69,11 +71,11 @@
    7.16    intros
    7.17      Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
    7.18      Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
    7.19 -    App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<^sub>\<degree> t) : U"
    7.20 +    App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
    7.21  
    7.22  inductive_cases typing_elims [elim!]:
    7.23    "e \<turnstile> Var i : T"
    7.24 -  "e \<turnstile> t \<^sub>\<degree> u : T"
    7.25 +  "e \<turnstile> t \<degree> u : T"
    7.26    "e \<turnstile> Abs t : T"
    7.27  
    7.28  primrec
    7.29 @@ -86,44 +88,44 @@
    7.30  
    7.31  subsection {* Some examples *}
    7.32  
    7.33 -lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<^sub>\<degree> (Var 2 \<^sub>\<degree> Var 1 \<^sub>\<degree> Var 0)))) : ?T"
    7.34 +lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
    7.35    by force
    7.36  
    7.37 -lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<^sub>\<degree> Var 0 \<^sub>\<degree> (Var 1 \<^sub>\<degree> Var 0)))) : ?T"
    7.38 +lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
    7.39    by force
    7.40  
    7.41  
    7.42  subsection {* n-ary function types *}
    7.43  
    7.44  lemma list_app_typeD:
    7.45 -    "\<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"
    7.46 +    "\<And>t T. e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
    7.47    apply (induct ts)
    7.48     apply simp
    7.49    apply atomize
    7.50    apply simp
    7.51 -  apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
    7.52 +  apply (erule_tac x = "t \<degree> a" in allE)
    7.53    apply (erule_tac x = T in allE)
    7.54    apply (erule impE)
    7.55     apply assumption
    7.56    apply (elim exE conjE)
    7.57 -  apply (ind_cases "e \<turnstile> t \<^sub>\<degree> u : T")
    7.58 +  apply (ind_cases "e \<turnstile> t \<degree> u : T")
    7.59    apply (rule_tac x = "Ta # Ts" in exI)
    7.60    apply simp
    7.61    done
    7.62  
    7.63  lemma list_app_typeE:
    7.64 -  "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"
    7.65 +  "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"
    7.66    by (insert list_app_typeD) fast
    7.67  
    7.68  lemma list_app_typeI:
    7.69 -    "\<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"
    7.70 +    "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
    7.71    apply (induct ts)
    7.72     apply simp
    7.73    apply atomize
    7.74    apply (case_tac Ts)
    7.75     apply simp
    7.76    apply simp
    7.77 -  apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
    7.78 +  apply (erule_tac x = "t \<degree> a" in allE)
    7.79    apply (erule_tac x = T in allE)
    7.80    apply (erule_tac x = lista in allE)
    7.81    apply (erule impE)
    7.82 @@ -152,11 +154,11 @@
    7.83  subsection {* Lifting preserves termination and well-typedness *}
    7.84  
    7.85  lemma lift_map [simp]:
    7.86 -    "\<And>t. lift (t \<^sub>\<degree>\<^sub>\<degree> ts) i = lift t i \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t i) ts"
    7.87 +    "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
    7.88    by (induct ts) simp_all
    7.89  
    7.90  lemma subst_map [simp]:
    7.91 -    "\<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"
    7.92 +    "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
    7.93    by (induct ts) simp_all
    7.94  
    7.95  lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> (\<And>i. lift t i \<in> IT)"
    7.96 @@ -206,39 +208,19 @@
    7.97    apply blast
    7.98    done
    7.99  
   7.100 -lemma substs_lemma [rule_format]:
   7.101 -  "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<longrightarrow>
   7.102 +lemma substs_lemma:
   7.103 +  "\<And>Ts. e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
   7.104       e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
   7.105 -  apply (induct_tac ts)
   7.106 -   apply (intro strip)
   7.107 +  apply (induct ts)
   7.108     apply (case_tac Ts)
   7.109      apply simp
   7.110     apply simp
   7.111 -  apply (intro strip)
   7.112 +  apply atomize
   7.113    apply (case_tac Ts)
   7.114     apply simp
   7.115    apply simp
   7.116    apply (erule conjE)
   7.117 -  apply (erule subst_lemma)
   7.118 -   apply assumption
   7.119 -  apply (rule refl)
   7.120 -  done
   7.121 -
   7.122 -lemma substs_lemma [rule_format]:
   7.123 -  "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<longrightarrow>
   7.124 -     e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
   7.125 -  apply (induct_tac ts)
   7.126 -   apply (intro strip)
   7.127 -   apply (case_tac Ts)
   7.128 -    apply simp
   7.129 -   apply simp
   7.130 -  apply (intro strip)
   7.131 -  apply (case_tac Ts)
   7.132 -   apply simp
   7.133 -  apply simp
   7.134 -  apply (erule conjE)
   7.135 -  apply (erule subst_lemma)
   7.136 -   apply assumption
   7.137 +  apply (erule (1) subst_lemma)
   7.138    apply (rule refl)
   7.139    done
   7.140  
   7.141 @@ -250,7 +232,7 @@
   7.142      apply blast
   7.143     apply blast
   7.144    apply atomize
   7.145 -  apply (ind_cases "s \<^sub>\<degree> t -> t'")
   7.146 +  apply (ind_cases "s \<degree> t -> t'")
   7.147      apply hypsubst
   7.148      apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
   7.149      apply (rule subst_lemma)
   7.150 @@ -264,13 +246,12 @@
   7.151  
   7.152  subsection {* Additional lemmas *}
   7.153  
   7.154 -lemma app_last: "(t \<^sub>\<degree>\<^sub>\<degree> ts) \<^sub>\<degree> u = t \<^sub>\<degree>\<^sub>\<degree> (ts @ [u])"
   7.155 +lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
   7.156    by simp
   7.157  
   7.158  lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> (\<And>i j. r[Var i/j] \<in> IT)"
   7.159    apply (induct set: IT)
   7.160      txt {* Case @{term Var}: *}
   7.161 -    apply atomize
   7.162      apply (simp (no_asm) add: subst_Var)
   7.163      apply
   7.164      ((rule conjI impI)+,
   7.165 @@ -297,13 +278,13 @@
   7.166    done
   7.167  
   7.168  lemma Var_IT: "Var n \<in> IT"
   7.169 -  apply (subgoal_tac "Var n \<^sub>\<degree>\<^sub>\<degree> [] \<in> IT")
   7.170 +  apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
   7.171     apply simp
   7.172    apply (rule IT.Var)
   7.173    apply (rule lists.Nil)
   7.174    done
   7.175  
   7.176 -lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<^sub>\<degree> Var i \<in> IT"
   7.177 +lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
   7.178    apply (induct set: IT)
   7.179      apply (subst app_last)
   7.180      apply (rule IT.Var)
   7.181 @@ -355,11 +336,11 @@
   7.182      assume uT: "e \<turnstile> u : T"
   7.183      {
   7.184        case (Var n rs)
   7.185 -      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree>\<^sub>\<degree> rs : T'"
   7.186 +      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
   7.187        let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
   7.188        let ?R = "\<lambda>t. \<forall>e T' u i.
   7.189          e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
   7.190 -      show "(Var n \<^sub>\<degree>\<^sub>\<degree> rs)[u/i] \<in> IT"
   7.191 +      show "(Var n \<degree>\<degree> rs)[u/i] \<in> IT"
   7.192        proof (cases "n = i")
   7.193          case True
   7.194          show ?thesis
   7.195 @@ -368,9 +349,9 @@
   7.196            with uIT True show ?thesis by simp
   7.197          next
   7.198            case (Cons a as)
   7.199 -          with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'" by simp
   7.200 +          with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp
   7.201            then obtain Ts
   7.202 -              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a : Ts \<Rrightarrow> T'"
   7.203 +              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'"
   7.204                and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
   7.205              by (rule list_app_typeE)
   7.206            from headT obtain T''
   7.207 @@ -380,14 +361,14 @@
   7.208            from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
   7.209              by cases auto
   7.210            with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
   7.211 -          from T have "(Var 0 \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t 0)
   7.212 -            (map (\<lambda>t. t[u/i]) as))[(u \<^sub>\<degree> a[u/i])/0] \<in> IT"
   7.213 +          from T have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
   7.214 +            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0] \<in> IT"
   7.215            proof (rule MI2)
   7.216 -            from T have "(lift u 0 \<^sub>\<degree> Var 0)[a[u/i]/0] \<in> IT"
   7.217 +            from T have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<in> IT"
   7.218              proof (rule MI1)
   7.219                have "lift u 0 \<in> IT" by (rule lift_IT)
   7.220 -              thus "lift u 0 \<^sub>\<degree> Var 0 \<in> IT" by (rule app_Var_IT)
   7.221 -              show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<^sub>\<degree> Var 0 : Ts \<Rrightarrow> T'"
   7.222 +              thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
   7.223 +              show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
   7.224                proof (rule typing.App)
   7.225                  show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
   7.226                    by (rule lift_type) (rule uT')
   7.227 @@ -399,7 +380,7 @@
   7.228                from argT uT show "e \<turnstile> a[u/i] : T''"
   7.229                  by (rule subst_lemma) simp
   7.230              qed
   7.231 -            thus "u \<^sub>\<degree> a[u/i] \<in> IT" by simp
   7.232 +            thus "u \<degree> a[u/i] \<in> IT" by simp
   7.233              from Var have "as \<in> lists {t. ?R t}"
   7.234                by cases (simp_all add: Cons)
   7.235              moreover from argsT have "as \<in> lists ?ty"
   7.236 @@ -421,18 +402,18 @@
   7.237                  by (rule lists.Cons) (rule Cons)
   7.238                thus ?case by simp
   7.239              qed
   7.240 -            thus "Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as \<in> IT" by (rule IT.Var)
   7.241 +            thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
   7.242              have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
   7.243                by (rule typing.Var) simp
   7.244              moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
   7.245                by (rule substs_lemma)
   7.246              hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
   7.247                by (rule lift_typings)
   7.248 -            ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as : T'"
   7.249 +            ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> ?ls as : T'"
   7.250                by (rule list_app_typeI)
   7.251              from argT uT have "e \<turnstile> a[u/i] : T''"
   7.252                by (rule subst_lemma) (rule refl)
   7.253 -            with uT' show "e \<turnstile> u \<^sub>\<degree> a[u/i] : Ts \<Rrightarrow> T'"
   7.254 +            with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'"
   7.255                by (rule typing.App)
   7.256            qed
   7.257            with Cons True show ?thesis
   7.258 @@ -469,25 +450,25 @@
   7.259          by fastsimp
   7.260      next
   7.261        case (Beta r a as)
   7.262 -      assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'"
   7.263 -      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<^sub>\<degree>\<^sub>\<degree> as) e T' u i T"
   7.264 +      assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
   7.265 +      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
   7.266        assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
   7.267 -      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"
   7.268 +      have "Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
   7.269        proof (rule IT.Beta)
   7.270 -        have "Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as -> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as"
   7.271 +        have "Abs r \<degree> a \<degree>\<degree> as -> r[a/0] \<degree>\<degree> as"
   7.272            by (rule apps_preserves_beta) (rule beta.beta)
   7.273 -        with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as : T'"
   7.274 +        with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
   7.275            by (rule subject_reduction)
   7.276 -        hence "(r[a/0] \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT"
   7.277 +        hence "(r[a/0] \<degree>\<degree> as)[u/i] \<in> IT"
   7.278            by (rule SI1)
   7.279 -        thus "r[lift u 0/Suc i][a[u/i]/0] \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
   7.280 +        thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
   7.281            by (simp del: subst_map add: subst_subst subst_map [symmetric])
   7.282 -        from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a : U"
   7.283 +        from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
   7.284            by (rule list_app_typeE) fast
   7.285          then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
   7.286          thus "a[u/i] \<in> IT" by (rule SI2)
   7.287        qed
   7.288 -      thus "(Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT" by simp
   7.289 +      thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
   7.290      }
   7.291    qed
   7.292  qed
   7.293 @@ -506,18 +487,18 @@
   7.294      show ?case by (rule IT.Lambda)
   7.295    next
   7.296      case (App T U e s t)
   7.297 -    have "(Var 0 \<^sub>\<degree> lift t 0)[s/0] \<in> IT"
   7.298 +    have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
   7.299      proof (rule subst_type_IT)
   7.300        have "lift t 0 \<in> IT" by (rule lift_IT)
   7.301        hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
   7.302 -      hence "Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
   7.303 -      also have "Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0] = Var 0 \<^sub>\<degree> lift t 0" by simp
   7.304 +      hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
   7.305 +      also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
   7.306        finally show "\<dots> \<in> IT" .
   7.307        have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
   7.308          by (rule typing.Var) simp
   7.309        moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
   7.310          by (rule lift_type)
   7.311 -      ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<^sub>\<degree> lift t 0 : U"
   7.312 +      ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
   7.313          by (rule typing.App)
   7.314      qed
   7.315      thus ?case by simp