# HG changeset patch
# User Andreas Lochbihler
# Date 1360861093 -3600
# Node ID 8fd094d5b7b7003ad41030d3f115dc513b7d46bd
# Parent  47af65ef228e92489948679bec1586b0a7f9bb8c
instantiate finite_UNIV and card_UNIV for finfun type

diff -r 47af65ef228e -r 8fd094d5b7b7 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Thu Feb 14 16:01:59 2013 +0100
+++ b/src/HOL/Library/FinFun.thy	Thu Feb 14 17:58:13 2013 +0100
@@ -1444,6 +1444,99 @@
   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
 by(simp add: finfun_to_list_update)
 
+text {* More type class instantiations *}
+
+lemma card_eq_1_iff: "card A = 1 \<longleftrightarrow> A \<noteq> {} \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  moreover {
+    fix x y
+    assume A: "x \<in> A" "y \<in> A" and neq: "x \<noteq> y"
+    have "finite A" using `?lhs` by(simp add: card_ge_0_finite)
+    from neq have "2 = card {x, y}" by simp
+    also have "\<dots> \<le> card A" using A `finite A`
+      by(auto intro: card_mono)
+    finally have False using `?lhs` by simp }
+  ultimately show ?rhs by auto
+next
+  assume ?rhs
+  hence "A = {THE x. x \<in> A}"
+    by safe (auto intro: theI the_equality[symmetric])
+  also have "card \<dots> = 1" by simp
+  finally show ?lhs .
+qed
+
+lemma card_UNIV_finfun: 
+  defines "F == finfun :: ('a \<Rightarrow> 'b) set"
+  shows "CARD('a \<Rightarrow>f 'b) = (if CARD('a) \<noteq> 0 \<and> CARD('b) \<noteq> 0 \<or> CARD('b) = 1 then CARD('b) ^ CARD('a) else 0)"
+proof(cases "0 < CARD('a) \<and> 0 < CARD('b) \<or> CARD('b) = 1")
+  case True
+  from True have "F = UNIV"
+  proof
+    assume b: "CARD('b) = 1"
+    hence "\<forall>x :: 'b. x = undefined"
+      by(auto simp add: card_eq_1_iff simp del: One_nat_def)
+    thus ?thesis by(auto simp add: finfun_def F_def intro: exI[where x=undefined])
+  qed(auto simp add: finfun_def card_gt_0_iff F_def intro: finite_subset[where B=UNIV])
+  moreover have "CARD('a \<Rightarrow>f 'b) = card F"
+    unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric]
+    by(auto intro!: card_image inj_onI simp add: Abs_finfun_inject F_def)
+  ultimately show ?thesis by(simp add: card_fun)
+next
+  case False
+  hence infinite: "\<not> (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set))"
+    and b: "CARD('b) \<noteq> 1" by(simp_all add: card_eq_0_iff)
+  from b obtain b1 b2 :: 'b where "b1 \<noteq> b2"
+    by(auto simp add: card_eq_1_iff simp del: One_nat_def)
+  let ?f = "\<lambda>a a' :: 'a. if a = a' then b1 else b2"
+  from infinite have "\<not> finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
+  proof(rule contrapos_nn[OF _ conjI])
+    assume finite: "finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
+    hence "finite F"
+      unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric] F_def
+      by(rule finite_imageD)(auto intro: inj_onI simp add: Abs_finfun_inject)
+    hence "finite (range ?f)" 
+      by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def `b1 \<noteq> b2` intro!: exI[where x=b2])
+    thus "finite (UNIV :: 'a set)"
+      by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff `b1 \<noteq> b2` split: split_if_asm)
+    
+    from finite have "finite (range (\<lambda>b. ((K$ b) :: 'a \<Rightarrow>f 'b)))"
+      by(rule finite_subset[rotated 1]) simp
+    thus "finite (UNIV :: 'b set)"
+      by(rule finite_imageD)(auto intro!: inj_onI)
+  qed
+  with False show ?thesis by simp
+qed
+
+lemma finite_UNIV_finfun:
+  "finite (UNIV :: ('a \<Rightarrow>f 'b) set) \<longleftrightarrow>
+  (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1)"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof -
+  have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow>f 'b) > 0" by(simp add: card_gt_0_iff)
+  also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1"
+    by(simp add: card_UNIV_finfun)
+  also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff)
+  finally show ?thesis .
+qed
+
+instantiation finfun :: (finite_UNIV, card_UNIV) finite_UNIV begin
+definition "finite_UNIV = Phantom('a \<Rightarrow>f 'b)
+  (let cb = of_phantom (card_UNIV :: 'b card_UNIV)
+   in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)"
+instance
+  by intro_classes (auto simp add: finite_UNIV_finfun_def Let_def card_UNIV finite_UNIV finite_UNIV_finfun card_gt_0_iff)
+end
+
+instantiation finfun :: (card_UNIV, card_UNIV) card_UNIV begin
+definition "card_UNIV = Phantom('a \<Rightarrow>f 'b)
+  (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
+       cb = of_phantom (card_UNIV :: 'b card_UNIV)
+   in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
+instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
+end
+
 text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
 
 no_type_notation