# HG changeset patch # User Lars Hupel # Date 1539707684 -7200 # Node ID c5e3212455edda1d1351c1e42ab50f8e564d46d5 # Parent 42504382f75b7dd57c312b1dbabc9248f1788a1a more material on finite maps diff -r 42504382f75b -r c5e3212455ed src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy Sat Oct 13 11:13:12 2018 +0200 +++ b/src/HOL/Library/Finite_Map.thy Tue Oct 16 18:34:44 2018 +0200 @@ -157,7 +157,7 @@ setup_lifting type_definition_fmap -lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))" +lemma dom_fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))" using fmap.fmlookup by auto lemma fmap_ext: @@ -225,6 +225,12 @@ lemma fmdom'_alt_def: "fmdom' m = fset (fmdom m)" by transfer' force +lemma finite_fmdom'[simp]: "finite (fmdom' m)" +unfolding fmdom'_alt_def by simp + +lemma dom_fmlookup[simp]: "dom (fmlookup m) = fmdom' m" +by transfer' simp + lift_definition fmempty :: "('a, 'b) fmap" is Map.empty by simp @@ -351,6 +357,12 @@ lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \ A" unfolding fmfilter_alt_defs by auto lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\| A" unfolding fmfilter_alt_defs by auto +lemma fmdom'_restrict_set_precise: "fmdom' (fmrestrict_set A m) = fmdom' m \ A" +unfolding fmfilter_alt_defs by auto + +lemma fmdom'_restrict_fset_precise: "fmdom (fmrestrict_fset A m) = fmdom m |\| A" +unfolding fmfilter_alt_defs by auto + lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A" unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits) @@ -425,6 +437,39 @@ lemma fmdrop_fset_insert[simp]: "fmdrop_fset (finsert x S) m = fmdrop x (fmdrop_fset S m)" by (rule fmap_ext) auto +lemma fmrestrict_set_twice[simp]: "fmrestrict_set S (fmrestrict_set T m) = fmrestrict_set (S \ T) m" +unfolding fmfilter_alt_defs by auto + +lemma fmrestrict_fset_twice[simp]: "fmrestrict_fset S (fmrestrict_fset T m) = fmrestrict_fset (S |\| T) m" +unfolding fmfilter_alt_defs by auto + +lemma fmrestrict_set_drop[simp]: "fmrestrict_set S (fmdrop b m) = fmrestrict_set (S - {b}) m" +unfolding fmfilter_alt_defs by auto + +lemma fmrestrict_fset_drop[simp]: "fmrestrict_fset S (fmdrop b m) = fmrestrict_fset (S - {| b |}) m" +unfolding fmfilter_alt_defs by auto + +lemma fmdrop_fmrestrict_set[simp]: "fmdrop b (fmrestrict_set S m) = fmrestrict_set (S - {b}) m" +by (rule fmap_ext) auto + +lemma fmdrop_fmrestrict_fset[simp]: "fmdrop b (fmrestrict_fset S m) = fmrestrict_fset (S - {| b |}) m" +by (rule fmap_ext) auto + +lemma fmdrop_idem[simp]: "fmdrop a (fmdrop a m) = fmdrop a m" +unfolding fmfilter_alt_defs by auto + +lemma fmdrop_set_twice[simp]: "fmdrop_set S (fmdrop_set T m) = fmdrop_set (S \ T) m" +unfolding fmfilter_alt_defs by auto + +lemma fmdrop_fset_twice[simp]: "fmdrop_fset S (fmdrop_fset T m) = fmdrop_fset (S |\| T) m" +unfolding fmfilter_alt_defs by auto + +lemma fmdrop_set_fmdrop[simp]: "fmdrop_set S (fmdrop b m) = fmdrop_set (insert b S) m" +by (rule fmap_ext) auto + +lemma fmdrop_fset_fmdrop[simp]: "fmdrop_fset S (fmdrop b m) = fmdrop_fset (finsert b S) m" +by (rule fmap_ext) auto + lift_definition fmadd :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl "++\<^sub>f" 100) is map_add parametric map_add_transfer @@ -576,6 +621,24 @@ lemma fmsubset_restrict_fset_mono: "m \\<^sub>f n \ fmrestrict_fset A m \\<^sub>f fmrestrict_fset A n" unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) +lemma fmfilter_subset[simp]: "fmfilter P m \\<^sub>f m" +unfolding fmsubset_alt_def fmpred_iff by auto + +lemma fmsubset_drop[simp]: "fmdrop a m \\<^sub>f m" +unfolding fmfilter_alt_defs by (rule fmfilter_subset) + +lemma fmsubset_drop_set[simp]: "fmdrop_set S m \\<^sub>f m" +unfolding fmfilter_alt_defs by (rule fmfilter_subset) + +lemma fmsubset_drop_fset[simp]: "fmdrop_fset S m \\<^sub>f m" +unfolding fmfilter_alt_defs by (rule fmfilter_subset) + +lemma fmsubset_restrict_set[simp]: "fmrestrict_set S m \\<^sub>f m" +unfolding fmfilter_alt_defs by (rule fmfilter_subset) + +lemma fmsubset_restrict_fset[simp]: "fmrestrict_fset S m \\<^sub>f m" +unfolding fmfilter_alt_defs by (rule fmfilter_subset) + lift_definition fset_of_fmap :: "('a, 'b) fmap \ ('a \ 'b) fset" is set_of_map by (rule set_of_map_finite)