doc-src/IsarAdvanced/Codegen/Thy/Program.thy

   Coming back to our introductory example, we
   could provide an alternative defining equations for @{const dequeue}
   explicitly:
 *}
 
-lemma %quoteme [code func]:
+lemma %quoteme [code]:
   "dequeue (Queue xs []) =
      (if xs = [] then (None, Queue [] [])
        else dequeue (Queue [] (rev xs)))"
   "dequeue (Queue xs (y # ys)) =
      (Some y, Queue xs ys)"
   by (cases xs, simp_all) (cases "rev xs", simp_all)
 
 text {*
-  \noindent The annotation @{text "[code func]"} is an @{text Isar}
+  \noindent The annotation @{text "[code]"} is an @{text Isar}
   @{text attribute} which states that the given theorems should be
   considered as defining equations for a @{text fun} statement --
   the corresponding constant is determined syntactically.  The resulting code:
 *}
 

 text {*
   \noindent Of course we also have to provide proper code equations for
   the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
 *}
 
-lemma %quoteme plus_Dig [code func]:
+lemma %quoteme plus_Dig [code]:
   "0 + n = n"
   "m + 0 = m"
   "1 + Dig0 n = Dig1 n"
   "Dig0 m + 1 = Dig1 m"
   "1 + Dig1 n = Dig0 (n + 1)"

   \noindent For the former constructor @{term Suc}, we provide a code
   equation and remove some parts of the default code generator setup
   which are an obstacle here:
 *}
 
-lemma %quoteme Suc_Dig [code func]:
+lemma %quoteme Suc_Dig [code]:
   "Suc n = n + 1"
   by simp
 
 declare %quoteme One_nat_def [code inline del]
-declare %quoteme add_Suc_shift [code func del] 
+declare %quoteme add_Suc_shift [code del] 
 
 text {*
   \noindent This yields the following code:
 *}
 

       without relying on a particular representation.
   \end{itemize}
 *}
 
 code_datatype %invisible "0::nat" Suc
-declare %invisible plus_Dig [code func del]
+declare %invisible plus_Dig [code del]
 declare %invisible One_nat_def [code inline]
-declare %invisible add_Suc_shift [code func] 
-lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
+declare %invisible add_Suc_shift [code] 
+lemma %invisible [code]: "0 + n = (n \<Colon> nat)" by simp
 
 
 subsection {* Equality and wellsortedness *}
 
 text {*

 *}
 
 instantiation %quoteme "*" :: (order, order) order
 begin
 
-definition %quoteme [code func del]:
+definition %quoteme [code del]:
   "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
 
-definition %quoteme [code func del]:
+definition %quoteme [code del]:
   "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
 
 instance %quoteme proof
 qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
 
 end %quoteme
 
-lemma %quoteme order_prod [code func]:
+lemma %quoteme order_prod [code]:
   "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   by (simp_all add: less_prod_def less_eq_prod_def)

 
   The solution is to add @{class eq} explicitly to the first sort arguments in the
   code theorems:
 *}
 
-lemma %quoteme order_prod_code [code func]:
+lemma %quoteme order_prod_code [code]:
   "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   by (simp_all add: less_prod_def less_eq_prod_def)

   In such cases, you have to provide your own equality equations
   involving auxiliary constants.  In our case,
   @{const [show_types] list_all2} can do the job:
 *}
 
-lemma %quoteme monotype_eq_list_all2 [code func]:
+lemma %quoteme monotype_eq_list_all2 [code]:
   "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
      eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
   by (simp add: eq list_all2_eq [symmetric])
 
 text {*