# HG changeset patch # User nipkow # Date 1380295202 -7200 # Node ID 967728367ad929a3ff418df95abdf8a9a3c5c451 # Parent 2f103a894ebe40c6719b3599ab651b08c854acc9# Parent 436649a2ed62b26cb6769d8d751094234f7fd713 merged diff -r 2f103a894ebe -r 967728367ad9 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Fri Sep 27 14:43:26 2013 +0200 +++ b/src/HOL/Library/RBT_Set.thy Fri Sep 27 17:20:02 2013 +0200 @@ -135,6 +135,9 @@ lemma [code, code del]: "List.map_project = List.map_project" .. +lemma [code, code del]: + "List.Bleast = List.Bleast" .. + section {* Lemmas *} @@ -805,6 +808,28 @@ "sorted_list_of_set (Set t) = keys t" by (auto simp add: set_keys intro: sorted_distinct_set_unique) +lemma Bleast_code [code]: + "Bleast (Set t) P = (case filter P (keys t) of + x#xs \ x | + [] \ abort_Bleast (Set t) P)" +proof (cases "filter P (keys t)") + case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def) +next + case (Cons x ys) + have "(LEAST x. x \ Set t \ P x) = x" + proof (rule Least_equality) + show "x \ Set t \ P x" using Cons[symmetric] + by(auto simp add: set_keys Cons_eq_filter_iff) + next + fix y assume "y : Set t \ P y" + then show "x \ y" using Cons[symmetric] + by(auto simp add: set_keys Cons_eq_filter_iff) + (metis sorted_Cons sorted_append sorted_keys) + qed + thus ?thesis using Cons by (simp add: Bleast_def) +qed + + hide_const (open) RBT_Set.Set RBT_Set.Coset end diff -r 2f103a894ebe -r 967728367ad9 src/HOL/List.thy --- a/src/HOL/List.thy Fri Sep 27 14:43:26 2013 +0200 +++ b/src/HOL/List.thy Fri Sep 27 17:20:02 2013 +0200 @@ -5961,6 +5961,37 @@ "setsum f (set [m.. S \ P x)" + +definition "abort_Bleast S P = (LEAST x. x \ S \ P x)" + +code_abort abort_Bleast + +lemma Bleast_code [code]: + "Bleast (set xs) P = (case filter P (sort xs) of + x#xs \ x | + [] \ 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 \ set xs \ P x) = x" + proof (rule Least_equality) + show "x \ set xs \ P x" + by (metis Cons Cons_eq_filter_iff in_set_conv_decomp set_sort) + next + fix y assume "y : set xs \ P y" + hence "y : set (filter P xs)" by auto + thus "x \ 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]: