adding code equations for max_extp and mlex
authorbulwahn
Mon Jan 30 13:55:24 2012 +0100 (2012-01-30)
changeset 4636187d5d36a9005
parent 46360 5cb81e3fa799
child 46362 b2878f059f91
adding code equations for max_extp and mlex
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Jan 30 13:55:23 2012 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Jan 30 13:55:24 2012 +0100
     1.3 @@ -799,6 +799,14 @@
     1.4    "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
     1.5  by (auto simp add: max_ext.simps)
     1.6  
     1.7 +lemma max_extp_eq[code]:
     1.8 +  "max_extp r x y = ((x, y) : max_ext {(x, y). r x y})"
     1.9 +unfolding max_ext_def by auto
    1.10 +
    1.11 +lemma mlex_eq[code]:
    1.12 +  "f <*mlex*> R = {(x, y). f x < f y \<or> (f x <= f y \<and> (x, y) : R)}"
    1.13 +unfolding mlex_prod_def by auto
    1.14 +
    1.15  subsection {* Executable accessible part *}
    1.16  (* FIXME: should be moved somewhere else !? *)
    1.17