src/HOL/Proofs/Lambda/Lambda.thy

 (*  Title:      HOL/Proofs/Lambda/Lambda.thy
     Author:     Tobias Nipkow
     Copyright   1995 TU Muenchen
 *)
 
-section {* Basic definitions of Lambda-calculus *}
+section \<open>Basic definitions of Lambda-calculus\<close>
 
 theory Lambda
 imports Main
 begin
 
 declare [[syntax_ambiguity_warning = false]]
 
 
-subsection {* Lambda-terms in de Bruijn notation and substitution *}
+subsection \<open>Lambda-terms in de Bruijn notation and substitution\<close>
 
 datatype dB =
     Var nat
   | App dB dB (infixl "\<degree>" 200)
   | Abs dB

   | 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]
 
-text {* Optimized versions of @{term subst} and @{term lift}. *}
+text \<open>Optimized versions of @{term subst} and @{term lift}.\<close>
 
 primrec
   liftn :: "[nat, dB, nat] => dB"
 where
     "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"

       (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
   | "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))"
 
 
-subsection {* Beta-reduction *}
+subsection \<open>Beta-reduction\<close>
 
 inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
   where
     beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
   | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"

   "Var i \<rightarrow>\<^sub>\<beta> t"
   "Abs r \<rightarrow>\<^sub>\<beta> s"
   "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
 
 declare if_not_P [simp] not_less_eq [simp]
-  -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
+  \<comment> \<open>don't add \<open>r_into_rtrancl[intro!]\<close>\<close>
 
 
-subsection {* Congruence rules *}
+subsection \<open>Congruence rules\<close>
 
 lemma rtrancl_beta_Abs [intro!]:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 

 lemma rtrancl_beta_App [intro]:
     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
   by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
 
 
-subsection {* Substitution-lemmas *}
+subsection \<open>Substitution-lemmas\<close>
 
 lemma subst_eq [simp]: "(Var k)[u/k] = u"
   by (simp add: subst_Var)
 
 lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"

   by (induct t arbitrary: i j u v)
     (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
       split: nat.split)
 
 
-subsection {* Equivalence proof for optimized substitution *}
+subsection \<open>Equivalence proof for optimized substitution\<close>
 
 lemma liftn_0 [simp]: "liftn 0 t k = t"
   by (induct t arbitrary: k) (simp_all add: subst_Var)
 
 lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"

 
 theorem substn_subst_0: "substn t s 0 = t[s/0]"
   by simp
 
 
-subsection {* Preservation theorems *}
+subsection \<open>Preservation theorems\<close>
 
-text {* Not used in Church-Rosser proof, but in Strong
-  Normalization. \medskip *}
+text \<open>Not used in Church-Rosser proof, but in Strong
+  Normalization. \medskip\<close>
 
 theorem subst_preserves_beta [simp]:
     "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
   by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])