src/HOL/Orderings.thy

-(*  Title:      HOL/Orderings.thy
+ (*  Title:      HOL/Orderings.thy
     ID:         $Id$
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
 
 header {* Abstract orderings *}
 
 theory Orderings
 imports Code_Setup
-uses
-  "~~/src/Provers/order.ML"
+uses "~~/src/Provers/order.ML"
 begin
 
 subsection {* Quasi orders *}
 
 class preorder = ord +

 
 
 text {* min/max *}
 
 definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
+  [code del]: "min a b = (if a \<le> b then a else b)"
 
 definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
+  [code del]: "max a b = (if a \<le> b then b else a)"
 
 lemma min_le_iff_disj:
   "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
 unfolding min_def using linear by (auto intro: order_trans)
 

 lemma split_max [noatp]:
   "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
 by (simp add: max_def)
 
 end
+
+text {* Explicit dictionaries for code generation *}
+
+lemma min_ord_min [code, code unfold, code inline del]:
+  "min = ord.min (op \<le>)"
+  by (rule ext)+ (simp add: min_def ord.min_def)
+
+declare ord.min_def [code]
+
+lemma max_ord_max [code, code unfold, code inline del]:
+  "max = ord.max (op \<le>)"
+  by (rule ext)+ (simp add: max_def ord.max_def)
+
+declare ord.max_def [code]
 
 
 subsection {* Reasoning tools setup *}
 
 ML {*