src/HOL/ex/Abstract_NAT.thy

 
 
 text {* \medskip The recursion operator -- polymorphic! *}
 
 definition
-  rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
+  rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a" where
   "rec e r x = (THE y. Rec e r x y)"
 
 lemma rec_eval:
   assumes Rec: "Rec e r x y"
   shows "rec e r x = y"

 
 
 text {* \medskip Example: addition (monomorphic) *}
 
 definition
-  add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
+  add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" where
   "add m n = rec n (\<lambda>_ k. succ k) m"
 
 lemma add_zero [simp]: "add zero n = n"
   and add_succ [simp]: "add (succ m) n = succ (add m n)"
   unfolding add_def by simp_all

 
 
 text {* \medskip Example: replication (polymorphic) *}
 
 definition
-  repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
+  repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" where
   "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
 
 lemma repl_zero [simp]: "repl zero x = []"
   and repl_succ [simp]: "repl (succ n) x = x # repl n x"
   unfolding repl_def by simp_all