# HG changeset patch # User Lars Hupel # Date 1474044258 -7200 # Node ID 2359e995264107456fd892f037457f60f085c673 # Parent dc036b1a2a6f22d68bcbc5ec5ccae37f66f77b77 tuned proofs diff -r dc036b1a2a6f -r 2359e9952641 src/HOL/Library/Finite_Map.thy --- a/src/HOL/Library/Finite_Map.thy Fri Sep 16 18:09:13 2016 +0200 +++ b/src/HOL/Library/Finite_Map.thy Fri Sep 16 18:44:18 2016 +0200 @@ -196,6 +196,7 @@ lemma fmdom_notI: "fmlookup m x = None \ x |\| fmdom m" by transfer' auto lemma fmdomI: "fmlookup m x = Some y \ x |\| fmdom m" by transfer' auto +lemma fmdom_notD: "x |\| fmdom m \ fmlookup m x = None" by transfer' auto lift_definition fmdom' :: "('a, 'b) fmap \ 'a set" is dom @@ -204,6 +205,7 @@ lemma fmdom'_notI: "fmlookup m x = None \ x \ fmdom' m" by transfer' auto lemma fmdom'I: "fmlookup m x = Some y \ x \ fmdom' m" by transfer' auto +lemma fmdom'_notD: "x \ fmdom' m \ fmlookup m x = None" by transfer' auto lemma fmdom'_alt_def: "fmdom' = fset \ fmdom" by transfer' force @@ -251,22 +253,20 @@ lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty" by transfer' (auto simp: map_filter_def) -lemma fmfilter_true[simp]: "(\x. x |\| fmdom m \ P x) \ fmfilter P m = m" -apply transfer' -apply (rule ext) -apply (auto simp: map_filter_def) -apply (case_tac "m x") -apply simp -apply simp -apply (drule_tac m = m in domI) -apply auto -done +lemma fmfilter_true[simp]: + assumes "\x. x |\| fmdom m \ P x" + shows "fmfilter P m = m" +proof (rule fmap_ext) + fix x + have "fmlookup m x = None" if "\ P x" + using that assms + unfolding fmlookup_dom_iff by fastforce + thus "fmlookup (fmfilter P m) x = fmlookup m x" + by simp +qed lemma fmfilter_false[simp]: "(\x. x |\| fmdom m \ \ P x) \ fmfilter P m = fmempty" -apply transfer' -apply (rule ext) -apply (auto simp: map_filter_def) -done +by transfer' (auto simp: map_filter_def fun_eq_iff) lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\x. P x \ Q x) m" by transfer' (auto simp: map_filter_def) @@ -277,26 +277,29 @@ lemma fmfilter_cong[cong]: assumes "\x. x |\| fmdom m \ P x = Q x" shows "fmfilter P m = fmfilter Q m" -using assms -apply transfer' -apply (rule ext) -apply (auto simp: map_filter_def split: if_splits) -apply (case_tac "m x") -apply simp -apply simp -apply (drule_tac m = m in domI) -apply auto -done +proof (rule fmap_ext) + fix x + have "fmlookup m x = None" if "P x \ Q x" + using that assms + unfolding fmlookup_dom_iff by fastforce + thus "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x" + by auto +qed lemma fmfilter_cong'[fundef_cong]: assumes "\x. x \ fmdom' m \ P x = Q x" shows "fmfilter P m = fmfilter Q m" -apply (rule fmfilter_cong) -using assms -unfolding fmdom'_alt_def fmember.rep_eq -by auto +proof (rule fmfilter_cong) + fix x + assume "x |\| fmdom m" + thus "P x = Q x" + using assms + unfolding fmdom'_alt_def fmember.rep_eq + by auto +qed -lemma fmfilter_upd[simp]: "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)" +lemma fmfilter_upd[simp]: + "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)" by transfer' (auto simp: map_upd_def map_filter_def) lift_definition fmdrop :: "'a \ ('a, 'b) fmap \ ('a, 'b) fmap" @@ -322,25 +325,11 @@ parametric map_restrict_set_transfer unfolding map_restrict_set_def by auto -lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m" -apply transfer' -apply (auto simp: map_restrict_set_def map_filter_def) -apply (rule ext) -apply (auto split: if_splits) -by (metis option.collapse) - lift_definition fmrestrict_fset :: "'a fset \ ('a, 'b) fmap \ ('a, 'b) fmap" is map_restrict_set parametric map_restrict_set_transfer unfolding map_restrict_set_def by auto -lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m" -apply transfer' -apply (auto simp: map_restrict_set_def map_filter_def) -apply (rule ext) -apply (auto split: if_splits) -by (metis option.collapse) - lemma fmfilter_alt_defs: "fmdrop a = fmfilter (\a'. a' \ a)" "fmdrop_set A = fmfilter (\a. a \ A)" @@ -382,6 +371,12 @@ "fmlookup (fmrestrict_fset A m) x = (if x |\| A then fmlookup m x else None)" unfolding fmfilter_alt_defs by simp +lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m" + by (rule fmap_ext) (auto dest: fmdom'_notD) + +lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m" + by (rule fmap_ext) (auto dest: fmdom_notD) + lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty" unfolding fmfilter_alt_defs by simp @@ -420,18 +415,18 @@ parametric map_add_transfer by simp +lemma fmlookup_add[simp]: + "fmlookup (m ++\<^sub>f n) x = (if x |\| fmdom n then fmlookup n x else fmlookup m x)" + by transfer' (auto simp: map_add_def split: option.splits) + lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\| fmdom n" by transfer' auto lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \ fmdom' n" by transfer' auto lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n" -apply transfer' -unfolding map_add_def dom_def map_drop_set_def map_filter_def -by (rule ext) auto + by (rule fmap_ext) auto lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n" -apply transfer' -unfolding map_add_def dom_def map_restrict_set_def map_filter_def -by (rule ext) auto + by (rule fmap_ext) (auto dest: fmdom_notD) lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n" by transfer' (auto simp: map_filter_def map_add_def) @@ -462,10 +457,6 @@ lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p" by transfer' simp -lemma fmlookup_add[simp]: - "fmlookup (m ++\<^sub>f n) x = (if x |\| fmdom n then fmlookup n x else fmlookup m x)" - by transfer' (auto simp: map_add_def split: option.splits) - lift_definition fmpred :: "('a \ 'b \ bool) \ ('a, 'b) fmap \ bool" is map_pred parametric map_pred_transfer @@ -488,6 +479,7 @@ apply auto apply (subst (asm) fmlookup_dom_iff) apply simp +apply (rename_tac x y) apply (erule_tac x = x in fBallE) apply simp by (simp add: fmlookup_dom_iff)