# HG changeset patch # User bulwahn # Date 1328435032 -3600 # Node ID b447318e5e1a6bd55e114b182745cff57564e6fb # Parent 51259911b9faf7c4985642372f766a7c66fc7577 adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists diff -r 51259911b9fa -r b447318e5e1a src/HOL/List.thy --- a/src/HOL/List.thy Sun Feb 05 10:42:57 2012 +0100 +++ b/src/HOL/List.thy Sun Feb 05 10:43:52 2012 +0100 @@ -5688,6 +5688,16 @@ "setsum f (set xs) = listsum (map f (remdups xs))" by (simp add: listsum_distinct_conv_setsum_set) +definition map_project :: "('a \ 'b option) \ 'a set \ 'b set" where + "map_project f A = {b. \ a \ A. f a = Some b}" + +lemma [code]: + "map_project f (set xs) = set (List.map_filter f xs)" +unfolding map_project_def map_filter_def +by auto (metis (lifting, mono_tags) CollectI image_eqI o_apply the.simps) + +hide_const (open) map_project + text {* Operations on relations *} lemma product_code [code]: @@ -5698,6 +5708,10 @@ "Id_on (set xs) = set [(x, x). x \ xs]" by (auto simp add: Id_on_def) +lemma [code]: + "R `` S = List.map_project (%(x, y). if x : S then Some y else None) R" +unfolding map_project_def by (auto split: prod.split split_if_asm) + lemma trancl_set_ntrancl [code]: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" by (simp add: finite_trancl_ntranl)