1.1 --- a/src/HOL/IsaMakefile Tue May 29 13:46:50 2012 +0200
1.2 +++ b/src/HOL/IsaMakefile Tue May 29 15:31:58 2012 +0200
1.3 @@ -441,7 +441,8 @@
1.4 Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \
1.5 Library/AList.thy Library/AList_Mapping.thy \
1.6 Library/BigO.thy Library/Binomial.thy \
1.7 - Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
1.8 + Library/Bit.thy Library/Boolean_Algebra.thy Library/Card_Univ.thy \
1.9 + Library/Cardinality.thy \
1.10 Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
1.11 Library/Code_Char_ord.thy Library/Code_Integer.thy \
1.12 Library/Code_Nat.thy Library/Code_Natural.thy \
1.13 @@ -453,7 +454,8 @@
1.14 Library/Dlist.thy Library/Eval_Witness.thy \
1.15 Library/DAList.thy Library/Dlist.thy \
1.16 Library/Eval_Witness.thy \
1.17 - Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \
1.18 + Library/Extended_Real.thy Library/Extended_Nat.thy \
1.19 + Library/FinFun.thy Library/Float.thy \
1.20 Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
1.21 Library/FrechetDeriv.thy Library/FuncSet.thy \
1.22 Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \
1.23 @@ -1020,7 +1022,8 @@
1.24 ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \
1.25 ex/Code_Nat_examples.thy \
1.26 ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
1.27 - ex/Eval_Examples.thy ex/Executable_Relation.thy ex/Fundefs.thy \
1.28 + ex/Eval_Examples.thy ex/Executable_Relation.thy \
1.29 + ex/FinFunPred.thy ex/Fundefs.thy \
1.30 ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
1.31 ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
1.32 ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Library/Card_Univ.thy Tue May 29 15:31:58 2012 +0200
2.3 @@ -0,0 +1,293 @@
2.4 +(* Author: Andreas Lochbihler, KIT *)
2.5 +
2.6 +header {* A type class for computing the cardinality of a type's universe *}
2.7 +
2.8 +theory Card_Univ imports Main begin
2.9 +
2.10 +subsection {* A type class for computing the cardinality of a type's universe *}
2.11 +
2.12 +class card_UNIV =
2.13 + fixes card_UNIV :: "'a itself \<Rightarrow> nat"
2.14 + assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
2.15 +begin
2.16 +
2.17 +lemma card_UNIV_neq_0_finite_UNIV:
2.18 + "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
2.19 +by(simp add: card_UNIV card_eq_0_iff)
2.20 +
2.21 +lemma card_UNIV_ge_0_finite_UNIV:
2.22 + "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
2.23 +by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
2.24 +
2.25 +lemma card_UNIV_eq_0_infinite_UNIV:
2.26 + "card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
2.27 +by(simp add: card_UNIV card_eq_0_iff)
2.28 +
2.29 +definition is_list_UNIV :: "'a list \<Rightarrow> bool"
2.30 +where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
2.31 +
2.32 +lemma is_list_UNIV_iff:
2.33 + fixes xs :: "'a list"
2.34 + shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
2.35 +proof
2.36 + assume "is_list_UNIV xs"
2.37 + hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
2.38 + unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
2.39 + from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
2.40 + have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
2.41 + also note set_remdups
2.42 + finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
2.43 +next
2.44 + assume xs: "set xs = UNIV"
2.45 + from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
2.46 + hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
2.47 + moreover have "size (remdups xs) = card (set (remdups xs))"
2.48 + by(subst distinct_card) auto
2.49 + ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
2.50 +qed
2.51 +
2.52 +lemma card_UNIV_eq_0_is_list_UNIV_False:
2.53 + assumes cU0: "card_UNIV x = 0"
2.54 + shows "is_list_UNIV = (\<lambda>xs. False)"
2.55 +proof(rule ext)
2.56 + fix xs :: "'a list"
2.57 + from cU0 have "\<not> finite (UNIV :: 'a set)"
2.58 + by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
2.59 + moreover have "finite (set xs)" by(rule finite_set)
2.60 + ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
2.61 + thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
2.62 +qed
2.63 +
2.64 +end
2.65 +
2.66 +subsection {* Instantiations for @{text "card_UNIV"} *}
2.67 +
2.68 +subsubsection {* @{typ "nat"} *}
2.69 +
2.70 +instantiation nat :: card_UNIV begin
2.71 +
2.72 +definition card_UNIV_nat_def:
2.73 + "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
2.74 +
2.75 +instance proof
2.76 + fix x :: "nat itself"
2.77 + show "card_UNIV x = card (UNIV :: nat set)"
2.78 + unfolding card_UNIV_nat_def by simp
2.79 +qed
2.80 +
2.81 +end
2.82 +
2.83 +subsubsection {* @{typ "int"} *}
2.84 +
2.85 +instantiation int :: card_UNIV begin
2.86 +
2.87 +definition card_UNIV_int_def:
2.88 + "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
2.89 +
2.90 +instance proof
2.91 + fix x :: "int itself"
2.92 + show "card_UNIV x = card (UNIV :: int set)"
2.93 + unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
2.94 +qed
2.95 +
2.96 +end
2.97 +
2.98 +subsubsection {* @{typ "'a list"} *}
2.99 +
2.100 +instantiation list :: (type) card_UNIV begin
2.101 +
2.102 +definition card_UNIV_list_def:
2.103 + "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
2.104 +
2.105 +instance proof
2.106 + fix x :: "'a list itself"
2.107 + show "card_UNIV x = card (UNIV :: 'a list set)"
2.108 + unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
2.109 +qed
2.110 +
2.111 +end
2.112 +
2.113 +subsubsection {* @{typ "unit"} *}
2.114 +
2.115 +lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
2.116 + unfolding UNIV_unit by simp
2.117 +
2.118 +instantiation unit :: card_UNIV begin
2.119 +
2.120 +definition card_UNIV_unit_def:
2.121 + "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
2.122 +
2.123 +instance proof
2.124 + fix x :: "unit itself"
2.125 + show "card_UNIV x = card (UNIV :: unit set)"
2.126 + by(simp add: card_UNIV_unit_def card_UNIV_unit)
2.127 +qed
2.128 +
2.129 +end
2.130 +
2.131 +subsubsection {* @{typ "bool"} *}
2.132 +
2.133 +lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
2.134 + unfolding UNIV_bool by simp
2.135 +
2.136 +instantiation bool :: card_UNIV begin
2.137 +
2.138 +definition card_UNIV_bool_def:
2.139 + "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
2.140 +
2.141 +instance proof
2.142 + fix x :: "bool itself"
2.143 + show "card_UNIV x = card (UNIV :: bool set)"
2.144 + by(simp add: card_UNIV_bool_def card_UNIV_bool)
2.145 +qed
2.146 +
2.147 +end
2.148 +
2.149 +subsubsection {* @{typ "char"} *}
2.150 +
2.151 +lemma card_UNIV_char: "card (UNIV :: char set) = 256"
2.152 +proof -
2.153 + from enum_distinct
2.154 + have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
2.155 + by (rule distinct_card)
2.156 + also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
2.157 + also note enum_chars
2.158 + finally show ?thesis by (simp add: chars_def)
2.159 +qed
2.160 +
2.161 +instantiation char :: card_UNIV begin
2.162 +
2.163 +definition card_UNIV_char_def:
2.164 + "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
2.165 +
2.166 +instance proof
2.167 + fix x :: "char itself"
2.168 + show "card_UNIV x = card (UNIV :: char set)"
2.169 + by(simp add: card_UNIV_char_def card_UNIV_char)
2.170 +qed
2.171 +
2.172 +end
2.173 +
2.174 +subsubsection {* @{typ "'a \<times> 'b"} *}
2.175 +
2.176 +instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
2.177 +
2.178 +definition card_UNIV_product_def:
2.179 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
2.180 +
2.181 +instance proof
2.182 + fix x :: "('a \<times> 'b) itself"
2.183 + show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
2.184 + by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
2.185 +qed
2.186 +
2.187 +end
2.188 +
2.189 +subsubsection {* @{typ "'a + 'b"} *}
2.190 +
2.191 +instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
2.192 +
2.193 +definition card_UNIV_sum_def:
2.194 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
2.195 + in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
2.196 +
2.197 +instance proof
2.198 + fix x :: "('a + 'b) itself"
2.199 + show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
2.200 + by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
2.201 +qed
2.202 +
2.203 +end
2.204 +
2.205 +subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
2.206 +
2.207 +instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
2.208 +
2.209 +definition card_UNIV_fun_def:
2.210 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
2.211 + in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
2.212 +
2.213 +instance proof
2.214 + fix x :: "('a \<Rightarrow> 'b) itself"
2.215 +
2.216 + { assume "0 < card (UNIV :: 'a set)"
2.217 + and "0 < card (UNIV :: 'b set)"
2.218 + hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
2.219 + by(simp_all only: card_ge_0_finite)
2.220 + from finite_distinct_list[OF finb] obtain bs
2.221 + where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
2.222 + from finite_distinct_list[OF fina] obtain as
2.223 + where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
2.224 + have cb: "card (UNIV :: 'b set) = length bs"
2.225 + unfolding bs[symmetric] distinct_card[OF distb] ..
2.226 + have ca: "card (UNIV :: 'a set) = length as"
2.227 + unfolding as[symmetric] distinct_card[OF dista] ..
2.228 + let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
2.229 + have "UNIV = set ?xs"
2.230 + proof(rule UNIV_eq_I)
2.231 + fix f :: "'a \<Rightarrow> 'b"
2.232 + from as have "f = the \<circ> map_of (zip as (map f as))"
2.233 + by(auto simp add: map_of_zip_map intro: ext)
2.234 + thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
2.235 + qed
2.236 + moreover have "distinct ?xs" unfolding distinct_map
2.237 + proof(intro conjI distinct_n_lists distb inj_onI)
2.238 + fix xs ys :: "'b list"
2.239 + assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
2.240 + and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
2.241 + and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
2.242 + from xs ys have [simp]: "length xs = length as" "length ys = length as"
2.243 + by(simp_all add: length_n_lists_elem)
2.244 + have "map_of (zip as xs) = map_of (zip as ys)"
2.245 + proof
2.246 + fix x
2.247 + from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
2.248 + by(simp_all add: map_of_zip_is_Some[symmetric])
2.249 + with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
2.250 + by(auto dest: fun_cong[where x=x])
2.251 + qed
2.252 + with dista show "xs = ys" by(simp add: map_of_zip_inject)
2.253 + qed
2.254 + hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
2.255 + moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
2.256 + ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
2.257 + using cb ca by simp }
2.258 + moreover {
2.259 + assume cb: "card (UNIV :: 'b set) = Suc 0"
2.260 + then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
2.261 + have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
2.262 + proof(rule UNIV_eq_I)
2.263 + fix x :: "'a \<Rightarrow> 'b"
2.264 + { fix y
2.265 + have "x y \<in> UNIV" ..
2.266 + hence "x y = b" unfolding b by simp }
2.267 + thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
2.268 + qed
2.269 + have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
2.270 + ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
2.271 + unfolding card_UNIV_fun_def card_UNIV Let_def
2.272 + by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
2.273 +qed
2.274 +
2.275 +end
2.276 +
2.277 +subsubsection {* @{typ "'a option"} *}
2.278 +
2.279 +instantiation option :: (card_UNIV) card_UNIV
2.280 +begin
2.281 +
2.282 +definition card_UNIV_option_def:
2.283 + "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
2.284 + in if c \<noteq> 0 then Suc c else 0)"
2.285 +
2.286 +instance proof
2.287 + fix x :: "'a option itself"
2.288 + show "card_UNIV x = card (UNIV :: 'a option set)"
2.289 + unfolding UNIV_option_conv
2.290 + by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
2.291 + (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
2.292 +qed
2.293 +
2.294 +end
2.295 +
2.296 +end
2.297 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Library/FinFun.thy Tue May 29 15:31:58 2012 +0200
3.3 @@ -0,0 +1,1473 @@
3.4 +(* Author: Andreas Lochbihler, Uni Karlsruhe *)
3.5 +
3.6 +header {* Almost everywhere constant functions *}
3.7 +
3.8 +theory FinFun
3.9 +imports Card_Univ
3.10 +begin
3.11 +
3.12 +text {*
3.13 + This theory defines functions which are constant except for finitely
3.14 + many points (FinFun) and introduces a type finfin along with a
3.15 + number of operators for them. The code generator is set up such that
3.16 + such functions can be represented as data in the generated code and
3.17 + all operators are executable.
3.18 +
3.19 + For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
3.20 +*}
3.21 +
3.22 +
3.23 +definition "code_abort" :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a"
3.24 +where [simp, code del]: "code_abort f = f ()"
3.25 +
3.26 +code_abort "code_abort"
3.27 +
3.28 +hide_const (open) "code_abort"
3.29 +
3.30 +subsection {* The @{text "map_default"} operation *}
3.31 +
3.32 +definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
3.33 +where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
3.34 +
3.35 +lemma map_default_delete [simp]:
3.36 + "map_default b (f(a := None)) = (map_default b f)(a := b)"
3.37 +by(simp add: map_default_def fun_eq_iff)
3.38 +
3.39 +lemma map_default_insert:
3.40 + "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
3.41 +by(simp add: map_default_def fun_eq_iff)
3.42 +
3.43 +lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
3.44 +by(simp add: fun_eq_iff map_default_def)
3.45 +
3.46 +lemma map_default_inject:
3.47 + fixes g g' :: "'a \<rightharpoonup> 'b"
3.48 + assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
3.49 + and fin: "finite (dom g)" and b: "b \<notin> ran g"
3.50 + and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
3.51 + and eq': "map_default b g = map_default b' g'"
3.52 + shows "b = b'" "g = g'"
3.53 +proof -
3.54 + from infin_eq show bb': "b = b'"
3.55 + proof
3.56 + assume infin: "\<not> finite (UNIV :: 'a set)"
3.57 + from fin fin' have "finite (dom g \<union> dom g')" by auto
3.58 + with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
3.59 + then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
3.60 + hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
3.61 + with eq' show "b = b'" by simp
3.62 + qed
3.63 +
3.64 + show "g = g'"
3.65 + proof
3.66 + fix x
3.67 + show "g x = g' x"
3.68 + proof(cases "g x")
3.69 + case None
3.70 + hence "map_default b g x = b" by(simp add: map_default_def)
3.71 + with bb' eq' have "map_default b' g' x = b'" by simp
3.72 + with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
3.73 + with None show ?thesis by simp
3.74 + next
3.75 + case (Some c)
3.76 + with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
3.77 + moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
3.78 + with eq' have "map_default b' g' x = c" by simp
3.79 + ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
3.80 + with Some show ?thesis by simp
3.81 + qed
3.82 + qed
3.83 +qed
3.84 +
3.85 +subsection {* The finfun type *}
3.86 +
3.87 +definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
3.88 +
3.89 +typedef (open) ('a,'b) finfun ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
3.90 +proof -
3.91 + have "\<exists>f. finite {x. f x \<noteq> undefined}"
3.92 + proof
3.93 + show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
3.94 + qed
3.95 + then show ?thesis unfolding finfun_def by auto
3.96 +qed
3.97 +
3.98 +setup_lifting type_definition_finfun
3.99 +
3.100 +lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
3.101 +proof -
3.102 + { fix b'
3.103 + have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
3.104 + proof(cases "b = b'")
3.105 + case True
3.106 + hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
3.107 + thus ?thesis by simp
3.108 + next
3.109 + case False
3.110 + hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
3.111 + thus ?thesis by simp
3.112 + qed }
3.113 + thus ?thesis unfolding finfun_def by blast
3.114 +qed
3.115 +
3.116 +lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
3.117 +by(auto simp add: finfun_def)
3.118 +
3.119 +lemma finfun_left_compose:
3.120 + assumes "y \<in> finfun"
3.121 + shows "g \<circ> y \<in> finfun"
3.122 +proof -
3.123 + from assms obtain b where "finite {a. y a \<noteq> b}"
3.124 + unfolding finfun_def by blast
3.125 + hence "finite {c. g (y c) \<noteq> g b}"
3.126 + proof(induct "{a. y a \<noteq> b}" arbitrary: y)
3.127 + case empty
3.128 + hence "y = (\<lambda>a. b)" by(auto intro: ext)
3.129 + thus ?case by(simp)
3.130 + next
3.131 + case (insert x F)
3.132 + note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
3.133 + from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
3.134 + have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
3.135 + show ?case
3.136 + proof(cases "g (y x) = g b")
3.137 + case True
3.138 + hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
3.139 + with IH[OF F] show ?thesis by simp
3.140 + next
3.141 + case False
3.142 + hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
3.143 + with IH[OF F] show ?thesis by(simp)
3.144 + qed
3.145 + qed
3.146 + thus ?thesis unfolding finfun_def by auto
3.147 +qed
3.148 +
3.149 +lemma assumes "y \<in> finfun"
3.150 + shows fst_finfun: "fst \<circ> y \<in> finfun"
3.151 + and snd_finfun: "snd \<circ> y \<in> finfun"
3.152 +proof -
3.153 + from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
3.154 + unfolding finfun_def by auto
3.155 + have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
3.156 + and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
3.157 + hence "finite {a. fst (y a) \<noteq> b}"
3.158 + and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
3.159 + thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
3.160 + unfolding finfun_def by auto
3.161 +qed
3.162 +
3.163 +lemma map_of_finfun: "map_of xs \<in> finfun"
3.164 +unfolding finfun_def
3.165 +by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
3.166 +
3.167 +lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
3.168 +by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
3.169 +
3.170 +lemma finfun_right_compose:
3.171 + assumes g: "g \<in> finfun" and inj: "inj f"
3.172 + shows "g o f \<in> finfun"
3.173 +proof -
3.174 + from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
3.175 + moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
3.176 + moreover from inj have "inj_on f {a. g (f a) \<noteq> b}" by(rule subset_inj_on) blast
3.177 + ultimately have "finite {a. g (f a) \<noteq> b}"
3.178 + by(blast intro: finite_imageD[where f=f] finite_subset)
3.179 + thus ?thesis unfolding finfun_def by auto
3.180 +qed
3.181 +
3.182 +lemma finfun_curry:
3.183 + assumes fin: "f \<in> finfun"
3.184 + shows "curry f \<in> finfun" "curry f a \<in> finfun"
3.185 +proof -
3.186 + from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
3.187 + moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
3.188 + hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
3.189 + by(auto simp add: curry_def fun_eq_iff)
3.190 + ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
3.191 + thus "curry f \<in> finfun" unfolding finfun_def by blast
3.192 +
3.193 + have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
3.194 + hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
3.195 + hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
3.196 + thus "curry f a \<in> finfun" unfolding finfun_def by auto
3.197 +qed
3.198 +
3.199 +lemmas finfun_simp =
3.200 + fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
3.201 +lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
3.202 +lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
3.203 +
3.204 +lemma Abs_finfun_inject_finite:
3.205 + fixes x y :: "'a \<Rightarrow> 'b"
3.206 + assumes fin: "finite (UNIV :: 'a set)"
3.207 + shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
3.208 +proof
3.209 + assume "Abs_finfun x = Abs_finfun y"
3.210 + moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
3.211 + by(auto intro: finite_subset[OF _ fin])
3.212 + ultimately show "x = y" by(simp add: Abs_finfun_inject)
3.213 +qed simp
3.214 +
3.215 +lemma Abs_finfun_inject_finite_class:
3.216 + fixes x y :: "('a :: finite) \<Rightarrow> 'b"
3.217 + shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
3.218 +using finite_UNIV
3.219 +by(simp add: Abs_finfun_inject_finite)
3.220 +
3.221 +lemma Abs_finfun_inj_finite:
3.222 + assumes fin: "finite (UNIV :: 'a set)"
3.223 + shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
3.224 +proof(rule inj_onI)
3.225 + fix x y :: "'a \<Rightarrow> 'b"
3.226 + assume "Abs_finfun x = Abs_finfun y"
3.227 + moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
3.228 + by(auto intro: finite_subset[OF _ fin])
3.229 + ultimately show "x = y" by(simp add: Abs_finfun_inject)
3.230 +qed
3.231 +
3.232 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.233 +
3.234 +lemma Abs_finfun_inverse_finite:
3.235 + fixes x :: "'a \<Rightarrow> 'b"
3.236 + assumes fin: "finite (UNIV :: 'a set)"
3.237 + shows "Rep_finfun (Abs_finfun x) = x"
3.238 +proof -
3.239 + from fin have "x \<in> finfun"
3.240 + by(auto simp add: finfun_def intro: finite_subset)
3.241 + thus ?thesis by simp
3.242 +qed
3.243 +
3.244 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.245 +
3.246 +lemma Abs_finfun_inverse_finite_class:
3.247 + fixes x :: "('a :: finite) \<Rightarrow> 'b"
3.248 + shows "Rep_finfun (Abs_finfun x) = x"
3.249 +using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
3.250 +
3.251 +lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
3.252 +unfolding finfun_def by(auto intro: finite_subset)
3.253 +
3.254 +lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
3.255 +by(simp add: finfun_eq_finite_UNIV)
3.256 +
3.257 +lemma map_default_in_finfun:
3.258 + assumes fin: "finite (dom f)"
3.259 + shows "map_default b f \<in> finfun"
3.260 +unfolding finfun_def
3.261 +proof(intro CollectI exI)
3.262 + from fin show "finite {a. map_default b f a \<noteq> b}"
3.263 + by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
3.264 +qed
3.265 +
3.266 +lemma finfun_cases_map_default:
3.267 + obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
3.268 +proof -
3.269 + obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
3.270 + from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
3.271 + let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
3.272 + have "map_default b ?g = y" by(simp add: fun_eq_iff map_default_def)
3.273 + with f have "f = Abs_finfun (map_default b ?g)" by simp
3.274 + moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
3.275 + moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
3.276 + ultimately show ?thesis by(rule that)
3.277 +qed
3.278 +
3.279 +
3.280 +subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
3.281 +
3.282 +lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
3.283 +is "\<lambda> b x. b" by (rule const_finfun)
3.284 +
3.285 +lift_definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd" by (simp add: fun_upd_finfun)
3.286 +
3.287 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.288 +
3.289 +lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(\<^sup>f a := b)(\<^sup>f a' := b') = f(\<^sup>f a' := b')(\<^sup>f a := b)"
3.290 +by transfer (simp add: fun_upd_twist)
3.291 +
3.292 +lemma finfun_update_twice [simp]:
3.293 + "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
3.294 +by transfer simp
3.295 +
3.296 +lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
3.297 +by transfer (simp add: fun_eq_iff)
3.298 +
3.299 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.300 +
3.301 +subsection {* Code generator setup *}
3.302 +
3.303 +definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
3.304 +where [simp, code del]: "finfun_update_code = finfun_update"
3.305 +
3.306 +code_datatype finfun_const finfun_update_code
3.307 +
3.308 +lemma finfun_update_const_code [code]:
3.309 + "(\<lambda>\<^isup>f b)(\<^sup>f a := b') = (if b = b' then (\<lambda>\<^isup>f b) else finfun_update_code (\<lambda>\<^isup>f b) a b')"
3.310 +by(simp add: finfun_update_const_same)
3.311 +
3.312 +lemma finfun_update_update_code [code]:
3.313 + "(finfun_update_code f a b)(\<^sup>f a' := b') = (if a = a' then f(\<^sup>f a := b') else finfun_update_code (f(\<^sup>f a' := b')) a b)"
3.314 +by(simp add: finfun_update_twist)
3.315 +
3.316 +
3.317 +subsection {* Setup for quickcheck *}
3.318 +
3.319 +quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b => 'a \<Rightarrow>\<^isub>f 'b"
3.320 +
3.321 +subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
3.322 +
3.323 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.324 +
3.325 +interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
3.326 +proof
3.327 + fix a a' :: 'a
3.328 + show "(\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b')) = (\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))"
3.329 + proof
3.330 + fix b
3.331 + have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
3.332 + by(cases "a = a'")(auto simp add: fun_upd_twist)
3.333 + then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
3.334 + by(auto simp add: finfun_update_def fun_upd_twist)
3.335 + then show "((\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b'))) b = ((\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))) b"
3.336 + by (simp add: fun_eq_iff)
3.337 + qed
3.338 +qed
3.339 +
3.340 +lemma fold_finfun_update_finite_univ:
3.341 + assumes fin: "finite (UNIV :: 'a set)"
3.342 + shows "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
3.343 +proof -
3.344 + { fix A :: "'a set"
3.345 + from fin have "finite A" by(auto intro: finite_subset)
3.346 + hence "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)"
3.347 + proof(induct)
3.348 + case (insert x F)
3.349 + have "(\<lambda>a. if a = x then b' else (if a \<in> F then b' else b)) = (\<lambda>a. if a = x \<or> a \<in> F then b' else b)"
3.350 + by(auto intro: ext)
3.351 + with insert show ?case
3.352 + by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
3.353 + qed(simp add: finfun_const_def) }
3.354 + thus ?thesis by(simp add: finfun_const_def)
3.355 +qed
3.356 +
3.357 +
3.358 +subsection {* Default value for FinFuns *}
3.359 +
3.360 +definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
3.361 +where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
3.362 +
3.363 +lemma finfun_default_aux_infinite:
3.364 + fixes f :: "'a \<Rightarrow> 'b"
3.365 + assumes infin: "\<not> finite (UNIV :: 'a set)"
3.366 + and fin: "finite {a. f a \<noteq> b}"
3.367 + shows "finfun_default_aux f = b"
3.368 +proof -
3.369 + let ?B = "{a. f a \<noteq> b}"
3.370 + from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
3.371 + proof(rule the_equality)
3.372 + fix b'
3.373 + assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
3.374 + with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
3.375 + then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
3.376 + thus "b' = b" by auto
3.377 + qed
3.378 + thus ?thesis using infin by(simp add: finfun_default_aux_def)
3.379 +qed
3.380 +
3.381 +
3.382 +lemma finite_finfun_default_aux:
3.383 + fixes f :: "'a \<Rightarrow> 'b"
3.384 + assumes fin: "f \<in> finfun"
3.385 + shows "finite {a. f a \<noteq> finfun_default_aux f}"
3.386 +proof(cases "finite (UNIV :: 'a set)")
3.387 + case True thus ?thesis using fin
3.388 + by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
3.389 +next
3.390 + case False
3.391 + from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
3.392 + unfolding finfun_def by blast
3.393 + with False show ?thesis by(simp add: finfun_default_aux_infinite)
3.394 +qed
3.395 +
3.396 +lemma finfun_default_aux_update_const:
3.397 + fixes f :: "'a \<Rightarrow> 'b"
3.398 + assumes fin: "f \<in> finfun"
3.399 + shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
3.400 +proof(cases "finite (UNIV :: 'a set)")
3.401 + case False
3.402 + from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
3.403 + hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
3.404 + proof(cases "b = b' \<and> f a \<noteq> b'")
3.405 + case True
3.406 + hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
3.407 + thus ?thesis using b' by simp
3.408 + next
3.409 + case False
3.410 + moreover
3.411 + { assume "b \<noteq> b'"
3.412 + hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
3.413 + hence ?thesis using b' by simp }
3.414 + moreover
3.415 + { assume "b = b'" "f a = b'"
3.416 + hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
3.417 + hence ?thesis using b' by simp }
3.418 + ultimately show ?thesis by blast
3.419 + qed
3.420 + with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
3.421 +next
3.422 + case True thus ?thesis by(simp add: finfun_default_aux_def)
3.423 +qed
3.424 +
3.425 +lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
3.426 +is "finfun_default_aux" ..
3.427 +
3.428 +lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
3.429 +apply transfer apply (erule finite_finfun_default_aux)
3.430 +unfolding Rel_def fun_rel_def cr_finfun_def by simp
3.431 +
3.432 +lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
3.433 +apply(transfer)
3.434 +apply(auto simp add: finfun_default_aux_infinite)
3.435 +apply(simp add: finfun_default_aux_def)
3.436 +done
3.437 +
3.438 +lemma finfun_default_update_const:
3.439 + "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
3.440 +by transfer (simp add: finfun_default_aux_update_const)
3.441 +
3.442 +lemma finfun_default_const_code [code]:
3.443 + "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
3.444 +by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
3.445 +
3.446 +lemma finfun_default_update_code [code]:
3.447 + "finfun_default (finfun_update_code f a b) = finfun_default f"
3.448 +by(simp add: finfun_default_update_const)
3.449 +
3.450 +subsection {* Recursion combinator and well-formedness conditions *}
3.451 +
3.452 +definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
3.453 +where [code del]:
3.454 + "finfun_rec cnst upd f \<equiv>
3.455 + let b = finfun_default f;
3.456 + g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
3.457 + in Finite_Set.fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
3.458 +
3.459 +locale finfun_rec_wf_aux =
3.460 + fixes cnst :: "'b \<Rightarrow> 'c"
3.461 + and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
3.462 + assumes upd_const_same: "upd a b (cnst b) = cnst b"
3.463 + and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
3.464 + and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
3.465 +begin
3.466 +
3.467 +
3.468 +lemma upd_left_comm: "comp_fun_commute (\<lambda>a. upd a (f a))"
3.469 +by(unfold_locales)(auto intro: upd_commute simp add: fun_eq_iff)
3.470 +
3.471 +lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
3.472 +by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
3.473 +
3.474 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.475 +
3.476 +lemma map_default_update_const:
3.477 + assumes fin: "finite (dom f)"
3.478 + and anf: "a \<notin> dom f"
3.479 + and fg: "f \<subseteq>\<^sub>m g"
3.480 + shows "upd a d (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
3.481 + Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
3.482 +proof -
3.483 + let ?upd = "\<lambda>a. upd a (map_default d g a)"
3.484 + let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
3.485 + interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
3.486 +
3.487 + from fin anf fg show ?thesis
3.488 + proof(induct "dom f" arbitrary: f)
3.489 + case empty
3.490 + from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
3.491 + thus ?case by(simp add: finfun_const_def upd_const_same)
3.492 + next
3.493 + case (insert a' A)
3.494 + note IH = `\<And>f. \<lbrakk> A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g \<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)`
3.495 + note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
3.496 + note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
3.497 +
3.498 + from domf obtain b where b: "f a' = Some b" by auto
3.499 + let ?f' = "f(a' := None)"
3.500 + have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
3.501 + by(subst gwf.fold_insert[OF fin a'nA]) rule
3.502 + also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
3.503 + hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
3.504 + also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
3.505 + also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def)
3.506 + note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
3.507 + also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
3.508 + unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
3.509 + also have "insert a' (dom ?f') = dom f" using domf by auto
3.510 + finally show ?case .
3.511 + qed
3.512 +qed
3.513 +
3.514 +lemma map_default_update_twice:
3.515 + assumes fin: "finite (dom f)"
3.516 + and anf: "a \<notin> dom f"
3.517 + and fg: "f \<subseteq>\<^sub>m g"
3.518 + shows "upd a d'' (upd a d' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
3.519 + upd a d'' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
3.520 +proof -
3.521 + let ?upd = "\<lambda>a. upd a (map_default d g a)"
3.522 + let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
3.523 + interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
3.524 +
3.525 + from fin anf fg show ?thesis
3.526 + proof(induct "dom f" arbitrary: f)
3.527 + case empty
3.528 + from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
3.529 + thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
3.530 + next
3.531 + case (insert a' A)
3.532 + note IH = `\<And>f. \<lbrakk>A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))`
3.533 + note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
3.534 + note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
3.535 +
3.536 + from domf obtain b where b: "f a' = Some b" by auto
3.537 + let ?f' = "f(a' := None)"
3.538 + let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
3.539 + from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
3.540 + also note gwf.fold_insert[OF fin a'nA]
3.541 + also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
3.542 + hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
3.543 + also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
3.544 + also note upd_commute[OF ana']
3.545 + also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def)
3.546 + note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
3.547 + also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
3.548 + also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
3.549 + finally show ?case .
3.550 + qed
3.551 +qed
3.552 +
3.553 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.554 +
3.555 +lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
3.556 +by(auto simp add: map_default_def restrict_map_def intro: ext)
3.557 +
3.558 +lemma finite_rec_cong1:
3.559 + assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
3.560 + and fin: "finite A"
3.561 + and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
3.562 + shows "Finite_Set.fold f z A = Finite_Set.fold g z A"
3.563 +proof -
3.564 + interpret f: comp_fun_commute f by(rule f)
3.565 + interpret g: comp_fun_commute g by(rule g)
3.566 + { fix B
3.567 + assume BsubA: "B \<subseteq> A"
3.568 + with fin have "finite B" by(blast intro: finite_subset)
3.569 + hence "B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B"
3.570 + proof(induct)
3.571 + case empty thus ?case by simp
3.572 + next
3.573 + case (insert a B)
3.574 + note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
3.575 + note IH = `B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B`
3.576 + from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
3.577 + from IH[OF BsubA] eq[OF aA] finB anB
3.578 + show ?case by(auto)
3.579 + qed
3.580 + with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast }
3.581 + thus ?thesis by blast
3.582 +qed
3.583 +
3.584 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.585 +
3.586 +lemma finfun_rec_upd [simp]:
3.587 + "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
3.588 +proof -
3.589 + obtain b where b: "b = finfun_default f" by auto
3.590 + let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
3.591 + obtain g where g: "g = The (?the f)" by blast
3.592 + obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
3.593 + from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
3.594 +
3.595 + let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
3.596 + from bfin have fing: "finite (dom ?g)" by auto
3.597 + have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
3.598 + have yg: "y = map_default b ?g" by simp
3.599 + have gg: "g = ?g" unfolding g
3.600 + proof(rule the_equality)
3.601 + from f y bfin show "?the f ?g"
3.602 + by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
3.603 + next
3.604 + fix g'
3.605 + assume "?the f g'"
3.606 + hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
3.607 + and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
3.608 + from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
3.609 + with eq have "map_default b ?g = map_default b g'" by simp
3.610 + with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
3.611 + qed
3.612 +
3.613 + show ?thesis
3.614 + proof(cases "b' = b")
3.615 + case True
3.616 + note b'b = True
3.617 +
3.618 + let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
3.619 + from bfin b'b have fing': "finite (dom ?g')"
3.620 + by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
3.621 + have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
3.622 +
3.623 + let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
3.624 + let ?b = "map_default b ?g"
3.625 + from upd_left_comm upd_left_comm fing'
3.626 + have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
3.627 + by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
3.628 + also interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
3.629 + have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
3.630 + proof(cases "y a' = b")
3.631 + case True
3.632 + with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
3.633 + from True have a'ndomg: "a' \<notin> dom ?g" by auto
3.634 + from f b'b b show ?thesis unfolding g'
3.635 + by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
3.636 + next
3.637 + case False
3.638 + hence domg: "dom ?g = insert a' (dom ?g')" by auto
3.639 + from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
3.640 + have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) =
3.641 + upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
3.642 + using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
3.643 + hence "upd a' b (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
3.644 + upd a' b (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
3.645 + also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
3.646 + note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
3.647 + also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
3.648 + finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
3.649 + qed
3.650 + also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
3.651 + proof(rule the_equality)
3.652 + from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
3.653 + by(auto simp del: fun_upd_apply simp add: finfun_update_def)
3.654 + next
3.655 + fix g'
3.656 + assume "?the (f(\<^sup>f a' := b')) g'"
3.657 + hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
3.658 + and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
3.659 + by(auto simp del: fun_upd_apply)
3.660 + from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
3.661 + by(blast intro: map_default_in_finfun)+
3.662 + with eq f b'b b have "map_default b ?g' = map_default b g'"
3.663 + by(simp del: fun_upd_apply add: finfun_update_def)
3.664 + with fing' brang' fin' ran' show "g' = ?g'"
3.665 + by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
3.666 + qed
3.667 + ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
3.668 + by(simp only: finfun_default_update_const map_default_def)
3.669 + next
3.670 + case False
3.671 + note b'b = this
3.672 + let ?g' = "?g(a' \<mapsto> b')"
3.673 + let ?b' = "map_default b ?g'"
3.674 + let ?b = "map_default b ?g"
3.675 + from fing have fing': "finite (dom ?g')" by auto
3.676 + from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
3.677 + have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
3.678 + with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
3.679 + have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
3.680 + proof (rule the_equality)
3.681 + from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
3.682 + next
3.683 + fix g' assume "?the (f(\<^sup>f a' := b')) g'"
3.684 + hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
3.685 + and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
3.686 + from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
3.687 + by(auto intro: map_default_in_finfun)
3.688 + with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
3.689 + with fin' brang' fing' bnrang' show "g' = ?g'"
3.690 + by(rule map_default_inject[OF disjI2[OF refl]])
3.691 + qed
3.692 + have dom: "dom (((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b})(a' \<mapsto> b')) = insert a' (dom ((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}))"
3.693 + by auto
3.694 + show ?thesis
3.695 + proof(cases "y a' = b")
3.696 + case True
3.697 + hence a'ndomg: "a' \<notin> dom ?g" by auto
3.698 + from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
3.699 + by(auto simp add: restrict_map_def map_default_def intro!: ext)
3.700 + hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
3.701 + interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
3.702 + from upd_left_comm upd_left_comm fing
3.703 + have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
3.704 + by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
3.705 + thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
3.706 + unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
3.707 + by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
3.708 + next
3.709 + case False
3.710 + hence "insert a' (dom ?g) = dom ?g" by auto
3.711 + moreover {
3.712 + let ?g'' = "?g(a' := None)"
3.713 + let ?b'' = "map_default b ?g''"
3.714 + from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
3.715 + from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
3.716 + have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
3.717 + have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
3.718 + interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
3.719 + interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
3.720 + have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
3.721 + upd a' b' (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
3.722 + unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
3.723 + also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
3.724 + have "dom (?g |` dom ?g'') = dom ?g''" by auto
3.725 + note map_default_update_twice[where d=b and f = "?g |` dom ?g''" and a=a' and d'="?b a'" and d''=b' and g="?g",
3.726 + unfolded this, OF fing'' a'ndomg'' g''leg]
3.727 + also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
3.728 + from upd_left_comm upd_left_comm fing''
3.729 + have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
3.730 + by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
3.731 + with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
3.732 + upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
3.733 + also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
3.734 + finally have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
3.735 + Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
3.736 + unfolding domg . }
3.737 + ultimately have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
3.738 + upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
3.739 + thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
3.740 + using b'b gg by(simp add: map_default_insert)
3.741 + qed
3.742 + qed
3.743 +qed
3.744 +
3.745 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.746 +
3.747 +end
3.748 +
3.749 +locale finfun_rec_wf = finfun_rec_wf_aux +
3.750 + assumes const_update_all:
3.751 + "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
3.752 +begin
3.753 +
3.754 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.755 +
3.756 +lemma finfun_rec_const [simp]:
3.757 + "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
3.758 +proof(cases "finite (UNIV :: 'a set)")
3.759 + case False
3.760 + hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
3.761 + moreover have "(THE g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
3.762 + proof (rule the_equality)
3.763 + show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
3.764 + by(auto simp add: finfun_const_def)
3.765 + next
3.766 + fix g :: "'a \<rightharpoonup> 'b"
3.767 + assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
3.768 + hence g: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
3.769 + from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
3.770 + by(simp add: finfun_const_def)
3.771 + moreover have "map_default c empty = (\<lambda>a. c)" by simp
3.772 + ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
3.773 + qed
3.774 + ultimately show ?thesis by(simp add: finfun_rec_def)
3.775 +next
3.776 + case True
3.777 + hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const)
3.778 + let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
3.779 + show ?thesis
3.780 + proof(cases "c = undefined")
3.781 + case True
3.782 + have the: "The ?the = empty"
3.783 + proof (rule the_equality)
3.784 + from True show "?the empty" by(auto simp add: finfun_const_def)
3.785 + next
3.786 + fix g'
3.787 + assume "?the g'"
3.788 + hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
3.789 + and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
3.790 + from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
3.791 + with fg have "map_default undefined g' = (\<lambda>a. c)"
3.792 + by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
3.793 + with True show "g' = empty"
3.794 + by -(rule map_default_inject(2)[OF _ fin g], auto)
3.795 + qed
3.796 + show ?thesis unfolding finfun_rec_def using `finite UNIV` True
3.797 + unfolding Let_def the default by(simp)
3.798 + next
3.799 + case False
3.800 + have the: "The ?the = (\<lambda>a :: 'a. Some c)"
3.801 + proof (rule the_equality)
3.802 + from False True show "?the (\<lambda>a :: 'a. Some c)"
3.803 + by(auto simp add: map_default_def [abs_def] finfun_const_def dom_def ran_def)
3.804 + next
3.805 + fix g' :: "'a \<rightharpoonup> 'b"
3.806 + assume "?the g'"
3.807 + hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
3.808 + and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
3.809 + from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
3.810 + with fg have "map_default undefined g' = (\<lambda>a. c)"
3.811 + by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
3.812 + with True False show "g' = (\<lambda>a::'a. Some c)"
3.813 + by - (rule map_default_inject(2)[OF _ fin g],
3.814 + auto simp add: dom_def ran_def map_default_def [abs_def])
3.815 + qed
3.816 + show ?thesis unfolding finfun_rec_def using True False
3.817 + unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
3.818 + qed
3.819 +qed
3.820 +
3.821 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.822 +
3.823 +end
3.824 +
3.825 +subsection {* Weak induction rule and case analysis for FinFuns *}
3.826 +
3.827 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.828 +
3.829 +lemma finfun_weak_induct [consumes 0, case_names const update]:
3.830 + assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
3.831 + and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
3.832 + shows "P x"
3.833 +proof(induct x rule: Abs_finfun_induct)
3.834 + case (Abs_finfun y)
3.835 + then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
3.836 + thus ?case using `y \<in> finfun`
3.837 + proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
3.838 + case empty
3.839 + hence "\<And>a. y a = b" by blast
3.840 + hence "y = (\<lambda>a. b)" by(auto intro: ext)
3.841 + hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
3.842 + thus ?case by(simp add: const)
3.843 + next
3.844 + case (insert a A)
3.845 + note IH = `\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
3.846 + note y = `y \<in> finfun`
3.847 + with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
3.848 + have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto
3.849 + from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
3.850 + thus ?case using y unfolding finfun_update_def by simp
3.851 + qed
3.852 +qed
3.853 +
3.854 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.855 +
3.856 +lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
3.857 +by(induct x rule: finfun_weak_induct) blast+
3.858 +
3.859 +lemma finfun_exhaust:
3.860 + obtains b where "x = (\<lambda>\<^isup>f b)"
3.861 + | f a b where "x = f(\<^sup>f a := b)"
3.862 +by(atomize_elim)(rule finfun_exhaust_disj)
3.863 +
3.864 +lemma finfun_rec_unique:
3.865 + fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
3.866 + assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
3.867 + and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
3.868 + and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
3.869 + and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
3.870 + shows "f = f'"
3.871 +proof
3.872 + fix g :: "'a \<Rightarrow>\<^isub>f 'b"
3.873 + show "f g = f' g"
3.874 + by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
3.875 +qed
3.876 +
3.877 +
3.878 +subsection {* Function application *}
3.879 +
3.880 +definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
3.881 +where [code del]: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
3.882 +
3.883 +interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
3.884 +by(unfold_locales) auto
3.885 +
3.886 +interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
3.887 +proof(unfold_locales)
3.888 + fix b' b :: 'a
3.889 + assume fin: "finite (UNIV :: 'b set)"
3.890 + { fix A :: "'b set"
3.891 + interpret comp_fun_commute "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
3.892 + from fin have "finite A" by(auto intro: finite_subset)
3.893 + hence "Finite_Set.fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
3.894 + by induct auto }
3.895 + from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
3.896 +qed
3.897 +
3.898 +lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
3.899 +by(simp add: finfun_apply_def)
3.900 +
3.901 +lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
3.902 + and finfun_upd_apply_code [code]: "(finfun_update_code f a b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
3.903 +by(simp_all add: finfun_apply_def)
3.904 +
3.905 +lemma finfun_upd_apply_same [simp]:
3.906 + "f(\<^sup>fa := b)\<^sub>f a = b"
3.907 +by(simp add: finfun_upd_apply)
3.908 +
3.909 +lemma finfun_upd_apply_other [simp]:
3.910 + "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
3.911 +by(simp add: finfun_upd_apply)
3.912 +
3.913 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.914 +
3.915 +lemma finfun_apply_Rep_finfun:
3.916 + "finfun_apply = Rep_finfun"
3.917 +proof(rule finfun_rec_unique)
3.918 + fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
3.919 +next
3.920 + fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)"
3.921 + by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
3.922 +qed(auto intro: ext)
3.923 +
3.924 +lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
3.925 +by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
3.926 +
3.927 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.928 +
3.929 +lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
3.930 +by(auto intro: finfun_ext)
3.931 +
3.932 +lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
3.933 +by(simp add: expand_finfun_eq fun_eq_iff)
3.934 +
3.935 +lemma finfun_const_eq_update:
3.936 + "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
3.937 +by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
3.938 +
3.939 +subsection {* Function composition *}
3.940 +
3.941 +definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
3.942 +where [code del]: "g \<circ>\<^isub>f f = finfun_rec (\<lambda>b. (\<lambda>\<^isup>f g b)) (\<lambda>a b c. c(\<^sup>f a := g b)) f"
3.943 +
3.944 +interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
3.945 +by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
3.946 +
3.947 +interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
3.948 +proof
3.949 + fix b' b :: 'a
3.950 + assume fin: "finite (UNIV :: 'c set)"
3.951 + { fix A :: "'c set"
3.952 + from fin have "finite A" by(auto intro: finite_subset)
3.953 + hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
3.954 + Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
3.955 + by induct (simp_all add: finfun_const_def, auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
3.956 + from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')"
3.957 + by(simp add: finfun_const_def)
3.958 +qed
3.959 +
3.960 +lemma finfun_comp_const [simp, code]:
3.961 + "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
3.962 +by(simp add: finfun_comp_def)
3.963 +
3.964 +lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
3.965 + and finfun_comp_update_code [code]: "g \<circ>\<^isub>f (finfun_update_code f a b) = finfun_update_code (g \<circ>\<^isub>f f) a (g b)"
3.966 +by(simp_all add: finfun_comp_def)
3.967 +
3.968 +lemma finfun_comp_apply [simp]:
3.969 + "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
3.970 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
3.971 +
3.972 +lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
3.973 +by(induct h rule: finfun_weak_induct) simp_all
3.974 +
3.975 +lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
3.976 +by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
3.977 +
3.978 +lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
3.979 +by(induct f rule: finfun_weak_induct) auto
3.980 +
3.981 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.982 +
3.983 +lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
3.984 +proof -
3.985 + have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
3.986 + proof(rule finfun_rec_unique)
3.987 + { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
3.988 + by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
3.989 + { fix g' a b show "Abs_finfun (g \<circ> g'(\<^sup>f a := b)\<^sub>f) = (Abs_finfun (g \<circ> g'\<^sub>f))(\<^sup>f a := g b)"
3.990 + proof -
3.991 + obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
3.992 + moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
3.993 + moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
3.994 + ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
3.995 + qed }
3.996 + qed auto
3.997 + thus ?thesis by(auto simp add: fun_eq_iff)
3.998 +qed
3.999 +
3.1000 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.1001 +
3.1002 +definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
3.1003 +where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
3.1004 +
3.1005 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.1006 +
3.1007 +lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
3.1008 +by(simp add: finfun_comp2_def finfun_const_def comp_def)
3.1009 +
3.1010 +lemma finfun_comp2_update:
3.1011 + assumes inj: "inj f"
3.1012 + shows "finfun_comp2 (g(\<^sup>f b := c)) f = (if b \<in> range f then (finfun_comp2 g f)(\<^sup>f inv f b := c) else finfun_comp2 g f)"
3.1013 +proof(cases "b \<in> range f")
3.1014 + case True
3.1015 + from inj have "\<And>x. (Rep_finfun g)(f x := c) \<circ> f = (Rep_finfun g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
3.1016 + with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
3.1017 +next
3.1018 + case False
3.1019 + hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: fun_eq_iff)
3.1020 + with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
3.1021 +qed
3.1022 +
3.1023 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.1024 +
3.1025 +
3.1026 +
3.1027 +subsection {* Universal quantification *}
3.1028 +
3.1029 +definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
3.1030 +where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
3.1031 +
3.1032 +lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
3.1033 +by(auto simp add: finfun_All_except_def)
3.1034 +
3.1035 +lemma finfun_All_except_const_finfun_UNIV_code [code]:
3.1036 + "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
3.1037 +by(simp add: finfun_All_except_const is_list_UNIV_iff)
3.1038 +
3.1039 +lemma finfun_All_except_update:
3.1040 + "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
3.1041 +by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
3.1042 +
3.1043 +lemma finfun_All_except_update_code [code]:
3.1044 + fixes a :: "'a :: card_UNIV"
3.1045 + shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
3.1046 +by(simp add: finfun_All_except_update)
3.1047 +
3.1048 +definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
3.1049 +where "finfun_All = finfun_All_except []"
3.1050 +
3.1051 +lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
3.1052 +by(simp add: finfun_All_def finfun_All_except_def)
3.1053 +
3.1054 +lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
3.1055 +by(simp add: finfun_All_def finfun_All_except_update)
3.1056 +
3.1057 +lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
3.1058 +by(simp add: finfun_All_def finfun_All_except_def)
3.1059 +
3.1060 +
3.1061 +definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
3.1062 +where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
3.1063 +
3.1064 +lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
3.1065 +unfolding finfun_Ex_def finfun_All_All by simp
3.1066 +
3.1067 +lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
3.1068 +by(simp add: finfun_Ex_def)
3.1069 +
3.1070 +
3.1071 +subsection {* A diagonal operator for FinFuns *}
3.1072 +
3.1073 +definition finfun_Diag :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
3.1074 +where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))) f"
3.1075 +
3.1076 +interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
3.1077 +by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
3.1078 +
3.1079 +interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
3.1080 +proof
3.1081 + fix b' b :: 'a
3.1082 + assume fin: "finite (UNIV :: 'c set)"
3.1083 + { fix A :: "'c set"
3.1084 + interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
3.1085 + from fin have "finite A" by(auto intro: finite_subset)
3.1086 + hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
3.1087 + Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
3.1088 + by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
3.1089 + auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
3.1090 + from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
3.1091 + by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
3.1092 +qed
3.1093 +
3.1094 +lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
3.1095 +by(simp add: finfun_Diag_def)
3.1096 +
3.1097 +text {*
3.1098 + Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{text "\<circ>\<^isub>f"}.
3.1099 +*}
3.1100 +
3.1101 +lemma finfun_Diag_const_code [code]:
3.1102 + "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
3.1103 + "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
3.1104 +by(simp_all add: finfun_Diag_const1)
3.1105 +
3.1106 +lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
3.1107 + and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
3.1108 +by(simp_all add: finfun_Diag_def)
3.1109 +
3.1110 +lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
3.1111 +by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
3.1112 +
3.1113 +lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
3.1114 +by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
3.1115 +
3.1116 +lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
3.1117 +by(simp add: finfun_Diag_const1)
3.1118 +
3.1119 +lemma finfun_Diag_const_update:
3.1120 + "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
3.1121 +by(simp add: finfun_Diag_const1)
3.1122 +
3.1123 +lemma finfun_Diag_update_const:
3.1124 + "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
3.1125 +by(simp add: finfun_Diag_def)
3.1126 +
3.1127 +lemma finfun_Diag_update_update:
3.1128 + "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))(\<^sup>f a' := (f\<^sub>f a', c)))"
3.1129 +by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
3.1130 +
3.1131 +lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
3.1132 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
3.1133 +
3.1134 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.1135 +
3.1136 +lemma finfun_Diag_conv_Abs_finfun:
3.1137 + "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
3.1138 +proof -
3.1139 + have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x))))"
3.1140 + proof(rule finfun_rec_unique)
3.1141 + { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g"
3.1142 + by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
3.1143 + { fix g' a b
3.1144 + show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
3.1145 + (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
3.1146 + by(auto simp add: finfun_update_def fun_eq_iff finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
3.1147 + qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
3.1148 + thus ?thesis by(auto simp add: fun_eq_iff)
3.1149 +qed
3.1150 +
3.1151 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.1152 +
3.1153 +lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
3.1154 +by(auto simp add: expand_finfun_eq fun_eq_iff)
3.1155 +
3.1156 +definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
3.1157 +where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
3.1158 +
3.1159 +lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
3.1160 +by(simp add: finfun_fst_def)
3.1161 +
3.1162 +lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
3.1163 + and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
3.1164 +by(simp_all add: finfun_fst_def)
3.1165 +
3.1166 +lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
3.1167 +by(simp add: finfun_fst_def)
3.1168 +
3.1169 +lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
3.1170 +by(induct f rule: finfun_weak_induct)(simp_all add: finfun_Diag_const1 finfun_fst_comp_conv o_def finfun_Diag_update1 finfun_fst_update)
3.1171 +
3.1172 +lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
3.1173 +by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
3.1174 +
3.1175 +
3.1176 +definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
3.1177 +where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
3.1178 +
3.1179 +lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
3.1180 +by(simp add: finfun_snd_def)
3.1181 +
3.1182 +lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
3.1183 + and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
3.1184 +by(simp_all add: finfun_snd_def)
3.1185 +
3.1186 +lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
3.1187 +by(simp add: finfun_snd_def)
3.1188 +
3.1189 +lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
3.1190 +apply(induct f rule: finfun_weak_induct)
3.1191 +apply(auto simp add: finfun_Diag_const1 finfun_snd_comp_conv o_def finfun_Diag_update1 finfun_snd_update finfun_upd_apply intro: finfun_ext)
3.1192 +done
3.1193 +
3.1194 +lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
3.1195 +by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
3.1196 +
3.1197 +lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
3.1198 +by(induct f rule: finfun_weak_induct)(simp_all add: finfun_fst_const finfun_snd_const finfun_fst_update finfun_snd_update finfun_Diag_update_update)
3.1199 +
3.1200 +subsection {* Currying for FinFuns *}
3.1201 +
3.1202 +definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
3.1203 +where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c)))"
3.1204 +
3.1205 +interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
3.1206 +apply(unfold_locales)
3.1207 +apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
3.1208 +done
3.1209 +
3.1210 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.1211 +
3.1212 +interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
3.1213 +proof(unfold_locales)
3.1214 + fix b' b :: 'b
3.1215 + assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
3.1216 + hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
3.1217 + unfolding UNIV_Times_UNIV[symmetric]
3.1218 + by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
3.1219 + note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
3.1220 + { fix A :: "('c \<times> 'a) set"
3.1221 + interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'"
3.1222 + by(rule finfun_curry_aux.upd_left_comm)
3.1223 + from fin have "finite A" by(auto intro: finite_subset)
3.1224 + hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))"
3.1225 + by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def finfun_apply_Rep_finfun intro!: arg_cong[where f="Abs_finfun"] ext) }
3.1226 + from this[of UNIV]
3.1227 + show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
3.1228 + by(simp add: finfun_const_def)
3.1229 +qed
3.1230 +
3.1231 +declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
3.1232 +
3.1233 +lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
3.1234 +by(simp add: finfun_curry_def)
3.1235 +
3.1236 +lemma finfun_curry_update [simp]:
3.1237 + "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
3.1238 + and finfun_curry_update_code [code]:
3.1239 + "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
3.1240 +by(simp_all add: finfun_curry_def)
3.1241 +
3.1242 +declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
3.1243 +
3.1244 +lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
3.1245 + shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
3.1246 +proof -
3.1247 + from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
3.1248 + have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
3.1249 + hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
3.1250 + by(auto simp add: curry_def fun_eq_iff)
3.1251 + with fin c have "finite {a. Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
3.1252 + by(simp add: finfun_const_def finfun_curry)
3.1253 + thus ?thesis unfolding finfun_def by auto
3.1254 +qed
3.1255 +
3.1256 +lemma finfun_curry_conv_curry:
3.1257 + fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
3.1258 + shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
3.1259 +proof -
3.1260 + have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
3.1261 + proof(rule finfun_rec_unique)
3.1262 + { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
3.1263 + { fix f a c show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))"
3.1264 + by(cases a) simp }
3.1265 + { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
3.1266 + by(simp add: finfun_curry_def finfun_const_def curry_def) }
3.1267 + { fix g a b
3.1268 + show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
3.1269 + (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
3.1270 + fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
3.1271 + by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_apply_Rep_finfun finfun_curry finfun_Abs_finfun_curry) }
3.1272 + qed
3.1273 + thus ?thesis by(auto simp add: fun_eq_iff)
3.1274 +qed
3.1275 +
3.1276 +subsection {* Executable equality for FinFuns *}
3.1277 +
3.1278 +lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
3.1279 +by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
3.1280 +
3.1281 +instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
3.1282 +definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
3.1283 +instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
3.1284 +end
3.1285 +
3.1286 +lemma [code nbe]:
3.1287 + "HOL.equal (f :: _ \<Rightarrow>\<^isub>f _) f \<longleftrightarrow> True"
3.1288 + by (fact equal_refl)
3.1289 +
3.1290 +subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
3.1291 +
3.1292 +definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
3.1293 +where [simp, code del]: "finfun_clearjunk = id"
3.1294 +
3.1295 +lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
3.1296 +by simp
3.1297 +
3.1298 +lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
3.1299 +by simp
3.1300 +
3.1301 +subsection {* The domain of a FinFun as a FinFun *}
3.1302 +
3.1303 +definition finfun_dom :: "('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> ('a \<Rightarrow>\<^isub>f bool)"
3.1304 +where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
3.1305 +
3.1306 +lemma finfun_dom_const:
3.1307 + "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
3.1308 +unfolding finfun_dom_def finfun_default_const
3.1309 +by(auto)(simp_all add: finfun_const_def)
3.1310 +
3.1311 +text {*
3.1312 + @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type.
3.1313 + For such FinFuns, the default value (and as such the domain) is undefined.
3.1314 +*}
3.1315 +
3.1316 +lemma finfun_dom_const_code [code]:
3.1317 + "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) =
3.1318 + (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
3.1319 +unfolding card_UNIV_eq_0_infinite_UNIV
3.1320 +by(simp add: finfun_dom_const)
3.1321 +
3.1322 +lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
3.1323 +using finite_finfun_default[of f]
3.1324 +by(simp add: finfun_def finfun_apply_Rep_finfun exI[where x=False])
3.1325 +
3.1326 +lemma finfun_dom_update [simp]:
3.1327 + "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
3.1328 +unfolding finfun_dom_def finfun_update_def
3.1329 +apply(simp add: finfun_default_update_const finfun_upd_apply finfun_dom_finfunI)
3.1330 +apply(fold finfun_update.rep_eq)
3.1331 +apply(simp add: finfun_upd_apply fun_eq_iff finfun_default_update_const)
3.1332 +done
3.1333 +
3.1334 +lemma finfun_dom_update_code [code]:
3.1335 + "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
3.1336 +by(simp)
3.1337 +
3.1338 +lemma finite_finfun_dom: "finite {x. (finfun_dom f)\<^sub>f x}"
3.1339 +proof(induct f rule: finfun_weak_induct)
3.1340 + case (const b)
3.1341 + thus ?case
3.1342 + by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined")
3.1343 + (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
3.1344 +next
3.1345 + case (update f a b)
3.1346 + have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} =
3.1347 + (if b = finfun_default f then {x. (finfun_dom f)\<^sub>f x} - {a} else insert a {x. (finfun_dom f)\<^sub>f x})"
3.1348 + by (auto simp add: finfun_upd_apply split: split_if_asm)
3.1349 + thus ?case using update by simp
3.1350 +qed
3.1351 +
3.1352 +
3.1353 +subsection {* The domain of a FinFun as a sorted list *}
3.1354 +
3.1355 +definition finfun_to_list :: "('a :: linorder) \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a list"
3.1356 +where
3.1357 + "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
3.1358 +
3.1359 +lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. (finfun_dom f)\<^sub>f x}" (is ?thesis1)
3.1360 + and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
3.1361 + and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
3.1362 +proof -
3.1363 + have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
3.1364 + unfolding finfun_to_list_def
3.1365 + by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
3.1366 + thus ?thesis1 ?thesis2 ?thesis3 by simp_all
3.1367 +qed
3.1368 +
3.1369 +lemma finfun_const_False_conv_bot: "(\<lambda>\<^isup>f False)\<^sub>f = bot"
3.1370 +by auto
3.1371 +
3.1372 +lemma finfun_const_True_conv_top: "(\<lambda>\<^isup>f True)\<^sub>f = top"
3.1373 +by auto
3.1374 +
3.1375 +lemma finfun_to_list_const:
3.1376 + "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>\<^isub>f 'b)) =
3.1377 + (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
3.1378 +by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
3.1379 +
3.1380 +lemma finfun_to_list_const_code [code]:
3.1381 + "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>\<^isub>f 'b)) =
3.1382 + (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>\<^isub>f 'b))))"
3.1383 +unfolding card_UNIV_eq_0_infinite_UNIV
3.1384 +by(auto simp add: finfun_to_list_const)
3.1385 +
3.1386 +lemma remove1_insort_insert_same:
3.1387 + "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
3.1388 +by (metis insort_insert_insort remove1_insort)
3.1389 +
3.1390 +lemma finfun_dom_conv:
3.1391 + "(finfun_dom f)\<^sub>f x \<longleftrightarrow> f\<^sub>f x \<noteq> finfun_default f"
3.1392 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
3.1393 +
3.1394 +lemma finfun_to_list_update:
3.1395 + "finfun_to_list (f(\<^sup>f a := b)) =
3.1396 + (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
3.1397 +proof(subst finfun_to_list_def, rule the_equality)
3.1398 + fix xs
3.1399 + assume "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} \<and> sorted xs \<and> distinct xs"
3.1400 + hence eq: "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x}"
3.1401 + and [simp]: "sorted xs" "distinct xs" by simp_all
3.1402 + show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
3.1403 + proof(cases "b = finfun_default f")
3.1404 + case True [simp]
3.1405 + show ?thesis
3.1406 + proof(cases "(finfun_dom f)\<^sub>f a")
3.1407 + case True
3.1408 + have "finfun_to_list f = insort_insert a xs"
3.1409 + unfolding finfun_to_list_def
3.1410 + proof(rule the_equality)
3.1411 + have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
3.1412 + also note eq also
3.1413 + have "insert a {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} = {x. (finfun_dom f)\<^sub>f x}" using True
3.1414 + by(auto simp add: finfun_upd_apply split: split_if_asm)
3.1415 + finally show 1: "set (insort_insert a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
3.1416 + by(simp add: sorted_insort_insert distinct_insort_insert)
3.1417 +
3.1418 + fix xs'
3.1419 + assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
3.1420 + thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
3.1421 + qed
3.1422 + with eq True show ?thesis by(simp add: remove1_insort_insert_same)
3.1423 + next
3.1424 + case False
3.1425 + hence "f\<^sub>f a = b" by(auto simp add: finfun_dom_conv)
3.1426 + hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
3.1427 + from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
3.1428 + by(auto elim: sorted_distinct_set_unique intro!: the_equality)
3.1429 + with eq False show ?thesis unfolding f by(simp add: remove1_idem)
3.1430 + qed
3.1431 + next
3.1432 + case False
3.1433 + show ?thesis
3.1434 + proof(cases "(finfun_dom f)\<^sub>f a")
3.1435 + case True
3.1436 + have "finfun_to_list f = xs"
3.1437 + unfolding finfun_to_list_def
3.1438 + proof(rule the_equality)
3.1439 + have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
3.1440 + by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
3.1441 + with eq show 1: "set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs"
3.1442 + by(simp del: finfun_dom_update)
3.1443 +
3.1444 + fix xs'
3.1445 + assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
3.1446 + thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
3.1447 + qed
3.1448 + thus ?thesis using False True eq by(simp add: insort_insert_triv)
3.1449 + next
3.1450 + case False
3.1451 + have "finfun_to_list f = remove1 a xs"
3.1452 + unfolding finfun_to_list_def
3.1453 + proof(rule the_equality)
3.1454 + have "set (remove1 a xs) = set xs - {a}" by simp
3.1455 + also note eq also
3.1456 + have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} - {a} = {x. (finfun_dom f)\<^sub>f x}" using False
3.1457 + by(auto simp add: finfun_upd_apply split: split_if_asm)
3.1458 + finally show 1: "set (remove1 a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
3.1459 + by(simp add: sorted_remove1)
3.1460 +
3.1461 + fix xs'
3.1462 + assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
3.1463 + thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
3.1464 + qed
3.1465 + thus ?thesis using False eq `b \<noteq> finfun_default f`
3.1466 + by (simp add: insort_insert_insort insort_remove1)
3.1467 + qed
3.1468 + qed
3.1469 +qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: split_if_asm)
3.1470 +
3.1471 +lemma finfun_to_list_update_code [code]:
3.1472 + "finfun_to_list (finfun_update_code f a b) =
3.1473 + (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
3.1474 +by(simp add: finfun_to_list_update)
3.1475 +
3.1476 +end
4.1 --- a/src/HOL/Library/Library.thy Tue May 29 13:46:50 2012 +0200
4.2 +++ b/src/HOL/Library/Library.thy Tue May 29 15:31:58 2012 +0200
4.3 @@ -14,6 +14,7 @@
4.4 Countable
4.5 Eval_Witness
4.6 Extended_Nat
4.7 + FinFun
4.8 Float
4.9 Formal_Power_Series
4.10 Fraction_Field
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/ex/FinFunPred.thy Tue May 29 15:31:58 2012 +0200
5.3 @@ -0,0 +1,261 @@
5.4 +(* Author: Andreas Lochbihler *)
5.5 +
5.6 +header {*
5.7 + Predicates modelled as FinFuns
5.8 +*}
5.9 +
5.10 +theory FinFunPred imports "~~/src/HOL/Library/FinFun" begin
5.11 +
5.12 +text {* Instantiate FinFun predicates just like predicates *}
5.13 +
5.14 +type_synonym 'a pred\<^isub>f = "'a \<Rightarrow>\<^isub>f bool"
5.15 +
5.16 +instantiation "finfun" :: (type, ord) ord
5.17 +begin
5.18 +
5.19 +definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f\<^sub>f x \<le> g\<^sub>f x)"
5.20 +
5.21 +definition [code del]: "(f\<Colon>'a \<Rightarrow>\<^isub>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
5.22 +
5.23 +instance ..
5.24 +
5.25 +lemma le_finfun_code [code]:
5.26 + "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>\<^isub>f (f, g)\<^sup>f)"
5.27 +by(simp add: le_finfun_def finfun_All_All o_def)
5.28 +
5.29 +end
5.30 +
5.31 +instance "finfun" :: (type, preorder) preorder
5.32 + by(intro_classes)(auto simp add: less_finfun_def le_finfun_def intro: order_trans)
5.33 +
5.34 +instance "finfun" :: (type, order) order
5.35 +by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext)
5.36 +
5.37 +instantiation "finfun" :: (type, bot) bot begin
5.38 +definition "bot = finfun_const bot"
5.39 +instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
5.40 +end
5.41 +
5.42 +lemma bot_finfun_apply [simp]: "bot\<^sub>f = (\<lambda>_. bot)"
5.43 +by(auto simp add: bot_finfun_def)
5.44 +
5.45 +instantiation "finfun" :: (type, top) top begin
5.46 +definition "top = finfun_const top"
5.47 +instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
5.48 +end
5.49 +
5.50 +lemma top_finfun_apply [simp]: "top\<^sub>f = (\<lambda>_. top)"
5.51 +by(auto simp add: top_finfun_def)
5.52 +
5.53 +instantiation "finfun" :: (type, inf) inf begin
5.54 +definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>\<^isub>f (f, g)\<^sup>f"
5.55 +instance ..
5.56 +end
5.57 +
5.58 +lemma inf_finfun_apply [simp]: "(inf f g)\<^sub>f = inf f\<^sub>f g\<^sub>f"
5.59 +by(auto simp add: inf_finfun_def o_def inf_fun_def)
5.60 +
5.61 +instantiation "finfun" :: (type, sup) sup begin
5.62 +definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>\<^isub>f (f, g)\<^sup>f"
5.63 +instance ..
5.64 +end
5.65 +
5.66 +lemma sup_finfun_apply [simp]: "(sup f g)\<^sub>f = sup f\<^sub>f g\<^sub>f"
5.67 +by(auto simp add: sup_finfun_def o_def sup_fun_def)
5.68 +
5.69 +instance "finfun" :: (type, semilattice_inf) semilattice_inf
5.70 +by(intro_classes)(simp_all add: inf_finfun_def le_finfun_def)
5.71 +
5.72 +instance "finfun" :: (type, semilattice_sup) semilattice_sup
5.73 +by(intro_classes)(simp_all add: sup_finfun_def le_finfun_def)
5.74 +
5.75 +instance "finfun" :: (type, lattice) lattice ..
5.76 +
5.77 +instance "finfun" :: (type, bounded_lattice) bounded_lattice
5.78 +by(intro_classes)
5.79 +
5.80 +instance "finfun" :: (type, distrib_lattice) distrib_lattice
5.81 +by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)
5.82 +
5.83 +instantiation "finfun" :: (type, minus) minus begin
5.84 +definition "f - g = split (op -) \<circ>\<^isub>f (f, g)\<^sup>f"
5.85 +instance ..
5.86 +end
5.87 +
5.88 +lemma minus_finfun_apply [simp]: "(f - g)\<^sub>f = f\<^sub>f - g\<^sub>f"
5.89 +by(simp add: minus_finfun_def o_def fun_diff_def)
5.90 +
5.91 +instantiation "finfun" :: (type, uminus) uminus begin
5.92 +definition "- A = uminus \<circ>\<^isub>f A"
5.93 +instance ..
5.94 +end
5.95 +
5.96 +lemma uminus_finfun_apply [simp]: "(- g)\<^sub>f = - g\<^sub>f"
5.97 +by(simp add: uminus_finfun_def o_def fun_Compl_def)
5.98 +
5.99 +instance "finfun" :: (type, boolean_algebra) boolean_algebra
5.100 +by(intro_classes)
5.101 + (simp_all add: uminus_finfun_def inf_finfun_def expand_finfun_eq sup_fun_def inf_fun_def fun_Compl_def o_def inf_compl_bot sup_compl_top diff_eq)
5.102 +
5.103 +text {*
5.104 + Replicate predicate operations for FinFuns
5.105 +*}
5.106 +
5.107 +abbreviation finfun_empty :: "'a pred\<^isub>f" ("{}\<^isub>f")
5.108 +where "{}\<^isub>f \<equiv> bot"
5.109 +
5.110 +abbreviation finfun_UNIV :: "'a pred\<^isub>f"
5.111 +where "finfun_UNIV \<equiv> top"
5.112 +
5.113 +definition finfun_single :: "'a \<Rightarrow> 'a pred\<^isub>f"
5.114 +where [code]: "finfun_single x = finfun_empty(\<^sup>f x := True)"
5.115 +
5.116 +lemma finfun_single_apply [simp]:
5.117 + "(finfun_single x)\<^sub>f y \<longleftrightarrow> x = y"
5.118 +by(simp add: finfun_single_def finfun_upd_apply)
5.119 +
5.120 +lemma [iff]:
5.121 + shows finfun_single_neq_bot: "finfun_single x \<noteq> bot"
5.122 + and bot_neq_finfun_single: "bot \<noteq> finfun_single x"
5.123 +by(simp_all add: expand_finfun_eq fun_eq_iff)
5.124 +
5.125 +lemma finfun_leI [intro!]: "(!!x. A\<^sub>f x \<Longrightarrow> B\<^sub>f x) \<Longrightarrow> A \<le> B"
5.126 +by(simp add: le_finfun_def)
5.127 +
5.128 +lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A\<^sub>f x \<rbrakk> \<Longrightarrow> B\<^sub>f x"
5.129 +by(simp add: le_finfun_def)
5.130 +
5.131 +text {* Bounded quantification.
5.132 + Warning: @{text "finfun_Ball"} and @{text "finfun_Ex"} may raise an exception, they should not be used for quickcheck
5.133 +*}
5.134 +
5.135 +definition finfun_Ball_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
5.136 +where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A\<^sub>f a \<longrightarrow> a \<in> set xs \<or> P a)"
5.137 +
5.138 +lemma finfun_Ball_except_const:
5.139 + "finfun_Ball_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (\<lambda>\<^isup>f b) P)"
5.140 +by(auto simp add: finfun_Ball_except_def)
5.141 +
5.142 +lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
5.143 + "finfun_Ball_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (\<lambda>\<^isup>f b) P)"
5.144 +by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff)
5.145 +
5.146 +lemma finfun_Ball_except_update:
5.147 + "finfun_Ball_except xs (A(\<^sup>f a := b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)"
5.148 +by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: split_if_asm)
5.149 +
5.150 +lemma finfun_Ball_except_update_code [code]:
5.151 + fixes a :: "'a :: card_UNIV"
5.152 + shows "finfun_Ball_except xs (finfun_update_code f a b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) f P)"
5.153 +by(simp add: finfun_Ball_except_update)
5.154 +
5.155 +definition finfun_Ball :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
5.156 +where [code del]: "finfun_Ball A P = Ball {x. A\<^sub>f x} P"
5.157 +
5.158 +lemma finfun_Ball_code [code]: "finfun_Ball = finfun_Ball_except []"
5.159 +by(auto intro!: ext simp add: finfun_Ball_except_def finfun_Ball_def)
5.160 +
5.161 +
5.162 +definition finfun_Bex_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
5.163 +where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A\<^sub>f a \<and> a \<notin> set xs \<and> P a)"
5.164 +
5.165 +lemma finfun_Bex_except_const:
5.166 + "finfun_Bex_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (\<lambda>\<^isup>f b) P)"
5.167 +by(auto simp add: finfun_Bex_except_def)
5.168 +
5.169 +lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
5.170 + "finfun_Bex_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (\<lambda>\<^isup>f b) P)"
5.171 +by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff)
5.172 +
5.173 +lemma finfun_Bex_except_update:
5.174 + "finfun_Bex_except xs (A(\<^sup>f a := b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P"
5.175 +by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: split_if_asm)
5.176 +
5.177 +lemma finfun_Bex_except_update_code [code]:
5.178 + fixes a :: "'a :: card_UNIV"
5.179 + shows "finfun_Bex_except xs (finfun_update_code f a b) P \<longleftrightarrow> ((a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) f P)"
5.180 +by(simp add: finfun_Bex_except_update)
5.181 +
5.182 +definition finfun_Bex :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
5.183 +where [code del]: "finfun_Bex A P = Bex {x. A\<^sub>f x} P"
5.184 +
5.185 +lemma finfun_Bex_code [code]: "finfun_Bex = finfun_Bex_except []"
5.186 +by(auto intro!: ext simp add: finfun_Bex_except_def finfun_Bex_def)
5.187 +
5.188 +
5.189 +text {* Automatically replace predicate operations by finfun predicate operations where possible *}
5.190 +
5.191 +lemma iso_finfun_le [code_unfold]:
5.192 + "A\<^sub>f \<le> B\<^sub>f \<longleftrightarrow> A \<le> B"
5.193 +by (metis le_finfun_def le_funD le_funI)
5.194 +
5.195 +lemma iso_finfun_less [code_unfold]:
5.196 + "A\<^sub>f < B\<^sub>f \<longleftrightarrow> A < B"
5.197 +by (metis iso_finfun_le less_finfun_def less_fun_def)
5.198 +
5.199 +lemma iso_finfun_eq [code_unfold]:
5.200 + "A\<^sub>f = B\<^sub>f \<longleftrightarrow> A = B"
5.201 +by(simp add: expand_finfun_eq)
5.202 +
5.203 +lemma iso_finfun_sup [code_unfold]:
5.204 + "sup A\<^sub>f B\<^sub>f = (sup A B)\<^sub>f"
5.205 +by(simp)
5.206 +
5.207 +lemma iso_finfun_disj [code_unfold]:
5.208 + "A\<^sub>f x \<or> B\<^sub>f x \<longleftrightarrow> (sup A B)\<^sub>f x"
5.209 +by(simp add: sup_fun_def)
5.210 +
5.211 +lemma iso_finfun_inf [code_unfold]:
5.212 + "inf A\<^sub>f B\<^sub>f = (inf A B)\<^sub>f"
5.213 +by(simp)
5.214 +
5.215 +lemma iso_finfun_conj [code_unfold]:
5.216 + "A\<^sub>f x \<and> B\<^sub>f x \<longleftrightarrow> (inf A B)\<^sub>f x"
5.217 +by(simp add: inf_fun_def)
5.218 +
5.219 +lemma iso_finfun_empty_conv [code_unfold]:
5.220 + "(\<lambda>_. False) = {}\<^isub>f\<^sub>f"
5.221 +by simp
5.222 +
5.223 +lemma iso_finfun_UNIV_conv [code_unfold]:
5.224 + "(\<lambda>_. True) = finfun_UNIV\<^sub>f"
5.225 +by simp
5.226 +
5.227 +lemma iso_finfun_upd [code_unfold]:
5.228 + fixes A :: "'a pred\<^isub>f"
5.229 + shows "A\<^sub>f(x := b) = (A(\<^sup>f x := b))\<^sub>f"
5.230 +by(simp add: fun_eq_iff)
5.231 +
5.232 +lemma iso_finfun_uminus [code_unfold]:
5.233 + fixes A :: "'a pred\<^isub>f"
5.234 + shows "- A\<^sub>f = (- A)\<^sub>f"
5.235 +by(simp)
5.236 +
5.237 +lemma iso_finfun_minus [code_unfold]:
5.238 + fixes A :: "'a pred\<^isub>f"
5.239 + shows "A\<^sub>f - B\<^sub>f = (A - B)\<^sub>f"
5.240 +by(simp)
5.241 +
5.242 +text {*
5.243 + Do not declare the following two theorems as @{text "[code_unfold]"},
5.244 + because this causes quickcheck to fail frequently when bounded quantification is used which raises an exception.
5.245 + For code generation, the same problems occur, but then, no randomly generated FinFun is usually around.
5.246 +*}
5.247 +
5.248 +lemma iso_finfun_Ball_Ball:
5.249 + "(\<forall>x. A\<^sub>f x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
5.250 +by(simp add: finfun_Ball_def)
5.251 +
5.252 +lemma iso_finfun_Bex_Bex:
5.253 + "(\<exists>x. A\<^sub>f x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
5.254 +by(simp add: finfun_Bex_def)
5.255 +
5.256 +text {* Test replacement setup *}
5.257 +
5.258 +notepad begin
5.259 +have "inf ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) ((\<lambda>_. True)(3 := False)) \<le>
5.260 + sup ((\<lambda>_. False)(1 := True, 5 := True)) (- ((\<lambda>_. True)(2 := False, 3 := False)))"
5.261 + by eval
5.262 +end
5.263 +
5.264 +end
5.265 \ No newline at end of file
6.1 --- a/src/HOL/ex/ROOT.ML Tue May 29 13:46:50 2012 +0200
6.2 +++ b/src/HOL/ex/ROOT.ML Tue May 29 15:31:58 2012 +0200
6.3 @@ -11,7 +11,8 @@
6.4 "Normalization_by_Evaluation",
6.5 "Hebrew",
6.6 "Chinese",
6.7 - "Serbian"
6.8 + "Serbian",
6.9 + "~~/src/HOL/Library/FinFun"
6.10 ];
6.11
6.12 use_thys [
6.13 @@ -70,7 +71,8 @@
6.14 "List_to_Set_Comprehension_Examples",
6.15 "Seq",
6.16 "Simproc_Tests",
6.17 - "Executable_Relation"
6.18 + "Executable_Relation",
6.19 + "FinFunPred"
6.20 ];
6.21
6.22 use_thy "SVC_Oracle";