instantiate finite_UNIV and card_UNIV for finfun type
authorAndreas Lochbihler
Thu Feb 14 17:58:13 2013 +0100 (2013-02-14)
changeset 511248fd094d5b7b7
parent 51117 47af65ef228e
child 51125 f90874d3a246
instantiate finite_UNIV and card_UNIV for finfun type
src/HOL/Library/FinFun.thy
     1.1 --- a/src/HOL/Library/FinFun.thy	Thu Feb 14 16:01:59 2013 +0100
     1.2 +++ b/src/HOL/Library/FinFun.thy	Thu Feb 14 17:58:13 2013 +0100
     1.3 @@ -1444,6 +1444,99 @@
     1.4    (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
     1.5  by(simp add: finfun_to_list_update)
     1.6  
     1.7 +text {* More type class instantiations *}
     1.8 +
     1.9 +lemma card_eq_1_iff: "card A = 1 \<longleftrightarrow> A \<noteq> {} \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
    1.10 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.11 +proof
    1.12 +  assume ?lhs
    1.13 +  moreover {
    1.14 +    fix x y
    1.15 +    assume A: "x \<in> A" "y \<in> A" and neq: "x \<noteq> y"
    1.16 +    have "finite A" using `?lhs` by(simp add: card_ge_0_finite)
    1.17 +    from neq have "2 = card {x, y}" by simp
    1.18 +    also have "\<dots> \<le> card A" using A `finite A`
    1.19 +      by(auto intro: card_mono)
    1.20 +    finally have False using `?lhs` by simp }
    1.21 +  ultimately show ?rhs by auto
    1.22 +next
    1.23 +  assume ?rhs
    1.24 +  hence "A = {THE x. x \<in> A}"
    1.25 +    by safe (auto intro: theI the_equality[symmetric])
    1.26 +  also have "card \<dots> = 1" by simp
    1.27 +  finally show ?lhs .
    1.28 +qed
    1.29 +
    1.30 +lemma card_UNIV_finfun: 
    1.31 +  defines "F == finfun :: ('a \<Rightarrow> 'b) set"
    1.32 +  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)"
    1.33 +proof(cases "0 < CARD('a) \<and> 0 < CARD('b) \<or> CARD('b) = 1")
    1.34 +  case True
    1.35 +  from True have "F = UNIV"
    1.36 +  proof
    1.37 +    assume b: "CARD('b) = 1"
    1.38 +    hence "\<forall>x :: 'b. x = undefined"
    1.39 +      by(auto simp add: card_eq_1_iff simp del: One_nat_def)
    1.40 +    thus ?thesis by(auto simp add: finfun_def F_def intro: exI[where x=undefined])
    1.41 +  qed(auto simp add: finfun_def card_gt_0_iff F_def intro: finite_subset[where B=UNIV])
    1.42 +  moreover have "CARD('a \<Rightarrow>f 'b) = card F"
    1.43 +    unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric]
    1.44 +    by(auto intro!: card_image inj_onI simp add: Abs_finfun_inject F_def)
    1.45 +  ultimately show ?thesis by(simp add: card_fun)
    1.46 +next
    1.47 +  case False
    1.48 +  hence infinite: "\<not> (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set))"
    1.49 +    and b: "CARD('b) \<noteq> 1" by(simp_all add: card_eq_0_iff)
    1.50 +  from b obtain b1 b2 :: 'b where "b1 \<noteq> b2"
    1.51 +    by(auto simp add: card_eq_1_iff simp del: One_nat_def)
    1.52 +  let ?f = "\<lambda>a a' :: 'a. if a = a' then b1 else b2"
    1.53 +  from infinite have "\<not> finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
    1.54 +  proof(rule contrapos_nn[OF _ conjI])
    1.55 +    assume finite: "finite (UNIV :: ('a \<Rightarrow>f 'b) set)"
    1.56 +    hence "finite F"
    1.57 +      unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric] F_def
    1.58 +      by(rule finite_imageD)(auto intro: inj_onI simp add: Abs_finfun_inject)
    1.59 +    hence "finite (range ?f)" 
    1.60 +      by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def `b1 \<noteq> b2` intro!: exI[where x=b2])
    1.61 +    thus "finite (UNIV :: 'a set)"
    1.62 +      by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff `b1 \<noteq> b2` split: split_if_asm)
    1.63 +    
    1.64 +    from finite have "finite (range (\<lambda>b. ((K$ b) :: 'a \<Rightarrow>f 'b)))"
    1.65 +      by(rule finite_subset[rotated 1]) simp
    1.66 +    thus "finite (UNIV :: 'b set)"
    1.67 +      by(rule finite_imageD)(auto intro!: inj_onI)
    1.68 +  qed
    1.69 +  with False show ?thesis by simp
    1.70 +qed
    1.71 +
    1.72 +lemma finite_UNIV_finfun:
    1.73 +  "finite (UNIV :: ('a \<Rightarrow>f 'b) set) \<longleftrightarrow>
    1.74 +  (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1)"
    1.75 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.76 +proof -
    1.77 +  have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow>f 'b) > 0" by(simp add: card_gt_0_iff)
    1.78 +  also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1"
    1.79 +    by(simp add: card_UNIV_finfun)
    1.80 +  also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff)
    1.81 +  finally show ?thesis .
    1.82 +qed
    1.83 +
    1.84 +instantiation finfun :: (finite_UNIV, card_UNIV) finite_UNIV begin
    1.85 +definition "finite_UNIV = Phantom('a \<Rightarrow>f 'b)
    1.86 +  (let cb = of_phantom (card_UNIV :: 'b card_UNIV)
    1.87 +   in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)"
    1.88 +instance
    1.89 +  by intro_classes (auto simp add: finite_UNIV_finfun_def Let_def card_UNIV finite_UNIV finite_UNIV_finfun card_gt_0_iff)
    1.90 +end
    1.91 +
    1.92 +instantiation finfun :: (card_UNIV, card_UNIV) card_UNIV begin
    1.93 +definition "card_UNIV = Phantom('a \<Rightarrow>f 'b)
    1.94 +  (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
    1.95 +       cb = of_phantom (card_UNIV :: 'b card_UNIV)
    1.96 +   in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
    1.97 +instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
    1.98 +end
    1.99 +
   1.100  text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
   1.101  
   1.102  no_type_notation