--- a/src/HOL/Orderings.thy Tue Oct 07 16:07:20 2008 +0200
+++ b/src/HOL/Orderings.thy Tue Oct 07 16:07:21 2008 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Orderings.thy
+ (* Title: HOL/Orderings.thy
ID: $Id$
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson
*)
@@ -7,8 +7,7 @@
theory Orderings
imports Code_Setup
-uses
- "~~/src/Provers/order.ML"
+uses "~~/src/Provers/order.ML"
begin
subsection {* Quasi orders *}
@@ -229,10 +228,10 @@
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"
@@ -268,6 +267,20 @@
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 *}