tuned min/max code generation
authorhaftmann
Tue Oct 07 16:07:21 2008 +0200 (2008-10-07)
changeset 28516e6fdcaaadbd3
parent 28515 b26ba1b1dbda
child 28517 dd46786d4f95
tuned min/max code generation
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Orderings.thy	Tue Oct 07 16:07:20 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Oct 07 16:07:21 2008 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Orderings.thy
     1.5 + (*  Title:      HOL/Orderings.thy
     1.6      ID:         $Id$
     1.7      Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     1.8  *)
     1.9 @@ -7,8 +7,7 @@
    1.10  
    1.11  theory Orderings
    1.12  imports Code_Setup
    1.13 -uses
    1.14 -  "~~/src/Provers/order.ML"
    1.15 +uses "~~/src/Provers/order.ML"
    1.16  begin
    1.17  
    1.18  subsection {* Quasi orders *}
    1.19 @@ -229,10 +228,10 @@
    1.20  text {* min/max *}
    1.21  
    1.22  definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.23 -  [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
    1.24 +  [code del]: "min a b = (if a \<le> b then a else b)"
    1.25  
    1.26  definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.27 -  [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
    1.28 +  [code del]: "max a b = (if a \<le> b then b else a)"
    1.29  
    1.30  lemma min_le_iff_disj:
    1.31    "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
    1.32 @@ -268,6 +267,20 @@
    1.33  
    1.34  end
    1.35  
    1.36 +text {* Explicit dictionaries for code generation *}
    1.37 +
    1.38 +lemma min_ord_min [code, code unfold, code inline del]:
    1.39 +  "min = ord.min (op \<le>)"
    1.40 +  by (rule ext)+ (simp add: min_def ord.min_def)
    1.41 +
    1.42 +declare ord.min_def [code]
    1.43 +
    1.44 +lemma max_ord_max [code, code unfold, code inline del]:
    1.45 +  "max = ord.max (op \<le>)"
    1.46 +  by (rule ext)+ (simp add: max_def ord.max_def)
    1.47 +
    1.48 +declare ord.max_def [code]
    1.49 +
    1.50  
    1.51  subsection {* Reasoning tools setup *}
    1.52