src/HOL/Library/Fin_Fun.thy
changeset 31380 f25536c0bb80
parent 31379 213299656575
child 31383 ac7abb2e5944
     1.1 --- a/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 15:53:34 2009 +0200
     1.2 +++ b/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 16:23:43 2009 +0200
     1.3 @@ -17,68 +17,12 @@
     1.4    For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
     1.5  *}
     1.6  
     1.7 -subsection {* Auxiliary definitions and lemmas *}
     1.8 -
     1.9 -(*FIXME move these to Finite_Set.thy*)
    1.10 -lemma card_ge_0_finite:
    1.11 -  "card A > 0 \<Longrightarrow> finite A"
    1.12 -by(rule ccontr, drule card_infinite, simp)
    1.13 -
    1.14 -lemma finite_UNIV_card_ge_0:
    1.15 -  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
    1.16 -by(rule ccontr) simp
    1.17 -
    1.18 -lemma card_eq_UNIV_imp_eq_UNIV:
    1.19 -  assumes fin: "finite (UNIV :: 'a set)"
    1.20 -  and card: "card A = card (UNIV :: 'a set)"
    1.21 -  shows "A = (UNIV :: 'a set)"
    1.22 -apply -
    1.23 -  proof
    1.24 -  show "A \<subseteq> UNIV" by simp
    1.25 -  show "UNIV \<subseteq> A"
    1.26 -  proof
    1.27 -    fix x
    1.28 -    show "x \<in> A"
    1.29 -    proof(rule ccontr)
    1.30 -      assume "x \<notin> A"
    1.31 -      hence "A \<subset> UNIV" by auto
    1.32 -      from psubset_card_mono[OF fin this] card show False by simp
    1.33 -    qed
    1.34 -  qed
    1.35 -qed
    1.36 -
    1.37 -lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
    1.38 -  shows "finite (UNIV :: 'b set)"
    1.39 -proof -
    1.40 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
    1.41 -    by(rule finite_imageI)
    1.42 -  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
    1.43 -    by(rule UNIV_eq_I) auto
    1.44 -  ultimately show "finite (UNIV :: 'b set)" by simp
    1.45 -qed
    1.46 -
    1.47 -lemma finite_fun_UNIVD1: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
    1.48 -  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
    1.49 -  shows "finite (UNIV :: 'a set)"
    1.50 -proof -
    1.51 -  from fin have finb: "finite (UNIV :: 'b set)" by(rule finite_fun_UNIVD2)
    1.52 -  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
    1.53 -    by(cases "card (UNIV :: 'b set)")(auto simp add: card_eq_0_iff)
    1.54 -  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - 2" by(auto)
    1.55 -  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by(auto simp add: card_Suc_eq)
    1.56 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by(rule finite_imageI)
    1.57 -  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
    1.58 -  proof(rule UNIV_eq_I)
    1.59 -    fix x :: 'a
    1.60 -    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by(simp add: inv_def)
    1.61 -    thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
    1.62 -  qed
    1.63 -  ultimately show "finite (UNIV :: 'a set)" by simp
    1.64 -qed
    1.65 -
    1.66  (*FIXME move to Map.thy*)
    1.67  lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
    1.68 -by(auto simp add: restrict_map_def intro: ext)
    1.69 +  by (auto simp add: restrict_map_def intro: ext)
    1.70 +
    1.71 +
    1.72 +subsection {* The @{text "map_default"} operation *}
    1.73  
    1.74  definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.75  where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"