src/HOL/Library/Finite_Map.thy
changeset 63900 2359e9952641
parent 63885 a6cd18af8bf9
child 64179 ce205d1f8592
     1.1 --- a/src/HOL/Library/Finite_Map.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/Library/Finite_Map.thy	Fri Sep 16 18:44:18 2016 +0200
     1.3 @@ -196,6 +196,7 @@
     1.4  
     1.5  lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by transfer' auto
     1.6  lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by transfer' auto
     1.7 +lemma fmdom_notD: "x |\<notin>| fmdom m \<Longrightarrow> fmlookup m x = None" by transfer' auto
     1.8  
     1.9  lift_definition fmdom' :: "('a, 'b) fmap \<Rightarrow> 'a set"
    1.10    is dom
    1.11 @@ -204,6 +205,7 @@
    1.12  
    1.13  lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by transfer' auto
    1.14  lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by transfer' auto
    1.15 +lemma fmdom'_notD: "x \<notin> fmdom' m \<Longrightarrow> fmlookup m x = None" by transfer' auto
    1.16  
    1.17  lemma fmdom'_alt_def: "fmdom' = fset \<circ> fmdom"
    1.18  by transfer' force
    1.19 @@ -251,22 +253,20 @@
    1.20  lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty"
    1.21  by transfer' (auto simp: map_filter_def)
    1.22  
    1.23 -lemma fmfilter_true[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x) \<Longrightarrow> fmfilter P m = m"
    1.24 -apply transfer'
    1.25 -apply (rule ext)
    1.26 -apply (auto simp: map_filter_def)
    1.27 -apply (case_tac "m x")
    1.28 -apply simp
    1.29 -apply simp
    1.30 -apply (drule_tac m = m in domI)
    1.31 -apply auto
    1.32 -done
    1.33 +lemma fmfilter_true[simp]:
    1.34 +  assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x"
    1.35 +  shows "fmfilter P m = m"
    1.36 +proof (rule fmap_ext)
    1.37 +  fix x
    1.38 +  have "fmlookup m x = None" if "\<not> P x"
    1.39 +    using that assms
    1.40 +    unfolding fmlookup_dom_iff by fastforce
    1.41 +  thus "fmlookup (fmfilter P m) x = fmlookup m x"
    1.42 +    by simp
    1.43 +qed
    1.44  
    1.45  lemma fmfilter_false[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> \<not> P x) \<Longrightarrow> fmfilter P m = fmempty"
    1.46 -apply transfer'
    1.47 -apply (rule ext)
    1.48 -apply (auto simp: map_filter_def)
    1.49 -done
    1.50 +by transfer' (auto simp: map_filter_def fun_eq_iff)
    1.51  
    1.52  lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\<lambda>x. P x \<and> Q x) m"
    1.53  by transfer' (auto simp: map_filter_def)
    1.54 @@ -277,26 +277,29 @@
    1.55  lemma fmfilter_cong[cong]:
    1.56    assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x = Q x"
    1.57    shows "fmfilter P m = fmfilter Q m"
    1.58 -using assms
    1.59 -apply transfer'
    1.60 -apply (rule ext)
    1.61 -apply (auto simp: map_filter_def split: if_splits)
    1.62 -apply (case_tac "m x")
    1.63 -apply simp
    1.64 -apply simp
    1.65 -apply (drule_tac m = m in domI)
    1.66 -apply auto
    1.67 -done
    1.68 +proof (rule fmap_ext)
    1.69 +  fix x
    1.70 +  have "fmlookup m x = None" if "P x \<noteq> Q x"
    1.71 +    using that assms
    1.72 +    unfolding fmlookup_dom_iff by fastforce
    1.73 +  thus "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
    1.74 +    by auto
    1.75 +qed
    1.76  
    1.77  lemma fmfilter_cong'[fundef_cong]:
    1.78    assumes "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
    1.79    shows "fmfilter P m = fmfilter Q m"
    1.80 -apply (rule fmfilter_cong)
    1.81 -using assms
    1.82 -unfolding fmdom'_alt_def fmember.rep_eq
    1.83 -by auto
    1.84 +proof (rule fmfilter_cong)
    1.85 +  fix x
    1.86 +  assume "x |\<in>| fmdom m"
    1.87 +  thus "P x = Q x"
    1.88 +    using assms
    1.89 +    unfolding fmdom'_alt_def fmember.rep_eq
    1.90 +    by auto
    1.91 +qed
    1.92  
    1.93 -lemma fmfilter_upd[simp]: "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
    1.94 +lemma fmfilter_upd[simp]:
    1.95 +  "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
    1.96  by transfer' (auto simp: map_upd_def map_filter_def)
    1.97  
    1.98  lift_definition fmdrop :: "'a \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
    1.99 @@ -322,25 +325,11 @@
   1.100    parametric map_restrict_set_transfer
   1.101  unfolding map_restrict_set_def by auto
   1.102  
   1.103 -lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
   1.104 -apply transfer'
   1.105 -apply (auto simp: map_restrict_set_def map_filter_def)
   1.106 -apply (rule ext)
   1.107 -apply (auto split: if_splits)
   1.108 -by (metis option.collapse)
   1.109 -
   1.110  lift_definition fmrestrict_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   1.111    is map_restrict_set
   1.112    parametric map_restrict_set_transfer
   1.113  unfolding map_restrict_set_def by auto
   1.114  
   1.115 -lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
   1.116 -apply transfer'
   1.117 -apply (auto simp: map_restrict_set_def map_filter_def)
   1.118 -apply (rule ext)
   1.119 -apply (auto split: if_splits)
   1.120 -by (metis option.collapse)
   1.121 -
   1.122  lemma fmfilter_alt_defs:
   1.123    "fmdrop a = fmfilter (\<lambda>a'. a' \<noteq> a)"
   1.124    "fmdrop_set A = fmfilter (\<lambda>a. a \<notin> A)"
   1.125 @@ -382,6 +371,12 @@
   1.126    "fmlookup (fmrestrict_fset A m) x = (if x |\<in>| A then fmlookup m x else None)"
   1.127  unfolding fmfilter_alt_defs by simp
   1.128  
   1.129 +lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
   1.130 +  by (rule fmap_ext) (auto dest: fmdom'_notD)
   1.131 +
   1.132 +lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
   1.133 +  by (rule fmap_ext) (auto dest: fmdom_notD)
   1.134 +
   1.135  lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
   1.136    unfolding fmfilter_alt_defs by simp
   1.137  
   1.138 @@ -420,18 +415,18 @@
   1.139    parametric map_add_transfer
   1.140  by simp
   1.141  
   1.142 +lemma fmlookup_add[simp]:
   1.143 +  "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
   1.144 +  by transfer' (auto simp: map_add_def split: option.splits)
   1.145 +
   1.146  lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\<union>| fmdom n" by transfer' auto
   1.147  lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
   1.148  
   1.149  lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
   1.150 -apply transfer'
   1.151 -unfolding map_add_def dom_def map_drop_set_def map_filter_def
   1.152 -by (rule ext) auto
   1.153 +  by (rule fmap_ext) auto
   1.154  
   1.155  lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
   1.156 -apply transfer'
   1.157 -unfolding map_add_def dom_def map_restrict_set_def map_filter_def
   1.158 -by (rule ext) auto
   1.159 +  by (rule fmap_ext) (auto dest: fmdom_notD)
   1.160  
   1.161  lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
   1.162  by transfer' (auto simp: map_filter_def map_add_def)
   1.163 @@ -462,10 +457,6 @@
   1.164  lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
   1.165  by transfer' simp
   1.166  
   1.167 -lemma fmlookup_add[simp]:
   1.168 -  "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
   1.169 -  by transfer' (auto simp: map_add_def split: option.splits)
   1.170 -
   1.171  lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
   1.172    is map_pred
   1.173    parametric map_pred_transfer
   1.174 @@ -488,6 +479,7 @@
   1.175  apply auto
   1.176  apply (subst (asm) fmlookup_dom_iff)
   1.177  apply simp
   1.178 +apply (rename_tac x y)
   1.179  apply (erule_tac x = x in fBallE)
   1.180  apply simp
   1.181  by (simp add: fmlookup_dom_iff)