author Lars Hupel Thu, 13 Oct 2016 14:41:45 +0200 changeset 64180 676763a9c269 parent 64179 ce205d1f8592 child 64181 4d1d2de432fa
tuned
```--- a/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:15:34 2016 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:41:45 2016 +0200
@@ -35,7 +35,7 @@
then obtain y where "n a = Some y" "A x y"
unfolding \<open>m a = _\<close>
by cases auto
-      thus "\<exists>y \<in> ran n. A x y"
+      then show "\<exists>y \<in> ran n. A x y"
unfolding ran_def by blast
next
fix y
@@ -49,7 +49,7 @@
then obtain x where "m a = Some x" "A x y"
unfolding \<open>n a = _\<close>
by cases auto
-      thus "\<exists>x \<in> ran m. A x y"
+      then show "\<exists>x \<in> ran m. A x y"
unfolding ran_def by blast
qed
qed
@@ -65,10 +65,10 @@
proof -
from \<open>rel_map A m n\<close> have "rel_option A (m a) (n a)"
unfolding rel_fun_def by auto
-      thus ?thesis
+      then show ?thesis
by cases auto
qed
-  thus "dom m = dom n"
+  then show "dom m = dom n"
by auto
qed

@@ -102,7 +102,7 @@
have "dom (map_filter P m) = Set.filter P (dom m)"
unfolding map_filter_def Set.filter_def dom_def
by auto
-  thus ?thesis
+  then show ?thesis
using assms
qed
@@ -261,7 +261,7 @@
have "fmlookup m x = None" if "\<not> P x"
using that assms
unfolding fmlookup_dom_iff by fastforce
-  thus "fmlookup (fmfilter P m) x = fmlookup m x"
+  then show "fmlookup (fmfilter P m) x = fmlookup m x"
by simp
qed

@@ -282,7 +282,7 @@
have "fmlookup m x = None" if "P x \<noteq> Q x"
using that assms
unfolding fmlookup_dom_iff by fastforce
-  thus "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
+  then show "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x"
by auto
qed

@@ -292,7 +292,7 @@
proof (rule fmfilter_cong)
fix x
assume "x |\<in>| fmdom m"
-  thus "P x = Q x"
+  then show "P x = Q x"
using assms
unfolding fmdom'_alt_def fmember.rep_eq
by auto
@@ -611,26 +611,36 @@
rel: fmrel
by auto

+text \<open>
+  Unfortunately, @{command lift_bnf} doesn't register the definitional theorems. We're doing it
+  manually below.
+\<close>
+
+local_setup \<open>fn lthy =>
+  let
+    val SOME bnf = BNF_Def.bnf_of lthy @{type_name fmap}
+  in
+    lthy
+    |> Local_Theory.note ((@{binding fmmap_def}, []), [BNF_Def.map_def_of_bnf bnf]) |> #2
+    |> Local_Theory.note ((@{binding fmran'_def}, []), BNF_Def.set_defs_of_bnf bnf) |> #2
+    |> Local_Theory.note ((@{binding fmrel_def}, []), [BNF_Def.rel_def_of_bnf bnf]) |> #2
+  end
+\<close>
+
context includes lifting_syntax begin

lemma fmmap_transfer[transfer_rule]:
"(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =) (\<lambda>f. op \<circ> (map_option f)) fmmap"
-apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
-apply (rule rel_funI ext)+
-apply (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
-done
+  unfolding fmmap_def
+  by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)

lemma fmran'_transfer[transfer_rule]:
"(pcr_fmap op = op = ===> op =) (\<lambda>x. UNION (range x) set_option) fmran'"
-apply (tactic \<open>Local_Defs.unfold_tac @{context} (BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.set_defs_of_bnf)\<close>)
-unfolding fmap.pcr_cr_eq cr_fmap_def
-by fastforce
+  unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce

lemma fmrel_transfer[transfer_rule]:
"(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op = ===> op =) rel_map fmrel"
-apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.rel_def_of_bnf]\<close>)
-unfolding fmap.pcr_cr_eq cr_fmap_def vimage2p_def
-  by fastforce
+  unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce

end

@@ -675,7 +685,7 @@
proof -
from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
by auto
-  thus thesis
+  then show thesis
using none some
by (cases rule: option.rel_cases) auto
qed
@@ -711,9 +721,7 @@
by simp

lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
-apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
-apply (auto simp: fmap.Abs_fmap_inverse)
-done
+by transfer' auto

lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
unfolding fmpred_iff pred_fmap_def fmap.set_map
@@ -758,7 +766,7 @@
fix m n :: "('a, 'b) fmap"
have "fmrel op = m n \<longleftrightarrow> (m = n)"
by transfer' (simp add: option.rel_eq rel_fun_eq)
-  thus "equal_class.equal m n \<longleftrightarrow> (m = n)"
+  then show "equal_class.equal m n \<longleftrightarrow> (m = n)"
unfolding equal_fmap_def