# HG changeset patch
# User bulwahn
# Date 1327928124 -3600
# Node ID 87d5d36a9005eb710b4f39759e580e2f4ddcd319
# Parent  5cb81e3fa79927f404ed40d366572324b8a304be
adding code equations for max_extp and mlex

diff -r 5cb81e3fa799 -r 87d5d36a9005 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Jan 30 13:55:23 2012 +0100
+++ b/src/HOL/Enum.thy	Mon Jan 30 13:55:24 2012 +0100
@@ -799,6 +799,14 @@
   "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
 by (auto simp add: max_ext.simps)
 
+lemma max_extp_eq[code]:
+  "max_extp r x y = ((x, y) : max_ext {(x, y). r x y})"
+unfolding max_ext_def by auto
+
+lemma mlex_eq[code]:
+  "f <*mlex*> R = {(x, y). f x < f y \<or> (f x <= f y \<and> (x, y) : R)}"
+unfolding mlex_prod_def by auto
+
 subsection {* Executable accessible part *}
 (* FIXME: should be moved somewhere else !? *)