# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1535618562 -7200
# Node ID 34e777447ed5421bd474351a99f4d9ae2a8ff860
# Parent  abc338d25640478fa221994a4f572343ff19f2dd
material on finite sets

diff -r abc338d25640 -r 34e777447ed5 src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Tue Sep 04 16:23:54 2018 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Thu Aug 30 10:42:42 2018 +0200
@@ -378,43 +378,43 @@
 unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
-  by (rule fmap_ext) auto
+by (rule fmap_ext) auto
 
 lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
-  by (rule fmap_ext) auto
+by (rule fmap_ext) auto
 
 lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m"
-  by (rule fmap_ext) auto
+by (rule fmap_ext) auto
 
 lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m"
-  by (rule fmap_ext) auto
+by (rule fmap_ext) auto
 
 lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
 unfolding fmfilter_alt_defs by (rule fmfilter_comm)
@@ -438,30 +438,30 @@
 lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
 
 lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
-  by (rule fmap_ext) auto
+by (rule fmap_ext) auto
 
 lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
-  by (rule fmap_ext) auto
+by (rule fmap_ext) auto
 
 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)
 
 lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_set_add_distrib[simp]:
   "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_fset_add_distrib[simp]:
   "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
-  unfolding fmfilter_alt_defs by simp
+unfolding fmfilter_alt_defs by simp
 
 lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
 by (transfer'; auto)+
@@ -527,19 +527,19 @@
 by transfer' (auto simp: map_pred_def map_filter_def)
 
 lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
-  by (auto simp: fmfilter_alt_defs)
+by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
-  by (auto simp: fmfilter_alt_defs)
+by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
-  by (auto simp: fmfilter_alt_defs)
+by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
-  by (auto simp: fmfilter_alt_defs)
+by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
-  by (auto simp: fmfilter_alt_defs)
+by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_cases[consumes 1]:
   assumes "fmpred P m"
@@ -590,7 +590,6 @@
 lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
 by transfer' (auto simp: set_of_map_def)
 
-
 lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
   is map_of
   parametric map_of_transfer
@@ -819,19 +818,19 @@
 unfolding fmrel_iff by auto
 
 lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
-  unfolding fmfilter_alt_defs by blast
+unfolding fmfilter_alt_defs by blast
 
 lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
-  unfolding fmfilter_alt_defs by blast
+unfolding fmfilter_alt_defs by blast
 
 lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
-  unfolding fmfilter_alt_defs by blast
+unfolding fmfilter_alt_defs by blast
 
 lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
-  unfolding fmfilter_alt_defs by blast
+unfolding fmfilter_alt_defs by blast
 
 lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
-  unfolding fmfilter_alt_defs by blast
+unfolding fmfilter_alt_defs by blast
 
 lemma fmrel_on_fset_fmrel_restrict:
   "fmrel_on_fset S P m n \<longleftrightarrow> fmrel P (fmrestrict_fset S m) (fmrestrict_fset S n)"
@@ -1057,6 +1056,27 @@
 by transfer (simp add: map_of_map_keys)
 
 
+subsection \<open>Additional properties\<close>
+
+lemma fmchoice':
+  assumes "finite S" "\<forall>x \<in> S. \<exists>y. Q x y"
+  shows "\<exists>m. fmdom' m = S \<and> fmpred Q m"
+proof -
+  obtain f where f: "Q x (f x)" if "x \<in> S" for x
+    using assms by (metis bchoice)
+  define f' where "f' x = (if x \<in> S then Some (f x) else None)" for x
+
+  have "eq_onp (\<lambda>m. finite (dom m)) f' f'"
+    unfolding eq_onp_def f'_def dom_def using assms by auto
+
+  show ?thesis
+    apply (rule exI[where x = "Abs_fmap f'"])
+    apply (subst fmpred.abs_eq, fact)
+    apply (subst fmdom'.abs_eq, fact)
+    unfolding f'_def dom_def map_pred_def using f
+    by auto
+qed
+
 subsection \<open>Lifting/transfer setup\<close>
 
 context includes lifting_syntax begin
@@ -1066,14 +1086,40 @@
 
 lemma fmadd_transfer[transfer_rule]:
   "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd"
-  by (intro fmrel_addI rel_funI)
+by (intro fmrel_addI rel_funI)
 
 lemma fmupd_transfer[transfer_rule]:
   "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd"
-  by auto
+by auto
 
 end
 
+lemma Quotient_fmap_bnf[quot_map]:
+  assumes "Quotient R Abs Rep T"
+  shows "Quotient (fmrel R) (fmmap Abs) (fmmap Rep) (fmrel T)"
+unfolding Quotient_alt_def4 proof safe
+  fix m n
+  assume "fmrel T m n"
+  then have "fmlookup (fmmap Abs m) x = fmlookup n x" for x
+    apply (cases rule: fmrel_cases[where x = x])
+    using assms unfolding Quotient_alt_def by auto
+  then show "fmmap Abs m = n"
+    by (rule fmap_ext)
+next
+  fix m
+  show "fmrel T (fmmap Rep m) m"
+    unfolding fmap.rel_map
+    apply (rule fmap.rel_refl)
+    using assms unfolding Quotient_alt_def
+    by auto
+next
+  from assms have "R = T OO T\<inverse>\<inverse>"
+    unfolding Quotient_alt_def4 by simp
+
+  then show "fmrel R = fmrel T OO (fmrel T)\<inverse>\<inverse>"
+    by (simp add: fmap.rel_compp fmap.rel_conversep)
+qed
+
 
 subsection \<open>View as datatype\<close>
 
@@ -1311,4 +1357,31 @@
 lifting_update fmap.lifting
 lifting_forget fmap.lifting
 
+
+subsection \<open>Tests\<close>
+
+\<comment> \<open>Code generation\<close>
+
+export_code
+  fBall fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset fmupd fmrel_on_fset
+  fmdrop fmdrop_set fmdrop_fset fmrestrict_set fmrestrict_fset fmimage fmlookup fmempty
+  fmfilter fmadd fmmap fmmap_keys fmcomp
+  checking SML Scala Haskell? OCaml?
+
+\<comment> \<open>\<open>lifting\<close> through @{type fmap}\<close>
+
+experiment begin
+
+context includes fset.lifting begin
+
+lift_definition test1 :: "('a, 'b fset) fmap" is "fmempty :: ('a, 'b set) fmap"
+  by auto
+
+lift_definition test2 :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b fset) fmap" is "\<lambda>a b. fmupd a {b} fmempty"
+  by auto
+
+end
+
+end
+
 end
\ No newline at end of file