# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID 360a05d6076159d185cf100e38dd2b7c140de821
# Parent  a16d294f7e3ff3bfcf1b4db41eb378acf4eea7b4
added 'size' of finite sets

diff -r a16d294f7e3f -r 360a05d60761 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Library/FSet.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -112,7 +112,7 @@
   fix X :: "'a fset set"
   {
     assume "x \<in> X" "bdd_below X" 
-    then show "Inf X |\<subseteq>| x"  by transfer auto
+    then show "Inf X |\<subseteq>| x" by transfer auto
   next
     assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z |\<subseteq>| x)"
     then show "z |\<subseteq>| Inf X" by transfer (clarsimp, blast)
@@ -150,6 +150,8 @@
 abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
 abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x"
 
+declare top_fset.rep_eq[simp]
+
 
 subsection {* Other operations *}
 
@@ -643,7 +645,7 @@
     by (transfer fixing: f) (rule fold_fun_left_comm)
 
   lemma ffold_finsert2:
-    "x |\<notin>| A \<Longrightarrow> ffold f z (finsert x A)  = ffold f (f x z) A"
+    "x |\<notin>| A \<Longrightarrow> ffold f z (finsert x A) = ffold f (f x z) A"
     by (transfer fixing: f) (rule fold_insert2)
 
   lemma ffold_rec:
@@ -672,7 +674,7 @@
 begin
 
   lemma ffold_finsert_idem:
-    "ffold f z (finsert x A)  = f x (ffold f z A)"
+    "ffold f z (finsert x A) = f x (ffold f z A)"
     by (transfer fixing: f) (rule fold_insert_idem)
   
   declare ffold_finsert [simp del] ffold_finsert_idem [simp]
@@ -782,7 +784,7 @@
   apply (subst bchoice_iff[symmetric])
   using R_S[unfolded rel_set_def OO_def] by blast
   
-  obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R  x (g z))"
+  obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
   apply atomize_elim
   apply (subst bchoice_iff[symmetric])
   using R_S[unfolded rel_set_def OO_def] by blast
@@ -978,6 +980,36 @@
 lemmas [simp] = fset.map_comp fset.map_id fset.set_map
 
 
+subsection {* Size setup *}
+
+context includes fset.lifting begin
+lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. setsum (Suc \<circ> f)" .
+end
+
+instantiation fset :: (type) size begin
+definition size_fset where
+  size_fset_overloaded_def: "size_fset = FSet.size_fset (\<lambda>_. 0)"
+instance ..
+end
+
+lemmas size_fset_simps[simp] =
+  size_fset_def[THEN meta_eq_to_obj_eq, THEN fun_cong, THEN fun_cong,
+    unfolded map_fun_def comp_def id_apply]
+
+lemmas size_fset_overloaded_simps[simp] =
+  size_fset_simps[of "\<lambda>_. 0", unfolded add_0_left add_0_right,
+    folded size_fset_overloaded_def]
+
+lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
+  unfolding size_fset_def fimage_def
+  by (auto simp: Abs_fset_inverse setsum_reindex_cong[OF subset_inj_on[OF _ top_greatest]])
+
+setup {*
+BNF_LFP_Size.register_size @{type_name fset} @{const_name size_fset}
+  @{thms size_fset_simps size_fset_overloaded_simps} @{thms fset_size_o_map}
+*}
+
+
 subsection {* Advanced relator customization *}
 
 (* Set vs. sum relators: *)