merged

--- a/src/HOL/Library/FSet.thy	Mon Jul 10 19:48:58 2017 +0200
+++ b/src/HOL/Library/FSet.thy	Tue Jul 11 12:24:27 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>Type of finite sets defined as a subtype of sets\<close>
 
 theory FSet
-imports Main
+imports Main Countable
 begin
 
 subsection \<open>Definition of the type\<close>
@@ -202,9 +202,10 @@
 
 lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
 
+lift_definition fsum :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a fset \<Rightarrow> 'b" is sum .
+
 lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set)
 
-
 subsection \<open>Transferred lemmas from Set.thy\<close>
 
 lemmas fset_eqI = set_eqI[Transfer.transferred]
@@ -226,8 +227,8 @@
 lemmas fBall_one_point2[simp] = ball_one_point2[Transfer.transferred]
 lemmas fBall_conj_distrib = ball_conj_distrib[Transfer.transferred]
 lemmas fBex_disj_distrib = bex_disj_distrib[Transfer.transferred]
-lemmas fBall_cong = ball_cong[Transfer.transferred]
-lemmas fBex_cong = bex_cong[Transfer.transferred]
+lemmas fBall_cong[fundef_cong] = ball_cong[Transfer.transferred]
+lemmas fBex_cong[fundef_cong] = bex_cong[Transfer.transferred]
 lemmas fsubsetI[intro!] = subsetI[Transfer.transferred]
 lemmas fsubsetD[elim, intro?] = subsetD[Transfer.transferred]
 lemmas rev_fsubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred]
@@ -451,6 +452,17 @@
 
 subsection \<open>Additional lemmas\<close>
 
+subsubsection \<open>\<open>ffUnion\<close>\<close>
+
+lemmas ffUnion_funion_distrib[simp] = Union_Un_distrib[Transfer.transferred]
+
+
+subsubsection \<open>\<open>fbind\<close>\<close>
+
+lemma fbind_cong[fundef_cong]: "A = B \<Longrightarrow> (\<And>x. x |\<in>| B \<Longrightarrow> f x = g x) \<Longrightarrow> fbind A f = fbind B g"
+by transfer force
+
+
 subsubsection \<open>\<open>fsingleton\<close>\<close>
 
 lemmas fsingletonE = fsingletonD [elim_format]
@@ -530,6 +542,12 @@
 lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
   by (rule exI [where x = "A |-| {|a|}"]) blast
 
+lemma finsert_eq_iff:
+  assumes "a |\<notin>| A" and "b |\<notin>| B"
+  shows "(finsert a A = finsert b B) =
+    (if a = b then A = B else \<exists>C. A = finsert b C \<and> b |\<notin>| C \<and> B = finsert a C \<and> a |\<notin>| C)"
+  using assms by transfer (force simp: insert_eq_iff)
+
 
 subsubsection \<open>\<open>fimage\<close>\<close>
 
@@ -588,7 +606,7 @@
   "fcard (finsert x A) = (if x |\<in>| A then fcard A else Suc (fcard A))"
   by transfer (rule card_insert_if)
 
-lemma card_0_eq [simp, no_atp]:
+lemma fcard_0_eq [simp, no_atp]:
   "fcard A = 0 \<longleftrightarrow> A = {||}"
   by transfer (rule card_0_eq)
 
@@ -713,6 +731,83 @@
 
 end
 
+lemmas fsum_cong[fundef_cong] = sum.cong[Transfer.transferred]
+
+lemma fsum_strong_cong[cong]:
+  assumes "A = B" "\<And>x. x |\<in>| B =simp=> g x = h x"
+  shows "fsum (\<lambda>x. g x) A = fsum (\<lambda>x. h x) B"
+using assms unfolding simp_implies_def by (auto cong: fsum_cong)
+
+
+subsubsection \<open>Semilattice operations\<close>
+
+(* FIXME should work for arbitrary comm_monoid_set.F and semilattice_set.F operations *)
+
+lift_definition fMax :: "'a::linorder fset \<Rightarrow> 'a" is Max .
+lift_definition fMin :: "'a::linorder fset \<Rightarrow> 'a" is Min .
+
+lemma mono_fMax_commute: "mono f \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> f (fMax A) = fMax (f |`| A)"
+by transfer (rule mono_Max_commute)
+
+lemma mono_fMin_commute: "mono f \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> f (fMin A) = fMin (f |`| A)"
+by transfer (rule mono_Min_commute)
+
+lemma fMax_in[simp]: "A \<noteq> {||} \<Longrightarrow> fMax A |\<in>| A"
+  by transfer (rule Max_in)
+
+lemma fMin_in[simp]: "A \<noteq> {||} \<Longrightarrow> fMin A |\<in>| A"
+  by transfer (rule Min_in)
+
+lemma fMax_ge[simp]: "x |\<in>| A \<Longrightarrow> x \<le> fMax A"
+  by transfer (rule Max_ge)
+
+lemma fMin_le[simp]: "x |\<in>| A \<Longrightarrow> fMin A \<le> x"
+  by transfer (rule Min_le)
+
+lemma fMax_eqI: "(\<And>y. y |\<in>| A \<Longrightarrow> y \<le> x) \<Longrightarrow> x |\<in>| A \<Longrightarrow> fMax A = x"
+  by transfer (rule Max_eqI)
+
+lemma fMin_eqI: "(\<And>y. y |\<in>| A \<Longrightarrow> x \<le> y) \<Longrightarrow> x |\<in>| A \<Longrightarrow> fMin A = x"
+  by transfer (rule Min_eqI)
+
+lemma fMax_singleton[simp]: "fMax {|x|} = x"
+  by transfer (rule Max_singleton)
+
+lemma fMin_singleton[simp]: "fMin {|x|} = x"
+  by transfer (rule Min_singleton)
+
+lemma fMax_finsert[simp]: "fMax (finsert x A) = (if A = {||} then x else max x (fMax A))"
+  by transfer simp
+
+lemma fMin_finsert[simp]: "fMin (finsert x A) = (if A = {||} then x else min x (fMin A))"
+  by transfer simp
+
+context linorder begin
+
+lemma fset_linorder_max_induct[case_names fempty finsert]:
+  assumes "P {||}"
+  and     "\<And>x S. \<lbrakk>\<forall>y. y |\<in>| S \<longrightarrow> y < x; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
+  shows "P S"
+proof -
+  (* FIXME transfer and right_total vs. bi_total *)
+  note Domainp_forall_transfer[transfer_rule]
+  show ?thesis
+  using assms by (transfer fixing: less) (auto intro: finite_linorder_max_induct)
+qed
+
+lemma fset_linorder_min_induct[case_names fempty finsert]:
+  assumes "P {||}"
+  and     "\<And>x S. \<lbrakk>\<forall>y. y |\<in>| S \<longrightarrow> y > x; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
+  shows "P S"
+proof -
+  (* FIXME transfer and right_total vs. bi_total *)
+  note Domainp_forall_transfer[transfer_rule]
+  show ?thesis
+  using assms by (transfer fixing: less) (auto intro: finite_linorder_min_induct)
+qed
+
+end
+
 
 subsection \<open>Choice in fsets\<close>
 
@@ -1107,6 +1202,33 @@
 qed
 
 
+subsubsection \<open>Countability\<close>
+
+lemma exists_fset_of_list: "\<exists>xs. fset_of_list xs = S"
+including fset.lifting
+by transfer (rule finite_list)
+
+lemma fset_of_list_surj[simp, intro]: "surj fset_of_list"
+proof -
+  have "x \<in> range fset_of_list" for x :: "'a fset"
+    unfolding image_iff
+    using exists_fset_of_list by fastforce
+  thus ?thesis by auto
+qed
+
+instance fset :: (countable) countable
+proof
+  obtain to_nat :: "'a list \<Rightarrow> nat" where "inj to_nat"
+    by (metis ex_inj)
+  moreover have "inj (inv fset_of_list)"
+    using fset_of_list_surj by (rule surj_imp_inj_inv)
+  ultimately have "inj (to_nat \<circ> inv fset_of_list)"
+    by (rule inj_comp)
+  thus "\<exists>to_nat::'a fset \<Rightarrow> nat. inj to_nat"
+    by auto
+qed
+
+
 subsection \<open>Quickcheck setup\<close>
 
 text \<open>Setup adapted from sets.\<close>
@@ -1174,4 +1296,4 @@
 
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
-end
+end
\ No newline at end of file

--- a/src/HOL/Library/Monad_Syntax.thy	Mon Jul 10 19:48:58 2017 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Tue Jul 11 12:24:27 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Monad notation for arbitrary types\<close>
 
 theory Monad_Syntax
-imports Main "~~/src/Tools/Adhoc_Overloading"
+imports FSet "~~/src/Tools/Adhoc_Overloading"
 begin
 
 text \<open>
@@ -61,6 +61,6 @@
   "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
 
 adhoc_overloading
-  bind Set.bind Predicate.bind Option.bind List.bind
+  bind Set.bind Predicate.bind Option.bind List.bind FSet.fbind
 
-end
+end
\ No newline at end of file

--- a/src/HOL/Probability/Fin_Map.thy	Mon Jul 10 19:48:58 2017 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Jul 11 12:24:27 2017 +0200
@@ -1352,4 +1352,4 @@
 
 end
 
-end
+end
\ No newline at end of file