# HG changeset patch
# User nipkow
# Date 1380289103 -7200
# Node ID ccfd22f937beeb185c928043c76a03c2fa113b3a
# Parent  54b08afc03c762706e9d04f1552cee9448a6795f
added code eqns for bounded LEAST operator

diff -r 54b08afc03c7 -r ccfd22f937be src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Sep 27 10:40:02 2013 +0200
+++ b/src/HOL/List.thy	Fri Sep 27 15:38:23 2013 +0200
@@ -5961,6 +5961,37 @@
   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
   by (simp add: interv_listsum_conv_setsum_set_nat)
 
+text{* Bounded @{text LEAST} operator: *}
+
+definition "Bleast S P = (LEAST x. x \<in> S \<and> P x)"
+
+definition "abort_Bleast S P = (LEAST x. x \<in> S \<and> P x)"
+
+code_abort abort_Bleast
+
+lemma Bleast_code [code]:
+ "Bleast (set xs) P = (case filter P (sort xs) of
+    x#xs \<Rightarrow> x |
+    [] \<Rightarrow> abort_Bleast (set xs) P)"
+proof (cases "filter P (sort xs)")
+  case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
+next
+  case (Cons x ys)
+  have "(LEAST x. x \<in> set xs \<and> P x) = x"
+  proof (rule Least_equality)
+    show "x \<in> set xs \<and> P x"
+      by (metis Cons Cons_eq_filter_iff in_set_conv_decomp set_sort)
+    next
+      fix y assume "y : set xs \<and> P y"
+      hence "y : set (filter P xs)" by auto
+      thus "x \<le> y"
+        by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted_Cons sorted_sort)
+  qed
+  thus ?thesis using Cons by (simp add: Bleast_def)
+qed
+
+declare Bleast_def[symmetric, code_unfold]
+
 text {* Summation over ints. *}
 
 lemma greaterThanLessThan_upto [code_unfold]: