equal
deleted
inserted
replaced
796 unfolding rtrancl_def by auto |
796 unfolding rtrancl_def by auto |
797 |
797 |
798 lemma max_ext_eq[code]: |
798 lemma max_ext_eq[code]: |
799 "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}" |
799 "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}" |
800 by (auto simp add: max_ext.simps) |
800 by (auto simp add: max_ext.simps) |
|
801 |
|
802 lemma max_extp_eq[code]: |
|
803 "max_extp r x y = ((x, y) : max_ext {(x, y). r x y})" |
|
804 unfolding max_ext_def by auto |
|
805 |
|
806 lemma mlex_eq[code]: |
|
807 "f <*mlex*> R = {(x, y). f x < f y \<or> (f x <= f y \<and> (x, y) : R)}" |
|
808 unfolding mlex_prod_def by auto |
801 |
809 |
802 subsection {* Executable accessible part *} |
810 subsection {* Executable accessible part *} |
803 (* FIXME: should be moved somewhere else !? *) |
811 (* FIXME: should be moved somewhere else !? *) |
804 |
812 |
805 subsubsection {* Finite monotone eventually stable sequences *} |
813 subsubsection {* Finite monotone eventually stable sequences *} |