src/HOL/Proofs/Lambda/WeakNorm.thy

 (*  Title:      HOL/Proofs/Lambda/WeakNorm.thy
     Author:     Stefan Berghofer
     Copyright   2003 TU Muenchen
 *)
 
-section {* Weak normalization for simply-typed lambda calculus *}
+section \<open>Weak normalization for simply-typed lambda calculus\<close>
 
 theory WeakNorm
 imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
   "~~/src/HOL/Library/Code_Target_Int"
 begin
 
-text {*
+text \<open>
 Formalization by Stefan Berghofer. Partly based on a paper proof by
 Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
-*}
-
-
-subsection {* Main theorems *}
+\<close>
+
+
+subsection \<open>Main theorems\<close>
 
 lemma norm_list:
   assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
   and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)"
   and uNF: "NF u" and uT: "e \<turnstile> u : T"

       qed
     next
       case (Abs r e1 T'1 u1 i1)
       assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
       then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
-      moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
+      moreover have "NF (lift u 0)" using \<open>NF u\<close> by (rule lift_NF)
       moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
       ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
       thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
         by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
     }
   qed
 qed
 
 
--- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
+\<comment> \<open>A computationally relevant copy of @{term "e \<turnstile> t : T"}\<close>
 inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   where
     Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
   | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
   | App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U"

   hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
   with unf show ?case by iprover
 qed
 
 
-subsection {* Extracting the program *}
+subsection \<open>Extracting the program\<close>
 
 declare NF.induct [ind_realizer]
 declare rtranclp.induct [ind_realizer irrelevant]
 declare rtyping.induct [ind_realizer]
 lemmas [extraction_expand] = conj_assoc listall_cons_eq

   apply (rule NF.intros)
   apply (simp add: listall_def)
   apply (erule NF.intros)
   done
 
-text_raw {*
+text_raw \<open>
 \begin{figure}
 \renewcommand{\isastyle}{\scriptsize\it}%
 @{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
 \renewcommand{\isastyle}{\small\it}%
-\caption{Program extracted from @{text subst_type_NF}}
+\caption{Program extracted from \<open>subst_type_NF\<close>}
 \label{fig:extr-subst-type-nf}
 \end{figure}
 
 \begin{figure}
 \renewcommand{\isastyle}{\scriptsize\it}%

 @{thm [display,eta_contract=false,margin=100] type_NF_def}
 \renewcommand{\isastyle}{\small\it}%
 \caption{Program extracted from lemmas and main theorem}
 \label{fig:extr-type-nf}
 \end{figure}
-*}
-
-text {*
+\<close>
+
+text \<open>
 The program corresponding to the proof of the central lemma, which
 performs substitution and normalization, is shown in Figure
 \ref{fig:extr-subst-type-nf}. The correctness
-theorem corresponding to the program @{text "subst_type_NF"} is
+theorem corresponding to the program \<open>subst_type_NF\<close> is
 @{thm [display,margin=100] subst_type_NF_correctness
   [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
-where @{text NFR} is the realizability predicate corresponding to
-the datatype @{text NFT}, which is inductively defined by the rules
+where \<open>NFR\<close> is the realizability predicate corresponding to
+the datatype \<open>NFT\<close>, which is inductively defined by the rules
 \pagebreak
 @{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}
 
-The programs corresponding to the main theorem @{text "type_NF"}, as
+The programs corresponding to the main theorem \<open>type_NF\<close>, as
 well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
-The correctness statement for the main function @{text "type_NF"} is
+The correctness statement for the main function \<open>type_NF\<close> is
 @{thm [display,margin=100] type_NF_correctness
   [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
-where the realizability predicate @{text "rtypingR"} corresponding to the
+where the realizability predicate \<open>rtypingR\<close> corresponding to the
 computationally relevant version of the typing judgement is inductively
 defined by the rules
 @{thm [display,margin=100] rtypingR.Var [no_vars]
   rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
-*}
-
-subsection {* Generating executable code *}
+\<close>
+
+subsection \<open>Generating executable code\<close>
 
 instantiation NFT :: default
 begin
 
 definition "default = Dummy ()"

 end
 
 definition int_of_nat :: "nat \<Rightarrow> int" where
   "int_of_nat = of_nat"
 
-text {*
+text \<open>
   The following functions convert between Isabelle's built-in {\tt term}
   datatype and the generated {\tt dB} datatype. This allows to
   generate example terms using Isabelle's parser and inspect
   normalized terms using Isabelle's pretty printer.
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 val nat_of_integer = @{code nat} o @{code int_of_integer};
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
   | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of

 val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
 
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
 val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
 val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
-*}
-
-end
+\<close>
+
+end