src/HOL/Nominal/Examples/SN.thy

 theory SN
-  imports Lam_Funs
+imports Lam_Funs
 begin
 
 text {* Strong Normalisation proof from the Proofs and Types book *}
 
 section {* Beta Reduction *}

 nominal_inductive typing
   by (simp_all add: abs_fresh fresh_ty)
 
 subsection {* a fact about beta *}
 
-constdefs
-  "NORMAL" :: "lam \<Rightarrow> bool"
+definition "NORMAL" :: "lam \<Rightarrow> bool" where
   "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"
 
 lemma NORMAL_Var:
   shows "NORMAL (Var a)"
 proof -

   "RED (TVar X) = {t. SN(t)}"
 | "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
 by (rule TrueI)+
 
 text {* neutral terms *}
-constdefs
-  NEUT :: "lam \<Rightarrow> bool"
+definition NEUT :: "lam \<Rightarrow> bool" where
   "NEUT t \<equiv> (\<exists>a. t = Var a) \<or> (\<exists>t1 t2. t = App t1 t2)" 
 
 (* a slight hack to get the first element of applications *)
 (* this is needed to get (SN t) from SN (App t s)         *) 
 inductive 

   then show "SN (fst_app (App t s))" by simp
 qed
 
 section {* Candidates *}
 
-constdefs
-  "CR1" :: "ty \<Rightarrow> bool"
+definition "CR1" :: "ty \<Rightarrow> bool" where
   "CR1 \<tau> \<equiv> \<forall>t. (t\<in>RED \<tau> \<longrightarrow> SN t)"
 
-  "CR2" :: "ty \<Rightarrow> bool"
+definition "CR2" :: "ty \<Rightarrow> bool" where
   "CR2 \<tau> \<equiv> \<forall>t t'. (t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>"
 
-  "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool"
+definition "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool" where
   "CR3_RED t \<tau> \<equiv> \<forall>t'. t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow>  t'\<in>RED \<tau>" 
 
-  "CR3" :: "ty \<Rightarrow> bool"
+definition "CR3" :: "ty \<Rightarrow> bool" where
   "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"
    
-  "CR4" :: "ty \<Rightarrow> bool"
+definition "CR4" :: "ty \<Rightarrow> bool" where
   "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
 
 lemma CR3_implies_CR4: 
   assumes a: "CR3 \<tau>" 
   shows "CR4 \<tau>"